awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsPrincipalIdealRing R
isf : ¬IsField R
neg :
  ∀ (x : R) (hx : Eq (α := Submodule R R) (maximalIdeal R) (R ∙ x)),
    (↑(Submodule.spanFinrank (maximalIdeal R)) : WithBot ℕ∞) ≤ ringKrullDim R
⊢ (↑(Submodule.spanFinrank (maximalIdeal R)) : WithBot ℕ∞) ≤ ringKrullDim R

Tactic:
rcases IsPrincipalIdealRing.principal (maximalIdeal R) with ⟨x, hx⟩

Premises used: IsLocalRing.maximalIdeal, IsPrincipalIdealRing.principal
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsPrincipalIdealRing R
isf : ¬IsField R
x : R
hx : Eq (α := Submodule R R) (maximalIdeal R) (R ∙ x)
⊢ (↑(Submodule.spanFinrank (maximalIdeal R)) : WithBot ℕ∞) ≤ ringKrullDim R

Tactic:
simpa only [(IsPrincipalIdealRing.ringKrullDim_eq_one R) isf,
      Nat.cast_le_one, ← Set.ncard_singleton x, hx] using
        Submodule.spanFinrank_span_le_ncard_of_finite (Set.finite_singleton x)

Premises used: Submodule.spanFinrank_span_le_ncard_of_finite, IsPrincipalIdealRing.ringKrullDim_eq_one, Set.ncard_singleton, Set.finite_singleton, Nat.cast_le_one
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
⊢ IsRegularRing R ↔ ∀ (p : Ideal R) [inst_2 : p.IsPrime], IsRegularLocalRing.{u_1} (Localization.AtPrime p)

Tactic:
⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

Premises used: IsRegularRing.mk, _private.0.isRegularRing_iff.match_1, Iff.intro
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
Goal:
R : Type u_1
inst : CommRing R
R' : Type u_2
inst_1 : CommRing R'
e : R ≃+* R'
inst_2 : IsRegularRing R
⊢ IsNoetherianRing R'

