Module: Mathlib.NumberTheory.RamificationInertia.Unramified

Goal state before:
pp: case pos
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 S T
inst✝⁸ : Algebra R T
inst✝⁷ : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst✝⁶ : P.LiesOver p
inst✝⁵ : p.IsPrime
inst✝⁴ : P.IsPrime
inst✝³ : IsUnramifiedAt R P
inst✝² : EssFiniteType R S
inst✝¹ : EssFiniteType R T
inst✝ : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this✝⁴ : P.LiesOver p₀
this✝³ : Algebra (Localization.AtPrime p₀) (Localization.AtPrime p) := Localization.AtPrime.algebraOfLiesOver p₀ p
this✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p P
this✝¹ : Algebra (Localization.AtPrime p₀) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this✝ : EssFiniteType S T
this : IsNoetherianRing T
h₁ : Algebra.IsSeparable p₀.ResidueField P.ResidueField
h₂ : Ideal.map (algebraMap R (Localization.AtPrime P)) p₀ = maximalIdeal (Localization.AtPrime P)
hp : p = ⊥
⊢ Ideal.map (algebraMap R (Localization.AtPrime p)) p₀ = maximalIdeal (Localization.AtPrime p)

pp: case neg
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 S T
inst✝⁸ : Algebra R T
inst✝⁷ : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst✝⁶ : P.LiesOver p
inst✝⁵ : p.IsPrime
inst✝⁴ : P.IsPrime
inst✝³ : IsUnramifiedAt R P
inst✝² : EssFiniteType R S
inst✝¹ : EssFiniteType R T
inst✝ : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this✝⁴ : P.LiesOver p₀
this✝³ : Algebra (Localization.AtPrime p₀) (Localization.AtPrime p) := Localization.AtPrime.algebraOfLiesOver p₀ p
this✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p P
this✝¹ : Algebra (Localization.AtPrime p₀) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this✝ : EssFiniteType S T
this : IsNoetherianRing T
h₁ : Algebra.IsSeparable p₀.ResidueField P.ResidueField
h₂ : Ideal.map (algebraMap R (Localization.AtPrime P)) p₀ = maximalIdeal (Localization.AtPrime P)
hp : ¬p = ⊥
⊢ Ideal.map (algebraMap R (Localization.AtPrime p)) p₀ = maximalIdeal (Localization.AtPrime p)

Tactic:
· have : p₀.map (algebraMap R S) = p := by
      subst hp
      exact le_bot_iff.mp (Ideal.map_comap_le)
    rw [IsScalarTower.algebraMap_eq _ S, ← Ideal.map_map, this,
      Localization.AtPrime.map_eq_maximalIdeal]

Goal state after:
case neg
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 S T
inst✝⁸ : Algebra R T
inst✝⁷ : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst✝⁶ : P.LiesOver p
inst✝⁵ : p.IsPrime
inst✝⁴ : P.IsPrime
inst✝³ : IsUnramifiedAt R P
inst✝² : EssFiniteType R S
inst✝¹ : EssFiniteType R T
inst✝ : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this✝⁴ : P.LiesOver p₀
this✝³ : Algebra (Localization.AtPrime p₀) (Localization.AtPrime p) := Localization.AtPrime.algebraOfLiesOver p₀ p
this✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p P
this✝¹ : Algebra (Localization.AtPrime p₀) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this✝ : EssFiniteType S T
this : IsNoetherianRing T
h₁ : Algebra.IsSeparable p₀.ResidueField P.ResidueField
h₂ : Ideal.map (algebraMap R (Localization.AtPrime P)) p₀ = maximalIdeal (Localization.AtPrime P)
hp : ¬p = ⊥
⊢ Ideal.map (algebraMap R (Localization.AtPrime p)) p₀ = maximalIdeal (Localization.AtPrime p)