awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
span_eq : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_5
inst_3 : (r : (↑s : Type u_1)) → AddCommMonoid (Mₚ r)
inst_4 : (r : (↑s : Type u_1)) → Module.{u_1, u_5} R (Mₚ r)
f : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ r)
inst_5 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (f r)
m : M
N : Submodule R M
h :
  ∀ (r : (↑s : Type u_1)),
    Membership.mem (α := Mₚ r) (localized₀ (Submonoid.powers (↑r : R)) (f r) N) ((f r : (a : M) → Mₚ r) m : Mₚ r)
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
ne : I ≠ ⊤
r_1 : R
hrs : r_1 ∈ s
disj : Disjoint (↑I : Set R) (↑(Submonoid.powers r_1) : Set R)
r : (↑s : Type u_1) := Subtype.mk (p := fun (x : R) ↦ x ∈ s) r_1 hrs
a : M
ha : a ∈ N
t : ↥(Submonoid.powers (↑r : R))
e :
  ∃ (s_1 : ↥(Submonoid.powers (↑r : R))),
    s_1 • t • m = s_1 • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(Submonoid.powers (↑r : R))) 1 a
u : ↥(Submonoid.powers (↑r : R))
hu : u • t • m = u • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(Submonoid.powers (↑r : R))) 1 a
⊢ False
have hu₁ : (u * t) • m = (u * 1) • a
Tactic: simp_rw [smul_smul] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
h : ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
⊢ ∃! I : Ideal R, I.IsMaximal
have rcases : ∀ (P : Ideal R) (hPunique : ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P) (hPnonzero : P ≠ ⊥)
  (hPnot_top : P ≠ ⊤), (∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P) → ∃! I : Ideal R, I.IsMaximal
Tactic: rcases h with ⟨P, ⟨hPnonzero, hPnot_top, _⟩, hPunique⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem' : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
⊢ ∃! I : Ideal R, I.IsMaximal
have refine_1 : ∀ (b : Ideal R), P < b → b = ⊤
Tactic: refine ⟨P, ⟨⟨hPnot_top, ?_⟩⟩, fun M hM => hPunique _ ⟨?_, Ideal.IsMaximal.isPrime hM⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem' : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
refine_1 : ∀ (b : Ideal R), P < b → b = ⊤
⊢ ∃! I : Ideal R, I.IsMaximal
have refine_2 : ∀ (M : Ideal R) (hM : (fun (I : Ideal R) ↦ I.IsMaximal) M), M ≠ ⊥
Tactic: refine ⟨P, ⟨⟨hPnot_top, ?_⟩⟩, fun M hM => hPunique _ ⟨?_, Ideal.IsMaximal.isPrime hM⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem' : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
⊢ ∀ (b : Ideal R), P < b → b = ⊤
have refine_1 : ∀ (M : Ideal R) (hPM : P < M) (hM : M.IsMaximal), P = M
Tactic: refine Ideal.maximal_of_no_maximal fun M hPM hM => ne_of_lt hPM ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
a b : R
h : IsUnit (a + b)
⊢ IsUnit a ∨ IsUnit b
have rcases : ∀ (u : Rˣ) (hu : (↑u : R) = a + b), IsUnit a ∨ IsUnit b
Tactic: rcases h with ⟨u, hu⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
a b : R
u : Rˣ
hu : (↑u : R) = a + b
⊢ IsUnit a ∨ IsUnit b
have hu₁ : (↑u⁻¹ : R) * a + (↑u⁻¹ : R) * b = 1
Tactic: rw [← Units.inv_mul_eq_one, mul_add] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Basic (goal)
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 a ∨ IsUnit b
have apply : IsUnit ((↑u⁻¹ : R) * a) → IsUnit a
Tactic: apply Or.imp _ _ (isUnit_or_isUnit_of_add_one hu)
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Basic (goal)
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
⊢ IsUnit a ∨ IsUnit b
have apply₁ : IsUnit ((↑u⁻¹ : R) * b) → IsUnit b
Tactic: apply Or.imp _ _ (isUnit_or_isUnit_of_add_one hu)
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Basic (goal)
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
⊢ IsUnit b ∨ IsUnit (1 - b)
have 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))
Tactic: obtain ⟨a, rfl⟩ := hf b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Basic (goal)
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.{u_2} (M := S) ((f : (a : R) → S) a : S) ∨
    IsUnit (HSub.hSub (α := S) (β := S) (1 : S) ((f : (a : R) → S) a : S))
have apply : IsUnit (1 - a) → 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 _
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Basic (goal)
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 (HSub.hSub (α := S) (β := S) (1 : S) ((f : (a : R) → S) a : S))
have rw : IsUnit (1 - a) → IsUnit.{u_2} (M := S) ((f : (a : R) → S) (1 - a) : S)
Tactic: rw [← f.map_one, ← f.map_sub]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : Field K
a : K
h : a = 0
⊢ IsUnit (1 - a)
have rw : IsUnit.{u_3} (M := K) 1
Tactic: rw [h, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
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
⊢ 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[β] ⊤
have 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[β] ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
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[β] ⊤
⊢ 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[β] ⊤
have 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)] ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
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[β] ⊤
have 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)
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 • ⊤)
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
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
⊢ 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
have 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
Tactic: rw [adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hβ
Cleared hypotheses: hβ, s, h
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
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
⊢ 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
have 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
Tactic: obtain ⟨p, hp⟩ := hβ (residue S s)
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
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)
⊢ 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
have 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
Tactic: obtain ⟨q, rfl⟩ := Polynomial.map_surjective _ residue_surjective p
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
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 (γ := 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
have 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
Tactic: rw [Ideal.smul_top_eq_map]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
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 (γ := 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
have 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)
Tactic: refine Submodule.mem_sup.mpr ⟨aeval β q, ?_, s - aeval β q, ?_, by ring⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
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)
⊢ 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
have 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))
Tactic: refine Submodule.mem_sup.mpr ⟨aeval β q, ?_, s - aeval β q, ?_, by ring⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
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) R[β] : Submodule R S)
    ((aeval β : (a : R[X]) → S) q : S)
have 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)
Tactic: rw [adjoin_singleton_eq_range_aeval]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
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 (γ := 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))
have mp : Eq (α := HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
  ((Ideal.Quotient.mk (maximalIdeal S) : (a : S) → S ⧸ maximalIdeal S) s :
    HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
  ((Ideal.Quotient.mk (maximalIdeal S) : (a : S) → S ⧸ maximalIdeal S) ((aeval β : (a : R[X]) → S) q) :
    HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
Tactic: rw [Algebra.FormallyUnramified.map_maximalIdeal, Submodule.restrictScalars_mem,
        ← Ideal.Quotient.eq]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (hypothesis)
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)
⊢ Eq (α := HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
    ((Ideal.Quotient.mk (maximalIdeal S) : (a : S) → S ⧸ maximalIdeal S) s :
      HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
    ((Ideal.Quotient.mk (maximalIdeal S) : (a : S) → S ⧸ maximalIdeal S) ((aeval β : (a : R[X]) → S) q) :
      HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
have hp₁ : Eq (α := ResidueField S) ((residue S : (a : S) → ResidueField S) ((aeval β : (a : R[X]) → S) q) : ResidueField S)
  ((residue S : (a : S) → ResidueField S) s : ResidueField S)
Tactic: rw [← map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
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β_gen : 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)] ⊤
have mpr : ∀ (hβ_gen : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑(aeval β) : (a : R[X]) → S)),
  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)
Tactic: rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at *
Cleared hypotheses: hβ_gen