Tactic:
have := isNoetherianRing_of_ringEquiv R e
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
Goal:
R : Type u_1
inst : CommRing R
R' : Type u_2
inst_1 : CommRing R'
e : R ≃+* R'
inst_2 : IsRegularRing R
this : IsNoetherianRing R'
rw : ∀ (p : Ideal R') [inst : p.IsPrime], IsRegularLocalRing.{u_2} (Localization.AtPrime p)
⊢ IsRegularRing R'

Tactic:
rw [isRegularRing_iff]

Premises used: isRegularRing_iff
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
Goal:
R : Type u_1
inst : CommRing R
R' : Type u_2
inst_1 : CommRing R'
e : R ≃+* R'
inst_2 : IsRegularRing R
this : IsNoetherianRing R'
p : Ideal R'
hp : p.IsPrime
⊢ IsRegularLocalRing.{u_2} (Localization.AtPrime p)

Tactic:
IsRegularLocalRing.of_ringEquiv <| IsLocalization.ringEquivOfRingEquiv
    (Localization.AtPrime (p.comap e)) (Localization.AtPrime p) e (e.map_primeCompl_comap_eq p)

Premises used: Localization.AtPrime, IsRegularLocalRing.of_ringEquiv, IsLocalization.ringEquivOfRingEquiv, RingEquiv.map_primeCompl_comap_eq, Ideal.comap
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
Goal:
R : Type u_1
inst : CommRing R
R' : Type u_2
inst_1 : CommRing R'
e : R ≃+* R'
inst_2 : IsRegularRing R
this : IsNoetherianRing R'
p : Ideal R'
hp : p.IsPrime
⊢ IsRegularLocalRing.{u_2} (Localization.AtPrime p)

Tactic:
exact IsRegularLocalRing.of_ringEquiv <| IsLocalization.ringEquivOfRingEquiv
    (Localization.AtPrime (p.comap e)) (Localization.AtPrime p) e (e.map_primeCompl_comap_eq p)

Premises used: Localization.AtPrime, IsRegularLocalRing.of_ringEquiv, IsLocalization.ringEquivOfRingEquiv, RingEquiv.map_primeCompl_comap_eq, Ideal.comap
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsRegularRing R
x : R
⊢ Membership.mem (γ := Submonoid R) (Ideal.primeCompl (maximalIdeal R)) x →
    Membership.mem (γ := Submonoid R) (IsUnit.submonoid R) x

Tactic:
simpa using fun a ↦ a
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsRegularRing R
e : R ≃ₐ[R] Localization.AtPrime (maximalIdeal R) := IsLocalization.atUnits R (Ideal.primeCompl (maximalIdeal R)) ⋯
⊢ IsRegularLocalRing R

Tactic:
IsRegularLocalRing.of_ringEquiv e.toRingEquiv.symm

Premises used: IsRegularLocalRing.of_ringEquiv, AlgEquiv.toRingEquiv, RingEquiv.symm
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsRegularRing R
e : R ≃ₐ[R] Localization.AtPrime (maximalIdeal R) := IsLocalization.atUnits R (Ideal.primeCompl (maximalIdeal R)) ⋯
⊢ IsRegularLocalRing R

Tactic:
exact IsRegularLocalRing.of_ringEquiv e.toRingEquiv.symm

Premises used: IsRegularLocalRing.of_ringEquiv, AlgEquiv.toRingEquiv, RingEquiv.symm
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
rw : ∀ (p : Ideal R) [inst_2 : p.IsPrime], IsRegularLocalRing.{u_1} (Localization.AtPrime p)
⊢ IsRegularRing R

Tactic:
rw [isRegularRing_iff]

Premises used: isRegularRing_iff
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
p : Ideal R
hp : p.IsPrime
pos : ∀ (eqbot : p = ⊥), IsRegularLocalRing.{u_1} (Localization.AtPrime p)
neg : ∀ (eqbot : ¬p = ⊥), IsRegularLocalRing.{u_1} (Localization.AtPrime p)
⊢ IsRegularLocalRing.{u_1} (Localization.AtPrime p)

Tactic:
by_cases eqbot : p = ⊥
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
p : Ideal R
hp : p.IsPrime
eqbot : p = ⊥
⊢ IsField.{u_1} (Localization.AtPrime p)

Tactic:
simp [isField_iff_maximalIdeal_eq, ← Localization.AtPrime.map_eq_maximalIdeal, eqbot]

Premises used: IsLocalRing.isField_iff_maximalIdeal_eq, Localization.AtPrime.map_eq_maximalIdeal
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
p : Ideal R
hp : p.IsPrime
eqbot : p = ⊥
this : Field (Localization.AtPrime p) := ⋯.toField
⊢ IsRegularLocalRing.{u_1} (Localization.AtPrime p)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
p : Ideal R
hp : p.IsPrime
eqbot : ¬p = ⊥
⊢ IsDiscreteValuationRing.{u_1} (Localization.AtPrime p)

Tactic:
have := IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain
      R eqbot (Localization.AtPrime p)
-- Module: Mathlib.RingTheory.RegularLocalRing.Defs
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
p : Ideal R
hp : p.IsPrime
eqbot : ¬p = ⊥
this : IsDiscreteValuationRing.{u_1} (Localization.AtPrime p)
⊢ IsRegularLocalRing.{u_1} (Localization.AtPrime p)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.RingHom.Bijective
Goal:
⊢ ContainsIdentities.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] (f : R →+* S) ↦
    Function.Bijective (α := R) (β := S) (⇑f : (a : R) → S)

Tactic:
fun _ _ ↦ Function.bijective_id

Premises used: Function.bijective_id, RingHom.ContainsIdentities
-- Module: Mathlib.RingTheory.RingHom.Bijective
Goal:
⊢ StableUnderComposition.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] (f : R →+* S) ↦
    Function.Bijective (α := R) (β := S) (⇑f : (a : R) → S)

Tactic:
fun _ _ _ _ _ _ _ _ hf hg ↦ hg.comp hf

