awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E : IntermediateField K L
inst_3 : Normal.{u_3, u_4} K ↥E
⊢ MonoidHom.ker (M := Gal(↥E/K)) (restrictNormalHom ↥E) = E.fixingSubgroup

Tactic:
simp only [Subgroup.ext_iff, MonoidHom.mem_ker, AlgEquiv.ext_iff, one_apply, Subtype.ext_iff,
    restrictNormalHom_apply, Subtype.forall, mem_fixingSubgroup_iff, implies_true]

Premises used: AlgEquiv.one_apply, AlgEquiv.ext_iff, Subtype.forall, MonoidHom.mem_ker, Subgroup.ext_iff, Subtype.ext_iff, AlgEquiv.restrictNormalHom_apply, implies_true, IntermediateField.mem_fixingSubgroup_iff
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E_1 : Type u_2
inst_1 : Field E_1
inst_2 : Algebra F E_1
H_1 : Subgroup Gal(E_1/F)
K_1 : IntermediateField F E_1
K : Type u_3
L : Type u_4
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
E : IntermediateField K L
inst_6 : IsGalois K L
H : Subgroup Gal(L/K)
hn : H.Normal
apply : ∀ (σ : Gal(L/K)), map (↑σ : L →ₐ[K] L) (fixedField H) ≤ fixedField H
⊢ Normal.{u_3, u_4} K ↥(fixedField H)

Tactic:
apply normal_iff_forall_map_le'.mpr

Premises used: Iff.mpr, IntermediateField.normal_iff_forall_map_le'
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E_1 : Type u_2
inst_1 : Field E_1
inst_2 : Algebra F E_1
H_1 : Subgroup Gal(E_1/F)
K_1 : IntermediateField F E_1
K : Type u_3
L : Type u_4
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
E : IntermediateField K L
inst_6 : IsGalois K L
H : Subgroup Gal(L/K)
hn : H.Normal
σ : Gal(L/K)
a : L
ha : a ∈ (↑(fixedField H).toSubsemiring : Set L)
τ : ↥H
⊢ HSMul.hSMul (β := L) τ (((↑(↑σ : L →ₐ[K] L) : L →+* L) : (a : L) → L) a : L) =
    ((↑(↑σ : L →ₐ[K] L) : L →+* L) : (a : L) → L) a

