awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
H : Etale K A
mp :
  ∀ (I : Type u),
    Finite I →
      ∀ (Ai : I → Type u) (w : (i : I) → Field (Ai i)) (w_1 : (i : I) → Algebra.{u_1, u} K (Ai i))
        (e : A ≃ₐ[K] (i : I) → Ai i),
        (∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)) →
          ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (x : (i : I) → Field (Ai i)) (x_1 :
            (i : I) → Algebra.{u_1, u} K (Ai i)) (x_2 : A ≃ₐ[K] (i : I) → Ai i),
            ∀ (i : I), Module.Finite.{u_1, u} K (Ai i) ∧ Algebra.IsSeparable.{u_1, u} K (Ai i)
⊢ ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (x : (i : I) → Field (Ai i)) (x_1 :
    (i : I) → Algebra.{u_1, u} K (Ai i)) (x_2 : A ≃ₐ[K] (i : I) → Ai i),
    ∀ (i : I), Module.Finite.{u_1, u} K (Ai i) ∧ Algebra.IsSeparable.{u_1, u} K (Ai i)

Tactic:
obtain ⟨I, _, Ai, _, _, e, _⟩ := (FormallyEtale.iff_exists_algEquiv_prod K A).mp inferInstance

Premises used: inferInstance, Algebra.FormallyEtale.iff_exists_algEquiv_prod, Iff.mp
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
H : Etale K A
I : Type u
w : Finite I
Ai : I → Type u
w_1 : (i : I) → Field (Ai i)
w_2 : (i : I) → Algebra.{u_1, u} K (Ai i)
e : A ≃ₐ[K] (i : I) → Ai i
h : ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)
⊢ Module.Finite K A

Tactic:
have := FormallyUnramified.finite_of_free K A
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
H : Etale K A
I : Type u
w : Finite I
Ai : I → Type u
w_1 : (i : I) → Field (Ai i)
w_2 : (i : I) → Algebra.{u_1, u} K (Ai i)
e : A ≃ₐ[K] (i : I) → Ai i
h : ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)
this : Module.Finite K A
⊢ ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (x : (i : I) → Field (Ai i)) (x_1 :
    (i : I) → Algebra.{u_1, u} K (Ai i)) (x_2 : A ≃ₐ[K] (i : I) → Ai i),
    ∀ (i : I), Module.Finite.{u_1, u} K (Ai i) ∧ Algebra.IsSeparable.{u_1, u} K (Ai i)

Tactic:
⟨_, ‹_›, _, _, _, e, fun i ↦ ⟨.of_surjective ((LinearMap.proj i).comp e.toLinearMap)
      ((Function.surjective_eval i).comp e.surjective), inferInstance⟩⟩

Premises used: Module.Finite.of_surjective, Function.surjective_eval, inferInstance, AlgEquiv.toLinearMap, LinearMap.proj, LinearMap.comp, And.intro, Exists.intro, Function.Surjective.comp, AlgEquiv.surjective
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
H : Etale K A
I : Type u
w : Finite I
Ai : I → Type u
w_1 : (i : I) → Field (Ai i)
w_2 : (i : I) → Algebra.{u_1, u} K (Ai i)
e : A ≃ₐ[K] (i : I) → Ai i
h : ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)
this : Module.Finite K A
⊢ ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (x : (i : I) → Field (Ai i)) (x_1 :
    (i : I) → Algebra.{u_1, u} K (Ai i)) (x_2 : A ≃ₐ[K] (i : I) → Ai i),
    ∀ (i : I), Module.Finite.{u_1, u} K (Ai i) ∧ Algebra.IsSeparable.{u_1, u} K (Ai i)

Tactic:
exact ⟨_, ‹_›, _, _, _, e, fun i ↦ ⟨.of_surjective ((LinearMap.proj i).comp e.toLinearMap)
      ((Function.surjective_eval i).comp e.surjective), inferInstance⟩⟩
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
I : Type u
w : Finite I
Ai : I → Type u
w_1 : (i : I) → Field (Ai i)
w_2 : (i : I) → Algebra.{u_1, u} K (Ai i)
e : A ≃ₐ[K] (i : I) → Ai i
H : ∀ (i : I), Module.Finite.{u_1, u} K (Ai i) ∧ Algebra.IsSeparable.{u_1, u} K (Ai i)
⊢ ∀ (i : I), Module.Finite.{u_1, u} K (Ai i)

