awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Conj
Goal:
α : Type u
inst : Monoid α
a : ConjClasses α
⊢ a.carrier = Set.preimage (β := ConjClasses α) ConjClasses.mk {a}

Tactic:
Set.ext fun _ => mem_carrier_iff_mk_eq

Premises used: Set.ext, ConjClasses.mem_carrier_iff_mk_eq
-- Module: Mathlib.Algebra.Group.ConjFinite
Goal:
α : Type u_1
inst : Monoid α
inst_1 : Finite α
⊢ Finite.{u_1 + 1} (ConjClasses α)

Tactic:
Quotient.finite _

Premises used: Quotient.finite, ConjClasses
-- Module: Mathlib.Algebra.Group.Defs
Goal:
R : Type u_2
inst : Mul R
rw : (∀ (x : R), IsLeftRegular x ∧ IsRightRegular x) ↔ ∀ (r : R), IsRegular r
⊢ IsCancelMul R ↔ ∀ (r : R), IsRegular r

Tactic:
rw [isCancelMul_iff, isLeftCancelMul_iff, isRightCancelMul_iff, ← forall_and]

Premises used: isCancelMul_iff, isLeftCancelMul_iff, isRightCancelMul_iff, forall_and
-- Module: Mathlib.Algebra.Group.Defs
Goal:
R : Type u_2
inst : Mul R
⊢ (∀ (x : R), IsLeftRegular x ∧ IsRightRegular x) ↔ ∀ (r : R), IsRegular r

Tactic:
forall_congr' fun _ ↦ isRegular_iff.symm

Premises used: isRegular_iff, forall_congr', Iff.symm
-- Module: Mathlib.Algebra.Group.Defs
Goal:
R : Type u_2
inst : Mul R
⊢ (∀ (x : R), IsLeftRegular x ∧ IsRightRegular x) ↔ ∀ (r : R), IsRegular r

Tactic:
exact forall_congr' fun _ ↦ isRegular_iff.symm

Premises used: isRegular_iff, forall_congr', Iff.symm
-- Module: Mathlib.Algebra.Group.Defs
Goal:
R : Type u_2
inst : Mul R
inst_1 : IsLeftCancelMul R
g : R
⊢ IsLeftRegular g

Tactic:
(isLeftCancelMul_iff R).mp ‹_› _

Premises used: Iff.mp, isLeftCancelMul_iff
-- Module: Mathlib.Algebra.Group.Defs
Goal:
R : Type u_2
inst : Mul R
inst_1 : IsRightCancelMul R
g : R
⊢ IsRightRegular g

Tactic:
(isRightCancelMul_iff R).mp ‹_› _

Premises used: Iff.mp, isRightCancelMul_iff
-- Module: Mathlib.Algebra.Group.Defs
Goal:
R : Type u_2
inst : Mul R
inst_1 : IsCancelMul R
g : R
⊢ IsRegular g

Tactic:
⟨.all g, .all g⟩

Premises used: IsRightRegular.all, IsLeftRegular.all, IsRegular.mk
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Mul G
inst_1 : IsLeftCancelMul G
a b c : G
⊢ a * b = a * c → b = c

Tactic:
(IsLeftCancelMul.mul_left_cancel a ·)

Premises used: IsLeftCancelMul.mul_left_cancel
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Mul G
inst_1 : IsLeftCancelMul G
a b c : G
⊢ a * b = a * c ↔ b = c

Tactic:
⟨mul_left_cancel, congrArg _⟩

Premises used: congrArg, mul_left_cancel, Iff.intro
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Mul G
inst_1 : IsLeftCancelMul G
a : G
⊢ Injective (β := G) fun (x : G) ↦ a * x

Tactic:
fun _ _ ↦ mul_left_cancel

Premises used: mul_left_cancel, Function.Injective
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Mul G
inst_1 : IsLeftCancelMul G
a b c : G
⊢ a * b = a * c ↔ b = c

Tactic:
(mul_right_injective a).eq_iff

Premises used: Function.Injective.eq_iff, mul_right_injective
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Mul G
inst_1 : IsLeftCancelMul G
a b c : G
⊢ a * b ≠ a * c ↔ b ≠ c

Tactic:
(mul_right_injective a).ne_iff

Premises used: Function.Injective.ne_iff, mul_right_injective
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Mul G
inst_1 : IsRightCancelMul G
a b c : G
⊢ a * b = c * b → a = c

Tactic:
(IsRightCancelMul.mul_right_cancel b ·)

