-- 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)
this : (h :
    LE.le (α := Submodule R P)
      (Submodule.restrictScalars R (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2))
      (LinearMap.ker (M₂ := S ⊗[P] Ω[P⁄R])
        ((↑R :
              {S M : Type u_2} →
                {M₂ : Type (max u_3 u_2)} →
                  [inst : Semiring R] →
                    [inst_7 : Semiring S] →
                      [inst_8 : AddCommMonoid M] →
                        [inst_9 : AddCommMonoid M₂] →
                          [inst_10 : Module R M] →
                            [inst_11 : Module R M₂] →
                              [inst_12 : Module S M] →
                                [inst_13 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (S := P) ((mk P S Ω[P⁄R] : (a : S) → Ω[P⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R]) 1) ∘ₗ
          (↑(D R P) : P →ₗ[R] Ω[P⁄R])))) →
  HasQuotient.Quotient P (B := Submodule R P)
      (Submodule.restrictScalars R
        (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)) →ₗ[R]
    S ⊗[P] Ω[P⁄R] :=
  Submodule.liftQ (R := R) (M := P)
    (Submodule.restrictScalars R (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2))
    (R₂ := R) (M₂ := S ⊗[P] Ω[P⁄R]) (τ₁₂ := RingHom.id R)
    ((↑R :
          {S M : Type u_2} →
            {M₂ : Type (max u_3 u_2)} →
              [inst : Semiring R] →
                [inst_7 : Semiring S] →
                  [inst_8 : AddCommMonoid M] →
                    [inst_9 : AddCommMonoid M₂] →
                      [inst_10 : Module R M] →
                        [inst_11 : Module R M₂] →
                          [inst_12 : Module S M] →
                            [inst_13 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (S := P) ((mk P S Ω[P⁄R] : (a : S) → Ω[P⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R]) 1) ∘ₗ
      (↑(D R P) : P →ₗ[R] Ω[P⁄R]))
b : P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2
a : P
⊢ (this ⋯ : (a : P ⧸ RingHom.ker (algebraMap P S) ^ 2) → S ⊗[P] Ω[P⁄R]) (Submodule.Quotient.mk a * b) =
    HSMul.hSMul (α := P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) (β :=
        S ⊗[P] Ω[P⁄R]) (Submodule.Quotient.mk a)
        ((this ⋯ : (a : P ⧸ RingHom.ker (algebraMap P S) ^ 2) → S ⊗[P] Ω[P⁄R]) b : S ⊗[P] Ω[P⁄R]) +
      HSMul.hSMul (β := S ⊗[P] Ω[P⁄R]) b
        ((this ⋯ : (a : P ⧸ RingHom.ker (algebraMap P S) ^ 2) → S ⊗[P] Ω[P⁄R]) (Submodule.Quotient.mk a) :
          S ⊗[P] Ω[P⁄R])
have refine_3 : ∀ (b : P),
  (this sorry : (a : P ⧸ RingHom.ker (algebraMap P S) ^ 2) → S ⊗[P] Ω[P⁄R])
      (HMul.hMul (α := P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)
        (Submodule.Quotient.mk a) (Submodule.Quotient.mk b)) =
    HSMul.hSMul (α := P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) (β :=
        S ⊗[P] Ω[P⁄R]) (Submodule.Quotient.mk a)
        ((this sorry : (a : P ⧸ RingHom.ker (algebraMap P S) ^ 2) → S ⊗[P] Ω[P⁄R]) (Submodule.Quotient.mk b) :
          S ⊗[P] Ω[P⁄R]) +
      HSMul.hSMul (α := P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) (β :=
        S ⊗[P] Ω[P⁄R]) (Submodule.Quotient.mk b)
        ((this sorry : (a : P ⧸ RingHom.ker (algebraMap P S) ^ 2) → S ⊗[P] Ω[P⁄R]) (Submodule.Quotient.mk a) :
          S ⊗[P] Ω[P⁄R])
Tactic: obtain ⟨b, rfl⟩ := Submodule.Quotient.mk_surjective _ b
Cleared hypotheses: b