-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
x : R₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
hI : IsNoetherian.{u_3, u_4} R₁ ↥(↑I : Submodule R₁ K)
pos :
  ∀ (hx : x = 0),
    IsNoetherian.{u_3, u_4} R₁
      ↥(↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
              (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
              I) :
          Submodule R₁ K)
neg neg₁ :
  ∀ (hx : ¬x = 0),
    IsNoetherian.{u_3, u_4} R₁
      ↥(↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
              (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
              I) :
          Submodule R₁ K)
neg₂ :
  ∀ (hx : ¬x = 0) (h_gx : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) x : K) (0 : K)),
    IsNoetherian.{u_3, u_4} R₁
      ↥(↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
              (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
              I) :
          Submodule R₁ K)
neg₃ :
  ∀ (hx : ¬x = 0) (h_gx : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) x : K) (0 : K))
    (h_spanx :
      Ne.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (0 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)),
    IsNoetherian.{u_3, u_4} R₁
      ↥(↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
              (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
              I) :
          Submodule R₁ K)
neg₄ neg₅ :
  ∀ (hI : ∀ J ≤ I, (↑J : Submodule R₁ K).FG) (hx : ¬x = 0)
    (h_gx : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) x : K) (0 : K))
    (h_spanx :
      Ne.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (0 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K))
    (J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (hJ :
      J ≤
        HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
          (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) I),
    (↑J : Submodule R₁ K).FG
neg₆ :
  ∀ (hI : ∀ J ≤ I, (↑J : Submodule R₁ K).FG) (hx : ¬x = 0)
    (h_gx : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) x : K) (0 : K))
    (h_spanx :
      Ne.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (0 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K))
    (J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (hJ :
      HMul.hMul (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) J
          (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) ≤
        I),
    (↑J : Submodule R₁ K).FG
neg₇ :
  ∀ (hI : ∀ J ≤ I, (↑J : Submodule R₁ K).FG) (hx : ¬x = 0)
    (h_gx : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) x : K) (0 : K))
    (h_spanx :
      Ne.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (0 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K))
    (J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (hJ :
      HMul.hMul (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) J
          (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) ≤
        I)
    (s : Finset K)
    (hs :
      span R₁ (↑s : Set K) =
        (↑(HMul.hMul (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) J
              (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)) :
          Submodule R₁ K)),
    (↑J : Submodule R₁ K).FG
h :
  ∀ (hI : ∀ J ≤ I, (↑J : Submodule R₁ K).FG) (hx : ¬x = 0)
    (h_gx : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) x : K) (0 : K))
    (h_spanx :
      Ne.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (0 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K))
    (J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (hJ :
      HMul.hMul (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) J
          (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) ≤
        I)
    (s : Finset K)
    (hs :
      span R₁ (↑s : Set K) =
        (↑(HMul.hMul (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) J
              (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)) :
          Submodule R₁ K)),
    span R₁ (↑(s * singleton (α := K) (((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : K)) : Set K) = (↑J : Submodule R₁ K)
⊢ IsNoetherian.{u_3, u_4} R₁
    ↥(↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
            (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) I) :
        Submodule R₁ K)

Tactic:
classical
  by_cases hx : x = 0
  · rw [hx, map_zero, inv_zero, spanSingleton_zero, zero_mul]
    exact isNoetherian_zero
  have h_gx : algebraMap R₁ K x ≠ 0 :=
    mt ((injective_iff_map_eq_zero (algebraMap R₁ K)).mp (IsFractionRing.injective _ _) x) hx
  have h_spanx : spanSingleton R₁⁰ (algebraMap R₁ K x) ≠ 0 := spanSingleton_ne_zero_iff.mpr h_gx
  rw [isNoetherian_iff] at hI ⊢
  intro J hJ
  rw [← div_spanSingleton, le_div_iff_mul_le h_spanx] at hJ
  obtain ⟨s, hs⟩ := hI _ hJ
  use s * {(algebraMap R₁ K x)⁻¹}
  rw [Finset.coe_mul, Finset.coe_singleton, ← span_mul_span, hs, ← coe_spanSingleton R₁⁰, ←
    coe_mul, mul_assoc, spanSingleton_mul_spanSingleton, mul_inv_cancel₀ h_gx, spanSingleton_one,
    mul_one]

Premises used: Finset.coe_singleton, Algebra.algebraMap, FractionalIdeal.spanSingleton_mul_spanSingleton, inv_zero, MulZeroClass.zero_mul, mul_assoc, Submodule.span_mul_span, nonZeroDivisors, Finset.coe_mul, map_zero, FractionalIdeal.isNoetherian_zero, FractionalIdeal.coe_mul, FractionalIdeal.spanSingleton_zero, FractionalIdeal.isNoetherian_iff, FractionalIdeal.div_spanSingleton, FractionalIdeal.coe_spanSingleton, FractionalIdeal.spanSingleton_one, mul_one, DFunLike.coe