Premises used: RingHom.StableUnderComposition, Function.Bijective.comp
-- Module: Mathlib.RingTheory.RingHom.Bijective
Goal:
⊢ RespectsIso.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] (f : R →+* S) ↦
    Function.Bijective (α := R) (β := S) (⇑f : (a : R) → S)

Tactic:
RingHom.Bijective.stableUnderComposition.respectsIso fun e ↦ e.bijective

Premises used: RingHom.StableUnderComposition.respectsIso, RingEquiv.bijective, RingHom.Bijective.stableUnderComposition
-- Module: Mathlib.RingTheory.RingHom.Bijective
Goal:
⊢ IsStableUnderBaseChange.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] (f : R →+* S) ↦
    Function.Bijective (α := R) (β := S) (⇑f : (a : R) → S)

Tactic:
.mk respectsIso fun R _ _ _ _ _ _ _ hf ↦
    Algebra.TensorProduct.includeLeft_bijective (S := R) hf

Premises used: RingHom.Bijective.respectsIso, RingHom.IsStableUnderBaseChange.mk, Algebra.TensorProduct.includeLeft_bijective
-- Module: Mathlib.RingTheory.RingHom.Bijective
Goal:
⊢ OfLocalizationSpan.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] (f : R →+* S) ↦
    Function.Bijective (α := R) (β := S) (⇑f : (a : R) → S)

Tactic:
fun _ _ _ _ f s hs hf ↦ bijective_of_isLocalization_of_span_eq_top (s := s) hs
    (fun r ↦ Localization.Away r.val) (fun r ↦ Localization.Away (f r.val)) f hf

Premises used: Localization.Away, RingHom.OfLocalizationSpan, bijective_of_isLocalization_of_span_eq_top, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.RingHom.EssFiniteType
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
g : S →+* T
hf : f.EssFiniteType
hg : g.EssFiniteType
⊢ Algebra.EssFiniteType R S

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

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.EssFiniteType
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
g : S →+* T
hf : f.EssFiniteType
hg : g.EssFiniteType
algebraizeInst : Algebra.EssFiniteType R S
⊢ Algebra.EssFiniteType S T

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

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.EssFiniteType
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
g : S →+* T
hf : f.EssFiniteType
hg : g.EssFiniteType
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.EssFiniteType R S
algebraizeInst_1 : Algebra.EssFiniteType S T
⊢ (g.comp f).EssFiniteType

Tactic:
Algebra.EssFiniteType.comp R S T

Premises used: Algebra.EssFiniteType.comp, RingHom.EssFiniteType
-- Module: Mathlib.RingTheory.RingHom.EssFiniteType
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
g : S →+* T
hf : f.EssFiniteType
hg : g.EssFiniteType
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.EssFiniteType R S
algebraizeInst_1 : Algebra.EssFiniteType S T
⊢ (g.comp f).EssFiniteType

Tactic:
exact Algebra.EssFiniteType.comp R S T

Premises used: Algebra.EssFiniteType.comp
-- Module: Mathlib.RingTheory.RingHom.EssFiniteType
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
g : S →+* T
hf : f.EssFiniteType
⊢ Algebra.EssFiniteType R S

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

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.EssFiniteType
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
g : S →+* T
hf : f.EssFiniteType
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.EssFiniteType R S
⊢ (g.comp f).EssFiniteType ↔ g.EssFiniteType

Tactic:
Algebra.EssFiniteType.comp_iff R S T

Premises used: RingHom.EssFiniteType, Algebra.EssFiniteType.comp_iff
-- Module: Mathlib.RingTheory.RingHom.EssFiniteType
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
g : S →+* T
hf : f.EssFiniteType
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.EssFiniteType R S
⊢ (g.comp f).EssFiniteType ↔ g.EssFiniteType

Tactic:
exact Algebra.EssFiniteType.comp_iff R S T

Premises used: Algebra.EssFiniteType.comp_iff
-- Module: Mathlib.RingTheory.RingHom.EssFiniteType
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
g : S →+* T
h : (g.comp f).EssFiniteType
⊢ Algebra.EssFiniteType R T

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

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.EssFiniteType
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
g : S →+* T
h : (g.comp f).EssFiniteType
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.EssFiniteType R T
⊢ g.EssFiniteType

