awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.Commute
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : IsUnit (a * b)
pos :
  ∀ (a b : M₀ˣ) (h : Commute (↑a : M₀) (↑b : M₀)) (hab : IsUnit ((↑a : M₀) * (↑b : M₀))),
    ((↑a : M₀) * (↑b : M₀))⁻¹ʳ = (↑b : M₀)⁻¹ʳ * (↑a : M₀)⁻¹ʳ
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
obtain ⟨⟨a, rfl⟩, b, rfl⟩ := h.isUnit_mul_iff.mp hab

Premises used: Commute.isUnit_mul_iff, Iff.mp, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Commute
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₀)
pos₅ pos₆ : (↑(b⁻¹ * a⁻¹) : M₀) = (↑(b⁻¹ * a⁻¹) : M₀)
⊢ ((↑a : M₀) * (↑b : M₀))⁻¹ʳ = (↑b : M₀)⁻¹ʳ * (↑a : M₀)⁻¹ʳ

Tactic:
rw [← Units.val_mul, inverse_unit, inverse_unit, inverse_unit, ← Units.val_mul, mul_inv_rev]

Premises used: Ring.inverse_unit, mul_inv_rev, Units.val_mul
-- Module: Mathlib.Algebra.GroupWithZero.Commute
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⁻¹ʳ
neg₁ : ∀ (hb : ¬IsUnit b), (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
obtain ha | hb := not_and_or.mp (mt h.isUnit_mul_iff.mpr hab)

Premises used: Iff.mpr, mt, not_and_or, Commute.isUnit_mul_iff, Iff.mp
-- Module: Mathlib.Algebra.GroupWithZero.Commute
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
neg₂ neg₃ : Eq.{u_1 + 1} (α := M₀) 0 0
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
rw [inverse_non_unit _ hab, inverse_non_unit _ ha, mul_zero]

Premises used: MulZeroClass.mul_zero, Ring.inverse_non_unit
-- Module: Mathlib.Algebra.GroupWithZero.Commute
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⁻¹ʳ
neg₂ neg₃ : Eq.{u_1 + 1} (α := M₀) 0 0
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
rw [inverse_non_unit _ hab, inverse_non_unit _ hb, zero_mul]

Premises used: MulZeroClass.zero_mul, Ring.inverse_non_unit
-- Module: Mathlib.Algebra.GroupWithZero.Commute
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
a b : M₀
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
mul_inverse_rev' (Commute.all _ _)

Premises used: Ring.mul_inverse_rev', Commute.all
-- Module: Mathlib.Algebra.GroupWithZero.Commute
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
r : M₀
rw : 1 = (HPow.hPow (β := ℕ) r 0)⁻¹ʳ
rw₁ : Eq.{u_1 + 1} (α := M₀) 1 1⁻¹ʳ
rw₂ rw₃ : Eq.{u_1 + 1} (α := M₀) 1 1
⊢ HPow.hPow (β := ℕ) r⁻¹ʳ 0 = (HPow.hPow (β := ℕ) r 0)⁻¹ʳ

Tactic:
rw [pow_zero, pow_zero, Ring.inverse_one]

Premises used: pow_zero, Ring.inverse_one
-- Module: Mathlib.Algebra.GroupWithZero.Commute
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)⁻¹ʳ
rw₃ rw₄ : r⁻¹ʳ * (r ^ n)⁻¹ʳ = r⁻¹ʳ * (r ^ n)⁻¹ʳ
⊢ r⁻¹ʳ ^ (n + 1) = (r ^ (n + 1))⁻¹ʳ

Tactic:
rw [pow_succ', pow_succ, Ring.mul_inverse_rev' ((Commute.refl r).pow_left n),
      Ring.inverse_pow r n]

Premises used: pow_succ, Ring.mul_inverse_rev', Commute.pow_left, Commute.refl, pow_succ'
-- Module: Mathlib.Algebra.GroupWithZero.Commute
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b c : M₀
ha : IsUnit a
k : ℕ
rw : (a ^ k)⁻¹ʳ * b = c ↔ b = a ^ k * c
rw₁ rw₂ : b = a ^ k * c ↔ b = a ^ k * c
⊢ a⁻¹ʳ ^ k * b = c ↔ b = a ^ k * c

