awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
refine_1 : α → ℕ∞
refine_2 refine_2₁ :
  ∀ {a b : α},
    DvdNotUnit a b →
      LT.lt (α := ℕ∞)
        (if h : a = 0 then ⊤
        else (↑(Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯).card : ℕ∞))
        (if h : b = 0 then ⊤
        else (↑(Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ b) ⋯).card : ℕ∞))
⊢ WellFounded.{u_1 + 1} (α := α) DvdNotUnit
have refine_2₂ : ∀ {a b : α} (ane0 : a ≠ 0) (c : α) (hc : ¬IsUnit c) (b_eq : b = a * c),
  LT.lt (α := ℕ∞)
    (if h : a = 0 then ⊤
    else (↑(Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) sorry).card : ℕ∞))
    (if h : b = 0 then ⊤
    else (↑(Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ b) sorry).card : ℕ∞))
Tactic: classical
      refine RelHomClass.wellFounded
        (RelHom.mk ?_ ?_ : (DvdNotUnit : α → α → Prop) →r ((· < ·) : ℕ∞ → ℕ∞ → Prop)) wellFounded_lt
      · intro a
        by_cases h : a = 0
        · exact ⊤
        exact ↑(Multiset.card (Classical.choose (pf a h)))
      rintro a b ⟨ane0, ⟨c, hc, b_eq⟩⟩
      rw [dif_neg ane0]
      by_cases h : b = 0
      · simp [h, lt_top_iff_ne_top]
      · rw [dif_neg h, Nat.cast_lt]
        have cne0 : c ≠ 0 := by
          refine mt (fun con => ?_) h
          rw [b_eq, con, mul_zero]
        calc
          Multiset.card (Classical.choose (pf a ane0)) <
              _ + Multiset.card (Classical.choose (pf c cne0)) :=
            lt_add_of_pos_right _
              (Multiset.card_pos.mpr fun con => hc (associated_one_iff_isUnit.mp ?_))
          _ = Multiset.card (Classical.choose (pf a ane0) + Classical.choose (pf c cne0)) :=
            (Multiset.card_add _ _).symm
          _ = Multiset.card (Classical.choose (pf b h)) :=
            Multiset.card_eq_card_of_rel
            (prime_factors_unique ?_ (Classical.choose_spec (pf _ h)).1 ?_)
        · convert! (Classical.choose_spec (pf c cne0)).2.symm
          rw [con, Multiset.prod_zero]
        · intro x hadd
          rw [Multiset.mem_add] at hadd
          rcases hadd with h | h <;> apply (Classical.choose_spec (pf _ _)).1 _ h <;> assumption
        · rw [Multiset.prod_add]
          trans a * c
          · apply Associated.mul_mul <;> apply (Classical.choose_spec (pf _ _)).2 <;> assumption
          · rw [← b_eq]
            apply (Classical.choose_spec (pf _ _)).2.symm; assumption
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
refine_1 : α → ℕ∞
refine_2 refine_2₁ :
  ∀ {a b : α},
    DvdNotUnit a b →
      LT.lt (α := ℕ∞)
        (if h : a = 0 then ⊤
        else (↑(Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯).card : ℕ∞))
        (if h : b = 0 then ⊤
        else (↑(Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ b) ⋯).card : ℕ∞))
refine_2₂ :
  ∀ {a b : α} (ane0 : a ≠ 0) (c : α) (hc : ¬IsUnit c) (b_eq : b = a * c),
    LT.lt (α := ℕ∞)
      (if h : a = 0 then ⊤
      else (↑(Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯).card : ℕ∞))
      (if h : b = 0 then ⊤
      else (↑(Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ b) ⋯).card : ℕ∞))
⊢ WellFounded.{u_1 + 1} (α := α) DvdNotUnit
have refine_2₃ : ∀ {a b : α} (ane0 : a ≠ 0) (c : α) (hc : ¬IsUnit c) (b_eq : b = a * c),
  LT.lt (α := ℕ∞) (↑(Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) sorry).card : ℕ∞)
    (if h : b = 0 then ⊤
    else (↑(Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ b) sorry).card : ℕ∞))
