awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨆ (i : ι), t i)
s : Finset ((i : ι) × ↥(t i))
hx :
  Membership.mem (γ := IntermediateField F K)
    (⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)) (↑x : K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)
hF : Normal.{u_1, u_2} F ↥E
hE : E ≤ ⨆ (i : ι), t i
⊢ Splits.{u_2} (R := ↥E)
    (Polynomial.map (algebraMap F ↥E) (minpoly F (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (↑x : K) hx)))

Tactic:
have := hF.splits ⟨x, hx⟩
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨆ (i : ι), t i)
s : Finset ((i : ι) × ↥(t i))
hx :
  Membership.mem (γ := IntermediateField F K)
    (⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)) (↑x : K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)
hF : Normal.{u_1, u_2} F ↥E
hE : E ≤ ⨆ (i : ι), t i
this :
  Splits.{u_2} (R := ↥E)
    (Polynomial.map (algebraMap F ↥E) (minpoly F (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (↑x : K) hx)))
⊢ Splits.{u_2} (R := ↥E) (Polynomial.map (algebraMap F ↥E) (minpoly F x))

Tactic:
rw [minpoly_eq, Subtype.coe_mk, ← minpoly_eq] at this

Premises used: Subtype.coe_mk, IntermediateField.minpoly_eq
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨆ (i : ι), t i)
s : Finset ((i : ι) × ↥(t i))
hx :
  Membership.mem (γ := IntermediateField F K)
    (⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)) (↑x : K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)
hF : Normal.{u_1, u_2} F ↥E
hE : E ≤ ⨆ (i : ι), t i
this : Splits.{u_2} (R := ↥E) (Polynomial.map (algebraMap F ↥E) (minpoly F x))
⊢ (Polynomial.map (inclusion hE).toRingHom (Polynomial.map (algebraMap F ↥E) (minpoly F x))).Splits

Tactic:
have := this.map (inclusion hE).toRingHom
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨆ (i : ι), t i)
s : Finset ((i : ι) × ↥(t i))
hx :
  Membership.mem (γ := IntermediateField F K)
    (⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)) (↑x : K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(t i)))) K)
hF : Normal.{u_1, u_2} F ↥E
hE : E ≤ ⨆ (i : ι), t i
this_1 : Splits.{u_2} (R := ↥E) (Polynomial.map (algebraMap F ↥E) (minpoly F x))
this : (Polynomial.map (inclusion hE).toRingHom (Polynomial.map (algebraMap F ↥E) (minpoly F x))).Splits
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : (Polynomial.map ((inclusion hE).comp (algebraMap F ↥E)) (minpoly F x)).Splits),
    Splits.{u_2} (R := ↥(⨆ (i : ι), t i)) (Polynomial.map (algebraMap F ↥(⨆ (i : ι), t i)) (minpoly F x))
⊢ Splits.{u_2} (R := ↥(⨆ (i : ι), t i)) (Polynomial.map (algebraMap F ↥(⨆ (i : ι), t i)) (minpoly F x))

Tactic:
rwa [Polynomial.map_map] at this

Premises used: Polynomial.map_map
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
L : Type u_3
inst_3 : Field L
inst_4 : Algebra F L
S : Set K
splits : ∀ x ∈ S, IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
x : K
hx : Membership.mem (γ := IntermediateField F K) (adjoin F S) x
E : IntermediateField F L := ⨆ (x : (↑S : Type u_2)), adjoin F (rootSet (minpoly F (↑x : K)) L)
⊢ Normal.{u_1, u_3} F ↥E

Tactic:
have normal : Normal F E := normal_iSup (h := fun x ↦
    Normal.of_isSplittingField (hFEp := adjoin_rootSet_isSplittingField (splits x x.2).2))
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
L : Type u_3
inst_3 : Field L
inst_4 : Algebra F L
S : Set K
splits : ∀ x ∈ S, IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
x_1 : K
hx_1 : Membership.mem (γ := IntermediateField F K) (adjoin F S) x_1
E : IntermediateField F L := ⨆ (x : (↑S : Type u_2)), adjoin F (rootSet (minpoly F (↑x : K)) L)
normal : Normal.{u_1, u_3} F ↥E
x : K
hx : x ∈ S
y : L
hy : y ∈ rootSet (minpoly F x) L
⊢ y ∈ rootSet (minpoly F (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ S) x hx) : K)) L

Tactic:
hy

