awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Etale.Basic
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
mpr₅ :
  FormallyUnramified R A →
    autoParam (FormallySmooth R A) Smooth.formallySmooth._autoParam →
      autoParam (FinitePresentation R A) Smooth.finitePresentation._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

Tactic:
tauto
-- Module: Mathlib.RingTheory.Etale.Basic
Goal:
R_1 : Type u
A : Type v
B : Type u_1
inst : CommRing R_1
inst_1 : CommRing A
inst_2 : Algebra R_1 A
inst_3 : CommRing B
inst_4 : Algebra R_1 B
R S : Type u
inst_5 : CommRing R
inst_6 : CommRing S
algInst : Algebra (R × S) S := RingHom.toAlgebra (RingHom.snd R S)
⊢ Etale (R × S) S

Tactic:
Algebra.Etale.of_isLocalizationAway (0, 1)

Premises used: Algebra.Etale.of_isLocalizationAway, Prod.mk, OfNat.ofNat
-- Module: Mathlib.RingTheory.Etale.Basic
Goal:
R_1 : Type u
A : Type v
B : Type u_1
inst : CommRing R_1
inst_1 : CommRing A
inst_2 : Algebra R_1 A
inst_3 : CommRing B
inst_4 : Algebra R_1 B
R S : Type u
inst_5 : CommRing R
inst_6 : CommRing S
algInst : Algebra (R × S) S := RingHom.toAlgebra (RingHom.snd R S)
⊢ Etale (R × S) S

Tactic:
exact Algebra.Etale.of_isLocalizationAway (0, 1)

Premises used: Algebra.Etale.of_isLocalizationAway, Prod.mk, OfNat.ofNat
-- Module: Mathlib.RingTheory.Etale.Basic
Goal:
R : Type u
A : Type v
B : Type u_1
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
S : Type u_2
inst_5 : CommRing S
algInst : Algebra (R × S) R := RingHom.toAlgebra (RingHom.fst R S)
⊢ Etale (R × S) R

Tactic:
Algebra.Etale.of_isLocalizationAway (1, 0)

Premises used: Algebra.Etale.of_isLocalizationAway, Prod.mk, OfNat.ofNat
-- Module: Mathlib.RingTheory.Etale.Basic
Goal:
R : Type u
A : Type v
B : Type u_1
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
S : Type u_2
inst_5 : CommRing S
algInst : Algebra (R × S) R := RingHom.toAlgebra (RingHom.fst R S)
⊢ Etale (R × S) R

Tactic:
exact Algebra.Etale.of_isLocalizationAway (1, 0)

Premises used: Algebra.Etale.of_isLocalizationAway, Prod.mk, OfNat.ofNat
-- Module: Mathlib.RingTheory.Etale.Basic
Goal:
R : Type u
A : Type v
B : Type u_1
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
S : Type u_2
inst_5 : CommRing S
algInst : Algebra (R × S) S := RingHom.toAlgebra (RingHom.snd R S)
⊢ Etale (R × S) S

Tactic:
Algebra.Etale.of_isLocalizationAway (0, 1)

Premises used: Algebra.Etale.of_isLocalizationAway, Prod.mk, OfNat.ofNat
-- Module: Mathlib.RingTheory.Etale.Basic
Goal:
R : Type u
A : Type v
B : Type u_1
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
S : Type u_2
inst_5 : CommRing S
algInst : Algebra (R × S) S := RingHom.toAlgebra (RingHom.snd R S)
⊢ Etale (R × S) S

Tactic:
exact Algebra.Etale.of_isLocalizationAway (0, 1)

Premises used: Algebra.Etale.of_isLocalizationAway, Prod.mk, OfNat.ofNat
-- Module: Mathlib.RingTheory.Etale.Basic
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
rw₁ rw₂ : Algebra.FormallyEtale R S ↔ Algebra.FormallyEtale R S
⊢ FormallyEtale (algebraMap R S) ↔ Algebra.FormallyEtale R S

