awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
⊢ span (↑(Finset.image p Finset.univ ∪ Finset.image (a • i) Finset.univ) : Set R) ≤ I
have refine_1 : span (Set.range p) ⊔ span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1) ≤ I
Tactic: simp only [coe_union, coe_image, coe_univ, image_univ, Pi.smul_apply, span_union]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
y : R
hy : y ∈ I
⊢ Membership.mem (γ := Submodule R R) (span (↑(Finset.image p Finset.univ ∪ Finset.image (a • i) Finset.univ) : Set R))
    y
have refine_2 : Membership.mem (γ := Submodule R R) (span (Set.range p) ⊔ span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1)) y
Tactic: simp only [coe_union, coe_image, coe_univ, image_univ, Pi.smul_apply, span_union]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
⊢ span (Set.range p) ⊔ span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1) ≤ I
have refine_1 : (∀ (y : Fin w), p y ∈ (↑I : Set R)) ∧ ∀ (y : Fin w_1), a * i y ∈ (↑I : Set R)
Tactic: simp only [sup_le_iff, span_le, range_subset_iff, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
y : R
hy : y ∈ I
⊢ Membership.mem (γ := Submodule R R) (span (Set.range p) ⊔ span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1)) y
have refine_2 : ∃ (y_1 : R),
  Membership.mem (γ := Submodule R R) (span (Set.range p)) y_1 ∧
    ∃ (z : R), Membership.mem (γ := Submodule R R) (span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1)) z ∧ y_1 + z = y
Tactic: rw [Submodule.mem_sup]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
y : R
hy : y ∈ I
⊢ ∃ (y_1 : R),
    Membership.mem (γ := Submodule R R) (span (Set.range p)) y_1 ∧
      ∃ (z : R), Membership.mem (γ := Submodule R R) (span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1)) z ∧ y_1 + z = y
have refine_2 : ∀ (s : Fin w → R) (H : ∑ i : Fin w, s i * f i = y),
  ∃ (y_1 : R),
    Membership.mem (γ := Submodule R R) (span (Set.range p)) y_1 ∧
      ∃ (z : R), Membership.mem (γ := Submodule R R) (span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1)) z ∧ y_1 + z = y
Tactic: obtain ⟨s, H⟩ := mem_span_range_iff_exists_fun.1 (hf ▸ Ideal.mem_sup_left hy)
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
y : R
hy : y ∈ I
s : Fin w → R
H : ∑ i : Fin w, s i * f i = y
⊢ ∃ (y_1 : R),
    Membership.mem (γ := Submodule R R) (span (Set.range p)) y_1 ∧
      ∃ (z : R), Membership.mem (γ := Submodule R R) (span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1)) z ∧ y_1 + z = y
have H₁ : ∑ x : Fin w, s x * (r x * a + p x) = y
Tactic: simp_rw [← Hf] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
y : R
hy : y ∈ I
s : Fin w → R
H : ∑ x : Fin w, s x * (r x * a + p x) = y
⊢ ∃ (y_1 : R),
    Membership.mem (γ := Submodule R R) (span (Set.range p)) y_1 ∧
      ∃ (z : R), Membership.mem (γ := Submodule R R) (span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1)) z ∧ y_1 + z = y
have H₁ : ∑ x : Fin w, (s x * r x * a + s x * p x) = y
Tactic: ring_nf at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
y : R
hy : y ∈ I
s : Fin w → R
H : ∑ x : Fin w, (s x * r x * a + s x * p x) = y
⊢ ∃ (y_1 : R),
    Membership.mem (γ := Submodule R R) (span (Set.range p)) y_1 ∧
      ∃ (z : R), Membership.mem (γ := Submodule R R) (span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1)) z ∧ y_1 + z = y
have H₁ : ∑ x : Fin w, s x * p x + (∑ i : Fin w, s i * r i) * a = y
Tactic: rw [sum_add_distrib, ← sum_mul, add_comm] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
y : R
hy : y ∈ I
s : Fin w → R
H : ∑ x : Fin w, s x * p x + (∑ i : Fin w, s i * r i) * a = y
⊢ ∃ (y_1 : R),
    Membership.mem (γ := Submodule R R) (span (Set.range p)) y_1 ∧
      ∃ (z : R), Membership.mem (γ := Submodule R R) (span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1)) z ∧ y_1 + z = y
