awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * (↑u : α) ≠ 0
hnu : ¬IsUnit (f.prod * (↑u : α))
b : α
h : b ∈ f
⊢ ∃ (f_1 : Multiset α), (∀ b ∈ f_1, Irreducible b) ∧ f_1.prod = f.prod * (↑u : α) ∧ f_1 ≠ ∅
have refine_1 : ∀ (a : α) (ha : a ∈ b * (↑u : α) ::ₘ f.erase b), Irreducible a
Tactic: classical
      refine ⟨(f.erase b).cons (b * u), fun a ha => ?_, ?_, Multiset.cons_ne_zero⟩
      · obtain rfl | ha := Multiset.mem_cons.1 ha
        exacts [Associated.irreducible ⟨u, rfl⟩ (hi b h), hi a (Multiset.mem_of_mem_erase ha)]
      · rw [Multiset.prod_cons, mul_comm b, mul_assoc, Multiset.prod_erase h, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * (↑u : α) ≠ 0
hnu : ¬IsUnit (f.prod * (↑u : α))
b : α
h : b ∈ f
refine_1 : ∀ (a : α) (ha : a ∈ b * (↑u : α) ::ₘ f.erase b), Irreducible a
⊢ ∃ (f_1 : Multiset α), (∀ b ∈ f_1, Irreducible b) ∧ f_1.prod = f.prod * (↑u : α) ∧ f_1 ≠ ∅
have refine_2 : (b * (↑u : α) ::ₘ f.erase b).prod = f.prod * (↑u : α)
Tactic: classical
      refine ⟨(f.erase b).cons (b * u), fun a ha => ?_, ?_, Multiset.cons_ne_zero⟩
      · obtain rfl | ha := Multiset.mem_cons.1 ha
        exacts [Associated.irreducible ⟨u, rfl⟩ (hi b h), hi a (Multiset.mem_of_mem_erase ha)]
      · rw [Multiset.prod_cons, mul_comm b, mul_assoc, Multiset.prod_erase h, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
⊢ a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
have simp_rw : a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
Tactic: simp_rw [← UniqueFactorizationMonoid.irreducible_iff_prime]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
⊢ (∃ (p : α), Prime p) ↔ ∃ (x : α), x ≠ 0 ∧ ¬IsUnit x
have refine : (∃ (x : α), x ≠ 0 ∧ ¬IsUnit x) → ∀ (x : α) (hx₀ : x ≠ 0) (hxu : ¬IsUnit x), ∃ (p : α), Prime p
Tactic: refine ⟨fun ⟨p, hp⟩ ↦ ⟨p, hp.ne_zero, hp.not_unit⟩, fun ⟨x, hx₀, hxu⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
h : ∃ (x : α), x ≠ 0 ∧ ¬IsUnit x
x : α
hx₀ : x ≠ 0
hxu : ¬IsUnit x
⊢ ∃ (p : α), Prime p
have obtain : ∀ (f : α) (hf : Irreducible f), ∃ (p : α), Prime p
Tactic: obtain ⟨f, hf, -⟩ := WfDvdMonoid.exists_irreducible_factor hxu hx₀
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
P : α → Prop
a : α
h₁ : P 0
h₂ : ∀ (x : α), IsUnit x → P x
h₃ : ∀ (a p : α), a ≠ 0 → Prime p → P a → P (p * a)
⊢ P a
have h₄ : ∀ (a p : α), a ≠ 0 → Irreducible p → P a → P (p * a)
Tactic: simp_rw [← UniqueFactorizationMonoid.irreducible_iff_prime] at h₃
Cleared hypotheses: h₃
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
⊢ IsPrimal a
have inl : IsPrimal.{u_1} (α := α) 0
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
inl : IsPrimal.{u_1} (α := α) 0
⊢ IsPrimal a
have inr : ∀ (ha : a ≠ 0), IsPrimal a
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : a ≠ 0
⊢ IsPrimal a
have inr : ∀ (f : Multiset α) (hf : ∀ b ∈ f, Prime b) (u : αˣ) (ha : f.prod * (↑u : α) ≠ 0), IsPrimal (f.prod * (↑u : α))
Tactic: obtain ⟨f, hf, u, rfl⟩ := exists_prime_factors a ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (factors a).prod ~ᵤ a
have rw : (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) sorry).prod ~ᵤ a
Tactic: rw [factors, dif_neg ane0]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a x : α
hx : x ∈ factors a
⊢ Prime x
have ane0 : a ≠ 0
Tactic: have ane0 := ne_zero_of_mem_factors hx
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a x : α
hx : x ∈ factors a
ane0 ane0₁ : a ≠ 0
⊢ Prime x
have hx₁ : x ∈ Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) sorry
Tactic: rw [factors, dif_neg ane0] at hx
Cleared hypotheses: hx, ane0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
⊢ (factors a).card = 1
have hf : factors a ≠ 0
Tactic: have hf : factors a ≠ 0 := by
    intro hf
    simpa [hf, Associated.comm, ha.not_isUnit] using factors_prod ha.ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf : factors a ≠ 0
