awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Fact (Splits (map (algebraMap F E) p))
ϕ : p.Gal
x : (↑(p.rootSet E) : Type u_2)
⊢ ϕ • x =
    ((rootsEquivRoots p E :
          Equiv.{u_1 + 1, u_2 + 1} (↑(p.rootSet p.SplittingField) : Type u_1) (↑(p.rootSet E) : Type u_2)) :
        (a : (↑(p.rootSet p.SplittingField) : Type u_1)) → (↑(p.rootSet E) : Type u_2))
      (HSMul.hSMul (β := (↑(p.rootSet p.SplittingField) : Type u_1)) ϕ
        (((Equiv.symm (rootsEquivRoots p E) :
                Equiv.{u_2 + 1, u_1 + 1} (↑(p.rootSet E) : Type u_2) (↑(p.rootSet p.SplittingField) : Type u_1)) :
              (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet p.SplittingField) : Type u_1))
            x :
          (↑(p.rootSet p.SplittingField) : Type u_1)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p q : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Fact (Splits (map (algebraMap F E) p))
x x_1 : p.Gal
x_2 : (↑(p.rootSet E) : Type u_2)
⊢ (x * x_1) • x_2 = x • x_1 • x_2

Tactic:
simp only [smul_def, Equiv.symm_apply_apply, mul_smul]

Premises used: Polynomial.Gal.smul_def, Equiv.symm_apply_apply, SemigroupAction.mul_smul
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p q : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Fact (Splits (map (algebraMap F E) p))
x : (↑(p.rootSet E) : Type u_2)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := p.Gal) 1 x = x

Tactic:
simp only [smul_def, Equiv.apply_symm_apply, one_smul]

Premises used: Polynomial.Gal.smul_def, Equiv.apply_symm_apply, one_smul
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Fact (Splits (map (algebraMap F E) p))
hp : Irreducible p
⊢ MulAction.IsPretransitive.{u_1, u_2} p.Gal (↑(p.rootSet E) : Type u_2)

Tactic:
⟨fun x y ↦ ?_⟩

Premises used: MulAction.IsPretransitive.mk
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Fact (Splits (map (algebraMap F E) p))
hp : Irreducible p
refine : ∀ (x y : (↑(p.rootSet E) : Type u_2)), ∃ (g : p.Gal), g • x = y
⊢ MulAction.IsPretransitive.{u_1, u_2} p.Gal (↑(p.rootSet E) : Type u_2)

Tactic:
refine ⟨fun x y ↦ ?_⟩
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Fact (Splits (map (algebraMap F E) p))
hp : Irreducible p
x y : (↑(p.rootSet E) : Type u_2)
⊢ HMul.hMul (β := F[X]) p ((C : (a : F) → F[X]) p.leadingCoeff⁻¹ : F[X]) =
    minpoly F (B := p.SplittingField)
      (↑(((Equiv.symm (rootsEquivRoots p E) :
                Equiv.{u_2 + 1, u_1 + 1} (↑(p.rootSet E) : Type u_2) (↑(p.rootSet p.SplittingField) : Type u_1)) :
              (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet p.SplittingField) : Type u_1))
            x) :
        p.SplittingField)

Tactic:
have hx := minpoly.eq_of_irreducible hp (mem_rootSet.mp ((rootsEquivRoots p E).symm x).2).2
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Fact (Splits (map (algebraMap F E) p))
hp : Irreducible p
x y : (↑(p.rootSet E) : Type u_2)
hx :
  HMul.hMul (β := F[X]) p ((C : (a : F) → F[X]) p.leadingCoeff⁻¹ : F[X]) =
    minpoly F (B := p.SplittingField)
      (↑(((Equiv.symm (rootsEquivRoots p E) :
                Equiv.{u_2 + 1, u_1 + 1} (↑(p.rootSet E) : Type u_2) (↑(p.rootSet p.SplittingField) : Type u_1)) :
              (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet p.SplittingField) : Type u_1))
            x) :
        p.SplittingField)
