awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.EssentialFiniteness
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 : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) s : T) ((g : (a : S) → T) s : T)
h : Eq.{u_2 + 1} (α := Subalgebra R ↥(subalgebra R S)) (adjoin R {x : ↥(subalgebra R S) | (↑x : S) ∈ finset R S}) ⊤
h₁ :
  Set.EqOn.{u_2, u_3} (α := ↥(subalgebra R S)) (β := T)
    (⇑(f.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S)) : (a : ↥(subalgebra R S)) → T)
    (⇑(g.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S)) : (a : ↥(subalgebra R S)) → T)
    {x : ↥(subalgebra R S) | (↑x : S) ∈ finset R S}
⊢ Eq (α := AlgHom.{u_1, u_2, u_3} R (↥(subalgebra R S)) T) (f.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S))
    (g.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S))

Tactic:
apply AlgHom.ext_of_adjoin_eq_top (s := { x | x.1 ∈ finset R S })

Premises used: AlgHom.ext_of_adjoin_eq_top
-- Module: Mathlib.RingTheory.EssentialFiniteness
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 : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) s : T) ((g : (a : S) → T) s : T)
⊢ Eq.{u_2 + 1} (α := Subalgebra R ↥(subalgebra R S)) (adjoin R {x : ↥(subalgebra R S) | (↑x : S) ∈ finset R S}) ⊤

Tactic:
adjoin_mem_finset R S

Premises used: Algebra.EssFiniteType.adjoin_mem_finset
-- Module: Mathlib.RingTheory.EssentialFiniteness
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 : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) s : T) ((g : (a : S) → T) s : T)
⊢ Eq.{u_2 + 1} (α := Subalgebra R ↥(subalgebra R S)) (adjoin R {x : ↥(subalgebra R S) | (↑x : S) ∈ finset R S}) ⊤

Tactic:
exact adjoin_mem_finset R S

Premises used: Algebra.EssFiniteType.adjoin_mem_finset
-- Module: Mathlib.RingTheory.EssentialFiniteness
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 : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) s : T) ((g : (a : S) → T) s : T)
x : S
hx : Membership.mem (γ := Subalgebra R S) (subalgebra R S) x
hx' :
  Membership.mem (γ := Set ↥(subalgebra R S)) {x : ↥(subalgebra R S) | (↑x : S) ∈ finset R S}
    (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (subalgebra R S) x) x hx)
⊢ Eq.{u_3 + 1} (α := T)
    ((f.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S) : (a : ↥(subalgebra R S)) → T)
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (subalgebra R S) x) x hx) :
      T)
    ((g.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S) : (a : ↥(subalgebra R S)) → T)
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (subalgebra R S) x) x hx) :
      T)

Tactic:
H x hx'
-- Module: Mathlib.RingTheory.EssentialFiniteness
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 : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) s : T) ((g : (a : S) → T) s : T)
x : S
hx : Membership.mem (γ := Subalgebra R S) (subalgebra R S) x
hx' :
  Membership.mem (γ := Set ↥(subalgebra R S)) {x : ↥(subalgebra R S) | (↑x : S) ∈ finset R S}
    (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (subalgebra R S) x) x hx)
⊢ Eq.{u_3 + 1} (α := T)
    ((f.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S) : (a : ↥(subalgebra R S)) → T)
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (subalgebra R S) x) x hx) :
      T)
    ((g.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S) : (a : ↥(subalgebra R S)) → T)
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (subalgebra R S) x) x hx) :
      T)

Tactic:
exact H x hx'
-- Module: Mathlib.RingTheory.EssentialFiniteness
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 : EssFiniteType R S
p : Ideal R
⊢ EssFiniteType.{u_1, u_2} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))

Tactic:
.of_surjective (Algebra.TensorProduct.quotIdealMapEquivQuotTensor S p).symm.toAlgHom
    (Algebra.TensorProduct.quotIdealMapEquivQuotTensor S p).symm.surjective

