-- Mathlib/NumberTheory/RamificationInertia/Galois.lean
theorem inertiaDegIn_eq_inertiaDeg [p.IsMaximal] [IsGalois K L] :
    inertiaDegIn p B = inertiaDeg p P

Proof state:
case intro
A : Type u_1
B : Type u_2
inst✝²⁰ : CommRing A
inst✝¹⁹ : IsDomain A
inst✝¹⁸ : IsIntegrallyClosed A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : IsDomain B
inst✝¹⁵ : IsIntegrallyClosed B
inst✝¹⁴ : Algebra A B
inst✝¹³ : Module.Finite A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
K : Type u_3
L : Type u_4
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra A K
inst✝⁹ : IsFractionRing A K
inst✝⁸ : Algebra B L
inst✝⁷ : IsFractionRing B L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : FiniteDimensional K L
inst✝¹ : p.IsMaximal
inst✝ : IsGalois K L
h : ∃ P, P.IsPrime ∧ P.LiesOver p
left✝ : h.choose.IsPrime
right✝ : h.choose.LiesOver p
⊢ p.inertiaDegIn B = p.inertiaDeg P

Tactic:
rw [inertiaDegIn, dif_pos h]

Result:
case intro
A : Type u_1
B : Type u_2
inst✝²⁰ : CommRing A
inst✝¹⁹ : IsDomain A
inst✝¹⁸ : IsIntegrallyClosed A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : IsDomain B
inst✝¹⁵ : IsIntegrallyClosed B
inst✝¹⁴ : Algebra A B
inst✝¹³ : Module.Finite A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
K : Type u_3
L : Type u_4
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra A K
inst✝⁹ : IsFractionRing A K
inst✝⁸ : Algebra B L
inst✝⁷ : IsFractionRing B L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : FiniteDimensional K L
inst✝¹ : p.IsMaximal
inst✝ : IsGalois K L
h : ∃ P, P.IsPrime ∧ P.LiesOver p
left✝ : h.choose.IsPrime
right✝ : h.choose.LiesOver p
⊢ p.inertiaDeg h.choose = p.inertiaDeg P

Proof state:
A : Type u_1
B : Type u_2
inst✝²⁰ : CommRing A
inst✝¹⁹ : IsDomain A
inst✝¹⁸ : IsIntegrallyClosed A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : IsDomain B
inst✝¹⁵ : IsIntegrallyClosed B
inst✝¹⁴ : Algebra A B
inst✝¹³ : Module.Finite A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
K : Type u_3
L : Type u_4
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra A K
inst✝⁹ : IsFractionRing A K
inst✝⁸ : Algebra B L
inst✝⁷ : IsFractionRing B L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : FiniteDimensional K L
inst✝¹ : p.IsMaximal
inst✝ : IsGalois K L
h : ∃ P, P.IsPrime ∧ P.LiesOver p
⊢ p.inertiaDegIn B = p.inertiaDeg P

Tactic:
obtain ⟨_, _⟩ := h.choose_spec

Result:
case intro
A : Type u_1
B : Type u_2
inst✝²⁰ : CommRing A
inst✝¹⁹ : IsDomain A
inst✝¹⁸ : IsIntegrallyClosed A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : IsDomain B
inst✝¹⁵ : IsIntegrallyClosed B
inst✝¹⁴ : Algebra A B
inst✝¹³ : Module.Finite A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
K : Type u_3
L : Type u_4
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra A K
inst✝⁹ : IsFractionRing A K
inst✝⁸ : Algebra B L
inst✝⁷ : IsFractionRing B L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : FiniteDimensional K L
inst✝¹ : p.IsMaximal
inst✝ : IsGalois K L
h : ∃ P, P.IsPrime ∧ P.LiesOver p
left✝ : h.choose.IsPrime
right✝ : h.choose.LiesOver p
⊢ p.inertiaDegIn B = p.inertiaDeg P

Proof state:
A : Type u_1
B : Type u_2
inst✝²⁰ : CommRing A
inst✝¹⁹ : IsDomain A
inst✝¹⁸ : IsIntegrallyClosed A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : IsDomain B
inst✝¹⁵ : IsIntegrallyClosed B
inst✝¹⁴ : Algebra A B
inst✝¹³ : Module.Finite A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
K : Type u_3
L : Type u_4
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra A K
inst✝⁹ : IsFractionRing A K
inst✝⁸ : Algebra B L
inst✝⁷ : IsFractionRing B L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : FiniteDimensional K L
inst✝¹ : p.IsMaximal
inst✝ : IsGalois K L
⊢ p.inertiaDegIn B = p.inertiaDeg P

Tactic:
have h : ∃ P : Ideal B, P.IsPrime ∧ P.LiesOver p := ⟨P, hPp, hp⟩

Result:
A : Type u_1
B : Type u_2
inst✝²⁰ : CommRing A
inst✝¹⁹ : IsDomain A
inst✝¹⁸ : IsIntegrallyClosed A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : IsDomain B
inst✝¹⁵ : IsIntegrallyClosed B
inst✝¹⁴ : Algebra A B
inst✝¹³ : Module.Finite A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
K : Type u_3
L : Type u_4
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra A K
inst✝⁹ : IsFractionRing A K
inst✝⁸ : Algebra B L
inst✝⁷ : IsFractionRing B L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : FiniteDimensional K L
inst✝¹ : p.IsMaximal
inst✝ : IsGalois K L
h : ∃ P, P.IsPrime ∧ P.LiesOver p
⊢ p.inertiaDegIn B = p.inertiaDeg P

Proof state:
case intro
A : Type u_1
B : Type u_2
inst✝²⁰ : CommRing A
inst✝¹⁹ : IsDomain A
inst✝¹⁸ : IsIntegrallyClosed A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : IsDomain B
inst✝¹⁵ : IsIntegrallyClosed B
inst✝¹⁴ : Algebra A B
inst✝¹³ : Module.Finite A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
K : Type u_3
L : Type u_4
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra A K
inst✝⁹ : IsFractionRing A K
inst✝⁸ : Algebra B L
inst✝⁷ : IsFractionRing B L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : FiniteDimensional K L
inst✝¹ : p.IsMaximal
inst✝ : IsGalois K L
h : ∃ P, P.IsPrime ∧ P.LiesOver p
left✝ : h.choose.IsPrime
right✝ : h.choose.LiesOver p
⊢ p.inertiaDeg h.choose = p.inertiaDeg P

Tactic:
exact inertiaDeg_eq_of_isGalois p h.choose P K L

Result:
no goals