awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
a b : R
h : IsUnit (a + b)
rcases : ∀ (u : Rˣ) (hu : (↑u : R) = a + b), IsUnit a ∨ IsUnit b
⊢ IsUnit a ∨ IsUnit b

Tactic:
rcases h with ⟨u, hu⟩
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
a b : R
u : Rˣ
hu : (↑u : R) = a + b
⊢ (↑u⁻¹ : R) * a + (↑u⁻¹ : R) * b = 1

Tactic:
rw [← Units.inv_mul_eq_one, mul_add] at hu

Premises used: Units.inv_mul_eq_one, mul_add
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
a b : R
u : Rˣ
hu : (↑u⁻¹ : R) * a + (↑u⁻¹ : R) * b = 1
apply : IsUnit ((↑u⁻¹ : R) * a) → IsUnit a
apply₁ : IsUnit ((↑u⁻¹ : R) * b) → IsUnit b
⊢ IsUnit a ∨ IsUnit b

Tactic:
apply Or.imp _ _ (isUnit_or_isUnit_of_add_one hu)

Premises used: IsLocalRing.isUnit_or_isUnit_of_add_one, Or.imp
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
a b : R
u : Rˣ
hu : (↑u⁻¹ : R) * a + (↑u⁻¹ : R) * b = 1
⊢ IsUnit ((↑u⁻¹ : R) * a) → IsUnit a

Tactic:
isUnit_of_mul_isUnit_right

Premises used: isUnit_of_mul_isUnit_right
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
a b : R
u : Rˣ
hu : (↑u⁻¹ : R) * a + (↑u⁻¹ : R) * b = 1
⊢ IsUnit ((↑u⁻¹ : R) * a) → IsUnit a

Tactic:
exact isUnit_of_mul_isUnit_right

Premises used: isUnit_of_mul_isUnit_right
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
a b : R
u : Rˣ
hu : (↑u⁻¹ : R) * a + (↑u⁻¹ : R) * b = 1
⊢ IsUnit ((↑u⁻¹ : R) * b) → IsUnit b

Tactic:
isUnit_of_mul_isUnit_right

Premises used: isUnit_of_mul_isUnit_right
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
a b : R
u : Rˣ
hu : (↑u⁻¹ : R) * a + (↑u⁻¹ : R) * b = 1
⊢ IsUnit ((↑u⁻¹ : R) * b) → IsUnit b

Tactic:
exact isUnit_of_mul_isUnit_right

Premises used: isUnit_of_mul_isUnit_right
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
a b : R
ha : a ∈ nonunits R
hb : b ∈ nonunits R
⊢ a + b ∈ nonunits R

Tactic:
fun H => not_or_intro ha hb (isUnit_or_isUnit_of_isUnit_add H)

Premises used: Set.Mem, setOf, nonunits, IsLocalRing.isUnit_or_isUnit_of_isUnit_add, not_or_intro, Not
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
h : ∀ (a : R), IsUnit a ∨ IsUnit (1 - a)
⊢ IsLocalRing R

Tactic:
⟨fun {a b} hab => add_sub_cancel_left a b ▸ hab.symm ▸ h a⟩

Premises used: add_sub_cancel_left, Eq.rec, IsLocalRing.of_is_unit_or_is_unit_of_add_one, Eq.symm
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
a : R
⊢ IsUnit a ∨ IsUnit (1 - a)

Tactic:
isUnit_or_isUnit_of_isUnit_add <| (add_sub_cancel a 1).symm ▸ isUnit_one

Premises used: Eq.rec, IsLocalRing.isUnit_or_isUnit_of_isUnit_add, isUnit_one, add_sub_cancel, OfNat.ofNat, Eq.symm
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
a : R
h : 1 - a ∈ nonunits R
⊢ IsUnit a

Tactic:
or_iff_not_imp_right.1 (isUnit_or_isUnit_one_sub_self a) h

Premises used: IsLocalRing.isUnit_or_isUnit_one_sub_self, Classical.or_iff_not_imp_right, Iff.mp
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
a : R
h : a ∈ nonunits R
⊢ IsUnit (1 - a)

Tactic:
or_iff_not_imp_left.1 (isUnit_or_isUnit_one_sub_self a) h