Tactic:
choose h₁ h₂ using H
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
I : Type u
w : Finite I
Ai : I → Type u
w_1 : (i : I) → Field (Ai i)
w_2 : (i : I) → Algebra.{u_1, u} K (Ai i)
e : A ≃ₐ[K] (i : I) → Ai i
H : ∀ (i : I), Module.Finite.{u_1, u} K (Ai i) ∧ Algebra.IsSeparable.{u_1, u} K (Ai i)
h₁ : ∀ (i : I), Module.Finite.{u_1, u} K (Ai i)
⊢ ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)

Tactic:
choose h₁ h₂ using H
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
I : Type u
w : Finite I
Ai : I → Type u
w_1 : (i : I) → Field (Ai i)
w_2 : (i : I) → Algebra.{u_1, u} K (Ai i)
e : A ≃ₐ[K] (i : I) → Ai i
h₁ : ∀ (i : I), Module.Finite.{u_1, u} K (Ai i)
h₂ : ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)
⊢ Module.Finite K A

Tactic:
have := Module.Finite.of_surjective e.symm.toLinearMap e.symm.surjective
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
I : Type u
w : Finite I
Ai : I → Type u
w_1 : (i : I) → Field (Ai i)
w_2 : (i : I) → Algebra.{u_1, u} K (Ai i)
e : A ≃ₐ[K] (i : I) → Ai i
h₁ : ∀ (i : I), Module.Finite.{u_1, u} K (Ai i)
h₂ : ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)
this : Module.Finite K A
⊢ Etale K A

Tactic:
⟨?_, FinitePresentation.of_finiteType.mp inferInstance⟩

Premises used: Algebra.Etale.mk, inferInstance, Algebra.FinitePresentation.of_finiteType, Iff.mp
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
I : Type u
w : Finite I
Ai : I → Type u
w_1 : (i : I) → Field (Ai i)
w_2 : (i : I) → Algebra.{u_1, u} K (Ai i)
e : A ≃ₐ[K] (i : I) → Ai i
h₁ : ∀ (i : I), Module.Finite.{u_1, u} K (Ai i)
h₂ : ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)
this : Module.Finite K A
mpr : FormallyEtale K A
⊢ Etale K A

Tactic:
refine ⟨?_, FinitePresentation.of_finiteType.mp inferInstance⟩
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
I : Type u
w : Finite I
Ai : I → Type u
w_1 : (i : I) → Field (Ai i)
w_2 : (i : I) → Algebra.{u_1, u} K (Ai i)
e : A ≃ₐ[K] (i : I) → Ai i
h₁ : ∀ (i : I), Module.Finite.{u_1, u} K (Ai i)
h₂ : ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)
this : Module.Finite K A
⊢ FormallyEtale K A

Tactic:
(FormallyEtale.iff_exists_algEquiv_prod K A).mpr ⟨_, inferInstance, _, _, _, e, h₂⟩

Premises used: Iff.mpr, inferInstance, Algebra.FormallyEtale.iff_exists_algEquiv_prod, Exists.intro
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
I : Type u
w : Finite I
Ai : I → Type u
w_1 : (i : I) → Field (Ai i)
w_2 : (i : I) → Algebra.{u_1, u} K (Ai i)
e : A ≃ₐ[K] (i : I) → Ai i
h₁ : ∀ (i : I), Module.Finite.{u_1, u} K (Ai i)
h₂ : ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)
this : Module.Finite K A
⊢ FormallyEtale K A

Tactic:
exact (FormallyEtale.iff_exists_algEquiv_prod K A).mpr ⟨_, inferInstance, _, _, _, e, h₂⟩

Premises used: Iff.mpr, inferInstance, Algebra.FormallyEtale.iff_exists_algEquiv_prod, Exists.intro
-- 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
inst_7 : Algebra.FormallyEtale S T
refine : Function.Injective (α := T ⊗[S] Ω[S⁄R]) (β := Ω[T⁄R]) (⇑(mapBaseChange R S T) : (a : T ⊗[S] Ω[S⁄R]) → Ω[T⁄R])
⊢ T ⊗[S] Ω[S⁄R] ≃ₗ[T] Ω[T⁄R]

Tactic:
refine LinearEquiv.ofBijective (mapBaseChange R S T)
    ⟨?_, fun x ↦ (KaehlerDifferential.exact_mapBaseChange_map R S T x).mp (Subsingleton.elim _ _)⟩

