awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
L : Type v
inst_3 : CommSemiring L
inst_4 : CharP L p
inst_5 : PerfectRing L p
f : RingHom.{u, v} (PerfectClosure K p) L
x_1 : PerfectClosure K p
n : ℕ
x : K
a :
  Eq (α := L)
    ((⇑(frobenius L p) : (a : L) → L)^[n]
        ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n]
          ((f : (a : PerfectClosure K p) → L) ((of K p : (a : K) → PerfectClosure K p) x : PerfectClosure K p))) :
      L)
    ((f : (a : PerfectClosure K p) → L)
        ((⇑(frobenius (PerfectClosure K p) p) : (a : PerfectClosure K p) → PerfectClosure K p)^[n] (mk K p (n, x))) :
      L)
a₁ :
  Eq (α := L)
    ((⇑(frobenius L p) : (a : L) → L)^[n]
        ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n]
          ((f : (a : PerfectClosure K p) → L) ((of K p : (a : K) → PerfectClosure K p) x : PerfectClosure K p))) :
      L)
    ((f : (a : PerfectClosure K p) → L) ((of K p : (a : K) → PerfectClosure K p) x : PerfectClosure K p) : L)
a₂ a₃ :
  Eq.{v + 1} (α := L)
    ((f : (a : PerfectClosure K p) → L) ((of K p : (a : K) → PerfectClosure K p) x : PerfectClosure K p) : L)
    ((f : (a : PerfectClosure K p) → L) ((of K p : (a : K) → PerfectClosure K p) x : PerfectClosure K p) : L)
⊢ Eq (α := L)
    ((⇑(frobenius L p) : (a : L) → L)^[n]
        ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n]
          ((f : (a : PerfectClosure K p) → L) ((of K p : (a : K) → PerfectClosure K p) x : PerfectClosure K p))) :
      L)
    ((⇑(frobenius L p) : (a : L) → L)^[n] ((f : (a : PerfectClosure K p) → L) (mk K p (n, x))) : L)

Tactic:
rw [← f.map_iterate_frobenius, iterate_frobenius_mk,
      RightInverse.iterate (frobenius_apply_frobeniusEquiv_symm L p) n]

