awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (hypothesis)
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' :
  ∀ {x y : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
h_right' :
  ∀ {y x : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (y * x)
I : TwoSidedIdeal R := mk' (↑(closure s) : Set R) ⋯ ⋯ ⋯ ⋯ ⋯
hz : z ∈ I
J : TwoSidedIdeal R
hJ : s ⊆ (↑J : Set R)
⊢ z ∈ J
have hz₁ : Membership.mem (γ := AddSubgroup R) (closure s) z
Tactic: case mem_ideal_of_subset =>
    simp only [I, SetLike.mem_coe, mem_mk'] at hz
    induction hz using closure_induction with
    | mem x hx => exact hJ hx
    | zero => exact zero_mem _
    | add x y _ _ hx hy => exact J.add_mem hx hy
    | neg x _ hx => exact J.neg_mem hx
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z : R
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z
have trans : Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔
  Membership.mem (γ := TwoSidedIdeal R) (span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z
Tactic: trans z ∈ span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z : R
trans :
  Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔
    Membership.mem (γ := TwoSidedIdeal R) (span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z
have trans₁ : Membership.mem (γ := TwoSidedIdeal R) (span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z ↔
  Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z
Tactic: trans z ∈ span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z : R
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔
    Membership.mem (γ := TwoSidedIdeal R) (span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z
have refine : ∀ (h : Membership.mem (γ := TwoSidedIdeal R) (span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z),
  Membership.mem (γ := TwoSidedIdeal R) (span s) z
Tactic: refine ⟨(span_mono (by simp only [Set.union_assoc, Set.subset_union_left]) ·), fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z : R
h : Membership.mem (γ := TwoSidedIdeal R) (span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z
have refine : s ∪ s * univ ∪ univ * s ∪ univ * s * univ ⊆ (↑(span s) : Set R)
Tactic: refine mem_span_iff.mp h (span s) ?_
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z : R
h : Membership.mem (γ := TwoSidedIdeal R) (span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z
⊢ s ∪ s * univ ∪ univ * s ∪ univ * s * univ ⊆ (↑(span s) : Set R)
have simp : s ⊆ (↑(span s) : Set R) ∧
  s * univ ⊆ (↑(span s) : Set R) ∧ univ * s ⊆ (↑(span s) : Set R) ∧ univ * s * univ ⊆ (↑(span s) : Set R)
Tactic: simp only [union_subset_iff, union_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z : R
⊢ Membership.mem (γ := TwoSidedIdeal R) (span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z ↔
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z
have refine_1 : ∀ (x y : R), y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ → x * y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ
Tactic: refine mem_span_iff_mem_addSubgroup_closure_absorbing ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z : R
refine_1 :
  ∀ (x y : R), y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ → x * y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ
⊢ Membership.mem (γ := TwoSidedIdeal R) (span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z ↔
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z
have refine_2 : ∀ (y x : R), y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ → y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ
Tactic: refine mem_span_iff_mem_addSubgroup_closure_absorbing ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ x * (fun (x1 x2 : R) ↦ x1 * x2) ((fun (x1 x2 : R) ↦ x1 * x2) r' y) r ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ
have refine_1 : (fun (x1 x2 : R) ↦ x1 * x2) (x * r') y = x * r' * y
Tactic: refine .inr <| ⟨x * r' * y, ⟨x * r', mem_univ _, y, hy, ?_⟩, ⟨r, mem_univ _, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
refine_1 : (fun (x1 x2 : R) ↦ x1 * x2) (x * r') y = x * r' * y
⊢ x * (fun (x1 x2 : R) ↦ x1 * x2) ((fun (x1 x2 : R) ↦ x1 * x2) r' y) r ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ
have refine_1₁ : (fun (x1 x2 : R) ↦ x1 * x2) (x * r' * y) r = x * (fun (x1 x2 : R) ↦ x1 * x2) ((fun (x1 x2 : R) ↦ x1 * x2) r' y) r
Tactic: refine .inr <| ⟨x * r' * y, ⟨x * r', mem_univ _, y, hy, ?_⟩, ⟨r, mem_univ _, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ (fun (x1 x2 : R) ↦ x1 * x2) ((fun (x1 x2 : R) ↦ x1 * x2) r' y) r * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ
have refine_2 : (fun (x1 x2 : R) ↦ x1 * x2) (r' * y) (r * x) = (fun (x1 x2 : R) ↦ x1 * x2) ((fun (x1 x2 : R) ↦ x1 * x2) r' y) r * x
Tactic: refine .inr <| ⟨r' * y, ⟨r', mem_univ _, y, hy, rfl⟩, r * x, mem_univ _, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
z : R
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (univ * s * univ)) z
have trans : Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔ Membership.mem (γ := TwoSidedIdeal R) (span (univ * s * univ)) z
Tactic: trans z ∈ span (univ * s * univ)
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
z : R
trans :
  Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔ Membership.mem (γ := TwoSidedIdeal R) (span (univ * s * univ)) z
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (univ * s * univ)) z
have trans₁ : Membership.mem (γ := TwoSidedIdeal R) (span (univ * s * univ)) z ↔
  Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (univ * s * univ)) z
Tactic: trans z ∈ span (univ * s * univ)
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
z : R
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔ Membership.mem (γ := TwoSidedIdeal R) (span (univ * s * univ)) z
have refine_1 : Membership.mem (γ := TwoSidedIdeal R) (span s) z → ∀ (x : R) (hx : x ∈ s), x ∈ univ * s * univ
Tactic: refine ⟨(span_mono (fun x hx ↦ ?_) ·), fun hz ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
z : R
refine_1 : Membership.mem (γ := TwoSidedIdeal R) (span s) z → ∀ (x : R) (hx : x ∈ s), x ∈ univ * s * univ
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔ Membership.mem (γ := TwoSidedIdeal R) (span (univ * s * univ)) z
have refine_2 : ∀ (hz : Membership.mem (γ := TwoSidedIdeal R) (span (univ * s * univ)) z),
  Membership.mem (γ := TwoSidedIdeal R) (span s) z
Tactic: refine ⟨(span_mono (fun x hx ↦ ?_) ·), fun hz ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
z : R
⊢ Membership.mem (γ := TwoSidedIdeal R) (span (univ * s * univ)) z ↔
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (univ * s * univ)) z
have refine_1 : ∀ (x y : R), y ∈ univ * s * univ → x * y ∈ univ * s * univ
Tactic: refine mem_span_iff_mem_addSubgroup_closure_absorbing ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
z : R
refine_1 : ∀ (x y : R), y ∈ univ * s * univ → x * y ∈ univ * s * univ
⊢ Membership.mem (γ := TwoSidedIdeal R) (span (univ * s * univ)) z ↔
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (univ * s * univ)) z
have refine_2 : ∀ (y x : R), y ∈ univ * s * univ → y * x ∈ univ * s * univ
Tactic: refine mem_span_iff_mem_addSubgroup_closure_absorbing ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
z x y : R
hy : y ∈ univ * s * univ
⊢ x * y ∈ univ * s * univ
have refine_1 : ∀ (hy : y ∈ univ * (s * univ)), x * y ∈ univ * (s * univ)
Tactic: rw [mul_assoc] at hy ⊢
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
z x y : R
hy : y ∈ univ * (s * univ)
⊢ x * y ∈ univ * (s * univ)
have refine_1 : ∀ (r y : R) (hy : y ∈ s * univ), x * (fun (x1 x2 : R) ↦ x1 * x2) r y ∈ univ * (s * univ)
Tactic: obtain ⟨r, -, y, hy, rfl⟩ := hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (hypothesis)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
J : TwoSidedIdeal R
h : I ≤ (asIdeal : (a : TwoSidedIdeal R) → Ideal R) J
x : R
hx : Membership.mem (γ := TwoSidedIdeal R) ((fromIdeal : (a : Ideal R) → TwoSidedIdeal R) I : TwoSidedIdeal R) x
⊢ x ∈ J
have hx₁ : ∀ (I_1 : TwoSidedIdeal R), (↑I : Set R) ⊆ (↑I_1 : Set R) → x ∈ I_1
Tactic: simp only [fromIdeal, OrderHom.coe_mk, mem_span_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : Ring R
I_1 I J : TwoSidedIdeal R
h : I ≤ J
x : Rᵐᵒᵖ
h' :
  Membership.mem (γ := Submodule Rᵐᵒᵖ Rᵐᵒᵖ)
    ((fun (I : TwoSidedIdeal R) ↦
        ((asIdeal : (a : TwoSidedIdeal Rᵐᵒᵖ) → Ideal Rᵐᵒᵖ) { ringCon := I.ringCon.op } : Ideal Rᵐᵒᵖ))
      I)
    x
⊢ Membership.mem (γ := Submodule Rᵐᵒᵖ Rᵐᵒᵖ)
    ((fun (I : TwoSidedIdeal R) ↦
        ((asIdeal : (a : TwoSidedIdeal Rᵐᵒᵖ) → Ideal Rᵐᵒᵖ) { ringCon := I.ringCon.op } : Ideal Rᵐᵒᵖ))
      J)
    x
have simp : ∀ (h' : (I.ringCon : (a : R) → R → Prop) 0 (MulOpposite.unop x)),
  (J.ringCon : (a : R) → R → Prop) 0 (MulOpposite.unop x)
Tactic: simp only [mem_asIdeal, mem_iff, RingCon.op_iff, MulOpposite.unop_zero] at h' ⊢
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : Ring R
I : TwoSidedIdeal R
⊢ toTwoSided ((TwoSidedIdeal.asIdeal : (a : TwoSidedIdeal R) → Ideal R) I) = I
have h : ∀ (x : R),
  Membership.mem (γ := TwoSidedIdeal R) (toTwoSided ((TwoSidedIdeal.asIdeal : (a : TwoSidedIdeal R) → Ideal R) I)) x ↔
    x ∈ I
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Operations (goal)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
⊢ (TwoSidedIdeal.asIdeal : (a : TwoSidedIdeal R) → Ideal R) I.toTwoSided = I
have h : ∀ (x : R),
  Membership.mem (γ := Ideal R) ((TwoSidedIdeal.asIdeal : (a : TwoSidedIdeal R) → Ideal R) I.toTwoSided : Ideal R) x ↔
    x ∈ I
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
h : WellFoundedLT.{u_1} (Associates α)
⊢ WellFounded.{u_1 + 1} (α := Associates α) DvdNotUnit
have h₁ : ∀ (x x : Associates α), Eq.{u_1 + 1} (α := (a b : Associates α) → Prop) DvdNotUnit LT.lt
Tactic: convert! h.wf
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
h : WellFoundedLT.{u_1} (Associates α)
x x_1 : Associates α
⊢ Eq.{u_1 + 1} (α := (a b : Associates α) → Prop) DvdNotUnit LT.lt
have h₁ : ∀ (x x_2 : Associates α), DvdNotUnit x x_2 ↔ x < x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
⊢ ∀ {a : Associates α}, Irreducible a ↔ Prime a
have rw : ∀ (a : α), Irreducible a ↔ Prime a
Tactic: rw [← Associates.irreducible_iff_prime_iff]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
⊢ Multiset.Rel Associated (p ::ₘ f) g
have cons : ∀ (b : α) (hbg : b ∈ g) (hb : p ~ᵤ b), Multiset.Rel Associated (p ::ₘ f) g
Tactic: let ⟨b, hbg, hb⟩ :=
      (exists_associated_mem_of_dvd_prod (hf p (by simp)) fun q hq => hg _ hq) <|
        hfg.dvd_iff_dvd_right.1 (show p ∣ (p ::ₘ f).prod by simp)
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
⊢ Multiset.Rel Associated (p ::ₘ f) g
have cons : ∀ (this : DecidableEq α), Multiset.Rel Associated (p ::ₘ f) g
Tactic: haveI := Classical.decEq α
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
⊢ Multiset.Rel Associated (p ::ₘ f) g
have cons : Multiset.Rel Associated (p ::ₘ f) (b ::ₘ g.erase b)
Tactic: rw [← Multiset.cons_erase hbg]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
⊢ p * f.prod ~ᵤ b * (g.erase b).prod
have rwa : (p ::ₘ f).prod ~ᵤ b * (g.erase b).prod
Tactic: rwa [← Multiset.prod_cons, ← Multiset.prod_cons, Multiset.cons_erase hbg]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
rwa : (p ::ₘ f).prod ~ᵤ b * (g.erase b).prod
⊢ p * f.prod ~ᵤ b * (g.erase b).prod
have rwa₁ : (p ::ₘ f).prod ~ᵤ (b ::ₘ g.erase b).prod
Tactic: rwa [← Multiset.prod_cons, ← Multiset.prod_cons, Multiset.cons_erase hbg]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
f : Multiset α
⊢ ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
have empty : ∀ {g : Multiset α},
  (∀ (x : α), Membership.mem (γ := Multiset α) 0 x → Prime x) →
    (∀ x ∈ g, Prime x) → Multiset.prod 0 ~ᵤ g.prod → Multiset.Rel Associated 0 g
Tactic: induction f using Multiset.induction_on with
  | empty =>
    intro g _ hg h
    exact Multiset.rel_zero_left.2 <|
      Multiset.eq_zero_of_forall_notMem fun x hx =>
        have : IsUnit g.prod := by simpa [associated_one_iff_isUnit] using h.symm
        (hg x hx).not_unit <|
          isUnit_iff_dvd_one.2 <| (Multiset.dvd_prod hx).trans (isUnit_iff_dvd_one.1 this)
  | cons p f ih =>
    intro g hf hg hfg
    let ⟨b, hbg, hb⟩ :=
      (exists_associated_mem_of_dvd_prod (hf p (by simp)) fun q hq => hg _ hq) <|
        hfg.dvd_iff_dvd_right.1 (show p ∣ (p ::ₘ f).prod by simp)
    haveI := Classical.decEq α
    rw [← Multiset.cons_erase hbg]
    exact
      Multiset.Rel.cons hb
        (ih (fun q hq => hf _ (by simp [hq]))
          (fun {q} (hq : q ∈ g.erase b) => hg q (Multiset.mem_of_mem_erase hq))
          (Associated.of_mul_left
            (by rwa [← Multiset.prod_cons, ← Multiset.prod_cons, Multiset.cons_erase hbg]) hb
            (hf p (by simp)).ne_zero))
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
f : Multiset α
empty :
  ∀ {g : Multiset α},
    (∀ (x : α), Membership.mem (γ := Multiset α) 0 x → Prime x) →
      (∀ x ∈ g, Prime x) → Multiset.prod 0 ~ᵤ g.prod → Multiset.Rel Associated 0 g
⊢ ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
have cons : ∀ (p : α) (f : Multiset α)
  (ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g)
  {g : Multiset α},
  (∀ x ∈ p ::ₘ f, Prime x) → (∀ x ∈ g, Prime x) → (p ::ₘ f).prod ~ᵤ g.prod → Multiset.Rel Associated (p ::ₘ f) g
Tactic: induction f using Multiset.induction_on with
  | empty =>
    intro g _ hg h
    exact Multiset.rel_zero_left.2 <|
      Multiset.eq_zero_of_forall_notMem fun x hx =>
        have : IsUnit g.prod := by simpa [associated_one_iff_isUnit] using h.symm
        (hg x hx).not_unit <|
          isUnit_iff_dvd_one.2 <| (Multiset.dvd_prod hx).trans (isUnit_iff_dvd_one.1 this)
  | cons p f ih =>
    intro g hf hg hfg
    let ⟨b, hbg, hb⟩ :=
      (exists_associated_mem_of_dvd_prod (hf p (by simp)) fun q hq => hg _ hq) <|
        hfg.dvd_iff_dvd_right.1 (show p ∣ (p ::ₘ f).prod by simp)
    haveI := Classical.decEq α
    rw [← Multiset.cons_erase hbg]
    exact
      Multiset.Rel.cons hb
        (ih (fun q hq => hf _ (by simp [hq]))
          (fun {q} (hq : q ∈ g.erase b) => hg q (Multiset.mem_of_mem_erase hq))
          (Associated.of_mul_left
            (by rwa [← Multiset.prod_cons, ← Multiset.prod_cons, Multiset.cons_erase hbg]) hb
            (hf p (by simp)).ne_zero))
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
⊢ (factors a).card = (factors b).card
have pos : ∀ (hb : b = 0), (factors a).card = (factors b).card
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
pos : ∀ (hb : b = 0), (factors a).card = (factors b).card
⊢ (factors a).card = (factors b).card
have neg : ∀ (hb : ¬b = 0), (factors a).card = (factors b).card
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : ¬b = 0
⊢ (factors a).card = (factors b).card
have ha : a ≠ 0
Tactic: have ha : a ≠ 0 := h.ne_zero_iff.mpr hb
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : ¬b = 0
ha : a ≠ 0
⊢ (factors a).card = (factors b).card
have neg : Multiset.Rel Associated (factors a) (factors b)
Tactic: apply Multiset.card_eq_card_of_rel
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : ¬b = 0
ha : a ≠ 0
neg : Multiset.Rel Associated (factors a) (factors b)
⊢ (factors a).card = (factors b).card
have neg₁ : α → α → Prop
Tactic: apply Multiset.card_eq_card_of_rel
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
⊢ ∃ (p : α), a ~ᵤ p ∧ f = {p}
have haveI : ∀ (this : DecidableEq α), ∃ (p : α), a ~ᵤ p ∧ f = {p}
Tactic: haveI := Classical.decEq α
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
⊢ ∃ (p : α), a ~ᵤ p ∧ f = {p}
have refine_1 : (fun (g : Multiset α) ↦ g.prod ~ᵤ a → (∀ b ∈ g, Prime b) → ∃ (p : α), a ~ᵤ p ∧ g = {p}) 0
Tactic: refine @Multiset.induction_on _
    (fun g => (g.prod ~ᵤ a) → (∀ b ∈ g, Prime b) → ∃ p, a ~ᵤ p ∧ g = {p}) f ?_ ?_ pfa.2 pfa.1
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
refine_1 :
  Multiset.prod 0 ~ᵤ a →
    (∀ (b : α), Membership.mem (γ := Multiset α) 0 b → Prime b) → ∃ (p : α), a ~ᵤ p ∧ Eq (α := Multiset α) 0 {p}
⊢ ∃ (p : α), a ~ᵤ p ∧ f = {p}
have refine_2 : ∀ (a_1 : α) (s : Multiset α),
  (fun (g : Multiset α) ↦ g.prod ~ᵤ a → (∀ b ∈ g, Prime b) → ∃ (p : α), a ~ᵤ p ∧ g = {p}) s →
    (fun (g : Multiset α) ↦ g.prod ~ᵤ a → (∀ b ∈ g, Prime b) → ∃ (p : α), a ~ᵤ p ∧ g = {p}) (a_1 ::ₘ s)
Tactic: refine @Multiset.induction_on _
    (fun g => (g.prod ~ᵤ a) → (∀ b ∈ g, Prime b) → ∃ p, a ~ᵤ p ∧ g = {p}) f ?_ ?_ pfa.2 pfa.1
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
h : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ (p : α), a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * (↑u : α) = a
hs : ∀ b ∈ p ::ₘ s, Prime b
⊢ ∃ (p_1 : α), a ~ᵤ p_1 ∧ p ::ₘ s = {p_1}
have h : a ~ᵤ p ∧ p ::ₘ s = {p}
Tactic: use p
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
h : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ (p : α), a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * (↑u : α) = a
hs : ∀ b ∈ p ::ₘ s, Prime b
⊢ s = 0
have by_contra : ∀ (hs0 : ¬s = 0), False
Tactic: by_contra hs0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
h : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ (p : α), a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * (↑u : α) = a
hs : ∀ b ∈ p ::ₘ s, Prime b
hs0 : ¬s = 0
⊢ False
have obtain : ∀ (q : α) (hq : q ∈ s), False
Tactic: obtain ⟨q, hq⟩ := Multiset.exists_mem_of_ne_zero hs0