awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
c : ↥M₀⁰
⊢ x * (↑c : M₀) = 0 ↔ x = 0

Tactic:
mul_right_mem_nonZeroDivisors_eq_zero_iff c.prop

Premises used: mul_right_mem_nonZeroDivisors_eq_zero_iff, Subtype.prop
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
hx : IsUnit x
⊢ Membership.mem (γ := Submonoid M₀) M₀⁰ x

Tactic:
⟨fun _ ↦ hx.mul_right_eq_zero.mp, fun _ ↦ hx.mul_left_eq_zero.mp⟩

Premises used: Set.Mem, setOf, IsUnit.mul_left_eq_zero, IsUnit.mul_right_eq_zero, Set.inter, And.intro, Iff.mp
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
⊢ LE.le (α := Submonoid M₀) (IsUnit.submonoid M₀) M₀⁰

Tactic:
fun _ ↦ (·.mem_nonZeroDivisors)

Premises used: Set.Mem, IsUnit.mem_nonZeroDivisors
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y : M₀
hx : Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsLeft M₀) x
hy : Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsLeft M₀) y
⊢ Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsLeft M₀) (x * y)

Tactic:
Submonoid.mul_mem _ hx hy

Premises used: Submonoid.mul_mem, Set.Mem, setOf
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y : M₀
hx : Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) x
hy : Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) y
⊢ Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) (x * y)

Tactic:
Submonoid.mul_mem _ hx hy

Premises used: Submonoid.mul_mem, Set.Mem, setOf
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y : M₀
hx : Membership.mem (γ := Submonoid M₀) M₀⁰ x
hy : Membership.mem (γ := Submonoid M₀) M₀⁰ y
⊢ Membership.mem (γ := Submonoid M₀) M₀⁰ (x * y)

Tactic:
mem_nonZeroDivisors_iff'.mpr ⟨Submonoid.mul_mem _ hx.1 hy.1, Submonoid.mul_mem _ hx.2 hy.2⟩

Premises used: Iff.mpr, Submonoid.mul_mem, mem_nonZeroDivisors_iff', And.right, And.left, And.intro
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
⊢ 0 ∉ nonZeroDivisorsLeft M₀

Tactic:
fun h ↦ one_ne_zero <| h 1 <| zero_mul _

Premises used: MulZeroClass.zero_mul, one_ne_zero, OfNat.ofNat, Not
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
⊢ 0 ∉ nonZeroDivisorsRight M₀

Tactic:
fun h ↦ one_ne_zero <| h 1 <| mul_zero _

Premises used: MulZeroClass.mul_zero, one_ne_zero, OfNat.ofNat, Not
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
⊢ 0 ∉ M₀⁰

Tactic:
fun h ↦ zero_notMem_nonZeroDivisorsLeft h.1

Premises used: And.left, zero_notMem_nonZeroDivisorsLeft, Not
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
inst_1 : Nontrivial M₀
hx : Membership.mem (γ := Submonoid M₀) M₀⁰ x
⊢ x ≠ 0

Tactic:
ne_of_mem_of_not_mem hx zero_notMem_nonZeroDivisors

Premises used: ne_of_mem_of_not_mem, zero_notMem_nonZeroDivisors
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
x : ↥M₀⁰
⊢ (↑x : M₀) ≠ 0

Tactic:
nonZeroDivisors.ne_zero x.2

Premises used: nonZeroDivisors.ne_zero, Subtype.property
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero M₀'
r x y : M₀
inst_2 : Nontrivial M₀
inst_3 : IsLeftCancelMulZero M₀
z x_1 x_2 : ↥M₀⁰
h : Eq.{u_2 + 1} (α := ↥M₀⁰) ((fun (x : ↥M₀⁰) ↦ z * x) x_1) ((fun (x : ↥M₀⁰) ↦ z * x) x_2)
⊢ (↑z : M₀) * (↑x_1 : M₀) = (↑z : M₀) * (↑x_2 : M₀)

