awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
y : ↥P.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
trans :
  Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
        (HSMul.hSMul (β := Q.Cotangent) x
          ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
              (Subtype.mk (p := fun (x : Q.Ring) ↦ x ∈ Q.ker) ((f.toRingHom : (a : P.Ring) → Q.Ring) (↑y : P.Ring)) ⋯) :
            Q.Cotangent)) :
      TensorProduct.{u_2, u_3, u} S T P.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 ⊗ₜ[P.Ring] y))) :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
⊢ (tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
      (HSMul.hSMul (β := Q.Cotangent) x
        ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
            (Subtype.mk (p := fun (x : Q.Ring) ↦ x ∈ Q.ker) ((f.toRingHom : (a : P.Ring) → Q.Ring) (↑y : P.Ring)) ⋯) :
          Q.Cotangent)) =
    HSMul.hSMul (β := TensorProduct.{u_2, u_3, u} S T P.Cotangent) x
      (1 ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) y : TensorProduct.{u_2, u_3, u} S T P.Cotangent)
have trans₁ : (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 ⊗ₜ[P.Ring] y))) =
  HSMul.hSMul (β := TensorProduct.{u_2, u_3, u} S T P.Cotangent) x
    (1 ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) y : TensorProduct.{u_2, u_3, u} S T P.Cotangent)
Tactic: trans tensorCotangentInvFun f halg H (.mk ((f.mapKer halg).liftBaseChange Q.Ring (x ⊗ₜ y)))
-- 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
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
y : ↥P.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
⊢ Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
        (HSMul.hSMul (β := Q.Cotangent) x
          ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
              (Subtype.mk (p := fun (x : Q.Ring) ↦ x ∈ Q.ker) ((f.toRingHom : (a : P.Ring) → Q.Ring) (↑y : P.Ring)) ⋯) :
            Q.Cotangent)) :
      TensorProduct.{u_2, u_3, u} S T P.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 ⊗ₜ[P.Ring] y))) :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
have simp : Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
  ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
      (HSMul.hSMul (β := Q.Cotangent) x
        ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
            (Subtype.mk (p := fun (x : Q.Ring) ↦ x ∈ Q.ker) ((f.toRingHom : (a : P.Ring) → Q.Ring) (↑y : P.Ring)) sorry) :
          Q.Cotangent)) :
    TensorProduct.{u_2, u_3, u} S T P.Cotangent)
  ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
      (HSMul.hSMul (β := Q.Cotangent) x
        ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent) ((f.mapKer halg : (a : ↥P.ker) → ↥Q.ker) y) : Q.Cotangent)) :
    TensorProduct.{u_2, u_3, u} S T P.Cotangent)
Tactic: simp
-- 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
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
y : ↥P.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
⊢ (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 ⊗ₜ[P.Ring] y))) =
    HSMul.hSMul (β := TensorProduct.{u_2, u_3, u} S T P.Cotangent) x
      (1 ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) y : TensorProduct.{u_2, u_3, u} S T P.Cotangent)
have change : (LinearMap.liftBaseChange Q.Ring
        ((↑P.Ring :
              {S_1 : Type u_2} →
                {M : Type u} →
                  {M₂ : Type (max u_3 u)} →
                    [inst_6 : Semiring P.Ring] →
                      [inst_7 : Semiring S_1] →
                        [inst_8 : AddCommMonoid M] →
                          [inst_9 : AddCommMonoid M₂] →
                            [inst_10 : Module P.Ring M] →
                              [inst_11 : Module P.Ring M₂] →
                                [inst_12 : Module S_1 M] →
                                  [inst_13 : 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)
    ((e.symm : (a : ↥Q.ker) → Q.Ring ⊗[P.Ring] ↥P.ker)
      ((e : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) (x ⊗ₜ[P.Ring] y))) =
  HSMul.hSMul (β := TensorProduct.{u_2, u_3, u} S T P.Cotangent) x
    (1 ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) y : TensorProduct.{u_2, u_3, u} S T P.Cotangent)
Tactic: change ((TensorProduct.mk _ _ _ 1).restrictScalars _ ∘ₗ Cotangent.mk).liftBaseChange _
    (e.symm (e (x ⊗ₜ y))) = _
-- 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)
a : T
b : P.Cotangent
⊢ Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
        ((LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent) (a ⊗ₜ[S] b)) :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (a ⊗ₜ[S] b : TensorProduct.{u_2, u_3, u} S T P.Cotangent)
have tmul : ∀ (b : ↥P.ker),
  Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
        ((LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent)
          (a ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) b)) :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (a ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) b : TensorProduct.{u_2, u_3, u} S T P.Cotangent)
