awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.InjSurj
Goal:
M₀ : Type u_1
M₀' : Type u_3
inst : Mul M₀
inst_1 : Zero M₀
inst_2 : Mul M₀'
inst_3 : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst_4 : NoZeroDivisors M₀'
a b : M₀
H_1 : a * b = 0
this : f a * f b = 0
H rwa rwa₁ rwa₂ rwa₃ : f a = 0
⊢ f a = f 0

Tactic:
rwa [zero]
-- Module: Mathlib.Algebra.GroupWithZero.InjSurj
Goal:
M₀ : Type u_1
M₀' : Type u_3
inst : Mul M₀
inst_1 : Zero M₀
inst_2 : Mul M₀'
inst_3 : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst_4 : NoZeroDivisors M₀'
a b : M₀
H_1 : a * b = 0
this : f a * f b = 0
H rwa rwa₁ rwa₂ rwa₃ : f b = 0
⊢ f b = f 0

Tactic:
rwa [zero]
-- Module: Mathlib.Algebra.GroupWithZero.InjSurj
Goal:
M₀ : Type u_1
M₀' : Type u_3
inst : Mul M₀
inst_1 : Zero M₀
inst_2 : Mul M₀'
inst_3 : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst_4 : IsLeftCancelMulZero M₀'
a : M₀
Hne : a ≠ 0
x x_1 : M₀
He : Eq.{u_1 + 1} (α := M₀) ((fun (x : M₀) ↦ a * x) x) ((fun (x : M₀) ↦ a * x) x_1)
⊢ f ((fun (x : M₀) ↦ a * x) x) = f ((fun (x : M₀) ↦ a * x) x_1)

Tactic:
have := congr_arg f He
-- Module: Mathlib.Algebra.GroupWithZero.InjSurj
Goal:
M₀ : Type u_1
M₀' : Type u_3
inst : Mul M₀
inst_1 : Zero M₀
inst_2 : Mul M₀'
inst_3 : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst_4 : IsLeftCancelMulZero M₀'
a : M₀
Hne : a ≠ 0
x x_1 : M₀
He : Eq.{u_1 + 1} (α := M₀) ((fun (x : M₀) ↦ a * x) x) ((fun (x : M₀) ↦ a * x) x_1)
this : f ((fun (x : M₀) ↦ a * x) x) = f ((fun (x : M₀) ↦ a * x) x_1)
⊢ f a * f x = f a * f x_1