have refine_2 : Membership.mem (γ := Submodule R R) (span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1)) ((∑ k : Fin w, s k * r k) * a)
Tactic: refine ⟨(∑ k, s k * p k), sum_mem _ (fun _ _ ↦ mul_mem_left _ _ mem_span_range_self),
        (∑ k, s k * r k) * a, ?_, H⟩
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
r p : (k : Fin w) → R
p_mem_I : ∀ (k : Fin w), p k ∈ I
Hf : ∀ (k : Fin w), r k * a + p k = f k
y : R
hy : y ∈ I
s : Fin w → R
H : ∑ x : Fin w, s x * p x + (∑ i : Fin w, s i * r i) * a = y
⊢ Membership.mem (γ := Submodule R R) (span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1)) ((∑ k : Fin w, s k * r k) * a)
have refine_2 : HSMul.hSMul (β := R) a (∑ k : Fin w, s k * r k) ∈ a • Submodule.colon I (↑(span {a}) : Set R)
Tactic: rw [mul_comm, ← smul_eq_mul, range_smul, ← submodule_span_eq, Submodule.span_smul, hi]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
⊢ I.FG
have obtain : ∀ (w : ℕ) (f : Fin w → R) (hf : Submodule.span R (Set.range f) = I ⊔ span {a}), I.FG
Tactic: classical
    obtain ⟨_, f, hf⟩ := Submodule.fg_iff_exists_fin_generating_family.1 hsup
    obtain ⟨_, i, hi⟩ := Submodule.fg_iff_exists_fin_generating_family.1 hcolon
    rw [submodule_span_eq] at hf
    have H k : ∃ r : R, ∃ p ∈ I, r * a + p = f k := by
      apply mem_span_singleton_sup.1
      rw [sup_comm, ← hf]
      exact mem_span_range_self
    choose! r p p_mem_I Hf using H
    refine ⟨image p univ ∪ image (a • i) univ, le_antisymm ?_ (fun y hy ↦ ?_)⟩
    <;> simp only [coe_union, coe_image, coe_univ, image_univ, Pi.smul_apply, span_union]
    · simp only [sup_le_iff, span_le, range_subset_iff, smul_eq_mul]
      exact ⟨p_mem_I, fun _ ↦ mul_comm a _ ▸ mem_colon_span_singleton.1 (hi ▸ mem_span_range_self)⟩
    · rw [Submodule.mem_sup]
      obtain ⟨s, H⟩ := mem_span_range_iff_exists_fun.1 (hf ▸ Ideal.mem_sup_left hy)
      simp_rw [← Hf] at H
      ring_nf at H
      rw [sum_add_distrib, ← sum_mul, add_comm] at H
      refine ⟨(∑ k, s k * p k), sum_mem _ (fun _ _ ↦ mul_mem_left _ _ mem_span_range_self),
        (∑ k, s k * r k) * a, ?_, H⟩
      rw [mul_comm, ← smul_eq_mul, range_smul, ← submodule_span_eq, Submodule.span_smul, hi]
      exact smul_mem_smul_set <| mem_colon_span_singleton.2 <|
        (I.add_mem_iff_right <| I.sum_mem (fun _ _ ↦ mul_mem_left _ _ <| p_mem_I _)).1 (H ▸ hy)
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
obtain : ∀ (w : ℕ) (f : Fin w → R) (hf : Submodule.span R (Set.range f) = I ⊔ span {a}), I.FG
⊢ I.FG
have obtain₁ : ∀ (w : ℕ) (f : Fin w → R) (hf : Submodule.span R (Set.range f) = I ⊔ span {a}) (w : ℕ) (i : Fin w → R)
  (hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)), I.FG