Tactic: obtain ⟨b, rfl⟩ := Cotangent.mk_surjective b
Cleared hypotheses: b
-- 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)
a : T
b : ↥P.ker
⊢ Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
        ((LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent)
          (a ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) b)) :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (a ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) b : TensorProduct.{u_2, u_3, u} S T P.Cotangent)
have tmul : ∀ (a : Q.Ring),
  Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
        ((LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent)
          ((algebraMap Q.Ring T : (a : Q.Ring) → T) a ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) b)) :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((algebraMap Q.Ring T : (a : Q.Ring) → T) a ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) b :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
Tactic: obtain ⟨a, rfl⟩ := Q.algebraMap_surjective a
Cleared hypotheses: a
-- 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)
b : ↥P.ker
a : Q.Ring
⊢ Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
        ((LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent)
          ((algebraMap Q.Ring T : (a : Q.Ring) → T) a ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) b)) :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((algebraMap Q.Ring T : (a : Q.Ring) → T) a ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) b :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
have tmul : Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
  ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
      (HSMul.hSMul (β := Q.Cotangent) a
        ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
            (Subtype.mk (p := fun (x : Q.Ring) ↦ x ∈ Q.ker) ((f.toRingHom : (a : P.Ring) → Q.Ring) (↑b : P.Ring)) sorry) :
          Q.Cotangent)) :
    TensorProduct.{u_2, u_3, u} S T P.Cotangent)
  ((algebraMap Q.Ring T : (a : Q.Ring) → T) a ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) b :
    TensorProduct.{u_2, u_3, u} S T P.Cotangent)
Tactic: simp only [LinearMap.liftBaseChange_tmul, Cotangent.map_mk, Hom.toAlgHom_apply,
          algebraMap_smul]
-- 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)
b : ↥P.ker
a : Q.Ring
⊢ Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
        (HSMul.hSMul (β := Q.Cotangent) a
          ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
              (Subtype.mk (p := fun (x : Q.Ring) ↦ x ∈ Q.ker) ((f.toRingHom : (a : P.Ring) → Q.Ring) (↑b : P.Ring)) ⋯) :
            Q.Cotangent)) :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((algebraMap Q.Ring T : (a : Q.Ring) → T) a ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) b :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
have tmul : HSMul.hSMul (β := TensorProduct.{u_2, u_3, u} S T P.Cotangent) a
    (1 ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) b : TensorProduct.{u_2, u_3, u} S T P.Cotangent) =
  (algebraMap Q.Ring T : (a : Q.Ring) → T) a ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) b
Tactic: refine (tensorCotangentInvFun_smul_mk f halg H a b).trans ?_
-- 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 : TensorProduct.{u_2, u_3, u} S T P.Cotangent
⊢ (tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
      ((LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent) x) =
    x
have zero : Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
  ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
    ((LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent) 0))
  0