Tactic:
rw [mul, mul] at this
-- Module: Mathlib.Algebra.GroupWithZero.InjSurj
Goal:
M₀ : Type u_1
M₀' : Type u_3
inst : Mul M₀
inst_1 : Zero M₀
inst_2 : Mul M₀'
inst_3 : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst_4 : IsLeftCancelMulZero M₀'
a : M₀
Hne : a ≠ 0
x x_1 : M₀
He : Eq.{u_1 + 1} (α := M₀) ((fun (x : M₀) ↦ a * x) x) ((fun (x : M₀) ↦ a * x) x_1)
this : f a * f x = f a * f x_1
Hfa : f a = 0
rw : 0 = f 0
rw₁ rw₂ : Eq.{u_3 + 1} (α := M₀') 0 0
⊢ f a = f 0

Tactic:
rw [Hfa, zero]
-- Module: Mathlib.Algebra.GroupWithZero.InjSurj
Goal:
M₀ : Type u_1
M₀' : Type u_3
inst : Mul M₀
inst_1 : Zero M₀
inst_2 : Mul M₀'
inst_3 : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst_4 : IsLeftCancelMulZero M₀'
a : M₀
Hne : a ≠ 0
x x_1 : M₀
He : Eq.{u_1 + 1} (α := M₀) ((fun (x : M₀) ↦ a * x) x) ((fun (x : M₀) ↦ a * x) x_1)
this : f a * f x = f a * f x_1
⊢ x = x_1

Tactic:
exact hf (mul_left_cancel₀ (fun Hfa => Hne <| hf <| by rw [Hfa, zero]) this)

Premises used: mul_left_cancel₀
-- Module: Mathlib.Algebra.GroupWithZero.InjSurj
Goal:
M₀ : Type u_1
M₀' : Type u_3
inst : Mul M₀
inst_1 : Zero M₀
inst_2 : Mul M₀'
inst_3 : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst_4 : IsRightCancelMulZero M₀'
a : M₀
Hne : a ≠ 0
x x_1 : M₀
He : Eq.{u_1 + 1} (α := M₀) ((fun (x : M₀) ↦ x * a) x) ((fun (x : M₀) ↦ x * a) x_1)
⊢ f ((fun (x : M₀) ↦ x * a) x) = f ((fun (x : M₀) ↦ x * a) x_1)

Tactic:
have := congr_arg f He
-- Module: Mathlib.Algebra.GroupWithZero.InjSurj
Goal:
M₀ : Type u_1
M₀' : Type u_3
inst : Mul M₀
inst_1 : Zero M₀
inst_2 : Mul M₀'
inst_3 : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst_4 : IsRightCancelMulZero M₀'
a : M₀
Hne : a ≠ 0
x x_1 : M₀
He : Eq.{u_1 + 1} (α := M₀) ((fun (x : M₀) ↦ x * a) x) ((fun (x : M₀) ↦ x * a) x_1)
this : f ((fun (x : M₀) ↦ x * a) x) = f ((fun (x : M₀) ↦ x * a) x_1)
⊢ f x * f a = f x_1 * f a

Tactic:
rw [mul, mul] at this
-- Module: Mathlib.Algebra.GroupWithZero.InjSurj
Goal:
M₀ : Type u_1
M₀' : Type u_3
inst : Mul M₀
inst_1 : Zero M₀
inst_2 : Mul M₀'
inst_3 : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst_4 : IsRightCancelMulZero M₀'
a : M₀
Hne : a ≠ 0
x x_1 : M₀
He : Eq.{u_1 + 1} (α := M₀) ((fun (x : M₀) ↦ x * a) x) ((fun (x : M₀) ↦ x * a) x_1)
this : f x * f a = f x_1 * f a
Hfa : f a = 0
rw : 0 = f 0
rw₁ rw₂ : Eq.{u_3 + 1} (α := M₀') 0 0
⊢ f a = f 0

Tactic:
rw [Hfa, zero]
-- Module: Mathlib.Algebra.GroupWithZero.InjSurj
Goal:
M₀ : Type u_1
M₀' : Type u_3
inst : Mul M₀
inst_1 : Zero M₀
inst_2 : Mul M₀'
inst_3 : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst_4 : IsRightCancelMulZero M₀'
a : M₀
Hne : a ≠ 0
x x_1 : M₀
He : Eq.{u_1 + 1} (α := M₀) ((fun (x : M₀) ↦ x * a) x) ((fun (x : M₀) ↦ x * a) x_1)
this : f x * f a = f x_1 * f a
⊢ x = x_1

Tactic:
exact hf (mul_right_cancel₀ (fun Hfa => Hne <| hf <| by rw [Hfa, zero]) this)

Premises used: mul_right_cancel₀
-- Module: Mathlib.Algebra.GroupWithZero.InjSurj
Goal:
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst : GroupWithZero G₀
inst_1 : Zero G₀'
inst_2 : Mul G₀'
inst_3 : One G₀'
inst_4 : Inv G₀'
inst_5 : Div G₀'
inst_6 : Pow G₀' ℕ
inst_7 : Pow G₀' ℤ
f : G₀' → G₀
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀'), f (x * y) = f x * f y
inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀'), f (x / y) = f x / f y
npow : ∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n
rw : (f 0)⁻¹ = f 0
rw₁ : Eq.{u_2 + 1} (α := G₀) 0⁻¹ 0
rw₂ rw₃ : Eq.{u_2 + 1} (α := G₀) 0 0
⊢ f 0⁻¹ = f 0

Tactic:
rw [inv, zero, inv_zero]

Premises used: inv_zero
-- Module: Mathlib.Algebra.GroupWithZero.InjSurj
Goal:
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst : GroupWithZero G₀
inst_1 : Zero G₀'
inst_2 : Mul G₀'
inst_3 : One G₀'
inst_4 : Inv G₀'
inst_5 : Div G₀'
inst_6 : Pow G₀' ℕ
inst_7 : Pow G₀' ℤ
f : G₀' → G₀
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀'), f (x * y) = f x * f y
inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀'), f (x / y) = f x / f y
npow : ∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n
x : G₀'
hx : x ≠ 0
rw : f (x * x⁻¹) = 1
rw₁ : f x * f x⁻¹ = 1
rw₂ : f x * (f x)⁻¹ = 1
rw₃ rw₄ : Eq.{u_2 + 1} (α := G₀) 1 1
⊢ f (x * x⁻¹) = f 1

Tactic:
rw [one, mul, inv, mul_inv_cancel₀ ((hf.ne_iff' zero).2 hx)]

Premises used: Iff.mpr, mul_inv_cancel₀, Function.Injective.ne_iff'
-- Module: Mathlib.Algebra.GroupWithZero.InjSurj
Goal:
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst : GroupWithZero G₀
inst_1 : Zero G₀'
inst_2 : Mul G₀'
inst_3 : One G₀'
inst_4 : Inv G₀'
inst_5 : Div G₀'
inst_6 : Pow G₀' ℕ
inst_7 : Pow G₀' ℤ
h01 : Ne.{u_4 + 1} (α := G₀') 0 1
f : G₀ → G₀'
hf : Surjective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀), f (x * y) = f x * f y
inv : ∀ (x : G₀), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀), f (x / y) = f x / f y
npow : ∀ (x : G₀) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀) (n : ℤ), f (x ^ n) = f x ^ n
rw : (f 0)⁻¹ = f 0
rw₁ : f 0⁻¹ = f 0
rw₂ rw₃ : f 0 = f 0
⊢ Eq.{u_4 + 1} (α := G₀') 0⁻¹ 0

Tactic:
rw [← zero, ← inv, inv_zero]

Premises used: inv_zero
-- Module: Mathlib.Algebra.GroupWithZero.InjSurj
Goal:
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst : GroupWithZero G₀
inst_1 : Zero G₀'
inst_2 : Mul G₀'
inst_3 : One G₀'
inst_4 : Inv G₀'
inst_5 : Div G₀'
inst_6 : Pow G₀' ℕ
inst_7 : Pow G₀' ℤ
h01 : Ne.{u_4 + 1} (α := G₀') 0 1
f : G₀ → G₀'
hf : Surjective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀), f (x * y) = f x * f y
inv : ∀ (x : G₀), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀), f (x / y) = f x / f y
npow : ∀ (x : G₀) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀) (n : ℤ), f (x ^ n) = f x ^ n
x : G₀
hx : f x ≠ 0
rw : f x * f x⁻¹ = 1
rw₁ : f (x * x⁻¹) = 1
rw₂ : f 1 = 1
rw₃ rw₄ : Eq.{u_4 + 1} (α := G₀') 1 1
⊢ f x * (f x)⁻¹ = 1

Tactic:
rw [← inv, ← mul, mul_inv_cancel₀ (mt (congr_arg f) fun h ↦ hx (h.trans zero)), one]

Premises used: mul_inv_cancel₀, mt, congr_arg, Eq.trans
-- Module: Mathlib.Algebra.GroupWithZero.Invertible
Goal:
α : Type u
inst : MulZeroOneClass α
a : α
inst_1 : Nontrivial α
inst_2 : Invertible a
ha : a = 0
⊢ 0 = @invOf _ MulZeroClass.toMul MulOne.toOne a _ * a

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.GroupWithZero.Invertible
Goal:
α : Type u
inst : MulZeroOneClass α
inst_1 : Nontrivial α
a : α
inst_2 : Invertible a
⊢ NeZero a

Tactic:
⟨Invertible.ne_zero a⟩

Premises used: NeZero.mk, Invertible.ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Invertible
Goal:
α : Type u
inst : MonoidWithZero α
x : α
inst_1 : Invertible x
⊢ x⁻¹ʳ = @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne x _

Tactic:
Ring.inverse_unit (unitOfInvertible _)

Premises used: Ring.inverse_unit, unitOfInvertible
-- Module: Mathlib.Algebra.GroupWithZero.Invertible
Goal:
α : Type u
inst : GroupWithZero α
a : α
inst_1 : Invertible a
⊢ @Invertible.invOf _ MulZeroClass.toMul InvOneClass.toOne a _ = a⁻¹

Tactic:
invOf_eq_right_inv (mul_inv_cancel₀ (Invertible.ne_zero a))

Premises used: Invertible.ne_zero, mul_inv_cancel₀, invOf_eq_right_inv
-- Module: Mathlib.Algebra.GroupWithZero.Invertible
Goal:
α : Type u
inst : GroupWithZero α
a : α
inst_1 : Invertible a
⊢ a⁻¹ * a = 1

Tactic:
inv_mul_cancel₀ (Invertible.ne_zero a)

Premises used: Invertible.ne_zero, inv_mul_cancel₀
-- Module: Mathlib.Algebra.GroupWithZero.Invertible
Goal:
α : Type u
inst : GroupWithZero α
a : α
inst_1 : Invertible a
⊢ a * a⁻¹ = 1

Tactic:
mul_inv_cancel₀ (Invertible.ne_zero a)

Premises used: Invertible.ne_zero, mul_inv_cancel₀
-- Module: Mathlib.Algebra.GroupWithZero.Invertible
Goal:
α : Type u
inst : GroupWithZero α
a : α
inst_1 : Invertible a
⊢ a * a⁻¹ = 1

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Invertible
Goal:
α : Type u
inst : GroupWithZero α
a : α
inst_1 : Invertible a
⊢ a⁻¹ * a = 1

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Invertible
Goal:
α : Type u
inst : GroupWithZero α
a b : α
inst_1 : Invertible b
⊢ a / b * b = a

Tactic:
div_mul_cancel₀ a (Invertible.ne_zero b)

Premises used: div_mul_cancel₀, Invertible.ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Invertible
Goal:
α : Type u
inst : GroupWithZero α
a b : α
inst_1 : Invertible b
⊢ a * b / b = a

Tactic:
mul_div_cancel_right₀ a (Invertible.ne_zero b)

Premises used: Invertible.ne_zero, mul_div_cancel_right₀
-- Module: Mathlib.Algebra.GroupWithZero.Invertible
Goal:
α : Type u
inst : GroupWithZero α
a : α
inst_1 : Invertible a
⊢ a / a = 1

Tactic:
div_self (Invertible.ne_zero a)

Premises used: Invertible.ne_zero, div_self
-- Module: Mathlib.Algebra.GroupWithZero.Invertible
Goal:
α : Type u
inst : GroupWithZero α
a b : α
inst_1 : Invertible a
inst_2 : Invertible b
⊢ b / a * (a / b) = 1

Tactic:
simp [← mul_div_assoc]

Premises used: mul_div_assoc
-- Module: Mathlib.Algebra.GroupWithZero.Invertible
Goal:
α : Type u
inst : GroupWithZero α
a b : α
inst_1 : Invertible a
inst_2 : Invertible b
⊢ a / b * (b / a) = 1

Tactic:
simp [← mul_div_assoc]

Premises used: mul_div_assoc
-- Module: Mathlib.Algebra.GroupWithZero.Invertible
Goal:
α : Type u
inst : GroupWithZero α
a b : α
inst_1 : Invertible a
inst_2 : Invertible b
inst_3 : Invertible (a / b)
⊢ a / b * (b / a) = 1

Tactic:
simp [← mul_div_assoc]

Premises used: mul_div_assoc
-- Module: Mathlib.Algebra.GroupWithZero.NeZero
Goal:
M₀ : Type u_1
M₀' : Type u_2
inst : MulZeroOneClass M₀
inst_1 : Nontrivial M₀
h : Eq.{u_1 + 1} (α := M₀) 1 0
rcases : ∀ (x y : M₀) (hx : x ≠ y), False
⊢ False

Tactic:
rcases exists_pair_ne M₀ with ⟨x, y, hx⟩

Premises used: exists_pair_ne
-- Module: Mathlib.Algebra.GroupWithZero.NeZero
Goal:
M₀ : Type u_1
M₀' : Type u_2
inst : MulZeroOneClass M₀
inst_1 : Nontrivial M₀
h : Eq.{u_1 + 1} (α := M₀) 1 0
x y : M₀
hx : x ≠ y
apply : x = y
⊢ False

Tactic:
apply hx
-- Module: Mathlib.Algebra.GroupWithZero.NeZero
Goal:
M₀ : Type u_1
M₀' : Type u_2
inst : MulZeroOneClass M₀
inst_1 : Nontrivial M₀
h : Eq.{u_1 + 1} (α := M₀) 1 0
x y : M₀
hx : x ≠ y
rw rw₁ : x = x
⊢ x = 1 * x

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.GroupWithZero.NeZero
Goal:
M₀ : Type u_1
M₀' : Type u_2
inst : MulZeroOneClass M₀
inst_1 : Nontrivial M₀
h : Eq.{u_1 + 1} (α := M₀) 1 0
x y : M₀
hx : x ≠ y
rw : 0 * x = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := M₀) 0 0
⊢ 1 * x = 0

Tactic:
rw [h, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.GroupWithZero.NeZero
Goal:
M₀ : Type u_1
M₀' : Type u_2
inst : MulZeroOneClass M₀
inst_1 : Nontrivial M₀
h : Eq.{u_1 + 1} (α := M₀) 1 0
x y : M₀
hx : x ≠ y
rw : 0 = 0 * y
rw₁ rw₂ : Eq.{u_1 + 1} (α := M₀) 0 0
⊢ 0 = 1 * y

Tactic:
rw [h, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.GroupWithZero.NeZero
Goal:
M₀ : Type u_1
M₀' : Type u_2
inst : MulZeroOneClass M₀
inst_1 : Nontrivial M₀
h : Eq.{u_1 + 1} (α := M₀) 1 0
x y : M₀
hx : x ≠ y
rw rw₁ : y = y
⊢ 1 * y = y

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.GroupWithZero.NeZero
Goal:
M₀ : Type u_1
M₀' : Type u_2
inst : MulZeroOneClass M₀
inst_1 : Nontrivial M₀
h : Eq.{u_1 + 1} (α := M₀) 1 0
x y : M₀
hx : x ≠ y
x₁ : x = 1 * x
x₂ : 1 * x = 0
x₃ : 0 = 1 * y
x₄ : 1 * y = y
⊢ x = y

Tactic:
calc
    x = 1 * x := by rw [one_mul]
    _ = 0 := by rw [h, zero_mul]
    _ = 1 * y := by rw [h, zero_mul]
    _ = y := by rw [one_mul]
-- Module: Mathlib.Algebra.GroupWithZero.NeZero
Goal:
M₀ : Type u_1
M₀' : Type u_2
inst : MulZeroOneClass M₀
inst_1 : Nontrivial M₀
inst_2 : Zero M₀'
inst_3 : One M₀'
f : M₀' → M₀
zero : f 0 = 0
one : f 1 = 1
rw : ¬Eq.{u_1 + 1} (α := M₀) 0 1
⊢ ¬f 0 = f 1

Tactic:
rw [zero, one]
-- Module: Mathlib.Algebra.GroupWithZero.NeZero
Goal:
M₀ : Type u_1
M₀' : Type u_2
inst : MulZeroOneClass M₀
inst_1 : Nontrivial M₀
inst_2 : Zero M₀'
inst_3 : One M₀'
f : M₀' → M₀
zero : f 0 = 0
one : f 1 = 1
⊢ ¬Eq.{u_1 + 1} (α := M₀) 0 1

Tactic:
zero_ne_one

Premises used: zero_ne_one
-- Module: Mathlib.Algebra.GroupWithZero.NeZero
Goal:
M₀ : Type u_1
M₀' : Type u_2
inst : MulZeroOneClass M₀
inst_1 : Nontrivial M₀
inst_2 : Zero M₀'
inst_3 : One M₀'
f : M₀' → M₀
zero : f 0 = 0
one : f 1 = 1
⊢ ¬Eq.{u_1 + 1} (α := M₀) 0 1

Tactic:
exact zero_ne_one

Premises used: zero_ne_one
-- Module: Mathlib.Algebra.GroupWithZero.NeZero
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
h : a ≠ 0
a_eq_0 : a⁻¹ = 0
⊢ False

Tactic:
simpa [a_eq_0] using mul_inv_cancel₀ h

Premises used: mul_inv_cancel₀
-- Module: Mathlib.Algebra.GroupWithZero.NeZero
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
h : a ≠ 0
⊢ a⁻¹ * a = a⁻¹ * a * a⁻¹ * a⁻¹⁻¹

Tactic:
simp [inv_ne_zero h]

Premises used: inv_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.NeZero
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
h : a ≠ 0
⊢ a⁻¹ * a * a⁻¹ * a⁻¹⁻¹ = a⁻¹ * a⁻¹⁻¹

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

Tactic:
simp [inv_ne_zero h]

Premises used: inv_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
S : Type u_2
inst : MonoidWithZero M₀
inst_1 : SetLike S M₀
inst_2 : SubmonoidClass S M₀
s : S
x : ↥s
hx : Irreducible x
h : (↑x : M₀) = 0
a : (↑x : M₀) = (↑(x * x) : M₀)
⊢ x = x * x

Tactic:
ext
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
S : Type u_2
inst : MonoidWithZero M₀
inst_1 : SetLike S M₀
inst_2 : SubmonoidClass S M₀
s : S
x : ↥s
hx : Irreducible x
h : (↑x : M₀) = 0
⊢ (↑x : M₀) = (↑(x * x) : M₀)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
S : Type u_2
inst : MonoidWithZero M₀
inst_1 : SetLike S M₀
inst_2 : SubmonoidClass S M₀
s : S
x : ↥s
hx : Irreducible x
h : (↑x : M₀) = 0
⊢ IsUnit x

Tactic:
simpa using hx.2 (a := x) (b := x) (by ext; simp [h])

Premises used: Irreducible.isUnit_or_isUnit
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
x : M₀
⊢ Membership.mem (γ := Set M₀) {x : M₀ | ∀ (y : M₀), x * y = 0 → y = 0} 1

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
x : M₀
⊢ Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsLeft M₀) x ↔ ∀ (y : M₀), x * y = 0 → y = 0

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
x : M₀
⊢ x ∉ nonZeroDivisorsLeft M₀ ↔ Set.Nonempty.{u_1} (α := M₀) {y : M₀ | x * y = 0 ∧ y ≠ 0}

Tactic:
simpa [mem_nonZeroDivisorsLeft_iff] using Set.nonempty_def.symm

Premises used: Set.nonempty_def, mem_nonZeroDivisorsLeft_iff, Iff.symm
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
x : M₀
⊢ Membership.mem (γ := Set M₀) {x : M₀ | ∀ (y : M₀), y * x = 0 → y = 0} 1

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
x : M₀
⊢ Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) x ↔ ∀ (y : M₀), y * x = 0 → y = 0

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
x : M₀
⊢ x ∉ nonZeroDivisorsRight M₀ ↔ Set.Nonempty.{u_1} (α := M₀) {y : M₀ | y * x = 0 ∧ y ≠ 0}

Tactic:
simpa [mem_nonZeroDivisorsRight_iff] using Set.nonempty_def.symm

Premises used: Set.nonempty_def, Iff.symm, mem_nonZeroDivisorsRight_iff
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : CommMonoidWithZero M₀
h :
  ∀ (x : M₀),
    Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsLeft M₀) x ↔
      Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) x
