awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
a b : (x : S) → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S)
r : R
hrp : r ∉ p
hr :
  ∀ (r' : R),
    r ∣ r' →
      Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
r' : R
x : S
hxs : x ∈ (↑s : Set S)
r'' : R
hr' : r' = (r * ∏ i ∈ s, b i) * r''
⊢ Eq.{u_2 + 1} (α := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
    (((IsLocalization.map (T := Submonoid.powers ((algebraMap R S : (a : R) → S) r'))
              (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S)) (algebraMap R S) ⋯ :
            RingHom.{u_1, u_2} (Away r') (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))) :
          (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
        (IsLocalization.mk' (M := Submonoid.powers r') (Away r') ((r'' * r * ∏ i ∈ s.erase x, b i) * a x)
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r') x)
            (HPow.hPow (β := ℕ) r' 1) ⋯)) :
      Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
    ((algebraMap S (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S)) :
          (a : S) → Away ((algebraMap R S : (a : R) → S) r'))
        x :
      Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
have simp : Eq (α := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
  ((algebraMap S (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S)) :
        (a : S) → Away ((algebraMap R S : (a : R) → S) r'))
      (HMul.hMul (β := S)
          (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) r'' : S) ((algebraMap R S : (a : R) → S) r : S))
          ((algebraMap R S : (a : R) → S) (∏ i ∈ s.erase x, b i) : S) *
        HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S)) :
    Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
  ((algebraMap S (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S)) :
        (a : S) → Away ((algebraMap R S : (a : R) → S) r'))
      (HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) r' : S)) :
    Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
Tactic: simp only [pow_one, IsLocalization.map_mk', IsLocalization.mk'_eq_iff_eq_mul,
      ← map_mul (algebraMap S _), map_mul (algebraMap R _), e]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
a b : (x : S) → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S)
r : R
hrp : r ∉ p
hr :
  ∀ (r' : R),
    r ∣ r' →
      Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
r' : R
x : S
hxs : x ∈ (↑s : Set S)
r'' : R
hr' : r' = (r * ∏ i ∈ s, b i) * r''
⊢ Eq (α := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
    ((algebraMap S (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S)) :
          (a : S) → Away ((algebraMap R S : (a : R) → S) r'))
        (HMul.hMul (β := S)
            (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) r'' : S)
              ((algebraMap R S : (a : R) → S) r : S))
            ((algebraMap R S : (a : R) → S) (∏ i ∈ s.erase x, b i) : S) *
          HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S)) :
      Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
    ((algebraMap S (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S)) :
          (a : S) → Away ((algebraMap R S : (a : R) → S) r'))
        (HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) r' : S)) :
      Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
have h : HMul.hMul (β := S)
      (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) r'' : S) ((algebraMap R S : (a : R) → S) r : S))
      ((algebraMap R S : (a : R) → S) (∏ i ∈ s.erase x, b i) : S) *
    HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S) =
  HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) r' : S)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
a b : (x : S) → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S)
r : R
hrp : r ∉ p
hr :
  ∀ (r' : R),
    r ∣ r' →
      Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
r' : R
x : S
hxs : x ∈ (↑s : Set S)
r'' : R
hr' : r' = (r * ∏ i ∈ s, b i) * r''
⊢ HMul.hMul (β := S)
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) r'' : S) ((algebraMap R S : (a : R) → S) r : S))
        ((algebraMap R S : (a : R) → S) (∏ i ∈ s.erase x, b i) : S) *
      HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S) =
    HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) r' : S)
have h : HMul.hMul (β := S)
      (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) r'' : S) ((algebraMap R S : (a : R) → S) r : S))
      ((algebraMap R S : (a : R) → S) (∏ i ∈ s.erase x, b i) : S) *
    HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S) =
  x *
    HMul.hMul (β := S)
      (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S)
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (∏ x ∈ s.erase x, b x) : S)
          ((algebraMap R S : (a : R) → S) (b x) : S)))
      ((algebraMap R S : (a : R) → S) r'' : S)
Tactic: rw [hr', ← Finset.prod_erase_mul s b hxs, map_mul, map_mul, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
a b : (x : S) → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S)
r : R
hrp : r ∉ p
hr :
  ∀ (r' : R),
    r ∣ r' →
      Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
r' : R
hr' : r * ∏ i ∈ s, b i ∣ r'
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
    (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
have H₁ : LE.le (α := Subalgebra R (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S)))
  (AlgHom.range (IsScalarTower.toAlgHom R S (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))))
  (AlgHom.range (awayMapₐ (Algebra.ofId R S) r'))
Tactic: have H : (IsScalarTower.toAlgHom R S _).range ≤ (awayMapₐ (Algebra.ofId R S) r').range := by
    rw [← Algebra.map_top, Subalgebra.map_le, ← hs, Algebra.adjoin_le_iff]
    intro x hxs
    obtain ⟨r'', hr'⟩ := hr'
    refine ⟨IsLocalization.mk' (M := .powers r') _
      (r'' * r * (∏ i ∈ s.erase x, b i) * a x) ⟨_, 1, rfl⟩, ?_⟩
    dsimp [awayMapₐ, IsLocalization.Away.map]
    simp only [pow_one, IsLocalization.map_mk', IsLocalization.mk'_eq_iff_eq_mul,
      ← map_mul (algebraMap S _), map_mul (algebraMap R _), e]
    congr 1
    rw [hr', ← Finset.prod_erase_mul s b hxs, map_mul, map_mul, map_mul]
    ring_nf
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H_1 :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
a b : (x : S) → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S)
r : R
hrp : r ∉ p
hr :
  ∀ (r' : R),
    r ∣ r' →
      Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
r' : R
hr' : r * ∏ i ∈ s, b i ∣ r'
H :
  LE.le (α := Subalgebra R (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S)))
    (AlgHom.range (IsScalarTower.toAlgHom R S (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))))
    (AlgHom.range (awayMapₐ (Algebra.ofId R S) r'))
x : Away (M := S) ((algebraMap R S : (a : R) → S) r' : S)
⊢ ∃ (a : Away r'),
    ((awayMap (algebraMap R S) r' :
            RingHom.{u_1, u_2} (Away r') (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))) :
          (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
        a =
      x
have obtain : ∀ (x : S) (n : ℕ),
  ∃ (a : Away r'),
    Eq (α := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
      (((awayMap (algebraMap R S) r' :
              RingHom.{u_1, u_2} (Away r') (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))) :
            (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
          a :
        Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
      (IsLocalization.mk' (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S)) x
          (Subtype.mk (p := fun (x : S) ↦
            Membership.mem (γ := Submonoid S) (Submonoid.powers ((algebraMap R S : (a : R) → S) r') : Submonoid S) x)
            ((fun (x : ℕ) ↦ HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r' : S) x) n) sorry) :
        Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
Tactic: obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq (.powers (algebraMap R S r')) x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f g : S
H : HasStandardEtaleSurjectionOn R f
h : f ∣ g
⊢ HasStandardEtaleSurjectionOn R g
have obtain : ∀ (P : StandardEtalePair R) (φ : AlgHom.{u_1, u_1, u_3} R P.Ring (Localization.Away f))
  (hsurj :
    Function.Surjective.{u_1 + 1, u_3 + 1} (α := P.Ring) (β := Localization.Away f)
      (⇑φ : (a : P.Ring) → Localization.Away f)),
  HasStandardEtaleSurjectionOn R g
Tactic: obtain ⟨P, φ, hsurj⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f g : S
h : f ∣ g
P : StandardEtalePair R
φ : AlgHom.{u_1, u_1, u_3} R P.Ring (Localization.Away f)
hsurj :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := P.Ring) (β := Localization.Away f)
    (⇑φ : (a : P.Ring) → Localization.Away f)
⊢ HasStandardEtaleSurjectionOn R g
have obtain : ∀ (g : S), HasStandardEtaleSurjectionOn R (f * g)
Tactic: obtain ⟨g, rfl⟩ := h
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S
P : StandardEtalePair R
φ : AlgHom.{u_1, u_1, u_3} R P.Ring (Localization.Away f)
hsurj :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := P.Ring) (β := Localization.Away f)
    (⇑φ : (a : P.Ring) → Localization.Away f)
g : S
⊢ HasStandardEtaleSurjectionOn R (f * g)
have obtain : ∀ (a : P.Ring)
  (ha :
    Eq.{u_3 + 1} (α := Localization.Away f) ((φ : (a : P.Ring) → Localization.Away f) a : Localization.Away f)
      ((algebraMap S (Localization.Away f) : (a : S) → Localization.Away f) g : Localization.Away f)),
  HasStandardEtaleSurjectionOn R (f * g)
Tactic: obtain ⟨a, ha⟩ := hsurj (algebraMap _ _ g)
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (hypothesis)
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S
P : StandardEtalePair R
φ : AlgHom.{u_1, u_1, u_3} R P.Ring (Localization.Away f)
hsurj :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := P.Ring) (β := Localization.Away f)
    (⇑φ : (a : P.Ring) → Localization.Away f)
g : S
a : P.Ring
ha :
  Eq.{u_3 + 1} (α := Localization.Away f) ((φ : (a : P.Ring) → Localization.Away f) a : Localization.Away f)
    ((algebraMap S (Localization.Away f) : (a : S) → Localization.Away f) g : Localization.Away f)
⊢ HasStandardEtaleSurjectionOn R (f * g)
have this : IsLocalization.Away (f * g)
  (Localization.Away (M := Localization.Away f) ((φ : (a : P.Ring) → Localization.Away f) a : Localization.Away f))
Tactic: have : IsLocalization.Away (f * g) (Localization.Away (φ a)) :=
    ha ▸ .mul' (Localization.Away f) _ _ _
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (hypothesis)
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S
P : StandardEtalePair R
φ : AlgHom.{u_1, u_1, u_3} R P.Ring (Localization.Away f)
hsurj :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := P.Ring) (β := Localization.Away f)
    (⇑φ : (a : P.Ring) → Localization.Away f)
g : S
a : P.Ring
ha :
  Eq.{u_3 + 1} (α := Localization.Away f) ((φ : (a : P.Ring) → Localization.Away f) a : Localization.Away f)
    ((algebraMap S (Localization.Away f) : (a : S) → Localization.Away f) g : Localization.Away f)
this :
  IsLocalization.Away (f * g)
    (Localization.Away (M := Localization.Away f) ((φ : (a : P.Ring) → Localization.Away f) a : Localization.Away f))
⊢ HasStandardEtaleSurjectionOn R (f * g)
have this₁ : IsStandardEtale R (Localization.Away a)
Tactic: have : IsStandardEtale R (Localization.Away a) := .of_isLocalizationAway a
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (hypothesis)
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Ideal R
inst_3 : P.IsPrime
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
⊢ Eq (α := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField))
      (RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))))
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
have hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
Tactic: have hx' : Function.Surjective (aeval (R := R) x) :=
    (AlgHom.range_eq_top _).mp ((adjoin_singleton_eq_range_aeval R x).symm.trans hx)
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Ideal R
inst_3 : P.IsPrime
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
e : P.Fiber S ≃ₐ[P.ResidueField]
  HasQuotient.Quotient P.ResidueField[X] (B := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I) :=
  fiberEquivQuotient (aeval x) hx' P
⊢ Eq (α := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField))
      (RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))))
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
have rw : Eq (α := Ideal P.ResidueField[X])
  (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField))
    (RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))))
  (RingHom.ker (F :=
    P.ResidueField[X] →+*
      HasQuotient.Quotient P.ResidueField[X] (B := Ideal P.ResidueField[X])
        (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I))
    (e.toRingEquiv.toRingHom.comp (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x)))))
Tactic: rw [← RingHom.ker_comp_of_injective _ (f := e.toRingHom) e.injective]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Ideal R
inst_3 : P.IsPrime
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
e : P.Fiber S ≃ₐ[P.ResidueField]
  HasQuotient.Quotient P.ResidueField[X] (B := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I) :=
  fiberEquivQuotient (aeval x) hx' P
⊢ Eq (α := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField))
      (RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))))
    (RingHom.ker (F :=
      P.ResidueField[X] →+*
        HasQuotient.Quotient P.ResidueField[X] (B := Ideal P.ResidueField[X])
          (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I))
      (e.toRingEquiv.toRingHom.comp (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x)))))
have h : e.toRingEquiv.toRingHom.comp (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))) =
  Ideal.Quotient.mk
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField))
      (RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))))
