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

State before:
P : 𝔽₂X
n : ℕ
⊢ P.natPow n.succ = P.natPow n * P
Tactic:
rw [← n.div_add_mod 2]
State after:
P : 𝔽₂X
n : ℕ
⊢ P.natPow (2 * (n / 2) + n % 2).succ = P.natPow (2 * (n / 2) + n % 2) * P

State before:
P : 𝔽₂X
n : ℕ
⊢ P.natPow (2 * (n / 2) + n % 2).succ = P.natPow (2 * (n / 2) + n % 2) * P
Tactic:
rcases n.mod_two_eq_zero_or_one with h0 | h0
State after:
case inl
P : 𝔽₂X
n : ℕ
h0 : n % 2 = 0
⊢ P.natPow (2 * (n / 2) + n % 2).succ = P.natPow (2 * (n / 2) + n % 2) * P

case inr
P : 𝔽₂X
n : ℕ
h0 : n % 2 = 1
⊢ P.natPow (2 * (n / 2) + n % 2).succ = P.natPow (2 * (n / 2) + n % 2) * P

State before:
case inl
P : 𝔽₂X
n : ℕ
h0 : n % 2 = 0
⊢ P.natPow (2 * (n / 2) + n % 2).succ = P.natPow (2 * (n / 2) + n % 2) * P
Tactic:
rw [h0, Nat.add_zero, 𝔽₂X.natPow_two_mul_add_one, 𝔽₂X.natPow_two_mul]
State after:
no goals

State before:
case inr
P : 𝔽₂X
n : ℕ
h0 : n % 2 = 1
⊢ P.natPow (2 * (n / 2) + n % 2).succ = P.natPow (2 * (n / 2) + n % 2) * P
Tactic:
rw [h0, Nat.succ_eq_add_one, ← Nat.mul_succ 2, 𝔽₂X.natPow_two_mul,
  𝔽₂X.natPow_two_mul_add_one, 𝔽₂X.mul_assoc, ← P.square_eq_mul_self]
State after:
case inr
P : 𝔽₂X
n : ℕ
h0 : n % 2 = 1
⊢ P.square.natPow (n / 2).succ = P.square.natPow (n / 2) * P.square

State before:
case inr
P : 𝔽₂X
n : ℕ
h0 : n % 2 = 1
⊢ P.square.natPow (n / 2).succ = P.square.natPow (n / 2) * P.square
Tactic:
exact (square P).natPow_succ (n / 2)
State after:
no goals

State before:
P : 𝔽₂X
n : ℕ
a✝ :
  ∀ (y : (_ : 𝔽₂X) ×' ℕ),
    (invImage (fun x => PSigma.casesOn x fun P n => n) instWellFoundedRelationOfSizeOf).1 y ⟨P, n⟩ →
      y.1.natPow y.2.succ = y.1.natPow y.2 * y.1
h0 : n % 2 = 1
⊢ (invImage (fun x => PSigma.casesOn x fun P n => n) instWellFoundedRelationOfSizeOf).1 ⟨P.square, n / 2⟩ ⟨P, n⟩
Tactic:
apply Nat.bitwise_rec_lemma
State after:
case hNe
P : 𝔽₂X
n : ℕ
a✝ :
  ∀ (y : (_ : 𝔽₂X) ×' ℕ),
    (invImage (fun x => PSigma.casesOn x fun P n => n) instWellFoundedRelationOfSizeOf).1 y ⟨P, n⟩ →
      y.1.natPow y.2.succ = y.1.natPow y.2 * y.1
h0 : n % 2 = 1
⊢ n ≠ 0

State before:
case hNe
P : 𝔽₂X
n : ℕ
a✝ :
  ∀ (y : (_ : 𝔽₂X) ×' ℕ),
    (invImage (fun x => PSigma.casesOn x fun P n => n) instWellFoundedRelationOfSizeOf).1 y ⟨P, n⟩ →
      y.1.natPow y.2.succ = y.1.natPow y.2 * y.1
h0 : n % 2 = 1
⊢ n ≠ 0
Tactic:
rintro rfl
State after:
case hNe
P : 𝔽₂X
a✝ :
  ∀ (y : (_ : 𝔽₂X) ×' ℕ),
    (invImage (fun x => PSigma.casesOn x fun P n => n) instWellFoundedRelationOfSizeOf).1 y ⟨P, 0⟩ →
      y.1.natPow y.2.succ = y.1.natPow y.2 * y.1
h0 : 0 % 2 = 1
⊢ False

State before:
case hNe
P : 𝔽₂X
a✝ :
  ∀ (y : (_ : 𝔽₂X) ×' ℕ),
    (invImage (fun x => PSigma.casesOn x fun P n => n) instWellFoundedRelationOfSizeOf).1 y ⟨P, 0⟩ →
      y.1.natPow y.2.succ = y.1.natPow y.2 * y.1
h0 : 0 % 2 = 1
⊢ False
Tactic:
exact absurd h0.symm Nat.one_ne_zero
State after:
no goals