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
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 :
  ∀ (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))
⊢ 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:
ext x
-- 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_1 : 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_1 : Q.H1Cotangent)
    (0 : Q.H1Cotangent)
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:
simp
-- 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 : Q.H1Cotangent
⊢ 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 _)
-- 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 : 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)
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)
⊢ 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)

Tactic:
apply (Extension.tensorCotangentSpaceOfFormallyEtale f H₁).injective

Premises used: LinearEquiv.injective, Algebra.Extension.tensorCotangentSpaceOfFormallyEtale
-- 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 : 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)
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)
⊢ 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:
rw [LinearEquiv.map_zero, ← x.2]

Premises used: LinearEquiv.map_zero, Subtype.property
-- 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 : 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)
a :
  ∀ (x : P.Cotangent),
    Eq (α := Q.CotangentSpace)
      ((((AlgebraTensorModule.curry
                    (LinearMap.liftBaseChange T (CotangentSpace.map f) ∘ₗ LinearMap.baseChange T P.cotangentComplex) :
                  T →ₗ[T] P.Cotangent →ₗ[S] Q.CotangentSpace) :
                (a : T) → P.Cotangent →ₗ[S] Q.CotangentSpace)
              1 :
            (a : P.Cotangent) → Q.CotangentSpace)
          x :
        Q.CotangentSpace)
      ((((AlgebraTensorModule.curry (Q.cotangentComplex ∘ₗ LinearMap.liftBaseChange T (Cotangent.map f)) :
                  T →ₗ[T] P.Cotangent →ₗ[S] Q.CotangentSpace) :
                (a : T) → P.Cotangent →ₗ[S] Q.CotangentSpace)
              1 :
            (a : P.Cotangent) → Q.CotangentSpace)
          x :
        Q.CotangentSpace)
⊢ Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent →ₗ[T] Q.CotangentSpace)
    (LinearMap.liftBaseChange T (CotangentSpace.map f) ∘ₗ LinearMap.baseChange T P.cotangentComplex)
    (Q.cotangentComplex ∘ₗ LinearMap.liftBaseChange T (Cotangent.map f))

Tactic:
ext x
-- 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_1 : 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)
x : P.Cotangent
a :
  ∀ (x : ↥P.ker),
    Eq (α := Q.CotangentSpace)
      ((((AlgebraTensorModule.curry
                    (LinearMap.liftBaseChange T (CotangentSpace.map f) ∘ₗ LinearMap.baseChange T P.cotangentComplex) :
                  T →ₗ[T] P.Cotangent →ₗ[S] Q.CotangentSpace) :
                (a : T) → P.Cotangent →ₗ[S] Q.CotangentSpace)
              1 :
            (a : P.Cotangent) → Q.CotangentSpace)
          ((Cotangent.mk : (a : ↥P.ker) → P.Cotangent) x) :
        Q.CotangentSpace)
      ((((AlgebraTensorModule.curry (Q.cotangentComplex ∘ₗ LinearMap.liftBaseChange T (Cotangent.map f)) :
                  T →ₗ[T] P.Cotangent →ₗ[S] Q.CotangentSpace) :
                (a : T) → P.Cotangent →ₗ[S] Q.CotangentSpace)
              1 :
            (a : P.Cotangent) → Q.CotangentSpace)
          ((Cotangent.mk : (a : ↥P.ker) → P.Cotangent) x) :
        Q.CotangentSpace)
⊢ Eq (α := Q.CotangentSpace)
    ((((AlgebraTensorModule.curry
                  (LinearMap.liftBaseChange T (CotangentSpace.map f) ∘ₗ LinearMap.baseChange T P.cotangentComplex) :
                T →ₗ[T] P.Cotangent →ₗ[S] Q.CotangentSpace) :
              (a : T) → P.Cotangent →ₗ[S] Q.CotangentSpace)
            1 :
          (a : P.Cotangent) → Q.CotangentSpace)
        x :
      Q.CotangentSpace)
    ((((AlgebraTensorModule.curry (Q.cotangentComplex ∘ₗ LinearMap.liftBaseChange T (Cotangent.map f)) :
                T →ₗ[T] P.Cotangent →ₗ[S] Q.CotangentSpace) :
              (a : T) → P.Cotangent →ₗ[S] Q.CotangentSpace)
            1 :
          (a : P.Cotangent) → Q.CotangentSpace)
        x :
      Q.CotangentSpace)

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
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_1 : 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)
x : ↥P.ker
a :
  HSMul.hSMul (α := T) (β := Q.CotangentSpace) 1
      ((CotangentSpace.map f : (a : P.CotangentSpace) → Q.CotangentSpace)
          (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (↑x : P.Ring)) :
        Q.CotangentSpace) =
    (Q.cotangentComplex : (a : Q.Cotangent) → Q.CotangentSpace)
      (HSMul.hSMul.{u_3, u, u} (α := T) (β := Q.Cotangent) 1
        ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
            (Subtype.mk (p := fun (x : Q.Ring) ↦ x ∈ Q.ker) ((f.toRingHom : (a : P.Ring) → Q.Ring) (↑x : P.Ring)) ⋯) :
          Q.Cotangent))
