-- Mathlib/FieldTheory/PolynomialGaloisGroup.lean
theorem galActionHom_injective [Fact (p.Splits (algebraMap F E))] :
    Function.Injective (galActionHom p 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)
⊢ Function.Injective ⇑(galActionHom p E)

Tactic:
rw [injective_iff_map_eq_one]

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)
⊢ ∀ (a : p.Gal), (galActionHom p E) a = 1 → a = 1

Proof state:
case h
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)
ϕ : p.Gal
hϕ : (galActionHom p E) ϕ = 1
x : p.SplittingField
hx : x ∈ p.rootSet p.SplittingField
key : (rootsEquivRoots p E) (ϕ • ⟨x, hx⟩) = (rootsEquivRoots p E) ⟨x, hx⟩
⊢ ϕ x = 1 x

Tactic:
exact Subtype.ext_iff.mp (Equiv.injective (rootsEquivRoots p E) key)

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)
ϕ : p.Gal
hϕ : (galActionHom p E) ϕ = 1
⊢ ϕ = 1

Tactic:
ext (x hx)

Result:
case h
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)
ϕ : p.Gal
hϕ : (galActionHom p E) ϕ = 1
x : p.SplittingField
hx : x ∈ p.rootSet p.SplittingField
⊢ ϕ x = 1 x

Proof state:
case h
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)
ϕ : p.Gal
hϕ : (galActionHom p E) ϕ = 1
x : p.SplittingField
hx : x ∈ p.rootSet p.SplittingField
key : ((galActionHom p E) ϕ) ((rootsEquivRoots p E) ⟨x, hx⟩) = 1 ((rootsEquivRoots p E) ⟨x, hx⟩)
⊢ ϕ x = 1 x

Tactic:
change
  rootsEquivRoots p E (ϕ • (rootsEquivRoots p E).symm (rootsEquivRoots p E ⟨x, hx⟩)) =
    rootsEquivRoots p E ⟨x, hx⟩
  at key

Result:
case h
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)
ϕ : p.Gal
hϕ : (galActionHom p E) ϕ = 1
x : p.SplittingField
hx : x ∈ p.rootSet p.SplittingField
key :
  (rootsEquivRoots p E) (ϕ • (rootsEquivRoots p E).symm ((rootsEquivRoots p E) ⟨x, hx⟩)) = (rootsEquivRoots p E) ⟨x, hx⟩
⊢ ϕ x = 1 x

Proof state:
case h
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)
ϕ : p.Gal
hϕ : (galActionHom p E) ϕ = 1
x : p.SplittingField
hx : x ∈ p.rootSet p.SplittingField
⊢ ϕ x = 1 x

Tactic:
have key := Equiv.Perm.ext_iff.mp hϕ (rootsEquivRoots p E ⟨x, hx⟩)

Result:
case h
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)
ϕ : p.Gal
hϕ : (galActionHom p E) ϕ = 1
x : p.SplittingField
hx : x ∈ p.rootSet p.SplittingField
key : ((galActionHom p E) ϕ) ((rootsEquivRoots p E) ⟨x, hx⟩) = 1 ((rootsEquivRoots p E) ⟨x, hx⟩)
⊢ ϕ x = 1 x

Proof state:
case h
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)
ϕ : p.Gal
hϕ : (galActionHom p E) ϕ = 1
x : p.SplittingField
hx : x ∈ p.rootSet p.SplittingField
key :
  (rootsEquivRoots p E) (ϕ • (rootsEquivRoots p E).symm ((rootsEquivRoots p E) ⟨x, hx⟩)) = (rootsEquivRoots p E) ⟨x, hx⟩
⊢ ϕ x = 1 x

Tactic:
rw [Equiv.symm_apply_apply] at key

Result:
case h
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)
ϕ : p.Gal
hϕ : (galActionHom p E) ϕ = 1
x : p.SplittingField
hx : x ∈ p.rootSet p.SplittingField
key : (rootsEquivRoots p E) (ϕ • ⟨x, hx⟩) = (rootsEquivRoots p E) ⟨x, hx⟩
⊢ ϕ x = 1 x

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)
⊢ ∀ (a : p.Gal), (galActionHom p E) a = 1 → a = 1

Tactic:
intro ϕ hϕ

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)
ϕ : p.Gal
hϕ : (galActionHom p E) ϕ = 1
⊢ ϕ = 1