Premises used: IsRightCancelMul.mul_right_cancel
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Mul G
inst_1 : IsRightCancelMul G
a b c : G
⊢ b * a = c * a ↔ b = c

Tactic:
⟨mul_right_cancel, congrArg (· * a)⟩

Premises used: HMul.hMul, congrArg, Iff.intro, mul_right_cancel
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Mul G
inst_1 : IsRightCancelMul G
a : G
⊢ Injective (β := G) fun (x : G) ↦ x * a

Tactic:
fun _ _ ↦ mul_right_cancel

Premises used: mul_right_cancel, Function.Injective
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Mul G
inst_1 : IsRightCancelMul G
a b c : G
⊢ b * a = c * a ↔ b = c

Tactic:
(mul_left_injective a).eq_iff

Premises used: Function.Injective.eq_iff, mul_left_injective
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Mul G
inst_1 : IsRightCancelMul G
a b c : G
⊢ b * a ≠ c * a ↔ b ≠ c

Tactic:
(mul_left_injective a).ne_iff

Premises used: Function.Injective.ne_iff, mul_left_injective
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : Semigroup G
⊢ ∀ (a b c : G), a * b * c = a * (b * c)

Tactic:
Semigroup.mul_assoc

Premises used: Semigroup.mul_assoc
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Mul M
⊢ IsMulCommutative M ↔ ∀ (a b : M), a * b = b * a

Tactic:
grind [IsMulCommutative, Std.Commutative]

Premises used: Std.Commutative, IsMulCommutative
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Mul M
inst_1 : IsMulCommutative M
a b : M
⊢ a * b = b * a

Tactic:
IsMulCommutative.is_comm.comm ..

Premises used: Std.Commutative.comm
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : CommMagma G
⊢ ∀ (a b : G), a * b = b * a

Tactic:
CommMagma.mul_comm

Premises used: CommMagma.mul_comm
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : CommMagma G
a : G
⊢ IsMulCommutative G

Tactic:
⟨⟨mul_comm⟩⟩

Premises used: mul_comm, IsMulCommutative.mk, Std.Commutative.mk
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : CommMagma G
a : G
⊢ IsLeftRegular a ↔ IsRegular a

Tactic:
simp [isRegular_iff, IsLeftRegular, IsRightRegular, mul_comm]

Premises used: isRegular_iff, IsLeftRegular, IsRightRegular, mul_comm
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u_1
inst : CommMagma G
a : G
⊢ IsRightRegular a ↔ IsRegular a

Tactic:
simp [isRegular_iff, IsLeftRegular, IsRightRegular, mul_comm]

Premises used: isRegular_iff, IsLeftRegular, IsRightRegular, mul_comm
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u
inst : CommMagma G
inst_1 : IsRightCancelMul G
⊢ IsLeftCancelMul G

Tactic:
⟨fun _ _ _ h => mul_right_cancel <| (mul_comm _ _).trans (h.trans (mul_comm _ _))⟩

Premises used: IsLeftCancelMul.mk, mul_comm, mul_right_cancel, Eq.trans
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u
inst : CommMagma G
inst_1 : IsLeftCancelMul G
⊢ IsRightCancelMul G

Tactic:
⟨fun _ _ _ h => mul_left_cancel <| (mul_comm _ _).trans (h.trans (mul_comm _ _))⟩

Premises used: mul_left_cancel, mul_comm, IsRightCancelMul.mk, Eq.trans
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u
inst : CommMagma G
inst_1 : IsLeftCancelMul G
⊢ IsCancelMul G

Tactic:
{ CommMagma.IsLeftCancelMul.toIsRightCancelMul G with }

Premises used: CommMagma.IsLeftCancelMul.toIsRightCancelMul, IsCancelMul.mk
-- Module: Mathlib.Algebra.Group.Defs
Goal:
G : Type u
inst : CommMagma G
inst_1 : IsRightCancelMul G
⊢ IsCancelMul G

Tactic:
{ CommMagma.IsRightCancelMul.toIsLeftCancelMul G with }

Premises used: CommMagma.IsRightCancelMul.toIsLeftCancelMul, IsCancelMul.mk
-- Module: Mathlib.Algebra.Group.Defs
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₂
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₂ }
⊢ { 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
-- Module: Mathlib.Algebra.Group.Defs
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_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:
rfl
-- Module: Mathlib.Algebra.Group.Defs
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
suffices : 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₂ }

Tactic:
suffices one₁ = one₂ by cases this; rfl
-- Module: Mathlib.Algebra.Group.Defs
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₂

Tactic:
(one_mul₂ one₁).symm.trans (mul_one₁ one₂)

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Group.Defs
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₂

