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
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
⊢ 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)
have 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)
Tactic: simp only [LinearMap.liftBaseChange_tmul, map_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)
x : 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)
have 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)
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
-- 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
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)
⊢ TensorProduct.{u_2, u_3, u} S T P.H1Cotangent ≃ₗ[T] Q.H1Cotangent
have 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)
Tactic: refine .ofBijective ((H1Cotangent.map f).liftBaseChange T) ?_
-- 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
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)
⊢ 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)
have 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)
Tactic: constructor
-- 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
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)
⊢ 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)
have 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)
Tactic: constructor
-- 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
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)
⊢ 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)
have 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
Tactic: rw [injective_iff_map_eq_zero]
-- 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
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)
⊢ x = 0
have 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)
Tactic: apply Module.Flat.lTensor_preserves_injective_linearMap _ h1Cotangentι_injective
-- 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
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)
⊢ 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)
have 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)
Tactic: apply (Extension.tensorCotangent f halg H₂).injective
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [← h1Cotangentι.map_zero, ← hx]
-- 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
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)
⊢ 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)
have 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)
Tactic: change ((Cotangent.map f).liftBaseChange T ∘ₗ h1Cotangentι.baseChange T) x =
      (h1Cotangentι ∘ₗ _) 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
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)
⊢ 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)
have 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))
Tactic: congr 1
-- 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
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)
⊢ 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))
have left : ∀ (x : P.H1Cotangent),
  Eq.{u + 1} (α := Q.ker.Cotangent)
    (Cotangent.val
      ((((AlgebraTensorModule.curry
                  (LinearMap.liftBaseChange T (Cotangent.map f) ∘ₗ LinearMap.baseChange T h1Cotangentι) :
                LinearMap.{u_3, u_3, u_3, u} (RingHom.id T) T (P.H1Cotangent →ₗ[S] Q.Cotangent)) :
              (a : T) → P.H1Cotangent →ₗ[S] Q.Cotangent)
            1 :
          (a : P.H1Cotangent) → Q.Cotangent)
        x))
    (Cotangent.val
      ((((AlgebraTensorModule.curry (h1Cotangentι ∘ₗ LinearMap.liftBaseChange T (H1Cotangent.map f)) :
                LinearMap.{u_3, u_3, u_3, u} (RingHom.id T) T (P.H1Cotangent →ₗ[S] Q.Cotangent)) :
              (a : T) → P.H1Cotangent →ₗ[S] Q.Cotangent)
            1 :
          (a : P.H1Cotangent) → Q.Cotangent)
        x))
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Kaehler (hypothesis)
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 : Q.H1Cotangent
⊢ ∃ (a : TensorProduct.{u_2, u_3, u} S T P.H1Cotangent),
    (LinearMap.liftBaseChange T (H1Cotangent.map f) : (a : T ⊗[S] P.H1Cotangent) → Q.H1Cotangent) a = x
have this : Function.Exact (M := TensorProduct.{u_2, u_3, u} S T P.H1Cotangent) (N := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
  (P := T ⊗[S] P.CotangentSpace)
  (⇑(LinearMap.baseChange T h1Cotangentι) : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent)
  (⇑(LinearMap.baseChange T P.cotangentComplex) : (a : T ⊗[S] P.Cotangent) → T ⊗[S] P.CotangentSpace)
Tactic: have : Function.Exact (h1Cotangentι.baseChange T) (P.cotangentComplex.baseChange T) :=
      Module.Flat.lTensor_exact T (LinearMap.exact_subtype_ker_map _)
-- 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
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 : Q.H1Cotangent
this :
  Function.Exact (M := TensorProduct.{u_2, u_3, u} S T P.H1Cotangent) (N := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (P := T ⊗[S] P.CotangentSpace)
    (⇑(LinearMap.baseChange T h1Cotangentι) : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent)
    (⇑(LinearMap.baseChange T P.cotangentComplex) : (a : T ⊗[S] P.Cotangent) → T ⊗[S] P.CotangentSpace)
⊢ Eq (α := T ⊗[S] P.CotangentSpace)
    ((LinearMap.baseChange T P.cotangentComplex : (a : T ⊗[S] P.Cotangent) → T ⊗[S] P.CotangentSpace)
        (((tensorCotangent f halg H₂).symm : (a : Q.Cotangent) → T ⊗[S] P.Cotangent) (↑x : Q.Cotangent)) :
      T ⊗[S] P.CotangentSpace)
    (0 : T ⊗[S] P.CotangentSpace)
have a : Eq (α := Q.CotangentSpace)
  ((tensorCotangentSpaceOfFormallyEtale f H₁ : (a : T ⊗[S] P.CotangentSpace) → Q.CotangentSpace)
      ((LinearMap.baseChange T P.cotangentComplex : (a : T ⊗[S] P.Cotangent) → T ⊗[S] P.CotangentSpace)
        (((tensorCotangent f halg H₂).symm : (a : Q.Cotangent) → T ⊗[S] P.Cotangent) (↑x : Q.Cotangent))) :
    Q.CotangentSpace)
  ((tensorCotangentSpaceOfFormallyEtale f H₁ : (a : T ⊗[S] P.CotangentSpace) → Q.CotangentSpace) 0 : Q.CotangentSpace)
Tactic: apply (Extension.tensorCotangentSpaceOfFormallyEtale f H₁).injective
-- 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
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 : Q.H1Cotangent
this :
  Function.Exact (M := TensorProduct.{u_2, u_3, u} S T P.H1Cotangent) (N := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (P := T ⊗[S] P.CotangentSpace)
    (⇑(LinearMap.baseChange T h1Cotangentι) : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent)
    (⇑(LinearMap.baseChange T P.cotangentComplex) : (a : T ⊗[S] P.Cotangent) → T ⊗[S] P.CotangentSpace)
⊢ Eq (α := Q.CotangentSpace)
    ((tensorCotangentSpaceOfFormallyEtale f H₁ : (a : T ⊗[S] P.CotangentSpace) → Q.CotangentSpace)
        ((LinearMap.baseChange T P.cotangentComplex : (a : T ⊗[S] P.Cotangent) → T ⊗[S] P.CotangentSpace)
          (((tensorCotangent f halg H₂).symm : (a : Q.Cotangent) → T ⊗[S] P.Cotangent) (↑x : Q.Cotangent))) :
      Q.CotangentSpace)
    ((tensorCotangentSpaceOfFormallyEtale f H₁ : (a : T ⊗[S] P.CotangentSpace) → Q.CotangentSpace) 0 : Q.CotangentSpace)
have a : Eq (α := Q.CotangentSpace)
  ((tensorCotangentSpaceOfFormallyEtale f H₁ : (a : T ⊗[S] P.CotangentSpace) → Q.CotangentSpace)
      ((LinearMap.baseChange T P.cotangentComplex : (a : T ⊗[S] P.Cotangent) → T ⊗[S] P.CotangentSpace)
        (((tensorCotangent f halg H₂).symm : (a : Q.Cotangent) → T ⊗[S] P.Cotangent) (↑x : Q.Cotangent))) :
    Q.CotangentSpace)
  ((Q.cotangentComplex : (a : Q.Cotangent) → Q.CotangentSpace) (↑x : Q.Cotangent) : Q.CotangentSpace)
Tactic: rw [LinearEquiv.map_zero, ← x.2]