Tactic: classical
    obtain ⟨_, f, hf⟩ := Submodule.fg_iff_exists_fin_generating_family.1 hsup
    obtain ⟨_, i, hi⟩ := Submodule.fg_iff_exists_fin_generating_family.1 hcolon
    rw [submodule_span_eq] at hf
    have H k : ∃ r : R, ∃ p ∈ I, r * a + p = f k := by
      apply mem_span_singleton_sup.1
      rw [sup_comm, ← hf]
      exact mem_span_range_self
    choose! r p p_mem_I Hf using H
    refine ⟨image p univ ∪ image (a • i) univ, le_antisymm ?_ (fun y hy ↦ ?_)⟩
    <;> simp only [coe_union, coe_image, coe_univ, image_univ, Pi.smul_apply, span_union]
    · simp only [sup_le_iff, span_le, range_subset_iff, smul_eq_mul]
      exact ⟨p_mem_I, fun _ ↦ mul_comm a _ ▸ mem_colon_span_singleton.1 (hi ▸ mem_span_range_self)⟩
    · rw [Submodule.mem_sup]
      obtain ⟨s, H⟩ := mem_span_range_iff_exists_fun.1 (hf ▸ Ideal.mem_sup_left hy)
      simp_rw [← Hf] at H
      ring_nf at H
      rw [sum_add_distrib, ← sum_mul, add_comm] at H
      refine ⟨(∑ k, s k * p k), sum_mem _ (fun _ _ ↦ mul_mem_left _ _ mem_span_range_self),
        (∑ k, s k * r k) * a, ?_, H⟩
      rw [mul_comm, ← smul_eq_mul, range_smul, ← submodule_span_eq, Submodule.span_smul, hi]
      exact smul_mem_smul_set <| mem_colon_span_singleton.2 <|
        (I.add_mem_iff_right <| I.sum_mem (fun _ _ ↦ mul_mem_left _ _ <| p_mem_I _)).1 (H ▸ hy)
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
obtain : ∀ (w : ℕ) (f : Fin w → R) (hf : Submodule.span R (Set.range f) = I ⊔ span {a}), I.FG
obtain₁ :
  ∀ (w : ℕ) (f : Fin w → R) (hf : Submodule.span R (Set.range f) = I ⊔ span {a}) (w : ℕ) (i : Fin w → R)
    (hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)), I.FG
⊢ I.FG
have obtain₂ : ∀ (w : ℕ) (f : Fin w → R) (hf : span (Set.range f) = I ⊔ span {a}) (w : ℕ) (i : Fin w → R)
  (hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)), I.FG
Tactic: classical
    obtain ⟨_, f, hf⟩ := Submodule.fg_iff_exists_fin_generating_family.1 hsup
    obtain ⟨_, i, hi⟩ := Submodule.fg_iff_exists_fin_generating_family.1 hcolon
    rw [submodule_span_eq] at hf
    have H k : ∃ r : R, ∃ p ∈ I, r * a + p = f k := by
      apply mem_span_singleton_sup.1
      rw [sup_comm, ← hf]
      exact mem_span_range_self
    choose! r p p_mem_I Hf using H
    refine ⟨image p univ ∪ image (a • i) univ, le_antisymm ?_ (fun y hy ↦ ?_)⟩
    <;> simp only [coe_union, coe_image, coe_univ, image_univ, Pi.smul_apply, span_union]
    · simp only [sup_le_iff, span_le, range_subset_iff, smul_eq_mul]
      exact ⟨p_mem_I, fun _ ↦ mul_comm a _ ▸ mem_colon_span_singleton.1 (hi ▸ mem_span_range_self)⟩
    · rw [Submodule.mem_sup]
      obtain ⟨s, H⟩ := mem_span_range_iff_exists_fun.1 (hf ▸ Ideal.mem_sup_left hy)
      simp_rw [← Hf] at H
      ring_nf at H
      rw [sum_add_distrib, ← sum_mul, add_comm] at H
      refine ⟨(∑ k, s k * p k), sum_mem _ (fun _ _ ↦ mul_mem_left _ _ mem_span_range_self),
        (∑ k, s k * r k) * a, ?_, H⟩
      rw [mul_comm, ← smul_eq_mul, range_smul, ← submodule_span_eq, Submodule.span_smul, hi]
      exact smul_mem_smul_set <| mem_colon_span_singleton.2 <|
        (I.add_mem_iff_right <| I.sum_mem (fun _ _ ↦ mul_mem_left _ _ <| p_mem_I _)).1 (H ▸ hy)
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
obtain : ∀ (w : ℕ) (f : Fin w → R) (hf : Submodule.span R (Set.range f) = I ⊔ span {a}), I.FG
obtain₁ :
  ∀ (w : ℕ) (f : Fin w → R) (hf : Submodule.span R (Set.range f) = I ⊔ span {a}) (w : ℕ) (i : Fin w → R)
    (hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)), I.FG