Tactic:
Algebra.EssFiniteType.of_comp R S T

Premises used: Algebra.EssFiniteType.of_comp, RingHom.EssFiniteType
-- Module: Mathlib.RingTheory.RingHom.EssFiniteType
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
g : S →+* T
h : (g.comp f).EssFiniteType
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.EssFiniteType R T
⊢ g.EssFiniteType

Tactic:
exact Algebra.EssFiniteType.of_comp R S T

Premises used: Algebra.EssFiniteType.of_comp
-- Module: Mathlib.RingTheory.RingHom.EssFiniteType
Goal:
⊢ StableUnderComposition.{u_4} fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ EssFiniteType

Tactic:
fun _ _ _ _ _ _ _ _ hf hg ↦ hf.comp hg

Premises used: RingHom.EssFiniteType.comp, RingHom.StableUnderComposition
-- Module: Mathlib.RingTheory.RingHom.EssFiniteType
Goal:
⊢ RespectsIso.{u_4} fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ EssFiniteType

Tactic:
stableUnderComposition.respectsIso fun e ↦ (FiniteType.of_surjective _ e.surjective).essFiniteType

Premises used: RingHom.StableUnderComposition.respectsIso, RingEquiv.toRingHom, RingHom.FiniteType.of_surjective, RingHom.FiniteType.essFiniteType, RingHom.EssFiniteType.stableUnderComposition
-- Module: Mathlib.RingTheory.RingHom.EssFiniteType
Goal:
R S T : Type u_4
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : EssFiniteType (algebraMap R T)
rw : ∀ (h : Algebra.EssFiniteType R T), Algebra.EssFiniteType S (TensorProduct R S T)
⊢ EssFiniteType (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))

Tactic:
rw [essFiniteType_algebraMap] at h ⊢

Premises used: RingHom.essFiniteType_algebraMap
-- Module: Mathlib.RingTheory.RingHom.EssFiniteType
Goal:
R S T : Type u_4
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : Algebra.EssFiniteType R T
⊢ Algebra.EssFiniteType S (TensorProduct R S T)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.RingHom.EssFiniteType
Goal:
R S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
rw : Algebra.EssFiniteType R S
⊢ EssFiniteType (algebraMap R S)

Tactic:
rw [essFiniteType_algebraMap]

Premises used: RingHom.essFiniteType_algebraMap
-- Module: Mathlib.RingTheory.RingHom.EssFiniteType
Goal:
R S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
⊢ Algebra.EssFiniteType R S

Tactic:
.of_isLocalization _ M

Premises used: Algebra.EssFiniteType.of_isLocalization
-- Module: Mathlib.RingTheory.RingHom.EssFiniteType
Goal:
R S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
⊢ Algebra.EssFiniteType R S

Tactic:
exact .of_isLocalization _ M
-- Module: Mathlib.RingTheory.RingHom.EssFiniteType
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalRing R
inst_3 : IsLocalRing S
inst_4 : IsLocalHom (R := R) (S := S) f
hf : f.EssFiniteType
⊢ EssFiniteType (R := IsLocalRing.ResidueField R) (S := IsLocalRing.ResidueField S) (IsLocalRing.ResidueField.map f)

Tactic:
.of_comp (IsLocalRing.residue R) ?_

Premises used: IsLocalRing.residue, RingHom.EssFiniteType.of_comp
-- Module: Mathlib.RingTheory.RingHom.EssFiniteType
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalRing R
inst_3 : IsLocalRing S
inst_4 : IsLocalHom (R := R) (S := S) f
hf : f.EssFiniteType
refine :
  EssFiniteType (S := IsLocalRing.ResidueField S)
    (RingHom.comp (β := IsLocalRing.ResidueField R) (IsLocalRing.ResidueField.map f) (IsLocalRing.residue R))
