awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Unramified.LocalRing
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'
⊢ 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
-- Module: Mathlib.RingTheory.Unramified.LocalRing
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)
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) ⋯) :
          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

Tactic:
obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq (.powers (algebraMap R S r')) x

Premises used: Algebra.algebraMap, Submonoid.powers, DFunLike.coe, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Unramified.LocalRing
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 : S
n : ℕ
y : Away r'
hy :
  Eq.{u_2 + 1} (α := 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'))
        y :
      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))
⊢ ∃ (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) ⋯) :
        Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))

Tactic:
⟨y * Localization.Away.invSelf _ ^ n, ?_⟩

Premises used: HMul.hMul, Localization.Away.invSelf, HPow.hPow, Exists.intro
-- Module: Mathlib.RingTheory.Unramified.LocalRing
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 : FaithfulSMul R S
inst_7 : q.LiesOver p
inst_8 : Algebra.IsUnramifiedAt R q
inst_9 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_10 : AtPrime.IsLiesOverAlgebra p q
H :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := p.ResidueField) (β := q.ResidueField)
    (⇑(algebraMap p.ResidueField q.ResidueField) : (a : p.ResidueField) → q.ResidueField)
⊢ Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))

Tactic:
simpa using Submodule.fg_bot

Premises used: Submodule.fg_bot
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
A : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : IsStandardEtale R A
Sf : Type u_4
inst_6 : CommRing Sf
inst_7 : Algebra R Sf
inst_8 : Algebra S Sf
inst_9 : IsScalarTower R S Sf
f : S
inst_10 : IsLocalization.Away f Sf
φ : A →ₐ[R] Sf
H : Function.Surjective.{u_2 + 1, u_4 + 1} (α := A) (β := Sf) (⇑φ : (a : A) → Sf)
P : StandardEtalePresentation R A := Nonempty.some ⋯
⊢ Function.Surjective.{u_1 + 1, u_3 + 1} (α := P.Ring) (β := Localization.Away f)
    (⇑(AlgHom.comp
          (↑(AlgEquiv.symm
                (AlgEquiv.restrictScalars R (IsLocalization.algEquiv (Submonoid.powers f) (Localization.Away f) Sf))) :
            Sf →ₐ[R] Localization.Away f)
          (φ.comp (↑P.equivRing.symm : P.Ring →ₐ[R] A))) :
      (a : P.Ring) → Localization.Away f)

Tactic:
simpa
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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
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
⊢ HasStandardEtaleSurjectionOn R g

Tactic:
obtain ⟨P, φ, hsurj⟩ := H
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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)
obtain : ∀ (g : S), HasStandardEtaleSurjectionOn R (f * g)
⊢ HasStandardEtaleSurjectionOn R g

Tactic:
obtain ⟨g, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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
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)
⊢ HasStandardEtaleSurjectionOn R (f * g)

Tactic:
obtain ⟨a, ha⟩ := hsurj (algebraMap _ _ g)

Premises used: Algebra.algebraMap, DFunLike.coe
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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)
⊢ 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) _ _ _
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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))
⊢ IsStandardEtale R (Localization.Away a)

Tactic:
have : IsStandardEtale R (Localization.Away a) := .of_isLocalizationAway a
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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_1 :
  IsLocalization.Away (f * g)
    (Localization.Away (M := Localization.Away f) ((φ : (a : P.Ring) → Localization.Away f) a : Localization.Away f))
this : IsStandardEtale R (Localization.Away a)
⊢ HasStandardEtaleSurjectionOn R (f * g)

Tactic:
.mk _ (IsLocalization.Away.mapₐ_surjective_of_surjective
    (Aₚ := Localization.Away a) (Bₚ := Localization.Away (φ a)) a hsurj)

Premises used: IsLocalization.Away.mapₐ_surjective_of_surjective, HasStandardEtaleSurjectionOn.mk
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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_1 :
  IsLocalization.Away (f * g)
    (Localization.Away (M := Localization.Away f) ((φ : (a : P.Ring) → Localization.Away f) a : Localization.Away f))
this : IsStandardEtale R (Localization.Away a)
⊢ HasStandardEtaleSurjectionOn R (f * g)

Tactic:
exact .mk _ (IsLocalization.Away.mapₐ_surjective_of_surjective
    (Aₚ := Localization.Away a) (Bₚ := Localization.Away (φ a)) a hsurj)
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S
H : HasStandardEtaleSurjectionOn R f
inst_3 : Etale.{u_1, u_3} R (Localization.Away f)
⊢ IsStandardEtale.{u_1, u_3} R (Localization.Away f)

Tactic:
.of_surjective _ H.choose_spec.choose_spec

Premises used: Exists.choose_spec, Algebra.IsStandardEtale.of_surjective
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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] ⊤
⊢ 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)
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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
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)))))
⊢ 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))))

Tactic:
rw [← RingHom.ker_comp_of_injective _ (f := e.toRingHom) e.injective]

Premises used: RingHom.ker_comp_of_injective, AlgEquiv.injective
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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))
            (RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval 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:
Ideal.mk_ker.symm

Premises used: Ideal.mk_ker, Eq.symm
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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
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))))
⊢ 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:
convert! Ideal.mk_ker.symm

Premises used: Ideal.mk_ker, Eq.symm
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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
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))
    ((algebraMap 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)) :
          (a : P.ResidueField) → P.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I)
        ((algebraMap R P.ResidueField : (a : R) → P.ResidueField) 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))
    ((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) (↑(aeval x) : R[X] →+* S))) :
          (a : P.ResidueField[X]) → P.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I)
        ((C : (a : P.ResidueField) → P.ResidueField[X]) ((algebraMap R P.ResidueField : (a : R) → P.ResidueField) 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:
simp [← Ideal.Quotient.mk_algebraMap, I]

Premises used: Ideal.Quotient.mk_algebraMap