-- Mathlib/NumberTheory/RamificationInertia/Galois.lean
theorem isPretransitive_of_isGalois [IsGalois K L] :
    MulAction.IsPretransitive (B ≃ₐ[A] B) (primesOver p B) where
  exists_smul_eq

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
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
⊢ ∀ (x y : ↑(p.primesOver B)), ∃ g, g • x = y

Tactic:
intro ⟨P, _, _⟩ ⟨Q, _, _⟩

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
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 : Ideal B
left✝¹ : P.IsPrime
right✝¹ : P.LiesOver p
Q : Ideal B
left✝ : Q.IsPrime
right✝ : Q.LiesOver p
⊢ ∃ g, g • ⟨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
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 : Ideal B
left✝¹ : P.IsPrime
right✝¹ : P.LiesOver p
Q : Ideal B
left✝ : Q.IsPrime
right✝ : Q.LiesOver p
⊢ ∃ g, g • ⟨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
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 : Ideal B
left✝¹ : P.IsPrime
right✝¹ : P.LiesOver p
Q : Ideal B
left✝ : Q.IsPrime
right✝ : Q.LiesOver p
σ : B ≃ₐ[A] B
hs : map σ P = Q
⊢ ∃ g, g • ⟨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
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 : Ideal B
left✝¹ : P.IsPrime
right✝¹ : P.LiesOver p
Q : Ideal B
left✝ : Q.IsPrime
right✝ : Q.LiesOver p
σ : B ≃ₐ[A] B
hs : map σ P = Q
⊢ ∃ g, g • ⟨P, ⋯⟩ = ⟨Q, ⋯⟩

Tactic:
exact ⟨σ, Subtype.val_inj.mp hs⟩

Result:
no goals