⊢ HMul.hMul (β := F[X]) p ((C : (a : F) → F[X]) p.leadingCoeff⁻¹ : F[X]) =
    minpoly F (B := p.SplittingField)
      (↑(((Equiv.symm (rootsEquivRoots p E) :
                Equiv.{u_2 + 1, u_1 + 1} (↑(p.rootSet E) : Type u_2) (↑(p.rootSet p.SplittingField) : Type u_1)) :
              (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet p.SplittingField) : Type u_1))
            y) :
        p.SplittingField)

Tactic:
have hy := minpoly.eq_of_irreducible hp (mem_rootSet.mp ((rootsEquivRoots p E).symm y).2).2
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Fact (Splits (map (algebraMap F E) p))
hp : Irreducible p
x y : (↑(p.rootSet E) : Type u_2)
hx :
  HMul.hMul (β := F[X]) p ((C : (a : F) → F[X]) p.leadingCoeff⁻¹ : F[X]) =
    minpoly F (B := p.SplittingField)
      (↑(((Equiv.symm (rootsEquivRoots p E) :
                Equiv.{u_2 + 1, u_1 + 1} (↑(p.rootSet E) : Type u_2) (↑(p.rootSet p.SplittingField) : Type u_1)) :
              (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet p.SplittingField) : Type u_1))
            x) :
        p.SplittingField)
hy :
  HMul.hMul (β := F[X]) p ((C : (a : F) → F[X]) p.leadingCoeff⁻¹ : F[X]) =
    minpoly F (B := p.SplittingField)
      (↑(((Equiv.symm (rootsEquivRoots p E) :
                Equiv.{u_2 + 1, u_1 + 1} (↑(p.rootSet E) : Type u_2) (↑(p.rootSet p.SplittingField) : Type u_1)) :
              (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet p.SplittingField) : Type u_1))
            y) :
        p.SplittingField)
obtain :
  ∀ (g : Gal(p.SplittingField/F))
    (hg :
      Eq.{u_1 + 1} (α := p.SplittingField)
        ((fun (m : Gal(p.SplittingField/F)) ↦
            HSMul.hSMul (β := p.SplittingField) m
              (↑(((Equiv.symm (rootsEquivRoots p E) :
                        Equiv.{u_2 + 1, u_1 + 1} (↑(p.rootSet E) : Type u_2)
                          (↑(p.rootSet p.SplittingField) : Type u_1)) :
                      (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet p.SplittingField) : Type u_1))
                    x) :
                p.SplittingField))
          g)
        (↑(((Equiv.symm (rootsEquivRoots p E) :
                  Equiv.{u_2 + 1, u_1 + 1} (↑(p.rootSet E) : Type u_2) (↑(p.rootSet p.SplittingField) : Type u_1)) :
                (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet p.SplittingField) : Type u_1))
              y) :
          p.SplittingField)),
    ∃ (g : p.Gal), g • x = y
⊢ ∃ (g : p.Gal), g • x = y

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

Premises used: Normal.minpoly_eq_iff_mem_orbit, Polynomial.SplittingField, Iff.mp, Eq.symm, Eq.trans
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Fact (Splits (map (algebraMap F E) p))
hp : Irreducible p
x y : (↑(p.rootSet E) : Type u_2)
hx :
  HMul.hMul (β := F[X]) p ((C : (a : F) → F[X]) p.leadingCoeff⁻¹ : F[X]) =
    minpoly F (B := p.SplittingField)
      (↑(((Equiv.symm (rootsEquivRoots p E) :
                Equiv.{u_2 + 1, u_1 + 1} (↑(p.rootSet E) : Type u_2) (↑(p.rootSet p.SplittingField) : Type u_1)) :
              (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet p.SplittingField) : Type u_1))
            x) :
        p.SplittingField)
hy :
  HMul.hMul (β := F[X]) p ((C : (a : F) → F[X]) p.leadingCoeff⁻¹ : F[X]) =
    minpoly F (B := p.SplittingField)
      (↑(((Equiv.symm (rootsEquivRoots p E) :
                Equiv.{u_2 + 1, u_1 + 1} (↑(p.rootSet E) : Type u_2) (↑(p.rootSet p.SplittingField) : Type u_1)) :
              (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet p.SplittingField) : Type u_1))
            y) :
        p.SplittingField)