Premises used: IsLocalRing.isUnit_or_isUnit_one_sub_self, Classical.or_iff_not_imp_left, Iff.mp
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : Ring S
inst_3 : Nontrivial S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
b : S
obtain :
  ∀ (a : R),
    IsUnit.{u_2} (M := S) ((f : (a : R) → S) a : S) ∨
      IsUnit (HSub.hSub (α := S) (β := S) (1 : S) ((f : (a : R) → S) a : S))
⊢ IsUnit b ∨ IsUnit (1 - b)

Tactic:
obtain ⟨a, rfl⟩ := hf b

Premises used: rfl
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : Ring S
inst_3 : Nontrivial S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
apply : IsUnit (1 - a) → IsUnit (HSub.hSub (α := S) (β := S) (1 : S) ((f : (a : R) → S) a : S))
⊢ IsUnit.{u_2} (M := S) ((f : (a : R) → S) a : S) ∨
    IsUnit (HSub.hSub (α := S) (β := S) (1 : S) ((f : (a : R) → S) a : S))

Tactic:
apply (isUnit_or_isUnit_one_sub_self a).imp <| RingHom.isUnit_map _

Premises used: IsLocalRing.isUnit_or_isUnit_one_sub_self, RingHom.isUnit_map, Or.imp
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : Ring S
inst_3 : Nontrivial S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
rw : IsUnit (1 - a) → IsUnit.{u_2} (M := S) ((f : (a : R) → S) (1 - a) : S)
⊢ IsUnit (1 - a) → IsUnit (HSub.hSub (α := S) (β := S) (1 : S) ((f : (a : R) → S) a : S))

Tactic:
rw [← f.map_one, ← f.map_sub]

Premises used: RingHom.map_one, RingHom.map_sub
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : Ring S
inst_3 : Nontrivial S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
⊢ IsUnit (1 - a) → IsUnit.{u_2} (M := S) ((f : (a : R) → S) (1 - a) : S)

Tactic:
apply f.isUnit_map

Premises used: RingHom.isUnit_map
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : Field K
a : K
h : a = 0
rw : IsUnit.{u_3} (M := K) 1
⊢ IsUnit (1 - a)

Tactic:
rw [h, sub_zero]

Premises used: sub_zero
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : Field K
a : K
h : a = 0
⊢ IsUnit.{u_3} (M := K) 1

Tactic:
isUnit_one

Premises used: isUnit_one
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : Field K
a : K
h : a = 0
⊢ IsUnit.{u_3} (M := K) 1

Tactic:
exact isUnit_one

Premises used: isUnit_one
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : Field K
⊢ IsLocalRing K

Tactic:
exact IsLocalRing.of_isUnit_or_isUnit_one_sub_self fun a =>
    if h : a = 0 then Or.inr (by rw [h, sub_zero]; exact isUnit_one)
    else Or.inl <| IsUnit.mk0 a h

Premises used: dite, Or.inl, OfNat.ofNat, Eq, IsLocalRing.of_isUnit_or_isUnit_one_sub_self, Or.inr
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : Field K
⊢ IsLocalRing K

Tactic:
classical exact IsLocalRing.of_isUnit_or_isUnit_one_sub_self fun a =>
    if h : a = 0 then Or.inr (by rw [h, sub_zero]; exact isUnit_one)
    else Or.inl <| IsUnit.mk0 a h

Premises used: dite, Or.inl, OfNat.ofNat, Eq, IsLocalRing.of_isUnit_or_isUnit_one_sub_self, Or.inr
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
mp :
  Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
      (ResidueField R)[((residue S : (a : S) → ResidueField S) β : ResidueField S)] ⊤ →
    Eq (α := Subalgebra R S) R[β] ⊤
mpr :
  Eq (α := Subalgebra R S) R[β] ⊤ →
    Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
      (ResidueField R)[((residue S : (a : S) → ResidueField S) β : ResidueField S)] ⊤
⊢ Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
      (ResidueField R)[((residue S : (a : S) → ResidueField S) β : ResidueField S)] ⊤ ↔
    Eq (α := Subalgebra R S) R[β] ⊤

Tactic:
constructor
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ :
  Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
    (ResidueField R)[((residue S : (a : S) → ResidueField S) β : ResidueField S)] ⊤
