mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
ε : S
hεI : ε ∈ I
b : S
hb : (aeval x) (derivative P.f) * b = 1 + ε
this✝ : (aeval x) P.f ^ 2 = 0
this : (aeval x) P.f * ε = 0
⊢ IsUnit ((aeval (x + (aeval x) P.f * -b)) P.g)

pp: case refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
ε : S
hεI : ε ∈ I
b : S
hb : (aeval x) (derivative P.f) * b = 1 + ε
this✝ : (aeval x) P.f ^ 2 = 0
this : (aeval x) P.f * ε = 0
⊢ ∀ (y : S), (fun ε ↦ ε ∈ I ∧ P.HasMap (x + ε)) y → y = (aeval x) P.f * -b

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
ε : S
hεI : ε ∈ I
b : S
hb : (aeval x) (derivative P.f) * b = 1 + ε
this✝ : (aeval x) P.f ^ 2 = 0
this : (aeval x) P.f * ε = 0
⊢ IsUnit ((aeval (x + (aeval x) P.f * -b)) P.g)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case hb
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) x.denom ≠ 0

pp: case hd
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) y.denom ≠ 0

Tactic:
·

Goal state after:
case hb
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) x.denom ≠ 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case hd
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) y.denom ≠ 0

Tactic:
·

Goal state after:
case hd
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) y.denom ≠ 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case mp
K : Type u
inst✝ : Field K
x : K⟮X⟯
p : K[X]
hp : p ≠ 0
⊢ x.num ∣ p → ∃ q, q ≠ 0 ∧ x = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q

pp: case mpr
K : Type u
inst✝ : Field K
x : K⟮X⟯
p : K[X]
hp : p ≠ 0
⊢ (∃ q, q ≠ 0 ∧ x = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) → x.num ∣ p

Tactic:
·

Goal state after:
case mp
K : Type u
inst✝ : Field K
x : K⟮X⟯
p : K[X]
hp : p ≠ 0
⊢ x.num ∣ p → ∃ q, q ≠ 0 ∧ x = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case h
K : Type u
inst✝ : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ x.denom * q ≠ 0 ∧ x = x

pp: case h
K : Type u
inst✝ : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) q ≠ 0

Tactic:
·

Goal state after:
case h
K : Type u
inst✝ : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ x.denom * q ≠ 0 ∧ x = x
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case h
K : Type u
inst✝ : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) q ≠ 0

Tactic:
·

Goal state after:
case h
K : Type u
inst✝ : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) q ≠ 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case mpr
K : Type u
inst✝ : Field K
x : K⟮X⟯
p : K[X]
hp : p ≠ 0
⊢ (∃ q, q ≠ 0 ∧ x = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) → x.num ∣ p

Tactic:
·

Goal state after:
case mpr
K : Type u
inst✝ : Field K
x : K⟮X⟯
p : K[X]
hp : p ≠ 0
⊢ (∃ q, q ≠ 0 ∧ x = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) → x.num ∣ p
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
ε : S
hεI : ε ∈ I
b : S
hb : (aeval x) (derivative P.f) * b = 1 + ε
this✝ : (aeval x) P.f ^ 2 = 0
this : (aeval x) P.f * ε = 0
⊢ ∀ (y : S), (fun ε ↦ ε ∈ I ∧ P.HasMap (x + ε)) y → y = (aeval x) P.f * -b

Tactic:
·

Goal state after:
case refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
ε : S
hεI : ε ∈ I
b : S
hb : (aeval x) (derivative P.f) * b = 1 + ε
this✝ : (aeval x) P.f ^ 2 = 0
this : (aeval x) P.f * ε = 0
⊢ ∀ (y : S), (fun ε ↦ ε ∈ I ∧ P.HasMap (x + ε)) y → y = (aeval x) P.f * -b
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case mp
K : Type u
inst✝ : Field K
x : K⟮X⟯
q : K[X]
hq : q ≠ 0
⊢ x.denom ∣ q → ∃ p, x = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q

pp: case mpr
K : Type u
inst✝ : Field K
x : K⟮X⟯
q : K[X]
hq : q ≠ 0
⊢ (∃ p, x = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) → x.denom ∣ q

Tactic:
·

Goal state after:
case mp
K : Type u
inst✝ : Field K
x : K⟮X⟯
q : K[X]
hq : q ≠ 0
⊢ x.denom ∣ q → ∃ p, x = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case mpr
K : Type u
inst✝ : Field K
x : K⟮X⟯
q : K[X]
hq : q ≠ 0
⊢ (∃ p, x = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) → x.denom ∣ q

Tactic:
·

