awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Etale.Kaehler
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
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)
⊢ (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

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']

Premises used: map_zero, map_add, algebraMap_smul, Algebra.algebraMap_eq_smul_one, LinearMap.liftBaseChange_tmul, TensorProduct.smul_tmul', TensorProduct.tmul, Algebra.Extension.Cotangent.map_mk, rfl, Algebra.Extension.Hom.toAlgHom_apply
-- Module: Mathlib.RingTheory.Etale.Kaehler
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
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
⊢ 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

Tactic:
obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x

Premises used: Algebra.Extension.Cotangent.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Etale.Kaehler
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
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)
⊢ 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⟩ := H.surjective x

Premises used: Function.Bijective.surjective, rfl
-- Module: Mathlib.RingTheory.Etale.Kaehler
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)
⊢ 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)

Tactic:
simp only [map_zero]

Premises used: map_zero
-- Module: Mathlib.RingTheory.Etale.Kaehler
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 y : Q.Ring ⊗[P.Ring] ↥P.ker
h :
  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)
h_1 :
  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:
simp only [map_add, *]

Premises used: map_add
-- Module: Mathlib.RingTheory.Etale.Kaehler
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 : Q.Ring
b : ↥P.ker
tmul :
  (LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent)
      ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
        (HSMul.hSMul (β := Q.Cotangent) a
          ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent) ((f.mapKer halg : (a : ↥P.ker) → ↥Q.ker) b) : Q.Cotangent))) =
    HSMul.hSMul (β := Q.Cotangent) a
      ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent) ((f.mapKer halg : (a : ↥P.ker) → ↥Q.ker) b) : 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)
              (a ⊗ₜ[P.Ring] b)))) :
      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) (a ⊗ₜ[P.Ring] b)) :
      Q.Cotangent)

Tactic:
simp only [LinearMap.liftBaseChange_tmul, map_smul]

Premises used: LinearMap.liftBaseChange_tmul, map_smul
-- Module: Mathlib.RingTheory.Etale.Kaehler
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 : Q.Ring
b : ↥P.ker
⊢ (LinearMap.liftBaseChange T (Cotangent.map f) : (a : T ⊗[S] P.Cotangent) → Q.Cotangent)
      ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
        (HSMul.hSMul (β := Q.Cotangent) a
          ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent) ((f.mapKer halg : (a : ↥P.ker) → ↥Q.ker) b) : Q.Cotangent))) =
    HSMul.hSMul (β := Q.Cotangent) a
      ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent) ((f.mapKer halg : (a : ↥P.ker) → ↥Q.ker) b) : Q.Cotangent)

Tactic:
simp [Hom.mapKer, tensorCotangentInvFun_smul_mk]

Premises used: Algebra.Extension.Hom.mapKer, Algebra.Extension.tensorCotangentInvFun_smul_mk
-- Module: Mathlib.RingTheory.Etale.Kaehler
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
inst_7 : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
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)
refine :
  Function.Bijective (α := TensorProduct.{u_2, u_3, u} S T P.H1Cotangent) (β := Q.H1Cotangent)
    (⇑(LinearMap.liftBaseChange T (H1Cotangent.map f)) : (a : T ⊗[S] P.H1Cotangent) → Q.H1Cotangent)
⊢ TensorProduct.{u_2, u_3, u} S T P.H1Cotangent ≃ₗ[T] Q.H1Cotangent

Tactic:
refine .ofBijective ((H1Cotangent.map f).liftBaseChange T) ?_
-- Module: Mathlib.RingTheory.Etale.Kaehler
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
inst_7 : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
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)
left :
  Function.Injective (α := TensorProduct.{u_2, u_3, u} S T P.H1Cotangent) (β := Q.H1Cotangent)
    (⇑(LinearMap.liftBaseChange T (H1Cotangent.map f)) : (a : T ⊗[S] P.H1Cotangent) → Q.H1Cotangent)
right :
  Function.Surjective (α := TensorProduct.{u_2, u_3, u} S T P.H1Cotangent) (β := Q.H1Cotangent)
    (⇑(LinearMap.liftBaseChange T (H1Cotangent.map f)) : (a : T ⊗[S] P.H1Cotangent) → Q.H1Cotangent)