⊢ Eq (α := Subalgebra R S) R[β] ⊤

Tactic:
eq_top_iff.mpr <| Submodule.le_of_le_smul_of_le_jacobson_bot
      (Module.finite_def.mp inferInstance) (IsLocalRing.maximalIdeal_le_jacobson ⊥)
      (?_ : ⊤ ≤ (adjoin R {β}).toSubmodule ⊔ maximalIdeal R • ⊤)

Premises used: Iff.mpr, Submodule.le_of_le_smul_of_le_jacobson_bot, eq_top_iff, IsLocalRing.maximalIdeal_le_jacobson, inferInstance, Bot.bot, Module.finite_def, Iff.mp
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ :
  Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
    (ResidueField R)[((residue S : (a : S) → ResidueField S) β : ResidueField S)] ⊤
mp :
  LE.le (α := Submodule R S) (⊤ : Submodule R S)
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[β] ⊔
        HSMul.hSMul (α := Ideal R) (β := Submodule R S) (maximalIdeal R) ⊤ :
      Submodule R S)
⊢ Eq (α := Subalgebra R S) R[β] ⊤

Tactic:
refine eq_top_iff.mpr <| Submodule.le_of_le_smul_of_le_jacobson_bot
      (Module.finite_def.mp inferInstance) (IsLocalRing.maximalIdeal_le_jacobson ⊥)
      (?_ : ⊤ ≤ (adjoin R {β}).toSubmodule ⊔ maximalIdeal R • ⊤)

Premises used: Submodule.le_of_le_smul_of_le_jacobson_bot, IsLocalRing.maximalIdeal_le_jacobson, inferInstance, Bot.bot, Module.finite_def, Iff.mp
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ :
  Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
    (ResidueField R)[((residue S : (a : S) → ResidueField S) β : ResidueField S)] ⊤
s : S
mp :
  Membership.mem (γ := Submodule R S) ⊤ s →
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[β] ⊔
          HSMul.hSMul (α := Ideal R) (β := Submodule R S) (maximalIdeal R) ⊤ :
        Submodule R S)
      s
⊢ Membership.mem (γ := Submodule R S) ⊤ s →
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[β] ⊔
          HSMul.hSMul (α := Ideal R) (β := Submodule R S) (maximalIdeal R) ⊤ :
        Submodule R S)
      s

Tactic:
_
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ :
  Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
    (ResidueField R)[((residue S : (a : S) → ResidueField S) β : ResidueField S)] ⊤
s : S
h : Membership.mem (γ := Submodule R S) ⊤ s
mp :
  ∀
    (hβ :
      Function.Surjective.{u_1 + 1, u_2 + 1} (α := (ResidueField R)[X]) (β := ResidueField S)
        (⇑(aeval ((residue S : (a : S) → ResidueField S) β) :
              AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
          (a : (ResidueField R)[X]) → ResidueField S))
    ⦃s : S⦄,
    Membership.mem (γ := Submodule R S) ⊤ s →
      Membership.mem (γ := Submodule R S)
        ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[β] ⊔
            HSMul.hSMul (α := Ideal R) (β := Submodule R S) (maximalIdeal R) ⊤ :
          Submodule R S)
        s
⊢ Membership.mem (γ := Submodule R S)
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[β] ⊔
        HSMul.hSMul (α := Ideal R) (β := Submodule R S) (maximalIdeal R) ⊤ :
      Submodule R S)
    s

Tactic:
rw [adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hβ

Premises used: Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := (ResidueField R)[X]) (β := ResidueField S)
    (⇑(aeval ((residue S : (a : S) → ResidueField S) β) :
          AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
      (a : (ResidueField R)[X]) → ResidueField S)
s : S
h : Membership.mem (γ := Submodule R S) ⊤ s
mp :
  ∀ (p : (ResidueField R)[X])
    (hp :
      Eq.{u_2 + 1} (α := ResidueField S)
        (((aeval ((residue S : (a : S) → ResidueField S) β) :
                AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
              (a : (ResidueField R)[X]) → ResidueField S)
            p :
          ResidueField S)
        ((residue S : (a : S) → ResidueField S) s : ResidueField S)),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[β] ⊔
          HSMul.hSMul (α := Ideal R) (β := Submodule R S) (maximalIdeal R) ⊤ :
        Submodule R S)
      s
⊢ Membership.mem (γ := Submodule R S)
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[β] ⊔
        HSMul.hSMul (α := Ideal R) (β := Submodule R S) (maximalIdeal R) ⊤ :
      Submodule R S)
    s

