-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
P' : Type u_2 := P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2
h₁ : Surjective.{u_2 + 1, u_3 + 1} (α := P') (β := S) (⇑(algebraMap P' S) : (a : P') → S)
h₂ : HPow.hPow (α := Ideal P') (β := ℕ) (RingHom.ker (F := P' →+* S) (algebraMap P' S)) 2 = ⊥
e₁ : Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) ≃ₗ[P]
  ↥(RingHom.ker (F := P' →+* S) (algebraMap P' S)) :=
  Ideal.cotangentEquivIdeal (RingHom.ker (F := P →+* S) (algebraMap P S)) ≪≫ₗ
    LinearEquiv.restrictScalars P
      (LinearEquiv.ofEq
        (Ideal.cotangentIdeal (RingHom.ker (F := P →+* S) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P S))))
        (RingHom.ker (F :=
          RingHom.{u_2, u_3}
            (P ⧸
              HPow.hPow (α := Ideal P) (β := ℕ)
                (RingHom.ker (F := P →+* S) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P S))) 2)
            S)
          (AlgHom.toRingHom (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P S))))
        ⋯)
e₂ : S ⊗[P'] Ω[P'⁄R] ≃ₗ[P] S ⊗[P] Ω[P⁄R] := LinearEquiv.restrictScalars P (tensorKaehlerQuotKerSqEquiv R P S)
H :
  kerCotangentToTensor R P S =
    (↑e₂ : S ⊗[P'] Ω[P'⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R]) ∘ₗ
      (↑P :
            {S M : Type u_2} →
              {M₂ : Type (max u_2 u_3)} →
                [inst : Semiring P] →
                  [inst_7 : Semiring S] →
                    [inst_8 : AddCommMonoid M] →
                      [inst_9 : AddCommMonoid M₂] →
                        [inst_10 : Module P M] →
                          [inst_11 : Module P M₂] →
                            [inst_12 : Module S M] →
                              [inst_13 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ P S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[P] M₂)
          (kerToTensor R P' S) ∘ₗ
        (↑e₁ : (RingHom.ker (algebraMap P S)).Cotangent →ₗ[P] ↥(RingHom.ker (algebraMap P' S)))
x_1 :
  { l : S ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) //
    l ∘ₗ kerCotangentToTensor R P S = LinearMap.id }
l : S ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S))
hl : l ∘ₗ kerCotangentToTensor R P S = LinearMap.id
y : S ⊗[P'] Ω[P'⁄R]
x : P
⊢ AddHom.toFun
      (↑((↑e₁ : (RingHom.ker (algebraMap P S)).Cotangent →ₗ[P] ↥(RingHom.ker (algebraMap P' S))) ∘ₗ
            l ∘ₗ (↑e₂ : S ⊗[P'] Ω[P'⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R])) :
        S ⊗[P'] Ω[P'⁄R] →ₙ+ ↥(RingHom.ker (algebraMap P' S)))
      (HSMul.hSMul (α := P')
        ((Ideal.Quotient.mk (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
              (a : P) → P ⧸ RingHom.ker (algebraMap P S) ^ 2)
            x :
          P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)
        y) =
    HSMul.hSMul (α := P')
      ((RingHom.id P' : (a : P') → P')
          ((Ideal.Quotient.mk (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
              (a : P) → P ⧸ RingHom.ker (algebraMap P S) ^ 2)
            x) :
        P')
      (AddHom.toFun
        (↑((↑e₁ : (RingHom.ker (algebraMap P S)).Cotangent →ₗ[P] ↥(RingHom.ker (algebraMap P' S))) ∘ₗ
              l ∘ₗ (↑e₂ : S ⊗[P'] Ω[P'⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R])) :
          S ⊗[P'] Ω[P'⁄R] →ₙ+ ↥(RingHom.ker (algebraMap P' S)))
        y)
have refine_1 : AddHom.toFun
    (↑((↑e₁ :
            (RingHom.ker (algebraMap P S)).Cotangent →ₗ[P]
              ↥(RingHom.ker (algebraMap (P ⧸ RingHom.ker (algebraMap P S) ^ 2) S))) ∘ₗ
          l ∘ₗ
            (↑e₂ :
              S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[P]
                S ⊗[P] Ω[P⁄R])) :
      S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₙ+
        ↥(RingHom.ker (algebraMap (P ⧸ RingHom.ker (algebraMap P S) ^ 2) S)))
    (x • y) =
  HSMul.hSMul (α := P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)
    ((RingHom.id (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
          (a : P ⧸ RingHom.ker (algebraMap P S) ^ 2) → P ⧸ RingHom.ker (algebraMap P S) ^ 2)
        (((algebraMap P (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
              P →+* P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
            (a : P) → P ⧸ RingHom.ker (algebraMap P S) ^ 2)
          x) :
      P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)
    (AddHom.toFun
      (↑((↑e₁ :
              (RingHom.ker (algebraMap P S)).Cotangent →ₗ[P]
                ↥(RingHom.ker (algebraMap (P ⧸ RingHom.ker (algebraMap P S) ^ 2) S))) ∘ₗ
            l ∘ₗ
              (↑e₂ :
                S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[P]
                  S ⊗[P] Ω[P⁄R])) :
        S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₙ+
          ↥(RingHom.ker (algebraMap (P ⧸ RingHom.ker (algebraMap P S) ^ 2) S)))
      y)
Tactic: simp only [P', ← Ideal.Quotient.algebraMap_eq, IsScalarTower.algebraMap_smul]