Premises used: Set.Mem
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
L : Type u_3
inst_3 : Field L
inst_4 : Algebra F L
S : Set K
splits : ∀ x ∈ S, IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
x_1 : K
hx_1 : Membership.mem (γ := IntermediateField F K) (adjoin F S) x_1
E : IntermediateField F L := ⨆ (x : (↑S : Type u_2)), adjoin F (rootSet (minpoly F (↑x : K)) L)
normal : Normal.{u_1, u_3} F ↥E
x : K
hx : x ∈ S
y : L
hy : y ∈ rootSet (minpoly F x) L
⊢ y ∈ rootSet (minpoly F (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ S) x hx) : K)) L

Tactic:
exact hy
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
L : Type u_3
inst_3 : Field L
inst_4 : Algebra F L
S : Set K
splits : ∀ x ∈ S, IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
x : K
hx : Membership.mem (γ := IntermediateField F K) (adjoin F S) x
E : IntermediateField F L := ⨆ (x : (↑S : Type u_2)), adjoin F (rootSet (minpoly F (↑x : K)) L)
normal : Normal.{u_1, u_3} F ↥E
⊢ ∀ x ∈ S, Splits.{u_3} (R := ↥E) (Polynomial.map (algebraMap F ↥E) (minpoly F x))

Tactic:
have : ∀ x ∈ S, ((minpoly F x).map (algebraMap F E)).Splits := fun x hx ↦ splits_of_splits
    (splits x hx).2 fun y hy ↦ (le_iSup _ ⟨x, hx⟩ : _ ≤ E) (subset_adjoin F _ <| by exact hy)
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
L : Type u_3
inst_3 : Field L
inst_4 : Algebra F L
S : Set K
splits : ∀ x ∈ S, IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
x : K
hx : Membership.mem (γ := IntermediateField F K) (adjoin F S) x
E : IntermediateField F L := ⨆ (x : (↑S : Type u_2)), adjoin F (rootSet (minpoly F (↑x : K)) L)
normal : Normal.{u_1, u_3} F ↥E
this : ∀ x ∈ S, Splits.{u_3} (R := ↥E) (Polynomial.map (algebraMap F ↥E) (minpoly F x))
obtain : ∀ (φ : AlgHom.{u_1, u_2, u_3} F ↥(adjoin F S) ↥E), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
⊢ Splits (Polynomial.map (algebraMap F L) (minpoly F x))

Tactic:
obtain ⟨φ⟩ := nonempty_algHom_adjoin_of_splits fun x hx ↦ ⟨(splits x hx).1, this x hx⟩

Premises used: And.left, And.intro, IntermediateField.nonempty_algHom_adjoin_of_splits
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
L : Type u_3
inst_3 : Field L
inst_4 : Algebra F L
S : Set K
splits : ∀ x ∈ S, IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
x : K
hx : Membership.mem (γ := IntermediateField F K) (adjoin F S) x
E : IntermediateField F L := ⨆ (x : (↑S : Type u_2)), adjoin F (rootSet (minpoly F (↑x : K)) L)
normal : Normal.{u_1, u_3} F ↥E
this : ∀ x ∈ S, Splits.{u_3} (R := ↥E) (Polynomial.map (algebraMap F ↥E) (minpoly F x))
φ : AlgHom.{u_1, u_2, u_3} F ↥(adjoin F S) ↥E
⊢ (Polynomial.map E.val.toRingHom
      (Polynomial.map (algebraMap F ↥E)
        (minpoly.{u_1, u_3} F (B := ↥E)
          ((φ : (a : ↥(adjoin F S)) → ↥E)
              (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := IntermediateField F K) (adjoin F S) x) x hx) :
            ↥E)))).Splits

Tactic:
(normal.splits <| φ ⟨x, hx⟩).map E.val.toRingHom

Premises used: Normal.splits, Subtype.mk, AlgHom.toRingHom, IntermediateField.val, Polynomial.Splits.map, DFunLike.coe
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
L : Type u_3
inst_3 : Field L
inst_4 : Algebra F L
S : Set K
splits : ∀ x ∈ S, IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
x : K
hx : Membership.mem (γ := IntermediateField F K) (adjoin F S) x
E : IntermediateField F L := ⨆ (x : (↑S : Type u_2)), adjoin F (rootSet (minpoly F (↑x : K)) L)
normal : Normal.{u_1, u_3} F ↥E
this : ∀ x ∈ S, Splits.{u_3} (R := ↥E) (Polynomial.map (algebraMap F ↥E) (minpoly F x))
φ : AlgHom.{u_1, u_2, u_3} F ↥(adjoin F S) ↥E
h :
  Polynomial.map (algebraMap F L) (minpoly F x) =
    Polynomial.map E.val.toRingHom
      (Polynomial.map (algebraMap F ↥E)
        (minpoly.{u_1, u_3} F (B := ↥E)
          ((φ : (a : ↥(adjoin F S)) → ↥E)
              (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := IntermediateField F K) (adjoin F S) x) x hx) :
            ↥E)))