Tactic:
rw [Ring.inverse_pow, Ring.inverse_mul_eq_iff_eq_mul _ _ _ (IsUnit.pow _ ha)]

Premises used: Ring.inverse_mul_eq_iff_eq_mul, IsUnit.pow, Ring.inverse_pow
-- Module: Mathlib.Algebra.GroupWithZero.Commute
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : M₀
h : Commute a b
⊢ Commute a⁻¹ʳ b⁻¹ʳ

Tactic:
(Ring.mul_inverse_rev' h.symm).symm.trans <| (congr_arg _ h.symm.eq).trans <|
    Ring.mul_inverse_rev' h

Premises used: Ring.mul_inverse_rev', SemiconjBy, Commute, congr_arg, Commute.symm, Eq.symm, Commute.eq, Eq.trans
-- Module: Mathlib.Algebra.GroupWithZero.Commute
Goal:
G₀ : Type u_2
inst : MulZeroClass G₀
a : G₀
⊢ Commute a 0

Tactic:
SemiconjBy.zero_right a

Premises used: SemiconjBy.zero_right, Commute
-- Module: Mathlib.Algebra.GroupWithZero.Commute
Goal:
G₀ : Type u_2
inst : MulZeroClass G₀
a : G₀
⊢ Commute 0 a

Tactic:
SemiconjBy.zero_left a a

Premises used: Commute, SemiconjBy.zero_left
-- Module: Mathlib.Algebra.GroupWithZero.Commute
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a b : G₀
⊢ Commute a⁻¹ b ↔ Commute a b

Tactic:
SemiconjBy.inv_symm_left_iff₀

Premises used: Commute, SemiconjBy.inv_symm_left_iff₀
-- Module: Mathlib.Algebra.GroupWithZero.Commute
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a b : G₀
h : Commute a b
⊢ Commute a⁻¹ b

Tactic:
inv_left_iff₀.2 h

Premises used: Iff.mpr, Commute.inv_left_iff₀
-- Module: Mathlib.Algebra.GroupWithZero.Commute
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a b : G₀
⊢ Commute a b⁻¹ ↔ Commute a b

Tactic:
SemiconjBy.inv_right_iff₀

Premises used: Commute, SemiconjBy.inv_right_iff₀
-- Module: Mathlib.Algebra.GroupWithZero.Commute
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a b : G₀
h : Commute a b
⊢ Commute a b⁻¹

Tactic:
inv_right_iff₀.2 h

Premises used: Iff.mpr, Commute.inv_right_iff₀
-- Module: Mathlib.Algebra.GroupWithZero.Commute
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a b c : G₀
hab : Commute a b
hac : Commute a c
⊢ Commute a (b / c)

Tactic:
SemiconjBy.div_right hab hac

Premises used: SemiconjBy.div_right, Commute
-- Module: Mathlib.Algebra.GroupWithZero.Commute
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a b c : G₀
hac : Commute a c
hbc : Commute b c
rw : Commute (a * b⁻¹) c
⊢ Commute (a / b) c

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.GroupWithZero.Commute
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a b c : G₀
hac : Commute a c
hbc : Commute b c
⊢ Commute (a * b⁻¹) c

Tactic:
hac.mul_left hbc.inv_left₀

Premises used: Commute.mul_left, Commute.inv_left₀
-- Module: Mathlib.Algebra.GroupWithZero.Commute
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a b c : G₀
hac : Commute a c
hbc : Commute b c
⊢ Commute (a * b⁻¹) c

Tactic:
exact hac.mul_left hbc.inv_left₀

Premises used: Commute.mul_left, Commute.inv_left₀
-- Module: Mathlib.Algebra.GroupWithZero.Commute
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a : G₀
m n : ℕ
⊢ a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m

Tactic:
(Commute.refl a).inv_left₀.pow_pow m n

Premises used: SemiconjBy, Commute.pow_pow, Commute, Commute.refl, Commute.inv_left₀
-- Module: Mathlib.Algebra.GroupWithZero.Conj
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
rw : (∃ (x : α), x ≠ 0 ∧ SemiconjBy x a b) ↔ ∃ (c : α), c ≠ 0 ∧ c * a * c⁻¹ = b
⊢ IsConj a b ↔ ∃ (c : α), c ≠ 0 ∧ c * a * c⁻¹ = b

Tactic:
rw [IsConj, Units.exists_iff_ne_zero (p := (SemiconjBy · a b))]

Premises used: Units.exists_iff_ne_zero, IsConj
-- Module: Mathlib.Algebra.GroupWithZero.Conj
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
a₁ : ∀ (c : α), c ≠ 0 ∧ SemiconjBy c a b ↔ c ≠ 0 ∧ c * a * c⁻¹ = b
⊢ (∃ (x : α), x ≠ 0 ∧ SemiconjBy x a b) ↔ ∃ (c : α), c ≠ 0 ∧ c * a * c⁻¹ = b

Tactic:
congr! 2 with c
-- Module: Mathlib.Algebra.GroupWithZero.Conj
Goal:
α : Type u_1
inst : GroupWithZero α
a b c : α
⊢ c ≠ 0 ∧ SemiconjBy c a b ↔ c ≠ 0 ∧ c * a * c⁻¹ = b

Tactic:
and_congr_right (mul_inv_eq_iff_eq_mul₀ · |>.symm)

Premises used: and_congr_right, mul_inv_eq_iff_eq_mul₀, Iff.symm
-- Module: Mathlib.Algebra.GroupWithZero.Conj
Goal:
α : Type u_1
inst : GroupWithZero α
a b c : α
⊢ c ≠ 0 ∧ SemiconjBy c a b ↔ c ≠ 0 ∧ c * a * c⁻¹ = b

Tactic:
exact and_congr_right (mul_inv_eq_iff_eq_mul₀ · |>.symm)

Premises used: and_congr_right, mul_inv_eq_iff_eq_mul₀, Iff.symm
-- Module: Mathlib.Algebra.GroupWithZero.Conj
Goal:
α : Type u_1
inst : GroupWithZero α
s : ℕ
a d : α
ha : a ≠ 0
⊢ (a⁻¹ * d * a) ^ s = a⁻¹ * d ^ s * a

Tactic:
let u : αˣ := ⟨a, a⁻¹, mul_inv_cancel₀ ha, inv_mul_cancel₀ ha⟩
  Units.conj_pow' u d s

Premises used: mul_inv_cancel₀, Units.conj_pow', Inv.inv, Units.mk, inv_mul_cancel₀
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : Mul M₀
inst_1 : Zero M₀
inst_2 : IsLeftCancelMulZero M₀
a b c : M₀
ha : a ≠ 0
h : a * b = a * c
⊢ b = c

Tactic:
IsLeftCancelMulZero.mul_left_cancel_of_ne_zero ha h

Premises used: IsLeftCancelMulZero.mul_left_cancel_of_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : Mul M₀
inst_1 : Zero M₀
inst_2 : IsLeftCancelMulZero M₀
a : M₀
ha : a ≠ 0
⊢ Function.Injective (β := M₀) fun (x : M₀) ↦ a * x

Tactic:
fun _ _ => mul_left_cancel₀ ha

Premises used: mul_left_cancel₀, Function.Injective
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : Mul M₀
inst_1 : Zero M₀
inst_2 : IsLeftCancelMulZero M₀
a b c : M₀
ha : a ≠ 0
⊢ a * b = a * c ↔ b = c

Tactic:
(mul_right_injective₀ ha).eq_iff

Premises used: Function.Injective.eq_iff, mul_right_injective₀
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : IsLeftCancelMulZero M₀
a b c : M₀
pos : ∀ (ha : a = 0), a * b = a * c ↔ b = c ∨ a = 0
neg : ∀ (ha : ¬a = 0), a * b = a * c ↔ b = c ∨ a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : IsLeftCancelMulZero M₀
a b c : M₀
ha : a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0

Tactic:
simp only [ha, zero_mul, or_true]

Premises used: MulZeroClass.zero_mul, or_true
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : IsLeftCancelMulZero M₀
a b c : M₀
ha : ¬a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0

Tactic:
simp [mul_right_inj', ha]

Premises used: mul_right_inj'
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : IsLeftCancelMulZero M₀
a b c : M₀
pos : ∀ (ha : a = 0), a * b = a * c ↔ b = c ∨ a = 0
neg : ∀ (ha : ¬a = 0), a * b = a * c ↔ b = c ∨ a = 0
pos₁ : ∀ (ha : a = 0), a * b = a * c ↔ b = c ∨ a = 0
neg₁ : ∀ (ha : ¬a = 0), a * b = a * c ↔ b = c ∨ a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0

Tactic:
by_cases ha : a = 0 <;> [simp only [ha, zero_mul, or_true]; simp [mul_right_inj', ha]]

Premises used: MulZeroClass.zero_mul, mul_right_inj', or_true
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : Mul M₀
inst_1 : Zero M₀
inst_2 : IsRightCancelMulZero M₀
a b c : M₀
hb : b ≠ 0
h : a * b = c * b
⊢ a = c

Tactic:
IsRightCancelMulZero.mul_right_cancel_of_ne_zero hb h

Premises used: IsRightCancelMulZero.mul_right_cancel_of_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : Mul M₀
inst_1 : Zero M₀
inst_2 : IsRightCancelMulZero M₀
b : M₀
hb : b ≠ 0
⊢ Function.Injective (β := M₀) fun (a : M₀) ↦ a * b

Tactic:
fun _ _ => mul_right_cancel₀ hb

Premises used: Function.Injective, mul_right_cancel₀
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : Mul M₀
inst_1 : Zero M₀
inst_2 : IsRightCancelMulZero M₀
a b c : M₀
hc : c ≠ 0
⊢ a * c = b * c ↔ a = b

Tactic:
(mul_left_injective₀ hc).eq_iff

Premises used: mul_left_injective₀, Function.Injective.eq_iff
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : IsRightCancelMulZero M₀
a b c : M₀
pos : ∀ (hc : c = 0), a * c = b * c ↔ a = b ∨ c = 0
neg : ∀ (hc : ¬c = 0), a * c = b * c ↔ a = b ∨ c = 0
⊢ a * c = b * c ↔ a = b ∨ c = 0

Tactic:
by_cases hc : c = 0
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : IsRightCancelMulZero M₀
a b c : M₀
hc : c = 0
⊢ a * c = b * c ↔ a = b ∨ c = 0

Tactic:
simp only [hc, mul_zero, or_true]

Premises used: MulZeroClass.mul_zero, or_true
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : IsRightCancelMulZero M₀
a b c : M₀
hc : ¬c = 0
⊢ a * c = b * c ↔ a = b ∨ c = 0

Tactic:
simp [mul_left_inj', hc]

Premises used: mul_left_inj'
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : IsRightCancelMulZero M₀
a b c : M₀
pos : ∀ (hc : c = 0), a * c = b * c ↔ a = b ∨ c = 0
neg : ∀ (hc : ¬c = 0), a * c = b * c ↔ a = b ∨ c = 0
pos₁ : ∀ (hc : c = 0), a * c = b * c ↔ a = b ∨ c = 0
neg₁ : ∀ (hc : ¬c = 0), a * c = b * c ↔ a = b ∨ c = 0
⊢ a * c = b * c ↔ a = b ∨ c = 0

Tactic:
by_cases hc : c = 0 <;> [simp only [hc, mul_zero, or_true]; simp [mul_left_inj', hc]]

Premises used: MulZeroClass.mul_zero, mul_left_inj', or_true
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_2
inst : Mul M₀
inst_1 : Zero M₀
simp : (∀ (x : M₀) (x_1 : x ≠ 0), IsLeftRegular x ∧ IsRightRegular x) ↔ ∀ {a : M₀}, a ≠ 0 → IsRegular a
⊢ IsCancelMulZero M₀ ↔ ∀ {a : M₀}, a ≠ 0 → IsRegular a

Tactic:
simp only [isCancelMulZero_iff, isLeftCancelMulZero_iff, isRightCancelMulZero_iff, ← forall_and]

Premises used: isCancelMulZero_iff, isRightCancelMulZero_iff, isLeftCancelMulZero_iff, forall_and
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_2
inst : Mul M₀
inst_1 : Zero M₀
⊢ (∀ (x : M₀) (x_1 : x ≠ 0), IsLeftRegular x ∧ IsRightRegular x) ↔ ∀ {a : M₀}, a ≠ 0 → IsRegular a

Tactic:
forall₂_congr fun _ _ ↦ isRegular_iff.symm

Premises used: isRegular_iff, forall₂_congr, Iff.symm
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_2
inst : Mul M₀
inst_1 : Zero M₀
⊢ (∀ (x : M₀) (x_1 : x ≠ 0), IsLeftRegular x ∧ IsRightRegular x) ↔ ∀ {a : M₀}, a ≠ 0 → IsRegular a

Tactic:
exact forall₂_congr fun _ _ ↦ isRegular_iff.symm

Premises used: isRegular_iff, forall₂_congr, Iff.symm
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
M : Type u_2
inst_1 : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
y : M₀
zero : f (1 * y) = HPow.hPow (β := ℕ) (f x) 0 * f y
zero₁ : f (1 * y) = 1 * f y
zero₂ : f y = 1 * f y
zero₃ zero₄ : f y = f y
⊢ f (HPow.hPow (β := ℕ) x 0 * y) = HPow.hPow (β := ℕ) (f x) 0 * f y

Tactic:
rw [pow_zero, pow_zero, one_mul, one_mul]

Premises used: pow_zero, one_mul
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
M : Type u_2
inst_1 : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
hn : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y
y : M₀
succ : f (x * x ^ n * y) = f x ^ (n + 1) * f y
succ₁ : f (x * x ^ n * y) = f x * f x ^ n * f y
succ₂ : f (x * (x ^ n * y)) = f x * f x ^ n * f y
succ₃ : f (x * (x ^ n * y)) = f x * (f x ^ n * f y)
succ₄ : f x * f (x ^ n * y) = f x * (f x ^ n * f y)
succ₅ succ₆ : f x * (f x ^ n * f y) = f x * (f x ^ n * f y)
⊢ f (x ^ (n + 1) * y) = f x ^ (n + 1) * f y

Tactic:
rw [pow_succ', pow_succ', mul_assoc, mul_assoc, hx, hn]

Premises used: mul_assoc, pow_succ'
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
M : Type u_2
inst_1 : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
zero : ∀ (y : M₀), f (HPow.hPow (β := ℕ) x 0 * y) = HPow.hPow (β := ℕ) (f x) 0 * f y
succ : ∀ (n : ℕ) (hn : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y) (y : M₀), f (x ^ (n + 1) * y) = f x ^ (n + 1) * f y
⊢ ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y

Tactic:
induction n with
  | zero => intro y; rw [pow_zero, pow_zero, one_mul, one_mul]
  | succ n hn => intro y; rw [pow_succ', pow_succ', mul_assoc, mul_assoc, hx, hn]

Premises used: mul_assoc, pow_zero, pow_succ', one_mul
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : CommMagma M₀
inst_1 : Zero M₀
inst_2 : IsLeftCancelMulZero M₀
⊢ IsCancelMulZero M₀

Tactic:
{ IsLeftCancelMulZero.to_isRightCancelMulZero with }

Premises used: IsCancelMulZero.mk, IsLeftCancelMulZero.to_isRightCancelMulZero
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : CommMagma M₀
inst_1 : Zero M₀
inst_2 : IsRightCancelMulZero M₀
⊢ IsCancelMulZero M₀

Tactic:
{ IsRightCancelMulZero.to_isLeftCancelMulZero with }

Premises used: IsRightCancelMulZero.to_isLeftCancelMulZero, IsCancelMulZero.mk
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : Div M₀
inst_2 : MulDivCancelClass M₀
a b : M₀
hb : b ≠ 0
⊢ a * b / b = a

Tactic:
MulDivCancelClass.mul_div_cancel _ _ hb

Premises used: MulDivCancelClass.mul_div_cancel
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
inst_1 : Div M₀
inst_2 : MulDivCancelClass M₀
b a : M₀
ha : a ≠ 0
rw : b * a / a = b
rw₁ rw₂ : b = b
⊢ a * b / a = b

Tactic:
rw [mul_comm, mul_div_cancel_right₀ _ ha]

Premises used: mul_div_cancel_right₀, mul_comm
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
G₀ : Type u
inst : GroupWithZero G₀
⊢ Eq.{u + 1} (α := G₀) 0⁻¹ 0

Tactic:
GroupWithZero.inv_zero

Premises used: GroupWithZero.inv_zero
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
G₀ : Type u
inst : GroupWithZero G₀
a : G₀
h : a ≠ 0
⊢ a * a⁻¹ = 1

Tactic:
GroupWithZero.mul_inv_cancel a h

Premises used: GroupWithZero.mul_inv_cancel
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
G₀ : Type u
M₀ : Type u_1
inst : GroupWithZero G₀
a_1 a b : G₀
hb : b ≠ 0
rw : a * b * b⁻¹ = a
rw₁ : a * (b * b⁻¹) = a
rw₂ : a * 1 = a
rw₃ rw₄ : a = a
⊢ a * b / b = a

Tactic:
rw [div_eq_mul_inv, mul_assoc, mul_inv_cancel₀ hb, mul_one]

Premises used: mul_inv_cancel₀, mul_assoc, div_eq_mul_inv, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
G₀ : Type u
inst : GroupWithZero G₀
b : G₀
h : b ≠ 0
a : G₀
⊢ a * (b * b⁻¹) = a

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

Tactic:
simp [h]
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
a : M₀
h : a = 0
b : M₀
⊢ a * b = 0

Tactic:
h.symm ▸ zero_mul b

Premises used: MulZeroClass.zero_mul, Eq.rec, Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
a b : M₀
h : b = 0
⊢ a * b = 0

Tactic:
h.symm ▸ mul_zero a

Premises used: Eq.rec, MulZeroClass.mul_zero, Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
simp : (∀ {a b : M₀}, a * b = 0 → ¬a = 0 → b = 0) ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), x * y = 0 → y = 0
⊢ NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), x * y = 0 → y = 0

Tactic:
simp only [noZeroDivisors_iff, or_iff_not_imp_left]

Premises used: Classical.or_iff_not_imp_left, noZeroDivisors_iff
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
⊢ (∀ {a b : M₀}, a * b = 0 → ¬a = 0 → b = 0) ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), x * y = 0 → y = 0

Tactic:
⟨fun h a ha b eq ↦ h eq ha, fun h a b eq ha ↦ h a ha b eq⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
⊢ (∀ {a b : M₀}, a * b = 0 → ¬a = 0 → b = 0) ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), x * y = 0 → y = 0

Tactic:
exact ⟨fun h a ha b eq ↦ h eq ha, fun h a b eq ha ↦ h a ha b eq⟩
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
simp : (∀ {a b : M₀}, a * b = 0 → ¬b = 0 → a = 0) ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), y * x = 0 → y = 0
⊢ NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), y * x = 0 → y = 0

Tactic:
simp only [noZeroDivisors_iff, or_iff_not_imp_right]

Premises used: Classical.or_iff_not_imp_right, noZeroDivisors_iff
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
⊢ (∀ {a b : M₀}, a * b = 0 → ¬b = 0 → a = 0) ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), y * x = 0 → y = 0

