awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : R
hx : x ∈ (↑(sSup C) : Set R) ∩ (↑S : Set R)
⊢ False
have inr : ∀ (J : Submodule R R) (hJ₁ : J ∈ C) (hJ₂ : x ∈ J), False
Tactic: rcases (Submodule.mem_sSup_of_directed ⟨_, hI⟩ hC₂.directedOn).1 hx.1 with ⟨J, hJ₁, hJ₂⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (hypothesis)
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
x : R
hx : x ∈ (↑(sSup C) : Set R) ∩ (↑S : Set R)
J : Submodule R R
hJ₁ : J ∈ C
hJ₂ : x ∈ J
⊢ False
have hx₂ : (↑J : Set R) ∩ (↑S : Set R) ≠ ∅
Tactic: have hx₂ : (J : Set R) ∩ S ≠ ∅ := nonempty_iff_ne_empty.1 ⟨x, hJ₂, hx.2⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
⊢ ∃ P ∈ kaplanskySet S, ∀ I ∈ kaplanskySet S, P ≤ I → I = P
have obtain : ∀ (P : Ideal R) (hP : Maximal (fun (x : Ideal R) ↦ x ∈ kaplanskySet S) P),
  ∃ P ∈ kaplanskySet S, ∀ I ∈ kaplanskySet S, P ≤ I → I = P
Tactic: obtain ⟨P, hP⟩ := zorn_le₀ (kaplanskySet S) (fun _ ↦ exists_mem_kaplanskySet_le hS)
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
h : Membership.mem (γ := Submonoid R) (closure {r : R | Prime r}) 0
⊢ False
have rcases : ∀ (l : Multiset R) (hl : ∀ y ∈ l, Membership.mem (γ := Set R) {r : R | Prime r} y) (hprod : l.prod = 0), False
Tactic: rcases exists_multiset_of_mem_closure h with ⟨l, hl, hprod⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
⊢ span {a} ∉ kaplanskySet (toSubsemigroup (closure {r : R | Prime r}))
have hzero : 0 ∉ closure {r : R | Prime r}
Tactic: have hzero : 0 ∉ closure {r : R | Prime r} := fun h ↦ by
    rcases exists_multiset_of_mem_closure h with ⟨l, hl, hprod⟩
    exact not_prime_zero (hl 0 (Multiset.prod_eq_zero_iff.1 hprod))
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
hzero : 0 ∉ closure {r : R | Prime r}
h : Membership.mem (γ := Set (Ideal R)) (kaplanskySet (toSubsemigroup (closure {r : R | Prime r}))) (span {a})
⊢ False
have rcases : ∀ (T : Ideal R) (hT : Membership.mem (γ := Set (Ideal R)) (kaplanskySet (toSubsemigroup (closure {r : R | Prime r}))) T)
  (hT₂ :
    ∀ (I : Ideal R),
      Membership.mem (γ := Set (Ideal R)) (kaplanskySet (toSubsemigroup (closure {r : R | Prime r}))) I →
        T ≤ I → I = T),
  False
Tactic: rcases exists_mem_kaplanskySet_eq_of_le hzero with ⟨T, hT, hT₂⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
hzero : 0 ∉ closure {r : R | Prime r}
h : Membership.mem (γ := Set (Ideal R)) (kaplanskySet (toSubsemigroup (closure {r : R | Prime r}))) (span {a})
T : Ideal R
hT : Membership.mem (γ := Set (Ideal R)) (kaplanskySet (toSubsemigroup (closure {r : R | Prime r}))) T
hT₂ :
  ∀ (I : Ideal R),
    Membership.mem (γ := Set (Ideal R)) (kaplanskySet (toSubsemigroup (closure {r : R | Prime r}))) I → T ≤ I → I = T