g : Gal(p.SplittingField/F)
hg :
  Eq.{u_1 + 1} (α := p.SplittingField)
    ((fun (m : Gal(p.SplittingField/F)) ↦
        HSMul.hSMul (β := p.SplittingField) m
          (↑(((Equiv.symm (rootsEquivRoots p E) :
                    Equiv.{u_2 + 1, u_1 + 1} (↑(p.rootSet E) : Type u_2) (↑(p.rootSet p.SplittingField) : Type u_1)) :
                  (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet p.SplittingField) : Type u_1))
                x) :
            p.SplittingField))
      g)
    (↑(((Equiv.symm (rootsEquivRoots p E) :
              Equiv.{u_2 + 1, u_1 + 1} (↑(p.rootSet E) : Type u_2) (↑(p.rootSet p.SplittingField) : Type u_1)) :
            (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet p.SplittingField) : Type u_1))
          y) :
      p.SplittingField)
⊢ ∃ (g : p.Gal), g • x = y

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

Premises used: Iff.mpr, Polynomial.Gal.rootsEquivRoots, Exists.intro, Subtype.ext, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Fact (Splits (map (algebraMap F E) p))
hp : Irreducible p
x y : (↑(p.rootSet E) : Type u_2)
hx :
  HMul.hMul (β := F[X]) p ((C : (a : F) → F[X]) p.leadingCoeff⁻¹ : F[X]) =
    minpoly F (B := p.SplittingField)
      (↑(((Equiv.symm (rootsEquivRoots p E) :
                Equiv.{u_2 + 1, u_1 + 1} (↑(p.rootSet E) : Type u_2) (↑(p.rootSet p.SplittingField) : Type u_1)) :
              (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet p.SplittingField) : Type u_1))
            x) :
        p.SplittingField)
hy :
  HMul.hMul (β := F[X]) p ((C : (a : F) → F[X]) p.leadingCoeff⁻¹ : F[X]) =
    minpoly F (B := p.SplittingField)
      (↑(((Equiv.symm (rootsEquivRoots p E) :
                Equiv.{u_2 + 1, u_1 + 1} (↑(p.rootSet E) : Type u_2) (↑(p.rootSet p.SplittingField) : Type u_1)) :
              (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet p.SplittingField) : Type u_1))
            y) :
        p.SplittingField)
g : Gal(p.SplittingField/F)
hg :
  Eq.{u_1 + 1} (α := p.SplittingField)
    ((fun (m : Gal(p.SplittingField/F)) ↦
        HSMul.hSMul (β := p.SplittingField) m
          (↑(((Equiv.symm (rootsEquivRoots p E) :
                    Equiv.{u_2 + 1, u_1 + 1} (↑(p.rootSet E) : Type u_2) (↑(p.rootSet p.SplittingField) : Type u_1)) :
                  (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet p.SplittingField) : Type u_1))
                x) :
            p.SplittingField))
      g)
    (↑(((Equiv.symm (rootsEquivRoots p E) :
              Equiv.{u_2 + 1, u_1 + 1} (↑(p.rootSet E) : Type u_2) (↑(p.rootSet p.SplittingField) : Type u_1)) :
            (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet p.SplittingField) : Type u_1))
          y) :
      p.SplittingField)
⊢ ∃ (g : p.Gal), g • x = y

Tactic:
exact ⟨g, (rootsEquivRoots p E).apply_eq_iff_eq_symm_apply.mpr (Subtype.ext hg)⟩
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Fact (Splits (map (algebraMap F E) p))
ϕ : Gal(E/F)
x : (↑(p.rootSet E) : Type u_2)
ψ : AlgEquiv.{u_1, u_1, u_2} F p.SplittingField
  ↥(AlgHom.range (A := p.SplittingField) (IsScalarTower.toAlgHom F p.SplittingField E)) :=
  AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)