Goal state after:
case mpr
K : Type u
inst✝ : Field K
x : K⟮X⟯
q : K[X]
hq : q ≠ 0
⊢ (∃ p, x = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) → x.denom ∣ q
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case pos
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : x = 0
⊢ (x * y).num ∣ x.num * y.num

pp: case neg
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : ¬x = 0
⊢ (x * y).num ∣ x.num * y.num

Tactic:
·

Goal state after:
case pos
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : x = 0
⊢ (x * y).num ∣ x.num * y.num
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case pos
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : ¬x = 0
hy : y = 0
⊢ (x * y).num ∣ x.num * y.num

pp: case neg
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : ¬x = 0
hy : ¬y = 0
⊢ (x * y).num ∣ x.num * y.num

Tactic:
·

Goal state after:
case pos
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : ¬x = 0
hy : y = 0
⊢ (x * y).num ∣ x.num * y.num
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (aeval ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f))) P.f = 0

pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ IsUnit
    ((aeval ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f))) P.g)

pp: case refine_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (P.lift ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f)) ⋯).comp
      (IsLocalization.Away.liftAlgHom ((AdjoinRoot.mk P.f) P.g) ⋯) =
    AlgHom.id R (Localization.Away ((AdjoinRoot.mk P.f) P.g))

pp: case refine_4
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (IsLocalization.Away.liftAlgHom ((AdjoinRoot.mk P.f) P.g) ⋯).comp
      (P.lift ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f)) ⋯) =
    AlgHom.id R P.Ring

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (aeval ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f))) P.f = 0
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ IsUnit
    ((aeval ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f))) P.g)

pp: case refine_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (P.lift ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f)) ⋯).comp
      (IsLocalization.Away.liftAlgHom ((AdjoinRoot.mk P.f) P.g) ⋯) =
    AlgHom.id R (Localization.Away ((AdjoinRoot.mk P.f) P.g))

pp: case refine_4
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (IsLocalization.Away.liftAlgHom ((AdjoinRoot.mk P.f) P.g) ⋯).comp
      (P.lift ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f)) ⋯) =
    AlgHom.id R P.Ring

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ IsUnit
    ((aeval ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f))) P.g)
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (P.lift ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f)) ⋯).comp
      (IsLocalization.Away.liftAlgHom ((AdjoinRoot.mk P.f) P.g) ⋯) =
    AlgHom.id R (Localization.Away ((AdjoinRoot.mk P.f) P.g))

pp: case refine_4
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (IsLocalization.Away.liftAlgHom ((AdjoinRoot.mk P.f) P.g) ⋯).comp
      (P.lift ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f)) ⋯) =
    AlgHom.id R P.Ring

Tactic:
·

Goal state after:
case refine_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (P.lift ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f)) ⋯).comp
      (IsLocalization.Away.liftAlgHom ((AdjoinRoot.mk P.f) P.g) ⋯) =
    AlgHom.id R (Localization.Away ((AdjoinRoot.mk P.f) P.g))
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_4
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (IsLocalization.Away.liftAlgHom ((AdjoinRoot.mk P.f) P.g) ⋯).comp
      (P.lift ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f)) ⋯) =
    AlgHom.id R P.Ring

Tactic:
·

Goal state after:
case refine_4
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (IsLocalization.Away.liftAlgHom ((AdjoinRoot.mk P.f) P.g) ⋯).comp
      (P.lift ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f)) ⋯) =
    AlgHom.id R P.Ring
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (aeval ((algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})) X))
      P.f =
    0

pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ IsUnit
    ((aeval ((algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})) X))
      P.g)

pp: case refine_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ ∀ a ∈ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f}, (IsLocalization.Away.liftAlgHom P.g ⋯) a = 0

pp: case refine_4
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (P.lift ((algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})) X)
          ⋯).comp
      (Ideal.Quotient.liftₐ (Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})
        (IsLocalization.Away.liftAlgHom P.g ⋯) ?refine_3) =
    AlgHom.id R (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})

pp: case refine_5
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (Ideal.Quotient.liftₐ (Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})
          (IsLocalization.Away.liftAlgHom P.g ⋯) ?refine_3).comp
      (P.lift ((algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})) X)
        ⋯) =
    AlgHom.id R P.Ring

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (aeval ((algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})) X))
      P.f =
    0
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ IsUnit
    ((aeval ((algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})) X))
      P.g)

pp: case refine_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ ∀ a ∈ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f}, (IsLocalization.Away.liftAlgHom P.g ⋯) a = 0

pp: case refine_4
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (P.lift ((algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})) X)
          ⋯).comp
      (Ideal.Quotient.liftₐ (Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})
        (IsLocalization.Away.liftAlgHom P.g ⋯) ?refine_3) =
    AlgHom.id R (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})

