-- Mathlib/FieldTheory/PolynomialGaloisGroup.lean
lemma galAction_isPretransitive [Fact (p.Splits (algebraMap F E))] (hp : Irreducible p) :
    MulAction.IsPretransitive p.Gal (p.rootSet E)

Proof state:
F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
hp : Irreducible p
x y : ↑(p.rootSet E)
hx : p * C p.leadingCoeff⁻¹ = minpoly F ↑((rootsEquivRoots p E).symm x)
hy : p * C p.leadingCoeff⁻¹ = minpoly F ↑((rootsEquivRoots p E).symm y)
⊢ ∃ g, g • x = y

Tactic:
obtain ⟨g, hg⟩ := (Normal.minpoly_eq_iff_mem_orbit p.SplittingField).mp (hy.symm.trans hx)

Result:
case intro
F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
hp : Irreducible p
x y : ↑(p.rootSet E)
hx : p * C p.leadingCoeff⁻¹ = minpoly F ↑((rootsEquivRoots p E).symm x)
hy : p * C p.leadingCoeff⁻¹ = minpoly F ↑((rootsEquivRoots p E).symm y)
g : p.SplittingField ≃ₐ[F] p.SplittingField
hg : (fun m => m • ↑((rootsEquivRoots p E).symm x)) g = ↑((rootsEquivRoots p E).symm y)
⊢ ∃ g, g • x = y

Proof state:
F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
hp : Irreducible p
x y : ↑(p.rootSet E)
⊢ ∃ g, g • x = y

Tactic:
have hx := minpoly.eq_of_irreducible hp (mem_rootSet.mp ((rootsEquivRoots p E).symm x).2).2

Result:
F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
hp : Irreducible p
x y : ↑(p.rootSet E)
hx : p * C p.leadingCoeff⁻¹ = minpoly F ↑((rootsEquivRoots p E).symm x)
⊢ ∃ g, g • x = y

Proof state:
case intro
F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
hp : Irreducible p
x y : ↑(p.rootSet E)
hx : p * C p.leadingCoeff⁻¹ = minpoly F ↑((rootsEquivRoots p E).symm x)
hy : p * C p.leadingCoeff⁻¹ = minpoly F ↑((rootsEquivRoots p E).symm y)
g : p.SplittingField ≃ₐ[F] p.SplittingField
hg : (fun m => m • ↑((rootsEquivRoots p E).symm x)) g = ↑((rootsEquivRoots p E).symm y)
⊢ ∃ g, g • x = y

Tactic:
exact ⟨g, (rootsEquivRoots p E).apply_eq_iff_eq_symm_apply.mpr (Subtype.ext hg)⟩

Result:
no goals

Proof state:
F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
hp : Irreducible p
x y : ↑(p.rootSet E)
hx : p * C p.leadingCoeff⁻¹ = minpoly F ↑((rootsEquivRoots p E).symm x)
⊢ ∃ g, g • x = y

Tactic:
have hy := minpoly.eq_of_irreducible hp (mem_rootSet.mp ((rootsEquivRoots p E).symm y).2).2

Result:
F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
hp : Irreducible p
x y : ↑(p.rootSet E)
hx : p * C p.leadingCoeff⁻¹ = minpoly F ↑((rootsEquivRoots p E).symm x)
hy : p * C p.leadingCoeff⁻¹ = minpoly F ↑((rootsEquivRoots p E).symm y)
⊢ ∃ g, g • x = y

Proof state:
F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
hp : Irreducible p
⊢ MulAction.IsPretransitive p.Gal ↑(p.rootSet E)

Tactic:
refine ⟨fun x y ↦ ?_⟩

Result:
F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (Splits (algebraMap F E) p)
hp : Irreducible p
x y : ↑(p.rootSet E)
⊢ ∃ g, g • x = y