Premises used: KaehlerDifferential.exact_mapBaseChange_map, KaehlerDifferential.mapBaseChange, And.intro, Iff.mp, Subsingleton.elim, OfNat.ofNat, DFunLike.coe, LinearEquiv.ofBijective, KaehlerDifferential.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
inst_7 : Algebra.FormallyEtale S T
rw :
  ∀ (a : T ⊗[S] Ω[S⁄R]),
    Eq.{u_3 + 1} (α := Ω[T⁄R]) ((mapBaseChange R S T : (a : T ⊗[S] Ω[S⁄R]) → Ω[T⁄R]) a : Ω[T⁄R]) (0 : Ω[T⁄R]) → a = 0
⊢ Function.Injective (α := T ⊗[S] Ω[S⁄R]) (β := Ω[T⁄R]) (⇑(mapBaseChange R S T) : (a : T ⊗[S] Ω[S⁄R]) → Ω[T⁄R])

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
inst_7 : Algebra.FormallyEtale S T
x : T ⊗[S] Ω[S⁄R]
hx : Eq.{u_3 + 1} (α := Ω[T⁄R]) ((mapBaseChange R S T : (a : T ⊗[S] Ω[S⁄R]) → Ω[T⁄R]) x : Ω[T⁄R]) (0 : Ω[T⁄R])
obtain :
  ∀ (x : Algebra.H1Cotangent S T)
    (hx :
      Eq.{u_3 + 1} (α := Ω[T⁄R])
        ((mapBaseChange R S T : (a : T ⊗[S] Ω[S⁄R]) → Ω[T⁄R])
            ((Algebra.H1Cotangent.δ R S T : (a : Algebra.H1Cotangent S T) → T ⊗[S] Ω[S⁄R]) x) :
          Ω[T⁄R])
        (0 : Ω[T⁄R])),
    Eq (α := T ⊗[S] Ω[S⁄R])
      ((Algebra.H1Cotangent.δ R S T : (a : Algebra.H1Cotangent S T) → T ⊗[S] Ω[S⁄R]) x : T ⊗[S] Ω[S⁄R])
      (0 : T ⊗[S] Ω[S⁄R])
⊢ x = 0

Tactic:
obtain ⟨x, rfl⟩ := (Algebra.H1Cotangent.exact_δ_mapBaseChange R S T x).mp hx

Premises used: Iff.mp, rfl, Algebra.H1Cotangent.exact_δ_mapBaseChange
-- 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
inst_7 : Algebra.FormallyEtale S T
x : Algebra.H1Cotangent S T
hx :
  Eq.{u_3 + 1} (α := Ω[T⁄R])
    ((mapBaseChange R S T : (a : T ⊗[S] Ω[S⁄R]) → Ω[T⁄R])
        ((Algebra.H1Cotangent.δ R S T : (a : Algebra.H1Cotangent S T) → T ⊗[S] Ω[S⁄R]) x) :
      Ω[T⁄R])
    (0 : Ω[T⁄R])
rw : Eq (α := T ⊗[S] Ω[S⁄R]) ((Algebra.H1Cotangent.δ R S T : (a : Algebra.H1Cotangent S T) → T ⊗[S] Ω[S⁄R]) 0) 0
rw₁ rw₂ : Eq (α := T ⊗[S] Ω[S⁄R]) 0 0
⊢ Eq (α := T ⊗[S] Ω[S⁄R])
    ((Algebra.H1Cotangent.δ R S T : (a : Algebra.H1Cotangent S T) → T ⊗[S] Ω[S⁄R]) x : T ⊗[S] Ω[S⁄R])
    (0 : T ⊗[S] Ω[S⁄R])

Tactic:
rw [Subsingleton.elim x 0, map_zero]

Premises used: map_zero, Subsingleton.elim, OfNat.ofNat
-- 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
inst_7 : Algebra.FormallyEtale S T
s : S
rw :
  Eq (α := Ω[T⁄R]) ((D R T : (a : T) → Ω[T⁄R]) ((algebraMap S T : (a : S) → T) s) : Ω[T⁄R])
    ((tensorKaehlerEquivOfFormallyEtale R S T : (a : T ⊗[S] Ω[S⁄R]) → Ω[T⁄R]) (1 ⊗ₜ[S] (D R S : (a : S) → Ω[S⁄R]) s) :
      Ω[T⁄R])
rw₁ :
  Eq (α := Ω[T⁄R]) ((D R T : (a : T) → Ω[T⁄R]) ((algebraMap S T : (a : S) → T) s) : Ω[T⁄R])
    ((mapBaseChange R S T : (a : T ⊗[S] Ω[S⁄R]) → Ω[T⁄R]) (1 ⊗ₜ[S] (D R S : (a : S) → Ω[S⁄R]) s) : Ω[T⁄R])