Tactic:
⟨fun h b hb a eq ↦ h eq hb, fun h a b eq hb ↦ h b hb a eq⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
⊢ (∀ {a b : M₀}, a * b = 0 → ¬b = 0 → a = 0) ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), y * x = 0 → y = 0

Tactic:
exact ⟨fun h b hb a eq ↦ h eq hb, fun h a b eq hb ↦ h b hb a eq⟩
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
⊢ NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → (∀ (y : M₀), x * y = 0 → y = 0) ∧ ∀ (y : M₀), y * x = 0 → y = 0

Tactic:
simp only [forall_and, ← noZeroDivisors_iff_right_eq_zero_of_mul,
    ← noZeroDivisors_iff_left_eq_zero_of_mul, and_self]

Premises used: and_self, noZeroDivisors_iff_left_eq_zero_of_mul, forall_and, noZeroDivisors_iff_right_eq_zero_of_mul
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : NoZeroDivisors M₀
a b : M₀
⊢ a * b = 0 ↔ a = 0 ∨ b = 0

Tactic:
⟨eq_zero_or_eq_zero_of_mul_eq_zero,
    fun o ↦ o.elim (fun h ↦ mul_eq_zero_of_left h b) (mul_eq_zero_of_right a)⟩

Premises used: mul_eq_zero_of_right, mul_eq_zero_of_left, Iff.intro, Or.elim, NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : NoZeroDivisors M₀
a b : M₀
⊢ 0 = a * b ↔ a = 0 ∨ b = 0

