-- Mathlib/Algebra/Group/Defs.lean
theorem npowBinRec.go_spec {M : Type*} [Semigroup M] [One M] (k : ℕ) (m n : M) :
    npowBinRec.go (k + 1) m n = m * npowRec' (k + 1) n

Proof state:
case f.true
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M),
    k' ≠ 0 →
      Nat.binaryRec (motive := fun x => M → M → M) (fun y x => y)
          (fun bn _n fn y x => fn (bif bn then y * x else y) (x * x)) k' m n =
        m * npowRec' k' n
m n : M
hk : Nat.bit true k' ≠ 0
⊢ m * n * npowRec' k' (n * n) = m * npowRec' (2 * k' + 1) n

Tactic:
rw [npowRec'_succ (by omega), npowRec'_two_mul, ← npowRec'_two_mul,
  ← npowRec'_mul_comm (by omega), mul_assoc]

Result:
no goals

Proof state:
case f
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
b : Bool
k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M),
    k' ≠ 0 →
      Nat.binaryRec (motive := fun x => M → M → M) (fun y x => y)
          (fun bn _n fn y x => fn (bif bn then y * x else y) (x * x)) k' m n =
        m * npowRec' k' n
m n : M
hk : Nat.bit b k' ≠ 0
⊢ Nat.binaryRec (motive := fun x => M → M → M) (fun y x => y)
      (fun bn _n fn y x => fn (bif bn then y * x else y) (x * x)) (Nat.bit b k') m n =
    m * npowRec' (Nat.bit b k') n

Tactic:
rw [Nat.binaryRec_eq _ _ (Or.inl rfl), ih _ _ k'0]

Result:
case f
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
b : Bool
k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M),
    k' ≠ 0 →
      Nat.binaryRec (motive := fun x => M → M → M) (fun y x => y)
          (fun bn _n fn y x => fn (bif bn then y * x else y) (x * x)) k' m n =
        m * npowRec' k' n
m n : M
hk : Nat.bit b k' ≠ 0
⊢ (bif b then m * n else m) * npowRec' k' (n * n) = m * npowRec' (Nat.bit b k') n

Proof state:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m n : M
k' : ℕ
hk : k + 1 = k'
⊢ k' ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
case f
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
b : Bool
k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M),
    k' ≠ 0 →
      Nat.binaryRec (motive := fun x => M → M → M) (fun y x => y)
          (fun bn _n fn y x => fn (bif bn then y * x else y) (x * x)) k' m n =
        m * npowRec' k' n
m n : M
hk : Nat.bit b k' ≠ 0
⊢ (bif b then m * n else m) * npowRec' k' (n * n) = m * npowRec' (Nat.bit b k') n

Tactic:
cases b <;> simp only [Nat.bit, cond_false, cond_true, ← Nat.two_mul, npowRec'_two_mul]

Result:
case f.true
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M),
    k' ≠ 0 →
      Nat.binaryRec (motive := fun x => M → M → M) (fun y x => y)
          (fun bn _n fn y x => fn (bif bn then y * x else y) (x * x)) k' m n =
        m * npowRec' k' n
m n : M
hk : Nat.bit true k' ≠ 0
⊢ m * n * npowRec' k' (n * n) = m * npowRec' (2 * k' + 1) n

Proof state:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m n : M
k' : ℕ
hk : k' ≠ 0
⊢ Nat.binaryRec (motive := fun x => M → M → M) (fun y x => y)
      (fun bn _n fn y x => fn (bif bn then y * x else y) (x * x)) k' m n =
    m * npowRec' k' n

Tactic:
induction k' using Nat.binaryRecFromOne generalizing n m with
| z₀ => simp at hk
| z₁ => simp [npowRec']
| f b k' k'0 ih =>
  rw [Nat.binaryRec_eq _ _ (Or.inl rfl), ih _ _ k'0]
  cases b <;> simp only [Nat.bit, cond_false, cond_true, ← Nat.two_mul, npowRec'_two_mul]
  rw [npowRec'_succ (by omega), npowRec'_two_mul, ← npowRec'_two_mul,
    ← npowRec'_mul_comm (by omega), mul_assoc]

Result:
no goals

Proof state:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m n : M
⊢ go (k + 1) m n = m * npowRec' (k + 1) n

Tactic:
unfold go

Result:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m n : M
⊢ Nat.binaryRec (motive := fun x => M → M → M) (fun y x => y)
      (fun bn _n fn y x => fn (bif bn then y * x else y) (x * x)) (k + 1) m n =
    m * npowRec' (k + 1) n

Proof state:
case z₀
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m n : M
hk : 0 ≠ 0
⊢ Nat.binaryRec (motive := fun x => M → M → M) (fun y x => y)
      (fun bn _n fn y x => fn (bif bn then y * x else y) (x * x)) 0 m n =
    m * npowRec' 0 n

Tactic:
simp at hk

Result:
no goals

Proof state:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m n : M
k' : ℕ
hk : k + 1 = k'
⊢ Nat.binaryRec (motive := fun x => M → M → M) (fun y x => y)
      (fun bn _n fn y x => fn (bif bn then y * x else y) (x * x)) k' m n =
    m * npowRec' k' n

Tactic:
replace hk : k' ≠ 0 := by omega

Result:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m n : M
k' : ℕ
hk : k' ≠ 0
⊢ Nat.binaryRec (motive := fun x => M → M → M) (fun y x => y)
      (fun bn _n fn y x => fn (bif bn then y * x else y) (x * x)) k' m n =
    m * npowRec' k' n

Proof state:
case z₁
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m n : M
hk : 1 ≠ 0
⊢ Nat.binaryRec (motive := fun x => M → M → M) (fun y x => y)
      (fun bn _n fn y x => fn (bif bn then y * x else y) (x * x)) 1 m n =
    m * npowRec' 1 n

Tactic:
simp [npowRec']

Result:
no goals

Proof state:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M),
    k' ≠ 0 →
      Nat.binaryRec (motive := fun x => M → M → M) (fun y x => y)
          (fun bn _n fn y x => fn (bif bn then y * x else y) (x * x)) k' m n =
        m * npowRec' k' n
m n : M
hk : Nat.bit true k' ≠ 0
⊢ 2 * k' ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m n : M
⊢ Nat.binaryRec (motive := fun x => M → M → M) (fun y x => y)
      (fun bn _n fn y x => fn (bif bn then y * x else y) (x * x)) (k + 1) m n =
    m * npowRec' (k + 1) n

Tactic:
generalize hk : k + 1 = k'

Result:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m n : M
k' : ℕ
hk : k + 1 = k'
⊢ Nat.binaryRec (motive := fun x => M → M → M) (fun y x => y)
      (fun bn _n fn y x => fn (bif bn then y * x else y) (x * x)) k' m n =
    m * npowRec' k' n