rw₂ :
  (D R T : (a : T) → Ω[T⁄R]) ((algebraMap S T : (a : S) → T) s) =
    HSMul.hSMul (α := T) (β := Ω[T⁄R]) 1
      (((map R R S T : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R]) : (a : Ω[S⁄R]) → Ω[T⁄R])
          ((D R S : (a : S) → Ω[S⁄R]) s) :
        Ω[T⁄R])
rw₃ :
  Eq (α := Ω[T⁄R]) ((D R T : (a : T) → Ω[T⁄R]) ((algebraMap S T : (a : S) → T) s) : Ω[T⁄R])
    (((map R R S T : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R]) : (a : Ω[S⁄R]) → Ω[T⁄R])
        ((D R S : (a : S) → Ω[S⁄R]) s) :
      Ω[T⁄R])
rw₄ rw₅ :
  Eq (α := Ω[T⁄R]) ((D R T : (a : T) → Ω[T⁄R]) ((algebraMap S T : (a : S) → T) s) : Ω[T⁄R])
    ((D R T : (a : T) → Ω[T⁄R]) ((algebraMap S T : (a : S) → T) s) : Ω[T⁄R])
⊢ Eq (α := T ⊗[S] Ω[S⁄R])
    ((LinearEquiv.symm (tensorKaehlerEquivOfFormallyEtale R S T) : (a : Ω[T⁄R]) → T ⊗[S] Ω[S⁄R])
        ((D R T : (a : T) → Ω[T⁄R]) ((algebraMap S T : (a : S) → T) s)) :
      T ⊗[S] Ω[S⁄R])
    (1 ⊗ₜ[S] (D R S : (a : S) → Ω[S⁄R]) s : T ⊗[S] Ω[S⁄R])

Tactic:
rw [LinearEquiv.symm_apply_eq, tensorKaehlerEquivOfFormallyEtale_apply, mapBaseChange_tmul,
    one_smul, map_D]

Premises used: LinearEquiv.symm_apply_eq, KaehlerDifferential.mapBaseChange_tmul, KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_apply, one_smul, KaehlerDifferential.map_D
-- 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
inst_7 : Algebra.FormallyEtale S T
⊢ Function.Bijective (α := T ⊗[S] Ω[S⁄R]) (β := Ω[T⁄R])
    (⇑(tensorKaehlerEquivOfFormallyEtale R S T) : (a : T ⊗[S] Ω[S⁄R]) → Ω[T⁄R])

Tactic:
(tensorKaehlerEquivOfFormallyEtale R S T).bijective

Premises used: LinearEquiv.bijective, KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale
-- 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
inst_7 : Algebra.FormallyEtale S T
h :
  Eq (α := T ⊗[S] Ω[S⁄R] → Ω[T⁄R])
    (⇑(lift
          ((↑S :
              {S_1 M : Type u_3} →
                {M₂ : Type (max u_2 u_3)} →
                  [inst : Semiring S] →
                    [inst_8 : Semiring S_1] →
                      [inst_9 : AddCommMonoid M] →
                        [inst_10 : AddCommMonoid M₂] →
                          [inst_11 : Module S M] →
                            [inst_12 : Module S M₂] →
                              [inst_13 : Module S_1 M] →
                                [inst_14 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            (S := T)
            (((LinearMap.flip
                    (Algebra.linearMap T (Module.End T (LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R]))) :
                  LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R] →ₗ[T]
                    T →ₗ[T] LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R]) :
                (a : Ω[S⁄R] →ₗ[S] Ω[T⁄R]) → T →ₗ[T] Ω[S⁄R] →ₗ[S] Ω[T⁄R])
              (map R R S T)))) :
      (a : T ⊗[S] Ω[S⁄R]) → Ω[T⁄R])
    (⇑(tensorKaehlerEquivOfFormallyEtale R S T) : (a : T ⊗[S] Ω[S⁄R]) → Ω[T⁄R])