pp: case refine_5
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (Ideal.Quotient.liftₐ (Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})
          (IsLocalization.Away.liftAlgHom P.g ⋯) ?refine_3).comp
      (P.lift ((algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})) X)
        ⋯) =
    AlgHom.id R P.Ring

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ IsUnit
    ((aeval ((algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})) X))
      P.g)
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ ∀ a ∈ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f}, (IsLocalization.Away.liftAlgHom P.g ⋯) a = 0

pp: case refine_4
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (P.lift ((algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})) X)
          ⋯).comp
      (Ideal.Quotient.liftₐ (Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})
        (IsLocalization.Away.liftAlgHom P.g ⋯) ?refine_3) =
    AlgHom.id R (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})

pp: case refine_5
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (Ideal.Quotient.liftₐ (Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})
          (IsLocalization.Away.liftAlgHom P.g ⋯) ?refine_3).comp
      (P.lift ((algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})) X)
        ⋯) =
    AlgHom.id R P.Ring

Tactic:
·

Goal state after:
case refine_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ ∀ a ∈ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f}, (IsLocalization.Away.liftAlgHom P.g ⋯) a = 0
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case e'_3.e'_8.h₁
R : Type u_1
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
x : S
hx : R[x] = ⊤
hx' : Function.Surjective ⇑(aeval x)
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
e : P.Fiber S ≃ₐ[P.ResidueField] P.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I :=
  fiberEquivQuotient (aeval x) hx' P
a : R
⊢ (((e.toRingEquiv.toRingHom.comp (aeval (1 ⊗ₜ[R] x)).toRingHom).comp C).comp (algebraMap R P.ResidueField)) a =
    (((Ideal.Quotient.mk (Ideal.map (mapRingHom (algebraMap R P.ResidueField)) (RingHom.ker (aeval x).toRingHom))).comp
            C).comp
        (algebraMap R P.ResidueField))
      a

pp: case h₂
R : Type u_1
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
x : S
hx : R[x] = ⊤
hx' : Function.Surjective ⇑(aeval x)
I : Ideal R[X] := ⋯
e : P.Fiber S ≃ₐ[P.ResidueField] P.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I := ⋯
⊢ (e.toRingEquiv.toRingHom.comp (aeval (1 ⊗ₜ[R] x)).toRingHom) X =
    (Ideal.Quotient.mk (Ideal.map (mapRingHom (algebraMap R P.ResidueField)) (RingHom.ker (aeval x).toRingHom))) X

Tactic:
·

Goal state after:
case e'_3.e'_8.h₁
R : Type u_1
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
x : S
hx : R[x] = ⊤
hx' : Function.Surjective ⇑(aeval x)
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
e : P.Fiber S ≃ₐ[P.ResidueField] P.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I :=
  fiberEquivQuotient (aeval x) hx' P
a : R
⊢ (((e.toRingEquiv.toRingHom.comp (aeval (1 ⊗ₜ[R] x)).toRingHom).comp C).comp (algebraMap R P.ResidueField)) a =
    (((Ideal.Quotient.mk (Ideal.map (mapRingHom (algebraMap R P.ResidueField)) (RingHom.ker (aeval x).toRingHom))).comp
            C).comp
        (algebraMap R P.ResidueField))
      a
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_4
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (P.lift ((algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})) X)
          ⋯).comp
      (Ideal.Quotient.liftₐ (Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})
        (IsLocalization.Away.liftAlgHom P.g ⋯) ⋯) =
    AlgHom.id R (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})

pp: case refine_5
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (Ideal.Quotient.liftₐ (Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})
          (IsLocalization.Away.liftAlgHom P.g ⋯) ⋯).comp
      (P.lift ((algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})) X)
        ⋯) =
    AlgHom.id R P.Ring

Tactic:
·

Goal state after:
case refine_4
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (P.lift ((algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})) X)
          ⋯).comp
      (Ideal.Quotient.liftₐ (Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})
        (IsLocalization.Away.liftAlgHom P.g ⋯) ⋯) =
    AlgHom.id R (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_5
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (Ideal.Quotient.liftₐ (Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})
          (IsLocalization.Away.liftAlgHom P.g ⋯) ⋯).comp
      (P.lift ((algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})) X)
        ⋯) =
    AlgHom.id R P.Ring

Tactic:
·

Goal state after:
case refine_5
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (Ideal.Quotient.liftₐ (Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})
          (IsLocalization.Away.liftAlgHom P.g ⋯) ⋯).comp
      (P.lift ((algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})) X)
        ⋯) =
    AlgHom.id R P.Ring