Tactic:
simpa only [Subtype.ext_iff, Submonoid.coe_mul] using h

Premises used: Subtype.ext_iff, Submonoid.coe_mul
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero M₀'
r x y : M₀
inst_2 : Nontrivial M₀
inst_3 : IsRightCancelMulZero M₀
z x_1 x_2 : ↥M₀⁰
h : Eq.{u_2 + 1} (α := ↥M₀⁰) ((fun (x : ↥M₀⁰) ↦ x * z) x_1) ((fun (x : ↥M₀⁰) ↦ x * z) x_2)
⊢ (↑x_1 : M₀) * (↑z : M₀) = (↑x_2 : M₀) * (↑z : M₀)

Tactic:
simpa only [Subtype.ext_iff, Submonoid.coe_mul] using h

Premises used: Subtype.ext_iff, Submonoid.coe_mul
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y : M₀
inst_1 : NoZeroDivisors M₀
hx : x ≠ 0
hxy : y * x = 0
⊢ y = 0

Tactic:
Or.resolve_right (eq_zero_or_eq_zero_of_mul_eq_zero hxy) hx

Premises used: Or.resolve_right, NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y : M₀
inst_1 : NoZeroDivisors M₀
hx : x ≠ 0
hxy : x * y = 0
⊢ y = 0

Tactic:
Or.resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero hxy) hx

Premises used: Or.resolve_left, NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
inst_1 : NoZeroDivisors M₀
hx : x ≠ 0
⊢ Membership.mem (γ := Submonoid M₀) M₀⁰ x

Tactic:
⟨fun _ ↦ eq_zero_of_ne_zero_of_mul_left_eq_zero hx,
   fun _ ↦ eq_zero_of_ne_zero_of_mul_right_eq_zero hx⟩

Premises used: Set.Mem, setOf, Set.inter, eq_zero_of_ne_zero_of_mul_right_eq_zero, eq_zero_of_ne_zero_of_mul_left_eq_zero, And.intro
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
⊢ Membership.mem (γ := Submonoid M₀) M₀⁰ x ↔ x ≠ 0

Tactic:
⟨nonZeroDivisors.ne_zero, mem_nonZeroDivisors_of_ne_zero⟩

Premises used: nonZeroDivisors.ne_zero, Iff.intro, mem_nonZeroDivisors_of_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
S : Submonoid M₀
hS : 0 ∉ S
hx : 0 ∈ S
⊢ False

Tactic:
hS hx
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
S : Submonoid M₀
hS : 0 ∉ S
hx : 0 ∈ S
⊢ False

Tactic:
exact hS hx
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
inst_1 : NoZeroDivisors M₀
hx : x ≠ 0
⊢ LE.le (α := Submonoid M₀) (Submonoid.powers x) M₀⁰

Tactic:
le_nonZeroDivisors_of_noZeroDivisors fun h ↦ hx (h.recOn fun _ ↦ eq_zero_of_pow_eq_zero)

Premises used: Set.Mem, le_nonZeroDivisors_of_noZeroDivisors, Exists.recOn
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
r : M₀
h : IsLeftRegular r
⊢ Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsLeft M₀) r

Tactic:
fun _x hx ↦ h.mul_left_eq_zero_iff.mp hx

Premises used: IsLeftRegular.mul_left_eq_zero_iff, Set.Mem, setOf, Iff.mp
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
r : M₀
h : IsRightRegular r
⊢ Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) r

Tactic:
fun _x hx ↦ h.mul_right_eq_zero_iff.mp hx

Premises used: Set.Mem, IsRightRegular.mul_right_eq_zero_iff, setOf, Iff.mp
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
r : M₀
h : IsRegular r
⊢ Membership.mem (γ := Submonoid M₀) M₀⁰ r

Tactic:
⟨h.1.mem_nonZeroDivisorsLeft, h.2.mem_nonZeroDivisorsRight⟩

