awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
a b : M₀
inst : MulZeroOneClass M₀
inst_1 : IsLeftCancelMulZero M₀
ha : a ≠ 0
rw : a * b = a ↔ b = 1
rw₁ rw₂ : b = 1 ↔ b = 1
⊢ a = a * b ↔ b = 1

Tactic:
rw [eq_comm, mul_eq_left₀ ha]

Premises used: mul_eq_left₀, eq_comm
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
a b : M₀
inst : MulZeroOneClass M₀
inst_1 : IsRightCancelMulZero M₀
hb : b ≠ 0
rw : a * b = b ↔ a = 1
rw₁ rw₂ : a = 1 ↔ a = 1
⊢ b = a * b ↔ a = 1

Tactic:
rw [eq_comm, mul_eq_right₀ hb]

Premises used: mul_eq_right₀, eq_comm
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
a b : M₀
inst : MulZeroOneClass M₀
inst_1 : IsLeftCancelMulZero M₀
h₁ : b ≠ 1
h₂ : a * b = a
⊢ a = 0

Tactic:
Classical.byContradiction fun ha => h₁ <| mul_left_cancel₀ ha <| h₂.symm ▸ (mul_one a).symm

Premises used: Classical.byContradiction, mul_left_cancel₀
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
a b : M₀
inst : MulZeroOneClass M₀
inst_1 : IsRightCancelMulZero M₀
h₁ : b ≠ 1
h₂ : b * a = a
⊢ a = 0

Tactic:
Classical.byContradiction fun ha => h₁ <| mul_right_cancel₀ ha <| h₂.symm ▸ (one_mul a).symm

