awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g : E[X] // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
g : IntermediateField F E → G :=
  fun (K : IntermediateField F E) ↦
    Subtype.mk (p := fun (g : E[X]) ↦ g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f)
      (Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)) ⋯
⊢ Function.Injective g

Tactic:
have hinj : Function.Injective g := fun K K' heq ↦ by
    rw [Subtype.mk.injEq] at heq
    apply_fun fun f : E[X] ↦ adjoin F (f.coeffs : Set E) at heq
    simpa only [adjoin_minpoly_coeff_of_exists_primitive_element F hprim] using heq
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g : E[X] // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
g : IntermediateField F E → G :=
  fun (K : IntermediateField F E) ↦
    Subtype.mk (p := fun (g : E[X]) ↦ g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f)
      (Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)) ⋯
hinj : Function.Injective g
⊢ Finite.{u_2 + 1} (IntermediateField F E)

Tactic:
Finite.of_injective g hinj

Premises used: Finite.of_injective
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g : E[X] // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
g : IntermediateField F E → G :=
  fun (K : IntermediateField F E) ↦
    Subtype.mk (p := fun (g : E[X]) ↦ g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f)
      (Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)) ⋯
hinj : Function.Injective g
⊢ Finite.{u_2 + 1} (IntermediateField F E)

Tactic:
exact Finite.of_injective g hinj

Premises used: Finite.of_injective
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ (Algebra.IsAlgebraic F E ∧ ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤) ↔
    Finite.{u_2 + 1} (IntermediateField F E)

Tactic:
⟨fun ⟨_, h⟩ ↦ finite_intermediateField_of_exists_primitive_element F E h,
    fun _ ↦ ⟨isAlgebraic_of_finite_intermediateField F E,
      exists_primitive_element_of_finite_intermediateField F E _⟩⟩

Premises used: Field.finite_intermediateField_of_exists_primitive_element, _private.0.Field.exists_primitive_element_iff_finite_intermediateField.match_1, IntermediateField, Finite, Field.isAlgebraic_of_finite_intermediateField, And.intro, Iff.intro, Field.exists_primitive_element_of_finite_intermediateField, Top.top
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
L : Type u_3
inst_5 : Field L
inst_6 : Algebra F L
hL : ∀ (x : E), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
⊢ Nat.card (E →ₐ[F] L) = finrank F E

Tactic:
(AlgHom.natCard_of_powerBasis (L := L) (Field.powerBasisOfFiniteOfSeparable F E)
    (Algebra.IsSeparable.isSeparable _ _) <| hL _).trans
      (PowerBasis.finrank _).symm

Premises used: Algebra.IsSeparable.isSeparable, PowerBasis.finrank, AlgHom.natCard_of_powerBasis, Field.powerBasisOfFiniteOfSeparable, Eq.symm, Eq.trans
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
L : Type u_3
inst_5 : Field L
inst_6 : Algebra F L
hL : ∀ (x : E), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
rw : Nat.card (E →ₐ[F] L) = finrank F E
rw₁ rw₂ : finrank F E = finrank F E
⊢ Fintype.card (E →ₐ[F] L) = finrank F E

Tactic:
rw [Fintype.card_eq_nat_card, AlgHom.natCard_of_splits F E L hL]

Premises used: AlgHom.natCard_of_splits, Fintype.card_eq_nat_card
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
K : Type u_3
inst_5 : Field K
inst_6 : IsAlgClosed K
inst_7 : Algebra F K
⊢ Fintype.card (E →ₐ[F] K) = finrank F E

Tactic:
AlgHom.card_of_splits _ _ _ (fun _ ↦ IsAlgClosed.splits _)

Premises used: Algebra.algebraMap, minpoly, IsAlgClosed.splits, Polynomial.map, AlgHom.card_of_splits
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
α : E
rw : Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ finrank.{u_3, u_4} F ↥F⟮α⟯ = finrank.{u_3, u_4} F ↥⊤
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ natDegree (minpoly F α) = finrank F E

Tactic:
rw [← adjoin.finrank (IsIntegral.of_finite F α), ← finrank_top F E]

Premises used: IntermediateField.adjoin.finrank, finrank_top, IsIntegral.of_finite
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
α : E
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ finrank.{u_3, u_4} F ↥F⟮α⟯ = finrank.{u_3, u_4} F ↥⊤

Tactic:
⟨fun h => ?_, fun h => eq_of_le_of_finrank_eq le_top h⟩