Tactic:
(symm_apply_eq σ).mp (ha ⟨σ⁻¹ * τ * σ, Subgroup.Normal.conj_mem' hn τ.1 τ.2 σ⟩)

Premises used: HMul.hMul, AlgEquiv.symm_apply_eq, Subtype.mk, Inv.inv, Iff.mp, Subtype.val, Subtype.property, Subgroup.Normal.conj_mem'
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E_1 : Type u_2
inst_1 : Field E_1
inst_2 : Algebra F E_1
H_1 : Subgroup Gal(E_1/F)
K_1 : IntermediateField F E_1
K : Type u_3
L : Type u_4
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
E : IntermediateField K L
inst_6 : IsGalois K L
H : Subgroup Gal(L/K)
hn : H.Normal
σ : Gal(L/K)
a : L
ha : a ∈ (↑(fixedField H).toSubsemiring : Set L)
τ : ↥H
⊢ HSMul.hSMul (β := L) τ (((↑(↑σ : L →ₐ[K] L) : L →+* L) : (a : L) → L) a : L) =
    ((↑(↑σ : L →ₐ[K] L) : L →+* L) : (a : L) → L) a

Tactic:
exact (symm_apply_eq σ).mp (ha ⟨σ⁻¹ * τ * σ, Subgroup.Normal.conj_mem' hn τ.1 τ.2 σ⟩)

Premises used: HMul.hMul, AlgEquiv.symm_apply_eq, Subtype.mk, Inv.inv, Iff.mp, Subtype.val, Subtype.property, Subgroup.Normal.conj_mem'
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
H : Subgroup Gal(L/K)
inst_5 : H.Normal
σ : Gal(L/K)
⊢ Eq (α := Gal(↥(fixedField H)/K))
    ((normalAutEquivQuotient H : (a : Gal(L/K) ⧸ H) → Gal(↥(fixedField H)/K)) (↑σ : Gal(L/K) ⧸ H) :
      Gal(↥(fixedField H)/K))
    ((restrictNormalHom ↥(fixedField H) : (a : Gal(L/K)) → Gal(↥(fixedField H)/K)) σ : Gal(↥(fixedField H)/K))

Tactic:
rfl

Premises used: Quotient.liftOn', AlgEquiv.ofBijective, AlgEquiv.restrictNormal, Con.liftOn, AlgHom.restrictNormal', rfl
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E : IntermediateField K L
σ : Gal(L/K)
h :
  ∀ (τ : Gal(L/K)),
    τ ∈ (map (↑σ : L →ₐ[K] L) E).fixingSubgroup ↔
      τ ∈
        HSMul.hSMul (α := MulAut Gal(L/K)) ((MulAut.conj : (a : Gal(L/K)) → MulAut Gal(L/K)) σ : MulAut Gal(L/K))
          E.fixingSubgroup
⊢ (map (↑σ : L →ₐ[K] L) E).fixingSubgroup =
    HSMul.hSMul (α := MulAut Gal(L/K)) ((MulAut.conj : (a : Gal(L/K)) → MulAut Gal(L/K)) σ : MulAut Gal(L/K))
      E.fixingSubgroup

Tactic:
ext τ
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E : IntermediateField K L
σ τ : Gal(L/K)
h :
  (∀ a ∈ E, (σ.symm : (a : L) → L) ((τ : (a : L) → L) ((σ : (a : L) → L) a : L) : L) = a) ↔
    ∀ y ∈ E,
      (HSMul.hSMul (α := MulAut Gal(L/K)) (((MulAut.conj : (a : Gal(L/K)) → MulAut Gal(L/K)) σ)⁻¹ : MulAut Gal(L/K)) τ :
            (a : L) → L)
          y =
        y
⊢ τ ∈ (map (↑σ : L →ₐ[K] L) E).fixingSubgroup ↔
    τ ∈
      HSMul.hSMul (α := MulAut Gal(L/K)) ((MulAut.conj : (a : Gal(L/K)) → MulAut Gal(L/K)) σ : MulAut Gal(L/K))
        E.fixingSubgroup

Tactic:
simp only [coe_map, AlgEquiv.coe_algHom, Set.mem_image, SetLike.mem_coe, AlgEquiv.smul_def,
    forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
    Subgroup.mem_pointwise_smul_iff_inv_smul_mem, ← symm_apply_eq,
    IntermediateField.fixingSubgroup, mem_fixingSubgroup_iff]

Premises used: AlgEquiv.symm_apply_eq, and_imp, AlgEquiv.smul_def, Set.mem_image, forall_exists_index, IntermediateField.fixingSubgroup, AlgEquiv.coe_algHom, SetLike.mem_coe, mem_fixingSubgroup_iff, Subgroup.mem_pointwise_smul_iff_inv_smul_mem, forall_apply_eq_imp_iff₂, IntermediateField.coe_map
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E : IntermediateField K L
σ τ : Gal(L/K)
⊢ (∀ a ∈ E, (σ.symm : (a : L) → L) ((τ : (a : L) → L) ((σ : (a : L) → L) a : L) : L) = a) ↔
    ∀ y ∈ E,
      (HSMul.hSMul (α := MulAut Gal(L/K)) (((MulAut.conj : (a : Gal(L/K)) → MulAut Gal(L/K)) σ)⁻¹ : MulAut Gal(L/K)) τ :
            (a : L) → L)
          y =
        y

Tactic:
rfl
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E_1 : Type u_2
inst_1 : Field E_1
inst_2 : Algebra F E_1
H : Subgroup Gal(E_1/F)
K_1 : IntermediateField F E_1
K : Type u_3
L : Type u_4
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
E : IntermediateField K L
inst_6 : IsGalois K L
inst_7 : IsGalois.{u_3, u_4} K ↥E
apply :
  ∀ (σ : Gal(L/K)),
    HSMul.hSMul (α := MulAut Gal(L/K)) ((MulAut.conj : (a : Gal(L/K)) → MulAut Gal(L/K)) σ : MulAut Gal(L/K))
        E.fixingSubgroup =
      E.fixingSubgroup
⊢ E.fixingSubgroup.Normal

Tactic:
apply Subgroup.Normal.of_conjugate_fixed (fun σ ↦ ?_)

Premises used: Subgroup.Normal.of_conjugate_fixed
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E_1 : Type u_2
inst_1 : Field E_1
inst_2 : Algebra F E_1
H : Subgroup Gal(E_1/F)
K_1 : IntermediateField F E_1
K : Type u_3
L : Type u_4
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
E : IntermediateField K L
inst_6 : IsGalois K L
inst_7 : IsGalois.{u_3, u_4} K ↥E
σ : Gal(L/K)
rw : (map (↑σ : L →ₐ[K] L) E).fixingSubgroup = E.fixingSubgroup
rw₁ rw₂ : E.fixingSubgroup = E.fixingSubgroup
⊢ HSMul.hSMul (α := MulAut Gal(L/K)) ((MulAut.conj : (a : Gal(L/K)) → MulAut Gal(L/K)) σ : MulAut Gal(L/K))
      E.fixingSubgroup =
    E.fixingSubgroup

Tactic:
rw [← map_fixingSubgroup, normal_iff_forall_map_eq'.mp inferInstance σ]

Premises used: inferInstance, IntermediateField.normal_iff_forall_map_eq', Iff.mp, IsGalois.map_fixingSubgroup
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
h : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
rw : IsGalois (↥(fixedField ⊤)) E
⊢ IsGalois F E

Tactic:
rw [← isGalois_iff_isGalois_bot, ← h]

Premises used: isGalois_iff_isGalois_bot
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
h : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
⊢ IsGalois (↥(fixedField ⊤)) E

Tactic:
IsGalois.of_fixed_field E (⊤ : Subgroup Gal(E/F))

Premises used: Subfield.subtype, FixedPoints.intermediateField, Set.Mem, Membership.mem, IntermediateField.fixedField, Subtype, Subfield.copy, FixedPoints.subfield, IsGalois.of_fixed_field, Top.top
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
h : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
⊢ IsGalois (↥(fixedField ⊤)) E

Tactic:
exact IsGalois.of_fixed_field E (⊤ : Subgroup Gal(E/F))

Premises used: Membership.mem, Subtype, IsGalois.of_fixed_field, Top.top
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
h : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
⊢ IsGalois (↥(fixedField ⊤)) E

Tactic:
classical exact IsGalois.of_fixed_field E (⊤ : Subgroup Gal(E/F))

Premises used: Membership.mem, Subtype, IsGalois.of_fixed_field, Top.top
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
h : Nat.card.{u_2} Gal(E/F) = finrank F E
h₁ : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
⊢ IsGalois F E

Tactic:
apply of_fixedField_eq_bot

Premises used: IsGalois.of_fixedField_eq_bot
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
h : Nat.card.{u_2} Gal(E/F) = finrank F E
⊢ 0 < finrank (↥(fixedField ⊤)) E

Tactic:
have p : 0 < finrank (IntermediateField.fixedField (⊤ : Subgroup Gal(E/F))) E := finrank_pos
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
h : Nat.card.{u_2} Gal(E/F) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
h₁ : Nat.card.{u_2} Gal(E/F) = Nat.card.{u_2} ↥⊤
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥

Tactic:
rw [← IntermediateField.finrank_eq_one_iff, ← mul_left_inj' (ne_of_lt p).symm,
    finrank_mul_finrank, ← h, one_mul, IntermediateField.finrank_fixedField_eq_card]

Premises used: IntermediateField.finrank_eq_one_iff, Ne.symm, IntermediateField.finrank_fixedField_eq_card, Module.finrank_mul_finrank, mul_left_inj', ne_of_lt, one_mul
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
h : Nat.card.{u_2} Gal(E/F) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
h₁ : Gal(E/F) ≃ ↥⊤
⊢ Nat.card.{u_2} Gal(E/F) = Nat.card.{u_2} ↥⊤

Tactic:
apply Nat.card_congr

Premises used: Nat.card_congr
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
h : Nat.card.{u_2} Gal(E/F) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
⊢ Gal(E/F) ≃ ↥⊤

Tactic:
exact { toFun := fun g => ⟨g, Subgroup.mem_top g⟩, invFun := (↑) }
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
h : Nat.card.{u_2} Gal(E/F) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
h₁ : finrank.{u_1, u_2} F ↥(fixedField ⊤) = 1
h₂ : finrank.{u_1, u_2} F ↥(fixedField ⊤) * finrank (↥(fixedField ⊤)) E = 1 * finrank (↥(fixedField ⊤)) E
h₃ : finrank F E = 1 * finrank (↥(fixedField ⊤)) E
h₄ : Nat.card.{u_2} Gal(E/F) = 1 * finrank (↥(fixedField ⊤)) E
h₅ : Nat.card.{u_2} Gal(E/F) = finrank (↥(fixedField ⊤)) E
h₆ h₇ h₈ : Nat.card.{u_2} Gal(E/F) = Nat.card.{u_2} ↥⊤
h₉ : Gal(E/F) ≃ ↥⊤
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥

Tactic:
classical
  rw [← IntermediateField.finrank_eq_one_iff, ← mul_left_inj' (ne_of_lt p).symm,
    finrank_mul_finrank, ← h, one_mul, IntermediateField.finrank_fixedField_eq_card]
  apply Nat.card_congr
  exact { toFun := fun g => ⟨g, Subgroup.mem_top g⟩, invFun := (↑) }

Premises used: IntermediateField.finrank_eq_one_iff, Ne.symm, Nat.card_congr, IntermediateField.finrank_fixedField_eq_card, Module.finrank_mul_finrank, mul_left_inj', ne_of_lt, one_mul
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
⊢ IsIntegral K x

Tactic:
have h : IsIntegral K x := (isIntegral_of_noetherian (IsNoetherian.iff_fg.2 hFE) x).tower_top
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp_1 : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
hp : p = 0
⊢ Membership.mem (γ := Multiset E) 0 x

Tactic:
rw [hp, Polynomial.aroots_zero] at hx

Premises used: Polynomial.aroots_zero
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp_1 : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
hp : p = 0
hx₁ : Membership.mem (γ := Multiset E) 0 x
⊢ IsIntegral K x

Tactic:
rw [hp, Polynomial.aroots_zero] at hx

Premises used: Polynomial.aroots_zero
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp_1 : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
hp : p = 0
hx₁ : Membership.mem (γ := Multiset E) 0 x
h₁ : IsIntegral K x
⊢ p = 0

Tactic:
rw [hp, Polynomial.aroots_zero] at hx

Premises used: Polynomial.aroots_zero
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp_1 : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : Membership.mem (γ := Multiset E) 0 x
h : IsIntegral K x
hp : p = 0
⊢ False

Tactic:
Multiset.notMem_zero x hx

Premises used: Multiset.notMem_zero
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp_1 : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : Membership.mem (γ := Multiset E) 0 x
h : IsIntegral K x
hp : p = 0
⊢ False

Tactic:
exact Multiset.notMem_zero x hx

Premises used: Multiset.notMem_zero
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
⊢ p ≠ 0

Tactic:
have h1 : p ≠ 0 := fun hp => by
    rw [hp, Polynomial.aroots_zero] at hx
    exact Multiset.notMem_zero x hx
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
hp₁ : Eq.{u_2 + 1} (α := E) ((Polynomial.aeval x : (a : K[X]) → E) (Polynomial.map (algebraMap F K) p) : E) (0 : E)
⊢ Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap F K) p)

Tactic:
apply minpoly.dvd

Premises used: minpoly.dvd
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
hp₁ : Polynomial.eval x (Polynomial.map (algebraMap F E) p) = 0
⊢ Eq.{u_2 + 1} (α := E) ((Polynomial.aeval x : (a : K[X]) → E) (Polynomial.map (algebraMap F K) p) : E) (0 : E)

Tactic:
rw [Polynomial.aeval_def, Polynomial.eval₂_map, ← Polynomial.eval_map, ←
      IsScalarTower.algebraMap_eq]

Premises used: Polynomial.eval_map, Polynomial.eval₂_map, Polynomial.aeval_def, IsScalarTower.algebraMap_eq
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
⊢ Polynomial.eval x (Polynomial.map (algebraMap F E) p) = 0

Tactic:
(Polynomial.mem_roots (Polynomial.map_ne_zero h1)).mp hx

Premises used: Polynomial.IsRoot, Polynomial.mem_roots, Iff.mp, Polynomial.map_ne_zero
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
⊢ Polynomial.eval x (Polynomial.map (algebraMap F E) p) = 0

Tactic:
exact (Polynomial.mem_roots (Polynomial.map_ne_zero h1)).mp hx

Premises used: Polynomial.mem_roots, Iff.mp, Polynomial.map_ne_zero
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
⊢ Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap F K) p)