Premises used: Classical.byContradiction, mul_right_cancel₀
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
x : G₀
h : x ≠ 0
y y' : G₀
w : Eq.{u_2 + 1} (α := G₀) ((fun (y : G₀) ↦ x * y) y) ((fun (y : G₀) ↦ x * y) y')
⊢ y = y'

Tactic:
simpa only [← mul_assoc, inv_mul_cancel₀ h, one_mul] using congr_arg (fun y => x⁻¹ * y) w

Premises used: HMul.hMul, mul_assoc, congr_arg, Inv.inv, inv_mul_cancel₀, one_mul
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
x : G₀
h : x ≠ 0
y y' : G₀
w : Eq.{u_2 + 1} (α := G₀) ((fun (y : G₀) ↦ y * x) y) ((fun (y : G₀) ↦ y * x) y')
⊢ y = y'

Tactic:
simpa only [mul_assoc, mul_inv_cancel₀ h, mul_one] using congr_arg (fun y => y * x⁻¹) w

Premises used: HMul.hMul, mul_inv_cancel₀, mul_assoc, congr_arg, Inv.inv, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
b : G₀
h : b ≠ 0
a : G₀
⊢ a * (b⁻¹ * b) = a

Tactic:
simp [h]
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : a ≠ 0
b : G₀
⊢ a⁻¹ * a * b = b

Tactic:
simp [h]
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a b : G₀
h : a * b = 1
rw : a⁻¹ = a⁻¹ * (a * b)
rw₁ : a⁻¹ = a⁻¹ * 1
rw₂ rw₃ : a⁻¹ = a⁻¹
⊢ a⁻¹ = b

Tactic:
rw [← inv_mul_cancel_left₀ (left_ne_zero_of_mul_eq_one h) b, h, mul_one]

Premises used: inv_mul_cancel_left₀, left_ne_zero_of_mul_eq_one, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a_1 b x a : G₀
pos : ∀ (h : a = 0), a⁻¹⁻¹ = a
neg : ∀ (h : ¬a = 0), a⁻¹⁻¹ = a
⊢ a⁻¹⁻¹ = a

Tactic:
by_cases h : a = 0
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a_1 b x a : G₀
h : a = 0
⊢ a⁻¹⁻¹ = a

Tactic:
simp [h]
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a_1 b x a : G₀
h : ¬a = 0
⊢ a⁻¹⁻¹ = a

Tactic:
left_inv_eq_right_inv (inv_mul_cancel₀ <| inv_ne_zero h) (inv_mul_cancel₀ h)

Premises used: left_inv_eq_right_inv, inv_ne_zero, inv_mul_cancel₀
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a_1 b x a : G₀
h : ¬a = 0
⊢ a⁻¹⁻¹ = a

Tactic:
exact left_inv_eq_right_inv (inv_mul_cancel₀ <| inv_ne_zero h) (inv_mul_cancel₀ h)

Premises used: left_inv_eq_right_inv, inv_ne_zero, inv_mul_cancel₀
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a_1 b_1 x a b : G₀
pos : ∀ (ha : a = 0), (a * b)⁻¹ = b⁻¹ * a⁻¹
neg : ∀ (ha : ¬a = 0), (a * b)⁻¹ = b⁻¹ * a⁻¹
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a_1 b_1 x a b : G₀
ha : a = 0
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a_1 b_1 x a b : G₀
ha : ¬a = 0
pos : ∀ (hb : b = 0), (a * b)⁻¹ = b⁻¹ * a⁻¹
neg : ∀ (hb : ¬b = 0), (a * b)⁻¹ = b⁻¹ * a⁻¹
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹

Tactic:
by_cases hb : b = 0
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a_1 b_1 x a b : G₀
ha : ¬a = 0
hb : b = 0
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹

Tactic:
simp [hb]
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a_1 b_1 x a b : G₀
ha : ¬a = 0
hb : ¬b = 0
neg : a * b * (b⁻¹ * a⁻¹) = 1
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹

Tactic:
apply inv_eq_of_mul

Premises used: _private.0.inv_eq_of_mul
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a_1 b_1 x a b : G₀
ha : ¬a = 0
hb : ¬b = 0
⊢ a * b * (b⁻¹ * a⁻¹) = 1

Tactic:
simp [mul_assoc, ha, hb]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a b x x_1 x_2 : G₀
⊢ x_1 * x_2 = 1 → x_1⁻¹ = x_2

Tactic:
inv_eq_of_mul

Premises used: _private.0.inv_eq_of_mul
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
M₀ : Type u_1
G₀ : Type u_2
inst : GroupWithZero G₀
a b x x_1 x_2 : G₀
⊢ x_1 * x_2 = 1 → x_1⁻¹ = x_2

Tactic:
exact inv_eq_of_mul

Premises used: _private.0.inv_eq_of_mul
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
rw₂ rw₃ : z = z
⊢ y = z

Tactic:
rw [← inv_mul_cancel_left₀ hx y, h, inv_mul_cancel_left₀ hx z]

Premises used: inv_mul_cancel_left₀
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
rw₂ rw₃ : z = z
⊢ y = z

Tactic:
rw [← mul_inv_cancel_right₀ hx y, h, mul_inv_cancel_right₀ hx z]

Premises used: mul_inv_cancel_right₀
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
rw : 0 * a⁻¹ = 0
rw₁ rw₂ : Eq.{u_2 + 1} (α := G₀) 0 0
⊢ 0 / a = 0

Tactic:
rw [div_eq_mul_inv, zero_mul]

Premises used: MulZeroClass.zero_mul, div_eq_mul_inv
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
rw : a * 0⁻¹ = 0
rw₁ : a * 0 = 0
rw₂ rw₃ : Eq.{u_2 + 1} (α := G₀) 0 0
⊢ a / 0 = 0

Tactic:
rw [div_eq_mul_inv, inv_zero, mul_zero]

Premises used: inv_zero, div_eq_mul_inv, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
pos : ∀ (h : a = 0), a * a * a⁻¹ = a
neg : ∀ (h : ¬a = 0), a * a * a⁻¹ = a
⊢ a * a * a⁻¹ = a

Tactic:
by_cases h : a = 0
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
pos₂ pos₃ : Eq.{u_2 + 1} (α := G₀) 0 0
⊢ a * a * a⁻¹ = a

Tactic:
rw [h, inv_zero, mul_zero]

Premises used: inv_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : ¬a = 0
neg : a * (a * a⁻¹) = a
neg₁ : a * 1 = a
neg₂ neg₃ : a = a
⊢ a * a * a⁻¹ = a

Tactic:
rw [mul_assoc, mul_inv_cancel₀ h, mul_one]

Premises used: mul_inv_cancel₀, mul_assoc, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
pos : ∀ (h : a = 0), a * a⁻¹ * a = a
neg : ∀ (h : ¬a = 0), a * a⁻¹ * a = a
⊢ a * a⁻¹ * a = a

Tactic:
by_cases h : a = 0
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
pos₂ pos₃ : Eq.{u_2 + 1} (α := G₀) 0 0
⊢ a * a⁻¹ * a = a

Tactic:
rw [h, inv_zero, mul_zero]

Premises used: inv_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : ¬a = 0
neg : 1 * a = a
neg₁ neg₂ : a = a
⊢ a * a⁻¹ * a = a

Tactic:
rw [mul_inv_cancel₀ h, one_mul]

Premises used: mul_inv_cancel₀, one_mul
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
pos : ∀ (h : a = 0), a⁻¹ * a * a = a
neg : ∀ (h : ¬a = 0), a⁻¹ * a * a = a
⊢ a⁻¹ * a * a = a

Tactic:
by_cases h : a = 0
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
pos₂ pos₃ : Eq.{u_2 + 1} (α := G₀) 0 0
⊢ a⁻¹ * a * a = a

Tactic:
rw [h, inv_zero, mul_zero]

Premises used: inv_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : ¬a = 0
neg : 1 * a = a
neg₁ neg₂ : a = a
⊢ a⁻¹ * a * a = a

Tactic:
rw [inv_mul_cancel₀ h, one_mul]

Premises used: inv_mul_cancel₀, one_mul
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
rw : a * a * a⁻¹ = a
rw₁ rw₂ : a = a
⊢ a * a / a = a

Tactic:
rw [div_eq_mul_inv, mul_self_mul_inv a]

Premises used: div_eq_mul_inv, mul_self_mul_inv
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
rw : a * a⁻¹ * a = a
rw₁ rw₂ : a = a
⊢ a / a * a = a

Tactic:
rw [div_eq_mul_inv, mul_inv_mul_cancel a]

Premises used: div_eq_mul_inv, mul_inv_mul_cancel
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
⊢ a / (a * a) = a⁻¹⁻¹ * a⁻¹ * a⁻¹

Tactic:
simp [mul_inv_rev]

Premises used: mul_inv_rev
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : a ≠ 0
⊢ 1 / a ≠ 0

Tactic:
simpa only [one_div] using inv_ne_zero h

Premises used: one_div, inv_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
rw : a = 0⁻¹ ↔ a = 0
rw₁ rw₂ : a = 0 ↔ a = 0
⊢ a⁻¹ = 0 ↔ a = 0

Tactic:
rw [inv_eq_iff_eq_inv, inv_zero]

Premises used: inv_zero, inv_eq_iff_eq_inv
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
⊢ 0 = a⁻¹ ↔ 0 = a

Tactic:
eq_comm.trans <| inv_eq_zero.trans eq_comm

Premises used: inv_eq_zero, eq_comm, Iff.trans
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
rw : a * a / a = a
⊢ a / (a / a) = a

Tactic:
rw [div_div_eq_mul_div]

Premises used: div_div_eq_mul_div
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
⊢ a * a / a = a

Tactic:
mul_self_div_self a

Premises used: mul_self_div_self
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
⊢ a * a / a = a

Tactic:
exact mul_self_div_self a

Premises used: mul_self_div_self
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : 1 / a ≠ 0
ha : a = 0
⊢ Ne.{u_2 + 1} (α := G₀) 0 0

Tactic:
rw [ha, div_zero] at h

Premises used: div_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : 1 / a ≠ 0
ha : a = 0
h₁ : Ne.{u_2 + 1} (α := G₀) 0 0
⊢ a = 0

Tactic:
rw [ha, div_zero] at h

Premises used: div_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : Ne.{u_2 + 1} (α := G₀) 0 0
ha : a = 0
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : 1 / a = 0
⊢ a = 0

Tactic:
Classical.byCases (fun ha => ha) fun ha => ((one_div_ne_zero ha) h).elim

Premises used: False.elim, Classical.byCases, one_div_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : a ≠ 0
g : G₀
⊢ (fun (g : G₀) ↦ a * g) (a⁻¹ * g) = g

Tactic:
simp [← mul_assoc, mul_inv_cancel₀ h]

Premises used: mul_inv_cancel₀, mul_assoc
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : a ≠ 0
g : G₀
⊢ (fun (g : G₀) ↦ g * a) (g * a⁻¹) = g

Tactic:
simp [mul_assoc, inv_mul_cancel₀ h]

Premises used: mul_assoc, inv_mul_cancel₀
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
n : ℕ
h : Ne (α := ℤ) (↑n : ℤ) 0
rw : n ≠ 0
⊢ HPow.hPow (α := G₀) (β := ℤ) 0 (↑n : ℤ) = 0

Tactic:
rw [zpow_natCast, zero_pow]

Premises used: zpow_natCast, zero_pow
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
n : ℕ
h : Ne (α := ℤ) (↑n : ℤ) 0
⊢ n ≠ 0

Tactic:
simpa [Int.natCast_eq_zero] using h

Premises used: Int.natCast_eq_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
n : ℕ
h : Int.negSucc n ≠ 0
⊢ HPow.hPow (α := G₀) 0 (Int.negSucc n) = 0

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
n : ℤ
pos : ∀ (h : n = 0), HPow.hPow (α := G₀) 0 n = 1
neg : ∀ (h : ¬n = 0), HPow.hPow (α := G₀) 0 n = 0
⊢ HPow.hPow (α := G₀) 0 n = if n = 0 then 1 else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
n : ℤ
h : n = 0
pos : HPow.hPow (α := G₀) (β := ℤ) 0 0 = 1
pos₁ pos₂ : Eq.{u_2 + 1} (α := G₀) 1 1
⊢ HPow.hPow (α := G₀) 0 n = 1

Tactic:
rw [h, zpow_zero]

Premises used: zpow_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
n : ℤ
h : ¬n = 0
neg neg₁ : Eq.{u_2 + 1} (α := G₀) 0 0
⊢ HPow.hPow (α := G₀) 0 n = 0

Tactic:
rw [zero_zpow _ h]

Premises used: zero_zpow
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
rw₁ rw₂ : n = 0 ↔ n = 0
⊢ HPow.hPow (α := G₀) 0 n = 1 ↔ n = 0

Tactic:
rw [zero_zpow_eq, one_ne_zero.ite_eq_left_iff]

Premises used: Ne.ite_eq_left_iff, zero_zpow_eq, one_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ a ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = HPow.hPow (β := ℤ) a (↑n : ℤ) * a

Tactic:
simp only [← Int.natCast_succ, zpow_natCast, pow_succ]

Premises used: zpow_natCast, pow_succ, Int.natCast_succ
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
⊢ a ^ HAdd.hAdd (α := ℤ) (-1) 1 = HPow.hPow (β := ℤ) a (-1) * a

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
rw₁₂ rw₁₃ : (a ^ (n + 1))⁻¹ = (a ^ (n + 1))⁻¹
⊢ a ^ (Int.negSucc (n + 1) + 1) = a ^ Int.negSucc (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]

Premises used: zpow_natCast, mul_assoc, Int.neg_add_cancel_right, Int.natCast_succ, HAdd.hAdd, Int.neg_add, zpow_neg, Int.negSucc_eq, mul_inv_rev, mul_one, OfNat.ofNat, inv_mul_cancel₀, pow_succ'
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
rw₂ rw₃ : a ^ (n - 1) = a ^ (n - 1)
⊢ a ^ (n - 1) = a ^ (n - 1) * a * a⁻¹

Tactic:
rw [mul_assoc, mul_inv_cancel₀ ha, mul_one]

Premises used: mul_inv_cancel₀, mul_assoc, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℤ
rw : a ^ (n - 1 + 1) * a⁻¹ = a ^ n * a⁻¹
rw₁ rw₂ : a ^ n * a⁻¹ = a ^ n * a⁻¹
⊢ a ^ (n - 1) * a * a⁻¹ = a ^ n * a⁻¹

Tactic:
rw [← zpow_add_one₀ ha, Int.sub_add_cancel]

Premises used: zpow_add_one₀, Int.sub_add_cancel
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
⊢ a ^ (m + 0) = a ^ m * HPow.hPow (β := ℤ) a 0

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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 + HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = a ^ m * a ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1

Tactic:
simp only [← Int.add_assoc, zpow_add_one₀ ha, ihn, mul_assoc]

Premises used: zpow_add_one₀, mul_assoc, Int.add_assoc
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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)
pred₄ pred₅ : a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
⊢ a ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = a ^ m * a ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1

Tactic:
rw [zpow_sub_one₀ ha, ← mul_assoc, ← ihn, ← zpow_sub_one₀ ha, Int.add_sub_assoc]

Premises used: mul_assoc, zpow_sub_one₀, Int.add_sub_assoc
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
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
⊢ a ^ (m + n) = a ^ m * a ^ n

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]

