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

State before:
P : 𝔽₂X
n : ℕ
⊢ P.natPow (2 * n) = P.square.natPow n
Tactic:
rcases Decidable.eq_or_ne n 0 with rfl | h
State after:
case inl
P : 𝔽₂X
⊢ P.natPow (2 * 0) = P.square.natPow 0

case inr
P : 𝔽₂X
n : ℕ
h : n ≠ 0
⊢ P.natPow (2 * n) = P.square.natPow n

State before:
case inl
P : 𝔽₂X
⊢ P.natPow (2 * 0) = P.square.natPow 0
Tactic:
rw [Nat.mul_zero, 𝔽₂X.natPow_zero, 𝔽₂X.natPow_zero]
State after:
no goals

State before:
case inr
P : 𝔽₂X
n : ℕ
h : n ≠ 0
⊢ P.natPow (2 * n) = P.square.natPow n
Tactic:
have h0 : 0 < 2 := Nat.two_pos
State after:
case inr
P : 𝔽₂X
n : ℕ
h : n ≠ 0
h0 : 0 < 2
⊢ P.natPow (2 * n) = P.square.natPow n

State before:
case inr
P : 𝔽₂X
n : ℕ
h : n ≠ 0
h0 : 0 < 2
⊢ P.natPow (2 * n) = P.square.natPow n
Tactic:
rw [P.natPow_of_ne_zero (Nat.mul_ne_zero h0.ne.symm h),
  if_pos (Nat.mul_mod_right _ _), Nat.mul_div_right _ h0]
State after:
no goals