Tactic: classical
      refine RelHomClass.wellFounded
        (RelHom.mk ?_ ?_ : (DvdNotUnit : α → α → Prop) →r ((· < ·) : ℕ∞ → ℕ∞ → Prop)) wellFounded_lt
      · intro a
        by_cases h : a = 0
        · exact ⊤
        exact ↑(Multiset.card (Classical.choose (pf a h)))
      rintro a b ⟨ane0, ⟨c, hc, b_eq⟩⟩
      rw [dif_neg ane0]
      by_cases h : b = 0
      · simp [h, lt_top_iff_ne_top]
      · rw [dif_neg h, Nat.cast_lt]
        have cne0 : c ≠ 0 := by
          refine mt (fun con => ?_) h
          rw [b_eq, con, mul_zero]
        calc
          Multiset.card (Classical.choose (pf a ane0)) <
              _ + Multiset.card (Classical.choose (pf c cne0)) :=
            lt_add_of_pos_right _
              (Multiset.card_pos.mpr fun con => hc (associated_one_iff_isUnit.mp ?_))
          _ = Multiset.card (Classical.choose (pf a ane0) + Classical.choose (pf c cne0)) :=
            (Multiset.card_add _ _).symm
          _ = Multiset.card (Classical.choose (pf b h)) :=
            Multiset.card_eq_card_of_rel
            (prime_factors_unique ?_ (Classical.choose_spec (pf _ h)).1 ?_)
        · convert! (Classical.choose_spec (pf c cne0)).2.symm
          rw [con, Multiset.prod_zero]
        · intro x hadd
          rw [Multiset.mem_add] at hadd
          rcases hadd with h | h <;> apply (Classical.choose_spec (pf _ _)).1 _ h <;> assumption
        · rw [Multiset.prod_add]
          trans a * c
          · apply Associated.mul_mul <;> apply (Classical.choose_spec (pf _ _)).2 <;> assumption
          · rw [← b_eq]
            apply (Classical.choose_spec (pf _ _)).2.symm; assumption
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
⊢ Irreducible p ↔ Prime p
have pos : ∀ (hp0 : p = 0), Irreducible p ↔ Prime p
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
pos : ∀ (hp0 : p = 0), Irreducible p ↔ Prime p
⊢ Irreducible p ↔ Prime p
have neg : ∀ (hp0 : ¬p = 0), Irreducible p ↔ Prime p
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
⊢ Irreducible p ↔ Prime p
have neg : ∀ (h : Irreducible p), Prime p
Tactic: refine ⟨fun h => ?_, Prime.irreducible⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
⊢ Prime p
have neg : ∀ (f : Multiset α) (hf : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ p), Prime p
Tactic: obtain ⟨f, hf⟩ := pf p hp0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
f : Multiset α
hf : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ p
⊢ Prime p
have neg : ∀ (q : α) (hq : p ~ᵤ q) (hf : (∀ (b : α), Membership.mem (γ := Multiset α) {q} b → Prime b) ∧ Multiset.prod {q} ~ᵤ p),
  Prime p
Tactic: obtain ⟨q, hq, rfl⟩ := prime_factors_irreducible h hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
q : α
hq : p ~ᵤ q
hf : (∀ (b : α), Membership.mem (γ := Multiset α) {q} b → Prime b) ∧ Multiset.prod {q} ~ᵤ p
⊢ Prime p
have neg : Prime q
Tactic: rw [hq.prime_iff]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : CommMonoidWithZero β
e : α ≃* β
hα : UniqueFactorizationMonoid α
⊢ UniqueFactorizationMonoid β
have this : IsCancelMulZero β
Tactic: have := e.isCancelMulZero_iff.mp inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : CommMonoidWithZero β
e : α ≃* β
hα : UniqueFactorizationMonoid α
this : IsCancelMulZero β
⊢ UniqueFactorizationMonoid β
have rw : ∀ (hα : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a) (this : IsCancelMulZero β) (a : β),
  a ≠ 0 → ∃ (f : Multiset β), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
Tactic: rw [UniqueFactorizationMonoid.iff_exists_prime_factors] at hα ⊢
Cleared hypotheses: hα, this
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
h : Eq.{u_1 + 1} (α := α) ((e.symm : (a : β) → α) a : α) (0 : α)
⊢ a = 0
have h₁ : (e : (a : α) → β) 0 = a
Tactic: convert! ← map_zero e
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
⊢ ∃ (f : Multiset β), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
have obtain : ∀ (w : Multiset α) (hp : ∀ b ∈ w, Prime b) (u : αˣ) (h : w.prod * (↑u : α) = (e.symm : (a : β) → α) a),
  ∃ (f : Multiset β), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
Tactic: obtain ⟨w, hp, u, h⟩ :=
    hα (e.symm a) fun h =>
      ha <| by
        convert! ← map_zero e
        simp [← h]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ b ∈ w, Prime b
u : αˣ
h : w.prod * (↑u : α) = (e.symm : (a : β) → α) a
⊢ HMul.hMul (α := β) (Multiset.prod (Multiset.map (⇑e : (a : α) → β) w))
      (↑((Units.map e.toMonoidHom : (a : αˣ) → βˣ) u) : β) =
    a
have rw : HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β) ((↑((Units.map e.toMonoidHom : (a : αˣ) → βˣ) u) : β) : β) =
  a