Tactic:
rw [FormallyEtale, toAlgebra_algebraMap]

Premises used: RingHom.FormallyEtale, toAlgebra_algebraMap
-- Module: Mathlib.RingTheory.Etale.Basic
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
⊢ Algebra.FormallyEtale R S

Tactic:
algebraize [f, g, g.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.Etale.Basic
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
⊢ Algebra.FormallyEtale S T

Tactic:
algebraize [f, g, g.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.Etale.Basic
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
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra S T := g.toAlgebra
algInst_2 : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Algebra.FormallyEtale R S
algebraizeInst_1 : Algebra.FormallyEtale S T
⊢ (g.comp f).FormallyEtale

Tactic:
Algebra.FormallyEtale.comp R S T

Premises used: Algebra.FormallyEtale.comp, RingHom.FormallyEtale
-- Module: Mathlib.RingTheory.Etale.Basic
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
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra S T := g.toAlgebra
algInst_2 : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Algebra.FormallyEtale R S
algebraizeInst_1 : Algebra.FormallyEtale S T
⊢ (g.comp f).FormallyEtale

Tactic:
exact Algebra.FormallyEtale.comp R S T

Premises used: Algebra.FormallyEtale.comp
-- Module: Mathlib.RingTheory.Etale.Descent
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)
subsingleton_kaehlerDifferential : Subsingleton.{u_2 + 1} Ω[S⁄R]
⊢ FormallyUnramified R S

Tactic:
constructor
-- Module: Mathlib.RingTheory.Etale.Descent
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 (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
-- Module: Mathlib.RingTheory.Etale.Descent
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
this : Subsingleton (TensorProduct.{u_1, u_3, u_2} R T Ω[S⁄R])
⊢ Subsingleton.{u_2 + 1} Ω[S⁄R]

Tactic:
Module.FaithfullyFlat.lTensor_reflects_triviality R T _

Premises used: Module.FaithfullyFlat.lTensor_reflects_triviality
-- Module: Mathlib.RingTheory.Etale.Descent
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
this : Subsingleton (TensorProduct.{u_1, u_3, u_2} R T Ω[S⁄R])
⊢ Subsingleton.{u_2 + 1} Ω[S⁄R]

Tactic:
exact Module.FaithfullyFlat.lTensor_reflects_triviality R T _

Premises used: Module.FaithfullyFlat.lTensor_reflects_triviality
-- Module: Mathlib.RingTheory.Etale.Descent
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)
⊢ FinitePresentation R S

Tactic:
have : Algebra.FinitePresentation R S := .of_finitePresentation_tensorProduct_of_faithfullyFlat T
-- Module: Mathlib.RingTheory.Etale.Descent
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

Tactic:
⟨?_, .of_finitePresentation_tensorProduct_of_faithfullyFlat T⟩

Premises used: Algebra.Smooth.mk, Algebra.FinitePresentation.of_finitePresentation_tensorProduct_of_faithfullyFlat
-- Module: Mathlib.RingTheory.Etale.Descent
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
refine : FormallySmooth R S
⊢ Smooth R S

Tactic:
refine ⟨?_, .of_finitePresentation_tensorProduct_of_faithfullyFlat T⟩
-- Module: Mathlib.RingTheory.Etale.Descent
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
rw : Module.Projective S Ω[S⁄R] ∧ Subsingleton (H1Cotangent R S)
⊢ FormallySmooth R S

Tactic:
rw [formallySmooth_iff]

Premises used: Algebra.formallySmooth_iff
-- Module: Mathlib.RingTheory.Etale.Descent
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]
right : Subsingleton (H1Cotangent R S)
⊢ Module.Projective S Ω[S⁄R] ∧ Subsingleton (H1Cotangent R S)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Etale.Descent
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
⊢ ∀ (x_1 : T),
    Eq (α := T ⊗[R] S)
      ((AlgEquiv.toRingEquiv (TensorProduct.comm R S T) : (a : S ⊗[R] T) → T ⊗[R] S)
          ((algebraMap T (S ⊗[R] T) : (a : T) → S ⊗[R] T) x_1) :
        T ⊗[R] S)
      ((algebraMap T (T ⊗[R] S) : (a : T) → T ⊗[R] S) x_1 : T ⊗[R] S)