Tactic:
obtain ⟨p, hp⟩ := hβ (residue S s)

Premises used: IsLocalRing.residue, DFunLike.coe
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := (ResidueField R)[X]) (β := ResidueField S)
    (⇑(aeval ((residue S : (a : S) → ResidueField S) β) :
          AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
      (a : (ResidueField R)[X]) → ResidueField S)
s : S
h : Membership.mem (γ := Submodule R S) ⊤ s
p : (ResidueField R)[X]
hp :
  Eq.{u_2 + 1} (α := ResidueField S)
    (((aeval ((residue S : (a : S) → ResidueField S) β) :
            AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
          (a : (ResidueField R)[X]) → ResidueField S)
        p :
      ResidueField S)
    ((residue S : (a : S) → ResidueField S) s : ResidueField S)
mp :
  ∀ (q : R[X])
    (hp :
      Eq.{u_2 + 1} (α := ResidueField S)
        (((aeval ((residue S : (a : S) → ResidueField S) β) :
                AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
              (a : (ResidueField R)[X]) → ResidueField S)
            (map (residue R) q) :
          ResidueField S)
        ((residue S : (a : S) → ResidueField S) s : ResidueField S)),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[β] ⊔
          HSMul.hSMul (α := Ideal R) (β := Submodule R S) (maximalIdeal R) ⊤ :
        Submodule R S)
      s
⊢ Membership.mem (γ := Submodule R S)
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[β] ⊔
        HSMul.hSMul (α := Ideal R) (β := Submodule R S) (maximalIdeal R) ⊤ :
      Submodule R S)
    s

Tactic:
obtain ⟨q, rfl⟩ := Polynomial.map_surjective _ residue_surjective p

Premises used: Polynomial.map_surjective, rfl, IsLocalRing.residue_surjective
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := (ResidueField R)[X]) (β := ResidueField S)
    (⇑(aeval ((residue S : (a : S) → ResidueField S) β) :
          AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
      (a : (ResidueField R)[X]) → ResidueField S)
s : S
h : Membership.mem (γ := Submodule R S) ⊤ s
q : R[X]
hp :
  Eq.{u_2 + 1} (α := ResidueField S)
    (((aeval ((residue S : (a : S) → ResidueField S) β) :
            AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
          (a : (ResidueField R)[X]) → ResidueField S)
        (map (residue R) q) :
      ResidueField S)
    ((residue S : (a : S) → ResidueField S) s : ResidueField S)
mp :
  Membership.mem (γ := Submodule R S)
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[β] ⊔
        Submodule.restrictScalars R (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) :
      Submodule R S)
    s
⊢ Membership.mem (γ := Submodule R S)
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[β] ⊔
        HSMul.hSMul (α := Ideal R) (β := Submodule R S) (maximalIdeal R) ⊤ :
      Submodule R S)
    s

Tactic:
rw [Ideal.smul_top_eq_map]