Tactic: rw [Multiset.prod_hom, toMonoidHom_eq_coe, Units.coe_map, MonoidHom.coe_coe, ← map_mul e, h,
          apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ b ∈ w, Prime b
u : αˣ
h : w.prod * (↑u : α) = (e.symm : (a : β) → α) a
rw :
  HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β)
      ((↑((Units.map e.toMonoidHom : (a : αˣ) → βˣ) u) : β) : β) =
    a
⊢ HMul.hMul (α := β) (Multiset.prod (Multiset.map (⇑e : (a : α) → β) w))
      (↑((Units.map e.toMonoidHom : (a : αˣ) → βˣ) u) : β) =
    a
have rw₁ : HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β)
    ((↑(((Units.map (↑e : α →* β) : MonoidHom.{u_1, u_2} αˣ βˣ) : (a : αˣ) → βˣ) u) : β) : β) =
  a
Tactic: rw [Multiset.prod_hom, toMonoidHom_eq_coe, Units.coe_map, MonoidHom.coe_coe, ← map_mul e, h,
          apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ b ∈ w, Prime b
u : αˣ
h : w.prod * (↑u : α) = (e.symm : (a : β) → α) a
rw :
  HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β)
      ((↑((Units.map e.toMonoidHom : (a : αˣ) → βˣ) u) : β) : β) =
    a
rw₁ :
  HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β)
      ((↑(((Units.map (↑e : α →* β) : MonoidHom.{u_1, u_2} αˣ βˣ) : (a : αˣ) → βˣ) u) : β) : β) =
    a
⊢ HMul.hMul (α := β) (Multiset.prod (Multiset.map (⇑e : (a : α) → β) w))
      (↑((Units.map e.toMonoidHom : (a : αˣ) → βˣ) u) : β) =
    a
have rw₂ : HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β) (((↑e : α →* β) : (a : α) → β) (↑u : α) : β) = a
Tactic: rw [Multiset.prod_hom, toMonoidHom_eq_coe, Units.coe_map, MonoidHom.coe_coe, ← map_mul e, h,
          apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ b ∈ w, Prime b
u : αˣ
h : w.prod * (↑u : α) = (e.symm : (a : β) → α) a
rw :
  HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β)
      ((↑((Units.map e.toMonoidHom : (a : αˣ) → βˣ) u) : β) : β) =
    a
rw₁ :
  HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β)
      ((↑(((Units.map (↑e : α →* β) : MonoidHom.{u_1, u_2} αˣ βˣ) : (a : αˣ) → βˣ) u) : β) : β) =
    a
rw₂ : HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β) (((↑e : α →* β) : (a : α) → β) (↑u : α) : β) = a
⊢ HMul.hMul (α := β) (Multiset.prod (Multiset.map (⇑e : (a : α) → β) w))
      (↑((Units.map e.toMonoidHom : (a : αˣ) → βˣ) u) : β) =
    a
have rw₃ : HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β) ((e : (a : α) → β) (↑u : α) : β) = a
Tactic: rw [Multiset.prod_hom, toMonoidHom_eq_coe, Units.coe_map, MonoidHom.coe_coe, ← map_mul e, h,
          apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ b ∈ w, Prime b
u : αˣ
h : w.prod * (↑u : α) = (e.symm : (a : β) → α) a
rw :
  HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β)
      ((↑((Units.map e.toMonoidHom : (a : αˣ) → βˣ) u) : β) : β) =
    a
rw₁ :
  HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β)
      ((↑(((Units.map (↑e : α →* β) : MonoidHom.{u_1, u_2} αˣ βˣ) : (a : αˣ) → βˣ) u) : β) : β) =
    a
rw₂ : HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β) (((↑e : α →* β) : (a : α) → β) (↑u : α) : β) = a
rw₃ : HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β) ((e : (a : α) → β) (↑u : α) : β) = a
⊢ HMul.hMul (α := β) (Multiset.prod (Multiset.map (⇑e : (a : α) → β) w))
      (↑((Units.map e.toMonoidHom : (a : αˣ) → βˣ) u) : β) =
    a
have rw₄ : (e : (a : α) → β) (w.prod * (↑u : α)) = a
Tactic: rw [Multiset.prod_hom, toMonoidHom_eq_coe, Units.coe_map, MonoidHom.coe_coe, ← map_mul e, h,
          apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ b ∈ w, Prime b
u : αˣ
h : w.prod * (↑u : α) = (e.symm : (a : β) → α) a
rw :
  HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β)
      ((↑((Units.map e.toMonoidHom : (a : αˣ) → βˣ) u) : β) : β) =
    a
rw₁ :
  HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β)
      ((↑(((Units.map (↑e : α →* β) : MonoidHom.{u_1, u_2} αˣ βˣ) : (a : αˣ) → βˣ) u) : β) : β) =
    a
