awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a b x_1 x : G₀
hx : x ≠ 0
y z : G₀
h : x * y = x * z
⊢ y = z
have rw : x⁻¹ * (x * y) = z
Tactic: rw [← inv_mul_cancel_left₀ hx y, h, inv_mul_cancel_left₀ hx z]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a b x_1 x : G₀
hx : x ≠ 0
y z : G₀
h : x * y = x * z
rw : x⁻¹ * (x * y) = z
⊢ y = z
have rw₁ : x⁻¹ * (x * z) = z
Tactic: rw [← inv_mul_cancel_left₀ hx y, h, inv_mul_cancel_left₀ hx z]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a b x_1 x : G₀
hx : x ≠ 0
y z : G₀
h : x * y = x * z
rw : x⁻¹ * (x * y) = z
rw₁ : x⁻¹ * (x * z) = z
⊢ y = z
have rw₂ : z = z
Tactic: rw [← inv_mul_cancel_left₀ hx y, h, inv_mul_cancel_left₀ hx z]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a b x_1 x : G₀
hx : x ≠ 0
y z : G₀
h : y * x = z * x
⊢ y = z
have rw : y * x * x⁻¹ = z
Tactic: rw [← mul_inv_cancel_right₀ hx y, h, mul_inv_cancel_right₀ hx z]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a b x_1 x : G₀
hx : x ≠ 0
y z : G₀
h : y * x = z * x
rw : y * x * x⁻¹ = z
⊢ y = z
have rw₁ : z * x * x⁻¹ = z
Tactic: rw [← mul_inv_cancel_right₀ hx y, h, mul_inv_cancel_right₀ hx z]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a b x_1 x : G₀
hx : x ≠ 0
y z : G₀
h : y * x = z * x
rw : y * x * x⁻¹ = z
rw₁ : z * x * x⁻¹ = z
⊢ y = z
have rw₂ : z = z
Tactic: rw [← mul_inv_cancel_right₀ hx y, h, mul_inv_cancel_right₀ hx z]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
⊢ 0 / a = 0
have rw : 0 * a⁻¹ = 0
Tactic: rw [div_eq_mul_inv, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
rw : 0 * a⁻¹ = 0
⊢ 0 / a = 0
have rw₁ : Eq.{u_2 + 1} (α := G₀) 0 0
Tactic: rw [div_eq_mul_inv, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
⊢ a / 0 = 0
have rw : a * 0⁻¹ = 0
Tactic: rw [div_eq_mul_inv, inv_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
rw : a * 0⁻¹ = 0
⊢ a / 0 = 0
have rw₁ : a * 0 = 0
Tactic: rw [div_eq_mul_inv, inv_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
rw : a * 0⁻¹ = 0
rw₁ : a * 0 = 0
⊢ a / 0 = 0
have rw₂ : Eq.{u_2 + 1} (α := G₀) 0 0
Tactic: rw [div_eq_mul_inv, inv_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
⊢ a * a * a⁻¹ = a
have pos : ∀ (h : a = 0), a * a * a⁻¹ = a
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
pos : ∀ (h : a = 0), a * a * a⁻¹ = a
⊢ a * a * a⁻¹ = a
have neg : ∀ (h : ¬a = 0), a * a * a⁻¹ = a
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : a = 0
⊢ a * a * a⁻¹ = a
have pos : HMul.hMul (α := G₀) 0 0 * 0⁻¹ = 0
Tactic: rw [h, inv_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : a = 0
pos : HMul.hMul (α := G₀) 0 0 * 0⁻¹ = 0
⊢ a * a * a⁻¹ = a
have pos₁ : HMul.hMul (α := G₀) 0 0 * 0 = 0
Tactic: rw [h, inv_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : a = 0
pos : HMul.hMul (α := G₀) 0 0 * 0⁻¹ = 0
pos₁ : HMul.hMul (α := G₀) 0 0 * 0 = 0
⊢ a * a * a⁻¹ = a
have pos₂ : Eq.{u_2 + 1} (α := G₀) 0 0
Tactic: rw [h, inv_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a * a * a⁻¹ = a
have neg : a * (a * a⁻¹) = a
Tactic: rw [mul_assoc, mul_inv_cancel₀ h, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : ¬a = 0
neg : a * (a * a⁻¹) = a
⊢ a * a * a⁻¹ = a
have neg₁ : a * 1 = a
Tactic: rw [mul_assoc, mul_inv_cancel₀ h, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : ¬a = 0
neg : a * (a * a⁻¹) = a
neg₁ : a * 1 = a
⊢ a * a * a⁻¹ = a
have neg₂ : a = a
Tactic: rw [mul_assoc, mul_inv_cancel₀ h, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
⊢ a * a⁻¹ * a = a
have pos : ∀ (h : a = 0), a * a⁻¹ * a = a
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
pos : ∀ (h : a = 0), a * a⁻¹ * a = a
⊢ a * a⁻¹ * a = a
have neg : ∀ (h : ¬a = 0), a * a⁻¹ * a = a
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : a = 0
⊢ a * a⁻¹ * a = a
have pos : HMul.hMul (α := G₀) 0 0⁻¹ * 0 = 0
Tactic: rw [h, inv_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : a = 0
pos : HMul.hMul (α := G₀) 0 0⁻¹ * 0 = 0
⊢ a * a⁻¹ * a = a
have pos₁ : HMul.hMul (α := G₀) 0 0 * 0 = 0
Tactic: rw [h, inv_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : a = 0
pos : HMul.hMul (α := G₀) 0 0⁻¹ * 0 = 0
pos₁ : HMul.hMul (α := G₀) 0 0 * 0 = 0
⊢ a * a⁻¹ * a = a
have pos₂ : Eq.{u_2 + 1} (α := G₀) 0 0
Tactic: rw [h, inv_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a * a⁻¹ * a = a
have neg : 1 * a = a
Tactic: rw [mul_inv_cancel₀ h, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : ¬a = 0
neg : 1 * a = a
⊢ a * a⁻¹ * a = a
have neg₁ : a = a
Tactic: rw [mul_inv_cancel₀ h, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
⊢ a⁻¹ * a * a = a
have pos : ∀ (h : a = 0), a⁻¹ * a * a = a
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
pos : ∀ (h : a = 0), a⁻¹ * a * a = a
⊢ a⁻¹ * a * a = a
have neg : ∀ (h : ¬a = 0), a⁻¹ * a * a = a
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : a = 0
⊢ a⁻¹ * a * a = a
have pos : HMul.hMul (α := G₀) 0⁻¹ 0 * 0 = 0
Tactic: rw [h, inv_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : a = 0
pos : HMul.hMul (α := G₀) 0⁻¹ 0 * 0 = 0
⊢ a⁻¹ * a * a = a
have pos₁ : HMul.hMul (α := G₀) 0 0 * 0 = 0
Tactic: rw [h, inv_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : a = 0
pos : HMul.hMul (α := G₀) 0⁻¹ 0 * 0 = 0
pos₁ : HMul.hMul (α := G₀) 0 0 * 0 = 0
⊢ a⁻¹ * a * a = a
have pos₂ : Eq.{u_2 + 1} (α := G₀) 0 0
Tactic: rw [h, inv_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a⁻¹ * a * a = a
have neg : 1 * a = a
Tactic: rw [inv_mul_cancel₀ h, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : ¬a = 0
neg : 1 * a = a
⊢ a⁻¹ * a * a = a
have neg₁ : a = a
Tactic: rw [inv_mul_cancel₀ h, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
⊢ a * a / a = a
have rw : a * a * a⁻¹ = a
Tactic: rw [div_eq_mul_inv, mul_self_mul_inv a]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
rw : a * a * a⁻¹ = a
⊢ a * a / a = a
have rw₁ : a = a
Tactic: rw [div_eq_mul_inv, mul_self_mul_inv a]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
⊢ a / a * a = a
have rw : a * a⁻¹ * a = a
Tactic: rw [div_eq_mul_inv, mul_inv_mul_cancel a]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
rw : a * a⁻¹ * a = a
⊢ a / a * a = a
have rw₁ : a = a
Tactic: rw [div_eq_mul_inv, mul_inv_mul_cancel a]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
⊢ a⁻¹ = 0 ↔ a = 0
have rw : a = 0⁻¹ ↔ a = 0
Tactic: rw [inv_eq_iff_eq_inv, inv_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
rw : a = 0⁻¹ ↔ a = 0
⊢ a⁻¹ = 0 ↔ a = 0
have rw₁ : a = 0 ↔ a = 0
Tactic: rw [inv_eq_iff_eq_inv, inv_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
⊢ a / (a / a) = a
have rw : a * a / a = a
Tactic: rw [div_div_eq_mul_div]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (hypothesis)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : 1 / a ≠ 0
ha : a = 0
⊢ False
have h₁ : Ne.{u_2 + 1} (α := G₀) 0 0
Tactic: rw [ha, div_zero] at h
Cleared hypotheses: h, ha
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
n : ℕ
h : Ne (α := ℤ) (↑n : ℤ) 0
⊢ HPow.hPow (α := G₀) (β := ℤ) 0 (↑n : ℤ) = 0
have rw : n ≠ 0
Tactic: rw [zpow_natCast, zero_pow]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
n : ℤ
⊢ HPow.hPow (α := G₀) 0 n = if n = 0 then 1 else 0
have pos : ∀ (h : n = 0), HPow.hPow (α := G₀) 0 n = 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
n : ℤ
pos : ∀ (h : n = 0), HPow.hPow (α := G₀) 0 n = 1
⊢ HPow.hPow (α := G₀) 0 n = if n = 0 then 1 else 0
have neg : ∀ (h : ¬n = 0), HPow.hPow (α := G₀) 0 n = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
n : ℤ
h : n = 0
⊢ HPow.hPow (α := G₀) 0 n = 1
have pos : HPow.hPow (α := G₀) (β := ℤ) 0 0 = 1
Tactic: rw [h, zpow_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
n : ℤ
h : n = 0
pos : HPow.hPow (α := G₀) (β := ℤ) 0 0 = 1
⊢ HPow.hPow (α := G₀) 0 n = 1
have pos₁ : Eq.{u_2 + 1} (α := G₀) 1 1
Tactic: rw [h, zpow_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
n : ℤ
h : ¬n = 0
⊢ HPow.hPow (α := G₀) 0 n = 0
have neg : Eq.{u_2 + 1} (α := G₀) 0 0
Tactic: rw [zero_zpow _ h]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
n : ℤ
⊢ HPow.hPow (α := G₀) 0 n = 1 ↔ n = 0
have rw : Eq.{u_2 + 1} (α := G₀) (if n = 0 then 1 else 0) 1 ↔ n = 0
Tactic: rw [zero_zpow_eq, one_ne_zero.ite_eq_left_iff]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Basic (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
n : ℤ
rw : Eq.{u_2 + 1} (α := G₀) (if n = 0 then 1 else 0) 1 ↔ n = 0
⊢ HPow.hPow (α := G₀) 0 n = 1 ↔ n = 0
have rw₁ : n = 0 ↔ n = 0
Tactic: rw [zero_zpow_eq, one_ne_zero.ite_eq_left_iff]
-- 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 ^ (Int.negSucc (n + 1) + 1) = a ^ Int.negSucc (n + 1) * a
have rw : a ^ (-HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1 + 1) = a ^ (-HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) * a
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 : ℕ
rw : a ^ (-HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1 + 1) = a ^ (-HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) * a
⊢ a ^ (Int.negSucc (n + 1) + 1) = a ^ Int.negSucc (n + 1) * a
have rw₁ : a ^ (-HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1 + 1) = (a ^ HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1)⁻¹ * a
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 : ℕ
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
⊢ a ^ (Int.negSucc (n + 1) + 1) = a ^ Int.negSucc (n + 1) * a
have rw₂ : a ^ (HAdd.hAdd (α := ℤ) (-(↑(n + 1) : ℤ)) (-1) + 1) = (a ^ HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1)⁻¹ * a
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 : ℕ
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
⊢ a ^ (Int.negSucc (n + 1) + 1) = a ^ Int.negSucc (n + 1) * a
have rw₃ : HPow.hPow (β := ℤ) a (-(↑(n + 1) : ℤ)) = (a ^ HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1)⁻¹ * a
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 : ℕ
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
⊢ a ^ (Int.negSucc (n + 1) + 1) = a ^ Int.negSucc (n + 1) * a
have rw₄ : (HPow.hPow (β := ℤ) a (↑(n + 1) : ℤ))⁻¹ = (a ^ HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1)⁻¹ * a
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 : ℕ
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
⊢ a ^ (Int.negSucc (n + 1) + 1) = a ^ Int.negSucc (n + 1) * a
have rw₅ : (HPow.hPow (β := ℤ) a (↑(n + 1) : ℤ))⁻¹ = (HPow.hPow (β := ℤ) a (↑(n + 1).succ : ℤ))⁻¹ * a
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 : ℕ
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
⊢ a ^ (Int.negSucc (n + 1) + 1) = a ^ Int.negSucc (n + 1) * a
have rw₆ : (a ^ (n + 1))⁻¹ = (HPow.hPow (β := ℤ) a (↑(n + 1).succ : ℤ))⁻¹ * a
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 : ℕ
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
⊢ a ^ (Int.negSucc (n + 1) + 1) = a ^ Int.negSucc (n + 1) * a
have rw₇ : (a ^ (n + 1))⁻¹ = (a ^ (n + 1).succ)⁻¹ * a
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 : ℕ
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
⊢ a ^ (Int.negSucc (n + 1) + 1) = a ^ Int.negSucc (n + 1) * a
have rw₈ : (a ^ (n + 1))⁻¹ = (a * a ^ (n + 1))⁻¹ * a
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 : ℕ
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
⊢ a ^ (Int.negSucc (n + 1) + 1) = a ^ Int.negSucc (n + 1) * a
have rw₉ : (a ^ (n + 1))⁻¹ = (a ^ (n + 1))⁻¹ * a⁻¹ * a
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 : ℕ
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
⊢ a ^ (Int.negSucc (n + 1) + 1) = a ^ Int.negSucc (n + 1) * a
have rw₁₀ : (a ^ (n + 1))⁻¹ = (a ^ (n + 1))⁻¹ * (a⁻¹ * a)
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 : ℕ
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)
⊢ a ^ (Int.negSucc (n + 1) + 1) = a ^ Int.negSucc (n + 1) * a
have rw₁₁ : (a ^ (n + 1))⁻¹ = (a ^ (n + 1))⁻¹ * 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]