Premises used: le_top, IntermediateField.eq_of_le_of_finrank_eq, Iff.intro
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
α : E
refine : ∀ (h : Eq (α := IntermediateField F E) F⟮α⟯ ⊤), finrank.{u_3, u_4} F ↥F⟮α⟯ = finrank.{u_3, u_4} F ↥⊤
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ finrank.{u_3, u_4} F ↥F⟮α⟯ = finrank.{u_3, u_4} F ↥⊤

Tactic:
refine ⟨fun h => ?_, fun h => eq_of_le_of_finrank_eq le_top h⟩
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
α : E
h : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
⊢ finrank.{u_3, u_4} F ↥F⟮α⟯ = finrank.{u_3, u_4} F ↥⊤

Tactic:
congr_arg (fun K : IntermediateField F E => finrank F K) h

Premises used: IntermediateField.copy, Set.Mem, Membership.mem, Subtype, congr_arg, Module.finrank
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
α : E
h : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
⊢ finrank.{u_3, u_4} F ↥F⟮α⟯ = finrank.{u_3, u_4} F ↥⊤

Tactic:
exact congr_arg (fun K : IntermediateField F E => finrank F K) h

Premises used: Membership.mem, Subtype, congr_arg, Module.finrank
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
α : E
rw : Ne (α := F[X]) (minpoly F α) 0
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ degree (minpoly F α) = (↑(finrank F E) : WithBot ℕ)

Tactic:
rw [degree_eq_iff_natDegree_eq, primitive_element_iff_minpoly_natDegree_eq]

Premises used: Field.primitive_element_iff_minpoly_natDegree_eq, Polynomial.degree_eq_iff_natDegree_eq
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
α : E
⊢ Ne (α := F[X]) (minpoly F α) 0

Tactic:
minpoly.ne_zero_of_finite F α

Premises used: minpoly.ne_zero_of_finite
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
α : E
⊢ Ne (α := F[X]) (minpoly F α) 0

Tactic:
exact minpoly.ne_zero_of_finite F α

Premises used: minpoly.ne_zero_of_finite
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
simp_rw : natDegree (minpoly F α) = finrank F E ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₁ :
  Fintype.card.{u_5} (↑(rootSet (minpoly F α) A) : Type u_5) = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₂ :
  (rootSet (minpoly F α) A).toFinset.card = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₃ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = finrank F E ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₄ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = Fintype.card (E →ₐ[F] A) ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₅ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) =
      Finset.card (α := E →ₐ[F] A) Finset.univ ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₆ :
  Finset.card.{u_5} (α := A) (Finset.image (fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α) Finset.univ) =
      Finset.card (α := E →ₐ[F] A) Finset.univ ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₇ :
  InjOn (β := A) (fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α) (↑Finset.univ : Set (E →ₐ[F] A)) ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₈ :
  InjOn (β := A) (fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α) univ ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α

Tactic:
simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
    (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card,
    ← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,
    ← AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff,
    Finset.coe_univ, injOn_univ]

Premises used: Algebra.IsSeparable.isSeparable, Set.toFinset_range, Finset.coe_univ, Fintype.card, Set.toFinset_card, Polynomial.card_rootSet_eq_natDegree, Field.primitive_element_iff_minpoly_natDegree_eq, Finset.card_image_iff, Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splits, AlgHom.card_of_splits, Set.injOn_univ
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
simp_rw : natDegree (minpoly F α) = finrank F E ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₁ :
  Fintype.card.{u_5} (↑(rootSet (minpoly F α) A) : Type u_5) = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₂ :
  (rootSet (minpoly F α) A).toFinset.card = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₃ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = finrank F E ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₄ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = Fintype.card (E →ₐ[F] A) ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₅ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) =
      Finset.card (α := E →ₐ[F] A) Finset.univ ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₆ :
  Finset.card.{u_5} (α := A) (Finset.image (fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α) Finset.univ) =
      Finset.card (α := E →ₐ[F] A) Finset.univ ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₇ :
  InjOn (β := A) (fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α) (↑Finset.univ : Set (E →ₐ[F] A)) ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₈ :
  InjOn (β := A) (fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α) univ ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α

Tactic:
classical
  simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
    (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card,
    ← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,
    ← AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff,
    Finset.coe_univ, injOn_univ]