change :
  Eq (α := E)
    ((↑((ψ : (a : p.SplittingField) → ↥(IsScalarTower.toAlgHom F p.SplittingField E).range)
            ((ψ.symm : (a : ↥(IsScalarTower.toAlgHom F p.SplittingField E).range) → p.SplittingField)
              (((↑((↑ϕ : E →ₐ[F] E).restrictNormalAux p.SplittingField) :
                    ↥(IsScalarTower.toAlgHom F p.SplittingField E).range →+*
                      ↥(IsScalarTower.toAlgHom F p.SplittingField E).range) :
                  (a : ↥(IsScalarTower.toAlgHom F p.SplittingField E).range) →
                    ↥(IsScalarTower.toAlgHom F p.SplittingField E).range)
                ((((↑(↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)) :
                            p.SplittingField →ₐ[F] ↥(IsScalarTower.toAlgHom F p.SplittingField E).range) :
                        RingHom.{u_1, u_2} p.SplittingField
                          ↥(AlgHom.range (A := p.SplittingField) (IsScalarTower.toAlgHom F p.SplittingField E))) :
                      RingHom.{u_1, u_2} p.SplittingField
                        ↥(AlgHom.range (A := p.SplittingField) (IsScalarTower.toAlgHom F p.SplittingField E))) :
                    (a : p.SplittingField) → ↥(IsScalarTower.toAlgHom F p.SplittingField E).range)
                  (↑(((Equiv.symm (rootsEquivRoots p E) :
                            Equiv.{u_2 + 1, u_1 + 1} (↑(p.rootSet E) : Type u_2)
                              (↑(p.rootSet p.SplittingField) : Type u_1)) :
                          (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet p.SplittingField) : Type u_1))
                        x) :
                    p.SplittingField))))) :
        E) :
      E)
    ((ϕ : (a : E) → E) (↑x : E) : E)
⊢ (↑(HSMul.hSMul.{u_1, u_2, u_2} (α := p.Gal)
          (((restrict p E : MonoidHom.{u_2, u_1} Gal(E/F) p.Gal) : (a : Gal(E/F)) → p.Gal) ϕ : p.Gal) x) :
      E) =
    (ϕ : (a : E) → E) (↑x : E)

Tactic:
change ↑(ψ (ψ.symm _)) = ϕ x

Premises used: AlgEquiv.symm, Subtype.val, DFunLike.coe
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Fact (Splits (map (algebraMap F E) p))
ϕ : Gal(E/F)
x : (↑(p.rootSet E) : Type u_2)
ψ : AlgEquiv.{u_1, u_1, u_2} F p.SplittingField
  ↥(AlgHom.range (A := p.SplittingField) (IsScalarTower.toAlgHom F p.SplittingField E)) :=
  AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)
change :
  Eq (α := E)
    ((ϕ : (a : E) → E)
        (↑(((rootsEquivRoots p E :
                  Equiv.{u_1 + 1, u_2 + 1} (↑(p.rootSet p.SplittingField) : Type u_1) (↑(p.rootSet E) : Type u_2)) :
                (a : (↑(p.rootSet p.SplittingField) : Type u_1)) → (↑(p.rootSet E) : Type u_2))
              (((Equiv.symm (rootsEquivRoots p E) :
                    Equiv.{u_2 + 1, u_1 + 1} (↑(p.rootSet E) : Type u_2) (↑(p.rootSet p.SplittingField) : Type u_1)) :
                  (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet p.SplittingField) : Type u_1))
                x)) :
          E) :
      E)
    ((ϕ : (a : E) → E) (↑x : E) : E)