Tactic: induction x with
      | zero => simp only [map_zero]
      | add x y _ _ => simp only [map_add, *]
      | tmul a b =>
        obtain ⟨b, rfl⟩ := Cotangent.mk_surjective b
        obtain ⟨a, rfl⟩ := Q.algebraMap_surjective a
        simp only [LinearMap.liftBaseChange_tmul, Cotangent.map_mk, Hom.toAlgHom_apply,
          algebraMap_smul]
        refine (tensorCotangentInvFun_smul_mk f halg H a b).trans ?_
        simp [algebraMap_eq_smul_one, TensorProduct.smul_tmul']
Cleared hypotheses: x
-- 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 : TensorProduct.{u_2, u_3, u} S T P.Cotangent
zero :
  Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
      ((LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent) 0))
    0
⊢ (tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
      ((LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent) x) =
    x
have add : ∀ (x y : TensorProduct.{u_2, u_3, u} S T P.Cotangent),
  (tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
        ((LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent) x) =
      x →
    (tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
          ((LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent) y) =
        y →
      (tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
          ((LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent) (x + y)) =
        x + y
Tactic: induction x with
      | zero => simp only [map_zero]
      | add x y _ _ => simp only [map_add, *]
      | tmul a b =>
        obtain ⟨b, rfl⟩ := Cotangent.mk_surjective b
        obtain ⟨a, rfl⟩ := Q.algebraMap_surjective a
        simp only [LinearMap.liftBaseChange_tmul, Cotangent.map_mk, Hom.toAlgHom_apply,
          algebraMap_smul]
        refine (tensorCotangentInvFun_smul_mk f halg H a b).trans ?_
        simp [algebraMap_eq_smul_one, TensorProduct.smul_tmul']
Cleared hypotheses: x
-- 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 : TensorProduct.{u_2, u_3, u} S T P.Cotangent
zero :
  Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
      ((LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent) 0))
    0
add :
  ∀ (x y : TensorProduct.{u_2, u_3, u} S T P.Cotangent),
    (tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
          ((LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent) x) =
        x →
      (tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
            ((LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent) y) =
          y →
        (tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
            ((LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent) (x + y)) =
          x + y
⊢ (tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
      ((LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent) x) =
    x
have tmul : ∀ (a : T) (b : P.Cotangent),
  Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
        ((LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent) (a ⊗ₜ[S] b)) :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (a ⊗ₜ[S] b : TensorProduct.{u_2, u_3, u} S T P.Cotangent)
Tactic: induction x with
      | zero => simp only [map_zero]
      | add x y _ _ => simp only [map_add, *]
      | tmul a b =>
        obtain ⟨b, rfl⟩ := Cotangent.mk_surjective b
        obtain ⟨a, rfl⟩ := Q.algebraMap_surjective a
        simp only [LinearMap.liftBaseChange_tmul, Cotangent.map_mk, Hom.toAlgHom_apply,
          algebraMap_smul]
        refine (tensorCotangentInvFun_smul_mk f halg H a b).trans ?_
        simp [algebraMap_eq_smul_one, TensorProduct.smul_tmul']
Cleared hypotheses: x
-- 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.Cotangent
⊢ AddHom.toFun (M := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
      (LinearMap.toAddHom (LinearMap.liftBaseChange T (Cotangent.map f)))
      ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent) x) =
    x
have obtain : ∀ (x : ↥Q.ker),
  AddHom.toFun (M := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
      (LinearMap.toAddHom (LinearMap.liftBaseChange T (Cotangent.map f)))
      ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
        ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent) x)) =
    (Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent) x
Tactic: obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x
Cleared hypotheses: x
-- 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.ker
⊢ AddHom.toFun (M := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
      (LinearMap.toAddHom (LinearMap.liftBaseChange T (Cotangent.map f)))
      ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
        ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent) x)) =
    (Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent) x
have obtain : ∀ (x : Q.Ring ⊗[P.Ring] ↥P.ker),
  AddHom.toFun (M := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
      (LinearMap.toAddHom (LinearMap.liftBaseChange T (Cotangent.map f)))
      ((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))) =
    (Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
      ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) x)
Tactic: obtain ⟨x, rfl⟩ := H.surjective x
Cleared hypotheses: x