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
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))
have 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)
Tactic: ext 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_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
⊢ 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)
have 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)
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
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
⊢ 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)
have 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)) sorry) :
        Q.Cotangent))
Tactic: dsimp
-- 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
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)
    ((Q.cotangentComplex : (a : Q.Cotangent) → Q.CotangentSpace) (↑x : Q.Cotangent) : Q.CotangentSpace)
have 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))
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]
-- 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)
⊢ ∃ (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 right : ∀ (a : TensorProduct.{u_2, u_3, u} S T P.H1Cotangent)
  (ha :
    Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
      ((LinearMap.baseChange T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) a :
        TensorProduct.{u_2, u_3, u} S T P.Cotangent)
      (((tensorCotangent f halg H₂).symm : (a : Q.Cotangent) → T ⊗[S] P.Cotangent) (↑x : Q.Cotangent) :
        TensorProduct.{u_2, u_3, u} S T P.Cotangent)),
  ∃ (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
Tactic: obtain ⟨a, ha⟩ := (this ((Extension.tensorCotangent f halg H₂).symm x.1)).mp (by
      apply (Extension.tensorCotangentSpaceOfFormallyEtale f H₁).injective
      rw [LinearEquiv.map_zero, ← x.2]
      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]
      exact (DFunLike.congr_fun this _).trans (DFunLike.congr_arg Q.cotangentComplex
        ((tensorCotangent f halg H₂).apply_symm_apply x.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 : 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 : TensorProduct.{u_2, u_3, u} S T P.H1Cotangent
ha :
  Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((LinearMap.baseChange T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) a :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (((tensorCotangent f halg H₂).symm : (a : Q.Cotangent) → T ⊗[S] P.Cotangent) (↑x : Q.Cotangent) :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
⊢ ∃ (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 right : Eq.{u + 1} (α := Q.Cotangent)
  ((↑((LinearMap.liftBaseChange T (H1Cotangent.map f) : (a : T ⊗[S] P.H1Cotangent) → Q.H1Cotangent) a) : Q.Cotangent) :
    Q.Cotangent)
  ((tensorCotangent f halg H₂ : (a : T ⊗[S] P.Cotangent) → Q.Cotangent)
      ((LinearMap.baseChange T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) a) :
    Q.Cotangent)
Tactic: refine ⟨a, Subtype.ext (.trans ?_ ((LinearEquiv.eq_symm_apply _).mp ha))⟩
-- 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)
a : TensorProduct.{u_2, u_3, u} S T P.H1Cotangent
ha :
  Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((LinearMap.baseChange T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) a :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (((tensorCotangent f halg H₂).symm : (a : Q.Cotangent) → T ⊗[S] P.Cotangent) (↑x : Q.Cotangent) :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
⊢ Eq.{u + 1} (α := Q.Cotangent)
    ((↑((LinearMap.liftBaseChange T (H1Cotangent.map f) : (a : T ⊗[S] P.H1Cotangent) → Q.H1Cotangent) a) :
        Q.Cotangent) :
      Q.Cotangent)
    ((tensorCotangent f halg H₂ : (a : T ⊗[S] P.Cotangent) → Q.Cotangent)
        ((LinearMap.baseChange T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) a) :
      Q.Cotangent)
have right : Eq.{u + 1} (α := Q.Cotangent)
  ((h1Cotangentι ∘ₗ LinearMap.liftBaseChange T (H1Cotangent.map f) : (a : T ⊗[S] P.H1Cotangent) → Q.Cotangent) a :
    Q.Cotangent)
  ((LinearMap.liftBaseChange T (Cotangent.map f) ∘ₗ LinearMap.baseChange T h1Cotangentι :
        (a : T ⊗[S] P.H1Cotangent) → Q.Cotangent)
      a :
    Q.Cotangent)
Tactic: change (h1Cotangentι ∘ₗ (H1Cotangent.map f).liftBaseChange T) _ =
      ((Cotangent.map f).liftBaseChange T ∘ₗ h1Cotangentι.baseChange 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)
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 : TensorProduct.{u_2, u_3, u} S T P.H1Cotangent
ha :
  Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((LinearMap.baseChange T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) a :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (((tensorCotangent f halg H₂).symm : (a : Q.Cotangent) → T ⊗[S] P.Cotangent) (↑x : Q.Cotangent) :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
⊢ Eq.{u + 1} (α := Q.Cotangent)
    ((h1Cotangentι ∘ₗ LinearMap.liftBaseChange T (H1Cotangent.map f) : (a : T ⊗[S] P.H1Cotangent) → Q.Cotangent) a :
      Q.Cotangent)
    ((LinearMap.liftBaseChange T (Cotangent.map f) ∘ₗ LinearMap.baseChange T h1Cotangentι :
          (a : T ⊗[S] P.H1Cotangent) → Q.Cotangent)
        a :
      Q.Cotangent)
have right : Eq (α := TensorProduct.{u_2, u_3, u} S T P.H1Cotangent →ₗ[T] Q.Cotangent)
  (h1Cotangentι ∘ₗ LinearMap.liftBaseChange T (H1Cotangent.map f))
  (LinearMap.liftBaseChange T (Cotangent.map f) ∘ₗ LinearMap.baseChange T h1Cotangentι)
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 : 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 : TensorProduct.{u_2, u_3, u} S T P.H1Cotangent
ha :
  Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((LinearMap.baseChange T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) a :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (((tensorCotangent f halg H₂).symm : (a : Q.Cotangent) → T ⊗[S] P.Cotangent) (↑x : Q.Cotangent) :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
⊢ Eq (α := TensorProduct.{u_2, u_3, u} S T P.H1Cotangent →ₗ[T] Q.Cotangent)
    (h1Cotangentι ∘ₗ LinearMap.liftBaseChange T (H1Cotangent.map f))
    (LinearMap.liftBaseChange T (Cotangent.map f) ∘ₗ LinearMap.baseChange T h1Cotangentι)
have right : ∀ (x : P.H1Cotangent),
  Eq.{u + 1} (α := Q.ker.Cotangent)
    (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))
    (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))
Tactic: ext
-- 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
M : Submonoid S
inst_7 : IsLocalization M T
P : Extension R S := Generators.toExtension (Generators.self R S)
M' : Submonoid P.Ring := Submonoid.comap (F := P.Ring →+* S) (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T :=
  IsLocalization.liftAlgHom (R := P.Ring) (M := M') (f :=
    AlgHom.comp (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R P.Ring S)) ⋯
x : T
⊢ ∃ (a : Localization M'), (fQ : (a : Localization M') → T) a = x
have obtain : ∀ (x s : S) (hs : s ∈ M),
  ∃ (a : Localization M'),
    (fQ : (a : Localization M') → T) a = IsLocalization.mk' T x (Subtype.mk (p := fun (x : S) ↦ x ∈ M) s hs)
Tactic: obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq M 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
M : Submonoid S
inst_7 : IsLocalization M T
P : Extension R S := Generators.toExtension (Generators.self R S)
M' : Submonoid P.Ring := Submonoid.comap (F := P.Ring →+* S) (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T :=
  IsLocalization.liftAlgHom (R := P.Ring) (M := M') (f :=
    AlgHom.comp (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R P.Ring S)) ⋯
x s : S
hs : s ∈ M
⊢ ∃ (a : Localization M'),
    (fQ : (a : Localization M') → T) a = IsLocalization.mk' T x (Subtype.mk (p := fun (x : S) ↦ x ∈ M) s hs)
have obtain : ∀ (x : P.Ring),
  ∃ (a : Localization M'),
    (fQ : (a : Localization M') → T) a =
      IsLocalization.mk' T ((algebraMap P.Ring S : (a : P.Ring) → S) x) (Subtype.mk (p := fun (x : S) ↦ x ∈ M) s hs)
Tactic: obtain ⟨x, rfl⟩ := P.algebraMap_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
M : Submonoid S
inst_7 : IsLocalization M T
P : Extension R S := Generators.toExtension (Generators.self R S)
M' : Submonoid P.Ring := Submonoid.comap (F := P.Ring →+* S) (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T :=
  IsLocalization.liftAlgHom (R := P.Ring) (M := M') (f :=
    AlgHom.comp (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R P.Ring S)) ⋯
s : S
hs : s ∈ M
x : P.Ring
⊢ ∃ (a : Localization M'),
    (fQ : (a : Localization M') → T) a =
      IsLocalization.mk' T ((algebraMap P.Ring S : (a : P.Ring) → S) x) (Subtype.mk (p := fun (x : S) ↦ x ∈ M) s hs)
have obtain : ∀ (s : P.Ring) (hs : Membership.mem (α := S) M ((algebraMap P.Ring S : (a : P.Ring) → S) s : S)),
  ∃ (a : Localization M'),
    (fQ : (a : Localization M') → T) a =
      IsLocalization.mk'.{u_2, u_3} (R := S) (M := M) T ((algebraMap P.Ring S : (a : P.Ring) → S) x : S)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ M) ((algebraMap P.Ring S : (a : P.Ring) → S) s) hs : ↥M)
Tactic: obtain ⟨s, rfl⟩ := P.algebraMap_surjective s
Cleared hypotheses: s, hs