⊢ Function.Bijective (α := T ⊗[S] Ω[S⁄R]) (β := Ω[T⁄R])
    (⇑(lift
          ((↑S :
              {S_1 M : Type u_3} →
                {M₂ : Type (max u_2 u_3)} →
                  [inst : Semiring S] →
                    [inst_8 : Semiring S_1] →
                      [inst_9 : AddCommMonoid M] →
                        [inst_10 : AddCommMonoid M₂] →
                          [inst_11 : Module S M] →
                            [inst_12 : Module S M₂] →
                              [inst_13 : Module S_1 M] →
                                [inst_14 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            (S := T)
            (((LinearMap.flip
                    (Algebra.linearMap T (Module.End T (LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R]))) :
                  LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R] →ₗ[T]
                    T →ₗ[T] LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R]) :
                (a : Ω[S⁄R] →ₗ[S] Ω[T⁄R]) → T →ₗ[T] Ω[S⁄R] →ₗ[S] Ω[T⁄R])
              (map R R S T)))) :
      (a : T ⊗[S] Ω[S⁄R]) → Ω[T⁄R])

Tactic:
convert! (tensorKaehlerEquivOfFormallyEtale R S T).bijective using 1

Premises used: LinearEquiv.bijective, KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale
-- 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
M : Submonoid S
inst_7 : IsLocalization M T
⊢ IsLocalizedModule (M := Ω[S⁄R]) (M' := Ω[T⁄R]) M (map R R S T)

Tactic:
have := Algebra.FormallyEtale.of_isLocalization (Rₘ := T) M
  (isLocalizedModule_iff_isBaseChange M T _).mpr (isBaseChange_of_formallyEtale R S T)

Premises used: Iff.mpr, isLocalizedModule_iff_isBaseChange, Algebra.FormallyEtale.of_isLocalization, KaehlerDifferential.isBaseChange_of_formallyEtale, KaehlerDifferential.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
M : Submonoid S
inst_7 : IsLocalization M T
⊢ Eq (α := Submodule T Ω[T⁄R])
    (Submodule.span T
      (Set.image (α := Ω[S⁄R]) (⇑(map R R S T) : (a : Ω[S⁄R]) → Ω[T⁄R])
        (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))))
    ⊤

Tactic:
span_eq_top_of_isLocalizedModule T M (map R R S T) (v := Set.range <| D R S)
      (span_range_derivation R S)

Premises used: KaehlerDifferential.span_range_derivation, span_eq_top_of_isLocalizedModule, KaehlerDifferential.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
M : Submonoid S
inst_7 : IsLocalization M T
h :
  Eq.{u_3 + 1} (α := Set Ω[T⁄R])
    (Set.range (ι := S)
      (Function.comp (β := Ω[S⁄R]) (⇑(map R R S T) : (a : Ω[S⁄R]) → Ω[T⁄R]) (⇑(D R S) : (a : S) → Ω[S⁄R])))
    (Set.image (α := Ω[S⁄R]) (⇑(map R R S T) : (a : Ω[S⁄R]) → Ω[T⁄R])
      (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))
⊢ Eq (α := Submodule T Ω[T⁄R])
    (Submodule.span T
      (Set.range (ι := S)
        (Function.comp (β := Ω[S⁄R]) (⇑(map R R S T) : (a : Ω[S⁄R]) → Ω[T⁄R]) (⇑(D R S) : (a : S) → Ω[S⁄R]))))
    ⊤

Tactic:
convert!
    span_eq_top_of_isLocalizedModule T M (map R R S T) (v := Set.range <| D R S)
      (span_range_derivation R S)

Premises used: KaehlerDifferential.span_range_derivation, span_eq_top_of_isLocalizedModule, KaehlerDifferential.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
M : Submonoid S
inst_7 : IsLocalization M T
h :
  Eq.{u_3 + 1} (α := Set Ω[T⁄R])
    (Set.range (ι := S)
      (Function.comp (β := Ω[S⁄R]) (⇑(map R R S T) : (a : Ω[S⁄R]) → Ω[T⁄R]) (⇑(D R S) : (a : S) → Ω[S⁄R])))
    (Set.range (ι := S)
      (Function.comp (β := Ω[S⁄R]) (⇑(map R R S T) : (a : Ω[S⁄R]) → Ω[T⁄R]) (⇑(D R S) : (a : S) → Ω[S⁄R])))
h₁ h₂ :
  Eq.{u_3 + 1} (α := Set Ω[T⁄R])
    (Set.range fun (x : S) ↦
      ((map R R S T : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R]) : (a : Ω[S⁄R]) → Ω[T⁄R])
        ((D R S : (a : S) → Ω[S⁄R]) x))
    (Set.range fun (x : S) ↦
      ((map R R S T : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R]) : (a : Ω[S⁄R]) → Ω[T⁄R])
        ((D R S : (a : S) → Ω[S⁄R]) x))