Premises used: AlgEquiv.toAlgHom, AlgEquiv.symm, Algebra.TensorProduct.quotIdealMapEquivQuotTensor, AlgEquiv.surjective, Algebra.EssFiniteType.of_surjective
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
rw : Algebra.EssFiniteType R S ↔ Algebra.EssFiniteType R S
rw₁ rw₂ : Algebra.EssFiniteType R S ↔ Algebra.EssFiniteType R S
⊢ EssFiniteType (algebraMap R S) ↔ Algebra.EssFiniteType R S

Tactic:
rw [RingHom.EssFiniteType, toAlgebra_algebraMap]

Premises used: RingHom.EssFiniteType, toAlgebra_algebraMap
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FiniteType
⊢ Algebra.FiniteType R S

Tactic:
algebraize [f]
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FiniteType
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.FiniteType R S
change : Algebra.EssFiniteType R S
⊢ f.EssFiniteType

Tactic:
change Algebra.EssFiniteType R S

Premises used: Algebra.EssFiniteType
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FiniteType
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.FiniteType R S
⊢ Algebra.EssFiniteType R S

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
hf : f.EssFiniteType
g₁ g₂ : S →+* T
h₁ : g₁.comp f = g₂.comp f
h₂ : ∀ x ∈ hf.finset, Eq.{u_3 + 1} (α := T) ((g₁ : (a : S) → T) x : T) ((g₂ : (a : S) → T) x : T)
⊢ Algebra.EssFiniteType R S

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

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
hf : f.EssFiniteType
g₁ g₂ : S →+* T
h₁ : g₁.comp f = g₂.comp f
h₂ : ∀ x ∈ hf.finset, Eq.{u_3 + 1} (α := T) ((g₁ : (a : S) → T) x : T) ((g₂ : (a : S) → T) x : T)
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra R T := (g₁.comp f).toAlgebra
algebraizeInst : Algebra.EssFiniteType R S
a : ∀ (x : S), Eq.{u_3 + 1} (α := T) ((g₁ : (a : S) → T) x : T) ((g₂ : (a : S) → T) x : T)
⊢ g₁ = g₂

Tactic:
ext x
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
hf : f.EssFiniteType
g₁ g₂ : S →+* T
h₁ : g₁.comp f = g₂.comp f
h₂ : ∀ x ∈ hf.finset, Eq.{u_3 + 1} (α := T) ((g₁ : (a : S) → T) x : T) ((g₂ : (a : S) → T) x : T)
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra R T := (g₁.comp f).toAlgebra
algebraizeInst : Algebra.EssFiniteType R S
x : S
⊢ Eq.{u_3 + 1} (α := T) ((g₁ : (a : S) → T) x : T) ((g₂ : (a : S) → T) x : T)

Tactic:
DFunLike.congr_fun (Algebra.EssFiniteType.algHom_ext T
    ⟨g₁, fun _ ↦ rfl⟩ ⟨g₂, DFunLike.congr_fun h₁.symm⟩ h₂) x

Premises used: Algebra.EssFiniteType.algHom_ext, DFunLike.congr_fun, AlgHom.mk, Eq.symm
-- Module: Mathlib.RingTheory.EssentialFiniteness
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
hf : f.EssFiniteType
g₁ g₂ : S →+* T
h₁ : g₁.comp f = g₂.comp f
h₂ : ∀ x ∈ hf.finset, Eq.{u_3 + 1} (α := T) ((g₁ : (a : S) → T) x : T) ((g₂ : (a : S) → T) x : T)
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra R T := (g₁.comp f).toAlgebra
algebraizeInst : Algebra.EssFiniteType R S
x : S
⊢ Eq.{u_3 + 1} (α := T) ((g₁ : (a : S) → T) x : T) ((g₂ : (a : S) → T) x : T)

Tactic:
exact DFunLike.congr_fun (Algebra.EssFiniteType.algHom_ext T
    ⟨g₁, fun _ ↦ rfl⟩ ⟨g₂, DFunLike.congr_fun h₁.symm⟩ h₂) x

Premises used: Algebra.EssFiniteType.algHom_ext, DFunLike.congr_fun, AlgHom.mk, Eq.symm
-- 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
inst_5 : FormallyEtale R A
⊢ FormallyUnramified R A

Tactic:
⟨inferInstance⟩