⊢ Splits (Polynomial.map (algebraMap F L) (minpoly F x))

Tactic:
convert! (normal.splits <| φ ⟨x, hx⟩).map E.val.toRingHom

Premises used: Normal.splits, Subtype.mk, AlgHom.toRingHom, IntermediateField.val, Polynomial.Splits.map, DFunLike.coe
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
L : Type u_3
inst_3 : Field L
inst_4 : Algebra F L
S : Set K
splits : ∀ x ∈ S, IsIntegral F x ∧ Splits (Polynomial.map (algebraMap F L) (minpoly F x))
x : K
hx : Membership.mem (γ := IntermediateField F K) (adjoin F S) x
E : IntermediateField F L := ⨆ (x : (↑S : Type u_2)), adjoin F (rootSet (minpoly F (↑x : K)) L)
normal : Normal.{u_1, u_3} F ↥E
this : ∀ x ∈ S, Splits.{u_3} (R := ↥E) (Polynomial.map (algebraMap F ↥E) (minpoly F x))
φ : AlgHom.{u_1, u_2, u_3} F ↥(adjoin F S) ↥E
⊢ Polynomial.map (algebraMap F L) (minpoly F x) =
    Polynomial.map E.val.toRingHom
      (Polynomial.map (algebraMap F ↥E)
        (minpoly.{u_1, u_3} F (B := ↥E)
          ((φ : (a : ↥(adjoin F S)) → ↥E)
              (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := IntermediateField F K) (adjoin F S) x) x hx) :
            ↥E)))

Tactic:
simp [minpoly.algHom_eq _ φ.injective, ← minpoly.algHom_eq _ (adjoin F S).val.injective,
    Polynomial.map_map]