Premises used: Function.RightInverse.iterate, RingHom.map_iterate_frobenius, frobenius_apply_frobeniusEquiv_symm, PerfectClosure.iterate_frobenius_mk
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
inst_1 : IsReduced K
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP K p
x y : ℕ × K
h : ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2
z : ℕ
H : (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2
⊢ (⇑(frobenius K p) : (a : K) → K)^[z] ((⇑(frobenius K p) : (a : K) → K)^[y.1] x.2) =
    (⇑(frobenius K p) : (a : K) → K)^[z] ((⇑(frobenius K p) : (a : K) → K)^[x.1] y.2)

Tactic:
simpa only [add_comm, iterate_add] using H

Premises used: Function.iterate_add, add_comm
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : Field K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x_1 y : ℕ × K
H : R K p x_1 y
n : ℕ
x : K
simp : R K p (n, x⁻¹) (n + 1, (x ^ p)⁻¹)
⊢ R K p ((n, x).1, (n, x).2⁻¹)
    (((n + 1, (frobenius K p : (a : K) → K) x) : ℕ × K).1, (n + 1, (frobenius K p : (a : K) → K) x).2⁻¹)

Tactic:
simp only [frobenius_def]

Premises used: frobenius_def
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : Field K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x_1 y : ℕ × K
H : R K p x_1 y
n : ℕ
x : K
rw : R K p (n, x⁻¹) (n + 1, x⁻¹ ^ p)
⊢ R K p (n, x⁻¹) (n + 1, (x ^ p)⁻¹)

Tactic:
rw [← inv_pow]

Premises used: inv_pow
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : Field K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x_1 y : ℕ × K
H : R K p x_1 y
n : ℕ
x : K
⊢ R K p (n, x⁻¹) (n + 1, x⁻¹ ^ p)

Tactic:
apply R.intro

Premises used: PerfectClosure.R.intro
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : Field K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : ℕ × K
⊢ Eq (α := PerfectClosure K p) (mk K p x)⁻¹ (mk K p (x.1, x.2⁻¹))

Tactic:
rfl

Premises used: PerfectClosure.mk, rfl
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : Field K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
e : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
H : Ne (α := PerfectClosure K p) (mk K p (m, x)) 0
⊢ ¬(⇑(frobenius K p) : (a : K) → K)^[(0, 0).1] (m, x).2 = (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] (0, 0).2

Tactic:
have := mt (eq_iff _ _ _ _).2 H
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : Field K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
e : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
H : Ne (α := PerfectClosure K p) (mk K p (m, x)) 0
this : ¬(⇑(frobenius K p) : (a : K) → K)^[(0, 0).1] (m, x).2 = (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] (0, 0).2
rw :
  Eq (α := PerfectClosure K p)
    (mk K p
      ((m, x).1 + ((m, x).1, (m, x).2⁻¹).1,
        (⇑(frobenius K p) : (a : K) → K)^[((m, x).1, (m, x).2⁻¹).1] (m, x).2 *
          (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] ((m, x).1, (m, x).2⁻¹).2))
    1
⊢ HMul.hMul (α := PerfectClosure K p) (mk K p (m, x)) (mk K p (m, x))⁻¹ = 1

Tactic:
rw [mk_inv, mk_mul_mk]

Premises used: PerfectClosure.mk_mul_mk, PerfectClosure.mk_inv
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : Field K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
e : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
H : Ne (α := PerfectClosure K p) (mk K p (m, x)) 0
this : ¬(⇑(frobenius K p) : (a : K) → K)^[(0, 0).1] (m, x).2 = (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] (0, 0).2
⊢ Eq (α := PerfectClosure K p)
    (mk K p
      ((m, x).1 + ((m, x).1, (m, x).2⁻¹).1,
        (⇑(frobenius K p) : (a : K) → K)^[((m, x).1, (m, x).2⁻¹).1] (m, x).2 *
          (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] ((m, x).1, (m, x).2⁻¹).2))
    1

Tactic:
(eq_iff K p _ _).2 ?_

Premises used: Iff.mpr, PerfectClosure.eq_iff
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : Field K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
e : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
H : Ne (α := PerfectClosure K p) (mk K p (m, x)) 0
this : ¬(⇑(frobenius K p) : (a : K) → K)^[(0, 0).1] (m, x).2 = (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] (0, 0).2
refine :
  (⇑(frobenius K p) : (a : K) → K)^[(0, 1).1]
      ((m, x).1 + ((m, x).1, (m, x).2⁻¹).1,
          (⇑(frobenius K p) : (a : K) → K)^[((m, x).1, (m, x).2⁻¹).1] (m, x).2 *
            (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] ((m, x).1, (m, x).2⁻¹).2).2 =
    (⇑(frobenius K p) :
          (a : K) →
            K)^[((m, x).1 + ((m, x).1, (m, x).2⁻¹).1,
            (⇑(frobenius K p) : (a : K) → K)^[((m, x).1, (m, x).2⁻¹).1] (m, x).2 *
              (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] ((m, x).1, (m, x).2⁻¹).2).1]
      (0, 1).2
⊢ Eq (α := PerfectClosure K p)
    (mk K p
      ((m, x).1 + ((m, x).1, (m, x).2⁻¹).1,
        (⇑(frobenius K p) : (a : K) → K)^[((m, x).1, (m, x).2⁻¹).1] (m, x).2 *
          (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] ((m, x).1, (m, x).2⁻¹).2))
    1

Tactic:
refine (eq_iff K p _ _).2 ?_

Premises used: Iff.mpr, PerfectClosure.eq_iff
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : Field K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
e : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
H : Ne (α := PerfectClosure K p) (mk K p (m, x)) 0
this : ¬(⇑(frobenius K p) : (a : K) → K)^[(0, 0).1] (m, x).2 = (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] (0, 0).2
simp : ∀ (this : ¬x = 0), (⇑(frobenius K p) : (a : K) → K)^[m] (x * x⁻¹) = 1
⊢ (⇑(frobenius K p) : (a : K) → K)^[(0, 1).1]
      ((m, x).1 + ((m, x).1, (m, x).2⁻¹).1,
          (⇑(frobenius K p) : (a : K) → K)^[((m, x).1, (m, x).2⁻¹).1] (m, x).2 *
            (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] ((m, x).1, (m, x).2⁻¹).2).2 =
    (⇑(frobenius K p) :
          (a : K) →
            K)^[((m, x).1 + ((m, x).1, (m, x).2⁻¹).1,
            (⇑(frobenius K p) : (a : K) → K)^[((m, x).1, (m, x).2⁻¹).1] (m, x).2 *
              (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] ((m, x).1, (m, x).2⁻¹).2).1]
      (0, 1).2

Tactic:
simp only [iterate_map_one, iterate_map_zero, iterate_zero_apply, ← iterate_map_mul] at this ⊢

Premises used: iterate_map_one, iterate_map_zero, iterate_map_mul, Function.iterate_zero_apply
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : Field K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
e : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
H : Ne (α := PerfectClosure K p) (mk K p (m, x)) 0
this : ¬x = 0
rw : Eq (α := K) ((⇑(frobenius K p) : (a : K) → K)^[m] 1) 1
rw₁ rw₂ : Eq.{u + 1} (α := K) 1 1
⊢ (⇑(frobenius K p) : (a : K) → K)^[m] (x * x⁻¹) = 1

Tactic:
rw [mul_inv_cancel₀ this, iterate_map_one]

Premises used: iterate_map_one, mul_inv_cancel₀
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : Field K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
rw rw₁ : Eq.{u + 1} (α := ℕ × K) ((0, 0).1, 0) (0, 0)
⊢ Eq.{u + 1} (α := ℕ × K) ((0, 0).1, (0, 0).2⁻¹) (0, 0)

Tactic:
rw [inv_zero]

Premises used: inv_zero
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : Field K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
⊢ PerfectField.{u} (PerfectClosure K p)

Tactic:
PerfectRing.toPerfectField _ p

Premises used: PerfectRing.toPerfectField
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
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)
⊢ σ = τ