Tactic:
simp [RingHom.algebraMap_toAlgebra]

Premises used: RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.Etale.Descent
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)) ⋯
⊢ FormallySmooth T (S ⊗[R] T)

Tactic:
have : FormallySmooth T (S ⊗[R] T) := .of_equiv e.symm
-- Module: Mathlib.RingTheory.Etale.Descent
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.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'
-- Module: Mathlib.RingTheory.Etale.Descent
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.Flat S Ω[S⁄R]

Tactic:
have : Module.Flat S Ω[S⁄R] := Module.Flat.of_flat_tensorProduct _ _ (S ⊗[R] T)
-- Module: Mathlib.RingTheory.Etale.Descent
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_3 : Module.Flat (S ⊗[R] T) (S ⊗[R] T ⊗[S] Ω[S⁄R])
this : Module.Flat S Ω[S⁄R]
⊢ Module.Projective S Ω[S⁄R]

Tactic:
Module.Flat.projective_of_finitePresentation

Premises used: Module.Flat.projective_of_finitePresentation
-- Module: Mathlib.RingTheory.Etale.Descent
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_3 : Module.Flat (S ⊗[R] T) (S ⊗[R] T ⊗[S] Ω[S⁄R])
this : Module.Flat S Ω[S⁄R]
⊢ Module.Projective S Ω[S⁄R]

Tactic:
exact Module.Flat.projective_of_finitePresentation

Premises used: Module.Flat.projective_of_finitePresentation
-- Module: Mathlib.RingTheory.Etale.Descent
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 (T ⊗[R] H1Cotangent R S)

Tactic:
have : Subsingleton (T ⊗[R] H1Cotangent R S) := (tensorH1CotangentOfFlat R S T).subsingleton
-- Module: Mathlib.RingTheory.Etale.Descent
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
this : Subsingleton (T ⊗[R] H1Cotangent R S)
⊢ Subsingleton (H1Cotangent R S)

Tactic:
Module.FaithfullyFlat.lTensor_reflects_triviality R T (H1Cotangent R S)

Premises used: Module.FaithfullyFlat.lTensor_reflects_triviality, Algebra.H1Cotangent
-- Module: Mathlib.RingTheory.Etale.Descent
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
this : Subsingleton (T ⊗[R] H1Cotangent R S)
⊢ Subsingleton (H1Cotangent R S)

Tactic:
exact Module.FaithfullyFlat.lTensor_reflects_triviality R T (H1Cotangent R S)

Premises used: Module.FaithfullyFlat.lTensor_reflects_triviality, Algebra.H1Cotangent
-- Module: Mathlib.RingTheory.Etale.Descent
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 : Unramified T (T ⊗[R] S)
⊢ Unramified R S

Tactic:
⟨.of_formallyUnramified_tensorProduct_of_faithfullyFlat T,
    .of_finiteType_tensorProduct_of_faithfullyFlat T⟩

Premises used: Algebra.FiniteType.of_finiteType_tensorProduct_of_faithfullyFlat, Algebra.Unramified.mk, Algebra.FormallyUnramified.of_formallyUnramified_tensorProduct_of_faithfullyFlat
-- Module: Mathlib.RingTheory.Etale.Descent
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)
rw : FormallyUnramified R S ∧ Smooth R S
⊢ Etale R S

Tactic:
rw [Etale.iff_formallyUnramified_and_smooth]

Premises used: Algebra.Etale.iff_formallyUnramified_and_smooth
-- Module: Mathlib.RingTheory.Etale.Descent
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)
⊢ FormallyUnramified R S ∧ Smooth R S