Premises used: minpoly.algHom_eq, RingHom.injective, AlgHom.toRingHom, IntermediateField.adjoin, IntermediateField.val, Polynomial.map_map
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
E E' : IntermediateField F K
inst_3 : Normal.{u_1, u_2} F ↥E
inst_4 : Normal.{u_1, u_2} F ↥E'
⊢ Normal.{u_1, u_2} F ↥(Bool.rec (motive := fun (x : Bool) ↦ IntermediateField F K) E' E false : IntermediateField F K)

Tactic:
infer_instance
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
E E' : IntermediateField F K
inst_3 : Normal.{u_1, u_2} F ↥E
inst_4 : Normal.{u_1, u_2} F ↥E'
⊢ Normal.{u_1, u_2} F ↥(Bool.rec (motive := fun (x : Bool) ↦ IntermediateField F K) E' E true : IntermediateField F K)

Tactic:
infer_instance
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
⊢ Normal.{u_1, u_2} F ↥(⨅ (i : ι), t i)

Tactic:
{ toIsAlgebraic := ?_, splits' := fun x => ?_ }

Premises used: Normal.mk
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
refine_1 : Algebra.IsAlgebraic.{u_1, u_2} F ↥(⨅ (i : ι), t i)
refine_2 :
  ∀ (x : ↥(⨅ (i : ι), t i)),
    Splits.{u_2} (R := ↥(⨅ (i : ι), t i)) (Polynomial.map (algebraMap F ↥(⨅ (i : ι), t i)) (minpoly F x))
⊢ Normal.{u_1, u_2} F ↥(⨅ (i : ι), t i)

Tactic:
refine { toIsAlgebraic := ?_, splits' := fun x => ?_ }
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
f : ↥(iInf t) →ₐ[F] ↥(t hι.some) := inclusion ⋯
⊢ Algebra.IsAlgebraic.{u_1, u_2} F ↥(⨅ (i : ι), t i)

Tactic:
Algebra.IsAlgebraic.of_injective f f.injective

Premises used: RingHom.injective, AlgHom.toRingHom, Algebra.IsAlgebraic.of_injective
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
f : ↥(iInf t) →ₐ[F] ↥(t hι.some) := inclusion ⋯
⊢ Algebra.IsAlgebraic.{u_1, u_2} F ↥(⨅ (i : ι), t i)

Tactic:
exact Algebra.IsAlgebraic.of_injective f f.injective

Premises used: RingHom.injective, AlgHom.toRingHom, Algebra.IsAlgebraic.of_injective
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨅ (i : ι), t i)
i : ι
rw :
  Splits.{u_2} (R := ↥(t i))
    (Polynomial.map (algebraMap F ↥(t i))
      (minpoly F (B := ↥(t i)) ((inclusion ⋯ : (a : ↥(iInf t)) → ↥(t i)) x : ↥(t i))))
⊢ Splits.{u_2} (R := ↥(t i)) (Polynomial.map (algebraMap F ↥(t i)) (minpoly F x))

Tactic:
rw [← minpoly.algHom_eq (inclusion (iInf_le t i)) (inclusion (iInf_le t i)).injective]

Premises used: minpoly.algHom_eq, RingHom.injective, AlgHom.toRingHom, IntermediateField.inclusion, iInf_le
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨅ (i : ι), t i)
i : ι
⊢ Splits.{u_2} (R := ↥(t i))
    (Polynomial.map (algebraMap F ↥(t i))
      (minpoly F (B := ↥(t i)) ((inclusion ⋯ : (a : ↥(iInf t)) → ↥(t i)) x : ↥(t i))))

Tactic:
(h i).splits' (inclusion (iInf_le t i) x)

Premises used: Normal.splits', IntermediateField.inclusion, DFunLike.coe, iInf_le
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨅ (i : ι), t i)
i : ι
⊢ Splits.{u_2} (R := ↥(t i))
    (Polynomial.map (algebraMap F ↥(t i))
      (minpoly F (B := ↥(t i)) ((inclusion ⋯ : (a : ↥(iInf t)) → ↥(t i)) x : ↥(t i))))

Tactic:
exact (h i).splits' (inclusion (iInf_le t i) x)

Premises used: Normal.splits', IntermediateField.inclusion, DFunLike.coe, iInf_le
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨅ (i : ι), t i)
⊢ ∀ (i : ι), Splits.{u_2} (R := ↥(t i)) (Polynomial.map (algebraMap F ↥(t i)) (minpoly F x))

Tactic:
have hx : ∀ i, Splits ((minpoly F x).map (algebraMap F (t i))) := by
      intro i
      rw [← minpoly.algHom_eq (inclusion (iInf_le t i)) (inclusion (iInf_le t i)).injective]
      exact (h i).splits' (inclusion (iInf_le t i) x)
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨅ (i : ι), t i)
hx : ∀ (i : ι), Splits.{u_2} (R := ↥(t i)) (Polynomial.map (algebraMap F ↥(t i)) (minpoly F x))
refine_2 :
  ∀ (hx : ∀ (i : ι), ∀ x_1 ∈ rootSet (minpoly F x) K, x_1 ∈ t i),
    ∀ x_1 ∈ rootSet (minpoly F x) K, Membership.mem (γ := IntermediateField F K) (⨅ (i : ι), t i) x_1
⊢ Splits.{u_2} (R := ↥(⨅ (i : ι), t i)) (Polynomial.map (algebraMap F ↥(⨅ (i : ι), t i)) (minpoly F x))

Tactic:
simp only [splits_iff_mem (Splits.of_isScalarTower K (hx hι.some))] at hx ⊢

Premises used: IntermediateField.splits_iff_mem, Nonempty.some, Polynomial.Splits.of_isScalarTower
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨅ (i : ι), t i)
hx : ∀ (i : ι), ∀ x_1 ∈ rootSet (minpoly F x) K, x_1 ∈ t i
y : K
hy : y ∈ rootSet (minpoly F x) K
i : ι
⊢ Membership.mem (γ := Set K) ((fun (x : IntermediateField F K) ↦ (↑x : Set K)) ((fun (i : ι) ↦ t i) i)) y

Tactic:
hx i y hy

Premises used: Set.Mem
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal.{u_1, u_2} F ↥(t i)
x : ↥(⨅ (i : ι), t i)
hx : ∀ (i : ι), ∀ x_1 ∈ rootSet (minpoly F x) K, x_1 ∈ t i
y : K
hy : y ∈ rootSet (minpoly F x) K
i : ι
⊢ Membership.mem (γ := Set K) ((fun (x : IntermediateField F K) ↦ (↑x : Set K)) ((fun (i : ι) ↦ t i) i)) y