Premises used: Algebra.FormallyUnramified.mk, inferInstance
-- 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
inst_5 : FormallyEtale R A
⊢ FormallySmooth R A

Tactic:
⟨inferInstance, inferInstance⟩

Premises used: Algebra.FormallySmooth.mk, inferInstance
-- Module: Mathlib.RingTheory.Etale.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ FormallyEtale R A ↔ FormallyUnramified R A ∧ FormallySmooth R A

Tactic:
⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ ⟨inferInstance, inferInstance⟩⟩

Premises used: Algebra.FormallyEtale, Algebra.FormallyEtale.mk, inferInstance, _private.0.Algebra.FormallyEtale.iff_formallyUnramified_and_formallySmooth.match_1, And.intro, Iff.intro
-- Module: Mathlib.RingTheory.Etale.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FormallyUnramified R A
inst_4 : FormallySmooth R A
⊢ FormallyEtale R A

Tactic:
FormallyEtale.iff_formallyUnramified_and_formallySmooth.mpr ⟨‹_›, ‹_›⟩

Premises used: Iff.mpr, Algebra.FormallyEtale.iff_formallyUnramified_and_formallySmooth, And.intro
-- 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
inst_5 : FormallyEtale R A
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
⊢ Function.Bijective (α := A →ₐ[R] B) (β := AlgHom.{u, v, u_1} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))

Tactic:
⟨FormallyUnramified.comp_injective I hI, FormallySmooth.comp_surjective R A I hI⟩

Premises used: Algebra.FormallyUnramified.comp_injective, Algebra.FormallySmooth.comp_surjective, And.intro, Function.Bijective
-- Module: Mathlib.RingTheory.Etale.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Bijective (α := A →ₐ[R] B) (β := A →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
⊢ ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := A →ₐ[R] B) (β := A →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))

Tactic:
aesop (add safe Function.Bijective.injective)

Premises used: Function.Bijective.injective
-- Module: Mathlib.RingTheory.Etale.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Bijective (α := A →ₐ[R] B) (β := A →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
this : FormallyUnramified R A
⊢ ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Surjective (α := A →ₐ[R] B) (β := A →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))

Tactic:
aesop (add safe Function.Bijective.surjective)

Premises used: Function.Bijective.surjective
-- 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
inst_5 : FormallyEtale R A
e : A ≃ₐ[R] B
⊢ FormallyEtale R B

Tactic:
FormallyEtale.iff_formallyUnramified_and_formallySmooth.mpr
    ⟨FormallyUnramified.of_equiv e, FormallySmooth.of_equiv e⟩

Premises used: Iff.mpr, Algebra.FormallySmooth.of_equiv, Algebra.FormallyEtale.iff_formallyUnramified_and_formallySmooth, And.intro, Algebra.FormallyUnramified.of_equiv
-- 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
e : A ≃ₐ[R] B
⊢ FormallyEtale R A ↔ FormallyEtale R B

Tactic:
⟨fun _ ↦ of_equiv e, fun _ ↦ of_equiv e.symm⟩

Premises used: AlgEquiv.symm, Iff.intro, Algebra.FormallyEtale.of_equiv
-- 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
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FormallyEtale R A
inst_8 : FormallyEtale A B
⊢ FormallyEtale R B

Tactic:
FormallyEtale.iff_formallyUnramified_and_formallySmooth.mpr
    ⟨FormallyUnramified.comp R A B, FormallySmooth.comp R A B⟩

Premises used: Iff.mpr, Algebra.FormallyUnramified.comp, Algebra.FormallyEtale.iff_formallyUnramified_and_formallySmooth, And.intro, Algebra.FormallySmooth.comp
-- 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
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FormallyUnramified R A
inst_8 : FormallyEtale R B
⊢ FormallyEtale A B

Tactic:
have := FormallyUnramified.of_restrictScalars R A B
  have := FormallySmooth.of_restrictScalars R A B
  .of_formallyUnramified_and_formallySmooth

Premises used: Algebra.FormallySmooth.of_restrictScalars, Algebra.FormallyEtale.of_formallyUnramified_and_formallySmooth, Algebra.FormallyUnramified.of_restrictScalars
-- 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
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FormallyEtale R A
⊢ FormallyEtale R B ↔ FormallyEtale A B