⊢ EssFiniteType (R := IsLocalRing.ResidueField R) (S := IsLocalRing.ResidueField S) (IsLocalRing.ResidueField.map f)

Tactic:
refine .of_comp (IsLocalRing.residue R) ?_
-- Module: Mathlib.RingTheory.RingHom.EssFiniteType
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalRing R
inst_3 : IsLocalRing S
inst_4 : IsLocalHom (R := R) (S := S) f
hf : f.EssFiniteType
rw : EssFiniteType (S := IsLocalRing.ResidueField S) (RingHom.comp (IsLocalRing.residue S) f)
⊢ EssFiniteType (S := IsLocalRing.ResidueField S)
    (RingHom.comp (β := IsLocalRing.ResidueField R) (IsLocalRing.ResidueField.map f) (IsLocalRing.residue R))

Tactic:
rw [IsLocalRing.ResidueField.map_comp_residue]

Premises used: IsLocalRing.ResidueField.map_comp_residue
-- Module: Mathlib.RingTheory.RingHom.EssFiniteType
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalRing R
inst_3 : IsLocalRing S
inst_4 : IsLocalHom (R := R) (S := S) f
hf : f.EssFiniteType
⊢ EssFiniteType (S := IsLocalRing.ResidueField S) (RingHom.comp (IsLocalRing.residue S) f)

Tactic:
.comp hf (FiniteType.of_surjective _ <| IsLocalRing.residue_surjective).essFiniteType

Premises used: RingHom.EssFiniteType.comp, RingHom.FiniteType.of_surjective, RingHom.FiniteType.essFiniteType, IsLocalRing.residue_surjective
-- Module: Mathlib.RingTheory.RingHom.EssFiniteType
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalRing R
inst_3 : IsLocalRing S
inst_4 : IsLocalHom (R := R) (S := S) f
hf : f.EssFiniteType
⊢ EssFiniteType (S := IsLocalRing.ResidueField S) (RingHom.comp (IsLocalRing.residue S) f)

Tactic:
exact .comp hf (FiniteType.of_surjective _ <| IsLocalRing.residue_surjective).essFiniteType
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.Etale
⊢ Algebra.Etale R S

Tactic:
hf

Premises used: RingHom.Etale
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
rw : Algebra.Etale R S ↔ Algebra.Etale R S
rw₁ rw₂ : Algebra.Etale R S ↔ Algebra.Etale R S
⊢ Etale (algebraMap R S) ↔ Algebra.Etale R S

Tactic:
rw [RingHom.Etale, toAlgebra_algebraMap]

Premises used: RingHom.Etale, toAlgebra_algebraMap
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
algInst : Algebra R S := f.toAlgebra
⊢ Algebra.Etale R S ↔ Algebra.FormallyUnramified R S ∧ Algebra.Smooth R S

Tactic:
⟨fun h ↦ ⟨inferInstance, inferInstance, inferInstance⟩,
    fun ⟨h1, h2⟩ ↦ ⟨.of_formallyUnramified_and_formallySmooth, inferInstance⟩⟩

Premises used: Algebra.Etale.mk, Algebra.Smooth.mk, _private.0.RingHom.etale_iff_formallyUnramified_and_smooth.match_1, Algebra.Etale, inferInstance, And.intro, Iff.intro, Algebra.FormallyEtale.of_formallyUnramified_and_formallySmooth
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
algInst : Algebra R S := f.toAlgebra
⊢ Algebra.Etale R S ↔ Algebra.FormallyUnramified R S ∧ Algebra.Smooth R S

Tactic:
exact ⟨fun h ↦ ⟨inferInstance, inferInstance, inferInstance⟩,
    fun ⟨h1, h2⟩ ↦ ⟨.of_formallyUnramified_and_formallySmooth, inferInstance⟩⟩
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
h :
  ∀ (x : Type u_6) (x_1 : Type u_5) (x_2 : CommRing x) (x_3 : CommRing x_1) (x_4 : x →+* x_1),
    x_4.Etale ↔ x_4.FormallyUnramified ∧ x_4.Smooth