Premises used: Set.Mem, setOf, IsRegular.right, Set.inter, IsLeftRegular.mem_nonZeroDivisorsLeft, IsRightRegular.mem_nonZeroDivisorsRight, And.intro, IsRegular.left
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
⊢ NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsLeft M₀) x

Tactic:
noZeroDivisors_iff_right_eq_zero_of_mul

Premises used: Set.Mem, setOf, noZeroDivisors_iff_right_eq_zero_of_mul
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
⊢ NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) x

Tactic:
noZeroDivisors_iff_left_eq_zero_of_mul

Premises used: Set.Mem, setOf, noZeroDivisors_iff_left_eq_zero_of_mul
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
⊢ NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → Membership.mem (γ := Submonoid M₀) M₀⁰ x

Tactic:
noZeroDivisors_iff_eq_zero_of_mul

Premises used: Set.Mem, setOf, Set.inter, noZeroDivisors_iff_eq_zero_of_mul
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
M : Type u_4
inst_1 : Zero M
inst_2 : MulActionWithZero M₀ M
m₀ : M₀
h : IsSMulRegular M m₀
⊢ Membership.mem (γ := Submonoid M₀) (nonZeroSMulDivisors M₀ M) m₀

Tactic:
fun _ ↦ h.right_eq_zero_of_smul

Premises used: Set.Mem, setOf, IsSMulRegular.right_eq_zero_of_smul
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
M : Type u_4
inst_1 : AddGroup M
inst_2 : DistribMulAction M₀ M
m₀ : M₀
⊢ IsSMulRegular M m₀ ↔ Membership.mem (γ := Submonoid M₀) (nonZeroSMulDivisors M₀ M) m₀

Tactic:
isSMulRegular_iff_right_eq_zero_of_smul

Premises used: Set.Mem, setOf, isSMulRegular_iff_right_eq_zero_of_smul
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero M₀'
inst_2 : FunLike F M₀ M₀'
inst_3 : Nontrivial M₀
inst_4 : ZeroHomClass F M₀ M₀'
g : F
hg : Injective.{u_2 + 1, u_3 + 1} (α := M₀) (β := M₀') (⇑g : (a : M₀) → M₀')
x : M₀
h : Membership.mem (γ := Submonoid M₀) M₀⁰ x
⊢ Ne.{u_3 + 1} (α := M₀') ((g : (a : M₀) → M₀') x : M₀') (0 : M₀')

Tactic:
fun h0 ↦
  one_ne_zero (h.2 1 ((one_mul x).symm ▸ hg (h0.trans (map_zero g).symm)))

Premises used: Eq.rec, map_zero, And.right, one_ne_zero, OfNat.ofNat, Eq.symm, Not, one_mul, Eq.trans
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero M₀'
inst_2 : FunLike F M₀ M₀'
inst_3 : Nontrivial M₀
inst_4 : NoZeroDivisors M₀'
inst_5 : ZeroHomClass F M₀ M₀'
g : F
hg : Injective.{u_2 + 1, u_3 + 1} (α := M₀) (β := M₀') (⇑g : (a : M₀) → M₀')
x : M₀
h : Membership.mem (γ := Submonoid M₀) M₀⁰ x
⊢ Membership.mem (α := M₀') (γ := Submonoid M₀') M₀'⁰ ((g : (a : M₀) → M₀') x : M₀')

Tactic:
⟨fun _ ↦ eq_zero_of_ne_zero_of_mul_left_eq_zero (map_ne_zero_of_mem_nonZeroDivisors g hg h),
    fun _ ↦ eq_zero_of_ne_zero_of_mul_right_eq_zero (map_ne_zero_of_mem_nonZeroDivisors g hg h)⟩

Premises used: Set.Mem, setOf, Set.inter, eq_zero_of_ne_zero_of_mul_right_eq_zero, map_ne_zero_of_mem_nonZeroDivisors, eq_zero_of_ne_zero_of_mul_left_eq_zero, And.intro
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
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)
change : Eq (α := Submonoid S) (Submonoid.map h M₀⁰) S⁰
⊢ Eq (α := Submonoid S) (Submonoid.map h_1 M₀⁰) S⁰