Tactic:
⟨fun _ ↦ .of_restrictScalars (R := R), fun _ ↦ .comp _ A _⟩

Premises used: Algebra.FormallyEtale.comp, Algebra.FormallyEtale.of_restrictScalars, Iff.intro
-- 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
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FormallyEtale R A
⊢ FormallySmooth R B ↔ FormallySmooth A B

Tactic:
⟨fun _ ↦ .of_restrictScalars R _ _, fun _ ↦ .comp _ A _⟩

Premises used: Algebra.FormallySmooth.of_restrictScalars, Iff.intro, Algebra.FormallySmooth.comp
-- Module: Mathlib.RingTheory.Etale.Basic
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
rw :
  FormallyUnramified R S ∧ FormallySmooth R S ↔
    IsIdempotentElem (M := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
rw₁ : FormallyUnramified R S ∧ FormallySmooth R S ↔ FormallySmooth R S
rw₂ rw₃ : FormallySmooth R S ↔ FormallySmooth R S
⊢ FormallyEtale R S ↔ IsIdempotentElem (M := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))

Tactic:
rw [FormallyEtale.iff_formallyUnramified_and_formallySmooth, ← FormallySmooth.iff_of_surjective h,
    and_iff_right (FormallyUnramified.of_surjective (Algebra.ofId R S) h)]

Premises used: Algebra.FormallyUnramified.of_surjective, Algebra.FormallySmooth.iff_of_surjective, and_iff_right, Algebra.ofId, Algebra.FormallyEtale.iff_formallyUnramified_and_formallySmooth
-- 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
inst_5 : FormallyEtale R A
⊢ FormallyEtale B (B ⊗[R] A)

Tactic:
.of_formallyUnramified_and_formallySmooth

Premises used: Algebra.FormallyEtale.of_formallyUnramified_and_formallySmooth
-- Module: Mathlib.RingTheory.Etale.Basic
Goal:
R : Type u_2
Rₘ : Type u_4
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
⊢ FormallyEtale R Rₘ

Tactic:
FormallyEtale.iff_formallyUnramified_and_formallySmooth.mpr
    ⟨FormallyUnramified.of_isLocalization M, FormallySmooth.of_isLocalization M⟩

Premises used: Iff.mpr, Algebra.FormallySmooth.of_isLocalization, Algebra.FormallyEtale.iff_formallyUnramified_and_formallySmooth, And.intro, Algebra.FormallyUnramified.of_isLocalization
-- 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 : Type u_2
S : Type u_3
Rₘ : Type u_4
Sₘ : Type u_5
inst_5 : CommRing R
inst_6 : CommRing S
inst_7 : CommRing Rₘ
inst_8 : CommRing Sₘ
M_1 : Submonoid R
inst_9 : Algebra R S
inst_10 : Algebra R Sₘ
inst_11 : Algebra S Sₘ
inst_12 : Algebra R Rₘ
inst_13 : Algebra Rₘ Sₘ
inst_14 : IsScalarTower R Rₘ Sₘ
inst_15 : IsScalarTower R S Sₘ
inst_16 : IsLocalization M_1 Rₘ
inst_17 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M_1) Sₘ
inst_18 : FormallyEtale R S
M : Submonoid S
⊢ FormallyEtale.{u_2, u_3} R (Localization (M := S) M)

Tactic:
.of_formallyUnramified_and_formallySmooth

Premises used: Algebra.FormallyEtale.of_formallyUnramified_and_formallySmooth
-- Module: Mathlib.RingTheory.Etale.Basic
Goal:
R : Type u_2
Rₘ : Type u_4
Sₘ : Type u_5
inst : CommRing R
inst_1 : CommRing Rₘ
inst_2 : CommRing Sₘ
M : Submonoid R
inst_3 : Algebra R Sₘ
inst_4 : Algebra R Rₘ
inst_5 : Algebra Rₘ Sₘ
inst_6 : IsScalarTower R Rₘ Sₘ
inst_7 : IsLocalization M Rₘ
inst_8 : FormallyEtale R Sₘ
⊢ FormallyEtale Rₘ Sₘ

