-- Module: Mathlib.RingTheory.Noetherian.OfPrime
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
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
refine_2 refine_2₁ :
  ∀ (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
⊢ 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)

Premises used: Ideal.span_le, Iff.mpr, Set.image_univ, Ideal.mem_colon_span_singleton, Ideal.submodule_span_eq, Finset.coe_univ, Finset.sum_add_distrib, Finset.coe_image, add_comm, sup_le_iff, Submodule.fg_iff_exists_fin_generating_family, Ideal.mem_span_range_iff_exists_fun, Submodule.span_smul, Iff.mp, mul_comm, Set.range_smul, Submodule.mem_sup, smul_eq_mul, Set.range_subset_iff, Ideal.span_union, Finset.sum_mul, Set.smul_mem_smul_set, Finset.coe_union, Pi.smul_apply