⊢ Eq (α := E)
    ((↑(((↑((↑ϕ : E →ₐ[F] E).restrictNormalAux p.SplittingField) :
                ↥(IsScalarTower.toAlgHom F p.SplittingField E).range →+*
                  ↥(IsScalarTower.toAlgHom F p.SplittingField E).range) :
              (a : ↥(IsScalarTower.toAlgHom F p.SplittingField E).range) →
                ↥(IsScalarTower.toAlgHom F p.SplittingField E).range)
            ((((↑(↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)) :
                        p.SplittingField →ₐ[F] ↥(IsScalarTower.toAlgHom F p.SplittingField E).range) :
                    RingHom.{u_1, u_2} p.SplittingField
                      ↥(AlgHom.range (A := p.SplittingField) (IsScalarTower.toAlgHom F p.SplittingField E))) :
                  RingHom.{u_1, u_2} p.SplittingField
                    ↥(AlgHom.range (A := p.SplittingField) (IsScalarTower.toAlgHom F p.SplittingField E))) :
                (a : p.SplittingField) → ↥(IsScalarTower.toAlgHom F p.SplittingField E).range)
              (↑(((Equiv.symm (rootsEquivRoots p E) :
                        Equiv.{u_2 + 1, u_1 + 1} (↑(p.rootSet E) : Type u_2)
                          (↑(p.rootSet p.SplittingField) : Type u_1)) :
                      (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet p.SplittingField) : Type u_1))
                    x) :
                p.SplittingField))) :
        E) :
      E)
    ((ϕ : (a : E) → E) (↑x : E) : E)

Tactic:
change ϕ (rootsEquivRoots p E ((rootsEquivRoots p E).symm x)) = ϕ x

Premises used: Polynomial.Gal.rootsEquivRoots, Equiv.symm, Subtype.val, DFunLike.coe
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Fact (Splits (map (algebraMap F E) p))
ϕ : Gal(E/F)
x : (↑(p.rootSet E) : Type u_2)
ψ : AlgEquiv.{u_1, u_1, u_2} F p.SplittingField
  ↥(AlgHom.range (A := p.SplittingField) (IsScalarTower.toAlgHom F p.SplittingField E)) :=
  AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)
rw rw₁ : Eq (α := E) ((ϕ : (a : E) → E) (↑x : E) : E) ((ϕ : (a : E) → E) (↑x : E) : E)
⊢ Eq (α := E)
    ((ϕ : (a : E) → E)
        (↑(((rootsEquivRoots p E :
                  Equiv.{u_1 + 1, u_2 + 1} (↑(p.rootSet p.SplittingField) : Type u_1) (↑(p.rootSet E) : Type u_2)) :
                (a : (↑(p.rootSet p.SplittingField) : Type u_1)) → (↑(p.rootSet E) : Type u_2))
              (((Equiv.symm (rootsEquivRoots p E) :
                    Equiv.{u_2 + 1, u_1 + 1} (↑(p.rootSet E) : Type u_2) (↑(p.rootSet p.SplittingField) : Type u_1)) :
                  (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet p.SplittingField) : Type u_1))
                x)) :
          E) :
      E)
    ((ϕ : (a : E) → E) (↑x : E) : E)

Tactic:
rw [Equiv.apply_symm_apply (rootsEquivRoots p E)]

Premises used: Equiv.apply_symm_apply, Polynomial.Gal.rootsEquivRoots
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Fact (Splits (map (algebraMap F E) p))
ϕ : Gal(E/F)
x : (↑(p.rootSet E) : Type u_2)
⊢ Eq (α := E)
    ((↑(((((galActionHom p E : MonoidHom.{u_1, u_2} p.Gal (Equiv.Perm (↑(p.rootSet E) : Type u_2))) :
                    (a : p.Gal) → Equiv.Perm (↑(p.rootSet E) : Type u_2))
                  (((restrict p E : MonoidHom.{u_2, u_1} Gal(E/F) p.Gal) : (a : Gal(E/F)) → p.Gal) ϕ) :
                Equiv.Perm (↑(p.rootSet E) : Type u_2)) :
              (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet E) : Type u_2))
            x) :
        E) :
      E)
    ((ϕ : (a : E) → E) (↑x : E) : E)

Tactic:
restrict_smul ϕ x

Premises used: Polynomial.Gal.restrict_smul
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Fact (Splits (map (algebraMap F E) p))
rw :
  ∀ (a : p.Gal),
    Eq.{u_2 + 1} (α := Equiv.Perm (↑(p.rootSet E) : Type u_2))
        (((galActionHom p E : MonoidHom.{u_1, u_2} p.Gal (Equiv.Perm (↑(p.rootSet E) : Type u_2))) :
              (a : p.Gal) → Equiv.Perm (↑(p.rootSet E) : Type u_2))
            a :
          Equiv.Perm (↑(p.rootSet E) : Type u_2))
        (1 : Equiv.Perm (↑(p.rootSet E) : Type u_2)) →
      a = 1
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := p.Gal) (β := Equiv.Perm (↑(p.rootSet E) : Type u_2))
    (⇑(galActionHom p E) : (a : p.Gal) → Equiv.Perm (↑(p.rootSet E) : Type u_2))

