awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p : F[X]
σ τ : p.Gal
h :
  ∀ (x : p.SplittingField),
    Membership.mem (γ := Set p.SplittingField) (p.rootSet p.SplittingField) x →
      Eq (α := p.SplittingField) ((σ : (a : p.SplittingField) → p.SplittingField) x : p.SplittingField)
        ((τ : (a : p.SplittingField) → p.SplittingField) x : p.SplittingField)
x : p.SplittingField
rwa :
  LE.le (α := Subalgebra F p.SplittingField) ⊤
    (AlgHom.equalizer (↑σ : p.SplittingField →ₐ[F] p.SplittingField) (↑τ : p.SplittingField →ₐ[F] p.SplittingField))
rwa₁ :
  LE.le (α := Subalgebra F p.SplittingField) (Algebra.adjoin F (p.rootSet p.SplittingField))
    (AlgHom.equalizer (↑σ : p.SplittingField →ₐ[F] p.SplittingField) (↑τ : p.SplittingField →ₐ[F] p.SplittingField))
⊢ Eq (α := Subalgebra F p.SplittingField)
    (AlgHom.equalizer (↑σ : p.SplittingField →ₐ[F] p.SplittingField) (↑τ : p.SplittingField →ₐ[F] p.SplittingField)) ⊤
have rwa₂ : p.rootSet p.SplittingField ⊆
  (↑(AlgHom.equalizer (↑σ : p.SplittingField →ₐ[F] p.SplittingField) (↑τ : p.SplittingField →ₐ[F] p.SplittingField)) :
    Set p.SplittingField)
