awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
p q : WithTop (Multiset { a : Associates α // Irreducible a })
h : prod p = prod q
top : ∀ (h : prod ⊤ = prod q), ⊤ = q
⊢ p = q
have coe : ∀ (a : Multiset { a : Associates α // Irreducible a })
  (h : prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = prod q),
  (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = q
Tactic: induction p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
q : WithTop (Multiset { a : Associates α // Irreducible a })
h : prod ⊤ = prod q
⊢ ⊤ = q
have top : ∀ (h : Eq.{u_1 + 1} (α := Associates α) (prod ⊤) (prod ⊤)), Eq.{u_1 + 1} (α := FactorSet α) ⊤ ⊤
Tactic: induction q
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
q : WithTop (Multiset { a : Associates α // Irreducible a })
h : prod ⊤ = prod q
top : ∀ (h : Eq.{u_1 + 1} (α := Associates α) (prod ⊤) (prod ⊤)), Eq.{u_1 + 1} (α := FactorSet α) ⊤ ⊤
⊢ ⊤ = q
have top₁ : ∀ (a : Multiset { a : Associates α // Irreducible a })
  (h : prod ⊤ = prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a }))),
  ⊤ = (↑a : WithTop (Multiset { a : Associates α // Irreducible a }))
Tactic: induction q
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
q : WithTop (Multiset { a : Associates α // Irreducible a })
a : Multiset { a : Associates α // Irreducible a }
h : prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = prod q
⊢ (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = q
have coe : ∀ (h : prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = prod ⊤),
  (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = ⊤
Tactic: induction q
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
q : WithTop (Multiset { a : Associates α // Irreducible a })
a : Multiset { a : Associates α // Irreducible a }
h : prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = prod q
coe :
  ∀ (h : prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = prod ⊤),
    (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = ⊤
⊢ (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = q
have coe₁ : ∀ (a_1 : Multiset { a : Associates α // Irreducible a })
  (h :
    prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) =
      prod (↑a_1 : WithTop (Multiset { a : Associates α // Irreducible a }))),
  (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) =
    (↑a_1 : WithTop (Multiset { a : Associates α // Irreducible a }))
Tactic: induction q
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
a : Multiset { a : Associates α // Irreducible a }
h : prod ⊤ = prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a }))
⊢ ⊤ = (↑a : WithTop (Multiset { a : Associates α // Irreducible a }))
have top : (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = ⊤
Tactic: rw [eq_comm, ← FactorSet.prod_eq_zero_iff, ← h, Associates.prod_top]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
a : Multiset { a : Associates α // Irreducible a }
h : prod ⊤ = prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a }))
top : (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = ⊤
⊢ ⊤ = (↑a : WithTop (Multiset { a : Associates α // Irreducible a }))
have top₁ : prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = 0
Tactic: rw [eq_comm, ← FactorSet.prod_eq_zero_iff, ← h, Associates.prod_top]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
a : Multiset { a : Associates α // Irreducible a }
h : prod ⊤ = prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a }))
top : (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = ⊤
top₁ : prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = 0
⊢ ⊤ = (↑a : WithTop (Multiset { a : Associates α // Irreducible a }))
have top₂ : Eq.{u_1 + 1} (α := Associates α) (prod ⊤) 0
Tactic: rw [eq_comm, ← FactorSet.prod_eq_zero_iff, ← h, Associates.prod_top]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
a : Multiset { a : Associates α // Irreducible a }
h : prod ⊤ = prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a }))
top : (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = ⊤
top₁ : prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = 0
top₂ : Eq.{u_1 + 1} (α := Associates α) (prod ⊤) 0
⊢ ⊤ = (↑a : WithTop (Multiset { a : Associates α // Irreducible a }))
have top₃ : Eq.{u_1 + 1} (α := Associates α) 0 0
Tactic: rw [eq_comm, ← FactorSet.prod_eq_zero_iff, ← h, Associates.prod_top]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
a : Multiset { a : Associates α // Irreducible a }
h : prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = prod ⊤
⊢ (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = ⊤
have coe : prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = 0
Tactic: rw [← FactorSet.prod_eq_zero_iff, h, Associates.prod_top]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
a : Multiset { a : Associates α // Irreducible a }
h : prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = prod ⊤
coe : prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = 0
⊢ (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = ⊤
have coe₁ : Eq.{u_1 + 1} (α := Associates α) (prod ⊤) 0
Tactic: rw [← FactorSet.prod_eq_zero_iff, h, Associates.prod_top]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
a : Multiset { a : Associates α // Irreducible a }
h : prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = prod ⊤
coe : prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = 0
coe₁ : Eq.{u_1 + 1} (α := Associates α) (prod ⊤) 0
⊢ (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = ⊤
have coe₂ : Eq.{u_1 + 1} (α := Associates α) 0 0
Tactic: rw [← FactorSet.prod_eq_zero_iff, h, Associates.prod_top]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
a a_1 : Multiset { a : Associates α // Irreducible a }
h :
  prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) =
    prod (↑a_1 : WithTop (Multiset { a : Associates α // Irreducible a }))
⊢ (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) =
    (↑a_1 : WithTop (Multiset { a : Associates α // Irreducible a }))
have coe : a = a_1
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
a a_1 : Multiset { a : Associates α // Irreducible a }
h :
  prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) =
    prod (↑a_1 : WithTop (Multiset { a : Associates α // Irreducible a }))
⊢ a = a_1
have coe : Eq (α := Multiset (Associates α))
  (Multiset.map (fun (a : { a : Associates α // Irreducible a }) ↦ (↑a : Associates α)) a)
  (Multiset.map (fun (a : { a : Associates α // Irreducible a }) ↦ (↑a : Associates α)) a_1)
Tactic: rw [← Multiset.map_eq_map Subtype.coe_injective]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
a a_1 : Multiset { a : Associates α // Irreducible a }
h :
  prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) =
    prod (↑a_1 : WithTop (Multiset { a : Associates α // Irreducible a }))
⊢ Eq (α := Multiset (Associates α))
    (Multiset.map (fun (a : { a : Associates α // Irreducible a }) ↦ (↑a : Associates α)) a)
    (Multiset.map (fun (a : { a : Associates α // Irreducible a }) ↦ (↑a : Associates α)) a_1)
have apply : ∀ a_2 ∈ Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a, Irreducible a_2
Tactic: apply unique' _ _ h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
a a_1 : Multiset { a : Associates α // Irreducible a }
h :
  prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) =
    prod (↑a_1 : WithTop (Multiset { a : Associates α // Irreducible a }))
apply : ∀ a_2 ∈ Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a, Irreducible a_2
⊢ Eq (α := Multiset (Associates α))
    (Multiset.map (fun (a : { a : Associates α // Irreducible a }) ↦ (↑a : Associates α)) a)
    (Multiset.map (fun (a : { a : Associates α // Irreducible a }) ↦ (↑a : Associates α)) a_1)
have apply₁ : ∀ a ∈ Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a_1, Irreducible a
Tactic: apply unique' _ _ h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
a_1 a_2 : Multiset { a : Associates α // Irreducible a }
h :
  prod (↑a_1 : WithTop (Multiset { a : Associates α // Irreducible a })) =
    prod (↑a_2 : WithTop (Multiset { a : Associates α // Irreducible a }))
a : Associates α
ha : a ∈ Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a_1
⊢ Irreducible a
have obtain : ∀ (a' : Associates α) (irred : Irreducible a')
  (ha :
    (↑(Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) a' irred) : Associates α) ∈
      Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a_1),
  Irreducible (↑(Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) a' irred) : Associates α)
Tactic: obtain ⟨⟨a', irred⟩, -, rfl⟩ := Multiset.mem_map.mp ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
a_1 a_2 : Multiset { a : Associates α // Irreducible a }
h :
  prod (↑a_1 : WithTop (Multiset { a : Associates α // Irreducible a })) =
    prod (↑a_2 : WithTop (Multiset { a : Associates α // Irreducible a }))
a : Associates α
ha : a ∈ Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a_2
⊢ Irreducible a
have obtain : ∀ (a' : Associates α) (irred : Irreducible a')
  (ha :
    (↑(Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) a' irred) : Associates α) ∈
      Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a_2),
  Irreducible (↑(Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) a' irred) : Associates α)
Tactic: obtain ⟨⟨a', irred⟩, -, rfl⟩ := Multiset.mem_map.mp ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
⊢ Eq (α := Multiset { a : Associates α // Irreducible a }) (factors' a) (factors' b)
have inl : ∀ (h : a ~ᵤ 0), Eq (α := Multiset { a : Associates α // Irreducible a }) (factors' a) (factors' 0)
Tactic: obtain rfl | hb := eq_or_ne b 0
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
inl : ∀ (h : a ~ᵤ 0), Eq (α := Multiset { a : Associates α // Irreducible a }) (factors' a) (factors' 0)
⊢ Eq (α := Multiset { a : Associates α // Irreducible a }) (factors' a) (factors' b)
have inr : ∀ (hb : b ≠ 0), Eq (α := Multiset { a : Associates α // Irreducible a }) (factors' a) (factors' b)
Tactic: obtain rfl | hb := eq_or_ne b 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
h : a ~ᵤ 0
⊢ Eq (α := Multiset { a : Associates α // Irreducible a }) (factors' a) (factors' 0)
have h₁ : a = 0
Tactic: rw [associated_zero_iff_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
h : a = 0
⊢ Eq (α := Multiset { a : Associates α // Irreducible a }) (factors' a) (factors' 0)
have inl : Eq.{u_1 + 1} (α := Multiset { a : Associates α // Irreducible a }) (factors' 0) (factors' 0)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : b ≠ 0
⊢ a ≠ 0
have contrapose : ∀ (ha : a = 0), b = 0
Tactic: contrapose hb with ha
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
ha : a = 0
⊢ b = 0
have rw : b ~ᵤ a
Tactic: rw [← associated_zero_iff_eq_zero, ← ha]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : b ≠ 0
⊢ Eq (α := Multiset { a : Associates α // Irreducible a }) (factors' a) (factors' b)
have ha : a ≠ 0
Tactic: have ha : a ≠ 0 := by
    contrapose hb with ha
    rw [← associated_zero_iff_eq_zero, ← ha]
    exact h.symm
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : b ≠ 0
ha : a ≠ 0
⊢ Eq (α := Multiset { a : Associates α // Irreducible a }) (factors' a) (factors' b)
have inr : Rel Associated (factors a) (factors b)
Tactic: rw [← Multiset.map_eq_map Subtype.coe_injective, map_subtype_coe_factors',
    map_subtype_coe_factors', ← rel_associated_iff_map_eq_map]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : Associates α
⊢ FactorSet α
have refine : ∀ (h : ¬a = 0) (a b : α) (p : a ≈ b),
  HEq.{u_1 + 1} (α := ¬⟦a⟧ = 0 → FactorSet α) fun (x : ¬⟦a⟧ = 0) ↦
    (↑(factors' a) : WithTop (Multiset { a : Associates α // Irreducible a })) (β := ¬⟦b⟧ = 0 → FactorSet α)
    fun (x : ¬⟦b⟧ = 0) ↦ (↑(factors' b) : WithTop (Multiset { a : Associates α // Irreducible a }))
Tactic: refine if h : a = 0 then ⊤ else Quotient.hrecOn a (fun x _ => factors' x) ?_ h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : Associates α
⊢ FactorSet α
have classical : ∀ (h : ¬a = 0) (a b : α) (p : a ≈ b),
  HEq.{u_1 + 1} (α := ¬⟦a⟧ = 0 → FactorSet α) fun (x : ¬⟦a⟧ = 0) ↦
    (↑(factors' a) : WithTop (Multiset { a : Associates α // Irreducible a })) (β := ¬⟦b⟧ = 0 → FactorSet α)
    fun (x : ¬⟦b⟧ = 0) ↦ (↑(factors' b) : WithTop (Multiset { a : Associates α // Irreducible a }))
Tactic: classical refine if h : a = 0 then ⊤ else Quotient.hrecOn a (fun x _ => factors' x) ?_ h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a_1 : Associates α
h : ¬a_1 = 0
a b : α
hab : a ≈ b
⊢ HEq.{u_1 + 1} (α := ¬⟦a⟧ = 0 → FactorSet α) fun (x : ¬⟦a⟧ = 0) ↦
    (↑(factors' a) : WithTop (Multiset { a : Associates α // Irreducible a })) (β := ¬⟦b⟧ = 0 → FactorSet α)
    fun (x : ¬⟦b⟧ = 0) ↦ (↑(factors' b) : WithTop (Multiset { a : Associates α // Irreducible a }))
have hα : (¬⟦a⟧ = 0) = ¬⟦b⟧ = 0
Tactic: apply Function.hfunext
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a_1 : Associates α
h : ¬a_1 = 0
a b : α
hab : a ≈ b
hα : (¬⟦a⟧ = 0) = ¬⟦b⟧ = 0
⊢ HEq.{u_1 + 1} (α := ¬⟦a⟧ = 0 → FactorSet α) fun (x : ¬⟦a⟧ = 0) ↦
    (↑(factors' a) : WithTop (Multiset { a : Associates α // Irreducible a })) (β := ¬⟦b⟧ = 0 → FactorSet α)
    fun (x : ¬⟦b⟧ = 0) ↦ (↑(factors' b) : WithTop (Multiset { a : Associates α // Irreducible a }))
have h₁ : ∀ (a_2 : ¬⟦a⟧ = 0) (a' : ¬⟦b⟧ = 0),
  a_2 ≍ a' →
    HEq (α := WithTop (Multiset { a : Associates α // Irreducible a }))
      (↑(factors' a) : WithTop (Multiset { a : Associates α // Irreducible a })) (β :=
      WithTop (Multiset { a : Associates α // Irreducible a }))
      (↑(factors' b) : WithTop (Multiset { a : Associates α // Irreducible a }))
Tactic: apply Function.hfunext
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a_1 : Associates α
h : ¬a_1 = 0
a b : α
hab : a ≈ b
⊢ (¬⟦a⟧ = 0) = ¬⟦b⟧ = 0
have this : a ~ᵤ 0 ↔ b ~ᵤ 0
Tactic: have : a ~ᵤ 0 ↔ b ~ᵤ 0 := Iff.intro (fun ha0 => hab.symm.trans ha0) fun hb0 => hab.trans hb0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a_1 : Associates α
h : ¬a_1 = 0
a b : α
hab : a ≈ b
this : a ~ᵤ 0 ↔ b ~ᵤ 0
⊢ (¬⟦a⟧ = 0) = ¬⟦b⟧ = 0
have this₁ : a = 0 ↔ b = 0
Tactic: simp only [associated_zero_iff_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
h : a ≠ 0
⊢ Eq (α := FactorSet α) (factors (Associates.mk a))
    (↑(factors' a) : WithTop (Multiset { a : Associates α // Irreducible a }))
have hnc : ¬Eq (α := Associates α) (Associates.mk a) 0
Tactic: apply dif_neg
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
h : a ≠ 0
⊢ Eq (α := FactorSet α) (factors (Associates.mk a))
    (↑(factors' a) : WithTop (Multiset { a : Associates α // Irreducible a }))
have hnc : ¬Eq (α := Associates α) (Associates.mk a) 0
Tactic: classical
    apply dif_neg
    apply mt mk_eq_zero.1 h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : Associates α
⊢ a.factors.prod = a
have rcases : ∀ (a : α), Eq (α := Associates α) (FactorSet.prod (factors (Associates.mk a))) (Associates.mk a)
Tactic: rcases Associates.mk_surjective a with ⟨a, rfl⟩
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
⊢ Eq (α := Associates α) (FactorSet.prod (factors (Associates.mk a))) (Associates.mk a)
have inl : Eq.{u_1 + 1} (α := Associates α) (FactorSet.prod (factors (Associates.mk 0))) (Associates.mk 0)
Tactic: rcases eq_or_ne a 0 with rfl | ha
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
inl : Eq.{u_1 + 1} (α := Associates α) (FactorSet.prod (factors (Associates.mk 0))) (Associates.mk 0)
⊢ Eq (α := Associates α) (FactorSet.prod (factors (Associates.mk a))) (Associates.mk a)
have inr : ∀ (ha : a ≠ 0), Eq (α := Associates α) (FactorSet.prod (factors (Associates.mk a))) (Associates.mk a)
Tactic: rcases eq_or_ne a 0 with rfl | ha
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Subsingleton α
a : Associates α
⊢ a.factors = ⊤
have this : Subsingleton.{u_1 + 1} (Associates α)
Tactic: have : Subsingleton (Associates α) := inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : Associates α
⊢ a.factors = ⊤ ↔ a = 0
have a₁ : Nontrivial α
Tactic: nontriviality α
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : Associates α
h_1 : Nontrivial α
h : a.factors = ⊤
⊢ a = 0
have rwa : a.factors.prod = 0
Tactic: rwa [← factors_prod a, FactorSet.prod_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : Associates α
⊢ (∃ (s : Multiset { p : Associates α // Irreducible p }),
      a.factors = (↑s : WithTop (Multiset { p : Associates α // Irreducible p }))) ↔
    a ≠ 0
have simp_rw : a.factors ≠ ⊤ ↔ a ≠ 0
Tactic: simp_rw [@eq_comm _ a.factors, ← WithTop.ne_top_iff_exists]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors = b.factors
⊢ a.factors.prod = b.factors.prod
have rw : b.factors.prod = b.factors.prod
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors = b.factors
⊢ a = b
have this : a.factors.prod = b.factors.prod
Tactic: have : a.factors.prod = b.factors.prod := by rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors = b.factors
this : a.factors.prod = b.factors.prod
⊢ a = b
have rwa : ∀ (this : a = b.factors.prod), a = b
Tactic: rwa [factors_prod, factors_prod] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors = b.factors
this : a.factors.prod = b.factors.prod
rwa : ∀ (this : a = b.factors.prod), a = b
⊢ a = b
have rwa₁ : ∀ (this : a = b), a = b
Tactic: rwa [factors_prod, factors_prod] at this
Cleared hypotheses: this