-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_1
S : Type u_2
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
inst_6 : FinitePresentation R S
p : Ideal S
inst_7 : p.IsPrime
inst_8 : IsSmoothAt R p
h : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb :
  ∀ (i : κ),
    Eq (α := Ω[Localization.AtPrime p⁄R]) ((b : (a : κ) → Ω[Localization.AtPrime p⁄R]) i : Ω[Localization.AtPrime p⁄R])
      (Function.comp (β := Ω[S⁄R]) (⇑(map R R S (Localization.AtPrime p)) : (a : Ω[S⁄R]) → Ω[Localization.AtPrime p⁄R])
          (⇑(D R S) : (a : S) → Ω[S⁄R]) (a i) :
        Ω[Localization.AtPrime p⁄R])
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun (i : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (a i)
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p :=
  Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
eₚ : LinearMap (R := Localization.AtPrime p) (RingHom.id (Localization.AtPrime p)) (κ →₀ Localization.AtPrime p)
  Ω[Localization.AtPrime p⁄R] :=
  ((IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p) :
        ((κ →₀ S) →ₗ[S] Ω[S⁄R]) →ₗ[S]
          LinearMap (R := Localization.AtPrime p) (RingHom.id (Localization.AtPrime p)) (κ →₀ Localization.AtPrime p)
            Ω[Localization.AtPrime p⁄R]) :
      (a : (κ →₀ S) →ₗ[S] Ω[S⁄R]) →
        (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R])
    e
i : κ
trans :
  Eq (α := Ω[Localization.AtPrime p⁄R])
    ((eₚ ∘ₗ Finsupp.lsingle i : (a : Localization.AtPrime p) → Ω[Localization.AtPrime p⁄R]) 1 :
      Ω[Localization.AtPrime p⁄R])
    ((((IsLocalizedModule.map p.primeCompl l₁ l₂ :
                (a : (κ →₀ S) →ₗ[S] Ω[S⁄R]) → (κ →₀ Localization.AtPrime p) →ₗ[S] Ω[Localization.AtPrime p⁄R])
              e :
            (κ →₀ Localization.AtPrime p) →ₗ[S] Ω[Localization.AtPrime p⁄R]) :
          (a : κ →₀ Localization.AtPrime p) → Ω[Localization.AtPrime p⁄R])
        ((l₁ : (a : κ →₀ S) → κ →₀ Localization.AtPrime p) (Finsupp.single i 1)) :
      Ω[Localization.AtPrime p⁄R])
trans₁ :
  Eq (α := Ω[Localization.AtPrime p⁄R])
    ((((IsLocalizedModule.map p.primeCompl l₁ l₂ :
                (a : (κ →₀ S) →ₗ[S] Ω[S⁄R]) → (κ →₀ Localization.AtPrime p) →ₗ[S] Ω[Localization.AtPrime p⁄R])
              e :
            (κ →₀ Localization.AtPrime p) →ₗ[S] Ω[Localization.AtPrime p⁄R]) :
          (a : κ →₀ Localization.AtPrime p) → Ω[Localization.AtPrime p⁄R])
        ((l₁ : (a : κ →₀ S) → κ →₀ Localization.AtPrime p) (Finsupp.single i 1)) :
      Ω[Localization.AtPrime p⁄R])
    (((↑b.repr.symm : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R]) ∘ₗ
            Finsupp.lsingle i :
          (a : Localization.AtPrime p) → Ω[Localization.AtPrime p⁄R])
        1 :
      Ω[Localization.AtPrime p⁄R])
⊢ Eq (α := Ω[Localization.AtPrime p⁄R])
    ((eₚ ∘ₗ Finsupp.lsingle i : (a : Localization.AtPrime p) → Ω[Localization.AtPrime p⁄R]) 1)
    (((↑b.repr.symm : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R]) ∘ₗ
          Finsupp.lsingle i :
        (a : Localization.AtPrime p) → Ω[Localization.AtPrime p⁄R])
      1)

Tactic:
trans IsLocalizedModule.map p.primeCompl l₁ l₂ e <| l₁ <| Finsupp.single i 1

Premises used: IsLocalizedModule.map, Ideal.primeCompl, OfNat.ofNat, DFunLike.coe, Finsupp.single