-- Mathlib/NumberTheory/RamificationInertia/Galois.lean
theorem exists_map_eq_of_isGalois [IsGalois K L] : ∃ σ : B ≃ₐ[A] B, map σ P = Q

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
this : FaithfulSMul A B
⊢ ∃ σ, map σ P = Q

Tactic:
have : IsInvariant A B (B ≃ₐ[A] B) := isInvariant_of_isGalois' A K L B

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 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
this✝ : FaithfulSMul A B
this : IsInvariant A B (B ≃ₐ[A] B)
⊢ ∃ σ, map σ P = Q

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
⊢ ∃ σ, map σ P = Q

Tactic:
have : FaithfulSMul A B := FaithfulSMul.of_field_isFractionRing A B K L

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 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
this : FaithfulSMul A B
⊢ ∃ σ, map σ P = Q

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
this✝ : FaithfulSMul A B
this : IsInvariant A B (B ≃ₐ[A] B)
⊢ ∃ σ, map σ P = Q

Tactic:
rcases IsInvariant.exists_smul_of_under_eq A B (B ≃ₐ[A] B) P Q <|
  (over_def P p).symm.trans (over_def Q p) 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
this✝ : FaithfulSMul A B
this : IsInvariant A B (B ≃ₐ[A] B)
σ : B ≃ₐ[A] B
hs : Q = σ • P
⊢ ∃ σ, map σ 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
this✝ : FaithfulSMul A B
this : IsInvariant A B (B ≃ₐ[A] B)
σ : B ≃ₐ[A] B
hs : Q = σ • P
⊢ ∃ σ, map σ P = Q

Tactic:
exact ⟨σ, hs.symm⟩

Result:
no goals