rw₂ : HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β) (((↑e : α →* β) : (a : α) → β) (↑u : α) : β) = a
rw₃ : HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β) ((e : (a : α) → β) (↑u : α) : β) = a
rw₄ : (e : (a : α) → β) (w.prod * (↑u : α)) = a
⊢ HMul.hMul (α := β) (Multiset.prod (Multiset.map (⇑e : (a : α) → β) w))
      (↑((Units.map e.toMonoidHom : (a : αˣ) → βˣ) u) : β) =
    a
have rw₅ : (e : (a : α) → β) ((e.symm : (a : β) → α) a : α) = a
Tactic: rw [Multiset.prod_hom, toMonoidHom_eq_coe, Units.coe_map, MonoidHom.coe_coe, ← map_mul e, h,
          apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ b ∈ w, Prime b
u : αˣ
h : w.prod * (↑u : α) = (e.symm : (a : β) → α) a
rw :
  HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β)
      ((↑((Units.map e.toMonoidHom : (a : αˣ) → βˣ) u) : β) : β) =
    a
rw₁ :
  HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β)
      ((↑(((Units.map (↑e : α →* β) : MonoidHom.{u_1, u_2} αˣ βˣ) : (a : αˣ) → βˣ) u) : β) : β) =
    a
rw₂ : HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β) (((↑e : α →* β) : (a : α) → β) (↑u : α) : β) = a
rw₃ : HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β) ((e : (a : α) → β) (↑u : α) : β) = a
rw₄ : (e : (a : α) → β) (w.prod * (↑u : α)) = a
rw₅ : (e : (a : α) → β) ((e.symm : (a : β) → α) a : α) = a
⊢ HMul.hMul (α := β) (Multiset.prod (Multiset.map (⇑e : (a : α) → β) w))
      (↑((Units.map e.toMonoidHom : (a : αˣ) → βˣ) u) : β) =
    a
have rw₆ : a = a
Tactic: rw [Multiset.prod_hom, toMonoidHom_eq_coe, Units.coe_map, MonoidHom.coe_coe, ← map_mul e, h,
          apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
⊢ ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
have h : ∀ (a : α), a ≠ 0 → ∀ (x : Multiset α), ∀ a ∈ x, Prime a ↔ Irreducible a
Tactic: convert! eif using 7
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a : R
⊢ a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
have refine_1 : Ne.{u_2 + 1} (α := R) 0 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = 0 ∧ c' * b' = b
Tactic: refine induction_on_prime a ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a : R
refine_1 :
  Ne.{u_2 + 1} (α := R) 0 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = 0 ∧ c' * b' = b
⊢ a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
have refine_2 : ∀ (x : R), IsUnit x → x ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = x ∧ c' * b' = b
Tactic: refine induction_on_prime a ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a : R
refine_1 :
  Ne.{u_2 + 1} (α := R) 0 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = 0 ∧ c' * b' = b
refine_2 :
  ∀ (x : R), IsUnit x → x ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = x ∧ c' * b' = b
⊢ a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
have refine_3 : ∀ (a p : R),
  a ≠ 0 →
    Prime p →
      (a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b) →
        p * a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b
Tactic: refine induction_on_prime a ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a : R
a_unit : IsUnit a
h : a ≠ 0
b : R
⊢ ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
have h : IsRelPrime a b ∧ 1 * a = a ∧ 1 * b = b
Tactic: use a, b, 1
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a : R
a_unit : IsUnit a
h : a ≠ 0
b : R
⊢ IsRelPrime a b ∧ 1 * a = a ∧ 1 * b = b
have h : IsRelPrime a b
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a : R
a_unit : IsUnit a
h_1 : a ≠ 0
b : R
h : IsRelPrime a b
⊢ IsRelPrime a b ∧ 1 * a = a ∧ 1 * b = b
have h₁ : 1 * a = a ∧ 1 * b = b
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
⊢ ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b
have pos : ∀ (h : p ∣ b), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b
Tactic: by_cases h : p ∣ b
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
pos : ∀ (h : p ∣ b), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b
⊢ ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b
have neg : ∀ (h : ¬p ∣ b), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b
Tactic: by_cases h : p ∣ b
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
h : p ∣ b
⊢ ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b
have pos : ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = p * b
Tactic: rcases h with ⟨b, rfl⟩
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
⊢ ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = p * b
have pos : ∀ (a' b' c' : R) (no_factor : IsRelPrime a' b') (ha' : c' * a' = a) (hb' : c' * b' = b),
  ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = p * b
Tactic: obtain ⟨a', b', c', no_factor, ha', hb'⟩ := ih_a a_ne_zero b