obtain₂ :
  ∀ (w : ℕ) (f : Fin w → R) (hf : span (Set.range f) = I ⊔ span {a}) (w : ℕ) (i : Fin w → R)
    (hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)), I.FG
⊢ I.FG
have obtain₃ : ∀ (w : ℕ) (f : Fin w → R) (hf : span (Set.range f) = I ⊔ span {a}) (w_1 : ℕ) (i : Fin w_1 → R)
  (hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R))
  (H : ∀ (k : Fin w), ∃ (r : R), ∃ p ∈ I, r * a + p = f k), I.FG
Tactic: classical
    obtain ⟨_, f, hf⟩ := Submodule.fg_iff_exists_fin_generating_family.1 hsup
    obtain ⟨_, i, hi⟩ := Submodule.fg_iff_exists_fin_generating_family.1 hcolon
    rw [submodule_span_eq] at hf
    have H k : ∃ r : R, ∃ p ∈ I, r * a + p = f k := by
      apply mem_span_singleton_sup.1
      rw [sup_comm, ← hf]
      exact mem_span_range_self
    choose! r p p_mem_I Hf using H
    refine ⟨image p univ ∪ image (a • i) univ, le_antisymm ?_ (fun y hy ↦ ?_)⟩
    <;> simp only [coe_union, coe_image, coe_univ, image_univ, Pi.smul_apply, span_union]
    · simp only [sup_le_iff, span_le, range_subset_iff, smul_eq_mul]
      exact ⟨p_mem_I, fun _ ↦ mul_comm a _ ▸ mem_colon_span_singleton.1 (hi ▸ mem_span_range_self)⟩
    · rw [Submodule.mem_sup]
      obtain ⟨s, H⟩ := mem_span_range_iff_exists_fun.1 (hf ▸ Ideal.mem_sup_left hy)
      simp_rw [← Hf] at H
      ring_nf at H
      rw [sum_add_distrib, ← sum_mul, add_comm] at H
      refine ⟨(∑ k, s k * p k), sum_mem _ (fun _ _ ↦ mul_mem_left _ _ mem_span_range_self),
        (∑ k, s k * r k) * a, ?_, H⟩
      rw [mul_comm, ← smul_eq_mul, range_smul, ← submodule_span_eq, Submodule.span_smul, hi]
      exact smul_mem_smul_set <| mem_colon_span_singleton.2 <|
        (I.add_mem_iff_right <| I.sum_mem (fun _ _ ↦ mul_mem_left _ _ <| p_mem_I _)).1 (H ▸ hy)
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
obtain : ∀ (w : ℕ) (f : Fin w → R) (hf : Submodule.span R (Set.range f) = I ⊔ span {a}), I.FG
obtain₁ :
  ∀ (w : ℕ) (f : Fin w → R) (hf : Submodule.span R (Set.range f) = I ⊔ span {a}) (w : ℕ) (i : Fin w → R)
    (hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)), I.FG
obtain₂ :
  ∀ (w : ℕ) (f : Fin w → R) (hf : span (Set.range f) = I ⊔ span {a}) (w : ℕ) (i : Fin w → R)
    (hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)), I.FG
obtain₃ :
  ∀ (w : ℕ) (f : Fin w → R) (hf : span (Set.range f) = I ⊔ span {a}) (w_1 : ℕ) (i : Fin w_1 → R)
    (hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R))
    (H : ∀ (k : Fin w), ∃ (r : R), ∃ p ∈ I, r * a + p = f k), I.FG
⊢ I.FG
have obtain₄ : ∀ (w : ℕ) (f : Fin w → R) (hf : span (Set.range f) = I ⊔ span {a}) (w_1 : ℕ) (i : Fin w_1 → R)
  (hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)) (r p : (k : Fin w) → R)
  (p_mem_I : ∀ (k : Fin w), p k ∈ I) (Hf : ∀ (k : Fin w), r k * a + p k = f k), I.FG