Premises used: Algebra.IsSeparable.isSeparable, Set.toFinset_range, Finset.coe_univ, Fintype.card, Set.toFinset_card, Polynomial.card_rootSet_eq_natDegree, Field.primitive_element_iff_minpoly_natDegree_eq, Finset.card_image_iff, Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splits, AlgHom.card_of_splits, Set.injOn_univ
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
φ : E →ₐ[F] A
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔
    ∀ (ψ : E →ₐ[F] A), Eq.{u_5 + 1} (α := A) ((φ : (a : E) → A) α : A) ((ψ : (a : E) → A) α : A) → φ = ψ

Tactic:
⟨fun h ψ hψ ↦ (Field.primitive_element_iff_algHom_eq_of_eval' F A hA α).mp h hψ,
    fun h ↦ eq_of_le_of_finrank_eq' le_top ?_⟩

Premises used: Field.primitive_element_iff_algHom_eq_of_eval', IntermediateField.eq_of_le_of_finrank_eq', le_top, Iff.intro, Iff.mp
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
φ : E →ₐ[F] A
refine :
  ∀ (h : ∀ (ψ : E →ₐ[F] A), Eq.{u_5 + 1} (α := A) ((φ : (a : E) → A) α : A) ((ψ : (a : E) → A) α : A) → φ = ψ),
    finrank (↥F⟮α⟯) E = finrank (↥⊤) E
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔
    ∀ (ψ : E →ₐ[F] A), Eq.{u_5 + 1} (α := A) ((φ : (a : E) → A) α : A) ((ψ : (a : E) → A) α : A) → φ = ψ

Tactic:
refine ⟨fun h ψ hψ ↦ (Field.primitive_element_iff_algHom_eq_of_eval' F A hA α).mp h hψ,
    fun h ↦ eq_of_le_of_finrank_eq' le_top ?_⟩
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), Eq.{u_5 + 1} (α := A) ((φ : (a : E) → A) α : A) ((ψ : (a : E) → A) α : A) → φ = ψ
this : Algebra.{u_4, u_5} (↥F⟮α⟯) A := RingHom.toAlgebra (AlgHom.toRingHom (φ.comp (val F⟮α⟯)))
rw : ∃ (x : E →ₐ[↥F⟮α⟯] A), ∀ (y : E →ₐ[↥F⟮α⟯] A), y = x
rw₁ : ∀ (x : E), Splits (Polynomial.map (R := ↥F⟮α⟯) (algebraMap (↥F⟮α⟯) A) (minpoly (↥F⟮α⟯) x))
⊢ finrank (↥F⟮α⟯) E = finrank (↥⊤) E

Tactic:
rw [IntermediateField.finrank_top, ← AlgHom.card_of_splits _ _ A, Fintype.card_eq_one_iff]

Premises used: IntermediateField.finrank_top, AlgHom.card_of_splits, Fintype.card_eq_one_iff
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), Eq.{u_5 + 1} (α := A) ((φ : (a : E) → A) α : A) ((ψ : (a : E) → A) α : A) → φ = ψ
this : Algebra.{u_4, u_5} (↥F⟮α⟯) A := RingHom.toAlgebra (AlgHom.toRingHom (φ.comp (val F⟮α⟯)))
⊢ ∃ (x : E →ₐ[↥F⟮α⟯] A), ∀ (y : E →ₐ[↥F⟮α⟯] A), y = x

Tactic:
⟨{ __ := φ, commutes' := fun _ ↦ rfl }, fun ψ ↦ AlgHom.restrictScalars_injective F <|
      Eq.symm <| h _ (ψ.commutes <| AdjoinSimple.gen F α).symm⟩

Premises used: IntermediateField.AdjoinSimple.gen, AlgHom.restrictScalars_injective, AlgHom.restrictScalars, AlgHom.toRingHom, AlgHom.commutes, Exists.intro, AlgHom.mk, Eq.symm, rfl
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), Eq.{u_5 + 1} (α := A) ((φ : (a : E) → A) α : A) ((ψ : (a : E) → A) α : A) → φ = ψ
this : Algebra.{u_4, u_5} (↥F⟮α⟯) A := RingHom.toAlgebra (AlgHom.toRingHom (φ.comp (val F⟮α⟯)))
⊢ ∃ (x : E →ₐ[↥F⟮α⟯] A), ∀ (y : E →ₐ[↥F⟮α⟯] A), y = x