⊢ (factors a).card = 1
have obtain : ∀ (b : α) (hb : b ∈ factors a), (factors a).card = 1
Tactic: obtain ⟨b, hb⟩ := exists_mem_of_ne_zero hf
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf : factors a ≠ 0
b : α
hb : b ∈ factors a
⊢ (factors a).card = 1
have obtain : ∀ (f : Multiset α) (hf : factors a = b ::ₘ f), (factors a).card = 1
Tactic: obtain ⟨f, hf⟩ := exists_cons_of_mem hb
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf_1 : factors a ≠ 0
b : α
hb : b ∈ factors a
f : Multiset α
hf : factors a = b ::ₘ f
⊢ (factors a).card = 1
have rw : ∀ (a : α), a ∉ f
Tactic: rw [hf, card_cons, add_eq_right, card_eq_zero, eq_zero_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf_1 : factors a ≠ 0
b : α
hb : b ∈ factors a
f : Multiset α
hf : factors a = b ::ₘ f
c : α
hc : c ∈ f
⊢ False
have obtain : ∀ (f : Multiset α) (hf : factors a = b ::ₘ c ::ₘ f) (hc : c ∈ c ::ₘ f), False
Tactic: obtain ⟨f, rfl⟩ := exists_cons_of_mem hc
Cleared hypotheses: f, hf, hc
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf_1 : factors a ≠ 0
b : α
hb : b ∈ factors a
c : α
f : Multiset α
hf : factors a = b ::ₘ c ::ₘ f
hc : c ∈ c ::ₘ f
⊢ False
have hb₁ : ¬IsUnit b
Tactic: replace hb := (irreducible_of_factor b hb).not_isUnit
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Defs (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf_1 : factors a ≠ 0
b c : α
f : Multiset α
hf : factors a = b ::ₘ c ::ₘ f
hc : c ∈ c ::ₘ f
hb : ¬IsUnit b
⊢ False
have hc₁ : ¬IsUnit c
Tactic: replace hc := (irreducible_of_factor c (hf ▸ mem_cons_of_mem hc)).not_isUnit
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a b : Multiset { a : Associates α // Irreducible a }
⊢ (↑(a + b) : WithTop (Multiset { a : Associates α // Irreducible a })) =
    (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) +
      (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
have norm_cast : a + b = a + b
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : DecidableEq (Associates α)
a b : Multiset { a : Associates α // Irreducible a }
⊢ (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) ⊔
        (↑b : WithTop (Multiset { a : Associates α // Irreducible a })) +
      (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) ⊓
        (↑b : WithTop (Multiset { a : Associates α // Irreducible a })) =
    (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) +
      (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
have rw : a ⊔ b + a ⊓ b = a + b
Tactic: rw [← WithTop.coe_sup, ← WithTop.coe_inf, ← WithTop.coe_add, ← WithTop.coe_add,
        WithTop.coe_eq_coe]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a b : Multiset { a : Associates α // Irreducible a }
⊢ ((↑a : WithTop (Multiset { a : Associates α // Irreducible a })) +
        (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))).prod =
    FactorSet.prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) *
      FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
have rw : FactorSet.prod (↑(a + b) : WithTop (Multiset { a : Associates α // Irreducible a })) =
  FactorSet.prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) *
    FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
Tactic: rw [← FactorSet.coe_add, prod_coe, prod_coe, prod_coe, Multiset.map_add, Multiset.prod_add]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a b : Multiset { a : Associates α // Irreducible a }
rw :
  FactorSet.prod (↑(a + b) : WithTop (Multiset { a : Associates α // Irreducible a })) =
    FactorSet.prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) *
      FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
⊢ ((↑a : WithTop (Multiset { a : Associates α // Irreducible a })) +
        (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))).prod =
    FactorSet.prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) *
      FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
have rw₁ : (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) (a + b)).prod =
  FactorSet.prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) *
    FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
Tactic: rw [← FactorSet.coe_add, prod_coe, prod_coe, prod_coe, Multiset.map_add, Multiset.prod_add]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a b : Multiset { a : Associates α // Irreducible a }
rw :
  FactorSet.prod (↑(a + b) : WithTop (Multiset { a : Associates α // Irreducible a })) =
    FactorSet.prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) *
      FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
rw₁ :
  (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) (a + b)).prod =
    FactorSet.prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) *
      FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
⊢ ((↑a : WithTop (Multiset { a : Associates α // Irreducible a })) +
        (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))).prod =
    FactorSet.prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) *
      FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
have rw₂ : (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) (a + b)).prod =
  (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a).prod *
    FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
Tactic: rw [← FactorSet.coe_add, prod_coe, prod_coe, prod_coe, Multiset.map_add, Multiset.prod_add]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a b : Multiset { a : Associates α // Irreducible a }
rw :
  FactorSet.prod (↑(a + b) : WithTop (Multiset { a : Associates α // Irreducible a })) =
    FactorSet.prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) *
      FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
rw₁ :
  (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) (a + b)).prod =
    FactorSet.prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) *
      FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
rw₂ :
  (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) (a + b)).prod =
    (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a).prod *
      FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
⊢ ((↑a : WithTop (Multiset { a : Associates α // Irreducible a })) +
        (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))).prod =
    FactorSet.prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) *
      FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
have rw₃ : (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) (a + b)).prod =
  (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a).prod *
    (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) b).prod
Tactic: rw [← FactorSet.coe_add, prod_coe, prod_coe, prod_coe, Multiset.map_add, Multiset.prod_add]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a b : Multiset { a : Associates α // Irreducible a }
rw :
  FactorSet.prod (↑(a + b) : WithTop (Multiset { a : Associates α // Irreducible a })) =
    FactorSet.prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) *
      FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
rw₁ :
  (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) (a + b)).prod =
    FactorSet.prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) *
      FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
rw₂ :
  (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) (a + b)).prod =
    (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a).prod *
      FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
rw₃ :
  (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) (a + b)).prod =
    (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a).prod *
      (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) b).prod
⊢ ((↑a : WithTop (Multiset { a : Associates α // Irreducible a })) +
        (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))).prod =
    FactorSet.prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) *
      FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
have rw₄ : (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a +
      Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) b).prod =
  (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a).prod *
    (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) b).prod
Tactic: rw [← FactorSet.coe_add, prod_coe, prod_coe, prod_coe, Multiset.map_add, Multiset.prod_add]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a b : Multiset { a : Associates α // Irreducible a }
rw :
  FactorSet.prod (↑(a + b) : WithTop (Multiset { a : Associates α // Irreducible a })) =
    FactorSet.prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) *
      FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
rw₁ :
  (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) (a + b)).prod =
    FactorSet.prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) *
      FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
rw₂ :
  (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) (a + b)).prod =
    (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a).prod *
      FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
rw₃ :
  (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) (a + b)).prod =
    (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a).prod *
      (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) b).prod
rw₄ :
  (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a +
        Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) b).prod =
    (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a).prod *
      (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) b).prod
⊢ ((↑a : WithTop (Multiset { a : Associates α // Irreducible a })) +
        (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))).prod =
    FactorSet.prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) *
      FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
have rw₅ : (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a).prod *
    (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) b).prod =
  (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a).prod *
    (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) b).prod
Tactic: rw [← FactorSet.coe_add, prod_coe, prod_coe, prod_coe, Multiset.map_add, Multiset.prod_add]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
b : FactorSet α
h : ⊤ ≤ b
⊢ FactorSet.prod ⊤ ≤ b.prod
have this : b = ⊤
Tactic: have : b = ⊤ := top_unique h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
b : FactorSet α
h : ⊤ ≤ b
this : b = ⊤
⊢ FactorSet.prod ⊤ ≤ b.prod
have rw : LE.le.{u_1} (α := Associates α) (FactorSet.prod ⊤) (FactorSet.prod ⊤)
Tactic: rw [this, prod_top]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
b : FactorSet α
h : ⊤ ≤ b
this : b = ⊤
rw : LE.le.{u_1} (α := Associates α) (FactorSet.prod ⊤) (FactorSet.prod ⊤)
⊢ FactorSet.prod ⊤ ≤ b.prod
have rw₁ : LE.le.{u_1} (α := Associates α) 0 0
Tactic: rw [this, prod_top]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : Nontrivial α
p : WithTop (Multiset { a : Associates α // Irreducible a })
⊢ prod p = 0 ↔ p = ⊤
have top : Eq.{u_1 + 1} (α := Associates α) (prod ⊤) 0 ↔ Eq.{u_1 + 1} (α := FactorSet α) ⊤ ⊤
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : Nontrivial α
p : WithTop (Multiset { a : Associates α // Irreducible a })
top : Eq.{u_1 + 1} (α := Associates α) (prod ⊤) 0 ↔ Eq.{u_1 + 1} (α := FactorSet α) ⊤ ⊤
⊢ prod p = 0 ↔ p = ⊤
have coe : ∀ (a : Multiset { a : Associates α // Irreducible a }),
  prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = 0 ↔
    (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = ⊤
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : Nontrivial α
a : Multiset { a : Associates α // Irreducible a }
⊢ prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = 0 ↔
    (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = ⊤
have coe : ∀ (x : { a : Associates α // Irreducible a }), ¬(x ∈ a ∧ (↑x : Associates α) = 0)
Tactic: rw [prod_coe, Multiset.prod_eq_zero_iff, Multiset.mem_map, eq_false WithTop.coe_ne_top,
      iff_false, not_exists]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
p : Associates α
hp : Irreducible p
⊢ if hp : Irreducible p then BfactorSetMem (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) ⊤ else False
have split_ifs : BfactorSetMem (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) ⊤
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
p : Associates α
hp : Irreducible p
l : Multiset { a : Associates α // Irreducible a }
⊢ (if hp : Irreducible p then
      BfactorSetMem (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp)
        (↑l : WithTop (Multiset { a : Associates α // Irreducible a }))
    else False) ↔
    l.Mem (Subtype.mk (p := Irreducible) p hp)
have split_ifs : BfactorSetMem (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp)
    (↑l : WithTop (Multiset { a : Associates α // Irreducible a })) ↔
  l.Mem (Subtype.mk (p := Irreducible) p hp)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
p : Associates α
hp : ¬Irreducible p
s : FactorSet α
h : p ∈ s
⊢ False
have rwa : ∀ (h : FactorSetMem s p), False
Tactic: rwa [← factorSetMem_eq_mem, FactorSetMem, dif_neg hp] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
p : Associates α
hp : ¬Irreducible p
s : FactorSet α
h : p ∈ s
rwa : ∀ (h : FactorSetMem s p), False
⊢ False
have rwa₁ : ∀
  (h :
    if hp : Irreducible p then BfactorSetMem (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) s
    else False),
  False
Tactic: rwa [← factorSetMem_eq_mem, FactorSetMem, dif_neg hp] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
p : Associates α
hp : ¬Irreducible p
s : FactorSet α
h : p ∈ s
rwa : ∀ (h : FactorSetMem s p), False
rwa₁ :
  ∀
    (h :
      if hp : Irreducible p then BfactorSetMem (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) s
      else False),
    False
⊢ False
have rwa₂ : ∀ (h : False), False
Tactic: rwa [← factorSetMem_eq_mem, FactorSetMem, dif_neg hp] at h
Cleared hypotheses: h
-- 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
⊢ p = q
have top : ∀ (h : prod ⊤ = prod q), ⊤ = q
Tactic: induction p
Cleared hypotheses: p, h