Premises used: zpow_add_one₀, mul_assoc, Int.add_assoc, zpow_sub_one₀, Int.add_sub_assoc
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
neg : ∀ (hm : ¬m = 0), a ^ (m + n) = a ^ m * a ^ n
⊢ a ^ (m + n) = a ^ m * a ^ n

Tactic:
by_cases hm : m = 0
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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

Tactic:
simp [hm]
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
neg : ∀ (hn : ¬n = 0), a ^ (m + n) = a ^ m * a ^ n
⊢ a ^ (m + n) = a ^ m * a ^ n

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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

Tactic:
simp [hn]
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
neg : ∀ (ha : ¬a = 0), a ^ (m + n) = a ^ m * a ^ n
⊢ a ^ (m + n) = a ^ m * a ^ n

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
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
⊢ a ^ (m + n) = a ^ m * a ^ n

Tactic:
subst a
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
⊢ ¬m + n = 0

Tactic:
simp only [false_or, not_true, Ne, hm, hn, false_and, or_false] at h

Premises used: false_and, Ne, false_or, not_true, or_false
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
pos₂ pos₃ : Eq.{u_2 + 1} (α := G₀) 0 0
⊢ HPow.hPow (α := G₀) 0 (m + n) = HPow.hPow (α := G₀) 0 m * HPow.hPow (α := G₀) 0 n