⊢ Function.Bijective (α := TensorProduct.{u_2, u_3, u} S T P.H1Cotangent) (β := Q.H1Cotangent)
    (⇑(LinearMap.liftBaseChange T (H1Cotangent.map f)) : (a : T ⊗[S] P.H1Cotangent) → Q.H1Cotangent)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Etale.Kaehler
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
inst_7 : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
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)
left :
  ∀ (a : TensorProduct.{u_2, u_3, u} S T P.H1Cotangent),
    Eq.{u + 1} (α := Q.H1Cotangent)
        ((LinearMap.liftBaseChange T (H1Cotangent.map f) : (a : T ⊗[S] P.H1Cotangent) → Q.H1Cotangent) a :
          Q.H1Cotangent)
        (0 : Q.H1Cotangent) →
      a = 0
⊢ Function.Injective (α := TensorProduct.{u_2, u_3, u} S T P.H1Cotangent) (β := Q.H1Cotangent)
    (⇑(LinearMap.liftBaseChange T (H1Cotangent.map f)) : (a : T ⊗[S] P.H1Cotangent) → Q.H1Cotangent)

Tactic:
rw [injective_iff_map_eq_zero]

Premises used: injective_iff_map_eq_zero
-- Module: Mathlib.RingTheory.Etale.Kaehler
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
inst_7 : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
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.H1Cotangent
hx :
  Eq.{u + 1} (α := Q.H1Cotangent)
    ((LinearMap.liftBaseChange T (H1Cotangent.map f) : (a : T ⊗[S] P.H1Cotangent) → Q.H1Cotangent) x : Q.H1Cotangent)
    (0 : Q.H1Cotangent)