⊢ False
have hT₃ : T ≠ ⊥
Tactic: have hT₃ : T ≠ ⊥ := fun h₂ ↦ ha (span_singleton_eq_bot.1 ((h₂ ▸ hT₂) _ h zero_le))
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
hzero : 0 ∉ closure {r : R | Prime r}
h : Membership.mem (γ := Set (Ideal R)) (kaplanskySet (toSubsemigroup (closure {r : R | Prime r}))) (span {a})
T : Ideal R
hT : Membership.mem (γ := Set (Ideal R)) (kaplanskySet (toSubsemigroup (closure {r : R | Prime r}))) T
hT₂ :
  ∀ (I : Ideal R),
    Membership.mem (γ := Set (Ideal R)) (kaplanskySet (toSubsemigroup (closure {r : R | Prime r}))) I → T ≤ I → I = T
hT₃ : T ≠ ⊥
⊢ False
have Tpri : T.IsPrime
Tactic: have Tpri := isPrime_of_maximally_disjoint T _ hT (fun J hJ H ↦ hJ.ne (hT₂ J H hJ.le).symm)
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
hzero : 0 ∉ closure {r : R | Prime r}
h : Membership.mem (γ := Set (Ideal R)) (kaplanskySet (toSubsemigroup (closure {r : R | Prime r}))) (span {a})
T : Ideal R
hT : Membership.mem (γ := Set (Ideal R)) (kaplanskySet (toSubsemigroup (closure {r : R | Prime r}))) T
hT₂ :
  ∀ (I : Ideal R),
    Membership.mem (γ := Set (Ideal R)) (kaplanskySet (toSubsemigroup (closure {r : R | Prime r}))) I → T ≤ I → I = T
hT₃ : T ≠ ⊥
Tpri : T.IsPrime
⊢ False
have rcases : ∀ (x : R) (H₃ : x ∈ T) (H₄ : Prime x), False
Tactic: rcases (H T) hT₃ Tpri with ⟨x, H₃, H₄⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
hzero : 0 ∉ closure {r : R | Prime r}
h : Membership.mem (γ := Set (Ideal R)) (kaplanskySet (toSubsemigroup (closure {r : R | Prime r}))) (span {a})
T : Ideal R
hT : Membership.mem (γ := Set (Ideal R)) (kaplanskySet (toSubsemigroup (closure {r : R | Prime r}))) T
hT₂ :
  ∀ (I : Ideal R),
    Membership.mem (γ := Set (Ideal R)) (kaplanskySet (toSubsemigroup (closure {r : R | Prime r}))) I → T ≤ I → I = T
hT₃ : T ≠ ⊥
Tpri : T.IsPrime
x : R
H₃ : x ∈ T
H₄ : Prime x
⊢ False
have rw : ∀ (hT : ∀ (x : R), x ∉ (↑T : Set R) ∩ (↑(toSubsemigroup (closure {r : R | Prime r}) : Subsemigroup R) : Set R))
  (hT₂ :
    ∀ (I : Ideal R),
      Membership.mem (γ := Set (Ideal R)) (kaplanskySet (toSubsemigroup (closure {r : R | Prime r}))) I → T ≤ I → I = T)
  (hT₃ : T ≠ ⊥) (Tpri : T.IsPrime) (x : R) (H₃ : x ∈ T) (H₄ : Prime x), False
Tactic: rw [mem_kaplanskySet_iff, eq_empty_iff_forall_notMem] at hT
Cleared hypotheses: hT, hT₂, hT₃, Tpri, x, H₃, H₄
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
⊢ UniqueFactorizationMonoid R
have refine : ∀ (a : R) (ha : a ≠ 0), ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod a
Tactic: refine UniqueFactorizationMonoid.of_exists_prime_factors fun a ha ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a : R
ha : a ≠ 0
⊢ ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod a
have ha₂ : span {a} ∉ kaplanskySet (toSubsemigroup (closure {r : R | Prime r}))
Tactic: have ha₂ := span_notMem_kaplanskySet ha H
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a : R
ha : a ≠ 0
ha₂ : span {a} ∉ kaplanskySet (toSubsemigroup (closure {r : R | Prime r}))
⊢ ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod a
have ha₃ : ¬(↑(span {a}) : Set R) ∩ (↑(toSubsemigroup (closure {r : R | Prime r}) : Subsemigroup R) : Set R) = ∅
Tactic: rw [mem_kaplanskySet_iff] at ha₂
Cleared hypotheses: ha₂
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a : R
ha : a ≠ 0
ha₂ : ¬(↑(span {a}) : Set R) ∩ (↑(toSubsemigroup (closure {r : R | Prime r}) : Subsemigroup R) : Set R) = ∅
⊢ ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod a
have rcases : ∀ (x : R) (hx : x ∈ (↑(span {a}) : Set R))
  (hx₂ : x ∈ (↑(toSubsemigroup (closure {r : R | Prime r}) : Subsemigroup R) : Set R)),
  ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod a
