awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ 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 one : ∀ (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: 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
-- 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
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
one :
  ∀ (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
⊢ 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 bit : ∀ (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
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
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
⊢ @npowRecAuto = @npowBinRecAuto
have h : ∀ (M : Type u_2) (x : Semigroup M) (x_1 : One M) (k : ℕ) (m : M), npowRecAuto k m = npowBinRecAuto k m
Tactic: funext M _ _ k m
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
x : Semigroup M
x_1 : One M
k : ℕ
m : M
⊢ npowRec 0 m = npowBinRec.go 0 1 m
have rw : 1 = npowBinRec.go 0 1 m
Tactic: rw [npowRec, npowBinRec.go, Nat.binaryRec_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
x : Semigroup M
x_1 : One M
k : ℕ
m : M
rw : 1 = npowBinRec.go 0 1 m
⊢ npowRec 0 m = npowBinRec.go 0 1 m
have rw₁ : Eq.{u_2 + 1} (α := M) (1 : M)
  (Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
      (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x_2 : M) ↦ fn (bif bn then y * x_2 else y) (x_2 * x_2)) 0 1 m :
    M)
Tactic: rw [npowRec, npowBinRec.go, Nat.binaryRec_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
x : Semigroup M
x_1 : One M
k : ℕ
m : M
rw : 1 = npowBinRec.go 0 1 m
rw₁ :
  Eq.{u_2 + 1} (α := M) (1 : M)
    (Nat.binaryRec (motive := fun (x : ℕ) ↦ M → M → M) (fun (y x : M) ↦ y)
        (fun (bn : Bool) (_n : ℕ) (fn : M → M → M) (y x_2 : M) ↦ fn (bif bn then y * x_2 else y) (x_2 * x_2)) 0 1 m :
      M)
⊢ npowRec 0 m = npowBinRec.go 0 1 m
have rw₂ : Eq.{u_2 + 1} (α := M) 1 1
Tactic: rw [npowRec, npowBinRec.go, Nat.binaryRec_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
x : Semigroup M
x_1 : One M
k_1 : ℕ
m : M
k : ℕ
⊢ npowRec (k + 1) m = npowBinRec.go (k + 1) 1 m
have rw : npowRec (k + 1) m = 1 * npowRec' (k + 1) m
Tactic: rw [npowBinRec.go_spec, npowRec_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
x : Semigroup M
x_1 : One M
k_1 : ℕ
m : M
k : ℕ
rw : npowRec (k + 1) m = 1 * npowRec' (k + 1) m
⊢ npowRec (k + 1) m = npowBinRec.go (k + 1) 1 m
have rw₁ : 1 * npowRec' (k + 1) m = 1 * npowRec' (k + 1) m
Tactic: rw [npowBinRec.go_spec, npowRec_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
n : ℕ
m : M
⊢ npowBinRec (n + 1) m = npowBinRec n m * m
have rw : npowRecAuto (n + 1) m = npowBinRec n m * m
Tactic: rw [← npowBinRecAuto, ← npowRec_eq_npowBinRec]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
n : ℕ
m : M
⊢ npowRecAuto (n + 1) m = npowBinRec n m * m
have rw : npowRecAuto (n + 1) m = npowRecAuto n m * m
Tactic: rw [← npowBinRecAuto, ← npowRec_eq_npowBinRec]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Semigroup M
inst_1 : One M
n : ℕ
m : M
⊢ npowBinRec (n + 1) m = npowBinRec n m * m
have iterate : npowRecAuto (n + 1) m = npowRecAuto n m * m
Tactic: iterate 2 rw [← npowBinRecAuto, ← npowRec_eq_npowBinRec]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a b c : M
hba : b * a = 1
hac : a * c = 1
⊢ b = c
have rw : b = 1 * c
Tactic: rw [← one_mul c, ← hba, mul_assoc, hac, mul_one b]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a b c : M
hba : b * a = 1
hac : a * c = 1
rw : b = 1 * c
⊢ b = c
have rw₁ : b = b * a * c
Tactic: rw [← one_mul c, ← hba, mul_assoc, hac, mul_one b]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a b c : M
hba : b * a = 1
hac : a * c = 1
rw : b = 1 * c
rw₁ : b = b * a * c
⊢ b = c
have rw₂ : b = b * (a * c)
Tactic: rw [← one_mul c, ← hba, mul_assoc, hac, mul_one b]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a b c : M
hba : b * a = 1
hac : a * c = 1
rw : b = 1 * c
rw₁ : b = b * a * c
rw₂ : b = b * (a * c)
⊢ b = c
have rw₃ : b = b * 1
Tactic: rw [← one_mul c, ← hba, mul_assoc, hac, mul_one b]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a b c : M
hba : b * a = 1
hac : a * c = 1
rw : b = 1 * c
rw₁ : b = b * a * c
rw₂ : b = b * (a * c)
rw₃ : b = b * 1
⊢ b = c
have rw₄ : b = b
Tactic: rw [← one_mul c, ← hba, mul_assoc, hac, mul_one b]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
⊢ HPow.hPow (β := ℕ) a 1 = a
have rw : HPow.hPow (β := ℕ) a 0 * a = a
Tactic: rw [pow_succ, pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
rw : HPow.hPow (β := ℕ) a 0 * a = a
⊢ HPow.hPow (β := ℕ) a 1 = a
have rw₁ : 1 * a = a
Tactic: rw [pow_succ, pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
rw : HPow.hPow (β := ℕ) a 0 * a = a
rw₁ : 1 * a = a
⊢ HPow.hPow (β := ℕ) a 1 = a
have rw₂ : a = a
Tactic: rw [pow_succ, pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
n : ℕ
⊢ a ^ (n + 1 + 1) = a * a ^ (n + 1)
have rw : a ^ (n + 1 + 1) = a * (a ^ n * a)
Tactic: rw [pow_succ _ n, pow_succ, pow_succ', mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
n : ℕ
rw : a ^ (n + 1 + 1) = a * (a ^ n * a)
⊢ a ^ (n + 1 + 1) = a * a ^ (n + 1)
have rw₁ : a ^ (n + 1) * a = a * (a ^ n * a)
Tactic: rw [pow_succ _ n, pow_succ, pow_succ', mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
n : ℕ
rw : a ^ (n + 1 + 1) = a * (a ^ n * a)
rw₁ : a ^ (n + 1) * a = a * (a ^ n * a)
⊢ a ^ (n + 1 + 1) = a * a ^ (n + 1)
have rw₂ : a * a ^ n * a = a * (a ^ n * a)
Tactic: rw [pow_succ _ n, pow_succ, pow_succ', mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
n : ℕ
rw : a ^ (n + 1 + 1) = a * (a ^ n * a)
rw₁ : a ^ (n + 1) * a = a * (a ^ n * a)
rw₂ : a * a ^ n * a = a * (a ^ n * a)
⊢ a ^ (n + 1 + 1) = a * a ^ (n + 1)
have rw₃ : a * (a ^ n * a) = a * (a ^ n * a)
Tactic: rw [pow_succ _ n, pow_succ, pow_succ', mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a b : M
n : ℕ
⊢ (a * b) ^ n * a = a * (b * a) ^ n
have zero : HPow.hPow (β := ℕ) (a * b) 0 * a = a * HPow.hPow (β := ℕ) (b * a) 0
Tactic: induction n with
  | zero => simp
  | succ n ih => simp [pow_succ', ← ih, mul_assoc]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a b : M
n : ℕ
zero : HPow.hPow (β := ℕ) (a * b) 0 * a = a * HPow.hPow (β := ℕ) (b * a) 0
⊢ (a * b) ^ n * a = a * (b * a) ^ n
have succ : ∀ (n : ℕ) (ih : (a * b) ^ n * a = a * (b * a) ^ n), (a * b) ^ (n + 1) * a = a * (b * a) ^ (n + 1)
Tactic: induction n with
  | zero => simp
  | succ n ih => simp [pow_succ', ← ih, mul_assoc]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
n : ℕ
⊢ a ^ n * a = a * a ^ n
have rw : a ^ (n + 1) = a * a ^ n
Tactic: rw [← pow_succ, pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
n : ℕ
rw : a ^ (n + 1) = a * a ^ n
⊢ a ^ n * a = a * a ^ n
have rw₁ : a * a ^ n = a * a ^ n
Tactic: rw [← pow_succ, pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
⊢ HPow.hPow (β := ℕ) a 2 = a * a
have rw : HPow.hPow (β := ℕ) a 1 * a = a * a
Tactic: rw [pow_succ, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
rw : HPow.hPow (β := ℕ) a 1 * a = a * a
⊢ HPow.hPow (β := ℕ) a 2 = a * a
have rw₁ : a * a = a * a
Tactic: rw [pow_succ, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
⊢ HPow.hPow (β := ℕ) a 3 = a * a * a
have rw : HPow.hPow (β := ℕ) a 2 * a = a * a * a
Tactic: rw [pow_succ, pow_two]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
rw : HPow.hPow (β := ℕ) a 2 * a = a * a * a
⊢ HPow.hPow (β := ℕ) a 3 = a * a * a
have rw₁ : a * a * a = a * a * a
Tactic: rw [pow_succ, pow_two]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
⊢ HPow.hPow (β := ℕ) a 3 = a * (a * a)
have rw : a * HPow.hPow (β := ℕ) a 2 = a * (a * a)
Tactic: rw [pow_succ', pow_two]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
rw : a * HPow.hPow (β := ℕ) a 2 = a * (a * a)
⊢ HPow.hPow (β := ℕ) a 3 = a * (a * a)
have rw₁ : a * (a * a) = a * (a * a)
Tactic: rw [pow_succ', pow_two]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
n : ℕ
⊢ HPow.hPow (α := M) 1 (n + 1) = 1
have rw : HPow.hPow (α := M) 1 n * 1 = 1
Tactic: rw [pow_succ, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
n : ℕ
rw : HPow.hPow (α := M) 1 n * 1 = 1
⊢ HPow.hPow (α := M) 1 (n + 1) = 1
have rw₁ : HMul.hMul (α := M) 1 1 = 1
Tactic: rw [pow_succ, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
n : ℕ
rw : HPow.hPow (α := M) 1 n * 1 = 1
rw₁ : HMul.hMul (α := M) 1 1 = 1
⊢ HPow.hPow (α := M) 1 (n + 1) = 1
have rw₂ : Eq.{u_2 + 1} (α := M) 1 1
Tactic: rw [pow_succ, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
m : ℕ
⊢ a ^ (m + 0) = a ^ m * HPow.hPow (β := ℕ) a 0
have rw : a ^ m = a ^ m * HPow.hPow (β := ℕ) a 0
Tactic: rw [Nat.add_zero, pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
m : ℕ
rw : a ^ m = a ^ m * HPow.hPow (β := ℕ) a 0
⊢ a ^ (m + 0) = a ^ m * HPow.hPow (β := ℕ) a 0
have rw₁ : a ^ m = a ^ m * 1
Tactic: rw [Nat.add_zero, pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
m : ℕ
rw : a ^ m = a ^ m * HPow.hPow (β := ℕ) a 0
rw₁ : a ^ m = a ^ m * 1
⊢ a ^ (m + 0) = a ^ m * HPow.hPow (β := ℕ) a 0
have rw₂ : a ^ m = a ^ m
Tactic: rw [Nat.add_zero, pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
m n : ℕ
⊢ a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1)
have rw : a ^ (m + (n + 1)) = a ^ m * (a ^ n * a)
Tactic: rw [pow_succ, ← mul_assoc, ← pow_add, ← pow_succ, Nat.add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
m n : ℕ
rw : a ^ (m + (n + 1)) = a ^ m * (a ^ n * a)
⊢ a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1)
have rw₁ : a ^ (m + (n + 1)) = a ^ m * a ^ n * a
Tactic: rw [pow_succ, ← mul_assoc, ← pow_add, ← pow_succ, Nat.add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
m n : ℕ
rw : a ^ (m + (n + 1)) = a ^ m * (a ^ n * a)
rw₁ : a ^ (m + (n + 1)) = a ^ m * a ^ n * a
⊢ a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1)
have rw₂ : a ^ (m + (n + 1)) = a ^ (m + n) * a
Tactic: rw [pow_succ, ← mul_assoc, ← pow_add, ← pow_succ, Nat.add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
m n : ℕ
rw : a ^ (m + (n + 1)) = a ^ m * (a ^ n * a)
rw₁ : a ^ (m + (n + 1)) = a ^ m * a ^ n * a
rw₂ : a ^ (m + (n + 1)) = a ^ (m + n) * a
⊢ a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1)
have rw₃ : a ^ (m + (n + 1)) = a ^ (m + n + 1)
Tactic: rw [pow_succ, ← mul_assoc, ← pow_add, ← pow_succ, Nat.add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
m n : ℕ
rw : a ^ (m + (n + 1)) = a ^ m * (a ^ n * a)
rw₁ : a ^ (m + (n + 1)) = a ^ m * a ^ n * a
rw₂ : a ^ (m + (n + 1)) = a ^ (m + n) * a
rw₃ : a ^ (m + (n + 1)) = a ^ (m + n + 1)
⊢ a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1)
have rw₄ : a ^ (m + (n + 1)) = a ^ (m + (n + 1))
Tactic: rw [pow_succ, ← mul_assoc, ← pow_add, ← pow_succ, Nat.add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
m n : ℕ
⊢ a ^ m * a ^ n = a ^ n * a ^ m
have rw : a ^ (m + n) = a ^ n * a ^ m
Tactic: rw [← pow_add, ← pow_add, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
m n : ℕ
rw : a ^ (m + n) = a ^ n * a ^ m
⊢ a ^ m * a ^ n = a ^ n * a ^ m
have rw₁ : a ^ (m + n) = a ^ (n + m)
Tactic: rw [← pow_add, ← pow_add, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
m n : ℕ
rw : a ^ (m + n) = a ^ n * a ^ m
rw₁ : a ^ (m + n) = a ^ (n + m)
⊢ a ^ m * a ^ n = a ^ n * a ^ m
have rw₂ : a ^ (n + m) = a ^ (n + m)
Tactic: rw [← pow_add, ← pow_add, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
m : ℕ
⊢ a ^ (m * 0) = HPow.hPow (β := ℕ) (a ^ m) 0
have rw : HPow.hPow (β := ℕ) a 0 = HPow.hPow (β := ℕ) (a ^ m) 0
Tactic: rw [Nat.mul_zero, pow_zero, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
m : ℕ
rw : HPow.hPow (β := ℕ) a 0 = HPow.hPow (β := ℕ) (a ^ m) 0
⊢ a ^ (m * 0) = HPow.hPow (β := ℕ) (a ^ m) 0
have rw₁ : 1 = HPow.hPow (β := ℕ) (a ^ m) 0
Tactic: rw [Nat.mul_zero, pow_zero, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
m : ℕ
rw : HPow.hPow (β := ℕ) a 0 = HPow.hPow (β := ℕ) (a ^ m) 0
rw₁ : 1 = HPow.hPow (β := ℕ) (a ^ m) 0
⊢ a ^ (m * 0) = HPow.hPow (β := ℕ) (a ^ m) 0
have rw₂ : Eq.{u_2 + 1} (α := M) 1 1
Tactic: rw [Nat.mul_zero, pow_zero, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
m n : ℕ
⊢ a ^ (m * (n + 1)) = (a ^ m) ^ (n + 1)
have rw : a ^ (m * n + m) = (a ^ m) ^ (n + 1)
Tactic: rw [Nat.mul_succ, pow_add, pow_succ, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
m n : ℕ
rw : a ^ (m * n + m) = (a ^ m) ^ (n + 1)
⊢ a ^ (m * (n + 1)) = (a ^ m) ^ (n + 1)
have rw₁ : a ^ (m * n) * a ^ m = (a ^ m) ^ (n + 1)
Tactic: rw [Nat.mul_succ, pow_add, pow_succ, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
m n : ℕ
rw : a ^ (m * n + m) = (a ^ m) ^ (n + 1)
rw₁ : a ^ (m * n) * a ^ m = (a ^ m) ^ (n + 1)
⊢ a ^ (m * (n + 1)) = (a ^ m) ^ (n + 1)
have rw₂ : a ^ (m * n) * a ^ m = (a ^ m) ^ n * a ^ m
Tactic: rw [Nat.mul_succ, pow_add, pow_succ, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
m n : ℕ
rw : a ^ (m * n + m) = (a ^ m) ^ (n + 1)
rw₁ : a ^ (m * n) * a ^ m = (a ^ m) ^ (n + 1)
rw₂ : a ^ (m * n) * a ^ m = (a ^ m) ^ n * a ^ m
⊢ a ^ (m * (n + 1)) = (a ^ m) ^ (n + 1)
have rw₃ : (a ^ m) ^ n * a ^ m = (a ^ m) ^ n * a ^ m
Tactic: rw [Nat.mul_succ, pow_add, pow_succ, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
m n : ℕ
⊢ a ^ (m * n) = (a ^ n) ^ m
have rw : a ^ (n * m) = (a ^ n) ^ m
Tactic: rw [Nat.mul_comm, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
m n : ℕ
rw : a ^ (n * m) = (a ^ n) ^ m
⊢ a ^ (m * n) = (a ^ n) ^ m
have rw₁ : (a ^ n) ^ m = (a ^ n) ^ m
Tactic: rw [Nat.mul_comm, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
m n : ℕ
⊢ (a ^ m) ^ n = (a ^ n) ^ m
have rw : a ^ (m * n) = (a ^ n) ^ m
Tactic: rw [← pow_mul, Nat.mul_comm, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
m n : ℕ
rw : a ^ (m * n) = (a ^ n) ^ m
⊢ (a ^ m) ^ n = (a ^ n) ^ m
have rw₁ : a ^ (n * m) = (a ^ n) ^ m
Tactic: rw [← pow_mul, Nat.mul_comm, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
m n : ℕ
rw : a ^ (m * n) = (a ^ n) ^ m
rw₁ : a ^ (n * m) = (a ^ n) ^ m
⊢ (a ^ m) ^ n = (a ^ n) ^ m
have rw₂ : (a ^ n) ^ m = (a ^ n) ^ m
Tactic: rw [← pow_mul, Nat.mul_comm, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ (z : M), y * z = 1
x y : M
h : x * y = 1
⊢ y * x = 1
have have : ∀ (z : M) (hz : y * z = 1), y * x = 1
Tactic: have ⟨z, hz⟩ := ex x y h
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ (z : M), z * x = 1
x y : M
h : x * y = 1
⊢ y * x = 1
have have : ∀ (z : M) (hz : z * x = 1), y * x = 1
Tactic: have ⟨z, hz⟩ := ex x y h
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : DivInvMonoid G
a : G
n : ℕ
⊢ a ^ Int.negSucc n = (a ^ (n + 1))⁻¹
have rw : a ^ Int.negSucc n = (HPow.hPow (β := ℤ) a (↑(n + 1) : ℤ))⁻¹
Tactic: rw [← zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_2
inst : SubNegMonoid G
a : G
n : ℕ
⊢ Int.negSucc n • a = -((n + 1) • a)
have rw : Int.negSucc n • a = -HSMul.hSMul (α := ℤ) (↑(n + 1) : ℤ) a
Tactic: rw [← natCast_zsmul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : DivInvMonoid G
x : G
⊢ x⁻¹ = 1 / x
have rw : x⁻¹ = 1 * x⁻¹
Tactic: rw [div_eq_mul_inv, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : DivInvMonoid G
x : G
rw : x⁻¹ = 1 * x⁻¹
⊢ x⁻¹ = 1 / x
have rw₁ : x⁻¹ = x⁻¹
Tactic: rw [div_eq_mul_inv, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : DivInvMonoid G
a b c : G
⊢ a * b / c = a * (b / c)
have rw : a * b * c⁻¹ = a * (b / c)
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, mul_assoc _ _ _]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : DivInvMonoid G
a b c : G
rw : a * b * c⁻¹ = a * (b / c)
⊢ a * b / c = a * (b / c)
have rw₁ : a * b * c⁻¹ = a * (b * c⁻¹)
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, mul_assoc _ _ _]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : DivInvMonoid G
a b c : G
rw : a * b * c⁻¹ = a * (b / c)
rw₁ : a * b * c⁻¹ = a * (b * c⁻¹)
⊢ a * b / c = a * (b / c)
have rw₂ : a * (b * c⁻¹) = a * (b * c⁻¹)
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, mul_assoc _ _ _]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : DivInvMonoid G
a : G
⊢ HPow.hPow (β := ℤ) a 1 = a
have rw : HPow.hPow (β := ℕ) a 1 = a
Tactic: rw [zpow_ofNat, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : DivInvMonoid G
a : G
rw : HPow.hPow (β := ℕ) a 1 = a
⊢ HPow.hPow (β := ℤ) a 1 = a
have rw₁ : a = a
Tactic: rw [zpow_ofNat, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : DivInvMonoid G
a : G
⊢ HPow.hPow (β := ℤ) a 2 = a * a
have rw : HPow.hPow (β := ℕ) a 2 = a * a
Tactic: rw [zpow_ofNat, pow_two]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : DivInvMonoid G
a : G
rw : HPow.hPow (β := ℕ) a 2 = a * a
⊢ HPow.hPow (β := ℤ) a 2 = a * a
have rw₁ : a * a = a * a
Tactic: rw [zpow_ofNat, pow_two]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : DivisionMonoid G
a b : G
h : a * b = 1
⊢ b⁻¹ = a
have rw : a⁻¹⁻¹ = a
Tactic: rw [← inv_eq_of_mul_eq_one_right h, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : DivisionMonoid G
a b : G
h : a * b = 1
rw : a⁻¹⁻¹ = a
⊢ b⁻¹ = a
have rw₁ : a = a
Tactic: rw [← inv_eq_of_mul_eq_one_right h, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a : G
⊢ a * a⁻¹ = 1
have rw : a * a⁻¹ = a⁻¹⁻¹ * a⁻¹
Tactic: rw [← inv_mul_cancel a⁻¹, inv_eq_of_mul (inv_mul_cancel a)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a : G
rw : a * a⁻¹ = a⁻¹⁻¹ * a⁻¹
⊢ a * a⁻¹ = 1
have rw₁ : a * a⁻¹ = a * a⁻¹
Tactic: rw [← inv_mul_cancel a⁻¹, inv_eq_of_mul (inv_mul_cancel a)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a : G
⊢ a / a = 1
have rw : a * a⁻¹ = 1
Tactic: rw [div_eq_mul_inv, mul_inv_cancel a]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a : G
rw : a * a⁻¹ = 1
⊢ a / a = 1
have rw₁ : Eq.{u_1 + 1} (α := G) 1 1
Tactic: rw [div_eq_mul_inv, mul_inv_cancel a]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
⊢ a⁻¹ * (a * b) = b
have rw : a⁻¹ * a * b = b
Tactic: rw [← mul_assoc, inv_mul_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
rw : a⁻¹ * a * b = b
⊢ a⁻¹ * (a * b) = b
have rw₁ : 1 * b = b
Tactic: rw [← mul_assoc, inv_mul_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Defs (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
rw : a⁻¹ * a * b = b
rw₁ : 1 * b = b
⊢ a⁻¹ * (a * b) = b
have rw₂ : b = b
Tactic: rw [← mul_assoc, inv_mul_cancel, one_mul]