Premises used: Ideal.smul_top_eq_map
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := (ResidueField R)[X]) (β := ResidueField S)
    (⇑(aeval ((residue S : (a : S) → ResidueField S) β) :
          AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
      (a : (ResidueField R)[X]) → ResidueField S)
s : S
h : Membership.mem (γ := Submodule R S) ⊤ s
q : R[X]
hp :
  Eq.{u_2 + 1} (α := ResidueField S)
    (((aeval ((residue S : (a : S) → ResidueField S) β) :
            AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
          (a : (ResidueField R)[X]) → ResidueField S)
        (map (residue R) q) :
      ResidueField S)
    ((residue S : (a : S) → ResidueField S) s : ResidueField S)
⊢ HAdd.hAdd (α := S) ((aeval β : (a : R[X]) → S) q : S) (HSub.hSub (β := S) s ((aeval β : (a : R[X]) → S) q : S)) = s

Tactic:
ring
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := (ResidueField R)[X]) (β := ResidueField S)
    (⇑(aeval ((residue S : (a : S) → ResidueField S) β) :
          AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
      (a : (ResidueField R)[X]) → ResidueField S)
s : S
h : Membership.mem (γ := Submodule R S) ⊤ s
q : R[X]
hp :
  Eq.{u_2 + 1} (α := ResidueField S)
    (((aeval ((residue S : (a : S) → ResidueField S) β) :
            AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
          (a : (ResidueField R)[X]) → ResidueField S)
        (map (residue R) q) :
      ResidueField S)
    ((residue S : (a : S) → ResidueField S) s : ResidueField S)
mp :
  Membership.mem (α := S) (γ := Submodule R S)
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[β] : Submodule R S)
    ((aeval β : (a : R[X]) → S) q : S)
mp₁ :
  Membership.mem (γ := Submodule R S)
    (Submodule.restrictScalars R (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
    (HSub.hSub (β := S) s ((aeval β : (a : R[X]) → S) q : S))
⊢ Membership.mem (γ := Submodule R S)
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[β] ⊔
        Submodule.restrictScalars R (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) :
      Submodule R S)
    s

Tactic:
refine Submodule.mem_sup.mpr ⟨aeval β q, ?_, s - aeval β q, ?_, by ring⟩

Premises used: Iff.mpr, HSub.hSub, And.intro, Exists.intro, Submodule.mem_sup, Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := (ResidueField R)[X]) (β := ResidueField S)
    (⇑(aeval ((residue S : (a : S) → ResidueField S) β) :
          AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
      (a : (ResidueField R)[X]) → ResidueField S)
s : S
h : Membership.mem (γ := Submodule R S) ⊤ s
q : R[X]
hp :
  Eq.{u_2 + 1} (α := ResidueField S)
    (((aeval ((residue S : (a : S) → ResidueField S) β) :
            AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
          (a : (ResidueField R)[X]) → ResidueField S)
        (map (residue R) q) :
      ResidueField S)
    ((residue S : (a : S) → ResidueField S) s : ResidueField S)
mp :
  Membership.mem (α := S) (γ := Submodule R S)
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (AlgHom.range (aeval β)) : Submodule R S)
    ((aeval β : (a : R[X]) → S) q : S)
⊢ Membership.mem (α := S) (γ := Submodule R S)
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[β] : Submodule R S)
    ((aeval β : (a : R[X]) → S) q : S)

Tactic:
rw [adjoin_singleton_eq_range_aeval]

Premises used: Algebra.adjoin_singleton_eq_range_aeval
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := (ResidueField R)[X]) (β := ResidueField S)
    (⇑(aeval ((residue S : (a : S) → ResidueField S) β) :
          AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
      (a : (ResidueField R)[X]) → ResidueField S)
s : S
h : Membership.mem (γ := Submodule R S) ⊤ s
q : R[X]
hp :
  Eq.{u_2 + 1} (α := ResidueField S)
    (((aeval ((residue S : (a : S) → ResidueField S) β) :
            AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
          (a : (ResidueField R)[X]) → ResidueField S)
        (map (residue R) q) :
      ResidueField S)
    ((residue S : (a : S) → ResidueField S) s : ResidueField S)
⊢ Membership.mem (α := S) (γ := Submodule R S)
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (AlgHom.range (aeval β)) : Submodule R S)
    ((aeval β : (a : R[X]) → S) q : S)

Tactic:
⟨q, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.RingTheory.LocalRing.Etale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := (ResidueField R)[X]) (β := ResidueField S)
    (⇑(aeval ((residue S : (a : S) → ResidueField S) β) :
          AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
      (a : (ResidueField R)[X]) → ResidueField S)
s : S
h : Membership.mem (γ := Submodule R S) ⊤ s
q : R[X]
hp :
  Eq.{u_2 + 1} (α := ResidueField S)
    (((aeval ((residue S : (a : S) → ResidueField S) β) :
            AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
          (a : (ResidueField R)[X]) → ResidueField S)
        (map (residue R) q) :
      ResidueField S)
    ((residue S : (a : S) → ResidueField S) s : ResidueField S)
⊢ Membership.mem (α := S) (γ := Submodule R S)
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (AlgHom.range (aeval β)) : Submodule R S)
    ((aeval β : (a : R[X]) → S) q : S)

Tactic:
exact ⟨q, rfl⟩