awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (goal)
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
mp :
  Etale 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)
⊢ Etale 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)
have mpr : (∃ (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)) →
  Etale K A
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (goal)
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) (_ : 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)
have 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)
Tactic: obtain ⟨I, _, Ai, _, _, e, _⟩ := (FormallyEtale.iff_exists_algEquiv_prod K A).mp inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (hypothesis)
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)
⊢ ∃ (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)
have this : Module.Finite K A
Tactic: have := FormallyUnramified.finite_of_free K A
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (hypothesis)
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)
⊢ Etale K A
have h₁ : ∀ (i : I), Module.Finite.{u_1, u} K (Ai i)
Tactic: choose h₁ h₂ using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (hypothesis)
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)
⊢ Etale K A
have h₂ : ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)
Tactic: choose h₁ h₂ using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (hypothesis)
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)
⊢ Etale K A
have this : Module.Finite K A
Tactic: have := Module.Finite.of_surjective e.symm.toLinearMap e.symm.surjective
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (goal)
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
have mpr : FormallyEtale K A
Tactic: refine ⟨?_, FinitePresentation.of_finiteType.mp inferInstance⟩
-- 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
inst_7 : Algebra.FormallyEtale S T
⊢ T ⊗[S] Ω[S⁄R] ≃ₗ[T] Ω[T⁄R]
have refine : Function.Injective (α := T ⊗[S] Ω[S⁄R]) (β := Ω[T⁄R]) (⇑(mapBaseChange R S T) : (a : T ⊗[S] Ω[S⁄R]) → Ω[T⁄R])
Tactic: refine LinearEquiv.ofBijective (mapBaseChange R S T)
    ⟨?_, fun x ↦ (KaehlerDifferential.exact_mapBaseChange_map R S T x).mp (Subsingleton.elim _ _)⟩
-- 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
inst_7 : Algebra.FormallyEtale S T
⊢ Function.Injective (α := T ⊗[S] Ω[S⁄R]) (β := Ω[T⁄R]) (⇑(mapBaseChange R S T) : (a : T ⊗[S] Ω[S⁄R]) → Ω[T⁄R])
have 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
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
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])
⊢ x = 0
have 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])
Tactic: obtain ⟨x, rfl⟩ := (Algebra.H1Cotangent.exact_δ_mapBaseChange R S T x).mp hx
Cleared hypotheses: x, 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
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])
⊢ 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])
have rw : Eq (α := T ⊗[S] Ω[S⁄R]) ((Algebra.H1Cotangent.δ R S T : (a : Algebra.H1Cotangent S T) → T ⊗[S] Ω[S⁄R]) 0) 0
Tactic: rw [Subsingleton.elim x 0, map_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
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
⊢ 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])
have rw₁ : Eq (α := T ⊗[S] Ω[S⁄R]) 0 0
Tactic: rw [Subsingleton.elim x 0, map_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
inst_7 : Algebra.FormallyEtale S T
s : S
⊢ 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])
have 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])
Tactic: rw [LinearEquiv.symm_apply_eq, tensorKaehlerEquivOfFormallyEtale_apply, mapBaseChange_tmul,
    one_smul, map_D]
-- 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
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])
⊢ 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])
have 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])
Tactic: rw [LinearEquiv.symm_apply_eq, tensorKaehlerEquivOfFormallyEtale_apply, mapBaseChange_tmul,
    one_smul, map_D]
-- 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
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])
⊢ 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])
have 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])
Tactic: rw [LinearEquiv.symm_apply_eq, tensorKaehlerEquivOfFormallyEtale_apply, mapBaseChange_tmul,
    one_smul, map_D]
-- 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
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])
⊢ 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])
have 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])
Tactic: rw [LinearEquiv.symm_apply_eq, tensorKaehlerEquivOfFormallyEtale_apply, mapBaseChange_tmul,
    one_smul, map_D]
-- 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
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])
⊢ 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])
have 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])
Tactic: rw [LinearEquiv.symm_apply_eq, tensorKaehlerEquivOfFormallyEtale_apply, mapBaseChange_tmul,
    one_smul, map_D]
-- 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
inst_7 : Algebra.FormallyEtale S T
⊢ 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])
have 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])
Tactic: convert! (tensorKaehlerEquivOfFormallyEtale R S T).bijective using 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
M : Submonoid S
inst_7 : IsLocalization M T
⊢ 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]))))
    ⊤
have 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])))
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)
-- 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
⊢ 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])))
have 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])))
Tactic: rw [← Set.range_comp, Function.comp_def]
-- 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
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])))
⊢ 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])))
have 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))
Tactic: rw [← Set.range_comp, Function.comp_def]
-- 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
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 := Q.Ring) (RingHom.id Q.Ring) Ω[Q.Ring⁄R] (T ⊗[S] P.CotangentSpace)
have refine : LinearMap (R := P.Ring) (RingHom.id P.Ring) Ω[P.Ring⁄R] (T ⊗[S] P.CotangentSpace)
Tactic: refine LinearMap.liftBaseChange _ ?_ ∘ₗ
        (tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring).symm.toLinearMap