⊢ Eq (α := Q.CotangentSpace)
    ((((AlgebraTensorModule.curry
                  (LinearMap.liftBaseChange T (CotangentSpace.map f) ∘ₗ LinearMap.baseChange T P.cotangentComplex) :
                T →ₗ[T] P.Cotangent →ₗ[S] Q.CotangentSpace) :
              (a : T) → P.Cotangent →ₗ[S] Q.CotangentSpace)
            1 :
          (a : P.Cotangent) → Q.CotangentSpace)
        ((Cotangent.mk : (a : ↥P.ker) → P.Cotangent) x) :
      Q.CotangentSpace)
    ((((AlgebraTensorModule.curry (Q.cotangentComplex ∘ₗ LinearMap.liftBaseChange T (Cotangent.map f)) :
                T →ₗ[T] P.Cotangent →ₗ[S] Q.CotangentSpace) :
              (a : T) → P.Cotangent →ₗ[S] Q.CotangentSpace)
            1 :
          (a : P.Cotangent) → Q.CotangentSpace)
        ((Cotangent.mk : (a : ↥P.ker) → P.Cotangent) x) :
      Q.CotangentSpace)

Tactic:
dsimp
-- 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_1 : 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)
x : ↥P.ker
⊢ HSMul.hSMul (α := T) (β := Q.CotangentSpace) 1
      ((CotangentSpace.map f : (a : P.CotangentSpace) → Q.CotangentSpace)
          (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (↑x : P.Ring)) :
        Q.CotangentSpace) =
    (Q.cotangentComplex : (a : Q.Cotangent) → Q.CotangentSpace)
      (HSMul.hSMul.{u_3, u, u} (α := T) (β := Q.Cotangent) 1
        ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
            (Subtype.mk (p := fun (x : Q.Ring) ↦ x ∈ Q.ker) ((f.toRingHom : (a : P.Ring) → Q.Ring) (↑x : P.Ring)) ⋯) :
          Q.Cotangent))

Tactic:
simp only [CotangentSpace.map_tmul,
          map_one, Hom.toAlgHom_apply, one_smul, cotangentComplex_mk]

Premises used: Algebra.Extension.CotangentSpace.map_tmul, one_smul, map_one, Algebra.Extension.Hom.toAlgHom_apply, Algebra.Extension.cotangentComplex_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)
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 (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent →ₗ[T] Q.CotangentSpace)
    (LinearMap.liftBaseChange T (CotangentSpace.map f) ∘ₗ LinearMap.baseChange T P.cotangentComplex)
    (Q.cotangentComplex ∘ₗ LinearMap.liftBaseChange T (Cotangent.map f))

Tactic:
have : (CotangentSpace.map f).liftBaseChange T ∘ₗ P.cotangentComplex.baseChange T =
          Q.cotangentComplex ∘ₗ (Cotangent.map f).liftBaseChange T := by
        ext x; obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x; dsimp
        simp only [CotangentSpace.map_tmul,
          map_one, Hom.toAlgHom_apply, one_smul, cotangentComplex_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)
x : Q.H1Cotangent
this_1 :
  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)
this :
  Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent →ₗ[T] Q.CotangentSpace)
    (LinearMap.liftBaseChange T (CotangentSpace.map f) ∘ₗ LinearMap.baseChange T P.cotangentComplex)
    (Q.cotangentComplex ∘ₗ LinearMap.liftBaseChange T (Cotangent.map f))
⊢ 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:
(DFunLike.congr_fun this _).trans (DFunLike.congr_arg Q.cotangentComplex
        ((tensorCotangent f halg H₂).apply_symm_apply x.1))

Premises used: DFunLike.congr_fun, Quotient.liftOn', AddCon.liftOn, Algebra.Extension.cotangentComplex, LinearEquiv.apply_symm_apply, Algebra.Extension.tensorCotangent, Subtype.val, Eq.trans, DFunLike.congr_arg
-- 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 : Q.H1Cotangent
this_1 :
  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)
this :
  Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent →ₗ[T] Q.CotangentSpace)
    (LinearMap.liftBaseChange T (CotangentSpace.map f) ∘ₗ LinearMap.baseChange T P.cotangentComplex)
    (Q.cotangentComplex ∘ₗ LinearMap.liftBaseChange T (Cotangent.map f))
⊢ 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:
exact (DFunLike.congr_fun this _).trans (DFunLike.congr_arg Q.cotangentComplex
        ((tensorCotangent f halg H₂).apply_symm_apply x.1))

Premises used: DFunLike.congr_fun, Algebra.Extension.cotangentComplex, LinearEquiv.apply_symm_apply, Algebra.Extension.tensorCotangent, Subtype.val, Eq.trans, DFunLike.congr_arg