awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Prime (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
x y a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hx : x * y = a * p i * ∏ x ∈ s, p x
hpi : Prime (p i)
⊢ ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
    t ∪ u = insert i s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
have insert : ∀ (t u : Finset α) (b c : R) (htus : t ∪ u = s) (htu : Disjoint t u) (hbc : a * p i = b * c)
  (hx : (b * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x),
  ∃ (t_1 : Finset α) (u_1 : Finset α) (b_1 : R) (c_1 : R),
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b_1 * c_1 ∧ b * ∏ i ∈ t, p i = b_1 * ∏ i ∈ t_1, p i ∧ c * ∏ i ∈ u, p i = c_1 * ∏ i ∈ u_1, p i
Tactic: rcases ih (fun i hi ↦ hp i (mem_insert_of_mem hi)) hx with
      ⟨t, u, b, c, htus, htu, hbc, rfl, rfl⟩
Cleared hypotheses: x, y, hx
-- Lean 4 proof step from Mathlib.RingTheory.Prime (hypothesis)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b c : R
htus : t ∪ u = s
htu : Disjoint t u
hbc : a * p i = b * c
hx : (b * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ ∃ (t_1 : Finset α) (u_1 : Finset α) (b_1 : R) (c_1 : R),
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b_1 * c_1 ∧ b * ∏ i ∈ t, p i = b_1 * ∏ i ∈ t_1, p i ∧ c * ∏ i ∈ u, p i = c_1 * ∏ i ∈ u_1, p i
have hit : i ∉ t
Tactic: have hit : i ∉ t := fun hit ↦ his (htus ▸ mem_union_left _ hit)
-- Lean 4 proof step from Mathlib.RingTheory.Prime (hypothesis)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b c : R
htus : t ∪ u = s
htu : Disjoint t u
hbc : a * p i = b * c
hx : (b * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
hit : i ∉ t
⊢ ∃ (t_1 : Finset α) (u_1 : Finset α) (b_1 : R) (c_1 : R),
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b_1 * c_1 ∧ b * ∏ i ∈ t, p i = b_1 * ∏ i ∈ t_1, p i ∧ c * ∏ i ∈ u, p i = c_1 * ∏ i ∈ u_1, p i
have hiu : i ∉ u
Tactic: have hiu : i ∉ u := fun hiu ↦ his (htus ▸ mem_union_right _ hiu)
-- Lean 4 proof step from Mathlib.RingTheory.Prime (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b c : R
htus : t ∪ u = s
htu : Disjoint t u
hbc : a * p i = b * c
hx : (b * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
hit : i ∉ t
hiu : i ∉ u
⊢ b * c = p i * a
have rw : a * p i = p i * a
Tactic: rw [← hbc, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Prime (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b c : R
htus : t ∪ u = s
htu : Disjoint t u
hbc : a * p i = b * c
hx : (b * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
hit : i ∉ t
hiu : i ∉ u
rw : a * p i = p i * a
⊢ b * c = p i * a
have rw₁ : p i * a = p i * a
Tactic: rw [← hbc, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Prime (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b c : R
htus : t ∪ u = s
htu : Disjoint t u
hbc : a * p i = b * c
hx : (b * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
hit : i ∉ t
hiu : i ∉ u
⊢ ∃ (t_1 : Finset α) (u_1 : Finset α) (b_1 : R) (c_1 : R),
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b_1 * c_1 ∧ b * ∏ i ∈ t, p i = b_1 * ∏ i ∈ t_1, p i ∧ c * ∏ i ∈ u, p i = c_1 * ∏ i ∈ u_1, p i
have insert : ∀ (d : R) (hbc : a * p i = p i * d * c) (hx : (p i * d * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x),
  ∃ (t_1 : Finset α) (u_1 : Finset α) (b : R) (c_1 : R),
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b * c_1 ∧ p i * d * ∏ i ∈ t, p i = b * ∏ i ∈ t_1, p i ∧ c * ∏ i ∈ u, p i = c_1 * ∏ i ∈ u_1, p i
Tactic: obtain ⟨d, rfl⟩ | ⟨d, rfl⟩ : p i ∣ b ∨ p i ∣ c := hpi.dvd_or_dvd ⟨a, by rw [← hbc, mul_comm]⟩
Cleared hypotheses: b, hbc, hx
-- Lean 4 proof step from Mathlib.RingTheory.Prime (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ Insert.insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b c : R
htus : t ∪ u = s
htu : Disjoint t u
hbc : a * p i = b * c
hx : (b * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
hit : i ∉ t
hiu : i ∉ u
insert :
  ∀ (d : R) (hbc : a * p i = p i * d * c) (hx : (p i * d * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x),
    ∃ (t_1 : Finset α) (u_1 : Finset α) (b : R) (c_1 : R),
      t_1 ∪ u_1 = Insert.insert i s ∧
        Disjoint t_1 u_1 ∧
          a = b * c_1 ∧ p i * d * ∏ i ∈ t, p i = b * ∏ i ∈ t_1, p i ∧ c * ∏ i ∈ u, p i = c_1 * ∏ i ∈ u_1, p i
⊢ ∃ (t_1 : Finset α) (u_1 : Finset α) (b_1 : R) (c_1 : R),
    t_1 ∪ u_1 = Insert.insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b_1 * c_1 ∧ b * ∏ i ∈ t, p i = b_1 * ∏ i ∈ t_1, p i ∧ c * ∏ i ∈ u, p i = c_1 * ∏ i ∈ u_1, p i
have insert₁ : ∀ (d : R) (hbc : a * p i = b * (p i * d)) (hx : (b * ∏ i ∈ t, p i) * (p i * d * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x),
  ∃ (t_1 : Finset α) (u_1 : Finset α) (b_1 : R) (c : R),
    t_1 ∪ u_1 = Insert.insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b_1 * c ∧ b * ∏ i ∈ t, p i = b_1 * ∏ i ∈ t_1, p i ∧ p i * d * ∏ i ∈ u, p i = c * ∏ i ∈ u_1, p i
Tactic: obtain ⟨d, rfl⟩ | ⟨d, rfl⟩ : p i ∣ b ∨ p i ∣ c := hpi.dvd_or_dvd ⟨a, by rw [← hbc, mul_comm]⟩
Cleared hypotheses: c, hbc, hx
-- Lean 4 proof step from Mathlib.RingTheory.Prime (hypothesis)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
c : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a * p i = p i * d * c
hx : (p i * d * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ ∃ (t_1 : Finset α) (u_1 : Finset α) (b : R) (c_1 : R),
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b * c_1 ∧ p i * d * ∏ i ∈ t, p i = b * ∏ i ∈ t_1, p i ∧ c * ∏ i ∈ u, p i = c_1 * ∏ i ∈ u_1, p i
have hbc₁ : a = d * c
Tactic: rw [mul_assoc, mul_comm a, mul_right_inj' hpi.ne_zero] at hbc
Cleared hypotheses: hbc, hx
-- Lean 4 proof step from Mathlib.RingTheory.Prime (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
c : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a = d * c
hx : (p i * d * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ insert i t ∪ u = insert i s
have rw : insert i (t ∪ u) = insert i s
Tactic: rw [insert_union, htus]
-- Lean 4 proof step from Mathlib.RingTheory.Prime (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
c : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a = d * c
hx : (p i * d * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
rw : insert i (t ∪ u) = insert i s
⊢ insert i t ∪ u = insert i s
have rw₁ : insert i s = insert i s
Tactic: rw [insert_union, htus]
-- Lean 4 proof step from Mathlib.RingTheory.Prime (hypothesis)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a * p i = b * (p i * d)
hx : (b * ∏ i ∈ t, p i) * (p i * d * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ ∃ (t_1 : Finset α) (u_1 : Finset α) (b_1 : R) (c : R),
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b_1 * c ∧ b * ∏ i ∈ t, p i = b_1 * ∏ i ∈ t_1, p i ∧ p i * d * ∏ i ∈ u, p i = c * ∏ i ∈ u_1, p i
have hbc₁ : a = b * d
Tactic: rw [← mul_assoc, mul_right_comm b, mul_left_inj' hpi.ne_zero] at hbc
Cleared hypotheses: hbc, hx
-- Lean 4 proof step from Mathlib.RingTheory.Prime (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a = b * d
hx : (b * ∏ i ∈ t, p i) * (p i * d * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ t ∪ insert i u = insert i s
have rw : insert i (t ∪ u) = insert i s
Tactic: rw [union_insert, htus]
-- Lean 4 proof step from Mathlib.RingTheory.Prime (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a = b * d
hx : (b * ∏ i ∈ t, p i) * (p i * d * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
rw : insert i (t ∪ u) = insert i s
⊢ t ∪ insert i u = insert i s
have rw₁ : insert i s = insert i s
Tactic: rw [union_insert, htus]
-- Lean 4 proof step from Mathlib.RingTheory.Prime (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
x y a : R
s : Finset α
p : α → R
hp : ∀ i ∈ s, Prime (p i)
hx : x * y = a * ∏ i ∈ s, p i
⊢ ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
    t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
have empty : ∀ {x y a : R} (hp : ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → Prime (p i)) (hx : x * y = a * ∏ i ∈ ∅, p i),
  ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
    t ∪ u = ∅ ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
Tactic: induction s using Finset.induction generalizing x y a with
  | empty => exact ⟨∅, ∅, x, y, by simp [hx]⟩
  | insert i s his ih =>
    rw [prod_insert his, ← mul_assoc] at hx
    have hpi : Prime (p i) := hp i (mem_insert_self _ _)
    rcases ih (fun i hi ↦ hp i (mem_insert_of_mem hi)) hx with
      ⟨t, u, b, c, htus, htu, hbc, rfl, rfl⟩
    have hit : i ∉ t := fun hit ↦ his (htus ▸ mem_union_left _ hit)
    have hiu : i ∉ u := fun hiu ↦ his (htus ▸ mem_union_right _ hiu)
    obtain ⟨d, rfl⟩ | ⟨d, rfl⟩ : p i ∣ b ∨ p i ∣ c := hpi.dvd_or_dvd ⟨a, by rw [← hbc, mul_comm]⟩
    · rw [mul_assoc, mul_comm a, mul_right_inj' hpi.ne_zero] at hbc
      exact ⟨insert i t, u, d, c, by rw [insert_union, htus], disjoint_insert_left.2 ⟨hiu, htu⟩, by
          simp [hbc, prod_insert hit, mul_comm, mul_left_comm]⟩
    · rw [← mul_assoc, mul_right_comm b, mul_left_inj' hpi.ne_zero] at hbc
      exact ⟨t, insert i u, b, d, by rw [union_insert, htus], disjoint_insert_right.2 ⟨hit, htu⟩, by
          simp [← hbc, prod_insert hiu, mul_comm, mul_left_comm]⟩
Cleared hypotheses: x, y, a, s, hp, hx
-- Lean 4 proof step from Mathlib.RingTheory.Prime (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
x y a : R
s : Finset α
p : α → R
hp : ∀ i ∈ s, Prime (p i)
hx : x * y = a * ∏ i ∈ s, p i
empty :
  ∀ {x y a : R} (hp : ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → Prime (p i)) (hx : x * y = a * ∏ i ∈ ∅, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = ∅ ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
⊢ ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
    t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
have insert : ∀ (i : α) (s : Finset α) (his : i ∉ s)
  (ih :
    ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
      ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
        t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i)
  {x y a : R} (hp : ∀ i_1 ∈ insert i s, Prime (p i_1)) (hx : x * y = a * ∏ i ∈ insert i s, p i),
  ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
    t ∪ u = insert i s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
Tactic: induction s using Finset.induction generalizing x y a with
  | empty => exact ⟨∅, ∅, x, y, by simp [hx]⟩
  | insert i s his ih =>
    rw [prod_insert his, ← mul_assoc] at hx
    have hpi : Prime (p i) := hp i (mem_insert_self _ _)
    rcases ih (fun i hi ↦ hp i (mem_insert_of_mem hi)) hx with
      ⟨t, u, b, c, htus, htu, hbc, rfl, rfl⟩
    have hit : i ∉ t := fun hit ↦ his (htus ▸ mem_union_left _ hit)
    have hiu : i ∉ u := fun hiu ↦ his (htus ▸ mem_union_right _ hiu)
    obtain ⟨d, rfl⟩ | ⟨d, rfl⟩ : p i ∣ b ∨ p i ∣ c := hpi.dvd_or_dvd ⟨a, by rw [← hbc, mul_comm]⟩
    · rw [mul_assoc, mul_comm a, mul_right_inj' hpi.ne_zero] at hbc
      exact ⟨insert i t, u, d, c, by rw [insert_union, htus], disjoint_insert_left.2 ⟨hiu, htu⟩, by
          simp [hbc, prod_insert hit, mul_comm, mul_left_comm]⟩
    · rw [← mul_assoc, mul_right_comm b, mul_left_inj' hpi.ne_zero] at hbc
      exact ⟨t, insert i u, b, d, by rw [union_insert, htus], disjoint_insert_right.2 ⟨hit, htu⟩, by
          simp [← hbc, prod_insert hiu, mul_comm, mul_left_comm]⟩
Cleared hypotheses: x, y, a, s, hp, hx
-- Lean 4 proof step from Mathlib.RingTheory.Prime (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x y a p : R
n : ℕ
hp : Prime p
hx : x * y = a * p ^ n
⊢ ∃ (i : ℕ) (j : ℕ) (b : R) (c : R), i + j = n ∧ a = b * c ∧ x = b * p ^ i ∧ y = c * p ^ j
have rcases : ∀ (t u : Finset ℕ) (b c : R) (htus : t ∪ u = range n) (htu : Disjoint t u)
  (hx : (b * ∏ i ∈ t, p) * (c * ∏ i ∈ u, p) = b * c * p ^ n),
  ∃ (i : ℕ) (j : ℕ) (b_1 : R) (c_1 : R),
    i + j = n ∧ b * c = b_1 * c_1 ∧ b * ∏ i ∈ t, p = b_1 * p ^ i ∧ c * ∏ i ∈ u, p = c_1 * p ^ j
Tactic: rcases mul_eq_mul_prime_prod (fun _ _ ↦ hp)
    (show x * y = a * (range n).prod fun _ ↦ p by simpa) with
      ⟨t, u, b, c, htus, htu, rfl, rfl, rfl⟩
Cleared hypotheses: x, y, a, hx
-- Lean 4 proof step from Mathlib.RingTheory.Prime (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
p : R
n : ℕ
hp : Prime p
t u : Finset ℕ
b c : R
htus : t ∪ u = range n
htu : Disjoint t u
hx : (b * ∏ i ∈ t, p) * (c * ∏ i ∈ u, p) = b * c * p ^ n
⊢ #t + #u = n
have rw : #(t ∪ u) = n
Tactic: rw [← card_union_of_disjoint htu, htus, card_range]
-- Lean 4 proof step from Mathlib.RingTheory.Prime (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
p : R
n : ℕ
hp : Prime p
t u : Finset ℕ
b c : R
htus : t ∪ u = range n
htu : Disjoint t u
hx : (b * ∏ i ∈ t, p) * (c * ∏ i ∈ u, p) = b * c * p ^ n
rw : #(t ∪ u) = n
⊢ #t + #u = n
have rw₁ : #(range n) = n
Tactic: rw [← card_union_of_disjoint htu, htus, card_range]
-- Lean 4 proof step from Mathlib.RingTheory.Prime (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
p : R
n : ℕ
hp : Prime p
t u : Finset ℕ
b c : R
htus : t ∪ u = range n
htu : Disjoint t u
hx : (b * ∏ i ∈ t, p) * (c * ∏ i ∈ u, p) = b * c * p ^ n
rw : #(t ∪ u) = n
rw₁ : #(range n) = n
⊢ #t + #u = n
have rw₂ : n = n
Tactic: rw [← card_union_of_disjoint htu, htus, card_range]
-- Lean 4 proof step from Mathlib.RingTheory.Prime (hypothesis)
Goal:
α : Type u_1
inst : CommRing α
p : α
hp : Prime p
⊢ Prime (-p)
have h1 : p ≠ 0
Tactic: obtain ⟨h1, h2, h3⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Prime (hypothesis)
Goal:
α : Type u_1
inst : CommRing α
p : α
hp : Prime p
h1 : p ≠ 0
⊢ Prime (-p)
have h2 : ¬IsUnit p
Tactic: obtain ⟨h1, h2, h3⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Prime (hypothesis)
Goal:
α : Type u_1
inst : CommRing α
p : α
hp : Prime p
h1 : p ≠ 0
h2 : ¬IsUnit p
⊢ Prime (-p)
have h3 : ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
Tactic: obtain ⟨h1, h2, h3⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Prime (goal)
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
p : α
hp : Prime p
⊢ Prime |p|
have inl : ∀ (h : |p| = p), Prime |p|
Tactic: obtain h | h := abs_choice p
-- Lean 4 proof step from Mathlib.RingTheory.Prime (goal)
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
p : α
hp : Prime p
inl : ∀ (h : |p| = p), Prime |p|
⊢ Prime |p|
have inr : ∀ (h : |p| = -p), Prime |p|
Tactic: obtain h | h := abs_choice p
-- Lean 4 proof step from Mathlib.RingTheory.Prime (goal)
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
p : α
hp : Prime p
h : |p| = -p
⊢ Prime |p|
have inr : Prime (-p)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
K : Type u
inst_3 : DivisionSemiring K
S : Ideal K
⊢ IsPrincipal S
have inl : IsPrincipal.{u, u} (R := K) (M := K) ⊥
Tactic: rcases Ideal.eq_bot_or_top S with (rfl | rfl)
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
K : Type u
inst_3 : DivisionSemiring K
S : Ideal K
inl : IsPrincipal.{u, u} (R := K) (M := K) ⊥
⊢ IsPrincipal S
have inr : IsPrincipal.{u, u} (R := K) (M := K) ⊤
Tactic: rcases Ideal.eq_bot_or_top S with (rfl | rfl)
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (hypothesis)
Goal:
R : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
S : Submodule R M
inst_3 : S.IsPrincipal
⊢ generator S ∈ S
have this : Membership.mem (γ := Submodule R M) (R ∙ generator S) (generator S)
Tactic: have : generator S ∈ span R {generator S} := subset_span (mem_singleton _)
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
S : Submodule R M
inst_3 : S.IsPrincipal
this : Membership.mem (γ := Submodule R M) (R ∙ generator S) (generator S)
⊢ generator S ∈ S
have h : S = R ∙ generator S
Tactic: convert! this
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
S : Submodule R M
inst_3 : S.IsPrincipal
x : M
⊢ x ∈ S ↔ ∃ (s : R), x = s • generator S
have simp_rw : x ∈ S ↔ ∃ (s : R), s • generator S = x
Tactic: simp_rw [@eq_comm _ x, ← mem_span_singleton, span_singleton_generator]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
S : Submodule R M
inst_3 : S.IsPrincipal
x : M
simp_rw : x ∈ S ↔ ∃ (s : R), s • generator S = x
⊢ x ∈ S ↔ ∃ (s : R), x = s • generator S
have simp_rw₁ : x ∈ S ↔ Membership.mem (γ := Submodule R M) (R ∙ generator S) x
Tactic: simp_rw [@eq_comm _ x, ← mem_span_singleton, span_singleton_generator]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
S : Submodule R M
inst_3 : S.IsPrincipal
⊢ S = ⊥ ↔ generator S = 0
have rw : S = ⊥ ↔ Eq (α := Submodule R M) (R ∙ generator S) ⊥
Tactic: rw [← @span_singleton_eq_bot R M, span_singleton_generator]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
S : Submodule R M
inst_3 : S.IsPrincipal
rw : S = ⊥ ↔ Eq (α := Submodule R M) (R ∙ generator S) ⊥
⊢ S = ⊥ ↔ generator S = 0
have rw₁ : S = ⊥ ↔ S = ⊥
Tactic: rw [← @span_singleton_eq_bot R M, span_singleton_generator]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsDomain R
r : R
⊢ Associated (generator (Ideal.span {r})) r
have rw : Eq (α := Ideal R) (Ideal.span {generator (Ideal.span {r})}) (Ideal.span {r})
Tactic: rw [← Ideal.span_singleton_eq_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : Module R M
N : Submodule R M
ϕ : M →ₗ[R] R
inst_3 : (map ϕ N).IsPrincipal
x : M
hx : x ∈ N
⊢ generator (map ϕ N) ∣ (ϕ : (a : M) → R) x
have rw : ∃ y ∈ N, Eq.{u + 1} (α := R) ((ϕ : (a : M) → R) y : R) ((ϕ : (a : M) → R) x : R)
Tactic: rw [← mem_iff_generator_dvd, Submodule.mem_map]