Tactic:
exact ⟨{ __ := φ, commutes' := fun _ ↦ rfl }, fun ψ ↦ AlgHom.restrictScalars_injective F <|
      Eq.symm <| h _ (ψ.commutes <| AdjoinSimple.gen F α).symm⟩
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), Eq.{u_5 + 1} (α := A) ((φ : (a : E) → A) α : A) ((ψ : (a : E) → A) α : A) → φ = ψ
this : Algebra.{u_4, u_5} (↥F⟮α⟯) A := RingHom.toAlgebra (AlgHom.toRingHom (φ.comp (val F⟮α⟯)))
⊢ ∀ (x : E), Splits (Polynomial.map (R := ↥F⟮α⟯) (algebraMap (↥F⟮α⟯) A) (minpoly (↥F⟮α⟯) x))

Tactic:
fun x ↦ (IsIntegral.of_finite F x).minpoly_splits_tower_top (hA x)

Premises used: IsIntegral.of_finite, IsIntegral.minpoly_splits_tower_top
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), Eq.{u_5 + 1} (α := A) ((φ : (a : E) → A) α : A) ((ψ : (a : E) → A) α : A) → φ = ψ
this : Algebra.{u_4, u_5} (↥F⟮α⟯) A := RingHom.toAlgebra (AlgHom.toRingHom (φ.comp (val F⟮α⟯)))
⊢ ∀ (x : E), Splits (Polynomial.map (R := ↥F⟮α⟯) (algebraMap (↥F⟮α⟯) A) (minpoly (↥F⟮α⟯) x))

Tactic:
exact fun x ↦ (IsIntegral.of_finite F x).minpoly_splits_tower_top (hA x)

Premises used: IsIntegral.of_finite, IsIntegral.minpoly_splits_tower_top
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s_1 t : Set M
y : N
s : Set M
u v : N
hu :
  Membership.mem (γ := Set N)
    {y : N |
      ∀ ⦃x : M⦄, x ∈ s → LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)}
    u
hv :
  Membership.mem (γ := Set N)
    {y : N |
      ∀ ⦃x : M⦄, x ∈ s → LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)}
    v
x : M
hx : x ∈ s
rw :
  0 ≤
    HAdd.hAdd (α := R) (β := R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) u : R)
      ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) v : R)
⊢ LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) (u + v) : R)

Tactic:
rw [map_add]

Premises used: map_add
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s_1 t : Set M
y : N
s : Set M
u v : N
hu :
  Membership.mem (γ := Set N)
    {y : N |
      ∀ ⦃x : M⦄, x ∈ s → LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)}
    u
hv :
  Membership.mem (γ := Set N)
    {y : N |
      ∀ ⦃x : M⦄, x ∈ s → LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)}
    v
x : M
hx : x ∈ s
⊢ 0 ≤
    HAdd.hAdd (α := R) (β := R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) u : R)
      ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) v : R)

Tactic:
add_nonneg (hu hx) (hv hx)

Premises used: add_nonneg
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s_1 t : Set M
y : N
s : Set M
u v : N
hu :
  Membership.mem (γ := Set N)
    {y : N |
      ∀ ⦃x : M⦄, x ∈ s → LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)}
    u
hv :
  Membership.mem (γ := Set N)
    {y : N |
      ∀ ⦃x : M⦄, x ∈ s → LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)}
    v
x : M
hx : x ∈ s
⊢ 0 ≤
    HAdd.hAdd (α := R) (β := R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) u : R)
      ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) v : R)

Tactic:
exact add_nonneg (hu hx) (hv hx)

Premises used: add_nonneg
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s_1 t : Set M
y : N
s : Set M
⊢ Membership.mem (γ := Set N)
    {y : N |
      ∀ ⦃x : M⦄, x ∈ s → LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)}
    0

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s_1 t : Set M
y_1 : N
s : Set M
c : R≥0
y : N
hy :
  Membership.mem (γ := Set N)
    {y : N |
      ∀ ⦃x : M⦄, x ∈ s → LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)}
    y
x : M
hx : x ∈ s
rw : 0 ≤ HSMul.hSMul (β := R) (↑c : R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)
⊢ LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) (c • y) : R)

Tactic:
rw [← Nonneg.coe_smul, map_smul]

Premises used: Nonneg.coe_smul, map_smul
-- Module: Mathlib.Geometry.Convex.Cone.Dual
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s_1 t : Set M
y_1 : N
s : Set M
c : R≥0
y : N
hy :
  Membership.mem (γ := Set N)
    {y : N |
      ∀ ⦃x : M⦄, x ∈ s → LE.le.{u_1} (α := R) (0 : R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)}
    y
x : M
hx : x ∈ s
⊢ 0 ≤ HSMul.hSMul (β := R) (↑c : R) ((((p : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) y : R)

Tactic:
mul_nonneg c.2 (hy hx)

Premises used: mul_nonneg, Subtype.property