Tactic:
FormallyEtale.iff_formallyUnramified_and_formallySmooth.mpr
    ⟨FormallyUnramified.localization_base M, FormallySmooth.localization_base M⟩

Premises used: Iff.mpr, Algebra.FormallyUnramified.localization_base, Algebra.FormallySmooth.localization_base, Algebra.FormallyEtale.iff_formallyUnramified_and_formallySmooth, And.intro
-- Module: Mathlib.RingTheory.Etale.Basic
Goal:
R : Type u_2
S : Type u_3
Rₘ : Type u_4
Sₘ : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
M : Submonoid R
inst_4 : Algebra R S
inst_5 : Algebra R Sₘ
inst_6 : Algebra S Sₘ
inst_7 : Algebra R Rₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : IsScalarTower R Rₘ Sₘ
inst_10 : IsScalarTower R S Sₘ
inst_11 : IsLocalization M Rₘ
inst_12 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) Sₘ
inst_13 : FormallyEtale R S
⊢ FormallyEtale S Sₘ

Tactic:
haveI : FormallyEtale S Sₘ := FormallyEtale.of_isLocalization (M.map (algebraMap R S))
-- Module: Mathlib.RingTheory.Etale.Basic
Goal:
R : Type u_2
S : Type u_3
Rₘ : Type u_4
Sₘ : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
M : Submonoid R
inst_4 : Algebra R S
inst_5 : Algebra R Sₘ
inst_6 : Algebra S Sₘ
inst_7 : Algebra R Rₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : IsScalarTower R Rₘ Sₘ
inst_10 : IsScalarTower R S Sₘ
inst_11 : IsLocalization M Rₘ
inst_12 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) Sₘ
inst_13 : FormallyEtale R S
this : FormallyEtale S Sₘ
⊢ FormallyEtale R Sₘ

Tactic:
haveI : FormallyEtale R Sₘ := FormallyEtale.comp R S Sₘ
-- Module: Mathlib.RingTheory.Etale.Basic
Goal:
R : Type u_2
S : Type u_3
Rₘ : Type u_4
Sₘ : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
M : Submonoid R
inst_4 : Algebra R S
inst_5 : Algebra R Sₘ
inst_6 : Algebra S Sₘ
inst_7 : Algebra R Rₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : IsScalarTower R Rₘ Sₘ
inst_10 : IsScalarTower R S Sₘ
inst_11 : IsLocalization M Rₘ
inst_12 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) Sₘ
inst_13 : FormallyEtale R S
this_1 : FormallyEtale S Sₘ
this : FormallyEtale R Sₘ
⊢ FormallyEtale Rₘ Sₘ

Tactic:
FormallyEtale.localization_base M

Premises used: Algebra.FormallyEtale.localization_base
-- Module: Mathlib.RingTheory.Etale.Basic
Goal:
R : Type u_2
S : Type u_3
Rₘ : Type u_4
Sₘ : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
M : Submonoid R
inst_4 : Algebra R S
inst_5 : Algebra R Sₘ
inst_6 : Algebra S Sₘ
inst_7 : Algebra R Rₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : IsScalarTower R Rₘ Sₘ
inst_10 : IsScalarTower R S Sₘ
inst_11 : IsLocalization M Rₘ
inst_12 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) Sₘ
inst_13 : FormallyEtale R S
this_1 : FormallyEtale S Sₘ
this : FormallyEtale R Sₘ
⊢ FormallyEtale Rₘ Sₘ

Tactic:
exact FormallyEtale.localization_base M

Premises used: Algebra.FormallyEtale.localization_base
-- Module: Mathlib.RingTheory.Etale.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
rw :
  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
⊢ Etale R A ↔ FormallyUnramified R A ∧ Smooth R A

Tactic:
rw [etale_iff, FormallyEtale.iff_formallyUnramified_and_formallySmooth, smooth_iff]

Premises used: Algebra.smooth_iff, Algebra.etale_iff, Algebra.FormallyEtale.iff_formallyUnramified_and_formallySmooth