⊢ Eq (α := Submonoid M₀) (nonZeroDivisorsLeft M₀) (nonZeroDivisorsRight M₀)

Tactic:
ext x
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : CommMonoidWithZero M₀
x : M₀
⊢ Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsLeft M₀) x ↔
    Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) x

Tactic:
simp [mul_comm x]

Premises used: mul_comm
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
h : ∀ (x : M₀), x ∈ (↑(nonZeroDivisorsLeft M₀) : Set M₀) ↔ Membership.mem (γ := Set M₀) {x : M₀ | x ≠ 0} x
⊢ (↑(nonZeroDivisorsLeft M₀) : Set M₀) = {x : M₀ | x ≠ 0}

Tactic:
ext x
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
x : M₀
h : (∀ (y : M₀), x = 0 ∨ y = 0 → y = 0) ↔ x ≠ 0
⊢ x ∈ (↑(nonZeroDivisorsLeft M₀) : Set M₀) ↔ Membership.mem (γ := Set M₀) {x : M₀ | x ≠ 0} x

Tactic:
simp only [SetLike.mem_coe, mem_nonZeroDivisorsLeft_iff, mul_eq_zero, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, mul_eq_zero, mem_nonZeroDivisorsLeft_iff, SetLike.mem_coe
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
x : M₀
hx : x ≠ 0
y : M₀
hx' : x = 0 ∨ y = 0
⊢ y = 0

Tactic:
simp_all
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
x : M₀
h : ∀ (h : ∀ (y : M₀), x = 0 ∨ y = 0 → y = 0), x ≠ 0
⊢ (∀ (y : M₀), x = 0 ∨ y = 0 → y = 0) ↔ x ≠ 0

Tactic:
refine ⟨fun h ↦ ?_, fun hx y hx' ↦ by simp_all⟩
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
x : M₀
h : ∀ (y : M₀), x = 0 ∨ y = 0 → y = 0
h₁ : ∀ (h : x = 0), ∃ (y : M₀), (x = 0 ∨ y = 0) ∧ y ≠ 0
⊢ x ≠ 0

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
x : M₀
h : x = 0
⊢ ∃ (y : M₀), (x = 0 ∨ y = 0) ∧ y ≠ 0

Tactic:
⟨1, Or.inl h, one_ne_zero⟩

Premises used: And.intro, Exists.intro, Or.inl, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
x : M₀
h : x = 0
⊢ ∃ (y : M₀), (x = 0 ∨ y = 0) ∧ y ≠ 0

Tactic:
exact ⟨1, Or.inl h, one_ne_zero⟩
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
h : ∀ (x : M₀), x ∈ (↑(nonZeroDivisorsRight M₀) : Set M₀) ↔ Membership.mem (γ := Set M₀) {x : M₀ | x ≠ 0} x
⊢ (↑(nonZeroDivisorsRight M₀) : Set M₀) = {x : M₀ | x ≠ 0}

Tactic:
ext x
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
x : M₀
h : (∀ (a : M₀), x = 0 → a = 0) ↔ x ≠ 0
⊢ x ∈ (↑(nonZeroDivisorsRight M₀) : Set M₀) ↔ Membership.mem (γ := Set M₀) {x : M₀ | x ≠ 0} x

Tactic:
simp only [SetLike.mem_coe, mem_nonZeroDivisorsRight_iff, mul_eq_zero, forall_eq_or_imp, true_and,
    Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, forall_eq_or_imp, mul_eq_zero, SetLike.mem_coe, true_and, mem_nonZeroDivisorsRight_iff
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
x : M₀
hx : x ≠ 0
y : M₀
hx' : x = 0
⊢ y = 0

Tactic:
contradiction
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
x : M₀
h : ∀ (h : ∀ (a : M₀), x = 0 → a = 0), x ≠ 0
⊢ (∀ (a : M₀), x = 0 → a = 0) ↔ x ≠ 0

Tactic:
refine ⟨fun h ↦ ?_, fun hx y hx' ↦ by contradiction⟩
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
x : M₀
h : ∀ (a : M₀), x = 0 → a = 0
h₁ : ∀ (h : x = 0), ∃ (a : M₀), x = 0 ∧ a ≠ 0
⊢ x ≠ 0

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
x : M₀
h : x = 0
⊢ ∃ (a : M₀), x = 0 ∧ a ≠ 0

Tactic:
⟨1, h, one_ne_zero⟩

Premises used: And.intro, Exists.intro, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
x : M₀
h : x = 0
⊢ ∃ (a : M₀), x = 0 ∧ a ≠ 0

Tactic:
exact ⟨1, h, one_ne_zero⟩
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
⊢ Eq (α := Submonoid M₀) (nonZeroDivisorsLeft M₀) (nonZeroSMulDivisors M₀ M₀)

Tactic:
rfl

Premises used: nonZeroSMulDivisors, setOf, rfl
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
r : M₀
⊢ Membership.mem (γ := Submonoid M₀) M₀⁰ r ↔ (∀ (x : M₀), r * x = 0 → x = 0) ∧ ∀ (x : M₀), x * r = 0 → x = 0

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
r : M₀
⊢ Membership.mem (γ := Submonoid M₀) M₀⁰ r ↔
    Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsLeft M₀) r ∧
      Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) r

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
r : M₀
⊢ r ∉ M₀⁰ ↔
    Set.Nonempty.{u_2} (α := M₀) {s : M₀ | r * s = 0 ∧ s ≠ 0} ∨
      Set.Nonempty.{u_2} (α := M₀) {s : M₀ | s * r = 0 ∧ s ≠ 0}

Tactic:
simp [-not_and, not_and_or, mem_nonZeroDivisors_iff, Set.nonempty_def]

Premises used: mem_nonZeroDivisors_iff, Set.nonempty_def, not_and_or, not_and
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
r x : M₀
hr : Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsLeft M₀) r
⊢ x = 0 → r * x = 0

Tactic:
simp +contextual
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
r x : M₀
hr : Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) r
⊢ x = 0 → x * r = 0

Tactic:
simp +contextual
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
r x : M₀
hr : Membership.mem (γ := Submonoid M₀) M₀⁰ r
⊢ x * r = 0 ↔ x = 0

Tactic:
mul_right_mem_nonZeroDivisorsRight_eq_zero_iff hr.2

Premises used: mul_right_mem_nonZeroDivisorsRight_eq_zero_iff, And.right