awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
M : Type u_1
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
x : M
m : ℕ
⊢ x ^ (m * 0) = HPow.hPow (β := ℕ) (x ^ m) 0
have zero : x ^ (m * 0) = 1
Tactic: rw [npow_zero, mul_zero, npow_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
M : Type u_1
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
x : M
m : ℕ
zero : x ^ (m * 0) = 1
⊢ x ^ (m * 0) = HPow.hPow (β := ℕ) (x ^ m) 0
have zero₁ : HPow.hPow (β := ℕ) x 0 = 1
Tactic: rw [npow_zero, mul_zero, npow_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
M : Type u_1
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
x : M
m : ℕ
zero : x ^ (m * 0) = 1
zero₁ : HPow.hPow (β := ℕ) x 0 = 1
⊢ x ^ (m * 0) = HPow.hPow (β := ℕ) (x ^ m) 0
have zero₂ : Eq.{u_1 + 1} (α := M) 1 1
Tactic: rw [npow_zero, mul_zero, npow_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
M : Type u_1
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
x : M
m n : ℕ
ih : x ^ (m * n) = (x ^ m) ^ n
⊢ x ^ (m * (n + 1)) = (x ^ m) ^ (n + 1)
have succ : x ^ (m * n + m * 1) = (x ^ m) ^ (n + 1)
Tactic: rw [mul_add, npow_add, ih, mul_one, npow_add, npow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
M : Type u_1
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
x : M
m n : ℕ
ih : x ^ (m * n) = (x ^ m) ^ n
succ : x ^ (m * n + m * 1) = (x ^ m) ^ (n + 1)
⊢ x ^ (m * (n + 1)) = (x ^ m) ^ (n + 1)
have succ₁ : x ^ (m * n) * x ^ (m * 1) = (x ^ m) ^ (n + 1)
Tactic: rw [mul_add, npow_add, ih, mul_one, npow_add, npow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
M : Type u_1
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
x : M
m n : ℕ
ih : x ^ (m * n) = (x ^ m) ^ n
succ : x ^ (m * n + m * 1) = (x ^ m) ^ (n + 1)
succ₁ : x ^ (m * n) * x ^ (m * 1) = (x ^ m) ^ (n + 1)
⊢ x ^ (m * (n + 1)) = (x ^ m) ^ (n + 1)
have succ₂ : (x ^ m) ^ n * x ^ (m * 1) = (x ^ m) ^ (n + 1)
Tactic: rw [mul_add, npow_add, ih, mul_one, npow_add, npow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
M : Type u_1
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
x : M
m n : ℕ
ih : x ^ (m * n) = (x ^ m) ^ n
succ : x ^ (m * n + m * 1) = (x ^ m) ^ (n + 1)
succ₁ : x ^ (m * n) * x ^ (m * 1) = (x ^ m) ^ (n + 1)
succ₂ : (x ^ m) ^ n * x ^ (m * 1) = (x ^ m) ^ (n + 1)
⊢ x ^ (m * (n + 1)) = (x ^ m) ^ (n + 1)
have succ₃ : (x ^ m) ^ n * x ^ m = (x ^ m) ^ (n + 1)
Tactic: rw [mul_add, npow_add, ih, mul_one, npow_add, npow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
M : Type u_1
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
x : M
m n : ℕ
ih : x ^ (m * n) = (x ^ m) ^ n
succ : x ^ (m * n + m * 1) = (x ^ m) ^ (n + 1)
succ₁ : x ^ (m * n) * x ^ (m * 1) = (x ^ m) ^ (n + 1)
succ₂ : (x ^ m) ^ n * x ^ (m * 1) = (x ^ m) ^ (n + 1)
succ₃ : (x ^ m) ^ n * x ^ m = (x ^ m) ^ (n + 1)
⊢ x ^ (m * (n + 1)) = (x ^ m) ^ (n + 1)
have succ₄ : (x ^ m) ^ n * x ^ m = (x ^ m) ^ n * HPow.hPow (β := ℕ) (x ^ m) 1
Tactic: rw [mul_add, npow_add, ih, mul_one, npow_add, npow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
M : Type u_1
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
x : M
m n : ℕ
ih : x ^ (m * n) = (x ^ m) ^ n
succ : x ^ (m * n + m * 1) = (x ^ m) ^ (n + 1)
succ₁ : x ^ (m * n) * x ^ (m * 1) = (x ^ m) ^ (n + 1)
succ₂ : (x ^ m) ^ n * x ^ (m * 1) = (x ^ m) ^ (n + 1)
succ₃ : (x ^ m) ^ n * x ^ m = (x ^ m) ^ (n + 1)
succ₄ : (x ^ m) ^ n * x ^ m = (x ^ m) ^ n * HPow.hPow (β := ℕ) (x ^ m) 1
⊢ x ^ (m * (n + 1)) = (x ^ m) ^ (n + 1)
have succ₅ : (x ^ m) ^ n * x ^ m = (x ^ m) ^ n * x ^ m
Tactic: rw [mul_add, npow_add, ih, mul_one, npow_add, npow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
M : Type u_1
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
x : M
m n : ℕ
⊢ x ^ (m * n) = (x ^ m) ^ n
have zero : x ^ (m * 0) = HPow.hPow (β := ℕ) (x ^ m) 0
Tactic: induction n with
  | zero => rw [npow_zero, mul_zero, npow_zero]
  | succ n ih => rw [mul_add, npow_add, ih, mul_one, npow_add, npow_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
M : Type u_1
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
x : M
m n : ℕ
zero : x ^ (m * 0) = HPow.hPow (β := ℕ) (x ^ m) 0
⊢ x ^ (m * n) = (x ^ m) ^ n
have succ : ∀ (n : ℕ) (ih : x ^ (m * n) = (x ^ m) ^ n), x ^ (m * (n + 1)) = (x ^ m) ^ (n + 1)
Tactic: induction n with
  | zero => rw [npow_zero, mul_zero, npow_zero]
  | succ n ih => rw [mul_add, npow_add, ih, mul_one, npow_add, npow_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
M : Type u_1
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
x : M
m n : ℕ
⊢ x ^ (m * n) = (x ^ n) ^ m
have rw : x ^ (n * m) = (x ^ n) ^ m
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
a b : R
k : ℕ
ih : HPow.hPow (α := R) (-1) k * a * b = HPow.hPow (α := R) (-1) k * (a * b)
⊢ HPow.hPow (α := R) (-1) (k + 1) * a * b = HPow.hPow (α := R) (-1) (k + 1) * (a * b)
have succ : -HPow.hPow (α := R) (-1) k * a * b = -HPow.hPow (α := R) (-1) k * (a * b)
Tactic: rw [npow_add, npow_one, ← neg_mul_comm, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
a b : R
k : ℕ
⊢ HPow.hPow (α := R) (-1) k * a * b = HPow.hPow (α := R) (-1) k * (a * b)
have zero : HPow.hPow (α := R) (β := ℕ) (-1) 0 * a * b = HPow.hPow (α := R) (β := ℕ) (-1) 0 * (a * b)
Tactic: induction k with
  | zero => simp only [npow_zero, one_mul]
  | succ k ih =>
    rw [npow_add, npow_one, ← neg_mul_comm, mul_one]
    simp only [neg_mul, ih]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
a b : R
k : ℕ
zero : HPow.hPow (α := R) (β := ℕ) (-1) 0 * a * b = HPow.hPow (α := R) (β := ℕ) (-1) 0 * (a * b)
⊢ HPow.hPow (α := R) (-1) k * a * b = HPow.hPow (α := R) (-1) k * (a * b)
have succ : ∀ (k : ℕ) (ih : HPow.hPow (α := R) (-1) k * a * b = HPow.hPow (α := R) (-1) k * (a * b)),
  HPow.hPow (α := R) (-1) (k + 1) * a * b = HPow.hPow (α := R) (-1) (k + 1) * (a * b)
Tactic: induction k with
  | zero => simp only [npow_zero, one_mul]
  | succ k ih =>
    rw [npow_add, npow_one, ← neg_mul_comm, mul_one]
    simp only [neg_mul, ih]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst : (i : ι) → MulOneClass (α i)
inst_1 : (i : ι) → Pow (α i) ℕ
inst_2 : ∀ (i : ι), NatPowAssoc.{u_3} (α i)
x x_1 : ℕ
x_2 : (i : ι) → α i
⊢ x_2 ^ (x + x_1) = x_2 ^ x * x_2 ^ x_1
have h : ∀ (x_3 : ι), (x_2 ^ (x + x_1)) x_3 = (x_2 ^ x * x_2 ^ x_1) x_3
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst : (i : ι) → MulOneClass (α i)
inst_1 : (i : ι) → Pow (α i) ℕ
inst_2 : ∀ (i : ι), NatPowAssoc.{u_3} (α i)
x : (i : ι) → α i
⊢ HPow.hPow (β := ℕ) x 0 = 1
have h : ∀ (x_1 : ι), HPow.hPow (β := ℕ) x 0 x_1 = 1 x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst : (i : ι) → MulOneClass (α i)
inst_1 : (i : ι) → Pow (α i) ℕ
inst_2 : ∀ (i : ι), NatPowAssoc.{u_3} (α i)
x : (i : ι) → α i
⊢ HPow.hPow (β := ℕ) x 1 = x
have h : ∀ (x_1 : ι), HPow.hPow (β := ℕ) x 1 x_1 = x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
inst_3 : MulOneClass N
inst_4 : Pow N ℕ
inst_5 : NatPowAssoc N
x x_1 : ℕ
x_2 : M × N
⊢ x_2 ^ (x + x_1) = x_2 ^ x * x_2 ^ x_1
have fst : (x_2 ^ (x + x_1)).1 = (x_2 ^ x * x_2 ^ x_1).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
inst_3 : MulOneClass N
inst_4 : Pow N ℕ
inst_5 : NatPowAssoc N
x x_1 : ℕ
x_2 : M × N
fst : (x_2 ^ (x + x_1)).1 = (x_2 ^ x * x_2 ^ x_1).1
⊢ x_2 ^ (x + x_1) = x_2 ^ x * x_2 ^ x_1
have snd : (x_2 ^ (x + x_1)).2 = (x_2 ^ x * x_2 ^ x_1).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
inst_3 : MulOneClass N
inst_4 : Pow N ℕ
inst_5 : NatPowAssoc N
x : M × N
⊢ HPow.hPow (β := ℕ) x 0 = 1
have fst : (HPow.hPow (β := ℕ) x 0).1 = 1.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
inst_3 : MulOneClass N
inst_4 : Pow N ℕ
inst_5 : NatPowAssoc N
x : M × N
fst : (HPow.hPow (β := ℕ) x 0).1 = 1.1
⊢ HPow.hPow (β := ℕ) x 0 = 1
have snd : (HPow.hPow (β := ℕ) x 0).2 = 1.2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
inst_3 : MulOneClass N
inst_4 : Pow N ℕ
inst_5 : NatPowAssoc N
x : M × N
⊢ HPow.hPow (β := ℕ) x 1 = x
have fst : (HPow.hPow (β := ℕ) x 1).1 = x.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : Pow M ℕ
inst_2 : NatPowAssoc M
inst_3 : MulOneClass N
inst_4 : Pow N ℕ
inst_5 : NatPowAssoc N
x : M × N
fst : (HPow.hPow (β := ℕ) x 1).1 = x.1
⊢ HPow.hPow (β := ℕ) x 1 = x
have snd : (HPow.hPow (β := ℕ) x 1).2 = x.2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n m : ℕ
ih : (↑(n ^ m) : R) = HPow.hPow (α := R) (↑n : R) m
⊢ (↑(n ^ (m + 1)) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
have succ : (↑(n ^ m * HPow.hPow (β := ℕ) n 1) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
Tactic: rw [npow_add, npow_add, Nat.cast_mul, ih, npow_one, npow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n m : ℕ
ih : (↑(n ^ m) : R) = HPow.hPow (α := R) (↑n : R) m
succ : (↑(n ^ m * HPow.hPow (β := ℕ) n 1) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
⊢ (↑(n ^ (m + 1)) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
have succ₁ : (↑(n ^ m * HPow.hPow (β := ℕ) n 1) : R) = HPow.hPow (α := R) (↑n : R) m * HPow.hPow (α := R) (β := ℕ) (↑n : R) 1
Tactic: rw [npow_add, npow_add, Nat.cast_mul, ih, npow_one, npow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n m : ℕ
ih : (↑(n ^ m) : R) = HPow.hPow (α := R) (↑n : R) m
succ : (↑(n ^ m * HPow.hPow (β := ℕ) n 1) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
succ₁ : (↑(n ^ m * HPow.hPow (β := ℕ) n 1) : R) = HPow.hPow (α := R) (↑n : R) m * HPow.hPow (α := R) (β := ℕ) (↑n : R) 1
⊢ (↑(n ^ (m + 1)) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
have succ₂ : HMul.hMul (α := R) (↑(n ^ m) : R) (↑(HPow.hPow (β := ℕ) n 1) : R) =
  HPow.hPow (α := R) (↑n : R) m * HPow.hPow (α := R) (β := ℕ) (↑n : R) 1
Tactic: rw [npow_add, npow_add, Nat.cast_mul, ih, npow_one, npow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n m : ℕ
ih : (↑(n ^ m) : R) = HPow.hPow (α := R) (↑n : R) m
succ : (↑(n ^ m * HPow.hPow (β := ℕ) n 1) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
succ₁ : (↑(n ^ m * HPow.hPow (β := ℕ) n 1) : R) = HPow.hPow (α := R) (↑n : R) m * HPow.hPow (α := R) (β := ℕ) (↑n : R) 1
succ₂ :
  HMul.hMul (α := R) (↑(n ^ m) : R) (↑(HPow.hPow (β := ℕ) n 1) : R) =
    HPow.hPow (α := R) (↑n : R) m * HPow.hPow (α := R) (β := ℕ) (↑n : R) 1
⊢ (↑(n ^ (m + 1)) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
have succ₃ : HPow.hPow (α := R) (↑n : R) m * (↑(HPow.hPow (β := ℕ) n 1) : R) =
  HPow.hPow (α := R) (↑n : R) m * HPow.hPow (α := R) (β := ℕ) (↑n : R) 1
Tactic: rw [npow_add, npow_add, Nat.cast_mul, ih, npow_one, npow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n m : ℕ
ih : (↑(n ^ m) : R) = HPow.hPow (α := R) (↑n : R) m
succ : (↑(n ^ m * HPow.hPow (β := ℕ) n 1) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
succ₁ : (↑(n ^ m * HPow.hPow (β := ℕ) n 1) : R) = HPow.hPow (α := R) (↑n : R) m * HPow.hPow (α := R) (β := ℕ) (↑n : R) 1
succ₂ :
  HMul.hMul (α := R) (↑(n ^ m) : R) (↑(HPow.hPow (β := ℕ) n 1) : R) =
    HPow.hPow (α := R) (↑n : R) m * HPow.hPow (α := R) (β := ℕ) (↑n : R) 1
succ₃ :
  HPow.hPow (α := R) (↑n : R) m * (↑(HPow.hPow (β := ℕ) n 1) : R) =
    HPow.hPow (α := R) (↑n : R) m * HPow.hPow (α := R) (β := ℕ) (↑n : R) 1
⊢ (↑(n ^ (m + 1)) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
have succ₄ : HPow.hPow (α := R) (↑n : R) m * (↑n : R) = HPow.hPow (α := R) (↑n : R) m * HPow.hPow (α := R) (β := ℕ) (↑n : R) 1
Tactic: rw [npow_add, npow_add, Nat.cast_mul, ih, npow_one, npow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n m : ℕ
ih : (↑(n ^ m) : R) = HPow.hPow (α := R) (↑n : R) m
succ : (↑(n ^ m * HPow.hPow (β := ℕ) n 1) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
succ₁ : (↑(n ^ m * HPow.hPow (β := ℕ) n 1) : R) = HPow.hPow (α := R) (↑n : R) m * HPow.hPow (α := R) (β := ℕ) (↑n : R) 1
succ₂ :
  HMul.hMul (α := R) (↑(n ^ m) : R) (↑(HPow.hPow (β := ℕ) n 1) : R) =
    HPow.hPow (α := R) (↑n : R) m * HPow.hPow (α := R) (β := ℕ) (↑n : R) 1
succ₃ :
  HPow.hPow (α := R) (↑n : R) m * (↑(HPow.hPow (β := ℕ) n 1) : R) =
    HPow.hPow (α := R) (↑n : R) m * HPow.hPow (α := R) (β := ℕ) (↑n : R) 1
succ₄ :
  HPow.hPow (α := R) (↑n : R) m * (↑n : R) = HPow.hPow (α := R) (↑n : R) m * HPow.hPow (α := R) (β := ℕ) (↑n : R) 1
⊢ (↑(n ^ (m + 1)) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
have succ₅ : HPow.hPow (α := R) (↑n : R) m * (↑n : R) = HPow.hPow (α := R) (↑n : R) m * (↑n : R)
Tactic: rw [npow_add, npow_add, Nat.cast_mul, ih, npow_one, npow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n m : ℕ
⊢ (↑(n ^ m) : R) = HPow.hPow (α := R) (↑n : R) m
have zero : (↑(HPow.hPow (β := ℕ) n 0) : R) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 0
Tactic: induction m with
  | zero => simp only [pow_zero, Nat.cast_one, npow_zero]
  | succ m ih => rw [npow_add, npow_add, Nat.cast_mul, ih, npow_one, npow_one]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n m : ℕ
zero : (↑(HPow.hPow (β := ℕ) n 0) : R) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 0
⊢ (↑(n ^ m) : R) = HPow.hPow (α := R) (↑n : R) m
have succ : ∀ (m : ℕ) (ih : (↑(n ^ m) : R) = HPow.hPow (α := R) (↑n : R) m),
  (↑(n ^ (m + 1)) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
Tactic: induction m with
  | zero => simp only [pow_zero, Nat.cast_one, npow_zero]
  | succ m ih => rw [npow_add, npow_add, Nat.cast_mul, ih, npow_one, npow_one]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n : ℤ
⊢ (↑(HPow.hPow (β := ℕ) n 0) : R) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 0
have rw : (↑1 : R) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 0
Tactic: rw [pow_zero, npow_zero, Int.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n : ℤ
rw : (↑1 : R) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 0
⊢ (↑(HPow.hPow (β := ℕ) n 0) : R) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 0
have rw₁ : Eq.{u_2 + 1} (α := R) (↑1 : R) 1
Tactic: rw [pow_zero, npow_zero, Int.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n : ℤ
rw : (↑1 : R) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 0
rw₁ : Eq.{u_2 + 1} (α := R) (↑1 : R) 1
⊢ (↑(HPow.hPow (β := ℕ) n 0) : R) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 0
have rw₂ : Eq.{u_2 + 1} (α := R) 1 1
Tactic: rw [pow_zero, npow_zero, Int.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n : ℤ
m : ℕ
⊢ (↑(n ^ (m + 1)) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
have rw : (↑(n ^ m * HPow.hPow (β := ℕ) n 1) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
Tactic: rw [npow_add, npow_one, Int.cast_mul, Int.cast_npow R n m, npow_add, npow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n : ℤ
m : ℕ
rw : (↑(n ^ m * HPow.hPow (β := ℕ) n 1) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
⊢ (↑(n ^ (m + 1)) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
have rw₁ : (↑(n ^ m * n) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
Tactic: rw [npow_add, npow_one, Int.cast_mul, Int.cast_npow R n m, npow_add, npow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n : ℤ
m : ℕ
rw : (↑(n ^ m * HPow.hPow (β := ℕ) n 1) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
rw₁ : (↑(n ^ m * n) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
⊢ (↑(n ^ (m + 1)) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
have rw₂ : HMul.hMul (α := R) (↑(n ^ m) : R) (↑n : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
Tactic: rw [npow_add, npow_one, Int.cast_mul, Int.cast_npow R n m, npow_add, npow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n : ℤ
m : ℕ
rw : (↑(n ^ m * HPow.hPow (β := ℕ) n 1) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
rw₁ : (↑(n ^ m * n) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
rw₂ : HMul.hMul (α := R) (↑(n ^ m) : R) (↑n : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
⊢ (↑(n ^ (m + 1)) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
have rw₃ : HPow.hPow (α := R) (↑n : R) m * (↑n : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
Tactic: rw [npow_add, npow_one, Int.cast_mul, Int.cast_npow R n m, npow_add, npow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n : ℤ
m : ℕ
rw : (↑(n ^ m * HPow.hPow (β := ℕ) n 1) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
rw₁ : (↑(n ^ m * n) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
rw₂ : HMul.hMul (α := R) (↑(n ^ m) : R) (↑n : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
rw₃ : HPow.hPow (α := R) (↑n : R) m * (↑n : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
⊢ (↑(n ^ (m + 1)) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
have rw₄ : HPow.hPow (α := R) (↑n : R) m * (↑n : R) = HPow.hPow (α := R) (↑n : R) m * HPow.hPow (α := R) (β := ℕ) (↑n : R) 1
Tactic: rw [npow_add, npow_one, Int.cast_mul, Int.cast_npow R n m, npow_add, npow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.NatPowAssoc (goal)
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n : ℤ
m : ℕ
rw : (↑(n ^ m * HPow.hPow (β := ℕ) n 1) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
rw₁ : (↑(n ^ m * n) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
rw₂ : HMul.hMul (α := R) (↑(n ^ m) : R) (↑n : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
rw₃ : HPow.hPow (α := R) (↑n : R) m * (↑n : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
rw₄ : HPow.hPow (α := R) (↑n : R) m * (↑n : R) = HPow.hPow (α := R) (↑n : R) m * HPow.hPow (α := R) (β := ℕ) (↑n : R) 1
⊢ (↑(n ^ (m + 1)) : R) = HPow.hPow (α := R) (↑n : R) (m + 1)
have rw₅ : HPow.hPow (α := R) (↑n : R) m * (↑n : R) = HPow.hPow (α := R) (↑n : R) m * (↑n : R)
Tactic: rw [npow_add, npow_one, Int.cast_mul, Int.cast_npow R n m, npow_add, npow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Opposite (goal)
Goal:
α : Type u_1
inst : DivInvMonoid α
x : ℕ
x_1 : αᵐᵒᵖ
⊢ unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x.succ : ℤ))) = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
have rw : HPow.hPow (β := ℤ) (unop x_1) (↑x.succ : ℤ) = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
Tactic: rw [unop_op, zpow_natCast, pow_succ', unop_mul, unop_op, zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Opposite (goal)
Goal:
α : Type u_1
inst : DivInvMonoid α
x : ℕ
x_1 : αᵐᵒᵖ
rw : HPow.hPow (β := ℤ) (unop x_1) (↑x.succ : ℤ) = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
⊢ unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x.succ : ℤ))) = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
have rw₁ : unop x_1 ^ x.succ = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
Tactic: rw [unop_op, zpow_natCast, pow_succ', unop_mul, unop_op, zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Opposite (goal)
Goal:
α : Type u_1
inst : DivInvMonoid α
x : ℕ
x_1 : αᵐᵒᵖ
rw : HPow.hPow (β := ℤ) (unop x_1) (↑x.succ : ℤ) = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
rw₁ : unop x_1 ^ x.succ = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
⊢ unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x.succ : ℤ))) = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
have rw₂ : unop x_1 * unop x_1 ^ x = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
Tactic: rw [unop_op, zpow_natCast, pow_succ', unop_mul, unop_op, zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Opposite (goal)
Goal:
α : Type u_1
inst : DivInvMonoid α
x : ℕ
x_1 : αᵐᵒᵖ
rw : HPow.hPow (β := ℤ) (unop x_1) (↑x.succ : ℤ) = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
rw₁ : unop x_1 ^ x.succ = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
rw₂ : unop x_1 * unop x_1 ^ x = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
⊢ unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x.succ : ℤ))) = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
have rw₃ : unop x_1 * unop x_1 ^ x = unop x_1 * unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)))
Tactic: rw [unop_op, zpow_natCast, pow_succ', unop_mul, unop_op, zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Opposite (goal)
Goal:
α : Type u_1
inst : DivInvMonoid α
x : ℕ
x_1 : αᵐᵒᵖ
rw : HPow.hPow (β := ℤ) (unop x_1) (↑x.succ : ℤ) = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
rw₁ : unop x_1 ^ x.succ = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
rw₂ : unop x_1 * unop x_1 ^ x = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
rw₃ : unop x_1 * unop x_1 ^ x = unop x_1 * unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)))
⊢ unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x.succ : ℤ))) = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
have rw₄ : unop x_1 * unop x_1 ^ x = unop x_1 * HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)
Tactic: rw [unop_op, zpow_natCast, pow_succ', unop_mul, unop_op, zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Opposite (goal)
Goal:
α : Type u_1
inst : DivInvMonoid α
x : ℕ
x_1 : αᵐᵒᵖ
rw : HPow.hPow (β := ℤ) (unop x_1) (↑x.succ : ℤ) = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
rw₁ : unop x_1 ^ x.succ = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
rw₂ : unop x_1 * unop x_1 ^ x = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
rw₃ : unop x_1 * unop x_1 ^ x = unop x_1 * unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)))
rw₄ : unop x_1 * unop x_1 ^ x = unop x_1 * HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)
⊢ unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x.succ : ℤ))) = unop (op (HPow.hPow (β := ℤ) (unop x_1) (↑x : ℤ)) * x_1)
have rw₅ : unop x_1 * unop x_1 ^ x = unop x_1 * unop x_1 ^ x
Tactic: rw [unop_op, zpow_natCast, pow_succ', unop_mul, unop_op, zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Group.Opposite (goal)
Goal:
α : Type u_1
inst : Mul α
a x y : αᵐᵒᵖ
| SemiconjBy a x y
have rw : SemiconjBy (unop a) (unop y) (unop x)
Tactic: rw [← op_unop a, ← op_unop x, ← op_unop y, semiconjBy_op]