Tactic: classical
    obtain ⟨_, f, hf⟩ := Submodule.fg_iff_exists_fin_generating_family.1 hsup
    obtain ⟨_, i, hi⟩ := Submodule.fg_iff_exists_fin_generating_family.1 hcolon
    rw [submodule_span_eq] at hf
    have H k : ∃ r : R, ∃ p ∈ I, r * a + p = f k := by
      apply mem_span_singleton_sup.1
      rw [sup_comm, ← hf]
      exact mem_span_range_self
    choose! r p p_mem_I Hf using H
    refine ⟨image p univ ∪ image (a • i) univ, le_antisymm ?_ (fun y hy ↦ ?_)⟩
    <;> simp only [coe_union, coe_image, coe_univ, image_univ, Pi.smul_apply, span_union]
    · simp only [sup_le_iff, span_le, range_subset_iff, smul_eq_mul]
      exact ⟨p_mem_I, fun _ ↦ mul_comm a _ ▸ mem_colon_span_singleton.1 (hi ▸ mem_span_range_self)⟩
    · rw [Submodule.mem_sup]
      obtain ⟨s, H⟩ := mem_span_range_iff_exists_fun.1 (hf ▸ Ideal.mem_sup_left hy)
      simp_rw [← Hf] at H
      ring_nf at H
      rw [sum_add_distrib, ← sum_mul, add_comm] at H
      refine ⟨(∑ k, s k * p k), sum_mem _ (fun _ _ ↦ mul_mem_left _ _ mem_span_range_self),
        (∑ k, s k * r k) * a, ?_, H⟩
      rw [mul_comm, ← smul_eq_mul, range_smul, ← submodule_span_eq, Submodule.span_smul, hi]
      exact smul_mem_smul_set <| mem_colon_span_singleton.2 <|
        (I.add_mem_iff_right <| I.sum_mem (fun _ _ ↦ mul_mem_left _ _ <| p_mem_I _)).1 (H ▸ hy)
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
obtain : ∀ (w : ℕ) (f : Fin w → R) (hf : Submodule.span R (Set.range f) = I ⊔ span {a}), I.FG
obtain₁ :
  ∀ (w : ℕ) (f : Fin w → R) (hf : Submodule.span R (Set.range f) = I ⊔ span {a}) (w : ℕ) (i : Fin w → R)
    (hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)), I.FG
obtain₂ :
  ∀ (w : ℕ) (f : Fin w → R) (hf : span (Set.range f) = I ⊔ span {a}) (w : ℕ) (i : Fin w → R)
    (hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)), I.FG
obtain₃ :
  ∀ (w : ℕ) (f : Fin w → R) (hf : span (Set.range f) = I ⊔ span {a}) (w_1 : ℕ) (i : Fin w_1 → R)
    (hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R))
    (H : ∀ (k : Fin w), ∃ (r : R), ∃ p ∈ I, r * a + p = f k), I.FG
obtain₄ :
  ∀ (w : ℕ) (f : Fin w → R) (hf : span (Set.range f) = I ⊔ span {a}) (w_1 : ℕ) (i : Fin w_1 → R)
    (hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)) (r p : (k : Fin w) → R)
    (p_mem_I : ∀ (k : Fin w), p k ∈ I) (Hf : ∀ (k : Fin w), r k * a + p k = f k), I.FG
⊢ I.FG
have refine_1 : ∀ (w : ℕ) (f : Fin w → R) (hf : span (Set.range f) = I ⊔ span {a}) (w_1 : ℕ) (i : Fin w_1 → R)
  (hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)) (r p : (k : Fin w) → R)
  (p_mem_I : ∀ (k : Fin w), p k ∈ I) (Hf : ∀ (k : Fin w), r k * a + p k = f k),
  span (Set.range p) ⊔ span (Set.range fun (a_1 : Fin w_1) ↦ a • i a_1) ≤ I