Tactic:
rw [injective_iff_map_eq_one]

Premises used: injective_iff_map_eq_one
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Fact (Splits (map (algebraMap F E) p))
ϕ : p.Gal
hϕ :
  Eq.{u_2 + 1} (α := Equiv.Perm (↑(p.rootSet E) : Type u_2))
    (((galActionHom p E : MonoidHom.{u_1, u_2} p.Gal (Equiv.Perm (↑(p.rootSet E) : Type u_2))) :
          (a : p.Gal) → Equiv.Perm (↑(p.rootSet E) : Type u_2))
        ϕ :
      Equiv.Perm (↑(p.rootSet E) : Type u_2))
    (1 : Equiv.Perm (↑(p.rootSet E) : Type u_2))
h :
  ∀ (x : p.SplittingField) (hx : Membership.mem (γ := Set p.SplittingField) (p.rootSet p.SplittingField) x),
    Eq (α := p.SplittingField) ((ϕ : (a : p.SplittingField) → p.SplittingField) x : p.SplittingField)
      ((1 : (a : p.SplittingField) → p.SplittingField) x : p.SplittingField)
⊢ ϕ = 1

Tactic:
ext (x hx)
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Fact (Splits (map (algebraMap F E) p))
ϕ : p.Gal
hϕ :
  Eq.{u_2 + 1} (α := Equiv.Perm (↑(p.rootSet E) : Type u_2))
    (((galActionHom p E : MonoidHom.{u_1, u_2} p.Gal (Equiv.Perm (↑(p.rootSet E) : Type u_2))) :
          (a : p.Gal) → Equiv.Perm (↑(p.rootSet E) : Type u_2))
        ϕ :
      Equiv.Perm (↑(p.rootSet E) : Type u_2))
    (1 : Equiv.Perm (↑(p.rootSet E) : Type u_2))
x : p.SplittingField
hx : Membership.mem (γ := Set p.SplittingField) (p.rootSet p.SplittingField) x
⊢ Eq.{u_2 + 1} (α := (↑(p.rootSet E) : Type u_2))
    (((((galActionHom p E : MonoidHom.{u_1, u_2} p.Gal (Equiv.Perm (↑(p.rootSet E) : Type u_2))) :
                (a : p.Gal) → Equiv.Perm (↑(p.rootSet E) : Type u_2))
              ϕ :
            Equiv.Perm (↑(p.rootSet E) : Type u_2)) :
          (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet E) : Type u_2))
        (((rootsEquivRoots p E :
              Equiv.{u_1 + 1, u_2 + 1} (↑(p.rootSet p.SplittingField) : Type u_1) (↑(p.rootSet E) : Type u_2)) :
            (a : (↑(p.rootSet p.SplittingField) : Type u_1)) → (↑(p.rootSet E) : Type u_2))
          (Subtype.mk (p := fun (x : p.SplittingField) ↦
            Membership.mem (γ := Set p.SplittingField) (p.rootSet p.SplittingField) x) x hx)) :
      (↑(p.rootSet E) : Type u_2))
    ((1 : (a : (↑(p.rootSet E) : Type u_2)) → (↑(p.rootSet E) : Type u_2))
        (((rootsEquivRoots p E :
              Equiv.{u_1 + 1, u_2 + 1} (↑(p.rootSet p.SplittingField) : Type u_1) (↑(p.rootSet E) : Type u_2)) :
            (a : (↑(p.rootSet p.SplittingField) : Type u_1)) → (↑(p.rootSet E) : Type u_2))
          (Subtype.mk (p := fun (x : p.SplittingField) ↦
            Membership.mem (γ := Set p.SplittingField) (p.rootSet p.SplittingField) x) x hx)) :
      (↑(p.rootSet E) : Type u_2))

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