left :
  Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((LinearMap.lTensor T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) x :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((LinearMap.lTensor T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) 0 :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
⊢ x = 0

Tactic:
apply Module.Flat.lTensor_preserves_injective_linearMap _ h1Cotangentι_injective

Premises used: Module.Flat.lTensor_preserves_injective_linearMap, Algebra.Extension.h1Cotangentι_injective
-- Module: Mathlib.RingTheory.Etale.Kaehler
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
inst_7 : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
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.H1Cotangent
hx :
  Eq.{u + 1} (α := Q.H1Cotangent)
    ((LinearMap.liftBaseChange T (H1Cotangent.map f) : (a : T ⊗[S] P.H1Cotangent) → Q.H1Cotangent) x : Q.H1Cotangent)
    (0 : Q.H1Cotangent)
left :
  Eq.{u + 1} (α := Q.Cotangent)
    ((tensorCotangent f halg H₂ : (a : T ⊗[S] P.Cotangent) → Q.Cotangent)
        ((LinearMap.lTensor T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) x) :
      Q.Cotangent)
    ((tensorCotangent f halg H₂ : (a : T ⊗[S] P.Cotangent) → Q.Cotangent)
        ((LinearMap.lTensor T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) 0) :
      Q.Cotangent)
⊢ Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((LinearMap.lTensor T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) x :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((LinearMap.lTensor T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) 0 :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)

Tactic:
apply (Extension.tensorCotangent f halg H₂).injective

Premises used: Algebra.Extension.tensorCotangent, LinearEquiv.injective
-- Module: Mathlib.RingTheory.Etale.Kaehler
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
inst_7 : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
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.H1Cotangent
hx :
  Eq.{u + 1} (α := Q.H1Cotangent)
    ((LinearMap.liftBaseChange T (H1Cotangent.map f) : (a : T ⊗[S] P.H1Cotangent) → Q.H1Cotangent) x : Q.H1Cotangent)
    (0 : Q.H1Cotangent)
left :
  Eq.{u + 1} (α := Q.Cotangent)
    ((tensorCotangent f halg H₂ : (a : T ⊗[S] P.Cotangent) → Q.Cotangent)
        ((LinearMap.lTensor T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) x) :
      Q.Cotangent)
    ((h1Cotangentι : (a : Q.H1Cotangent) → Q.Cotangent)
        ((LinearMap.liftBaseChange T (H1Cotangent.map f) : (a : T ⊗[S] P.H1Cotangent) → Q.H1Cotangent) x) :
      Q.Cotangent)
⊢ Eq.{u + 1} (α := Q.Cotangent)
    ((tensorCotangent f halg H₂ : (a : T ⊗[S] P.Cotangent) → Q.Cotangent)
        ((LinearMap.lTensor T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) x) :
      Q.Cotangent)
    (0 : Q.Cotangent)

Tactic:
rw [← h1Cotangentι.map_zero, ← hx]

Premises used: LinearMap.map_zero, Algebra.Extension.h1Cotangentι
-- Module: Mathlib.RingTheory.Etale.Kaehler
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
inst_7 : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
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.H1Cotangent
hx :
  Eq.{u + 1} (α := Q.H1Cotangent)
    ((LinearMap.liftBaseChange T (H1Cotangent.map f) : (a : T ⊗[S] P.H1Cotangent) → Q.H1Cotangent) x : Q.H1Cotangent)
    (0 : Q.H1Cotangent)
left :
  Eq.{u + 1} (α := Q.Cotangent)
    ((LinearMap.liftBaseChange T (Cotangent.map f) ∘ₗ LinearMap.baseChange T h1Cotangentι :
          (a : T ⊗[S] P.H1Cotangent) → Q.Cotangent)
        x :
      Q.Cotangent)
    ((h1Cotangentι ∘ₗ LinearMap.liftBaseChange T (H1Cotangent.map f) : (a : T ⊗[S] P.H1Cotangent) → Q.Cotangent) x :
      Q.Cotangent)
⊢ Eq.{u + 1} (α := Q.Cotangent)
    ((tensorCotangent f halg H₂ : (a : T ⊗[S] P.Cotangent) → Q.Cotangent)
        ((LinearMap.lTensor T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) x) :
      Q.Cotangent)
    ((h1Cotangentι : (a : Q.H1Cotangent) → Q.Cotangent)
        ((LinearMap.liftBaseChange T (H1Cotangent.map f) : (a : T ⊗[S] P.H1Cotangent) → Q.H1Cotangent) x) :
      Q.Cotangent)

Tactic:
change ((Cotangent.map f).liftBaseChange T ∘ₗ h1Cotangentι.baseChange T) x =
      (h1Cotangentι ∘ₗ _) x

Premises used: LinearMap.baseChange, LinearMap.comp, LinearMap.liftBaseChange, Algebra.Extension.h1Cotangentι, Algebra.Extension.Cotangent.map, DFunLike.coe
-- Module: Mathlib.RingTheory.Etale.Kaehler
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
inst_7 : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
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.H1Cotangent
hx :
  Eq.{u + 1} (α := Q.H1Cotangent)
    ((LinearMap.liftBaseChange T (H1Cotangent.map f) : (a : T ⊗[S] P.H1Cotangent) → Q.H1Cotangent) x : Q.H1Cotangent)
    (0 : Q.H1Cotangent)
left :
  Eq (α := TensorProduct.{u_2, u_3, u} S T P.H1Cotangent →ₗ[T] Q.Cotangent)
    (LinearMap.liftBaseChange T (Cotangent.map f) ∘ₗ LinearMap.baseChange T h1Cotangentι)
    (h1Cotangentι ∘ₗ LinearMap.liftBaseChange T (H1Cotangent.map f))
⊢ Eq.{u + 1} (α := Q.Cotangent)
    ((LinearMap.liftBaseChange T (Cotangent.map f) ∘ₗ LinearMap.baseChange T h1Cotangentι :
          (a : T ⊗[S] P.H1Cotangent) → Q.Cotangent)
        x :
      Q.Cotangent)
    ((h1Cotangentι ∘ₗ LinearMap.liftBaseChange T (H1Cotangent.map f) : (a : T ⊗[S] P.H1Cotangent) → Q.Cotangent) x :
      Q.Cotangent)

Tactic:
congr 1