awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Conj (goal)
Goal:
α : Type u
β : Type v
inst : Monoid α
inst_1 : Monoid β
f : α →* β
a b : α
c : αˣ
hc : SemiconjBy (↑c : α) a b
rw : SemiconjBy.{v} (M := β) ((f : (a : α) → β) (↑c : α) : β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
rw₁ :
  HMul.hMul (α := β) (β := β) ((f : (a : α) → β) (↑c : α) : β) ((f : (a : α) → β) a : β) =
    HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) (↑c : α) : β)
rw₂ :
  (f : (a : α) → β) ((↑c : α) * a) =
    HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) (↑c : α) : β)
rw₃ :
  (f : (a : α) → β) (b * (↑c : α)) =
    HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) (↑c : α) : β)
⊢ SemiconjBy.{v} (M := β) ((↑((Units.map f : (a : αˣ) → βˣ) c) : β) : β) ((f : (a : α) → β) a : β)
    ((f : (a : α) → β) b : β)
have rw₄ : HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) (↑c : α) : β) =
  HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) (↑c : α) : β)
Tactic: rw [Units.coe_map, SemiconjBy, ← f.map_mul, hc.eq, f.map_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Conj (goal)
Goal:
α : Type u
inst : Monoid α
a : α
h : a = 1
⊢ IsConj 1 a
have rw : IsConj.{u} (α := α) 1 1
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Group.Conj (goal)
Goal:
α : Type u
inst : Monoid α
a : α
⊢ IsConj 1 a ↔ a = 1
have refine : IsConj 1 a → ∀ (c : αˣ) (h : SemiconjBy (↑c : α) 1 a), a = 1
Tactic: refine ⟨fun ⟨c, h⟩ => ?_, fun h => by rw [h]⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Conj (hypothesis)
Goal:
α : Type u
inst : Monoid α
a : α
h_1 : IsConj 1 a
c : αˣ
h : SemiconjBy (↑c : α) 1 a
⊢ a = 1
have h₁ : (↑c : α) = a * (↑c : α)
Tactic: rw [SemiconjBy, mul_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.Conj (goal)
Goal:
α : Type u
inst : Group α
i : ℕ
a b : α
⊢ (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
have zero : HPow.hPow (β := ℕ) (a * b * a⁻¹) 0 = a * HPow.hPow (β := ℕ) b 0 * a⁻¹
Tactic: induction i with
  | zero => simp
  | succ i hi => simp [pow_succ, hi]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Group.Conj (goal)
Goal:
α : Type u
inst : Group α
i : ℕ
a b : α
zero : HPow.hPow (β := ℕ) (a * b * a⁻¹) 0 = a * HPow.hPow (β := ℕ) b 0 * a⁻¹
⊢ (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
have succ : ∀ (i : ℕ) (hi : (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹), (a * b * a⁻¹) ^ (i + 1) = a * b ^ (i + 1) * a⁻¹
Tactic: induction i with
  | zero => simp
  | succ i hi => simp [pow_succ, hi]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Group.Conj (goal)
Goal:
α : Type u
inst : Group α
i : ℤ
a b : α
⊢ (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
have ofNat : ∀ (a_1 : ℕ), (a * b * a⁻¹) ^ Int.ofNat a_1 = a * b ^ Int.ofNat a_1 * a⁻¹
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Group.Conj (goal)
Goal:
α : Type u
inst : Group α
i : ℤ
a b : α
ofNat : ∀ (a_1 : ℕ), (a * b * a⁻¹) ^ Int.ofNat a_1 = a * b ^ Int.ofNat a_1 * a⁻¹
⊢ (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
have negSucc : ∀ (a_1 : ℕ), (a * b * a⁻¹) ^ Int.negSucc a_1 = a * b ^ Int.negSucc a_1 * a⁻¹
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Group.Conj (goal)
Goal:
α : Type u
inst : Group α
a b : α
a_1 : ℕ
⊢ (a * b * a⁻¹) ^ Int.negSucc a_1 = a * b ^ Int.negSucc a_1 * a⁻¹
have negSucc : a * ((b ^ (a_1 + 1))⁻¹ * a⁻¹) = a * (b ^ (a_1 + 1))⁻¹ * a⁻¹
Tactic: simp only [zpow_negSucc, conj_pow, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Conj (goal)
Goal:
α : Type u
inst : Group α
a b : α
a_1 : ℕ
⊢ a * ((b ^ (a_1 + 1))⁻¹ * a⁻¹) = a * (b ^ (a_1 + 1))⁻¹ * a⁻¹
have negSucc : a * ((b ^ (a_1 + 1))⁻¹ * a⁻¹) = a * ((b ^ (a_1 + 1))⁻¹ * a⁻¹)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Conj (goal)
Goal:
α : Type u
β : Type v
inst : Monoid α
inst_1 : Monoid β
f : α →* β
hf : Function.Surjective.{u + 1, v + 1} (α := α) (β := β) (⇑f : (a : α) → β)
b : ConjClasses β
⊢ ∃ (a : ConjClasses α), map f a = b
have obtain : ∀ (b : β), ∃ (a : ConjClasses α), map f a = ConjClasses.mk b
Tactic: obtain ⟨b, rfl⟩ := ConjClasses.mk_surjective b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Group.Conj (goal)
Goal:
α : Type u
β : Type v
inst : Monoid α
inst_1 : Monoid β
f : α →* β
hf : Function.Surjective.{u + 1, v + 1} (α := α) (β := β) (⇑f : (a : α) → β)
b : β
⊢ ∃ (a : ConjClasses α), map f a = ConjClasses.mk b
have obtain : ∀ (a : α), ∃ (a_1 : ConjClasses α), map f a_1 = ConjClasses.mk ((f : (a : α) → β) a)
Tactic: obtain ⟨a, rfl⟩ := hf b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Group.Conj (goal)
Goal:
α : Type u
β : Type v
inst : CommMonoid α
⊢ Function.RightInverse.{u + 1, u + 1} (α := α) (β := ConjClasses α) (Quotient.lift id ⋯) ConjClasses.mk
have rw : ∀ (a : α),
  Eq (α := ConjClasses α) (ConjClasses.mk (Quotient.lift (s := IsConj.setoid α) id sorry (ConjClasses.mk a)))
    (ConjClasses.mk a)
Tactic: rw [Function.RightInverse, Function.LeftInverse, forall_isConj]
-- Lean 4 proof step from Mathlib.Algebra.Group.Conj (hypothesis)
Goal:
α : Type u
inst : Monoid α
a b : α
h : conjugatesOf a = conjugatesOf b
⊢ IsConj a b
have ha : b ∈ conjugatesOf b
Tactic: have ha := mem_conjugatesOf_self (a := b)
-- Lean 4 proof step from Mathlib.Algebra.Group.Conj (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
h : conjugatesOf a = conjugatesOf b
ha : b ∈ conjugatesOf b
⊢ IsConj a b
have rwa : ∀ (ha : b ∈ conjugatesOf a), IsConj a b
Tactic: rwa [← h] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Group.Conj (goal)
Goal:
α : Type u
inst : Monoid α
a : α
b : ConjClasses α
⊢ a ∈ b.carrier ↔ ConjClasses.mk a = b
have revert : ∀ {b : ConjClasses α}, a ∈ b.carrier ↔ ConjClasses.mk a = b
Tactic: revert b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Group.Conj (goal)
Goal:
α : Type u
inst : Monoid α
a : α
⊢ ∀ {b : ConjClasses α}, a ∈ b.carrier ↔ ConjClasses.mk a = b
have rw : ∀ (a_1 : α), a ∈ carrier (ConjClasses.mk a_1) ↔ Eq (α := ConjClasses α) (ConjClasses.mk a) (ConjClasses.mk a_1)
Tactic: rw [forall_isConj]
-- Lean 4 proof step from Mathlib.Algebra.Group.Conj (goal)
Goal:
α : Type u
inst : Monoid α
a b : α
⊢ a ∈ carrier (ConjClasses.mk b) ↔ Eq (α := ConjClasses α) (ConjClasses.mk a) (ConjClasses.mk b)
have rw : a ∈ conjugatesOf b ↔ IsConj b a
Tactic: rw [carrier, eq_comm, mk_eq_mk_iff_isConj, ← quotient_mk_eq_mk, Quotient.lift_mk]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
R : Type u_2
inst : Mul R
⊢ IsCancelMul R ↔ ∀ (r : R), IsRegular r
have rw : (∀ (x : R), IsLeftRegular x ∧ IsRightRegular x) ↔ ∀ (r : R), IsRegular r
Tactic: rw [isCancelMul_iff, isLeftCancelMul_iff, isRightCancelMul_iff, ← forall_and]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one₂ : M
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
this : one₁ = one₂
⊢ { one := one₁, mul := mul₁, one_mul := one_mul₁, mul_one := mul_one₁ : MulOneClass M } =
    { one := one₂, mul := mul₁, one_mul := one_mul₂, mul_one := mul_one₂ }
have refl : ∀ (one_mul₂ : ∀ (a : M), 1 * a = a) (mul_one₂ : ∀ (a : M), a * 1 = a),
  { one := one₁, mul := mul₁, one_mul := one_mul₁, mul_one := mul_one₁ : MulOneClass M } =
    { one := one₁, mul := mul₁, one_mul := one_mul₂, mul_one := mul_one₂ }
Tactic: cases this
Cleared hypotheses: one₂, one_mul₂, mul_one₂, this
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one₂ : M
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
⊢ { one := one₁, mul := mul₁, one_mul := one_mul₁, mul_one := mul_one₁ : MulOneClass M } =
    { one := one₂, mul := mul₁, one_mul := one_mul₂, mul_one := mul_one₂ }
have suffices : one₁ = one₂
Tactic: suffices one₁ = one₂ by cases this; rfl
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u
inst : One M
inst_1 : Semigroup M
m n : ℕ
hn : n ≠ 0
a : M
ha : 1 * a = a
⊢ npowRec (m + n) a = npowRec m a * npowRec n a
have zero : ∀ (hn : Ne (α := ℕ) 0 0), npowRec (m + 0) a = npowRec m a * npowRec 0 a
Tactic: obtain _ | n := n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u
inst : One M
inst_1 : Semigroup M
m n : ℕ
hn : n ≠ 0
a : M
ha : 1 * a = a
zero : ∀ (hn : Ne (α := ℕ) 0 0), npowRec (m + 0) a = npowRec m a * npowRec 0 a
⊢ npowRec (m + n) a = npowRec m a * npowRec n a
have succ : ∀ (n : ℕ) (hn : n + 1 ≠ 0), npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a
Tactic: obtain _ | n := n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u
inst : One M
inst_1 : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
n : ℕ
ih : ∀ (hn : n + 1 ≠ 0), npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a
hn : n + 1 + 1 ≠ 0
⊢ npowRec (m + (n + 1 + 1)) a = npowRec m a * npowRec (n + 1 + 1) a
have succ : npowRec m a * npowRec (n + 1) a * a = npowRec m a * npowRec (n + 1 + 1) a
Tactic: rw [← Nat.add_assoc, npowRec, ih n.succ_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u
inst : One M
inst_1 : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
n : ℕ
hn : n + 1 ≠ 0
⊢ npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a
have succ : ∀ (hn : HAdd.hAdd (α := ℕ) 0 1 ≠ 0),
  npowRec (m + HAdd.hAdd (α := ℕ) 0 1) a = npowRec m a * npowRec (HAdd.hAdd (α := ℕ) 0 1) a
Tactic: induction n with
  | zero => simp only [npowRec, ha]
  | succ n ih => rw [← Nat.add_assoc, npowRec, ih n.succ_ne_zero]; simp only [npowRec, mul_assoc]
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u
inst : One M
inst_1 : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
n : ℕ
hn : n + 1 ≠ 0
succ :
  ∀ (hn : HAdd.hAdd (α := ℕ) 0 1 ≠ 0),
    npowRec (m + HAdd.hAdd (α := ℕ) 0 1) a = npowRec m a * npowRec (HAdd.hAdd (α := ℕ) 0 1) a
⊢ npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a
have succ₁ : ∀ (n : ℕ) (ih : ∀ (hn : n + 1 ≠ 0), npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a) (hn : n + 1 + 1 ≠ 0),
  npowRec (m + (n + 1 + 1)) a = npowRec m a * npowRec (n + 1 + 1) a
Tactic: induction n with
  | zero => simp only [npowRec, ha]
  | succ n ih => rw [← Nat.add_assoc, npowRec, ih n.succ_ne_zero]; simp only [npowRec, mul_assoc]
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u
inst : One M
inst_1 : Semigroup M
n : ℕ
hn : n ≠ 0
a : M
ha : 1 * a = a
⊢ npowRec (n + 1) a = a * npowRec n a
have rw : npowRec (1 + n) a = a * npowRec n a
Tactic: rw [Nat.add_comm, npowRec_add 1 n hn a ha, npowRec, npowRec, ha]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u
inst : One M
inst_1 : Semigroup M
n : ℕ
hn : n ≠ 0
a : M
ha : 1 * a = a
rw : npowRec (1 + n) a = a * npowRec n a
⊢ npowRec (n + 1) a = a * npowRec n a
have rw₁ : npowRec 1 a * npowRec n a = a * npowRec n a
Tactic: rw [Nat.add_comm, npowRec_add 1 n hn a ha, npowRec, npowRec, ha]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u
inst : One M
inst_1 : Semigroup M
n : ℕ
hn : n ≠ 0
a : M
ha : 1 * a = a
rw : npowRec (1 + n) a = a * npowRec n a
rw₁ : npowRec 1 a * npowRec n a = a * npowRec n a
⊢ npowRec (n + 1) a = a * npowRec n a
have rw₂ : npowRec 0 a * a * npowRec n a = a * npowRec n a
Tactic: rw [Nat.add_comm, npowRec_add 1 n hn a ha, npowRec, npowRec, ha]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u
inst : One M
inst_1 : Semigroup M
n : ℕ
hn : n ≠ 0
a : M
ha : 1 * a = a
rw : npowRec (1 + n) a = a * npowRec n a
rw₁ : npowRec 1 a * npowRec n a = a * npowRec n a
rw₂ : npowRec 0 a * a * npowRec n a = a * npowRec n a
⊢ npowRec (n + 1) a = a * npowRec n a
have rw₃ : 1 * a * npowRec n a = a * npowRec n a
Tactic: rw [Nat.add_comm, npowRec_add 1 n hn a ha, npowRec, npowRec, ha]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u
inst : One M
inst_1 : Semigroup M
n : ℕ
hn : n ≠ 0
a : M
ha : 1 * a = a
rw : npowRec (1 + n) a = a * npowRec n a
rw₁ : npowRec 1 a * npowRec n a = a * npowRec n a
rw₂ : npowRec 0 a * a * npowRec n a = a * npowRec n a
rw₃ : 1 * a * npowRec n a = a * npowRec n a
⊢ npowRec (n + 1) a = a * npowRec n a
have rw₄ : a * npowRec n a = a * npowRec n a
Tactic: rw [Nat.add_comm, npowRec_add 1 n hn a ha, npowRec, npowRec, ha]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k : ℕ
m : M
⊢ npowRec' (2 * k) m = npowRec' k (m * m)
have ind : ∀ (k' : ℕ) (ih : ∀ (m_1 : ℕ), m_1 < k' → npowRec' (2 * m_1) m = npowRec' m_1 (m * m)),
  npowRec' (2 * k') m = npowRec' k' (m * m)
Tactic: induction k using Nat.strongRecOn with
  | ind k' ih =>
    match k' with
    | 0 => rfl
    | 1 => simp [npowRec']
    | k + 2 => simp [npowRec', ← mul_assoc, ← ih]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k : ℕ
k0 : k ≠ 0
m : M
⊢ m * npowRec' k m = npowRec' k m * m
have ind : ∀ (k' : ℕ) (ih : ∀ (m_1 : ℕ), m_1 < k' → ∀ (k0 : m_1 ≠ 0), m * npowRec' m_1 m = npowRec' m_1 m * m) (k0 : k' ≠ 0),
  m * npowRec' k' m = npowRec' k' m * m
Tactic: induction k using Nat.strongRecOn with
  | ind k' ih =>
    match k' with
    | 1 => simp [npowRec']
    | k + 2 => simp [npowRec', ← mul_assoc, ih]
Cleared hypotheses: k, k0
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
m : M
k' k : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k + 1 → npowRec (m_1 + 1) m = 1 * npowRec' (m_1 + 1) m
⊢ npowRec (k + 1 + 1) m = 1 * npowRec' (k + 1 + 1) m
have rw : npowRec (k + 1) m * m = 1 * npowRec' k.succ m * m
Tactic: rw [npowRec, npowRec'_succ k.succ_ne_zero, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
m : M
k' k : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k + 1 → npowRec (m_1 + 1) m = 1 * npowRec' (m_1 + 1) m
⊢ npowRec (k + 1) m * m = 1 * npowRec' k.succ m * m
have e_a : npowRec (k + 1) m = 1 * npowRec' k.succ m
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k : ℕ
m : M
⊢ npowRec (k + 1) m = 1 * npowRec' (k + 1) m
have ind : ∀ (k' : ℕ) (ih : ∀ (m_1 : ℕ), m_1 < k' → npowRec (m_1 + 1) m = 1 * npowRec' (m_1 + 1) m),
  npowRec (k' + 1) m = 1 * npowRec' (k' + 1) m
Tactic: induction k using Nat.strongRecOn with
  | ind k' ih =>
    match k' with
    | 0 => rfl
    | k + 1 =>
      rw [npowRec, npowRec'_succ k.succ_ne_zero, ← mul_assoc]
      congr
      simp [ih]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k : ℕ
m n : M
⊢ go (k + 1) m n = m * npowRec' (k + 1) n
have unfold : Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
    (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) ↦ fn (bif bn then y * x else y) (x * x)) (k + 1) m n =
  m * npowRec' (k + 1) n
Tactic: unfold go
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k : ℕ
m n : M
⊢ Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
      (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) ↦ fn (bif bn then y * x else y) (x * x)) (k + 1) m n =
    m * npowRec' (k + 1) n
have generalize : ∀ (k' : ℕ) (hk : k + 1 = k'),
  Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
      (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) ↦ fn (bif bn then y * x else y) (x * x)) k' m n =
    m * npowRec' k' n
Tactic: generalize hk : k + 1 = k'
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (hypothesis)
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k : ℕ
m n : M
k' : ℕ
hk : k + 1 = k'
⊢ Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
      (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) ↦ fn (bif bn then y * x else y) (x * x)) k' m n =
    m * npowRec' k' n
have hk₁ : k' ≠ 0
Tactic: replace hk : k' ≠ 0 := by lia
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k : ℕ
b : Bool
k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M) (hk : k' ≠ 0),
    Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
        (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) ↦ 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 : M) ↦ y)
      (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) ↦ fn (bif bn then y * x else y) (x * x)) (Nat.bit b k') m n =
    m * npowRec' (Nat.bit b k') n
have bit : (bif b then m * n else m) * npowRec' k' (n * n) = m * npowRec' (Nat.bit b k') n
Tactic: rw [Nat.binaryRec_eq _ _ (Or.inl rfl), ih _ _ k'0]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k : ℕ
b : Bool
k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M) (hk : k' ≠ 0),
    Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
        (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) ↦ 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
have bit : ∀ (hk : Nat.bit false k' ≠ 0), (bif false then m * n else m) * npowRec' k' (n * n) = m * npowRec' (Nat.bit false k') n
Tactic: cases b
Cleared hypotheses: b, hk
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k : ℕ
b : Bool
k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M) (hk : k' ≠ 0),
    Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
        (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) ↦ 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
bit :
  ∀ (hk : Nat.bit false k' ≠ 0), (bif false then m * n else m) * npowRec' k' (n * n) = m * npowRec' (Nat.bit false k') n
⊢ (bif b then m * n else m) * npowRec' k' (n * n) = m * npowRec' (Nat.bit b k') n
have bit₁ : ∀ (hk : Nat.bit true k' ≠ 0), (bif true then m * n else m) * npowRec' k' (n * n) = m * npowRec' (Nat.bit true k') n
Tactic: cases b
Cleared hypotheses: b, hk
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M) (hk : k' ≠ 0),
    Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
        (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) ↦ 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
⊢ (bif true then m * n else m) * npowRec' k' (n * n) = m * npowRec' (Nat.bit true k') n
have bit : m * n * npowRec' k' (n * n) = m * npowRec' (2 * k' + 1) n
Tactic: simp only [Nat.bit, cond_false, cond_true, npowRec'_two_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M) (hk : k' ≠ 0),
    Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
        (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) ↦ 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
have bit : m * n * npowRec' k' (n * n) = m * (npowRec' (2 * k') n * n)
Tactic: rw [npowRec'_succ (by lia), npowRec'_two_mul, ← npowRec'_two_mul,
      ← npowRec'_mul_comm (by lia), mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M) (hk : k' ≠ 0),
    Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
        (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) ↦ 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
bit : m * n * npowRec' k' (n * n) = m * (npowRec' (2 * k') n * n)
⊢ m * n * npowRec' k' (n * n) = m * npowRec' (2 * k' + 1) n
have bit₁ : m * n * npowRec' k' (n * n) = m * (npowRec' k' (n * n) * n)
Tactic: rw [npowRec'_succ (by lia), npowRec'_two_mul, ← npowRec'_two_mul,
      ← npowRec'_mul_comm (by lia), mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M) (hk : k' ≠ 0),
    Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
        (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) ↦ 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
bit : m * n * npowRec' k' (n * n) = m * (npowRec' (2 * k') n * n)
bit₁ : m * n * npowRec' k' (n * n) = m * (npowRec' k' (n * n) * n)
⊢ m * n * npowRec' k' (n * n) = m * npowRec' (2 * k' + 1) n
have bit₂ : m * n * npowRec' (2 * k') n = m * (npowRec' (2 * k') n * n)
Tactic: rw [npowRec'_succ (by lia), npowRec'_two_mul, ← npowRec'_two_mul,
      ← npowRec'_mul_comm (by lia), mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M) (hk : k' ≠ 0),
    Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
        (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) ↦ 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
bit : m * n * npowRec' k' (n * n) = m * (npowRec' (2 * k') n * n)
bit₁ : m * n * npowRec' k' (n * n) = m * (npowRec' k' (n * n) * n)
bit₂ : m * n * npowRec' (2 * k') n = m * (npowRec' (2 * k') n * n)
⊢ m * n * npowRec' k' (n * n) = m * npowRec' (2 * k' + 1) n
have bit₃ : m * n * npowRec' (2 * k') n = m * (n * npowRec' (2 * k') n)
Tactic: rw [npowRec'_succ (by lia), npowRec'_two_mul, ← npowRec'_two_mul,
      ← npowRec'_mul_comm (by lia), mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M) (hk : k' ≠ 0),
    Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
        (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) ↦ 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
bit : m * n * npowRec' k' (n * n) = m * (npowRec' (2 * k') n * n)
bit₁ : m * n * npowRec' k' (n * n) = m * (npowRec' k' (n * n) * n)
bit₂ : m * n * npowRec' (2 * k') n = m * (npowRec' (2 * k') n * n)
bit₃ : m * n * npowRec' (2 * k') n = m * (n * npowRec' (2 * k') n)
⊢ m * n * npowRec' k' (n * n) = m * npowRec' (2 * k' + 1) n
have bit₄ : m * (n * npowRec' (2 * k') n) = m * (n * npowRec' (2 * k') n)
Tactic: rw [npowRec'_succ (by lia), npowRec'_two_mul, ← npowRec'_two_mul,
      ← npowRec'_mul_comm (by lia), mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k : ℕ
m n : M
k' : ℕ
hk : k' ≠ 0
⊢ Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
      (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) ↦ fn (bif bn then y * x else y) (x * x)) k' m n =
    m * npowRec' k' n
have zero : ∀ (m n : M) (hk : Ne (α := ℕ) 0 0),
  Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
      (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x : M) ↦ fn (bif bn then y * x else y) (x * x)) 0 m n =
    m * npowRec' 0 n
Tactic: induction k' using Nat.binaryRecFromOne generalizing n m with
  | zero => simp at hk
  | one => simp [npowRec']
  | bit 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, npowRec'_two_mul]
    rw [npowRec'_succ (by lia), npowRec'_two_mul, ← npowRec'_two_mul,
      ← npowRec'_mul_comm (by lia), mul_assoc]
Cleared hypotheses: m, n, k', hk