-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
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 : ∀ 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)
h :
  span R₁ ((↑s : Set K) * (↑(singleton (α := K) (((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : K)) : Set K)) =
    (↑J : Submodule R₁ K)
h₁ : span R₁ ((↑s : Set K) * singleton (α := K) (((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : K)) = (↑J : Submodule R₁ K)
h₂ :
  HMul.hMul (α := Submodule R₁ K) (span R₁ (↑s : Set K))
      (span R₁ (singleton (α := K) (((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : K))) =
    (↑J : Submodule R₁ K)
h₃ :
  (↑(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₁ (singleton (α := K) (((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : K)) =
    (↑J : Submodule R₁ K)
h₄ :
  HMul.hMul (β := Submodule R₁ 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)
      ((↑(spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) x)⁻¹) : Submodule R₁ K) : Submodule R₁ K) =
    (↑J : Submodule R₁ K)
h₅ :
  (↑(HMul.hMul (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ 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))
          (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)
h₆ :
  (↑(J *
          HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (β := 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)
            (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)
h₇ :
  (↑(J *
          spanSingleton R₁⁰
            (HMul.hMul (α := K) (β := K) ((algebraMap R₁ K : (a : R₁) → K) x : K)
              (((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : K))) :
      Submodule R₁ K) =
    (↑J : Submodule R₁ K)
⊢ span R₁ (↑(s * singleton (α := K) (((algebraMap R₁ K : (a : R₁) → K) x)⁻¹ : K)) : Set K) = (↑J : Submodule R₁ K)
have h₈ : (↑(J * spanSingleton R₁⁰ 1) : Submodule R₁ K) = (↑J : Submodule R₁ K)
Tactic: 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]