Tactic:
AlgEquiv.ext fun x =>
      (AlgHom.mem_equalizer σ.toAlgHom τ.toAlgHom x).mp
        ((SetLike.ext_iff.mp ?_ x).mpr Algebra.mem_top)

Premises used: Iff.mpr, Algebra.mem_top, AlgEquiv.toAlgHom, Polynomial.Gal, SetLike.ext_iff, AlgEquiv.ext, Iff.mp, AlgHom.mem_equalizer
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
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)
fun :
  ∀ (x : p.SplittingField),
    Eq (α := Subalgebra F p.SplittingField)
      (AlgHom.equalizer (↑σ : p.SplittingField →ₐ[F] p.SplittingField) (↑τ : p.SplittingField →ₐ[F] p.SplittingField)) ⊤
⊢ σ = τ

Tactic:
refine
    AlgEquiv.ext fun x =>
      (AlgHom.mem_equalizer σ.toAlgHom τ.toAlgHom x).mp
        ((SetLike.ext_iff.mp ?_ x).mpr Algebra.mem_top)

Premises used: Iff.mpr, Algebra.mem_top, AlgEquiv.toAlgHom, SetLike.ext_iff, AlgEquiv.ext, Iff.mp, AlgHom.mem_equalizer
-- Module: Mathlib.FieldTheory.PolynomialGaloisGroup
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))
rwa₂ rwa₃ rwa₄ rwa₅ :
  p.rootSet p.SplittingField ⊆
    (↑(AlgHom.equalizer (↑σ : p.SplittingField →ₐ[F] p.SplittingField) (↑τ : p.SplittingField →ₐ[F] p.SplittingField)) :
      Set p.SplittingField)
⊢ Eq (α := Subalgebra F p.SplittingField)
    (AlgHom.equalizer (↑σ : p.SplittingField →ₐ[F] p.SplittingField) (↑τ : p.SplittingField →ₐ[F] p.SplittingField)) ⊤

Tactic:
rwa [eq_top_iff, ← SplittingField.adjoin_rootSet, Algebra.adjoin_le_iff]

Premises used: eq_top_iff, Algebra.adjoin_le_iff, Polynomial.SplittingField.adjoin_rootSet
-- 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
h : p.Splits
f : p.Gal
x : p.SplittingField
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)
⊢ Eq (α := p.SplittingField) ((f : (a : p.SplittingField) → p.SplittingField) x : p.SplittingField)
    ((1 : (a : p.SplittingField) → p.SplittingField) x : 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)

Premises used: Algebra.mem_top, Polynomial.IsSplittingField.splits_iff, Algebra.mem_bot, SetLike.ext_iff, Iff.mp, 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
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)
rw₁ 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)
⊢ 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:
rw [AlgEquiv.commutes, AlgEquiv.commutes]

Premises used: AlgEquiv.commutes
-- 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
⊢ Splits.{u_1} (R := F) 0

Tactic:
simp
-- 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
x : F
⊢ Splits.{u_1} (R := F) ((C : (a : F) → F[X]) x)

Tactic:
simp
-- 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
h : Fact (Splits (map (algebraMap F E) p))
⊢ IsScalarTower F p.SplittingField E

