-- Lean 4 proof step from Mathlib.RingTheory.Etale.Kaehler (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
P : Extension.{u, u_1, u_2} R S
Q : Extension.{u, u_1, u_3} R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H :
  Function.Bijective (α := Q.Ring ⊗[P.Ring] ↥P.ker) (β := ↥Q.ker)
    (⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker)
this_1 : Algebra.{u, u_3} P.Ring T :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap P.Ring S))
this_2 : IsScalarTower.{u, u_2, u_3} P.Ring S T
this : IsScalarTower.{u, u, u_3} P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : LinearMap (R := Q.Ring) (RingHom.id Q.Ring) (↥Q.ker) (TensorProduct.{u_2, u_3, u} S T P.Cotangent) :=
  LinearMap.liftBaseChange Q.Ring
      ((↑P.Ring :
            {S_1 : Type u_2} →
              {M : Type u} →
                {M₂ : Type (max u_3 u)} →
                  [inst_7 : Semiring P.Ring] →
                    [inst_8 : Semiring S_1] →
                      [inst_9 : AddCommMonoid M] →
                        [inst_10 : AddCommMonoid M₂] →
                          [inst_11 : Module P.Ring M] →
                            [inst_12 : Module P.Ring M₂] →
                              [inst_13 : Module S_1 M] →
                                [inst_14 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ P.Ring S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
          (S := S) ((TensorProduct.mk S T P.Cotangent : (a : T) → P.Cotangent →ₗ[S] T ⊗[S] P.Cotangent) 1) ∘ₗ
        Cotangent.mk) ∘ₗ
    (↑e.symm : ↥Q.ker →ₗ[Q.Ring] Q.Ring ⊗[P.Ring] ↥P.ker)
x y : Q.Ring ⊗[P.Ring] ↥P.ker
⊢ HSMul.hSMul (α := Q.Ring) (β := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
      (↑((e : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) x) : Q.Ring)
      ((LinearMap.liftBaseChange Q.Ring
              ((↑P.Ring :
                    {S_1 : Type u_2} →
                      {M : Type u} →
                        {M₂ : Type (max u_3 u)} →
                          [inst_7 : Semiring P.Ring] →
                            [inst_8 : Semiring S_1] →
                              [inst_9 : AddCommMonoid M] →
                                [inst_10 : AddCommMonoid M₂] →
                                  [inst_11 : Module P.Ring M] →
                                    [inst_12 : Module P.Ring M₂] →
                                      [inst_13 : Module S_1 M] →
                                        [inst_14 : Module S_1 M₂] →
                                          [LinearMap.CompatibleSMul M M₂ P.Ring S_1] →
                                            (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
                  (S := S) ((TensorProduct.mk S T P.Cotangent : (a : T) → P.Cotangent →ₗ[S] T ⊗[S] P.Cotangent) 1) ∘ₗ
                Cotangent.mk) :
            (a : Q.Ring ⊗[P.Ring] ↥P.ker) → T ⊗[S] P.Cotangent)
          y :
        TensorProduct.{u_2, u_3, u} S T P.Cotangent) =
    0
have zero : HSMul.hSMul (α := Q.Ring) (β := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (↑((e : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) 0) : Q.Ring)
    ((LinearMap.liftBaseChange Q.Ring
            ((↑P.Ring :
                  {S_1 : Type u_2} →
                    {M : Type u} →
                      {M₂ : Type (max u_3 u)} →
                        [inst_7 : Semiring P.Ring] →
                          [inst_8 : Semiring S_1] →
                            [inst_9 : AddCommMonoid M] →
                              [inst_10 : AddCommMonoid M₂] →
                                [inst_11 : Module P.Ring M] →
                                  [inst_12 : Module P.Ring M₂] →
                                    [inst_13 : Module S_1 M] →
                                      [inst_14 : Module S_1 M₂] →
                                        [LinearMap.CompatibleSMul M M₂ P.Ring S_1] →
                                          (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
                (S := S) ((TensorProduct.mk S T P.Cotangent : (a : T) → P.Cotangent →ₗ[S] T ⊗[S] P.Cotangent) 1) ∘ₗ
              Cotangent.mk) :
          (a : Q.Ring ⊗[P.Ring] ↥P.ker) → T ⊗[S] P.Cotangent)
        y :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent) =
  0
Tactic: induction x with
    | zero => simp only [map_zero, ZeroMemClass.coe_zero, zero_smul]
    | add x y _ _ =>
      simp only [map_add, Submodule.coe_add, add_smul, zero_add, *]
    | tmul a b =>
      induction y with
      | zero => simp only [map_zero, smul_zero]
      | add x y hx hy => simp only [LinearMap.map_add, smul_add, hx, hy, zero_add]
      | tmul c d =>
        simp only [LinearMap.liftBaseChange_tmul, LinearMap.coe_comp, SetLike.val_smul,
          LinearMap.coe_restrictScalars, Function.comp_apply, mk_apply, smul_eq_mul, e,
          LinearMap.liftBaseChange_tmul, LinearEquiv.ofBijective_apply]
        have h₂ : b.1 • Cotangent.mk d = 0 := by ext; simp [Cotangent.smul_eq_zero_of_mem _ b.2]
        rw [TensorProduct.smul_tmul', mul_smul, f.mapKer_apply_coe, ← halg,
          algebraMap_smul, ← TensorProduct.tmul_smul, h₂, tmul_zero, smul_zero]
Cleared hypotheses: x