Tactic:
change Submonoid.map h _ = _

Premises used: Submonoid.map
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
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)
h₁ : ∀ (x : S), Membership.mem (γ := Submonoid S) (Submonoid.map h M₀⁰) x ↔ Membership.mem (γ := Submonoid S) S⁰ x
⊢ Eq (α := Submonoid S) (Submonoid.map h M₀⁰) S⁰

Tactic:
ext
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero M₀'
inst_2 : FunLike F M₀ M₀'
inst_3 : NoZeroDivisors M₀'
inst_4 : MonoidWithZeroHomClass F M₀ M₀'
f : F
hf : Injective.{u_2 + 1, u_3 + 1} (α := M₀) (β := M₀') (⇑f : (a : M₀) → M₀')
S : Submonoid M₀
hS : S ≤ M₀⁰
inl : Subsingleton M₀ → LE.le (α := Submonoid M₀') (Submonoid.map f S) M₀'⁰
inr : Nontrivial M₀ → LE.le (α := Submonoid M₀') (Submonoid.map f S) M₀'⁰
⊢ LE.le (α := Submonoid M₀') (Submonoid.map f S) M₀'⁰

Tactic:
cases subsingleton_or_nontrivial M₀

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero M₀'
inst_2 : FunLike F M₀ M₀'
inst_3 : NoZeroDivisors M₀'
inst_4 : MonoidWithZeroHomClass F M₀ M₀'
f : F
hf : Injective.{u_2 + 1, u_3 + 1} (α := M₀) (β := M₀') (⇑f : (a : M₀) → M₀')
S : Submonoid M₀
hS : S ≤ M₀⁰
h : Subsingleton M₀
⊢ LE.le (α := Submonoid M₀') (Submonoid.map f S) M₀'⁰

Tactic:
simp [Subsingleton.elim S ⊥]

Premises used: Bot.bot, Subsingleton.elim
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero M₀'
inst_2 : FunLike F M₀ M₀'
inst_3 : NoZeroDivisors M₀'
inst_4 : MonoidWithZeroHomClass F M₀ M₀'
f : F
hf : Injective.{u_2 + 1, u_3 + 1} (α := M₀) (β := M₀') (⇑f : (a : M₀) → M₀')
S : Submonoid M₀
hS : S ≤ M₀⁰
h : Nontrivial M₀
⊢ LE.le (α := Submonoid M₀') (Submonoid.map f S) M₀'⁰

Tactic:
le_nonZeroDivisors_of_noZeroDivisors ?_

Premises used: le_nonZeroDivisors_of_noZeroDivisors
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero M₀'
inst_2 : FunLike F M₀ M₀'
inst_3 : NoZeroDivisors M₀'
inst_4 : MonoidWithZeroHomClass F M₀ M₀'
f : F
hf : Injective.{u_2 + 1, u_3 + 1} (α := M₀) (β := M₀') (⇑f : (a : M₀) → M₀')
S : Submonoid M₀
hS : S ≤ M₀⁰
h : Nontrivial M₀
inr : 0 ∉ Submonoid.map f S
⊢ LE.le (α := Submonoid M₀') (Submonoid.map f S) M₀'⁰

Tactic:
refine le_nonZeroDivisors_of_noZeroDivisors ?_

Premises used: le_nonZeroDivisors_of_noZeroDivisors
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero M₀'
inst_2 : FunLike F M₀ M₀'
inst_3 : NoZeroDivisors M₀'
inst_4 : MonoidWithZeroHomClass F M₀ M₀'
f : F
hf : Injective.{u_2 + 1, u_3 + 1} (α := M₀) (β := M₀') (⇑f : (a : M₀) → M₀')
S : Submonoid M₀
hS : S ≤ M₀⁰
h : Nontrivial M₀
x : M₀
hx : x ∈ (↑S : Set M₀)
hx0 : Eq.{u_3 + 1} (α := M₀') ((f : (a : M₀) → M₀') x : M₀') (0 : M₀')
⊢ False

Tactic:
zero_notMem_nonZeroDivisors <| hS <| map_eq_zero_iff f hf |>.mp hx0 ▸ hx

Premises used: Eq.rec, map_eq_zero_iff, Iff.mp, zero_notMem_nonZeroDivisors
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero M₀'
inst_2 : FunLike F M₀ M₀'
inst_3 : NoZeroDivisors M₀'
inst_4 : MonoidWithZeroHomClass F M₀ M₀'
f : F
hf : Injective.{u_2 + 1, u_3 + 1} (α := M₀) (β := M₀') (⇑f : (a : M₀) → M₀')
S : Submonoid M₀
hS : S ≤ M₀⁰
h : Nontrivial M₀
x : M₀
hx : x ∈ (↑S : Set M₀)
hx0 : Eq.{u_3 + 1} (α := M₀') ((f : (a : M₀) → M₀') x : M₀') (0 : M₀')
⊢ False

Tactic:
exact zero_notMem_nonZeroDivisors <| hS <| map_eq_zero_iff f hf |>.mp hx0 ▸ hx

Premises used: zero_notMem_nonZeroDivisors
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero M₀'
inst_2 : FunLike F M₀ M₀'
inst_3 : NoZeroDivisors M₀'
inst_4 : MonoidWithZeroHomClass F M₀ M₀'
f : F
hf : Injective.{u_2 + 1, u_3 + 1} (α := M₀) (β := M₀') (⇑f : (a : M₀) → M₀')
⊢ LE.le (α := Submonoid M₀) M₀⁰ (Submonoid.comap f M₀'⁰)

Tactic:
Submonoid.le_comap_of_map_le _ (map_le_nonZeroDivisors_of_injective _ hf le_rfl)

Premises used: le_rfl, map_le_nonZeroDivisors_of_injective, Submonoid.le_comap_of_map_le
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero M₀'
x : M₀
inst_2 : FunLike F M₀ M₀'
inst_3 : MonoidWithZeroHomClass F M₀ M₀'
f : F
hf : Injective.{u_2 + 1, u_3 + 1} (α := M₀) (β := M₀') (⇑f : (a : M₀) → M₀')
hx : Membership.mem (α := M₀') (γ := Submonoid M₀') M₀'⁰ ((f : (a : M₀) → M₀') x : M₀')
⊢ Membership.mem (γ := Submonoid M₀) M₀⁰ x

Tactic:
⟨fun y hy ↦ hf <| map_zero f ▸ hx.1 (f y) (map_mul f x y ▸ map_zero f ▸ congrArg f hy),
    fun y hy ↦ hf <| map_zero f ▸ hx.2 (f y) (map_mul f y x ▸ map_zero f ▸ congrArg f hy)⟩

Premises used: congrArg, Set.Mem, setOf, Eq.rec, map_zero, Set.inter, map_mul, And.right, And.left, And.intro, Eq.symm, DFunLike.coe
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst : MonoidWithZero M₀
inst_1 : MonoidWithZero M₀'
inst_2 : FunLike F M₀ M₀'
inst_3 : MonoidWithZeroHomClass F M₀ M₀'
f : F
hf : Injective.{u_2 + 1, u_3 + 1} (α := M₀) (β := M₀') (⇑f : (a : M₀) → M₀')
⊢ LE.le (α := Submonoid M₀) (Submonoid.comap f M₀'⁰) M₀⁰

Tactic:
fun _ ha ↦ mem_nonZeroDivisors_of_injective hf (Submonoid.mem_comap.mp ha)

Premises used: Submonoid.mem_comap, Iff.mp, mem_nonZeroDivisors_of_injective
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
rw : Eq (α := Submonoid M₀) (nonZeroDivisorsLeft M₀) (nonZeroDivisorsLeft M₀ ⊓ nonZeroDivisorsRight M₀)
rw₁ : Eq (α := Submonoid M₀) (nonZeroDivisorsRight M₀) (nonZeroDivisorsRight M₀ ⊓ nonZeroDivisorsRight M₀)
rw₂ rw₃ : Eq (α := Submonoid M₀) (nonZeroDivisorsRight M₀) (nonZeroDivisorsRight M₀)
⊢ Eq (α := Submonoid M₀) (nonZeroDivisorsLeft M₀) M₀⁰

Tactic:
rw [nonZeroDivisors, nonZeroDivisorsLeft_eq_right, inf_idem]

Premises used: nonZeroDivisorsLeft_eq_right, nonZeroDivisors, inf_idem
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
rw : Eq (α := Submonoid M₀) (nonZeroDivisorsLeft M₀) M₀⁰
rw₁ rw₂ : Eq (α := Submonoid M₀) M₀⁰ M₀⁰
⊢ Eq (α := Submonoid M₀) (nonZeroDivisorsRight M₀) M₀⁰

Tactic:
rw [← nonZeroDivisorsLeft_eq_right, nonZeroDivisorsLeft_eq_nonZeroDivisors]

Premises used: nonZeroDivisorsLeft_eq_right, nonZeroDivisorsLeft_eq_nonZeroDivisors
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
rw rw₁ : Eq (α := Submonoid M₀) (nonZeroDivisorsRight M₀) (nonZeroDivisorsRight M₀)
⊢ Eq (α := Submonoid M₀) (nonZeroDivisorsRight M₀) (nonZeroDivisorsLeft M₀)

Tactic:
rw [nonZeroDivisorsLeft_eq_right]

Premises used: nonZeroDivisorsLeft_eq_right
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
r : M₀
rw : Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsLeft M₀) r ↔ ∀ (x : M₀), r * x = 0 → x = 0
⊢ Membership.mem (γ := Submonoid M₀) M₀⁰ r ↔ ∀ (x : M₀), r * x = 0 → x = 0

Tactic:
rw [← nonZeroDivisorsLeft_eq_nonZeroDivisors]

Premises used: nonZeroDivisorsLeft_eq_nonZeroDivisors
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
r : M₀
⊢ Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsLeft M₀) r ↔ ∀ (x : M₀), r * x = 0 → x = 0

Tactic:
rfl
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
r : M₀
rw : Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) r ↔ ∀ (x : M₀), x * r = 0 → x = 0
⊢ Membership.mem (γ := Submonoid M₀) M₀⁰ r ↔ ∀ (x : M₀), x * r = 0 → x = 0

Tactic:
rw [← nonZeroDivisorsRight_eq_nonZeroDivisors]

Premises used: nonZeroDivisorsRight_eq_nonZeroDivisors
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
r : M₀
⊢ Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) r ↔ ∀ (x : M₀), x * r = 0 → x = 0

Tactic:
rfl
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
r : M₀
⊢ r ∉ M₀⁰ ↔ Set.Nonempty.{u_1} (α := M₀) {s : M₀ | r * s = 0 ∧ s ≠ 0}

Tactic:
simp [mem_nonZeroDivisors_iff_left, Set.nonempty_def]

Premises used: mem_nonZeroDivisors_iff_left, Set.nonempty_def
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
r : M₀
⊢ r ∉ M₀⁰ ↔ Set.Nonempty.{u_1} (α := M₀) {s : M₀ | s * r = 0 ∧ s ≠ 0}

Tactic:
simp [mem_nonZeroDivisors_iff_right, Set.nonempty_def]

Premises used: mem_nonZeroDivisors_iff_right, Set.nonempty_def
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
r x : M₀
hr : Membership.mem (γ := Submonoid M₀) M₀⁰ r
rw : x * r = 0 ↔ x = 0
rw₁ rw₂ : x = 0 ↔ x = 0
⊢ r * x = 0 ↔ x = 0

Tactic:
rw [mul_comm, mul_right_mem_nonZeroDivisors_eq_zero_iff hr]

Premises used: mul_right_mem_nonZeroDivisors_eq_zero_iff, mul_comm
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
x : M₀
c : ↥M₀⁰
⊢ (↑c : M₀) * x = 0 ↔ x = 0

Tactic:
mul_left_mem_nonZeroDivisors_eq_zero_iff c.prop

Premises used: mul_left_mem_nonZeroDivisors_eq_zero_iff, Subtype.prop
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a b : M₀
h : Membership.mem (γ := Submonoid M₀) M₀⁰ (a * b)
rw :
  Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) a ∧
    Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) b
