awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.InjSurj (goal)
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
⊢ f 0⁻¹ = f 0
have rw₂ : Eq.{u_2 + 1} (α := G₀) 0 0
Tactic: rw [inv, zero, inv_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.InjSurj (goal)
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
⊢ f (x * x⁻¹) = f 1
have rw : f (x * x⁻¹) = 1
Tactic: rw [one, mul, inv, mul_inv_cancel₀ ((hf.ne_iff' zero).2 hx)]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.InjSurj (goal)
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
⊢ f (x * x⁻¹) = f 1
have rw₁ : f x * f x⁻¹ = 1
Tactic: rw [one, mul, inv, mul_inv_cancel₀ ((hf.ne_iff' zero).2 hx)]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.InjSurj (goal)
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
⊢ f (x * x⁻¹) = f 1
have rw₂ : f x * (f x)⁻¹ = 1
Tactic: rw [one, mul, inv, mul_inv_cancel₀ ((hf.ne_iff' zero).2 hx)]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.InjSurj (goal)
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
⊢ f (x * x⁻¹) = f 1
have rw₃ : Eq.{u_2 + 1} (α := G₀) 1 1
Tactic: rw [one, mul, inv, mul_inv_cancel₀ ((hf.ne_iff' zero).2 hx)]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.InjSurj (goal)
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
⊢ Eq.{u_4 + 1} (α := G₀') 0⁻¹ 0
have rw : (f 0)⁻¹ = f 0
Tactic: rw [← zero, ← inv, inv_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.InjSurj (goal)
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
⊢ Eq.{u_4 + 1} (α := G₀') 0⁻¹ 0
have rw₁ : f 0⁻¹ = f 0
Tactic: rw [← zero, ← inv, inv_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.InjSurj (goal)
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
⊢ Eq.{u_4 + 1} (α := G₀') 0⁻¹ 0
have rw₂ : f 0 = f 0
Tactic: rw [← zero, ← inv, inv_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.InjSurj (goal)
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
⊢ f x * (f x)⁻¹ = 1
have rw : f x * f x⁻¹ = 1
Tactic: rw [← inv, ← mul, mul_inv_cancel₀ (mt (congr_arg f) fun h ↦ hx (h.trans zero)), one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.InjSurj (goal)
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
⊢ f x * (f x)⁻¹ = 1
have rw₁ : f (x * x⁻¹) = 1
Tactic: rw [← inv, ← mul, mul_inv_cancel₀ (mt (congr_arg f) fun h ↦ hx (h.trans zero)), one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.InjSurj (goal)
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
⊢ f x * (f x)⁻¹ = 1
have rw₃ : Eq.{u_4 + 1} (α := G₀') 1 1
Tactic: rw [← inv, ← mul, mul_inv_cancel₀ (mt (congr_arg f) fun h ↦ hx (h.trans zero)), one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NeZero (goal)
Goal:
M₀ : Type u_1
M₀' : Type u_2
inst : MulZeroOneClass M₀
inst_1 : Nontrivial M₀
h : Eq.{u_1 + 1} (α := M₀) 1 0
⊢ False
have rcases : ∀ (x y : M₀) (hx : x ≠ y), False
Tactic: rcases exists_pair_ne M₀ with ⟨x, y, hx⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NeZero (goal)
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
⊢ False
have apply : x = y
Tactic: apply hx
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NeZero (goal)
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 = 1 * x
have rw : x = x
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NeZero (goal)
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
⊢ 1 * x = 0
have rw : 0 * x = 0
Tactic: rw [h, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NeZero (goal)
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
⊢ 1 * x = 0
have rw₁ : Eq.{u_1 + 1} (α := M₀) 0 0
Tactic: rw [h, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NeZero (goal)
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
⊢ 0 = 1 * y
have rw : 0 = 0 * y
Tactic: rw [h, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NeZero (goal)
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
⊢ 0 = 1 * y
have rw₁ : Eq.{u_1 + 1} (α := M₀) 0 0
Tactic: rw [h, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NeZero (goal)
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
⊢ 1 * y = y
have rw : y = y
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NeZero (goal)
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 = y
have x₁ : x = 1 * x
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]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NeZero (goal)
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 = y
have x₂ : 1 * x = 0
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]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NeZero (goal)
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 = y
have x₃ : 0 = 1 * 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]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NeZero (goal)
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 = y
have x₄ : 1 * y = 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]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NeZero (goal)
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
⊢ ¬f 0 = f 1
have rw : ¬Eq.{u_1 + 1} (α := M₀) 0 1
Tactic: rw [zero, one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
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 = x * x
have a : (↑x : M₀) = (↑(x * x) : M₀)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_2
inst : CommMonoidWithZero M₀
⊢ Eq (α := Submonoid M₀) (nonZeroDivisorsLeft M₀) (nonZeroDivisorsRight M₀)
have h : ∀ (x : M₀),
  Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsLeft M₀) x ↔
    Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
⊢ (↑(nonZeroDivisorsLeft M₀) : Set M₀) = {x : M₀ | x ≠ 0}
have h : ∀ (x : M₀), x ∈ (↑(nonZeroDivisorsLeft M₀) : Set M₀) ↔ Membership.mem (γ := Set M₀) {x : M₀ | x ≠ 0} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
x : M₀
⊢ x ∈ (↑(nonZeroDivisorsLeft M₀) : Set M₀) ↔ Membership.mem (γ := Set M₀) {x : M₀ | x ≠ 0} x
have h : (∀ (y : M₀), x = 0 ∨ y = 0 → y = 0) ↔ x ≠ 0
Tactic: simp only [SetLike.mem_coe, mem_nonZeroDivisorsLeft_iff, mul_eq_zero, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
x : M₀
⊢ (∀ (y : M₀), x = 0 ∨ y = 0 → y = 0) ↔ x ≠ 0
have h : ∀ (h : ∀ (y : M₀), x = 0 ∨ y = 0 → y = 0), x ≠ 0
Tactic: refine ⟨fun h ↦ ?_, fun hx y hx' ↦ by simp_all⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
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
have h₁ : ∀ (h : x = 0), ∃ (y : M₀), (x = 0 ∨ y = 0) ∧ y ≠ 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
⊢ (↑(nonZeroDivisorsRight M₀) : Set M₀) = {x : M₀ | x ≠ 0}
have h : ∀ (x : M₀), x ∈ (↑(nonZeroDivisorsRight M₀) : Set M₀) ↔ Membership.mem (γ := Set M₀) {x : M₀ | x ≠ 0} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
x : M₀
⊢ x ∈ (↑(nonZeroDivisorsRight M₀) : Set M₀) ↔ Membership.mem (γ := Set M₀) {x : M₀ | x ≠ 0} x
have h : (∀ (a : M₀), x = 0 → a = 0) ↔ x ≠ 0
Tactic: simp only [SetLike.mem_coe, mem_nonZeroDivisorsRight_iff, mul_eq_zero, forall_eq_or_imp, true_and,
    Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
x : M₀
⊢ (∀ (a : M₀), x = 0 → a = 0) ↔ x ≠ 0
have h : ∀ (h : ∀ (a : M₀), x = 0 → a = 0), x ≠ 0
Tactic: refine ⟨fun h ↦ ?_, fun hx y hx' ↦ by contradiction⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
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
have h₁ : ∀ (h : x = 0), ∃ (a : M₀), x = 0 ∧ a ≠ 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_4
S : Type u_5
F : Type u_6
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero S
inst_2 : EquivLike F M₀ S
inst_3 : MulEquivClass F M₀ S
h_1 : F
h : M₀ ≃* S := (↑h_1 : M₀ ≃* S)
⊢ Eq (α := Submonoid S) (Submonoid.map h_1 M₀⁰) S⁰
have change : Eq (α := Submonoid S) (Submonoid.map h M₀⁰) S⁰
Tactic: change Submonoid.map h _ = _
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_4
S : Type u_5
F : Type u_6
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero S
inst_2 : EquivLike F M₀ S
inst_3 : MulEquivClass F M₀ S
h_1 : F
h : M₀ ≃* S := (↑h_1 : M₀ ≃* S)
⊢ Eq (α := Submonoid S) (Submonoid.map h M₀⁰) S⁰
have h₁ : ∀ (x : S), Membership.mem (γ := Submonoid S) (Submonoid.map h M₀⁰) x ↔ Membership.mem (γ := Submonoid S) S⁰ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_4
S : Type u_5
F : Type u_6
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero S
inst_2 : EquivLike F M₀ S
inst_3 : MulEquivClass F M₀ S
h_1 : F
h : M₀ ≃* S := (↑h_1 : M₀ ≃* S)
x : S
⊢ Membership.mem (γ := Submonoid S) (Submonoid.map h M₀⁰) x ↔ Membership.mem (γ := Submonoid S) S⁰ x
have h₁ : Membership.mem (γ := Submonoid S) (Submonoid.comap h.symm M₀⁰) x ↔ Membership.mem (γ := Submonoid S) S⁰ x
Tactic: simp_rw [Submonoid.map_equiv_eq_comap_symm, Submonoid.mem_comap, mem_nonZeroDivisors_iff,
    ← h.symm.forall_congr_right, h.symm.toEquiv_eq_coe, h.symm.coe_toEquiv, ← map_mul,
    map_eq_zero_iff _ h.symm.injective]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_4
S : Type u_5
F : Type u_6
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero S
inst_2 : EquivLike F M₀ S
inst_3 : MulEquivClass F M₀ S
h_1 : F
h : M₀ ≃* S := (↑h_1 : M₀ ≃* S)
x : S
h₁ : Membership.mem (γ := Submonoid S) (Submonoid.comap h.symm M₀⁰) x ↔ Membership.mem (γ := Submonoid S) S⁰ x
⊢ Membership.mem (γ := Submonoid S) (Submonoid.map h M₀⁰) x ↔ Membership.mem (γ := Submonoid S) S⁰ x
have h₂ : Membership.mem (α := M₀) (γ := Submonoid M₀) M₀⁰ ((h.symm : (a : S) → M₀) x : M₀) ↔
  Membership.mem (γ := Submonoid S) S⁰ x
Tactic: simp_rw [Submonoid.map_equiv_eq_comap_symm, Submonoid.mem_comap, mem_nonZeroDivisors_iff,
    ← h.symm.forall_congr_right, h.symm.toEquiv_eq_coe, h.symm.coe_toEquiv, ← map_mul,
    map_eq_zero_iff _ h.symm.injective]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_4
S : Type u_5
F : Type u_6
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero S
inst_2 : EquivLike F M₀ S
inst_3 : MulEquivClass F M₀ S
h_1 : F
h : M₀ ≃* S := (↑h_1 : M₀ ≃* S)
x : S
h₁ : Membership.mem (γ := Submonoid S) (Submonoid.comap h.symm M₀⁰) x ↔ Membership.mem (γ := Submonoid S) S⁰ x
h₂ :
  Membership.mem (α := M₀) (γ := Submonoid M₀) M₀⁰ ((h.symm : (a : S) → M₀) x : M₀) ↔
    Membership.mem (γ := Submonoid S) S⁰ x
⊢ Membership.mem (γ := Submonoid S) (Submonoid.map h M₀⁰) x ↔ Membership.mem (γ := Submonoid S) S⁰ x
have h₃ : ((∀ (x_1 : M₀), HMul.hMul (α := M₀) ((h.symm : (a : S) → M₀) x : M₀) x_1 = 0 → x_1 = 0) ∧
    ∀ (x_1 : M₀), HMul.hMul (β := M₀) x_1 ((h.symm : (a : S) → M₀) x : M₀) = 0 → x_1 = 0) ↔
  (∀ (x_1 : S), x * x_1 = 0 → x_1 = 0) ∧ ∀ (x_1 : S), x_1 * x = 0 → x_1 = 0
Tactic: simp_rw [Submonoid.map_equiv_eq_comap_symm, Submonoid.mem_comap, mem_nonZeroDivisors_iff,
    ← h.symm.forall_congr_right, h.symm.toEquiv_eq_coe, h.symm.coe_toEquiv, ← map_mul,
    map_eq_zero_iff _ h.symm.injective]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_4
S : Type u_5
F : Type u_6
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero S
inst_2 : EquivLike F M₀ S
inst_3 : MulEquivClass F M₀ S
h_1 : F
h : M₀ ≃* S := (↑h_1 : M₀ ≃* S)
x : S
h₁ : Membership.mem (γ := Submonoid S) (Submonoid.comap h.symm M₀⁰) x ↔ Membership.mem (γ := Submonoid S) S⁰ x
h₂ :
  Membership.mem (α := M₀) (γ := Submonoid M₀) M₀⁰ ((h.symm : (a : S) → M₀) x : M₀) ↔
    Membership.mem (γ := Submonoid S) S⁰ x
h₃ :
  ((∀ (x_1 : M₀), HMul.hMul (α := M₀) ((h.symm : (a : S) → M₀) x : M₀) x_1 = 0 → x_1 = 0) ∧
      ∀ (x_1 : M₀), HMul.hMul (β := M₀) x_1 ((h.symm : (a : S) → M₀) x : M₀) = 0 → x_1 = 0) ↔
    (∀ (x_1 : S), x * x_1 = 0 → x_1 = 0) ∧ ∀ (x_1 : S), x_1 * x = 0 → x_1 = 0
⊢ Membership.mem (γ := Submonoid S) (Submonoid.map h M₀⁰) x ↔ Membership.mem (γ := Submonoid S) S⁰ x
have h₄ : ((∀ (a : S),
      HMul.hMul (α := M₀) (β := M₀) ((h.symm : (a : S) → M₀) x : M₀) ((h.symm.toEquiv : (a : S) → M₀) a : M₀) = 0 →
        Eq.{u_4 + 1} (α := M₀) ((h.symm.toEquiv : (a : S) → M₀) a : M₀) (0 : M₀)) ∧
    ∀ (a : S),
      HMul.hMul (α := M₀) (β := M₀) ((h.symm.toEquiv : (a : S) → M₀) a : M₀) ((h.symm : (a : S) → M₀) x : M₀) = 0 →
        Eq.{u_4 + 1} (α := M₀) ((h.symm.toEquiv : (a : S) → M₀) a : M₀) (0 : M₀)) ↔
  (∀ (x_1 : S), x * x_1 = 0 → x_1 = 0) ∧ ∀ (x_1 : S), x_1 * x = 0 → x_1 = 0
Tactic: simp_rw [Submonoid.map_equiv_eq_comap_symm, Submonoid.mem_comap, mem_nonZeroDivisors_iff,
    ← h.symm.forall_congr_right, h.symm.toEquiv_eq_coe, h.symm.coe_toEquiv, ← map_mul,
    map_eq_zero_iff _ h.symm.injective]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_4
S : Type u_5
F : Type u_6
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero S
inst_2 : EquivLike F M₀ S
inst_3 : MulEquivClass F M₀ S
h_1 : F
h : M₀ ≃* S := (↑h_1 : M₀ ≃* S)
x : S
h₁ : Membership.mem (γ := Submonoid S) (Submonoid.comap h.symm M₀⁰) x ↔ Membership.mem (γ := Submonoid S) S⁰ x
h₂ :
  Membership.mem (α := M₀) (γ := Submonoid M₀) M₀⁰ ((h.symm : (a : S) → M₀) x : M₀) ↔
    Membership.mem (γ := Submonoid S) S⁰ x
h₃ :
  ((∀ (x_1 : M₀), HMul.hMul (α := M₀) ((h.symm : (a : S) → M₀) x : M₀) x_1 = 0 → x_1 = 0) ∧
      ∀ (x_1 : M₀), HMul.hMul (β := M₀) x_1 ((h.symm : (a : S) → M₀) x : M₀) = 0 → x_1 = 0) ↔
    (∀ (x_1 : S), x * x_1 = 0 → x_1 = 0) ∧ ∀ (x_1 : S), x_1 * x = 0 → x_1 = 0
h₄ :
  ((∀ (a : S),
        HMul.hMul (α := M₀) (β := M₀) ((h.symm : (a : S) → M₀) x : M₀) ((h.symm.toEquiv : (a : S) → M₀) a : M₀) = 0 →
          Eq.{u_4 + 1} (α := M₀) ((h.symm.toEquiv : (a : S) → M₀) a : M₀) (0 : M₀)) ∧
      ∀ (a : S),
        HMul.hMul (α := M₀) (β := M₀) ((h.symm.toEquiv : (a : S) → M₀) a : M₀) ((h.symm : (a : S) → M₀) x : M₀) = 0 →
          Eq.{u_4 + 1} (α := M₀) ((h.symm.toEquiv : (a : S) → M₀) a : M₀) (0 : M₀)) ↔
    (∀ (x_1 : S), x * x_1 = 0 → x_1 = 0) ∧ ∀ (x_1 : S), x_1 * x = 0 → x_1 = 0
⊢ Membership.mem (γ := Submonoid S) (Submonoid.map h M₀⁰) x ↔ Membership.mem (γ := Submonoid S) S⁰ x
have h₅ : ((∀ (a : S),
      HMul.hMul (α := M₀) (β := M₀) ((h.symm : (a : S) → M₀) x : M₀) (((↑h.symm : S ≃ M₀) : (a : S) → M₀) a : M₀) = 0 →
        Eq.{u_4 + 1} (α := M₀) (((↑h.symm : S ≃ M₀) : (a : S) → M₀) a : M₀) (0 : M₀)) ∧
    ∀ (a : S),
      HMul.hMul (α := M₀) (β := M₀) (((↑h.symm : S ≃ M₀) : (a : S) → M₀) a : M₀) ((h.symm : (a : S) → M₀) x : M₀) = 0 →
        Eq.{u_4 + 1} (α := M₀) (((↑h.symm : S ≃ M₀) : (a : S) → M₀) a : M₀) (0 : M₀)) ↔
  (∀ (x_1 : S), x * x_1 = 0 → x_1 = 0) ∧ ∀ (x_1 : S), x_1 * x = 0 → x_1 = 0
Tactic: simp_rw [Submonoid.map_equiv_eq_comap_symm, Submonoid.mem_comap, mem_nonZeroDivisors_iff,
    ← h.symm.forall_congr_right, h.symm.toEquiv_eq_coe, h.symm.coe_toEquiv, ← map_mul,
    map_eq_zero_iff _ h.symm.injective]