-- Mathlib/NumberTheory/RamificationInertia/Galois.lean
theorem ramificationIdx_eq_of_isGalois [IsGalois K L] :
    ramificationIdx (algebraMap A B) p P = ramificationIdx (algebraMap A B) 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✝ : IsGalois K L
σ : B ≃ₐ[A] B
hs : map σ P = Q
⊢ ramificationIdx (algebraMap A B) p P = ramificationIdx (algebraMap A B) p 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✝ : IsGalois K L
σ : B ≃ₐ[A] B
hs : map σ P = Q
⊢ ramificationIdx (algebraMap A B) p P = ramificationIdx (algebraMap A B) p (map σ 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 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✝ : IsGalois K L
⊢ ramificationIdx (algebraMap A B) p P = ramificationIdx (algebraMap A B) p 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✝ : IsGalois K L
σ : B ≃ₐ[A] B
hs : map σ P = Q
⊢ ramificationIdx (algebraMap A B) p P = ramificationIdx (algebraMap A B) 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✝ : IsGalois K L
σ : B ≃ₐ[A] B
hs : map σ P = Q
⊢ ramificationIdx (algebraMap A B) p P = ramificationIdx (algebraMap A B) p (map σ P)

Tactic:
exact (ramificationIdx_map_eq p P σ).symm

Result:
no goals