Tactic: rcases nonempty_iff_ne_empty.2 ha₂ with ⟨x, hx, hx₂⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a : R
ha : a ≠ 0
ha₂ : ¬(↑(span {a}) : Set R) ∩ (↑(toSubsemigroup (closure {r : R | Prime r}) : Subsemigroup R) : Set R) = ∅
x : R
hx : x ∈ (↑(span {a}) : Set R)
hx₂ : x ∈ (↑(toSubsemigroup (closure {r : R | Prime r}) : Subsemigroup R) : Set R)
⊢ ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod a
have obtain : ∀ (b : R) (hb : b * a = x), ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod a
Tactic: obtain ⟨b, hb⟩ := mem_span_singleton'.1 hx
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a : R
ha : a ≠ 0
ha₂ : ¬(↑(span {a}) : Set R) ∩ (↑(toSubsemigroup (closure {r : R | Prime r}) : Subsemigroup R) : Set R) = ∅
x : R
hx : x ∈ (↑(span {a}) : Set R)
hx₂ : x ∈ (↑(toSubsemigroup (closure {r : R | Prime r}) : Subsemigroup R) : Set R)
b : R
hb : b * a = x
⊢ ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod a
have hx₃ : a * b ∈ (↑(toSubsemigroup (closure {r : R | Prime r}) : Subsemigroup R) : Set R)
Tactic: rw [← hb, mul_comm] at hx₂
Cleared hypotheses: hx₂, hb
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a : R
ha : a ≠ 0
ha₂ : ¬(↑(span {a}) : Set R) ∩ (↑(toSubsemigroup (closure {r : R | Prime r}) : Subsemigroup R) : Set R) = ∅
x : R
hx : x ∈ (↑(span {a}) : Set R)
b : R
hx₂ : a * b ∈ (↑(toSubsemigroup (closure {r : R | Prime r}) : Subsemigroup R) : Set R)
hb : b * a = x
⊢ ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod a
have hsubset : LE.le.{u_1} (α := Submonoid R) (closure {r : R | Prime r}) (closure {r : R | IsUnit r ∨ Prime r})
Tactic: have hsubset : closure {r : R | Prime r} ≤ closure {r : R | IsUnit r ∨ Prime r} :=
    closure_mono (by grind)
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a : R
ha : a ≠ 0
ha₂ : ¬(↑(span {a}) : Set R) ∩ (↑(toSubsemigroup (closure {r : R | Prime r}) : Subsemigroup R) : Set R) = ∅
x : R
hx : x ∈ (↑(span {a}) : Set R)
b : R
hx₂ : a * b ∈ (↑(toSubsemigroup (closure {r : R | Prime r}) : Subsemigroup R) : Set R)
hb : b * a = x
hsubset : LE.le.{u_1} (α := Submonoid R) (closure {r : R | Prime r}) (closure {r : R | IsUnit r ∨ Prime r})
⊢ ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod a
have this : Membership.mem (γ := Submonoid R) (closure {r : R | IsUnit r ∨ Prime r}) a
Tactic: have := divisor_closure_eq_closure _ _ (hsubset hx₂)
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : LE.le.{u_1} (α := Submonoid R) (closure {r : R | Prime r}) (closure {r : R | IsUnit r ∨ Prime r})
z : R
hz : Membership.mem (γ := Set R) {r : R | IsUnit r ∨ Prime r} z
⊢ ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod z
have mem : ∀ (h : IsUnit z), ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod z
Tactic: rcases hz with h | h
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : LE.le.{u_1} (α := Submonoid R) (closure {r : R | Prime r}) (closure {r : R | IsUnit r ∨ Prime r})
z : R
hz : Membership.mem (γ := Set R) {r : R | IsUnit r ∨ Prime r} z
mem : ∀ (h : IsUnit z), ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod z
⊢ ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod z
have mem₁ : ∀ (h : Prime z), ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod z
Tactic: rcases hz with h | h
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : LE.le.{u_1} (α := Submonoid R) (closure {r : R | Prime r}) (closure {r : R | IsUnit r ∨ Prime r})
z₁ z₂ : R
hz₁ : Membership.mem (γ := Submonoid R) (closure {r : R | IsUnit r ∨ Prime r}) z₁
hz₂ : Membership.mem (γ := Submonoid R) (closure {r : R | IsUnit r ∨ Prime r}) z₂
h₁ : ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod z₁
h₂ : ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod z₂
⊢ ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod (z₁ * z₂)
have mul : ∀ (S₁ : Multiset R) (hS₁pri : ∀ b ∈ S₁, Prime b) (hS₁ : Associated S₁.prod z₁),
  ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod (z₁ * z₂)
