-- 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)
x : Q.Ring ⊗[P.Ring] ↥P.ker
zero :
  Eq (α := Q.Cotangent)
    ((LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent)
        ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
          ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
            ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) 0))) :
      Q.Cotangent)
    ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
        ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) 0) :
      Q.Cotangent)
⊢ Eq.{u + 1} (α := Q.Cotangent)
    ((LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent)
        ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
          ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
            ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) x))) :
      Q.Cotangent)
    ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
        ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) x) :
      Q.Cotangent)
have add : ∀ (x y : Q.Ring ⊗[P.Ring] ↥P.ker),
  Eq.{u + 1} (α := Q.Cotangent)
      ((LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent)
          ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
            ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
              ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) x))) :
        Q.Cotangent)
      ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
          ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) x) :
        Q.Cotangent) →
    Eq.{u + 1} (α := Q.Cotangent)
        ((LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent)
            ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
              ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
                ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) y))) :
          Q.Cotangent)
        ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
            ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) y) :
          Q.Cotangent) →
      Eq.{u + 1} (α := Q.Cotangent)
        ((LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent)
            ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
              ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
                ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) (x + y)))) :
          Q.Cotangent)
        ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
            ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) (x + y)) :
          Q.Cotangent)
Tactic: induction x with
      | zero => simp only [map_zero]
      | add x y _ _ => simp only [map_add, *]
      | tmul a b =>
        simp only [LinearMap.liftBaseChange_tmul, map_smul]
        simp [Hom.mapKer, tensorCotangentInvFun_smul_mk]
Cleared hypotheses: x