Tactic:
simp [eqComm]

Premises used: eqComm
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : NoZeroDivisors M₀
a b : M₀
⊢ a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0

Tactic:
mul_eq_zero.not.trans not_or

Premises used: Iff.not, mul_eq_zero, not_or, Iff.trans
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : NoZeroDivisors M₀
a b : M₀
⊢ a * b = 0 ↔ b * a = 0

Tactic:
mul_eq_zero.trans <| or_comm.trans mul_eq_zero.symm

Premises used: mul_eq_zero, Iff.trans, or_comm, Iff.symm
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : NoZeroDivisors M₀
a b : M₀
⊢ a * b ≠ 0 ↔ b * a ≠ 0

Tactic:
mul_eq_zero_comm.not

Premises used: Iff.not, mul_eq_zero_comm
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : NoZeroDivisors M₀
a : M₀
⊢ a * a = 0 ↔ a = 0

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : NoZeroDivisors M₀
a : M₀
⊢ 0 = a * a ↔ a = 0

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : NoZeroDivisors M₀
a : M₀
⊢ a * a ≠ 0 ↔ a ≠ 0

Tactic:
mul_self_eq_zero.not

Premises used: mul_self_eq_zero, Iff.not
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : NoZeroDivisors M₀
a : M₀
⊢ 0 ≠ a * a ↔ a ≠ 0