Tactic:
rw [zero_zpow _ h, zero_zpow _ hm, zero_mul]

Premises used: zero_zpow, MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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

Tactic:
zpow_add₀ ha m n

Premises used: zpow_add₀
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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

Tactic:
exact zpow_add₀ ha m n

Premises used: zpow_add₀
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
h : a ≠ 0
i : ℤ
rw : HPow.hPow (β := ℤ) a 1 * a ^ i = a * a ^ i
rw₁ rw₂ : a * a ^ i = a * a ^ i
⊢ a ^ (1 + i) = a * a ^ i

Tactic:
rw [zpow_add₀ h, zpow_one]

Premises used: zpow_one, zpow_add₀
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : CommGroupWithZero G₀
a b c : G₀
simp_rw : a * c⁻¹ * b = a * b * c⁻¹
simp_rw₁ : a * (c⁻¹ * b) = a * (b * c⁻¹)
⊢ a / c * b = a * b / c

Tactic:
simp_rw [div_eq_mul_inv, mul_assoc, mul_comm c⁻¹]

Premises used: mul_assoc, div_eq_mul_inv, Inv.inv, mul_comm
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : CommGroupWithZero G₀
a b : G₀
inl : HPow.hPow (α := G₀) (β := ℕ) 0 2 * b / 0 = 0 * b
inr : ∀ (ha : a ≠ 0), HPow.hPow (β := ℕ) a 2 * b / a = a * b
⊢ HPow.hPow (β := ℕ) a 2 * b / a = a * b

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Basic
Goal:
G₀ : Type u_2
inst : CommGroupWithZero G₀
b : G₀
⊢ HPow.hPow (α := G₀) (β := ℕ) 0 2 * b / 0 = 0 * b

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Basic
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
inr₂ inr₃ : a * b = a * b
⊢ HPow.hPow (β := ℕ) a 2 * b / a = a * b

Tactic:
rw [sq, mul_assoc, mul_div_cancel_left₀ _ ha]

Premises used: mul_assoc, mul_div_cancel_left₀, sq
-- Module: Mathlib.Algebra.GroupWithZero.Commute
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀
h : Commute a b
pos : ∀ (hab : IsUnit (a * b)), (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
neg : ∀ (hab : ¬IsUnit (a * b)), (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
by_cases hab : IsUnit (a * b)

Premises used: HMul.hMul, IsUnit