Tactic:
have h2 : minpoly K x ∣ p.map (algebraMap F K) := by
    apply minpoly.dvd
    rw [Polynomial.aeval_def, Polynomial.eval₂_map, ← Polynomial.eval_map, ←
      IsScalarTower.algebraMap_eq]
    exact (Polynomial.mem_roots (Polynomial.map_ne_zero h1)).mp hx
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap F K) p)
change : (↥K⟮x⟯ →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E)
⊢ (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E)

Tactic:
change (K⟮x⟯ →ₐ[F] E) ≃ Σ f : K →ₐ[F] E, _

Premises used: AlgHom, Membership.mem, Subtype, IntermediateField.adjoin, Singleton.singleton
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap F K) p)
⊢ (↥K⟮x⟯ →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E)

Tactic:
exact algHomEquivSigma

Premises used: algHomEquivSigma
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap F K) p)
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
f : K →ₐ[F] E
⊢ Finite ((f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E))

Tactic:
have := Finite.of_equiv _ key_equiv
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap F K) p)
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
f : K →ₐ[F] E
this : Finite ((f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E))
⊢ Finite.{u_2 + 1} (↥K⟮x⟯ →ₐ[K] E)

Tactic:
apply Finite.of_injective (Sigma.mk f) fun _ _ H => eq_of_heq (Sigma.ext_iff.mp H).2

Premises used: Sigma.ext_iff, And.right, Iff.mp, eq_of_heq, Sigma.mk, Finite.of_injective
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap F K) p)
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
⊢ ∀ (f : K →ₐ[F] E), Finite.{u_2 + 1} (↥K⟮x⟯ →ₐ[K] E)

Tactic:
haveI : ∀ f : K →ₐ[F] E, Finite (@AlgHom K K⟮x⟯ E _ _ _ _ (RingHom.toAlgebra f)) := fun f => by
    have := Finite.of_equiv _ key_equiv
    apply Finite.of_injective (Sigma.mk f) fun _ _ H => eq_of_heq (Sigma.ext_iff.mp H).2
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra K E
inst_6 : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : Dvd.dvd (α := K[X]) (minpoly K x) (Polynomial.map (algebraMap F K) p)
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
this : ∀ (f : K →ₐ[F] E), Finite.{u_2 + 1} (↥K⟮x⟯ →ₐ[K] E)
⊢ FiniteDimensional F K

Tactic:
have : FiniteDimensional F K := FiniteDimensional.left F K E