⊢ Eq.{u_3 + 1} (α := Set Ω[T⁄R])
    (Set.range (ι := S)
      (Function.comp (β := Ω[S⁄R]) (⇑(map R R S T) : (a : Ω[S⁄R]) → Ω[T⁄R]) (⇑(D R S) : (a : S) → Ω[S⁄R])))
    (Set.image (α := Ω[S⁄R]) (⇑(map R R S T) : (a : Ω[S⁄R]) → Ω[T⁄R])
      (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R])))

Tactic:
rw [← Set.range_comp, Function.comp_def]

Premises used: Set.range_comp, Function.comp_def
-- 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
H : f.toRingHom.FormallyEtale
this_1 : Algebra P.Ring Q.Ring := f.toRingHom.toAlgebra
this_2 : IsScalarTower.{u_1, u, u} R P.Ring Q.Ring
this_3 : Algebra.{u, u_3} P.Ring T :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap P.Ring S))
this_4 : IsScalarTower.{u, u_2, u_3} P.Ring S T
this_5 : IsScalarTower.{u, u, u_3} P.Ring Q.Ring T
this : FormallyEtale.{u, u} P.Ring Q.Ring
refine : LinearMap (R := P.Ring) (RingHom.id P.Ring) Ω[P.Ring⁄R] (T ⊗[S] P.CotangentSpace)
⊢ LinearMap (R := Q.Ring) (RingHom.id Q.Ring) Ω[Q.Ring⁄R] (T ⊗[S] P.CotangentSpace)

Tactic:
refine LinearMap.liftBaseChange _ ?_ ∘ₗ
        (tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring).symm.toLinearMap

Premises used: LinearEquiv.symm, Algebra.Extension.Ring, LinearEquiv.toLinearMap, LinearMap.liftBaseChange, KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale
-- 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
H : f.toRingHom.FormallyEtale
this_1 : Algebra P.Ring Q.Ring := f.toRingHom.toAlgebra
this_2 : IsScalarTower.{u_1, u, u} R P.Ring Q.Ring
this_3 : Algebra.{u, u_3} P.Ring T :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap P.Ring S))
this_4 : IsScalarTower.{u, u_2, u_3} P.Ring S T
this_5 : IsScalarTower.{u, u, u_3} P.Ring Q.Ring T
this : FormallyEtale.{u, u} P.Ring Q.Ring
⊢ LinearMap (R := P.Ring) (RingHom.id P.Ring) Ω[P.Ring⁄R] (T ⊗[S] P.CotangentSpace)

Tactic:
exact (TensorProduct.mk _ _ _ 1).restrictScalars P.Ring ∘ₗ
        (TensorProduct.mk _ _ _ 1).restrictScalars P.Ring

Premises used: LinearMap.restrictScalars, Algebra.Extension.Ring, OfNat.ofNat, DFunLike.coe, TensorProduct.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
H : f.toRingHom.FormallyEtale
this_1 : Algebra P.Ring Q.Ring := f.toRingHom.toAlgebra
this_2 : IsScalarTower.{u_1, u, u} R P.Ring Q.Ring
this_3 : Algebra.{u, u_3} P.Ring T :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap P.Ring S))
this_4 : IsScalarTower.{u, u_2, u_3} P.Ring S T
this_5 : IsScalarTower.{u, u, u_3} P.Ring Q.Ring T
this : FormallyEtale.{u, u} P.Ring Q.Ring
x : T ⊗[S] P.CotangentSpace
a : P.Ring
⊢ Eq (α := Q.Ring ⊗[P.Ring] Ω[P.Ring⁄R])
    ((LinearEquiv.symm (tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring) :
          (a : Ω[Q.Ring⁄R]) → Q.Ring ⊗[P.Ring] Ω[P.Ring⁄R])
        ((D R Q.Ring : (a : Q.Ring) → Ω[Q.Ring⁄R]) ((f.toRingHom : (a : P.Ring) → Q.Ring) a)) :
      Q.Ring ⊗[P.Ring] Ω[P.Ring⁄R])
    (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) a : Q.Ring ⊗[P.Ring] Ω[P.Ring⁄R])

Tactic:
have : (tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring).symm
          ((D R Q.Ring) (f.toRingHom a)) = 1 ⊗ₜ D _ _ a :=
        tensorKaehlerEquivOfFormallyEtale_symm_D_algebraMap R P.Ring Q.Ring a