-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : EssFiniteType R S
let let₁ let₂ : Module.Finite S Ω[S⁄R]
let₃ :
  let s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S);
  LE.le (α := Submodule S Ω[S⁄R]) ⊤ (Submodule.span S (↑s : Set Ω[S⁄R]))
let₄ :
  let s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S);
  Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]) ⊆ (↑(Submodule.span S (↑s : Set Ω[S⁄R])) : Set Ω[S⁄R])
let₅ :
  let s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S);
  ∀ (x : S),
    Membership.mem (α := Ω[S⁄R]) (↑(Submodule.span S (↑s : Set Ω[S⁄R])) : Set Ω[S⁄R])
      ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])
let₆ :
  let s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S);
  ∀ (x : S)
    (this :
      ∀ (x : S),
        Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x →
          Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
            ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])),
    Membership.mem (α := Ω[S⁄R]) (↑(Submodule.span S (↑s : Set Ω[S⁄R])) : Set Ω[S⁄R])
      ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])
let₇ :
  let s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S);
  ∀ (x : S)
    (this :
      ∀ (x : S),
        Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x →
          Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
            ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R]))
    (t : S) (ht : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) t)
    (ht' : IsUnit t)
    (hxt : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) (x * t)),
    Membership.mem (α := Ω[S⁄R]) (↑(Submodule.span S (↑s : Set Ω[S⁄R])) : Set Ω[S⁄R])
      ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R])
let₈ :
  let s : Finset Ω[S⁄R] := Finset.image (fun (s : S) ↦ (D R S : (a : S) → Ω[S⁄R]) s) (EssFiniteType.finset R S);
  ∀ (x : S)
    (this :
      ∀ (x : S),
        Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) x →
          Membership.mem (α := Ω[S⁄R]) (γ := Submodule S Ω[S⁄R]) (Submodule.span S (↑s : Set Ω[S⁄R]))
            ((D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R]))
    (t : S) (ht : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) t)
    (ht' : IsUnit t)
    (hxt : Membership.mem (γ := Subalgebra R S) (adjoin R (↑(EssFiniteType.finset R S) : Set S)) (x * t)),
    ht'.unit⁻¹ •
        HSub.hSub (α := Ω[S⁄R]) ((D R S : (a : S) → Ω[S⁄R]) (x * t) : Ω[S⁄R])
          (HSMul.hSMul (β := Ω[S⁄R]) x ((D R S : (a : S) → Ω[S⁄R]) t : Ω[S⁄R])) ∈
      (↑(Submodule.span S (↑s : Set Ω[S⁄R])) : Set Ω[S⁄R])
⊢ Module.Finite S Ω[S⁄R]

Tactic:
classical
  let s := (EssFiniteType.finset R S).image (fun s ↦ D R S s)
  refine ⟨⟨s, top_le_iff.mp ?_⟩⟩
  rw [← span_range_derivation, Submodule.span_le]
  rintro _ ⟨x, rfl⟩
  have : ∀ x ∈ adjoin R (EssFiniteType.finset R S : Set S),
      .D _ _ x ∈ Submodule.span S (s : Set Ω[S⁄R]) := by
    intro x hx
    refine adjoin_induction ?_ ?_ ?_ ?_ hx
    · exact fun x hx ↦ Submodule.subset_span (Finset.mem_image_of_mem _ hx)
    · simp
    · exact fun x y _ _ hx hy ↦ (D R S).map_add x y ▸ add_mem hx hy
    · intro x y _ _ hx hy
      simp only [Derivation.leibniz]
      exact add_mem (Submodule.smul_mem _ _ hy) (Submodule.smul_mem _ _ hx)
  obtain ⟨t, ht, ht', hxt⟩ := (essFiniteType_cond_iff R S (EssFiniteType.finset R S)).mp
    EssFiniteType.cond.choose_spec x
  rw [show D R S x =
    ht'.unit⁻¹ • (D R S (x * t) - x • D R S t) by simp [smul_smul, Units.smul_def]]
  exact Submodule.smul_mem _ _ (sub_mem (this _ hxt) (Submodule.smul_mem _ _ (this _ ht)))

Premises used: KaehlerDifferential.span_range_derivation, Submodule.span_le, rfl