awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
mp :
  autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
mpr :
  FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam →
    autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam
mp₁ mp₂ :
  autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A →
      FormallySmooth R A →
        FormallyUnramified R A ∧
          autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
            autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
mp₃ :
  autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A → FormallySmooth R A → FormallyUnramified R A
mp₄ :
  autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A → FormallySmooth R A → autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam
⊢ autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam ↔
    FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
have mp₅ : autoParam (FinitePresentation R A) finitePresentation._autoParam →
  FormallyUnramified R A → FormallySmooth R A → autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
mp :
  autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
mpr :
  FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam →
    autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam
mp₁ mp₂ :
  autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A →
      FormallySmooth R A →
        FormallyUnramified R A ∧
          autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
            autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
mp₃ :
  autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A → FormallySmooth R A → FormallyUnramified R A
mp₄ :
  autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A → FormallySmooth R A → autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam
mp₅ :
  autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A →
      FormallySmooth R A → autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
⊢ autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam ↔
    FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
have mpr₁ : FormallyUnramified R A →
  autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam →
    autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam →
      autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
        autoParam (FinitePresentation R A) finitePresentation._autoParam
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
mp :
  autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
mpr :
  FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam →
    autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam
mp₁ mp₂ :
  autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A →
      FormallySmooth R A →
        FormallyUnramified R A ∧
          autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
            autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
mp₃ :
  autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A → FormallySmooth R A → FormallyUnramified R A
mp₄ :
  autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A → FormallySmooth R A → autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam
mp₅ :
  autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A →
      FormallySmooth R A → autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
mpr₁ mpr₂ :
  FormallyUnramified R A →
    autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam →
      autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam →
        autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
          autoParam (FinitePresentation R A) finitePresentation._autoParam
⊢ autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam ↔
    FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
have mpr₃ : FormallyUnramified R A →
  autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam →
    autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam → FormallyUnramified R A
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
mp :
  autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
mpr :
  FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam →
    autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam
mp₁ mp₂ :
  autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A →
      FormallySmooth R A →
        FormallyUnramified R A ∧
          autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
            autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
mp₃ :
  autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A → FormallySmooth R A → FormallyUnramified R A
mp₄ :
  autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A → FormallySmooth R A → autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam
mp₅ :
  autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A →
      FormallySmooth R A → autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
mpr₁ mpr₂ :
  FormallyUnramified R A →
    autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam →
      autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam →
        autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
          autoParam (FinitePresentation R A) finitePresentation._autoParam
mpr₃ :
  FormallyUnramified R A →
    autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam →
      autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam → FormallyUnramified R A
⊢ autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam ↔
    FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
have mpr₄ : FormallyUnramified R A →
  autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam →
    autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam → FormallySmooth R A
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
mp :
  autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
mpr :
  FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam →
    autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam
mp₁ mp₂ :
  autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A →
      FormallySmooth R A →
        FormallyUnramified R A ∧
          autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
            autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
mp₃ :
  autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A → FormallySmooth R A → FormallyUnramified R A
mp₄ :
  autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A → FormallySmooth R A → autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam
mp₅ :
  autoParam (FinitePresentation R A) finitePresentation._autoParam →
    FormallyUnramified R A →
      FormallySmooth R A → autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
mpr₁ mpr₂ :
  FormallyUnramified R A →
    autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam →
      autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam →
        autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
          autoParam (FinitePresentation R A) finitePresentation._autoParam
mpr₃ :
  FormallyUnramified R A →
    autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam →
      autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam → FormallyUnramified R A
mpr₄ :
  FormallyUnramified R A →
    autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam →
      autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam → FormallySmooth R A
⊢ autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam ↔
    FormallyUnramified R A ∧
      autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam ∧
        autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam
have mpr₅ : FormallyUnramified R A →
  autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam →
    autoParam (FinitePresentation R A) Smooth.finitePresentation._autoParam →
      autoParam (FinitePresentation R A) finitePresentation._autoParam
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ FormallyEtale (algebraMap R S) ↔ Algebra.FormallyEtale R S
have rw : Algebra.FormallyEtale R S ↔ Algebra.FormallyEtale R S
Tactic: rw [FormallyEtale, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
rw : Algebra.FormallyEtale R S ↔ Algebra.FormallyEtale R S
⊢ FormallyEtale (algebraMap R S) ↔ Algebra.FormallyEtale R S
have rw₁ : Algebra.FormallyEtale R S ↔ Algebra.FormallyEtale R S
Tactic: rw [FormallyEtale, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
T : Type u_3
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.FormallyEtale
hg : g.FormallyEtale
⊢ (g.comp f).FormallyEtale
have algebraizeInst : Algebra.FormallyEtale R S
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
T : Type u_3
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.FormallyEtale
hg : g.FormallyEtale
algebraizeInst : Algebra.FormallyEtale R S
⊢ (g.comp f).FormallyEtale
have algebraizeInst₁ : Algebra.FormallyEtale S T
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.FaithfullyFlat R T
inst_6 : FormallyUnramified T (T ⊗[R] S)
⊢ FormallyUnramified R S
have subsingleton_kaehlerDifferential : Subsingleton.{u_2 + 1} Ω[S⁄R]
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Descent (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.FaithfullyFlat R T
inst_6 : FormallyUnramified T (T ⊗[R] S)
x : Algebra S (T ⊗[R] S) := TensorProduct.rightAlgebra
⊢ Subsingleton.{u_2 + 1} Ω[S⁄R]
have this : Subsingleton (TensorProduct.{u_1, u_3, u_2} R T Ω[S⁄R])
Tactic: have : Subsingleton (T ⊗[R] Ω[S⁄R]) :=
    (KaehlerDifferential.tensorKaehlerEquivBase R T S (T ⊗[R] S)).subsingleton
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Descent (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.FaithfullyFlat R T
inst_6 : Smooth T (T ⊗[R] S)
⊢ Smooth R S
have this : FinitePresentation R S
Tactic: have : Algebra.FinitePresentation R S := .of_finitePresentation_tensorProduct_of_faithfullyFlat T
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.FaithfullyFlat R T
inst_6 : Smooth T (T ⊗[R] S)
this : FinitePresentation R S
⊢ Smooth R S
have refine : FormallySmooth R S
Tactic: refine ⟨?_, .of_finitePresentation_tensorProduct_of_faithfullyFlat T⟩
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.FaithfullyFlat R T
inst_6 : Smooth T (T ⊗[R] S)
this : FinitePresentation R S
⊢ FormallySmooth R S
have rw : Module.Projective S Ω[S⁄R] ∧ Subsingleton (H1Cotangent R S)
Tactic: rw [formallySmooth_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.FaithfullyFlat R T
inst_6 : Smooth T (T ⊗[R] S)
this : FinitePresentation R S
⊢ Module.Projective S Ω[S⁄R] ∧ Subsingleton (H1Cotangent R S)
have left : Module.Projective S Ω[S⁄R]
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.FaithfullyFlat R T
inst_6 : Smooth T (T ⊗[R] S)
this : FinitePresentation R S
left : Module.Projective S Ω[S⁄R]
⊢ Module.Projective S Ω[S⁄R] ∧ Subsingleton (H1Cotangent R S)
have right : Subsingleton (H1Cotangent R S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Descent (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.FaithfullyFlat R T
inst_6 : Smooth T (T ⊗[R] S)
this : FinitePresentation R S
x : Algebra T (S ⊗[R] T) := TensorProduct.rightAlgebra
e : S ⊗[R] T ≃ₐ[T] T ⊗[R] S := AlgEquiv.ofRingEquiv (f := AlgEquiv.toRingEquiv (TensorProduct.comm R S T)) ⋯
⊢ Module.Projective S Ω[S⁄R]
have this₁ : FormallySmooth T (S ⊗[R] T)
Tactic: have : FormallySmooth T (S ⊗[R] T) := .of_equiv e.symm
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Descent (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.FaithfullyFlat R T
inst_6 : Smooth T (T ⊗[R] S)
this_1 : FinitePresentation R S
x : Algebra T (S ⊗[R] T) := TensorProduct.rightAlgebra
e : S ⊗[R] T ≃ₐ[T] T ⊗[R] S := AlgEquiv.ofRingEquiv (f := AlgEquiv.toRingEquiv (TensorProduct.comm R S T)) ⋯
this : FormallySmooth T (S ⊗[R] T)
e' : S ⊗[R] T ⊗[S] Ω[S⁄R] ≃ₗ[S ⊗[R] T] Ω[S ⊗[R] T⁄T] := KaehlerDifferential.tensorKaehlerEquiv R T S (S ⊗[R] T)
⊢ Module.Projective S Ω[S⁄R]
have this₁ : Module.Flat (S ⊗[R] T) (S ⊗[R] T ⊗[S] Ω[S⁄R])
Tactic: have : Module.Flat (S ⊗[R] T) ((S ⊗[R] T) ⊗[S] Ω[S⁄R]) := .of_linearEquiv e'
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Descent (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.FaithfullyFlat R T
inst_6 : Smooth T (T ⊗[R] S)
this_1 : FinitePresentation R S
x : Algebra T (S ⊗[R] T) := TensorProduct.rightAlgebra
e : S ⊗[R] T ≃ₐ[T] T ⊗[R] S := AlgEquiv.ofRingEquiv (f := AlgEquiv.toRingEquiv (TensorProduct.comm R S T)) ⋯
this_2 : FormallySmooth T (S ⊗[R] T)
e' : S ⊗[R] T ⊗[S] Ω[S⁄R] ≃ₗ[S ⊗[R] T] Ω[S ⊗[R] T⁄T] := KaehlerDifferential.tensorKaehlerEquiv R T S (S ⊗[R] T)
this : Module.Flat (S ⊗[R] T) (S ⊗[R] T ⊗[S] Ω[S⁄R])
⊢ Module.Projective S Ω[S⁄R]
have this₁ : Module.Flat S Ω[S⁄R]
Tactic: have : Module.Flat S Ω[S⁄R] := Module.Flat.of_flat_tensorProduct _ _ (S ⊗[R] T)
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Descent (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.FaithfullyFlat R T
inst_6 : Smooth T (T ⊗[R] S)
this : FinitePresentation R S
⊢ Subsingleton (H1Cotangent R S)
have this₁ : Subsingleton (T ⊗[R] H1Cotangent R S)
Tactic: have : Subsingleton (T ⊗[R] H1Cotangent R S) := (tensorH1CotangentOfFlat R S T).subsingleton
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.FaithfullyFlat R T
inst_6 : Etale T (T ⊗[R] S)
⊢ Etale R S
have rw : FormallyUnramified R S ∧ Smooth R S
Tactic: rw [Etale.iff_formallyUnramified_and_smooth]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Descent (goal)
Goal:
⊢ CodescendsAlong.{u_1} (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ Smooth)
    fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ FaithfullyFlat
have refine : ∀ (R S T : Type u_1) (x : CommRing R) (x_1 : CommRing S) (x_2 : CommRing T) (x_3 : Algebra R S) (x_4 : Algebra R T)
  (h : FaithfullyFlat (algebraMap R S)) (h' : Smooth (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))), Smooth (algebraMap R T)
Tactic: refine .mk _ Smooth.respectsIso fun R S T _ _ _ _ _ h h' ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Descent (goal)
Goal:
R S T : Type u_1
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : FaithfullyFlat (algebraMap R S)
h' : Smooth (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
⊢ Smooth (algebraMap R T)
have rw : ∀ (h' : Algebra.Smooth S (S ⊗[R] T)), Algebra.Smooth R T
Tactic: rw [smooth_algebraMap] at h' ⊢
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Descent (hypothesis)
Goal:
R S T : Type u_1
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : FaithfullyFlat (algebraMap R S)
h' : Algebra.Smooth S (S ⊗[R] T)
⊢ Algebra.Smooth R T
have h₁ : Module.FaithfullyFlat R S
Tactic: rw [faithfullyFlat_algebraMap_iff] at h
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Descent (goal)
Goal:
⊢ CodescendsAlong.{u_1} (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ FormallyUnramified)
    fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ FaithfullyFlat
have refine : ∀ (R S T : Type u_1) (x : CommRing R) (x_1 : CommRing S) (x_2 : CommRing T) (x_3 : Algebra R S) (x_4 : Algebra R T)
  (h : FaithfullyFlat (algebraMap R S)) (h' : FormallyUnramified (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))),
  FormallyUnramified (algebraMap R T)
Tactic: refine .mk _ FormallyUnramified.respectsIso fun R S T _ _ _ _ _ h h' ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Descent (goal)
Goal:
R S T : Type u_1
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : FaithfullyFlat (algebraMap R S)
h' : FormallyUnramified (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
⊢ FormallyUnramified (algebraMap R T)
have rw : ∀ (h' : Algebra.FormallyUnramified S (S ⊗[R] T)), Algebra.FormallyUnramified R T
Tactic: rw [formallyUnramified_algebraMap] at h' ⊢
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Descent (hypothesis)
Goal:
R S T : Type u_1
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : FaithfullyFlat (algebraMap R S)
h' : Algebra.FormallyUnramified S (S ⊗[R] T)
⊢ Algebra.FormallyUnramified R T
have h₁ : Module.FaithfullyFlat R S
Tactic: rw [faithfullyFlat_algebraMap_iff] at h
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Descent (goal)
Goal:
⊢ CodescendsAlong.{u_1} (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ Etale)
    fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ FaithfullyFlat
have refine : ∀ (R S T : Type u_1) (x : CommRing R) (x_1 : CommRing S) (x_2 : CommRing T) (x_3 : Algebra R S) (x_4 : Algebra R T)
  (h : FaithfullyFlat (algebraMap R S)) (h' : Etale (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))), Etale (algebraMap R T)
Tactic: refine .mk _ Etale.respectsIso fun R S T _ _ _ _ _ h h' ↦ ?_