Tactic:
exact hx i y hy
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
E : IntermediateField F K
inst_3 : Normal.{u_1, u_2} F ↥E
f : ↥E →ₐ[F] K
g : Gal(↥E/F) := f.restrictNormal' ↥E
rw : (E.val.comp (↑g : ↥E →ₐ[F] ↥E)).fieldRange = E
rw₁ : IntermediateField.map E.val (↑g : ↥E →ₐ[F] ↥E).fieldRange = E
rw₂ : IntermediateField.map E.val ⊤ = E
rw₃ : E.val.fieldRange = E
rw₄ rw₅ : E = E
⊢ f.fieldRange = E

Tactic:
rw [← show E.val.comp ↑g = f from DFunLike.ext_iff.mpr (f.restrictNormal_commutes E),
    ← AlgHom.map_fieldRange, AlgEquiv.fieldRange_eq_top g, ← AlgHom.fieldRange_eq_map,
    IntermediateField.fieldRange_val]

Premises used: Iff.mpr, AlgHom.fieldRange_eq_map, Membership.mem, Subtype, AlgHom.map_fieldRange, DFunLike.ext_iff, AlgEquiv.fieldRange_eq_top, IntermediateField.fieldRange_val, AlgHom.restrictNormal_commutes
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
K₁ : Type u_3
K₂ : Type u_4
inst_1 : Field K₁
inst_2 : Field K₂
inst_3 : Algebra F K₁
inst_4 : Algebra F K₂
ϕ : K₁ →ₐ[F] K₂
E : Type u_6
inst_5 : Field E
inst_6 : Algebra F E
inst_7 : Algebra K₁ E
inst_8 : Algebra K₂ E
inst_9 : IsScalarTower F K₁ E
inst_10 : IsScalarTower F K₂ E
inst_11 : Normal F E
x : K₁
⊢ Eq (α := E) ((ϕ.liftNormal E : (a : E) → E) ((algebraMap K₁ E : (a : K₁) → E) x : E) : E)
    ((algebraMap K₂ E : (a : K₂) → E) ((ϕ : (a : K₁) → K₂) x : K₂) : E)

Tactic:
@AlgHom.commutes K₁ E E _ _ _ _ (_) _ _

Premises used: AlgHom.commutes
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
K₁ : Type u_3
inst_1 : Field K₁
inst_2 : Algebra F K₁
E : Type u_6
inst_3 : Field E
inst_4 : Algebra F E
inst_5 : Algebra K₁ E
inst_6 : IsScalarTower F K₁ E
ϕ : K₁ →ₐ[F] K₁
inst_7 : Normal F K₁
inst_8 : Normal F E
⊢ restrictNormal (ϕ.liftNormal E) K₁ = ϕ

Tactic:
AlgHom.ext fun x =>
    (algebraMap K₁ E).injective
      (Eq.trans (AlgHom.restrictNormal_commutes _ K₁ x) (ϕ.liftNormal_commutes E x))

Premises used: Algebra.algebraMap, AlgHom.liftNormal, AlgHom.ext, RingHom.injective, AlgHom.liftNormal_commutes, AlgHom.restrictNormal_commutes, Eq.trans
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
K₁ : Type u_3
K₂ : Type u_4
inst_1 : Field K₁
inst_2 : Field K₂
inst_3 : Algebra F K₁
inst_4 : Algebra F K₂
χ : K₁ ≃ₐ[F] K₂
E : Type u_6
inst_5 : Field E
inst_6 : Algebra F E
inst_7 : Algebra K₁ E
inst_8 : Algebra K₂ E
inst_9 : IsScalarTower F K₁ E
inst_10 : IsScalarTower F K₂ E
inst_11 : Normal F E
x : K₁
⊢ Eq (α := E) ((χ.liftNormal E : (a : E) → E) ((algebraMap K₁ E : (a : K₁) → E) x : E) : E)
    ((algebraMap K₂ E : (a : K₂) → E) ((χ : (a : K₁) → K₂) x : K₂) : E)

Tactic:
χ.toAlgHom.liftNormal_commutes E x

Premises used: AlgEquiv.toAlgHom, AlgHom.liftNormal_commutes
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
K₁ : Type u_3
inst_1 : Field K₁
inst_2 : Algebra F K₁
E : Type u_6
inst_3 : Field E
inst_4 : Algebra F E
inst_5 : Algebra K₁ E
inst_6 : IsScalarTower F K₁ E
χ : Gal(K₁/F)
inst_7 : Normal F K₁
inst_8 : Normal F E
⊢ restrictNormal (χ.liftNormal E) K₁ = χ

