-- Mathlib/NumberTheory/RamificationInertia/Galois.lean
theorem ramificationIdxIn_eq_ramificationIdx [IsGalois K L] :
    ramificationIdxIn p B = ramificationIdx (algebraMap A B) 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✝ : IsGalois K L
h : ∃ P, P.IsPrime ∧ P.LiesOver p
left✝ : h.choose.IsPrime
right✝ : h.choose.LiesOver p
⊢ p.ramificationIdxIn B = ramificationIdx (algebraMap A B) p P

Tactic:
rw [ramificationIdxIn, 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✝ : IsGalois K L
h : ∃ P, P.IsPrime ∧ P.LiesOver p
left✝ : h.choose.IsPrime
right✝ : h.choose.LiesOver p
⊢ ramificationIdx (algebraMap A B) p h.choose = ramificationIdx (algebraMap A B) p 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✝ : IsGalois K L
h : ∃ P, P.IsPrime ∧ P.LiesOver p
⊢ p.ramificationIdxIn B = ramificationIdx (algebraMap A B) p 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✝ : IsGalois K L
h : ∃ P, P.IsPrime ∧ P.LiesOver p
left✝ : h.choose.IsPrime
right✝ : h.choose.LiesOver p
⊢ p.ramificationIdxIn B = ramificationIdx (algebraMap A B) p 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✝ : IsGalois K L
⊢ p.ramificationIdxIn B = ramificationIdx (algebraMap A B) p 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✝ : IsGalois K L
h : ∃ P, P.IsPrime ∧ P.LiesOver p
⊢ p.ramificationIdxIn B = ramificationIdx (algebraMap A B) 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✝ : IsGalois K L
h : ∃ P, P.IsPrime ∧ P.LiesOver p
left✝ : h.choose.IsPrime
right✝ : h.choose.LiesOver p
⊢ ramificationIdx (algebraMap A B) p h.choose = ramificationIdx (algebraMap A B) p P

Tactic:
exact ramificationIdx_eq_of_isGalois p h.choose P K L

Result:
no goals