awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid (goal)
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
rw :
  Eq (α := Associates α)
    (Associates.mk
      (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b) *
        Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b)))
    (Associates.mk (a * b))
rw₁ :
  HMul.hMul (α := Associates α)
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b)))
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b))) =
    Associates.mk (a * b)
⊢ Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b) *
      Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b) ~ᵤ
    a * b
have rw₂ : HMul.hMul (α := Associates α)
    (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b)))
    (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b))) ~ᵤ
  Associates.mk (a * b)
Tactic: rw [← mk_eq_mk_iff_associated, ← Associates.mk_mul_mk, ← associated_iff_eq, Associates.quot_out,
      Associates.quot_out, mul_comm, sup_mul_inf, Associates.mk_mul_mk]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid (goal)
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
rw :
  Eq (α := Associates α)
    (Associates.mk
      (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b) *
        Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b)))
    (Associates.mk (a * b))
rw₁ :
  HMul.hMul (α := Associates α)
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b)))
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b))) =
    Associates.mk (a * b)
rw₂ :
  HMul.hMul (α := Associates α)
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b)))
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b))) ~ᵤ
    Associates.mk (a * b)
⊢ Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b) *
      Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b) ~ᵤ
    a * b
have rw₃ : HMul.hMul (α := Associates α) (Associates.mk a ⊓ Associates.mk b)
    (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b))) ~ᵤ
  Associates.mk (a * b)
Tactic: rw [← mk_eq_mk_iff_associated, ← Associates.mk_mul_mk, ← associated_iff_eq, Associates.quot_out,
      Associates.quot_out, mul_comm, sup_mul_inf, Associates.mk_mul_mk]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid (goal)
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
rw :
  Eq (α := Associates α)
    (Associates.mk
      (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b) *
        Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b)))
    (Associates.mk (a * b))
rw₁ :
  HMul.hMul (α := Associates α)
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b)))
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b))) =
    Associates.mk (a * b)
rw₂ :
  HMul.hMul (α := Associates α)
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b)))
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b))) ~ᵤ
    Associates.mk (a * b)
rw₃ :
  HMul.hMul (α := Associates α) (Associates.mk a ⊓ Associates.mk b)
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b))) ~ᵤ
    Associates.mk (a * b)
⊢ Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b) *
      Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b) ~ᵤ
    a * b
have rw₄ : HMul.hMul (α := Associates α) (Associates.mk a ⊓ Associates.mk b) (Associates.mk a ⊔ Associates.mk b) ~ᵤ
  Associates.mk (a * b)
Tactic: rw [← mk_eq_mk_iff_associated, ← Associates.mk_mul_mk, ← associated_iff_eq, Associates.quot_out,
      Associates.quot_out, mul_comm, sup_mul_inf, Associates.mk_mul_mk]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid (goal)
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
rw :
  Eq (α := Associates α)
    (Associates.mk
      (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b) *
        Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b)))
    (Associates.mk (a * b))
rw₁ :
  HMul.hMul (α := Associates α)
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b)))
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b))) =
    Associates.mk (a * b)
rw₂ :
  HMul.hMul (α := Associates α)
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b)))
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b))) ~ᵤ
    Associates.mk (a * b)
rw₃ :
  HMul.hMul (α := Associates α) (Associates.mk a ⊓ Associates.mk b)
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b))) ~ᵤ
    Associates.mk (a * b)
rw₄ :
  HMul.hMul (α := Associates α) (Associates.mk a ⊓ Associates.mk b) (Associates.mk a ⊔ Associates.mk b) ~ᵤ
    Associates.mk (a * b)
⊢ Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b) *
      Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b) ~ᵤ
    a * b
have rw₅ : HMul.hMul (α := Associates α) (Associates.mk a ⊔ Associates.mk b) (Associates.mk a ⊓ Associates.mk b) ~ᵤ
  Associates.mk (a * b)
Tactic: rw [← mk_eq_mk_iff_associated, ← Associates.mk_mul_mk, ← associated_iff_eq, Associates.quot_out,
      Associates.quot_out, mul_comm, sup_mul_inf, Associates.mk_mul_mk]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid (goal)
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
rw :
  Eq (α := Associates α)
    (Associates.mk
      (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b) *
        Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b)))
    (Associates.mk (a * b))
rw₁ :
  HMul.hMul (α := Associates α)
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b)))
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b))) =
    Associates.mk (a * b)
rw₂ :
  HMul.hMul (α := Associates α)
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b)))
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b))) ~ᵤ
    Associates.mk (a * b)