⊢ Membership.mem (γ := Submonoid M₀) M₀⁰ a ∧ Membership.mem (γ := Submonoid M₀) M₀⁰ b

Tactic:
rw [← nonZeroDivisorsRight_eq_nonZeroDivisors]

Premises used: nonZeroDivisorsRight_eq_nonZeroDivisors
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a b : M₀
h : Membership.mem (γ := Submonoid M₀) M₀⁰ (a * b)
left : Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) a
right : Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) b
⊢ Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) a ∧
    Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) b

Tactic:
constructor
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a b : M₀
h : Membership.mem (γ := Submonoid M₀) M₀⁰ (a * b)
x : M₀
h' : x * a = 0
left : x * (a * b) = 0
⊢ x = 0

Tactic:
apply h.2

Premises used: And.right
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a b : M₀
h : Membership.mem (γ := Submonoid M₀) M₀⁰ (a * b)
x : M₀
h' : x * b = 0
right : x * (a * b) = 0
⊢ x = 0

Tactic:
apply h.2

Premises used: And.right
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a b : M₀
h : Membership.mem (γ := Submonoid M₀) M₀⁰ (a * b)
x : M₀
h' : x * a = 0
left : x * a * b = 0
left₁ : 0 * b = 0
left₂ left₃ : Eq.{u_1 + 1} (α := M₀) 0 0
⊢ x * (a * b) = 0