Tactic: obtain ⟨S₁, hS₁pri, hS₁⟩ := h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : LE.le.{u_1} (α := Submonoid R) (closure {r : R | Prime r}) (closure {r : R | IsUnit r ∨ Prime r})
z₁ z₂ : R
hz₁ : Membership.mem (γ := Submonoid R) (closure {r : R | IsUnit r ∨ Prime r}) z₁
hz₂ : Membership.mem (γ := Submonoid R) (closure {r : R | IsUnit r ∨ Prime r}) z₂
h₂ : ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod z₂
S₁ : Multiset R
hS₁pri : ∀ b ∈ S₁, Prime b
hS₁ : Associated S₁.prod z₁
⊢ ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod (z₁ * z₂)
have mul : ∀ (S₂ : Multiset R) (hS₂pri : ∀ b ∈ S₂, Prime b) (hS₂ : Associated S₂.prod z₂),
  ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod (z₁ * z₂)
Tactic: obtain ⟨S₂, hS₂pri, hS₂⟩ := h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : LE.le.{u_1} (α := Submonoid R) (closure {r : R | Prime r}) (closure {r : R | IsUnit r ∨ Prime r})
z₁ z₂ : R
hz₁ : Membership.mem (γ := Submonoid R) (closure {r : R | IsUnit r ∨ Prime r}) z₁
hz₂ : Membership.mem (γ := Submonoid R) (closure {r : R | IsUnit r ∨ Prime r}) z₂
S₁ : Multiset R
hS₁pri : ∀ b ∈ S₁, Prime b
hS₁ : Associated S₁.prod z₁
S₂ : Multiset R
hS₂pri : ∀ b ∈ S₂, Prime b
hS₂ : Associated S₂.prod z₂
⊢ ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod (z₁ * z₂)
have mul : Associated (S₁ + S₂).prod (z₁ * z₂)
Tactic: refine ⟨S₁ + S₂, by grind, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : LE.le.{u_1} (α := Submonoid R) (closure {r : R | Prime r}) (closure {r : R | IsUnit r ∨ Prime r})
z₁ z₂ : R
hz₁ : Membership.mem (γ := Submonoid R) (closure {r : R | IsUnit r ∨ Prime r}) z₁
hz₂ : Membership.mem (γ := Submonoid R) (closure {r : R | IsUnit r ∨ Prime r}) z₂
S₁ : Multiset R
hS₁pri : ∀ b ∈ S₁, Prime b
hS₁ : Associated S₁.prod z₁
S₂ : Multiset R
hS₂pri : ∀ b ∈ S₂, Prime b
hS₂ : Associated S₂.prod z₂
⊢ Associated (S₁ + S₂).prod (z₁ * z₂)
have mul : Associated (S₁.prod * S₂.prod) (z₁ * z₂)
Tactic: rw [Multiset.prod_add]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : LE.le.{u_1} (α := Submonoid R) (closure {r : R | Prime r}) (closure {r : R | IsUnit r ∨ Prime r})
this : Membership.mem (γ := Submonoid R) (closure {r : R | IsUnit r ∨ Prime r}) a
⊢ ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod a
have mem : ∀ (z : R) (hz : Membership.mem (γ := Set R) {r : R | IsUnit r ∨ Prime r} z),
  ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod z