Tactic:
IsScalarTower.of_algebraMap_eq fun x =>
    ((IsSplittingField.lift p.SplittingField p h.1).commutes x).symm

Premises used: Polynomial.SplittingField, Polynomial.IsSplittingField.lift, IsScalarTower.of_algebraMap_eq, AlgHom.commutes, Eq.symm, Fact.out
-- 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))
inst_4 : Normal F E
⊢ Function.Surjective.{u_2 + 1, u_1 + 1} (α := Gal(E/F)) (β := p.Gal) (⇑(restrict p E) : (a : Gal(E/F)) → p.Gal)

Tactic:
AlgEquiv.restrictNormalHom_surjective E

Premises used: AlgEquiv.restrictNormalHom_surjective, Polynomial.Gal
-- 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
h : Fact (Splits (map (algebraMap F E) p))
left : Function.Injective (β := (↑(p.rootSet E) : Type u_2)) (mapRoots p E)
right : Function.Surjective (β := (↑(p.rootSet E) : Type u_2)) (mapRoots p E)
⊢ Function.Bijective (β := (↑(p.rootSet E) : Type u_2)) (mapRoots p E)

Tactic:
constructor
-- 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
h : Fact (Splits (map (algebraMap F E) p))
⊢ Function.Injective (β := (↑(p.rootSet E) : Type u_2)) (mapRoots p E)

Tactic:
fun _ _ h => Subtype.ext (RingHom.injective _ (Subtype.ext_iff.mp h))

Premises used: IsScalarTower.toAlgHom, Polynomial.SplittingField, RingHom.injective, Subtype.ext_iff, AlgHom.toRingHom, Iff.mp, Function.Injective, Subtype.ext
-- 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
h : Fact (Splits (map (algebraMap F E) p))
⊢ Function.Injective (β := (↑(p.rootSet E) : Type u_2)) (mapRoots p E)

Tactic:
exact fun _ _ h => Subtype.ext (RingHom.injective _ (Subtype.ext_iff.mp h))

Premises used: RingHom.injective, Subtype.ext
-- 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
h : Fact (Splits (map (algebraMap F E) p))
y : (↑(p.rootSet E) : Type u_2)
⊢ 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)
-- 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
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))
⊢ 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

Premises used: AlgHom.comp_algebraMap, Polynomial.map_map
-- 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
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))
⊢ (↑y : E) ∈ p.rootSet E

Tactic:
have hy := Subtype.mem 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
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.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

Premises used: Multiset.mem_map, Polynomial.rootSet, Finset.mem_coe, Multiset.mem_toFinset
-- 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
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)
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
⊢ ∃ (a : (↑(p.rootSet p.SplittingField) : Type u_1)), mapRoots p E a = y

Tactic:
rcases hy with ⟨x, hx1, hx2⟩
-- 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
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))
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:
⟨⟨x, (@Multiset.mem_toFinset _ (Classical.decEq _) _ _).mpr hx1⟩, Subtype.ext hx2⟩

Premises used: Iff.mpr, Subtype.mk, Exists.intro, Multiset.mem_toFinset, Subtype.ext
-- 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
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))
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:
exact ⟨⟨x, (@Multiset.mem_toFinset _ (Classical.decEq _) _ _).mpr hx1⟩, Subtype.ext hx2⟩
-- 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
x x_1 : p.Gal
x_2 : (↑(p.rootSet p.SplittingField) : Type u_1)
a : (↑((x * x_1) • x_2) : p.SplittingField) = (↑(x • x_1 • x_2) : p.SplittingField)
⊢ (x * x_1) • x_2 = x • x_1 • x_2

Tactic:
ext
-- 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
x x_1 : p.Gal
x_2 : (↑(p.rootSet p.SplittingField) : Type u_1)
⊢ (↑((x * x_1) • x_2) : p.SplittingField) = (↑(x • x_1 • x_2) : p.SplittingField)

Tactic:
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
x : (↑(p.rootSet p.SplittingField) : Type u_1)
a : (↑(HSMul.hSMul (α := p.Gal) 1 x) : p.SplittingField) = (↑x : p.SplittingField)
⊢ HSMul.hSMul (α := p.Gal) 1 x = x

Tactic:
ext
-- 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
x : (↑(p.rootSet p.SplittingField) : Type u_1)
⊢ (↑(HSMul.hSMul (α := p.Gal) 1 x) : p.SplittingField) = (↑x : p.SplittingField)

Tactic:
rfl