Tactic:
rw [← mul_assoc, h', zero_mul]

Premises used: MulZeroClass.zero_mul, mul_assoc
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a b : M₀
h : Membership.mem (γ := Submonoid M₀) M₀⁰ (a * b)
x : M₀
h' : x * b = 0
right : x * (b * a) = 0
right₁ : x * b * a = 0
right₂ : 0 * a = 0
right₃ right₄ : Eq.{u_1 + 1} (α := M₀) 0 0
⊢ x * (a * b) = 0

Tactic:
rw [mul_comm a b, ← mul_assoc, h', zero_mul]

Premises used: MulZeroClass.zero_mul, mul_assoc, mul_comm
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a b : ↥M₀⁰
h : a ∣ b
c : ↥M₀⁰
hc : b = a * c
simp_rw : (↑a : M₀) ∣ (↑(a * c) : M₀)
simp_rw₁ : (↑a : M₀) ∣ (↑a : M₀) * (↑c : M₀)
⊢ (↑a : M₀) ∣ (↑b : M₀)

Tactic:
simp_rw [hc, Submonoid.coe_mul, dvd_mul_right]

Premises used: dvd_mul_right, Submonoid.coe_mul
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a b : ↥M₀⁰
h : (↑a : M₀) ∣ (↑b : M₀)
c : M₀
hc : (↑b : M₀) = (↑a : M₀) * c
simp_rw : (↑b : M₀) = (↑(a * Subtype.mk (p := fun (x : M₀) ↦ Membership.mem (γ := Submonoid M₀) M₀⁰ x) c ⋯) : M₀)
simp_rw₁ : (↑b : M₀) = (↑a : M₀) * c
⊢ b = a * Subtype.mk (p := fun (x : M₀) ↦ Membership.mem (γ := Submonoid M₀) M₀⁰ x) c ⋯

Tactic:
simp_rw [Subtype.ext_iff, Submonoid.coe_mul, hc]

Premises used: Subtype.ext_iff, Submonoid.coe_mul