Tactic: induction this using closure_induction with
  | mem z hz =>
      rcases hz with h | h
      · exact ⟨∅, by simpa using (associated_one_iff_isUnit.2 h).symm⟩
      · exact ⟨{z}, by simpa⟩
  | one => exact ⟨∅, by simp⟩
  | mul z₁ z₂ hz₁ hz₂ h₁ h₂ =>
      obtain ⟨S₁, hS₁pri, hS₁⟩ := h₁
      obtain ⟨S₂, hS₂pri, hS₂⟩ := h₂
      refine ⟨S₁ + S₂, by grind, ?_⟩
      rw [Multiset.prod_add]
      exact hS₁.mul_mul hS₂
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : LE.le.{u_1} (α := Submonoid R) (closure {r : R | Prime r}) (closure {r : R | IsUnit r ∨ Prime r})
this : Membership.mem (γ := Submonoid R) (closure {r : R | IsUnit r ∨ Prime r}) a
mem :
  ∀ (z : R) (hz : Membership.mem (γ := Set R) {r : R | IsUnit r ∨ Prime r} z),
    ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod z
⊢ ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod a
have one : ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod 1
Tactic: induction this using closure_induction with
  | mem z hz =>
      rcases hz with h | h
      · exact ⟨∅, by simpa using (associated_one_iff_isUnit.2 h).symm⟩
      · exact ⟨{z}, by simpa⟩
  | one => exact ⟨∅, by simp⟩
  | mul z₁ z₂ hz₁ hz₂ h₁ h₂ =>
      obtain ⟨S₁, hS₁pri, hS₁⟩ := h₁
      obtain ⟨S₂, hS₂pri, hS₂⟩ := h₂
      refine ⟨S₁ + S₂, by grind, ?_⟩
      rw [Multiset.prod_add]
      exact hS₁.mul_mul hS₂
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : LE.le.{u_1} (α := Submonoid R) (closure {r : R | Prime r}) (closure {r : R | IsUnit r ∨ Prime r})
this : Membership.mem (γ := Submonoid R) (closure {r : R | IsUnit r ∨ Prime r}) a
mem :
  ∀ (z : R) (hz : Membership.mem (γ := Set R) {r : R | IsUnit r ∨ Prime r} z),
    ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod z
one : ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod 1
⊢ ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod a
have mul : ∀ (z₁ z₂ : R) (hz₁ : Membership.mem (γ := Submonoid R) (closure {r : R | IsUnit r ∨ Prime r}) z₁)
  (hz₂ : Membership.mem (γ := Submonoid R) (closure {r : R | IsUnit r ∨ Prime r}) z₂)
  (h₁ : ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod z₁)
  (h₂ : ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod z₂),
  ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod (z₁ * z₂)
