-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
σ : Type u_4
P : PreSubmersivePresentation R S ι σ
inst_3 : Finite σ
b : Module.Basis σ S P.toExtension.Cotangent
hb :
  ∀ (r : σ),
    Eq (α := P.toExtension.Cotangent) ((b : (a : σ) → P.toExtension.Cotangent) r : P.toExtension.Cotangent)
      ((Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) (P.relation r) ⋯) :
        P.toExtension.Cotangent)
h :
  Function.Bijective (α := P.toExtension.Cotangent) (β := σ →₀ S)
    (⇑(P.cotangentRestrict ⋯) : (a : P.toExtension.Cotangent) → σ →₀ S)
heq :
  Eq (α := (j i : σ) → S)
    (fun (j i : σ) ↦
      (aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j) : MvPolynomial ι R))
    (Function.comp (β := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
      (Function.comp (β := P.toExtension.Cotangent) (⇑(P.cotangentRestrict ⋯) : (a : P.toExtension.Cotangent) → σ →₀ S)
        (⇑b : (a : σ) → P.toExtension.Cotangent)))
hsp :
  Eq (α := Submodule S ((i : σ) → S))
    (Submodule.span S
      (Set.range (ι := σ)
        (Function.comp (β := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
          (Function.comp (β := P.toExtension.Cotangent)
            (⇑(P.cotangentRestrict ⋯) : (a : P.toExtension.Cotangent) → σ →₀ S)
            (⇑b : (a : σ) → P.toExtension.Cotangent)))))
    ⊤
hsp₁ :
  Eq (α := Submodule S ((i : σ) → S))
    (Submodule.span S
      (Set.image (α := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
        (Set.range (ι := σ)
          (Function.comp (β := P.toExtension.Cotangent)
            (⇑(P.cotangentRestrict ⋯) : (a : P.toExtension.Cotangent) → σ →₀ S)
            (⇑b : (a : σ) → P.toExtension.Cotangent)))))
    ⊤
hsp₂ :
  Eq (α := Submodule S ((i : σ) → S))
    (Submodule.span S
      (Set.image (α := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
        (Set.image (α := P.toExtension.Cotangent) (⇑(P.cotangentRestrict ⋯) : (a : P.toExtension.Cotangent) → σ →₀ S)
          (Set.range (ι := σ) (⇑b : (a : σ) → P.toExtension.Cotangent)))))
    ⊤
⊢ Eq (α := Submodule S ((i : σ) → S))
    (Submodule.span S
      (Set.range fun (j i : σ) ↦
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j) : MvPolynomial ι R)))
    ⊤
have hsp₃ : Eq (α := Submodule S ((i : σ) → S))
  (Submodule.map (↑(Finsupp.linearEquivFunOnFinite S S σ) : (σ →₀ S) →ₗ[S] (i : σ) → S)
    (Submodule.span S
      (Set.image (α := P.toExtension.Cotangent) (⇑(P.cotangentRestrict sorry) : (a : P.toExtension.Cotangent) → σ →₀ S)
        (Set.range (ι := σ) (⇑b : (a : σ) → P.toExtension.Cotangent)))))
  ⊤
Tactic: rw [heq, Set.range_comp, Set.range_comp, Submodule.span_image_linearEquiv, ← Submodule.map_span,
      b.span_eq, Submodule.map_top, LinearMap.range_eq_top_of_surjective _ h.surjective,
      Submodule.map_top, LinearEquiv.range]