⊢ @Etale = fun (R : Type u_6) (S : Type u_5) (x : CommRing R) (x_1 : CommRing S) (f : R →+* S) ↦
    f.FormallyUnramified ∧ f.Smooth

Tactic:
ext
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
x : Type u_6
x_1 : Type u_5
x_2 : CommRing x
x_3 : CommRing x_1
x_4 : x →+* x_1
h h₁ : x_4.FormallyUnramified ∧ x_4.Smooth ↔ x_4.FormallyUnramified ∧ x_4.Smooth
⊢ x_4.Etale ↔ x_4.FormallyUnramified ∧ x_4.Smooth

Tactic:
rw [etale_iff_formallyUnramified_and_smooth]

Premises used: RingHom.etale_iff_formallyUnramified_and_smooth
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.Etale
⊢ f.FormallyUnramified ∧ f.Smooth

Tactic:
rw [etale_iff_formallyUnramified_and_smooth] at hf

Premises used: RingHom.etale_iff_formallyUnramified_and_smooth
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FormallyUnramified ∧ f.Smooth
⊢ f.FormallyUnramified

Tactic:
hf.1

Premises used: And.left
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FormallyUnramified ∧ f.Smooth
⊢ f.FormallyUnramified

Tactic:
exact hf.1

Premises used: And.left
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Bijective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
rw : f.FormallyUnramified ∧ f.Smooth
⊢ f.Etale

Tactic:
rw [etale_iff_formallyUnramified_and_smooth]

Premises used: RingHom.etale_iff_formallyUnramified_and_smooth
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Bijective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ f.FormallyUnramified ∧ f.Smooth

Tactic:
⟨.of_surjective hf.2, .of_bijective hf⟩

Premises used: RingHom.Smooth.of_bijective, And.right, And.intro, RingHom.FormallyUnramified.of_surjective
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Bijective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ f.FormallyUnramified ∧ f.Smooth

Tactic:
exact ⟨.of_surjective hf.2, .of_bijective hf⟩
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
⊢ ContainsIdentities.{u_5} fun {R S : Type u_5} [CommRing R] [CommRing S] ↦ Etale

Tactic:
fun _ _ ↦ .of_bijective Function.bijective_id

Premises used: Function.bijective_id, RingHom.ContainsIdentities, RingHom.Etale.of_bijective
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
rw :
  IsStableUnderBaseChange.{u_5} fun {R S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] ↦
    (fun (R S : Type u_5) (x : CommRing R) (x_1 : CommRing S) (f : R →+* S) ↦ f.FormallyUnramified ∧ f.Smooth) R S inst
      inst_1
⊢ IsStableUnderBaseChange.{u_5} fun {R S : Type u_5} [CommRing R] [CommRing S] ↦ Etale

Tactic:
rw [eq_formallyUnramified_and_smooth]

Premises used: RingHom.Etale.eq_formallyUnramified_and_smooth
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
⊢ IsStableUnderBaseChange.{u_5} fun {R S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] ↦
    (fun (R S : Type u_5) (x : CommRing R) (x_1 : CommRing S) (f : R →+* S) ↦ f.FormallyUnramified ∧ f.Smooth) R S inst
      inst_1

Tactic:
FormallyUnramified.isStableUnderBaseChange.and Smooth.isStableUnderBaseChange

Premises used: RingHom.FormallyUnramified.isStableUnderBaseChange, RingHom.IsStableUnderBaseChange.and, RingHom.Smooth.isStableUnderBaseChange
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
⊢ IsStableUnderBaseChange.{u_5} fun {R S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] ↦
    (fun (R S : Type u_5) (x : CommRing R) (x_1 : CommRing S) (f : R →+* S) ↦ f.FormallyUnramified ∧ f.Smooth) R S inst
      inst_1

Tactic:
exact FormallyUnramified.isStableUnderBaseChange.and Smooth.isStableUnderBaseChange

Premises used: RingHom.FormallyUnramified.isStableUnderBaseChange, RingHom.IsStableUnderBaseChange.and, RingHom.Smooth.isStableUnderBaseChange