Tactic: induction this using closure_induction with
  | mem z hz =>
      rcases hz with h | h
      · exact ⟨∅, by simpa using (associated_one_iff_isUnit.2 h).symm⟩
      · exact ⟨{z}, by simpa⟩
  | one => exact ⟨∅, by simp⟩
  | mul z₁ z₂ hz₁ hz₂ h₁ h₂ =>
      obtain ⟨S₁, hS₁pri, hS₁⟩ := h₁
      obtain ⟨S₂, hS₂pri, hS₂⟩ := h₂
      refine ⟨S₁ + S₂, by grind, ?_⟩
      rw [Multiset.prod_add]
      exact hS₁.mul_mul hS₂
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
n : ℕ
⊢ (if Squarefree n then HPow.hPow (α := ℤ) (-1) (factors n).card else 0) = (ArithmeticFunction.moebius : (a : ℕ) → ℤ) n
have e_t : (factors n).card = (ArithmeticFunction.cardFactors : (a : ℕ) → ℕ) n
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : Associated a b
⊢ moebius a = moebius b
have rw : (if Squarefree a then HPow.hPow (α := ℤ) (-1) (factors a).card else 0) = moebius b
Tactic: rw [moebius, moebius, h.squarefree_iff, h.card_factors_eq]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : Associated a b
rw : (if Squarefree a then HPow.hPow (α := ℤ) (-1) (factors a).card else 0) = moebius b
⊢ moebius a = moebius b
have rw₁ : (if Squarefree a then HPow.hPow (α := ℤ) (-1) (factors a).card else 0) =
  if Squarefree b then HPow.hPow (α := ℤ) (-1) (factors b).card else 0
Tactic: rw [moebius, moebius, h.squarefree_iff, h.card_factors_eq]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : Associated a b
rw : (if Squarefree a then HPow.hPow (α := ℤ) (-1) (factors a).card else 0) = moebius b
rw₁ :
  (if Squarefree a then HPow.hPow (α := ℤ) (-1) (factors a).card else 0) =
    if Squarefree b then HPow.hPow (α := ℤ) (-1) (factors b).card else 0
⊢ moebius a = moebius b
have rw₂ : (if Squarefree b then HPow.hPow (α := ℤ) (-1) (factors a).card else 0) =
  if Squarefree b then HPow.hPow (α := ℤ) (-1) (factors b).card else 0
Tactic: rw [moebius, moebius, h.squarefree_iff, h.card_factors_eq]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : Associated a b
rw : (if Squarefree a then HPow.hPow (α := ℤ) (-1) (factors a).card else 0) = moebius b
rw₁ :
  (if Squarefree a then HPow.hPow (α := ℤ) (-1) (factors a).card else 0) =
    if Squarefree b then HPow.hPow (α := ℤ) (-1) (factors b).card else 0
rw₂ :
  (if Squarefree b then HPow.hPow (α := ℤ) (-1) (factors a).card else 0) =
    if Squarefree b then HPow.hPow (α := ℤ) (-1) (factors b).card else 0
⊢ moebius a = moebius b
have rw₃ : (if Squarefree b then HPow.hPow (α := ℤ) (-1) (factors b).card else 0) =
  if Squarefree b then HPow.hPow (α := ℤ) (-1) (factors b).card else 0
Tactic: rw [moebius, moebius, h.squarefree_iff, h.card_factors_eq]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : IsUnit a
⊢ moebius a = 1
have rw : moebius.{u_1} (α := α) 1 = 1
Tactic: rw [(associated_one_iff_isUnit.mpr ha).moebius_eq, moebius_one]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : IsUnit a
rw : moebius.{u_1} (α := α) 1 = 1
⊢ moebius a = 1
have rw₁ : Eq (α := ℤ) 1 1
Tactic: rw [(associated_one_iff_isUnit.mpr ha).moebius_eq, moebius_one]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
⊢ moebius a = -1
have rw : HPow.hPow (α := ℤ) (-1) (factors a).card = -1
Tactic: rw [ha.squarefree.moebius_eq, card_factors_of_irreducible ha, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
rw : HPow.hPow (α := ℤ) (-1) (factors a).card = -1
⊢ moebius a = -1
have rw₁ : HPow.hPow (α := ℤ) (β := ℕ) (-1) 1 = -1
Tactic: rw [ha.squarefree.moebius_eq, card_factors_of_irreducible ha, pow_one]