rw₃ :
  HMul.hMul (α := Associates α) (Associates.mk a ⊓ Associates.mk b)
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b))) ~ᵤ
    Associates.mk (a * b)
rw₄ :
  HMul.hMul (α := Associates α) (Associates.mk a ⊓ Associates.mk b) (Associates.mk a ⊔ Associates.mk b) ~ᵤ
    Associates.mk (a * b)
rw₅ :
  HMul.hMul (α := Associates α) (Associates.mk a ⊔ Associates.mk b) (Associates.mk a ⊓ Associates.mk b) ~ᵤ
    Associates.mk (a * b)
⊢ Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b) *
      Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b) ~ᵤ
    a * b
have rw₆ : HMul.hMul (α := Associates α) (Associates.mk a) (Associates.mk b) ~ᵤ Associates.mk (a * b)
Tactic: rw [← mk_eq_mk_iff_associated, ← Associates.mk_mul_mk, ← associated_iff_eq, Associates.quot_out,
      Associates.quot_out, mul_comm, sup_mul_inf, Associates.mk_mul_mk]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid (goal)
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
rw :
  Eq (α := Associates α)
    (Associates.mk
      (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b) *
        Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b)))
    (Associates.mk (a * b))
rw₁ :
  HMul.hMul (α := Associates α)
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b)))
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b))) =
    Associates.mk (a * b)
rw₂ :
  HMul.hMul (α := Associates α)
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b)))
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b))) ~ᵤ
    Associates.mk (a * b)
rw₃ :
  HMul.hMul (α := Associates α) (Associates.mk a ⊓ Associates.mk b)
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b))) ~ᵤ
    Associates.mk (a * b)
rw₄ :
  HMul.hMul (α := Associates α) (Associates.mk a ⊓ Associates.mk b) (Associates.mk a ⊔ Associates.mk b) ~ᵤ
    Associates.mk (a * b)
rw₅ :
  HMul.hMul (α := Associates α) (Associates.mk a ⊔ Associates.mk b) (Associates.mk a ⊓ Associates.mk b) ~ᵤ
    Associates.mk (a * b)
rw₆ : HMul.hMul (α := Associates α) (Associates.mk a) (Associates.mk b) ~ᵤ Associates.mk (a * b)
⊢ Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b) *
      Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b) ~ᵤ
    a * b
have rw₇ : Associated (M := Associates α) (Associates.mk (a * b)) (Associates.mk (a * b))
Tactic: rw [← mk_eq_mk_iff_associated, ← Associates.mk_mul_mk, ← associated_iff_eq, Associates.quot_out,
      Associates.quot_out, mul_comm, sup_mul_inf, Associates.mk_mul_mk]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid (goal)
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : NormalizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
⊢ a ∣ Associates.out (Associates.mk c ⊓ Associates.mk b)
have rw : a ∣ c ∧ a ∣ b
Tactic: rw [dvd_out_iff, le_inf_iff, mk_le_mk_iff_dvd, mk_le_mk_iff_dvd]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid (goal)
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : NormalizationMonoid α
a b : α
⊢ Associates.out (Associates.mk a ⊓ Associates.mk b) * Associates.out (Associates.mk a ⊔ Associates.mk b) ~ᵤ a * b
have rw : (normalize : (a : α) → α) (a * b) ~ᵤ a * b
Tactic: rw [← out_mul, mul_comm, sup_mul_inf, mk_mul_mk, out_mk]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Ideal (goal)
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
⊢ ∃ x ∈ I, Prime x
have obtain : ∀ (a : R) (ha₁ : a ∈ I) (ha₂ : a ≠ 0), ∃ x ∈ I, Prime x
Tactic: obtain ⟨a : R, ha₁ : a ∈ I, ha₂ : a ≠ 0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hI
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Ideal (goal)
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₁ : a ∈ I
ha₂ : a ≠ 0
⊢ (factors a).prod ∈ I
have obtain : ∀ (u : Rˣ) (hu : (factors a).prod * (↑u : R) = a), (factors a).prod ∈ I
Tactic: obtain ⟨u : Rˣ, hu : (factors a).prod * u = a⟩ := factors_prod ha₂
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Ideal (goal)
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₁ : a ∈ I
ha₂ : a ≠ 0
u : Rˣ
hu : (factors a).prod * (↑u : R) = a
⊢ (factors a).prod ∈ I
have rwa : ∀ (ha₁ : (factors a).prod * (↑u : R) ∈ I) (hu : (factors a).prod * (↑u : R) = a), (factors a).prod ∈ I
Tactic: rwa [← hu, mul_unit_mem_iff_mem _ u.isUnit] at ha₁
Cleared hypotheses: ha₁, hu
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Ideal (goal)
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₁ : a ∈ I
ha₂ : a ≠ 0
u : Rˣ
hu : (factors a).prod * (↑u : R) = a
rwa : ∀ (ha₁ : (factors a).prod * (↑u : R) ∈ I) (hu : (factors a).prod * (↑u : R) = a), (factors a).prod ∈ I
⊢ (factors a).prod ∈ I
have rwa₁ : ∀ (ha₁ : (factors a).prod ∈ I) (hu : (factors a).prod * (↑u : R) = a), (factors a).prod ∈ I
Tactic: rwa [← hu, mul_unit_mem_iff_mem _ u.isUnit] at ha₁
Cleared hypotheses: ha₁, hu
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Ideal (hypothesis)
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₁ : a ∈ I
ha₂ : a ≠ 0
⊢ ∃ x ∈ I, Prime x
have ha₃ : (factors a).prod ∈ I
Tactic: replace ha₁ : (factors a).prod ∈ I := by
    obtain ⟨u : Rˣ, hu : (factors a).prod * u = a⟩ := factors_prod ha₂
    rwa [← hu, mul_unit_mem_iff_mem _ u.isUnit] at ha₁