Tactic: rwa [eq_top_iff, ← SplittingField.adjoin_rootSet, Algebra.adjoin_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
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
h : p.Splits
f : p.Gal
x : p.SplittingField
⊢ Eq (α := p.SplittingField) ((f : (a : p.SplittingField) → p.SplittingField) x : p.SplittingField)
    ((1 : (a : p.SplittingField) → p.SplittingField) x : p.SplittingField)
have obtain : ∀ (y : F),
  Eq (α := p.SplittingField)
    ((f : (a : p.SplittingField) → p.SplittingField) ((algebraMap F p.SplittingField : (a : F) → p.SplittingField) y) :
      p.SplittingField)
    ((1 : (a : p.SplittingField) → p.SplittingField) ((algebraMap F p.SplittingField : (a : F) → p.SplittingField) y) :
      p.SplittingField)
Tactic: obtain ⟨y, rfl⟩ :=
        Algebra.mem_bot.mp
          ((SetLike.ext_iff.mp ((IsSplittingField.splits_iff _ p).mp h) x).mp Algebra.mem_top)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
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
h : p.Splits
f : p.Gal
y : F
⊢ Eq (α := p.SplittingField)
    ((f : (a : p.SplittingField) → p.SplittingField) ((algebraMap F p.SplittingField : (a : F) → p.SplittingField) y) :
      p.SplittingField)
    ((1 : (a : p.SplittingField) → p.SplittingField) ((algebraMap F p.SplittingField : (a : F) → p.SplittingField) y) :
      p.SplittingField)
have rw : Eq (α := p.SplittingField) ((algebraMap F p.SplittingField : (a : F) → p.SplittingField) y : p.SplittingField)
  ((1 : (a : p.SplittingField) → p.SplittingField) ((algebraMap F p.SplittingField : (a : F) → p.SplittingField) y) :
    p.SplittingField)
Tactic: rw [AlgEquiv.commutes, AlgEquiv.commutes]
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
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
h : p.Splits
f : p.Gal
y : F
rw :
  Eq (α := p.SplittingField) ((algebraMap F p.SplittingField : (a : F) → p.SplittingField) y : p.SplittingField)
    ((1 : (a : p.SplittingField) → p.SplittingField) ((algebraMap F p.SplittingField : (a : F) → p.SplittingField) y) :
      p.SplittingField)
⊢ Eq (α := p.SplittingField)
    ((f : (a : p.SplittingField) → p.SplittingField) ((algebraMap F p.SplittingField : (a : F) → p.SplittingField) y) :
      p.SplittingField)
    ((1 : (a : p.SplittingField) → p.SplittingField) ((algebraMap F p.SplittingField : (a : F) → p.SplittingField) y) :
      p.SplittingField)
have rw₁ : Eq (α := p.SplittingField) ((algebraMap F p.SplittingField : (a : F) → p.SplittingField) y : p.SplittingField)
  ((algebraMap F p.SplittingField : (a : F) → p.SplittingField) y : p.SplittingField)
Tactic: rw [AlgEquiv.commutes, AlgEquiv.commutes]
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
h : Fact (Splits (map (algebraMap F E) p))
⊢ Function.Bijective (β := (↑(p.rootSet E) : Type u_2)) (mapRoots p E)
have left : Function.Injective (β := (↑(p.rootSet E) : Type u_2)) (mapRoots p E)
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
h : Fact (Splits (map (algebraMap F E) p))
left : Function.Injective (β := (↑(p.rootSet E) : Type u_2)) (mapRoots p E)
⊢ Function.Bijective (β := (↑(p.rootSet E) : Type u_2)) (mapRoots p E)
have right : Function.Surjective (β := (↑(p.rootSet E) : Type u_2)) (mapRoots p E)
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (hypothesis)
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
h : Fact (Splits (map (algebraMap F E) p))
y : (↑(p.rootSet E) : Type u_2)
⊢ ∃ (a : (↑(p.rootSet p.SplittingField) : Type u_1)), mapRoots p E a = y
have key : roots
    (map (↑(IsScalarTower.toAlgHom F p.SplittingField E) : p.SplittingField →+* E)
      (map (algebraMap F p.SplittingField) p)) =
  Multiset.map (α := p.SplittingField)
    (⇑(↑(IsScalarTower.toAlgHom F p.SplittingField E) : p.SplittingField →+* E) : (a : p.SplittingField) → E)
    (roots (map (algebraMap F p.SplittingField) p))
Tactic: have key := (IsSplittingField.splits p.SplittingField p).roots_map
      (IsScalarTower.toAlgHom F p.SplittingField E : p.SplittingField →+* E)
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (hypothesis)
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
h : Fact (Splits (map (algebraMap F E) p))
y : (↑(p.rootSet E) : Type u_2)
key :
  roots
      (map (↑(IsScalarTower.toAlgHom F p.SplittingField E) : p.SplittingField →+* E)
        (map (algebraMap F p.SplittingField) p)) =
    Multiset.map (α := p.SplittingField)
      (⇑(↑(IsScalarTower.toAlgHom F p.SplittingField E) : p.SplittingField →+* E) : (a : p.SplittingField) → E)
      (roots (map (algebraMap F p.SplittingField) p))
⊢ ∃ (a : (↑(p.rootSet p.SplittingField) : Type u_1)), mapRoots p E a = y
have key₁ : roots (map (algebraMap F E) p) =
  Multiset.map (α := p.SplittingField)
    (⇑(↑(IsScalarTower.toAlgHom F p.SplittingField E) : p.SplittingField →+* E) : (a : p.SplittingField) → E)
    (roots (map (algebraMap F p.SplittingField) p))
Tactic: rw [map_map, AlgHom.comp_algebraMap] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (hypothesis)
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
h : Fact (Splits (map (algebraMap F E) p))
y : (↑(p.rootSet E) : Type u_2)
key :
  roots (map (algebraMap F E) p) =
    Multiset.map (α := p.SplittingField)
      (⇑(↑(IsScalarTower.toAlgHom F p.SplittingField E) : p.SplittingField →+* E) : (a : p.SplittingField) → E)
      (roots (map (algebraMap F p.SplittingField) p))
⊢ ∃ (a : (↑(p.rootSet p.SplittingField) : Type u_1)), mapRoots p E a = y
have hy : (↑y : E) ∈ p.rootSet E
Tactic: have hy := Subtype.mem y
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (hypothesis)
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
h : Fact (Splits (map (algebraMap F E) p))
y : (↑(p.rootSet E) : Type u_2)
key :
  roots (map (algebraMap F E) p) =
    Multiset.map (α := p.SplittingField)
      (⇑(↑(IsScalarTower.toAlgHom F p.SplittingField E) : p.SplittingField →+* E) : (a : p.SplittingField) → E)
      (roots (map (algebraMap F p.SplittingField) p))
hy : (↑y : E) ∈ p.rootSet E
⊢ ∃ (a : (↑(p.rootSet p.SplittingField) : Type u_1)), mapRoots p E a = y
have hy₁ : ∃ (a : p.SplittingField),
  Membership.mem (γ := Multiset p.SplittingField) (roots (map (algebraMap F p.SplittingField) p)) a ∧
    ((↑(IsScalarTower.toAlgHom F p.SplittingField E) : p.SplittingField →+* E) : (a : p.SplittingField) → E) a =
      (↑y : E)
Tactic: simp only [rootSet, Finset.mem_coe, Multiset.mem_toFinset, key, Multiset.mem_map] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p : F[X]
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
h : Fact (Splits (map (algebraMap F E) p))
y : (↑(p.rootSet E) : Type u_2)
key :
  roots (map (algebraMap F E) p) =
    Multiset.map (α := p.SplittingField)
      (⇑(↑(IsScalarTower.toAlgHom F p.SplittingField E) : p.SplittingField →+* E) : (a : p.SplittingField) → E)
      (roots (map (algebraMap F p.SplittingField) p))
hy :
  ∃ (a : p.SplittingField),
    Membership.mem (γ := Multiset p.SplittingField) (roots (map (algebraMap F p.SplittingField) p)) a ∧
      ((↑(IsScalarTower.toAlgHom F p.SplittingField E) : p.SplittingField →+* E) : (a : p.SplittingField) → E) a =
        (↑y : E)
⊢ ∃ (a : (↑(p.rootSet p.SplittingField) : Type u_1)), mapRoots p E a = y
have right : ∀ (x : p.SplittingField)
  (hx1 : Membership.mem (γ := Multiset p.SplittingField) (roots (map (algebraMap F p.SplittingField) p)) x)
  (hx2 :
    ((↑(IsScalarTower.toAlgHom F p.SplittingField E) : p.SplittingField →+* E) : (a : p.SplittingField) → E) x =
      (↑y : E)),
  ∃ (a : (↑(p.rootSet p.SplittingField) : Type u_1)), mapRoots p E a = y
Tactic: rcases hy with ⟨x, hx1, hx2⟩
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
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
x x_1 : p.Gal
x_2 : (↑(p.rootSet p.SplittingField) : Type u_1)
⊢ (x * x_1) • x_2 = x • x_1 • x_2
have a : (↑((x * x_1) • x_2) : p.SplittingField) = (↑(x • x_1 • x_2) : p.SplittingField)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
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
x : (↑(p.rootSet p.SplittingField) : Type u_1)
⊢ HSMul.hSMul (α := p.Gal) 1 x = x
have a : (↑(HSMul.hSMul (α := p.Gal) 1 x) : p.SplittingField) = (↑x : p.SplittingField)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
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)
have refine : ∀ (x y : (↑(p.rootSet E) : Type u_2)), ∃ (g : p.Gal), g • x = y
Tactic: refine ⟨fun x y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (hypothesis)
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)
⊢ ∃ (g : p.Gal), g • x = y
have 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)
Tactic: have hx := minpoly.eq_of_irreducible hp (mem_rootSet.mp ((rootsEquivRoots p E).symm x).2).2
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (hypothesis)
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)
⊢ ∃ (g : p.Gal), g • x = y
have 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)
Tactic: have hy := minpoly.eq_of_irreducible hp (mem_rootSet.mp ((rootsEquivRoots p E).symm y).2).2
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
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 : p.Gal), g • x = y
have 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
Tactic: obtain ⟨g, hg⟩ := (Normal.minpoly_eq_iff_mem_orbit p.SplittingField).mp (hy.symm.trans hx)
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
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)
⊢ (↑(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)
have 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)
Tactic: change ↑(ψ (ψ.symm _)) = ϕ x
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
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)
⊢ 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)
have 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)
Tactic: change ϕ (rootsEquivRoots p E ((rootsEquivRoots p E).symm x)) = ϕ x
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
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)
⊢ 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)
have rw : Eq (α := E) ((ϕ : (a : E) → E) (↑x : E) : E) ((ϕ : (a : E) → E) (↑x : E) : E)
Tactic: rw [Equiv.apply_symm_apply (rootsEquivRoots p E)]
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
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))
⊢ 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))
have 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
Tactic: rw [injective_iff_map_eq_one]
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
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))
⊢ ϕ = 1
have 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)
Tactic: ext (x hx)