Tactic:
AlgEquiv.ext fun x =>
    (algebraMap K₁ E).injective
      (Eq.trans (AlgEquiv.restrictNormal_commutes _ K₁ x) (χ.liftNormal_commutes E x))

Premises used: Algebra.algebraMap, RingHom.injective, AlgEquiv.restrictNormal_commutes, AlgEquiv.ext, AlgEquiv.liftNormal, AlgEquiv.liftNormal_commutes, Eq.trans
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
K₁ : Type u_3
inst_1 : Field K₁
inst_2 : Algebra F K₁
E : Type u_6
inst_3 : Field E
inst_4 : Algebra F E
inst_5 : Algebra K₁ E
inst_6 : IsScalarTower F K₁ E
inst_7 : Normal F K₁
inst_8 : Normal F E
⊢ Function.Surjective.{u_6 + 1, u_3 + 1} (α := Gal(E/F)) (β := Gal(K₁/F))
    (⇑(restrictNormalHom K₁) : (a : Gal(E/F)) → Gal(K₁/F))

Tactic:
fun χ =>
  ⟨χ.liftNormal E, χ.restrict_liftNormal E⟩

Premises used: AlgEquiv.restrict_liftNormal, AlgEquiv.liftNormal, Exists.intro, Function.Surjective
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_6
inst_1 : Field E
inst_2 : Algebra F E
h : Normal F E
x y : E
⊢ Eq (α := F[X]) (minpoly F x) (minpoly F y) ↔ x ∈ MulAction.orbit Gal(E/F) y

Tactic:
⟨fun he ↦ ?_, fun ⟨f, he⟩ ↦ he ▸ minpoly.algEquiv_eq f y⟩

Premises used: Eq.rec, minpoly.algEquiv_eq, _private.0.Normal.minpoly_eq_iff_mem_orbit.match_1, minpoly, Iff.intro, Eq
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_6
inst_1 : Field E
inst_2 : Algebra F E
h : Normal F E
x y : E
refine : ∀ (he : Eq (α := F[X]) (minpoly F x) (minpoly F y)), x ∈ MulAction.orbit Gal(E/F) y
⊢ Eq (α := F[X]) (minpoly F x) (minpoly F y) ↔ x ∈ MulAction.orbit Gal(E/F) y

Tactic:
refine ⟨fun he ↦ ?_, fun ⟨f, he⟩ ↦ he ▸ minpoly.algEquiv_eq f y⟩
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_6
inst_1 : Field E
inst_2 : Algebra F E
h : Normal F E
x y : E
he : Eq (α := F[X]) (minpoly F x) (minpoly F y)
obtain : ∀ (φ : E →ₐ[F] E) (hφ : (φ : (a : E) → E) y = x), x ∈ MulAction.orbit Gal(E/F) y
⊢ x ∈ MulAction.orbit Gal(E/F) y

Tactic:
obtain ⟨φ, hφ⟩ := exists_algHom_of_splits_of_aeval (normal_iff.mp h) (he ▸ minpoly.aeval F x)

Premises used: normal_iff, Iff.mp, IntermediateField.exists_algHom_of_splits_of_aeval
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_6
inst_1 : Field E
inst_2 : Algebra F E
h : Normal F E
x y : E
he : Eq (α := F[X]) (minpoly F x) (minpoly F y)
φ : E →ₐ[F] E
hφ : (φ : (a : E) → E) y = x
⊢ x ∈ MulAction.orbit Gal(E/F) y

Tactic:
⟨AlgEquiv.ofBijective φ (φ.normal_bijective F E E), hφ⟩

Premises used: Set.Mem, AlgEquiv.ofBijective, setOf, MulAction.orbit, Exists.intro, AlgHom.normal_bijective, Set.range
-- Module: Mathlib.FieldTheory.Normal.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_6
inst_1 : Field E
inst_2 : Algebra F E
h : Normal F E
x y : E
he : Eq (α := F[X]) (minpoly F x) (minpoly F y)
φ : E →ₐ[F] E
hφ : (φ : (a : E) → E) y = x
⊢ x ∈ MulAction.orbit Gal(E/F) y

Tactic:
exact ⟨AlgEquiv.ofBijective φ (φ.normal_bijective F E E), hφ⟩