Cleared hypotheses: ha₁
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Ideal (goal)
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₂ : a ≠ 0
ha₁ : (factors a).prod ∈ I
⊢ ∃ x ∈ I, Prime x
have obtain : ∀ (p : R) (hp₁ : p ∈ factors a) (hp₂ : p ∈ I), ∃ x ∈ I, Prime x
Tactic: obtain ⟨p : R, hp₁ : p ∈ factors a, hp₂ : p ∈ I⟩ :=
    (hI₂.multiset_prod_mem_iff_exists_mem <| factors a).1 ha₁
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Ideal (goal)
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
⊢ ∃ x ∈ I, Prime x
have obtain : ∀ (a : R) (ha₁ : a ∈ I) (ha₂ : a ≠ 0), ∃ x ∈ I, Prime x
Tactic: classical
  obtain ⟨a : R, ha₁ : a ∈ I, ha₂ : a ≠ 0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hI
  replace ha₁ : (factors a).prod ∈ I := by
    obtain ⟨u : Rˣ, hu : (factors a).prod * u = a⟩ := factors_prod ha₂
    rwa [← hu, mul_unit_mem_iff_mem _ u.isUnit] at ha₁
  obtain ⟨p : R, hp₁ : p ∈ factors a, hp₂ : p ∈ I⟩ :=
    (hI₂.multiset_prod_mem_iff_exists_mem <| factors a).1 ha₁
  exact ⟨p, hp₂, prime_of_factor p hp₁⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Ideal (goal)
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
obtain : ∀ (a : R) (ha₁ : a ∈ I) (ha₂ : a ≠ 0), ∃ x ∈ I, Prime x
⊢ ∃ x ∈ I, Prime x
have obtain₁ : ∀ (a : R) (ha₂ : a ≠ 0) (ha₁ : (factors a).prod ∈ I), ∃ x ∈ I, Prime x
Tactic: classical
  obtain ⟨a : R, ha₁ : a ∈ I, ha₂ : a ≠ 0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hI
  replace ha₁ : (factors a).prod ∈ I := by
    obtain ⟨u : Rˣ, hu : (factors a).prod * u = a⟩ := factors_prod ha₂
    rwa [← hu, mul_unit_mem_iff_mem _ u.isUnit] at ha₁
  obtain ⟨p : R, hp₁ : p ∈ factors a, hp₂ : p ∈ I⟩ :=
    (hI₂.multiset_prod_mem_iff_exists_mem <| factors a).1 ha₁
  exact ⟨p, hp₂, prime_of_factor p hp₁⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Ideal (goal)
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
obtain : ∀ (a : R) (ha₁ : a ∈ I) (ha₂ : a ≠ 0), ∃ x ∈ I, Prime x
obtain₁ : ∀ (a : R) (ha₂ : a ≠ 0) (ha₁ : (factors a).prod ∈ I), ∃ x ∈ I, Prime x
⊢ ∃ x ∈ I, Prime x
have obtain₂ : ∀ (a : R) (ha₂ : a ≠ 0) (ha₁ : (factors a).prod ∈ I) (p : R) (hp₁ : p ∈ factors a) (hp₂ : p ∈ I), ∃ x ∈ I, Prime x
Tactic: classical
  obtain ⟨a : R, ha₁ : a ∈ I, ha₂ : a ≠ 0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hI
  replace ha₁ : (factors a).prod ∈ I := by
    obtain ⟨u : Rˣ, hu : (factors a).prod * u = a⟩ := factors_prod ha₂
    rwa [← hu, mul_unit_mem_iff_mem _ u.isUnit] at ha₁
  obtain ⟨p : R, hp₁ : p ∈ factors a, hp₂ : p ∈ I⟩ :=
    (hI₂.multiset_prod_mem_iff_exists_mem <| factors a).1 ha₁
  exact ⟨p, hp₂, prime_of_factor p hp₁⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Ideal (goal)
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : WfDvdMonoid α
inst_2 : IsDomain α
⊢ Eq.{u_1 + 1} (α := Set (Ideal α)) {I : Ideal α | Submodule.IsPrincipal I} ((fun (a : α) ↦ span {a}) '' Set.univ)
have h : ∀ (x : Ideal α),
  Membership.mem (γ := Set (Ideal α)) {I : Ideal α | Submodule.IsPrincipal I} x ↔
    Membership.mem (γ := Set (Ideal α)) ((fun (a : α) ↦ span {a}) '' Set.univ) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Ideal (hypothesis)
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : WfDvdMonoid α
inst_2 : IsDomain α
⊢ Set.WellFoundedOn {I : Ideal α | Submodule.IsPrincipal I} fun (x1 x2 : Ideal α) ↦ x1 > x2
have this : Eq.{u_1 + 1} (α := Set (Ideal α)) {I : Ideal α | Submodule.IsPrincipal I} ((fun (a : α) ↦ span {a}) '' Set.univ)
Tactic: have : {I : Ideal α | I.IsPrincipal} = ((fun a ↦ Ideal.span {a}) '' Set.univ) := by
    ext
    simp [Submodule.isPrincipal_iff, eq_comm]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Ideal (goal)
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : WfDvdMonoid α
inst_2 : IsDomain α
this : Eq.{u_1 + 1} (α := Set (Ideal α)) {I : Ideal α | Submodule.IsPrincipal I} ((fun (a : α) ↦ span {a}) '' Set.univ)
⊢ Set.WellFoundedOn {I : Ideal α | Submodule.IsPrincipal I} fun (x1 x2 : Ideal α) ↦ x1 > x2
have rw : WellFounded.{u_1 + 1} (α := α) (Function.onFun (fun (x1 x2 : Ideal α) ↦ x1 > x2) fun (a : α) ↦ span {a})
Tactic: rw [this, Set.wellFoundedOn_image, Set.wellFoundedOn_univ]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Ideal (goal)
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : WfDvdMonoid α
inst_2 : IsDomain α
this : Eq.{u_1 + 1} (α := Set (Ideal α)) {I : Ideal α | Submodule.IsPrincipal I} ((fun (a : α) ↦ span {a}) '' Set.univ)
⊢ WellFounded.{u_1 + 1} (α := α) (Function.onFun (fun (x1 x2 : Ideal α) ↦ x1 > x2) fun (a : α) ↦ span {a})
have h : Eq.{u_1 + 1} (α := α → α → Prop) (Function.onFun (fun (x1 x2 : Ideal α) ↦ x1 > x2) fun (a : α) ↦ span {a}) DvdNotUnit
Tactic: convert! wellFounded_dvdNotUnit (α := α)
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Ideal (goal)
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : WfDvdMonoid α
inst_2 : IsDomain α
this : Eq.{u_1 + 1} (α := Set (Ideal α)) {I : Ideal α | Submodule.IsPrincipal I} ((fun (a : α) ↦ span {a}) '' Set.univ)
⊢ Eq.{u_1 + 1} (α := α → α → Prop) (Function.onFun (fun (x1 x2 : Ideal α) ↦ x1 > x2) fun (a : α) ↦ span {a}) DvdNotUnit
have h : ∀ (x x_1 : α), Function.onFun (fun (x1 x2 : Ideal α) ↦ x1 > x2) (fun (a : α) ↦ span {a}) x x_1 ↔ DvdNotUnit x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Ideal (hypothesis)
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : IsDomain α
h : Set.WellFoundedOn {I : Ideal α | Submodule.IsPrincipal I} fun (x1 x2 : Ideal α) ↦ x1 > x2
⊢ WfDvdMonoid α
have this : WellFounded fun (x1 x2 : { I : Ideal α // Submodule.IsPrincipal I }) ↦ x1 > x2
Tactic: have : WellFounded (α := {I : Ideal α // I.IsPrincipal}) (· > ·) := h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Ideal (goal)
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : IsDomain α
h : Set.WellFoundedOn {I : Ideal α | Submodule.IsPrincipal I} fun (x1 x2 : Ideal α) ↦ x1 > x2
this : WellFounded fun (x1 x2 : { I : Ideal α // Submodule.IsPrincipal I }) ↦ x1 > x2
⊢ WfDvdMonoid α
have wf : WellFounded.{u_1 + 1} (α := α) DvdNotUnit
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Ideal (goal)
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : IsDomain α
h : Set.WellFoundedOn {I : Ideal α | Submodule.IsPrincipal I} fun (x1 x2 : Ideal α) ↦ x1 > x2
this : WellFounded fun (x1 x2 : { I : Ideal α // Submodule.IsPrincipal I }) ↦ x1 > x2
⊢ WellFounded.{u_1 + 1} (α := α) DvdNotUnit
have h₁ : Eq.{u_1 + 1} (α := α → α → Prop) DvdNotUnit
  (InvImage (fun (x1 x2 : { I : Ideal α // Submodule.IsPrincipal I }) ↦ x1 > x2) fun (a : α) ↦
    Subtype.mk (p := fun (I : Ideal α) ↦ Submodule.IsPrincipal I) (Ideal.span {a}) sorry)
Tactic: convert! InvImage.wf (fun a => ⟨Ideal.span ({ a } : Set α), _, rfl⟩) this
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Ideal (goal)
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : IsDomain α
h : Set.WellFoundedOn {I : Ideal α | Submodule.IsPrincipal I} fun (x1 x2 : Ideal α) ↦ x1 > x2
this : WellFounded fun (x1 x2 : { I : Ideal α // Submodule.IsPrincipal I }) ↦ x1 > x2
⊢ Eq.{u_1 + 1} (α := α → α → Prop) DvdNotUnit
    (InvImage (fun (x1 x2 : { I : Ideal α // Submodule.IsPrincipal I }) ↦ x1 > x2) fun (a : α) ↦
      Subtype.mk (p := fun (I : Ideal α) ↦ Submodule.IsPrincipal I) (Ideal.span {a}) ⋯)
have h₁ : ∀ (x x_1 : α),
  DvdNotUnit x x_1 ↔
    InvImage (fun (x1 x2 : { I : Ideal α // Submodule.IsPrincipal I }) ↦ x1 > x2)
      (fun (a : α) ↦ Subtype.mk (p := fun (I : Ideal α) ↦ Submodule.IsPrincipal I) (Ideal.span {a}) sorry) x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
⊢ ∃ P ∈ kaplanskySet S, ∀ J ∈ C, J ≤ P
have inl : ∀ (hC : ∅ ⊆ kaplanskySet S) (hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) ∅),
  ∃ P ∈ kaplanskySet S, ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) ∅ J → J ≤ P
Tactic: rcases C.eq_empty_or_nonempty with rfl | ⟨_, hI⟩
Cleared hypotheses: C, hC, hC₂
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
inl :
  ∀ (hC : ∅ ⊆ kaplanskySet S) (hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) ∅),
    ∃ P ∈ kaplanskySet S, ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) ∅ J → J ≤ P
⊢ ∃ P ∈ kaplanskySet S, ∀ J ∈ C, J ≤ P
have inr : ∀ (w : Ideal R) (hI : w ∈ C), ∃ P ∈ kaplanskySet S, ∀ J ∈ C, J ≤ P
Tactic: rcases C.eq_empty_or_nonempty with rfl | ⟨_, hI⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
w : Ideal R
hI : w ∈ C
⊢ ∃ P ∈ kaplanskySet S, ∀ J ∈ C, J ≤ P
have inr : sSup C ∈ kaplanskySet S
Tactic: refine ⟨sSup C, ?_, fun _ hz ↦ le_sSup hz⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
w : Ideal R
hI : w ∈ C
⊢ sSup C ∈ kaplanskySet S
have inr : ∀ (x : R), x ∉ (↑(sSup C) : Set R) ∩ (↑S : Set R)
Tactic: rw [mem_kaplanskySet_iff, eq_empty_iff_forall_notMem]