awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
rw : a ^ (-HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1 + 1) = a ^ (-HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) * a
rw₁ : a ^ (-HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1 + 1) = (a ^ HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1)⁻¹ * a
rw₂ : a ^ (HAdd.hAdd (α := ℤ) (-(↑(n + 1) : ℤ)) (-1) + 1) = (a ^ HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1)⁻¹ * a
rw₃ : HPow.hPow (β := ℤ) a (-(↑(n + 1) : ℤ)) = (a ^ HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1)⁻¹ * a
rw₄ : (HPow.hPow (β := ℤ) a (↑(n + 1) : ℤ))⁻¹ = (a ^ HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1)⁻¹ * a
rw₅ : (HPow.hPow (β := ℤ) a (↑(n + 1) : ℤ))⁻¹ = (HPow.hPow (β := ℤ) a (↑(n + 1).succ : ℤ))⁻¹ * a
rw₆ : (a ^ (n + 1))⁻¹ = (HPow.hPow (β := ℤ) a (↑(n + 1).succ : ℤ))⁻¹ * a
rw₇ : (a ^ (n + 1))⁻¹ = (a ^ (n + 1).succ)⁻¹ * a
rw₈ : (a ^ (n + 1))⁻¹ = (a * a ^ (n + 1))⁻¹ * a
rw₉ : (a ^ (n + 1))⁻¹ = (a ^ (n + 1))⁻¹ * a⁻¹ * a
rw₁₀ : (a ^ (n + 1))⁻¹ = (a ^ (n + 1))⁻¹ * (a⁻¹ * a)
rw₁₁ : (a ^ (n + 1))⁻¹ = (a ^ (n + 1))⁻¹ * 1
⊢ a ^ (Int.negSucc (n + 1) + 1) = a ^ Int.negSucc (n + 1) * a
have rw₁₂ : (a ^ (n + 1))⁻¹ = (a ^ (n + 1))⁻¹
Tactic: rw [Int.negSucc_eq, zpow_neg, Int.neg_add, Int.neg_add_cancel_right, zpow_neg,
      ← Int.natCast_succ, zpow_natCast, zpow_natCast, pow_succ' _ (n + 1), mul_inv_rev, mul_assoc,
      inv_mul_cancel₀ ha, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℤ
⊢ a ^ (n - 1) = a ^ (n - 1) * a * a⁻¹
have rw : a ^ (n - 1) = a ^ (n - 1) * (a * a⁻¹)
Tactic: rw [mul_assoc, mul_inv_cancel₀ ha, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℤ
rw : a ^ (n - 1) = a ^ (n - 1) * (a * a⁻¹)
⊢ a ^ (n - 1) = a ^ (n - 1) * a * a⁻¹
have rw₁ : a ^ (n - 1) = a ^ (n - 1) * 1
Tactic: rw [mul_assoc, mul_inv_cancel₀ ha, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℤ
rw : a ^ (n - 1) = a ^ (n - 1) * (a * a⁻¹)
rw₁ : a ^ (n - 1) = a ^ (n - 1) * 1
⊢ a ^ (n - 1) = a ^ (n - 1) * a * a⁻¹
have rw₂ : a ^ (n - 1) = a ^ (n - 1)
Tactic: rw [mul_assoc, mul_inv_cancel₀ ha, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℤ
⊢ a ^ (n - 1) * a * a⁻¹ = a ^ n * a⁻¹
have rw : a ^ (n - 1 + 1) * a⁻¹ = a ^ n * a⁻¹
Tactic: rw [← zpow_add_one₀ ha, Int.sub_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℤ
rw : a ^ (n - 1 + 1) * a⁻¹ = a ^ n * a⁻¹
⊢ a ^ (n - 1) * a * a⁻¹ = a ^ n * a⁻¹
have rw₁ : a ^ n * a⁻¹ = a ^ n * a⁻¹
Tactic: rw [← zpow_add_one₀ ha, Int.sub_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
n : ℕ
ihn : a ^ (m + -(↑n : ℤ)) = a ^ m * HPow.hPow (β := ℤ) a (-(↑n : ℤ))
⊢ a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * a ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
have pred : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * (HPow.hPow (β := ℤ) a (-(↑n : ℤ)) * a⁻¹)
Tactic: rw [zpow_sub_one₀ ha, ← mul_assoc, ← ihn, ← zpow_sub_one₀ ha, Int.add_sub_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
n : ℕ
ihn : a ^ (m + -(↑n : ℤ)) = a ^ m * HPow.hPow (β := ℤ) a (-(↑n : ℤ))
pred : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * (HPow.hPow (β := ℤ) a (-(↑n : ℤ)) * a⁻¹)
⊢ a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * a ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
have pred₁ : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * HPow.hPow (β := ℤ) a (-(↑n : ℤ)) * a⁻¹
Tactic: rw [zpow_sub_one₀ ha, ← mul_assoc, ← ihn, ← zpow_sub_one₀ ha, Int.add_sub_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
n : ℕ
ihn : a ^ (m + -(↑n : ℤ)) = a ^ m * HPow.hPow (β := ℤ) a (-(↑n : ℤ))
pred : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * (HPow.hPow (β := ℤ) a (-(↑n : ℤ)) * a⁻¹)
pred₁ : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * HPow.hPow (β := ℤ) a (-(↑n : ℤ)) * a⁻¹
⊢ a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * a ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
have pred₂ : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ (m + -(↑n : ℤ)) * a⁻¹
Tactic: rw [zpow_sub_one₀ ha, ← mul_assoc, ← ihn, ← zpow_sub_one₀ ha, Int.add_sub_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
n : ℕ
ihn : a ^ (m + -(↑n : ℤ)) = a ^ m * HPow.hPow (β := ℤ) a (-(↑n : ℤ))
pred : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * (HPow.hPow (β := ℤ) a (-(↑n : ℤ)) * a⁻¹)
pred₁ : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * HPow.hPow (β := ℤ) a (-(↑n : ℤ)) * a⁻¹
pred₂ : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ (m + -(↑n : ℤ)) * a⁻¹
⊢ a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * a ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
have pred₃ : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ (m + -(↑n : ℤ) - 1)
Tactic: rw [zpow_sub_one₀ ha, ← mul_assoc, ← ihn, ← zpow_sub_one₀ ha, Int.add_sub_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
n : ℕ
ihn : a ^ (m + -(↑n : ℤ)) = a ^ m * HPow.hPow (β := ℤ) a (-(↑n : ℤ))
pred : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * (HPow.hPow (β := ℤ) a (-(↑n : ℤ)) * a⁻¹)
pred₁ : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * HPow.hPow (β := ℤ) a (-(↑n : ℤ)) * a⁻¹
pred₂ : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ (m + -(↑n : ℤ)) * a⁻¹
pred₃ : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ (m + -(↑n : ℤ) - 1)
⊢ a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * a ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
have pred₄ : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: rw [zpow_sub_one₀ ha, ← mul_assoc, ← ihn, ← zpow_sub_one₀ ha, Int.add_sub_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℤ
⊢ a ^ (m + n) = a ^ m * a ^ n
have zero : a ^ (m + 0) = a ^ m * HPow.hPow (β := ℤ) a 0
Tactic: induction n with
  | zero => simp
  | succ n ihn => simp only [← Int.add_assoc, zpow_add_one₀ ha, ihn, mul_assoc]
  | pred n ihn => rw [zpow_sub_one₀ ha, ← mul_assoc, ← ihn, ← zpow_sub_one₀ ha, Int.add_sub_assoc]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℤ
zero : a ^ (m + 0) = a ^ m * HPow.hPow (β := ℤ) a 0
⊢ a ^ (m + n) = a ^ m * a ^ n
have succ : ∀ (n : ℕ) (ihn : a ^ (m + (↑n : ℤ)) = a ^ m * HPow.hPow (β := ℤ) a (↑n : ℤ)),
  a ^ (m + HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = a ^ m * a ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
Tactic: induction n with
  | zero => simp
  | succ n ihn => simp only [← Int.add_assoc, zpow_add_one₀ ha, ihn, mul_assoc]
  | pred n ihn => rw [zpow_sub_one₀ ha, ← mul_assoc, ← ihn, ← zpow_sub_one₀ ha, Int.add_sub_assoc]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℤ
zero : a ^ (m + 0) = a ^ m * HPow.hPow (β := ℤ) a 0
succ :
  ∀ (n : ℕ) (ihn : a ^ (m + (↑n : ℤ)) = a ^ m * HPow.hPow (β := ℤ) a (↑n : ℤ)),
    a ^ (m + HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = a ^ m * a ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
⊢ a ^ (m + n) = a ^ m * a ^ n
have pred : ∀ (n : ℕ) (ihn : a ^ (m + -(↑n : ℤ)) = a ^ m * HPow.hPow (β := ℤ) a (-(↑n : ℤ))),
  a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * a ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
Tactic: induction n with
  | zero => simp
  | succ n ihn => simp only [← Int.add_assoc, zpow_add_one₀ ha, ihn, mul_assoc]
  | pred n ihn => rw [zpow_sub_one₀ ha, ← mul_assoc, ← ihn, ← zpow_sub_one₀ ha, Int.add_sub_assoc]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
⊢ a ^ (m + n) = a ^ m * a ^ n
have pos : ∀ (hm : m = 0), a ^ (m + n) = a ^ m * a ^ n
Tactic: by_cases hm : m = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
pos : ∀ (hm : m = 0), a ^ (m + n) = a ^ m * a ^ n
⊢ a ^ (m + n) = a ^ m * a ^ n
have neg : ∀ (hm : ¬m = 0), a ^ (m + n) = a ^ m * a ^ n
Tactic: by_cases hm : m = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
⊢ a ^ (m + n) = a ^ m * a ^ n
have pos : ∀ (hn : n = 0), a ^ (m + n) = a ^ m * a ^ n
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
pos : ∀ (hn : n = 0), a ^ (m + n) = a ^ m * a ^ n
⊢ a ^ (m + n) = a ^ m * a ^ n
have neg : ∀ (hn : ¬n = 0), a ^ (m + n) = a ^ m * a ^ n
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
hn : ¬n = 0
⊢ a ^ (m + n) = a ^ m * a ^ n
have pos : ∀ (ha : a = 0), a ^ (m + n) = a ^ m * a ^ n
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
hn : ¬n = 0
pos : ∀ (ha : a = 0), a ^ (m + n) = a ^ m * a ^ n
⊢ a ^ (m + n) = a ^ m * a ^ n
have neg : ∀ (ha : ¬a = 0), a ^ (m + n) = a ^ m * a ^ n
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
hn : ¬n = 0
ha : a = 0
⊢ a ^ (m + n) = a ^ m * a ^ n
have pos : ∀ (h : Ne.{u_2 + 1} (α := G₀) 0 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0),
  HPow.hPow (α := G₀) 0 (m + n) = HPow.hPow (α := G₀) 0 m * HPow.hPow (α := G₀) 0 n
Tactic: subst a
Cleared hypotheses: a, h, ha
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (hypothesis)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
m n : ℤ
hm : ¬m = 0
hn : ¬n = 0
h : Ne.{u_2 + 1} (α := G₀) 0 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
⊢ HPow.hPow (α := G₀) 0 (m + n) = HPow.hPow (α := G₀) 0 m * HPow.hPow (α := G₀) 0 n
have h₁ : ¬m + n = 0
Tactic: simp only [false_or, not_true, Ne, hm, hn, false_and, or_false] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
m n : ℤ
hm : ¬m = 0
hn : ¬n = 0
h : ¬m + n = 0
⊢ HPow.hPow (α := G₀) 0 (m + n) = HPow.hPow (α := G₀) 0 m * HPow.hPow (α := G₀) 0 n
have pos : 0 = HPow.hPow (α := G₀) 0 m * HPow.hPow (α := G₀) 0 n
Tactic: rw [zero_zpow _ h, zero_zpow _ hm, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
m n : ℤ
hm : ¬m = 0
hn : ¬n = 0
h : ¬m + n = 0
pos : 0 = HPow.hPow (α := G₀) 0 m * HPow.hPow (α := G₀) 0 n
⊢ HPow.hPow (α := G₀) 0 (m + n) = HPow.hPow (α := G₀) 0 m * HPow.hPow (α := G₀) 0 n
have pos₁ : 0 = 0 * HPow.hPow (α := G₀) 0 n
Tactic: rw [zero_zpow _ h, zero_zpow _ hm, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
m n : ℤ
hm : ¬m = 0
hn : ¬n = 0
h : ¬m + n = 0
pos : 0 = HPow.hPow (α := G₀) 0 m * HPow.hPow (α := G₀) 0 n
pos₁ : 0 = 0 * HPow.hPow (α := G₀) 0 n
⊢ HPow.hPow (α := G₀) 0 (m + n) = HPow.hPow (α := G₀) 0 m * HPow.hPow (α := G₀) 0 n
have pos₂ : Eq.{u_2 + 1} (α := G₀) 0 0
Tactic: rw [zero_zpow _ h, zero_zpow _ hm, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : a ≠ 0
i : ℤ
⊢ a ^ (1 + i) = a * a ^ i
have rw : HPow.hPow (β := ℤ) a 1 * a ^ i = a * a ^ i
Tactic: rw [zpow_add₀ h, zpow_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : a ≠ 0
i : ℤ
rw : HPow.hPow (β := ℤ) a 1 * a ^ i = a * a ^ i
⊢ a ^ (1 + i) = a * a ^ i
have rw₁ : a * a ^ i = a * a ^ i
Tactic: rw [zpow_add₀ h, zpow_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : CommGroupWithZero G₀
a b c : G₀
⊢ a / c * b = a * b / c
have simp_rw : a * c⁻¹ * b = a * b * c⁻¹
Tactic: simp_rw [div_eq_mul_inv, mul_assoc, mul_comm c⁻¹]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : CommGroupWithZero G₀
a b c : G₀
simp_rw : a * c⁻¹ * b = a * b * c⁻¹
⊢ a / c * b = a * b / c
have simp_rw₁ : a * (c⁻¹ * b) = a * (b * c⁻¹)
Tactic: simp_rw [div_eq_mul_inv, mul_assoc, mul_comm c⁻¹]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : CommGroupWithZero G₀
a b : G₀
⊢ HPow.hPow (β := ℕ) a 2 * b / a = a * b
have inl : HPow.hPow (α := G₀) (β := ℕ) 0 2 * b / 0 = 0 * b
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : CommGroupWithZero G₀
a b : G₀
inl : HPow.hPow (α := G₀) (β := ℕ) 0 2 * b / 0 = 0 * b
⊢ HPow.hPow (β := ℕ) a 2 * b / a = a * b
have inr : ∀ (ha : a ≠ 0), HPow.hPow (β := ℕ) a 2 * b / a = a * b
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : CommGroupWithZero G₀
a b : G₀
ha : a ≠ 0
⊢ HPow.hPow (β := ℕ) a 2 * b / a = a * b
have inr : a * a * b / a = a * b
Tactic: rw [sq, mul_assoc, mul_div_cancel_left₀ _ ha]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : CommGroupWithZero G₀
a b : G₀
ha : a ≠ 0
inr : a * a * b / a = a * b
⊢ HPow.hPow (β := ℕ) a 2 * b / a = a * b
have inr₁ : a * (a * b) / a = a * b
Tactic: rw [sq, mul_assoc, mul_div_cancel_left₀ _ ha]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : CommGroupWithZero G₀
a b : G₀
ha : a ≠ 0
inr : a * a * b / a = a * b
inr₁ : a * (a * b) / a = a * b
⊢ HPow.hPow (β := ℕ) a 2 * b / a = a * b
have inr₂ : a * b = a * b
Tactic: rw [sq, mul_assoc, mul_div_cancel_left₀ _ ha]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀
h : Commute a b
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
have pos : ∀ (hab : IsUnit (a * b)), (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
Tactic: by_cases hab : IsUnit (a * b)
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀
h : Commute a b
pos : ∀ (hab : IsUnit (a * b)), (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
have neg : ∀ (hab : ¬IsUnit (a * b)), (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
Tactic: by_cases hab : IsUnit (a * b)
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : IsUnit (a * b)
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
have pos : ∀ (a b : M₀ˣ) (h : Commute (↑a : M₀) (↑b : M₀)) (hab : IsUnit ((↑a : M₀) * (↑b : M₀))),
  ((↑a : M₀) * (↑b : M₀))⁻¹ʳ = (↑b : M₀)⁻¹ʳ * (↑a : M₀)⁻¹ʳ
Tactic: obtain ⟨⟨a, rfl⟩, b, rfl⟩ := h.isUnit_mul_iff.mp hab
Cleared hypotheses: a, b, h, hab
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀ˣ
h : Commute (↑a : M₀) (↑b : M₀)
hab : IsUnit ((↑a : M₀) * (↑b : M₀))
⊢ ((↑a : M₀) * (↑b : M₀))⁻¹ʳ = (↑b : M₀)⁻¹ʳ * (↑a : M₀)⁻¹ʳ
have pos : (↑(a * b) : M₀)⁻¹ʳ = (↑b : M₀)⁻¹ʳ * (↑a : M₀)⁻¹ʳ
Tactic: rw [← Units.val_mul, inverse_unit, inverse_unit, inverse_unit, ← Units.val_mul, mul_inv_rev]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀ˣ
h : Commute (↑a : M₀) (↑b : M₀)
hab : IsUnit ((↑a : M₀) * (↑b : M₀))
pos : (↑(a * b) : M₀)⁻¹ʳ = (↑b : M₀)⁻¹ʳ * (↑a : M₀)⁻¹ʳ
⊢ ((↑a : M₀) * (↑b : M₀))⁻¹ʳ = (↑b : M₀)⁻¹ʳ * (↑a : M₀)⁻¹ʳ
have pos₁ : (↑(a * b)⁻¹ : M₀) = (↑b : M₀)⁻¹ʳ * (↑a : M₀)⁻¹ʳ
Tactic: rw [← Units.val_mul, inverse_unit, inverse_unit, inverse_unit, ← Units.val_mul, mul_inv_rev]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀ˣ
h : Commute (↑a : M₀) (↑b : M₀)
hab : IsUnit ((↑a : M₀) * (↑b : M₀))
pos : (↑(a * b) : M₀)⁻¹ʳ = (↑b : M₀)⁻¹ʳ * (↑a : M₀)⁻¹ʳ
pos₁ : (↑(a * b)⁻¹ : M₀) = (↑b : M₀)⁻¹ʳ * (↑a : M₀)⁻¹ʳ
⊢ ((↑a : M₀) * (↑b : M₀))⁻¹ʳ = (↑b : M₀)⁻¹ʳ * (↑a : M₀)⁻¹ʳ
have pos₂ : (↑(a * b)⁻¹ : M₀) = (↑b⁻¹ : M₀) * (↑a : M₀)⁻¹ʳ
Tactic: rw [← Units.val_mul, inverse_unit, inverse_unit, inverse_unit, ← Units.val_mul, mul_inv_rev]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀ˣ
h : Commute (↑a : M₀) (↑b : M₀)
hab : IsUnit ((↑a : M₀) * (↑b : M₀))
pos : (↑(a * b) : M₀)⁻¹ʳ = (↑b : M₀)⁻¹ʳ * (↑a : M₀)⁻¹ʳ
pos₁ : (↑(a * b)⁻¹ : M₀) = (↑b : M₀)⁻¹ʳ * (↑a : M₀)⁻¹ʳ
pos₂ : (↑(a * b)⁻¹ : M₀) = (↑b⁻¹ : M₀) * (↑a : M₀)⁻¹ʳ
⊢ ((↑a : M₀) * (↑b : M₀))⁻¹ʳ = (↑b : M₀)⁻¹ʳ * (↑a : M₀)⁻¹ʳ
have pos₃ : (↑(a * b)⁻¹ : M₀) = (↑b⁻¹ : M₀) * (↑a⁻¹ : M₀)
Tactic: rw [← Units.val_mul, inverse_unit, inverse_unit, inverse_unit, ← Units.val_mul, mul_inv_rev]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀ˣ
h : Commute (↑a : M₀) (↑b : M₀)
hab : IsUnit ((↑a : M₀) * (↑b : M₀))
pos : (↑(a * b) : M₀)⁻¹ʳ = (↑b : M₀)⁻¹ʳ * (↑a : M₀)⁻¹ʳ
pos₁ : (↑(a * b)⁻¹ : M₀) = (↑b : M₀)⁻¹ʳ * (↑a : M₀)⁻¹ʳ
pos₂ : (↑(a * b)⁻¹ : M₀) = (↑b⁻¹ : M₀) * (↑a : M₀)⁻¹ʳ
pos₃ : (↑(a * b)⁻¹ : M₀) = (↑b⁻¹ : M₀) * (↑a⁻¹ : M₀)
⊢ ((↑a : M₀) * (↑b : M₀))⁻¹ʳ = (↑b : M₀)⁻¹ʳ * (↑a : M₀)⁻¹ʳ
have pos₄ : (↑(a * b)⁻¹ : M₀) = (↑(b⁻¹ * a⁻¹) : M₀)
Tactic: rw [← Units.val_mul, inverse_unit, inverse_unit, inverse_unit, ← Units.val_mul, mul_inv_rev]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀ˣ
h : Commute (↑a : M₀) (↑b : M₀)
hab : IsUnit ((↑a : M₀) * (↑b : M₀))
pos : (↑(a * b) : M₀)⁻¹ʳ = (↑b : M₀)⁻¹ʳ * (↑a : M₀)⁻¹ʳ
pos₁ : (↑(a * b)⁻¹ : M₀) = (↑b : M₀)⁻¹ʳ * (↑a : M₀)⁻¹ʳ
pos₂ : (↑(a * b)⁻¹ : M₀) = (↑b⁻¹ : M₀) * (↑a : M₀)⁻¹ʳ
pos₃ : (↑(a * b)⁻¹ : M₀) = (↑b⁻¹ : M₀) * (↑a⁻¹ : M₀)
pos₄ : (↑(a * b)⁻¹ : M₀) = (↑(b⁻¹ * a⁻¹) : M₀)
⊢ ((↑a : M₀) * (↑b : M₀))⁻¹ʳ = (↑b : M₀)⁻¹ʳ * (↑a : M₀)⁻¹ʳ
have pos₅ : (↑(b⁻¹ * a⁻¹) : M₀) = (↑(b⁻¹ * a⁻¹) : M₀)
Tactic: rw [← Units.val_mul, inverse_unit, inverse_unit, inverse_unit, ← Units.val_mul, mul_inv_rev]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
have neg : ∀ (ha : ¬IsUnit a), (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
Tactic: obtain ha | hb := not_and_or.mp (mt h.isUnit_mul_iff.mpr hab)
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
neg : ∀ (ha : ¬IsUnit a), (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
have neg₁ : ∀ (hb : ¬IsUnit b), (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
Tactic: obtain ha | hb := not_and_or.mp (mt h.isUnit_mul_iff.mpr hab)
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
ha : ¬IsUnit a
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
have neg : 0 = b⁻¹ʳ * a⁻¹ʳ
Tactic: rw [inverse_non_unit _ hab, inverse_non_unit _ ha, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
ha : ¬IsUnit a
neg : 0 = b⁻¹ʳ * a⁻¹ʳ
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
have neg₁ : 0 = b⁻¹ʳ * 0
Tactic: rw [inverse_non_unit _ hab, inverse_non_unit _ ha, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
ha : ¬IsUnit a
neg : 0 = b⁻¹ʳ * a⁻¹ʳ
neg₁ : 0 = b⁻¹ʳ * 0
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
have neg₂ : Eq.{u_1 + 1} (α := M₀) 0 0
Tactic: rw [inverse_non_unit _ hab, inverse_non_unit _ ha, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
hb : ¬IsUnit b
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
have neg : 0 = b⁻¹ʳ * a⁻¹ʳ
Tactic: rw [inverse_non_unit _ hab, inverse_non_unit _ hb, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
hb : ¬IsUnit b
neg : 0 = b⁻¹ʳ * a⁻¹ʳ
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
have neg₁ : 0 = 0 * a⁻¹ʳ
Tactic: rw [inverse_non_unit _ hab, inverse_non_unit _ hb, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
hb : ¬IsUnit b
neg : 0 = b⁻¹ʳ * a⁻¹ʳ
neg₁ : 0 = 0 * a⁻¹ʳ
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
have neg₂ : Eq.{u_1 + 1} (α := M₀) 0 0
Tactic: rw [inverse_non_unit _ hab, inverse_non_unit _ hb, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
r : M₀
⊢ HPow.hPow (β := ℕ) r⁻¹ʳ 0 = (HPow.hPow (β := ℕ) r 0)⁻¹ʳ
have rw : 1 = (HPow.hPow (β := ℕ) r 0)⁻¹ʳ
Tactic: rw [pow_zero, pow_zero, Ring.inverse_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
r : M₀
rw : 1 = (HPow.hPow (β := ℕ) r 0)⁻¹ʳ
⊢ HPow.hPow (β := ℕ) r⁻¹ʳ 0 = (HPow.hPow (β := ℕ) r 0)⁻¹ʳ
have rw₁ : Eq.{u_1 + 1} (α := M₀) 1 1⁻¹ʳ
Tactic: rw [pow_zero, pow_zero, Ring.inverse_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
r : M₀
rw : 1 = (HPow.hPow (β := ℕ) r 0)⁻¹ʳ
rw₁ : Eq.{u_1 + 1} (α := M₀) 1 1⁻¹ʳ
⊢ HPow.hPow (β := ℕ) r⁻¹ʳ 0 = (HPow.hPow (β := ℕ) r 0)⁻¹ʳ
have rw₂ : Eq.{u_1 + 1} (α := M₀) 1 1
Tactic: rw [pow_zero, pow_zero, Ring.inverse_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
r : M₀
n : ℕ
⊢ r⁻¹ʳ ^ (n + 1) = (r ^ (n + 1))⁻¹ʳ
have rw : r⁻¹ʳ * r⁻¹ʳ ^ n = (r ^ (n + 1))⁻¹ʳ
Tactic: rw [pow_succ', pow_succ, Ring.mul_inverse_rev' ((Commute.refl r).pow_left n),
      Ring.inverse_pow r n]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
r : M₀
n : ℕ
rw : r⁻¹ʳ * r⁻¹ʳ ^ n = (r ^ (n + 1))⁻¹ʳ
⊢ r⁻¹ʳ ^ (n + 1) = (r ^ (n + 1))⁻¹ʳ
have rw₁ : r⁻¹ʳ * r⁻¹ʳ ^ n = (r ^ n * r)⁻¹ʳ
Tactic: rw [pow_succ', pow_succ, Ring.mul_inverse_rev' ((Commute.refl r).pow_left n),
      Ring.inverse_pow r n]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
r : M₀
n : ℕ
rw : r⁻¹ʳ * r⁻¹ʳ ^ n = (r ^ (n + 1))⁻¹ʳ
rw₁ : r⁻¹ʳ * r⁻¹ʳ ^ n = (r ^ n * r)⁻¹ʳ
⊢ r⁻¹ʳ ^ (n + 1) = (r ^ (n + 1))⁻¹ʳ
have rw₂ : r⁻¹ʳ * r⁻¹ʳ ^ n = r⁻¹ʳ * (r ^ n)⁻¹ʳ
Tactic: rw [pow_succ', pow_succ, Ring.mul_inverse_rev' ((Commute.refl r).pow_left n),
      Ring.inverse_pow r n]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
r : M₀
n : ℕ
rw : r⁻¹ʳ * r⁻¹ʳ ^ n = (r ^ (n + 1))⁻¹ʳ
rw₁ : r⁻¹ʳ * r⁻¹ʳ ^ n = (r ^ n * r)⁻¹ʳ
rw₂ : r⁻¹ʳ * r⁻¹ʳ ^ n = r⁻¹ʳ * (r ^ n)⁻¹ʳ
⊢ r⁻¹ʳ ^ (n + 1) = (r ^ (n + 1))⁻¹ʳ
have rw₃ : r⁻¹ʳ * (r ^ n)⁻¹ʳ = r⁻¹ʳ * (r ^ n)⁻¹ʳ
Tactic: rw [pow_succ', pow_succ, Ring.mul_inverse_rev' ((Commute.refl r).pow_left n),
      Ring.inverse_pow r n]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b c : M₀
ha : IsUnit a
k : ℕ
⊢ a⁻¹ʳ ^ k * b = c ↔ b = a ^ k * c
have rw : (a ^ k)⁻¹ʳ * b = c ↔ b = a ^ k * c
Tactic: rw [Ring.inverse_pow, Ring.inverse_mul_eq_iff_eq_mul _ _ _ (IsUnit.pow _ ha)]