awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ 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 : (a : S) → M₀) a : M₀) = 0 →
        Eq.{u_4 + 1} (α := M₀) ((h.symm : (a : S) → M₀) a : M₀) (0 : M₀)) ∧
    ∀ (a : S),
      HMul.hMul (α := M₀) (β := M₀) ((h.symm : (a : S) → M₀) a : M₀) ((h.symm : (a : S) → M₀) x : M₀) = 0 →
        Eq.{u_4 + 1} (α := M₀) ((h.symm : (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
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
h₆ :
  ((∀ (a : S),
        HMul.hMul (α := M₀) (β := M₀) ((h.symm : (a : S) → M₀) x : M₀) ((h.symm : (a : S) → M₀) a : M₀) = 0 →
          Eq.{u_4 + 1} (α := M₀) ((h.symm : (a : S) → M₀) a : M₀) (0 : M₀)) ∧
      ∀ (a : S),
        HMul.hMul (α := M₀) (β := M₀) ((h.symm : (a : S) → M₀) a : M₀) ((h.symm : (a : S) → M₀) x : M₀) = 0 →
          Eq.{u_4 + 1} (α := M₀) ((h.symm : (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),
      Eq.{u_4 + 1} (α := M₀) ((h.symm : (a : S) → M₀) (x * a) : M₀) (0 : M₀) →
        Eq.{u_4 + 1} (α := M₀) ((h.symm : (a : S) → M₀) a : M₀) (0 : M₀)) ∧
    ∀ (a : S),
      Eq.{u_4 + 1} (α := M₀) ((h.symm : (a : S) → M₀) (a * x) : M₀) (0 : M₀) →
        Eq.{u_4 + 1} (α := M₀) ((h.symm : (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:
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₀⁰
⊢ LE.le (α := Submonoid M₀') (Submonoid.map f S) M₀'⁰
have inl : Subsingleton M₀ → LE.le (α := Submonoid M₀') (Submonoid.map f S) M₀'⁰
Tactic: cases subsingleton_or_nontrivial M₀
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
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₀'⁰
⊢ LE.le (α := Submonoid M₀') (Submonoid.map f S) M₀'⁰
have inr : Nontrivial M₀ → LE.le (α := Submonoid M₀') (Submonoid.map f S) M₀'⁰
Tactic: cases subsingleton_or_nontrivial M₀
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
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₀'⁰
have inr : 0 ∉ Submonoid.map f S
Tactic: refine le_nonZeroDivisors_of_noZeroDivisors ?_
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
⊢ Eq (α := Submonoid M₀) (nonZeroDivisorsLeft M₀) M₀⁰
have rw : Eq (α := Submonoid M₀) (nonZeroDivisorsLeft M₀) (nonZeroDivisorsLeft M₀ ⊓ nonZeroDivisorsRight M₀)
Tactic: rw [nonZeroDivisors, nonZeroDivisorsLeft_eq_right, inf_idem]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
rw : Eq (α := Submonoid M₀) (nonZeroDivisorsLeft M₀) (nonZeroDivisorsLeft M₀ ⊓ nonZeroDivisorsRight M₀)
⊢ Eq (α := Submonoid M₀) (nonZeroDivisorsLeft M₀) M₀⁰
have rw₁ : Eq (α := Submonoid M₀) (nonZeroDivisorsRight M₀) (nonZeroDivisorsRight M₀ ⊓ nonZeroDivisorsRight M₀)
Tactic: rw [nonZeroDivisors, nonZeroDivisorsLeft_eq_right, inf_idem]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
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₀)
⊢ Eq (α := Submonoid M₀) (nonZeroDivisorsLeft M₀) M₀⁰
have rw₂ : Eq (α := Submonoid M₀) (nonZeroDivisorsRight M₀) (nonZeroDivisorsRight M₀)
Tactic: rw [nonZeroDivisors, nonZeroDivisorsLeft_eq_right, inf_idem]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
⊢ Eq (α := Submonoid M₀) (nonZeroDivisorsRight M₀) M₀⁰
have rw : Eq (α := Submonoid M₀) (nonZeroDivisorsLeft M₀) M₀⁰
Tactic: rw [← nonZeroDivisorsLeft_eq_right, nonZeroDivisorsLeft_eq_nonZeroDivisors]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
rw : Eq (α := Submonoid M₀) (nonZeroDivisorsLeft M₀) M₀⁰
⊢ Eq (α := Submonoid M₀) (nonZeroDivisorsRight M₀) M₀⁰
have rw₁ : Eq (α := Submonoid M₀) M₀⁰ M₀⁰
Tactic: rw [← nonZeroDivisorsLeft_eq_right, nonZeroDivisorsLeft_eq_nonZeroDivisors]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
⊢ Eq (α := Submonoid M₀) (nonZeroDivisorsRight M₀) (nonZeroDivisorsLeft M₀)
have rw : Eq (α := Submonoid M₀) (nonZeroDivisorsRight M₀) (nonZeroDivisorsRight M₀)
Tactic: rw [nonZeroDivisorsLeft_eq_right]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
r : M₀
⊢ Membership.mem (γ := Submonoid M₀) M₀⁰ r ↔ ∀ (x : M₀), r * x = 0 → x = 0
have rw : Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsLeft M₀) r ↔ ∀ (x : M₀), r * x = 0 → x = 0
Tactic: rw [← nonZeroDivisorsLeft_eq_nonZeroDivisors]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
r : M₀
⊢ Membership.mem (γ := Submonoid M₀) M₀⁰ r ↔ ∀ (x : M₀), x * r = 0 → x = 0
have rw : Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) r ↔ ∀ (x : M₀), x * r = 0 → x = 0
Tactic: rw [← nonZeroDivisorsRight_eq_nonZeroDivisors]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
r x : M₀
hr : Membership.mem (γ := Submonoid M₀) M₀⁰ r
⊢ r * x = 0 ↔ x = 0
have rw : x * r = 0 ↔ x = 0
Tactic: rw [mul_comm, mul_right_mem_nonZeroDivisors_eq_zero_iff hr]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
r x : M₀
hr : Membership.mem (γ := Submonoid M₀) M₀⁰ r
rw : x * r = 0 ↔ x = 0
⊢ r * x = 0 ↔ x = 0
have rw₁ : x = 0 ↔ x = 0
Tactic: rw [mul_comm, mul_right_mem_nonZeroDivisors_eq_zero_iff hr]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a b : M₀
h : Membership.mem (γ := Submonoid M₀) M₀⁰ (a * b)
⊢ Membership.mem (γ := Submonoid M₀) M₀⁰ a ∧ Membership.mem (γ := Submonoid M₀) M₀⁰ b
have rw : Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) a ∧
  Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) b
Tactic: rw [← nonZeroDivisorsRight_eq_nonZeroDivisors]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a b : M₀
h : Membership.mem (γ := Submonoid M₀) M₀⁰ (a * b)
⊢ Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) a ∧
    Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) b
have left : Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
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
⊢ Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) a ∧
    Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) b
have right : Membership.mem (γ := Submonoid M₀) (nonZeroDivisorsRight M₀) b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
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
⊢ x = 0
have left : x * (a * b) = 0
Tactic: apply h.2
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
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
⊢ x = 0
have right : x * (a * b) = 0
Tactic: apply h.2
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
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
⊢ x * (a * b) = 0
have left : x * a * b = 0
Tactic: rw [← mul_assoc, h', zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
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 * (a * b) = 0
have left₁ : 0 * b = 0
Tactic: rw [← mul_assoc, h', zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
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
⊢ x * (a * b) = 0
have left₂ : Eq.{u_1 + 1} (α := M₀) 0 0
Tactic: rw [← mul_assoc, h', zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
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
⊢ x * (a * b) = 0
have right : x * (b * a) = 0
Tactic: rw [mul_comm a b, ← mul_assoc, h', zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
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
⊢ x * (a * b) = 0
have right₁ : x * b * a = 0
Tactic: rw [mul_comm a b, ← mul_assoc, h', zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
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
⊢ x * (a * b) = 0
have right₂ : 0 * a = 0
Tactic: rw [mul_comm a b, ← mul_assoc, h', zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
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
⊢ x * (a * b) = 0
have right₃ : Eq.{u_1 + 1} (α := M₀) 0 0
Tactic: rw [mul_comm a b, ← mul_assoc, h', zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a b : ↥M₀⁰
h : a ∣ b
c : ↥M₀⁰
hc : b = a * c
⊢ (↑a : M₀) ∣ (↑b : M₀)
have simp_rw : (↑a : M₀) ∣ (↑(a * c) : M₀)
Tactic: simp_rw [hc, Submonoid.coe_mul, dvd_mul_right]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
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₀)
⊢ (↑a : M₀) ∣ (↑b : M₀)
have simp_rw₁ : (↑a : M₀) ∣ (↑a : M₀) * (↑c : M₀)
Tactic: simp_rw [hc, Submonoid.coe_mul, dvd_mul_right]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a b : ↥M₀⁰
h : (↑a : M₀) ∣ (↑b : M₀)
c : M₀
hc : (↑b : M₀) = (↑a : M₀) * c
⊢ b = a * Subtype.mk (p := fun (x : M₀) ↦ Membership.mem (γ := Submonoid M₀) M₀⁰ x) c ⋯
have simp_rw : (↑b : M₀) = (↑(a * Subtype.mk (p := fun (x : M₀) ↦ Membership.mem (γ := Submonoid M₀) M₀⁰ x) c sorry) : M₀)
Tactic: simp_rw [Subtype.ext_iff, Submonoid.coe_mul, hc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : ↥M₀⁰
⊢ (∃ (b_1 : (↥M₀⁰)ˣ),
      (↑a : M₀) *
          (↑((Equiv.symm (MulEquiv.toEquiv (MulEquiv.symm unitsNonZeroDivisorsEquiv)) : (a : (↥M₀⁰)ˣ) → M₀ˣ) b_1) :
            M₀) =
        (↑b : M₀)) ↔
    Associated a b
have simp : (∃ (b_1 : (↥M₀⁰)ˣ), (↑a : M₀) * (↑(↑b_1 : ↥M₀⁰) : M₀) = (↑b : M₀)) ↔ ∃ (u : (↥M₀⁰)ˣ), a * (↑u : ↥M₀⁰) = b
Tactic: simp [Associated]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : ↥M₀⁰
⊢ (∃ (b_1 : (↥M₀⁰)ˣ), (↑a : M₀) * (↑(↑b_1 : ↥M₀⁰) : M₀) = (↑b : M₀)) ↔ ∃ (u : (↥M₀⁰)ˣ), a * (↑u : ↥M₀⁰) = b
have norm_cast : (∃ (b_1 : (↥M₀⁰)ˣ), a * (↑b_1 : ↥M₀⁰) = b) ↔ ∃ (u : (↥M₀⁰)ˣ), a * (↑u : ↥M₀⁰) = b
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
⊢ Membership.mem (γ := Submonoid (Associates M₀)) (Associates M₀)⁰ (Associates.mk a) ↔
    Membership.mem (γ := Submonoid M₀) M₀⁰ a
have rw : (∀ (x : Associates M₀), x * Associates.mk a = 0 → x = 0) ↔ ∀ (x : M₀), x * a = 0 → x = 0
Tactic: rw [mem_nonZeroDivisors_iff_right, mem_nonZeroDivisors_iff_right]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
⊢ (∀ (x : Associates M₀), x * Associates.mk a = 0 → x = 0) ↔ ∀ (x : M₀), x * a = 0 → x = 0
have contrapose! : (∃ (x : Associates M₀), x * Associates.mk a = 0 ∧ x ≠ 0) ↔ ∃ (x : M₀), x * a = 0 ∧ x ≠ 0
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
⊢ (∃ (x : Associates M₀), x * Associates.mk a = 0 ∧ x ≠ 0) ↔ ∃ (x : M₀), x * a = 0 ∧ x ≠ 0
have mp : (∃ (x : Associates M₀), x * Associates.mk a = 0 ∧ x ≠ 0) → ∃ (x : M₀), x * a = 0 ∧ x ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
mp : (∃ (x : Associates M₀), x * Associates.mk a = 0 ∧ x ≠ 0) → ∃ (x : M₀), x * a = 0 ∧ x ≠ 0
⊢ (∃ (x : Associates M₀), x * Associates.mk a = 0 ∧ x ≠ 0) ↔ ∃ (x : M₀), x * a = 0 ∧ x ≠ 0
have mpr : (∃ (x : M₀), x * a = 0 ∧ x ≠ 0) → ∃ (x : Associates M₀), x * Associates.mk a = 0 ∧ x ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
w : Associates M₀
x : M₀
hx₁ : HMul.hMul (α := Associates M₀) (Quot.mk (⇑(Associated.setoid M₀) : M₀ → M₀ → Prop) x) (Associates.mk a) = 0
hx₂ : Ne (α := Associates M₀) (Quot.mk (⇑(Associated.setoid M₀) : M₀ → M₀ → Prop) x) 0
⊢ ∃ (x : M₀), x * a = 0 ∧ x ≠ 0
have mp : x * a = 0
Tactic: refine ⟨x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
w : Associates M₀
x : M₀
hx₁ : HMul.hMul (α := Associates M₀) (Quot.mk (⇑(Associated.setoid M₀) : M₀ → M₀ → Prop) x) (Associates.mk a) = 0
hx₂ : Ne (α := Associates M₀) (Quot.mk (⇑(Associated.setoid M₀) : M₀ → M₀ → Prop) x) 0
mp : x * a = 0
⊢ ∃ (x : M₀), x * a = 0 ∧ x ≠ 0
have mp₁ : x ≠ 0
Tactic: refine ⟨x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
w : Associates M₀
x : M₀
hx₁ : HMul.hMul (α := Associates M₀) (Quot.mk (⇑(Associated.setoid M₀) : M₀ → M₀ → Prop) x) (Associates.mk a) = 0
hx₂ : Ne (α := Associates M₀) (Quot.mk (⇑(Associated.setoid M₀) : M₀ → M₀ → Prop) x) 0
⊢ x * a = 0
have mp : Eq (α := Associates M₀) (Associates.mk (x * a)) 0
Tactic: rwa [← Associates.mk_eq_zero, ← Associates.mk_mul_mk, ← Associates.quot_mk_eq_mk]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
w : Associates M₀
x : M₀
hx₁ : HMul.hMul (α := Associates M₀) (Quot.mk (⇑(Associated.setoid M₀) : M₀ → M₀ → Prop) x) (Associates.mk a) = 0
hx₂ : Ne (α := Associates M₀) (Quot.mk (⇑(Associated.setoid M₀) : M₀ → M₀ → Prop) x) 0
mp : Eq (α := Associates M₀) (Associates.mk (x * a)) 0
⊢ x * a = 0
have mp₁ : HMul.hMul (α := Associates M₀) (Associates.mk x) (Associates.mk a) = 0
Tactic: rwa [← Associates.mk_eq_zero, ← Associates.mk_mul_mk, ← Associates.quot_mk_eq_mk]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
w : Associates M₀
x : M₀
hx₁ : HMul.hMul (α := Associates M₀) (Quot.mk (⇑(Associated.setoid M₀) : M₀ → M₀ → Prop) x) (Associates.mk a) = 0
hx₂ : Ne (α := Associates M₀) (Quot.mk (⇑(Associated.setoid M₀) : M₀ → M₀ → Prop) x) 0
⊢ x ≠ 0
have mp : Ne (α := Associates M₀) (Associates.mk x) 0
Tactic: rwa [← Associates.mk_ne_zero, ← Associates.quot_mk_eq_mk]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
⊢ (∃ (x : M₀), x * a = 0 ∧ x ≠ 0) → ∃ (x : Associates M₀), x * Associates.mk a = 0 ∧ x ≠ 0
have mpr : (∃ (x : M₀), x * a = 0 ∧ x ≠ 0) →
  ∀ (b : M₀) (hb₁ : b * a = 0) (hb₂ : b ≠ 0), HMul.hMul (α := Associates M₀) (Associates.mk b) (Associates.mk a) = 0
Tactic: refine fun ⟨b, hb₁, hb₂⟩ ↦ ⟨Associates.mk b, ?_, by rwa [Associates.mk_ne_zero]⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
h : ∃ (x : M₀), x * a = 0 ∧ x ≠ 0
b : M₀
hb₁ : b * a = 0
hb₂ : b ≠ 0
⊢ HMul.hMul (α := Associates M₀) (Associates.mk b) (Associates.mk a) = 0
have mpr : Eq (α := Associates M₀) (Associates.mk (b * a)) 0
Tactic: rw [Associates.mk_mul_mk, hb₁, Associates.mk_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
h : ∃ (x : M₀), x * a = 0 ∧ x ≠ 0
b : M₀
hb₁ : b * a = 0
hb₂ : b ≠ 0
mpr : Eq (α := Associates M₀) (Associates.mk (b * a)) 0
⊢ HMul.hMul (α := Associates M₀) (Associates.mk b) (Associates.mk a) = 0
have mpr₁ : Eq.{u_1 + 1} (α := Associates M₀) (Associates.mk 0) 0
Tactic: rw [Associates.mk_mul_mk, hb₁, Associates.mk_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.NonZeroDivisors (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
h : ∃ (x : M₀), x * a = 0 ∧ x ≠ 0
b : M₀
hb₁ : b * a = 0
hb₂ : b ≠ 0
mpr : Eq (α := Associates M₀) (Associates.mk (b * a)) 0
mpr₁ : Eq.{u_1 + 1} (α := Associates M₀) (Associates.mk 0) 0
⊢ HMul.hMul (α := Associates M₀) (Associates.mk b) (Associates.mk a) = 0
have mpr₂ : Eq.{u_1 + 1} (α := Associates M₀) 0 0
Tactic: rw [Associates.mk_mul_mk, hb₁, Associates.mk_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MulZeroClass (α i)
inst_1 : DecidableEq ι
i : ι
f a : (i : ι) → α i
⊢ 0 * a = 0
have h : ∀ (x : ι), HMul.hMul (α := (i : ι) → α i) 0 a x = 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MulZeroClass (α i)
inst_1 : DecidableEq ι
i : ι
f a : (i : ι) → α i
⊢ a * 0 = 0
have h : ∀ (x : ι), HMul.hMul (β := (i : ι) → α i) a 0 x = 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Pointwise.Finset (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : DecidableEq α
s : Finset α
inst_3 : IsLeftCancelMulZero α
⊢ #s ≤ #(s * s)
have inl : ∀ (hs : s.erase 0 = ∅), #s ≤ #(s * s)
Tactic: obtain hs | hs := (s.erase 0).eq_empty_or_nonempty