Tactic:
exact (one_mul₂ one₁).symm.trans (mul_one₁ one₂)

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u
inst : MulOneClass M
⊢ ∀ (a : M), 1 * a = a

Tactic:
MulOneClass.one_mul

Premises used: MulOneClass.one_mul
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u
inst : MulOneClass M
⊢ ∀ (a : M), a * 1 = a

Tactic:
MulOneClass.mul_one

Premises used: MulOneClass.mul_one
-- Module: Mathlib.Algebra.Group.Defs
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
succ : ∀ (n : ℕ) (hn : n + 1 ≠ 0), npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a
⊢ npowRec (m + n) a = npowRec m a * npowRec n a

Tactic:
obtain _ | n := n
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u
inst : One M
inst_1 : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
hn : Ne (α := ℕ) 0 0
⊢ npowRec (m + 0) a = npowRec m a * npowRec 0 a

Tactic:
(hn rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u
inst : One M
inst_1 : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
hn : Ne (α := ℕ) 0 0
⊢ npowRec (m + 0) a = npowRec m a * npowRec 0 a

Tactic:
exact (hn rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u
inst : One M
inst_1 : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
hn : HAdd.hAdd (α := ℕ) 0 1 ≠ 0
⊢ npowRec (m + HAdd.hAdd (α := ℕ) 0 1) a = npowRec m a * npowRec (HAdd.hAdd (α := ℕ) 0 1) a

Tactic:
simp only [npowRec, ha]

Premises used: npowRec
-- Module: Mathlib.Algebra.Group.Defs
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
succ : npowRec m a * npowRec (n + 1) a * a = npowRec m a * npowRec (n + 1 + 1) a
⊢ npowRec (m + (n + 1 + 1)) a = npowRec m a * npowRec (n + 1 + 1) a

Tactic:
rw [← Nat.add_assoc, npowRec, ih n.succ_ne_zero]

Premises used: npowRec, Nat.succ_ne_zero, Nat.add_assoc
-- Module: Mathlib.Algebra.Group.Defs
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 a * npowRec (n + 1) a * a = npowRec m a * npowRec (n + 1 + 1) a

Tactic:
simp only [npowRec, mul_assoc]

Premises used: mul_assoc, npowRec
-- Module: Mathlib.Algebra.Group.Defs
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
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
⊢ npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 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]

Premises used: mul_assoc, npowRec, Nat.add_assoc
-- Module: Mathlib.Algebra.Group.Defs
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
rw₄ rw₅ : a * npowRec n a = a * npowRec n a
⊢ npowRec (n + 1) a = a * npowRec n a

Tactic:
rw [Nat.add_comm, npowRec_add 1 n hn a ha, npowRec, npowRec, ha]

Premises used: npowRec_add, npowRec, OfNat.ofNat, Nat.add_comm
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Mul M
inst_1 : One M
k : ℕ
h : k ≠ 0
m : M
⊢ npowRec' (k + 1) m = npowRec' k m * m

Tactic:
match k with
  | _ + 1 => rfl

Premises used: HMul.hMul, npowRec', _private.0.npowRec'_succ.match_1, HAdd.hAdd, OfNat.ofNat, Eq, rfl
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
m : M
k' : ℕ
ih : ∀ (m_1 : ℕ), m_1 < 0 → npowRec' (2 * m_1) m = npowRec' m_1 (m * m)
⊢ npowRec' (HMul.hMul (α := ℕ) 2 0) m = npowRec' 0 (m * m)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
m : M
k' : ℕ
ih : ∀ (m_1 : ℕ), m_1 < 1 → npowRec' (2 * m_1) m = npowRec' m_1 (m * m)
⊢ npowRec' (HMul.hMul (α := ℕ) 2 1) m = npowRec' 1 (m * m)

Tactic:
simp [npowRec']

Premises used: npowRec'
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
m : M
k' k : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k + 2 → npowRec' (2 * m_1) m = npowRec' m_1 (m * m)
⊢ npowRec' (2 * (k + 2)) m = npowRec' (k + 2) (m * m)

Tactic:
simp [npowRec', ← mul_assoc, ← ih]

Premises used: npowRec', mul_assoc
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
m : M
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:
match k' with
    | 0 => rfl
    | 1 => simp [npowRec']
    | k + 2 => simp [npowRec', ← mul_assoc, ← ih]
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k : ℕ
m : M
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)
⊢ 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]
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
m : M
k' : ℕ
ih : ∀ (m_1 : ℕ), m_1 < 1 → ∀ (k0 : m_1 ≠ 0), m * npowRec' m_1 m = npowRec' m_1 m * m
k0 : Ne (α := ℕ) 1 0
⊢ m * npowRec' 1 m = npowRec' 1 m * m

Tactic:
simp [npowRec']

Premises used: npowRec'
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
m : M
k' k : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k + 2 → ∀ (k0 : m_1 ≠ 0), m * npowRec' m_1 m = npowRec' m_1 m * m
k0 : k + 2 ≠ 0
⊢ m * npowRec' (k + 2) m = npowRec' (k + 2) m * m

Tactic:
simp [npowRec', ← mul_assoc, ih]

Premises used: npowRec', mul_assoc
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
m : M
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:
match k' with
    | 1 => simp [npowRec']
    | k + 2 => simp [npowRec', ← mul_assoc, ih]
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k : ℕ
k0 : k ≠ 0
m : M
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
⊢ 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]
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
m : M
k' : ℕ
ih : ∀ (m_1 : ℕ), m_1 < 0 → npowRec (m_1 + 1) m = 1 * npowRec' (m_1 + 1) m
⊢ npowRec (HAdd.hAdd (α := ℕ) 0 1) m = 1 * npowRec' (HAdd.hAdd (α := ℕ) 0 1) m

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Defs
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
rw : npowRec (k + 1) m * m = 1 * npowRec' k.succ m * m
⊢ npowRec (k + 1 + 1) m = 1 * npowRec' (k + 1 + 1) m

Tactic:
rw [npowRec, npowRec'_succ k.succ_ne_zero, ← mul_assoc]

Premises used: npowRec'_succ, mul_assoc, npowRec, Nat.succ_ne_zero
-- Module: Mathlib.Algebra.Group.Defs
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
e_a : npowRec (k + 1) m = 1 * npowRec' k.succ m
⊢ npowRec (k + 1) m * m = 1 * npowRec' k.succ m * m

Tactic:
congr
-- Module: Mathlib.Algebra.Group.Defs
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 = 1 * npowRec' k.succ m

Tactic:
simp [ih]
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
m : M
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:
match k' with
    | 0 => rfl
    | k + 1 =>
      rw [npowRec, npowRec'_succ k.succ_ne_zero, ← mul_assoc]
      congr
      simp [ih]
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k : ℕ
m : M
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
⊢ 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]
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k : ℕ
m n : M
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
⊢ go (k + 1) m n = m * npowRec' (k + 1) n

Tactic:
unfold go

Premises used: npowBinRec.go
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k : ℕ
m n : M
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
⊢ 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:
generalize hk : k + 1 = k'
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k : ℕ
m n : M
k' : ℕ
hk : k + 1 = k'
⊢ k' ≠ 0

Tactic:
lia
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k : ℕ
m n : M
k' : ℕ
hk : k + 1 = k'
⊢ k' ≠ 0

Tactic:
replace hk : k' ≠ 0 := by lia
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k : ℕ
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:
simp at hk
-- Module: Mathlib.Algebra.Group.Defs
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
k : ℕ
m n : M
hk : Ne (α := ℕ) 1 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)) 1 m n =
    m * npowRec' 1 n

Tactic:
simp [npowRec']

Premises used: npowRec'
-- Module: Mathlib.Algebra.Group.Defs
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 : (bif b then m * n else m) * npowRec' k' (n * n) = m * npowRec' (Nat.bit b k') n
⊢ 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

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

Premises used: Or.inl, Nat.binaryRec_eq
-- Module: Mathlib.Algebra.Group.Defs
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
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
⊢ (bif b then m * n else m) * npowRec' k' (n * n) = m * npowRec' (Nat.bit b k') n

Tactic:
cases b
-- Module: Mathlib.Algebra.Group.Defs
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 false k' ≠ 0
⊢ (bif false then m * n else m) * npowRec' k' (n * n) = m * npowRec' (Nat.bit false k') n

Tactic:
simp only [Nat.bit, cond_false, cond_true, npowRec'_two_mul]

Premises used: Nat.bit, npowRec'_two_mul, cond_true, cond_false
-- Module: Mathlib.Algebra.Group.Defs
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' + 1) n
⊢ (bif true then m * n else m) * npowRec' k' (n * n) = m * npowRec' (Nat.bit true k') n

Tactic:
simp only [Nat.bit, cond_false, cond_true, npowRec'_two_mul]

Premises used: Nat.bit, npowRec'_two_mul, cond_true, cond_false
-- Module: Mathlib.Algebra.Group.Defs
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
⊢ 2 * k' ≠ 0

Tactic:
lia