Theorem: IMOSL.IMO2012A5.𝔽₂X.square_XpowMul (IMOSLLean4/Extra/F2X/Defs.lean)

State before:
n : ℕ
P : 𝔽₂X
⊢ (XpowMul n P).square = XpowMul (2 * n) P.square
Tactic:
unfold square XpowMul
State after:
n : ℕ
P : 𝔽₂X
⊢ { toFinset := Finset.image (fun n => 2 * n) { toFinset := Finset.image (fun k => k + n) P.toFinset }.toFinset } =
    { toFinset := Finset.image (fun k => k + 2 * n) { toFinset := Finset.image (fun n => 2 * n) P.toFinset }.toFinset }

State before:
n : ℕ
P : 𝔽₂X
⊢ { toFinset := Finset.image (fun n => 2 * n) { toFinset := Finset.image (fun k => k + n) P.toFinset }.toFinset } =
    { toFinset := Finset.image (fun k => k + 2 * n) { toFinset := Finset.image (fun n => 2 * n) P.toFinset }.toFinset }
Tactic:
rw [Finset.image_image, Finset.image_image]
State after:
n : ℕ
P : 𝔽₂X
⊢ { toFinset := Finset.image ((fun n => 2 * n) ∘ fun k => k + n) P.toFinset } =
    { toFinset := Finset.image ((fun k => k + 2 * n) ∘ fun n => 2 * n) P.toFinset }

State before:
n : ℕ
P : 𝔽₂X
⊢ { toFinset := Finset.image ((fun n => 2 * n) ∘ fun k => k + n) P.toFinset } =
    { toFinset := Finset.image ((fun k => k + 2 * n) ∘ fun n => 2 * n) P.toFinset }
Tactic:
exact 𝔽₂X.ext _ _ (congrArg P.toFinset.image <| funext λ n ↦ Nat.mul_add 2 _ _)
State after:
no goals