Tactic: classical
    obtain ⟨_, f, hf⟩ := Submodule.fg_iff_exists_fin_generating_family.1 hsup
    obtain ⟨_, i, hi⟩ := Submodule.fg_iff_exists_fin_generating_family.1 hcolon
    rw [submodule_span_eq] at hf
    have H k : ∃ r : R, ∃ p ∈ I, r * a + p = f k := by
      apply mem_span_singleton_sup.1
      rw [sup_comm, ← hf]
      exact mem_span_range_self
    choose! r p p_mem_I Hf using H
    refine ⟨image p univ ∪ image (a • i) univ, le_antisymm ?_ (fun y hy ↦ ?_)⟩
    <;> simp only [coe_union, coe_image, coe_univ, image_univ, Pi.smul_apply, span_union]
    · simp only [sup_le_iff, span_le, range_subset_iff, smul_eq_mul]
      exact ⟨p_mem_I, fun _ ↦ mul_comm a _ ▸ mem_colon_span_singleton.1 (hi ▸ mem_span_range_self)⟩
    · rw [Submodule.mem_sup]
      obtain ⟨s, H⟩ := mem_span_range_iff_exists_fun.1 (hf ▸ Ideal.mem_sup_left hy)
      simp_rw [← Hf] at H
      ring_nf at H
      rw [sum_add_distrib, ← sum_mul, add_comm] at H
      refine ⟨(∑ k, s k * p k), sum_mem _ (fun _ _ ↦ mul_mem_left _ _ mem_span_range_self),
        (∑ k, s k * r k) * a, ?_, H⟩
      rw [mul_comm, ← smul_eq_mul, range_smul, ← submodule_span_eq, Submodule.span_smul, hi]
      exact smul_mem_smul_set <| mem_colon_span_singleton.2 <|
        (I.add_mem_iff_right <| I.sum_mem (fun _ _ ↦ mul_mem_left _ _ <| p_mem_I _)).1 (H ▸ hy)
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
Goal:
R : Type u_1
inst : CommRing R
H : ∀ (I : Ideal R), I.IsPrime → I.FG
⊢ IsNoetherianRing R
have refine : ∀ (C : Set (Ideal R)) (hC₁ : C ⊆ {I : Ideal R | ¬I.FG}) (hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C)
  (I : Ideal R) (hI : I ∈ C) (h : (sSup C).FG), sSup C ∈ C
Tactic: refine ⟨isOka_fg.forall_of_forall_prime' (fun C hC₁ hC₂ I hI h ↦ ⟨sSup C, ?_, h⟩) H⟩
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
Goal:
R : Type u_1
inst : CommRing R
H : ∀ (I : Ideal R), I.IsPrime → I.FG
C : Set (Ideal R)
hC₁ : C ⊆ {I : Ideal R | ¬I.FG}
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
I : Ideal R
hI : I ∈ C
h : (sSup C).FG
⊢ sSup C ∈ C
have obtain : ∀ (G : Finset R) (hG : span (↑G : Set R) = sSup C), sSup C ∈ C
Tactic: obtain ⟨G, hG⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
Goal:
R : Type u_1
inst : CommRing R
H : ∀ (I : Ideal R), I.IsPrime → I.FG
C : Set (Ideal R)
hC₁ : C ⊆ {I : Ideal R | ¬I.FG}
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
I : Ideal R
hI : I ∈ C
G : Finset R
hG : span (↑G : Set R) = sSup C
⊢ ∃ J ∈ C, (↑G : Set R) ⊆ (↑J : Set R)
have refine : ∀ (x : R) (hx : x ∈ (↑G : Set R)), Membership.mem (γ := Set R) (⋃ i ∈ C, (↑i : Set R)) x
Tactic: refine hC₂.directedOn.exists_mem_subset_of_finset_subset_biUnion ⟨I, hI⟩ (fun _ hx ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
Goal:
R : Type u_1
inst : CommRing R
H : ∀ (I : Ideal R), I.IsPrime → I.FG
C : Set (Ideal R)
hC₁ : C ⊆ {I : Ideal R | ¬I.FG}
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
I : Ideal R
hI : I ∈ C
G : Finset R
hG : span (↑G : Set R) = sSup C
x : R
hx : x ∈ (↑G : Set R)
⊢ Membership.mem (γ := Set R) (⋃ i ∈ C, (↑i : Set R)) x
have simp : ∃ i ∈ C, x ∈ i
Tactic: simp only [Set.mem_iUnion, SetLike.mem_coe, exists_prop]