-- 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
g_1 : S →ₐ[R] P
f : P →ₐ[R] S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f) 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
a b : P
this :
  HSub.hSub (β := P) a ((g : (a : S) → P) ((f : (a : P) → S) a : S) : P) *
      HSub.hSub (β := P) b ((g : (a : S) → P) ((f : (a : P) → S) b : S) : P) =
    0
⊢ (↑(({
                toFun := fun (x : P) ↦
                  Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
                    (HSub.hSub (β := P) x ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P)) ⋯,
                map_add' := ⋯, map_smul' := ⋯ : P →ₗ[R] ↥(RingHom.ker f) } :
              (a : P) → ↥(RingHom.ker f))
            (a * b)) :
        P) -
      (↑(HSMul.hSMul (β := ↥(RingHom.ker f)) a
              (({
                      toFun := fun (x : P) ↦
                        Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
                          (HSub.hSub (β := P) x ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P)) ⋯,
                      map_add' := ⋯, map_smul' := ⋯ : P →ₗ[R] ↥(RingHom.ker f) } :
                    (a : P) → ↥(RingHom.ker f))
                  b :
                ↥(RingHom.ker f)) +
            HSMul.hSMul (β := ↥(RingHom.ker f)) b
              (({
                      toFun := fun (x : P) ↦
                        Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
                          (HSub.hSub (β := P) x ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P)) ⋯,
                      map_add' := ⋯, map_smul' := ⋯ : P →ₗ[R] ↥(RingHom.ker f) } :
                    (a : P) → ↥(RingHom.ker f))
                  a :
                ↥(RingHom.ker f))) :
        P) =
    0
have a₁ : (↑(({
              toFun := fun (x : P) ↦
                Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
                  (HSub.hSub (β := P) x ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P)) sorry,
              map_add' := sorry, map_smul' := sorry : P →ₗ[R] ↥(RingHom.ker f) } :
            (a : P) → ↥(RingHom.ker f))
          (a * b)) :
      P) -
    (↑(HSMul.hSMul (β := ↥(RingHom.ker f)) a
            (({
                    toFun := fun (x : P) ↦
                      Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
                        (HSub.hSub (β := P) x ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P)) sorry,
                    map_add' := sorry, map_smul' := sorry : P →ₗ[R] ↥(RingHom.ker f) } :
                  (a : P) → ↥(RingHom.ker f))
                b :
              ↥(RingHom.ker f)) +
          HSMul.hSMul (β := ↥(RingHom.ker f)) b
            (({
                    toFun := fun (x : P) ↦
                      Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker f) x)
                        (HSub.hSub (β := P) x ((g : (a : S) → P) ((f : (a : P) → S) x : S) : P)) sorry,
                    map_add' := sorry, map_smul' := sorry : P →ₗ[R] ↥(RingHom.ker f) } :
                  (a : P) → ↥(RingHom.ker f))
                a :
              ↥(RingHom.ker f))) :
      P) =
  -(HSub.hSub (β := P) a ((g : (a : S) → P) ((f : (a : P) → S) a : S) : P) *
      HSub.hSub (β := P) b ((g : (a : S) → P) ((f : (a : P) → S) b : S) : P))
Tactic: conv_rhs => rw [← neg_zero, ← this]