Tactic:
zero_eq_mul_self.not

Premises used: Iff.not, zero_eq_mul_self
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : NoZeroDivisors M₀
a b : M₀
ha : a ≠ 0
⊢ a * b = 0 ↔ b = 0

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : NoZeroDivisors M₀
a b : M₀
hb : b ≠ 0
⊢ a * b = 0 ↔ a = 0

Tactic:
simp [hb]
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : NoZeroDivisors M₀
a b : M₀
ha : a ≠ 0
⊢ a * b ≠ 0 ↔ b ≠ 0

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.GroupWithZero.Defs
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : NoZeroDivisors M₀
a b : M₀
hb : b ≠ 0
⊢ a * b ≠ 0 ↔ a ≠ 0

Tactic:
simp [hb]
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : SemigroupWithZero α
a : α
h : 0 ∣ a
⊢ a = 0

Tactic:
Dvd.elim h fun c H' => H'.trans (zero_mul c)

Premises used: Dvd.elim, MulZeroClass.zero_mul, Eq.trans
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : SemigroupWithZero α
a : α
h : a = 0
rw : Dvd.dvd.{u_1} (α := α) 0 0
⊢ 0 ∣ a

Tactic:
rw [h]
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : SemigroupWithZero α
a : α
h : a = 0
⊢ 0 = HMul.hMul (α := α) 0 0

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : SemigroupWithZero α
a : α
h : a = 0
⊢ Dvd.dvd.{u_1} (α := α) 0 0

Tactic:
exact ⟨0, by simp⟩
-- Module: Mathlib.Algebra.GroupWithZero.Divisibility
Goal:
α : Type u_1
inst : SemigroupWithZero α
a : α
⊢ a * 0 = 0

Tactic:
simp