Tactic: convert! Ideal.mk_ker.symm
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Ideal R
inst_3 : P.IsPrime
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
e : P.Fiber S ≃ₐ[P.ResidueField]
  HasQuotient.Quotient P.ResidueField[X] (B := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I) :=
  fiberEquivQuotient (aeval x) hx' P
⊢ e.toRingEquiv.toRingHom.comp (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))) =
    Ideal.Quotient.mk
      (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField))
        (RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))))
have h : ∀ (a : R),
  Eq (α :=
    HasQuotient.Quotient P.ResidueField[X] (B := Ideal P.ResidueField[X])
      (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I))
    ((@RingHom.comp _ P.ResidueField _ _ Semiring.toNonAssocSemiring _
            (RingHom.comp (e.toRingEquiv.toRingHom.comp (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x)))) C)
            (algebraMap R P.ResidueField) :
          (a : R) → P.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I)
        a :
      HasQuotient.Quotient P.ResidueField[X] (B := Ideal P.ResidueField[X])
        (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I))
    ((@RingHom.comp _ P.ResidueField _ _ Semiring.toNonAssocSemiring _
            (RingHom.comp
              (Ideal.Quotient.mk
                (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField))
                  (RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x)))))
              C)
            (algebraMap R P.ResidueField) :
          (a : R) → P.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I)
        a :
      HasQuotient.Quotient P.ResidueField[X] (B := Ideal P.ResidueField[X])
        (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I))
Tactic: ext a
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (hypothesis)
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Ideal R
inst_3 : P.IsPrime
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : Q.LiesOver P
inst_6 : IsUnramifiedAt R Q
x : S
p : R[X]
inst_7 : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
hp₂ : Eq (α := Subalgebra R S) R[x] ⊤
Q' : Ideal (P.Fiber S) :=
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.primesOverOrderIsoFiber R S P : (a : (↑(P.primesOver S) : Type u_3)) → PrimeSpectrum (P.Fiber S))
      (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯))
⊢ ¬HPow.hPow (α := P.ResidueField[X]) (β := ℕ)
        (minpoly P.ResidueField (B := Q.ResidueField)
          ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x : Q.ResidueField))
        2 ∣
      Polynomial.map (algebraMap R P.ResidueField) p
have this : Q'.LiesOver Q
Tactic: have : Q'.LiesOver Q := ⟨congr($((PrimeSpectrum.primesOverOrderIsoFiber R S P).symm_apply_apply
    ⟨Q, ‹_›, ‹_›⟩).1).symm⟩