Tactic:
⟨.of_formallyUnramified_tensorProduct_of_faithfullyFlat T,
    .of_smooth_tensorProduct_of_faithfullyFlat T⟩

Premises used: Algebra.FormallyUnramified.of_formallyUnramified_tensorProduct_of_faithfullyFlat, And.intro, Algebra.Smooth.of_smooth_tensorProduct_of_faithfullyFlat
-- Module: Mathlib.RingTheory.Etale.Descent
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)
⊢ FormallyUnramified R S ∧ Smooth R S

Tactic:
exact ⟨.of_formallyUnramified_tensorProduct_of_faithfullyFlat T,
    .of_smooth_tensorProduct_of_faithfullyFlat T⟩
-- Module: Mathlib.RingTheory.Etale.Descent
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

Tactic:
.mk _ Smooth.respectsIso fun R S T _ _ _ _ _ h h' ↦ ?_

Premises used: RingHom.CodescendsAlong.mk, RingHom.Smooth.respectsIso
-- Module: Mathlib.RingTheory.Etale.Descent
Goal:
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)
⊢ 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

Tactic:
refine .mk _ Smooth.respectsIso fun R S T _ _ _ _ _ h h' ↦ ?_
-- Module: Mathlib.RingTheory.Etale.Descent
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))
rw : ∀ (h' : Algebra.Smooth S (S ⊗[R] T)), Algebra.Smooth R T
⊢ Smooth (algebraMap R T)

Tactic:
rw [smooth_algebraMap] at h' ⊢

Premises used: RingHom.smooth_algebraMap
-- Module: Mathlib.RingTheory.Etale.Descent
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)
⊢ Module.FaithfullyFlat R S

Tactic:
rw [faithfullyFlat_algebraMap_iff] at h

Premises used: RingHom.faithfullyFlat_algebraMap_iff
-- Module: Mathlib.RingTheory.Etale.Descent
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)
h₁ : Module.FaithfullyFlat R S
⊢ Algebra.Smooth S (S ⊗[R] T)

Tactic:
rw [faithfullyFlat_algebraMap_iff] at h

Premises used: RingHom.faithfullyFlat_algebraMap_iff
-- Module: Mathlib.RingTheory.Etale.Descent
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 : Module.FaithfullyFlat R S
h' : Algebra.Smooth S (S ⊗[R] T)
⊢ Algebra.Smooth R T

Tactic:
.of_smooth_tensorProduct_of_faithfullyFlat S

Premises used: Algebra.Smooth.of_smooth_tensorProduct_of_faithfullyFlat
-- Module: Mathlib.RingTheory.Etale.Descent
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 : Module.FaithfullyFlat R S
h' : Algebra.Smooth S (S ⊗[R] T)
⊢ Algebra.Smooth R T

Tactic:
exact .of_smooth_tensorProduct_of_faithfullyFlat S
-- Module: Mathlib.RingTheory.Etale.Descent
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

Tactic:
.mk _ FormallyUnramified.respectsIso fun R S T _ _ _ _ _ h h' ↦ ?_

Premises used: RingHom.CodescendsAlong.mk, RingHom.FormallyUnramified.respectsIso
-- Module: Mathlib.RingTheory.Etale.Descent
Goal:
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)
⊢ 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

Tactic:
refine .mk _ FormallyUnramified.respectsIso fun R S T _ _ _ _ _ h h' ↦ ?_
-- Module: Mathlib.RingTheory.Etale.Descent
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))
rw : ∀ (h' : Algebra.FormallyUnramified S (S ⊗[R] T)), Algebra.FormallyUnramified R T
⊢ FormallyUnramified (algebraMap R T)

Tactic:
rw [formallyUnramified_algebraMap] at h' ⊢

Premises used: RingHom.formallyUnramified_algebraMap
-- Module: Mathlib.RingTheory.Etale.Descent
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)
⊢ Module.FaithfullyFlat R S

Tactic:
rw [faithfullyFlat_algebraMap_iff] at h

Premises used: RingHom.faithfullyFlat_algebraMap_iff