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

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 Q : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
hQp : Q.IsPrime
inst✝¹³ : Q.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
σ : B ≃ₐ[A] B
hs : map σ P = Q
⊢ p.inertiaDeg P = p.inertiaDeg Q

Tactic:
rw [← hs]

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 Q : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
hQp : Q.IsPrime
inst✝¹³ : Q.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
σ : B ≃ₐ[A] B
hs : map σ P = Q
⊢ p.inertiaDeg P = p.inertiaDeg (map σ 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 Q : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
hQp : Q.IsPrime
inst✝¹³ : Q.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
σ : B ≃ₐ[A] B
hs : map σ P = Q
⊢ p.inertiaDeg P = p.inertiaDeg (map σ P)

Tactic:
exact (inertiaDeg_map_eq p P σ).symm

Result:
no goals

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 Q : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
hQp : Q.IsPrime
inst✝¹³ : Q.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.inertiaDeg P = p.inertiaDeg Q

Tactic:
rcases exists_map_eq_of_isGalois p P Q K L with ⟨σ, hs⟩

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 Q : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
hQp : Q.IsPrime
inst✝¹³ : Q.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
σ : B ≃ₐ[A] B
hs : map σ P = Q
⊢ p.inertiaDeg P = p.inertiaDeg Q