awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.EssFiniteType F E
d : (s : Finset E) → ℕ := fun (s : Finset E) ↦ finInsepDegree (↥(adjoin F (↑s : Set E))) E
Hexists :
  Set.Nonempty.{v} (α := Finset E)
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
s : Finset E :=
  Function.argminOn d
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))} Hexists
hs :
  Membership.mem (γ := Set (Finset E))
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
    (Function.argminOn d
      {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))} Hexists)
t : Finset E
ht :
  IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ (↑t : Set E) }) F
    (Subtype.val (p := fun (x : E) ↦ x ∈ (↑t : Set E)))
H :
  LT.lt.{v} (α := IntermediateField F E)
    ((fun (t : Set E) ↦
        (restrictScalars F (L' := ↥(adjoin F t)) (separableClosure (↥(adjoin F t)) E) : IntermediateField F E))
      (↑s : Set E))
    ((fun (t : Set E) ↦
        (restrictScalars F (L' := ↥(adjoin F t)) (separableClosure (↥(adjoin F t)) E) : IntermediateField F E))
      (↑t : Set E))
this_1 : Module.Finite (↥(adjoin F (↑s : Set E))) E
this :
  Module.Finite (↥(restrictScalars F (L' := ↥(adjoin F (↑s : Set E))) (separableClosure (↥(adjoin F (↑s : Set E))) E)))
    E
⊢ d t <
    d
      (Function.argminOn d
        {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))} ⋯)

Tactic:
apply finrank_lt_of_gt H

Premises used: IntermediateField.finrank_lt_of_gt
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.EssFiniteType F E
d : (s : Finset E) → ℕ := fun (s : Finset E) ↦ finInsepDegree (↥(adjoin F (↑s : Set E))) E
Hexists :
  Set.Nonempty.{v} (α := Finset E)
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
s : Finset E :=
  Function.argminOn d
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))} Hexists
hs :
  Membership.mem (γ := Set (Finset E))
    {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))}
    (Function.argminOn d
      {s : Finset E | IsTranscendenceBasis.{v, u, v} (ι := ↥s) F (Subtype.val (p := fun (x : E) ↦ x ∈ s))} Hexists)
t : Finset E
ht :
  IsTranscendenceBasis.{v, u, v} (ι := { x : E // x ∈ (↑t : Set E) }) F
    (Subtype.val (p := fun (x : E) ↦ x ∈ (↑t : Set E)))
H :
  LT.lt.{v} (α := IntermediateField F E)
    ((fun (t : Set E) ↦
        (restrictScalars F (L' := ↥(adjoin F t)) (separableClosure (↥(adjoin F t)) E) : IntermediateField F E))
      (↑s : Set E))
    ((fun (t : Set E) ↦
        (restrictScalars F (L' := ↥(adjoin F t)) (separableClosure (↥(adjoin F t)) E) : IntermediateField F E))
      (↑t : Set E))
this_1 : Module.Finite (↥(adjoin F (↑s : Set E))) E
this :
  Module.Finite (↥(restrictScalars F (L' := ↥(adjoin F (↑s : Set E))) (separableClosure (↥(adjoin F (↑s : Set E))) E)))
    E
⊢ False

Tactic:
exact d.not_lt_argminOn _ ht (by apply finrank_lt_of_gt H)

Premises used: Function.not_lt_argminOn
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ Cardinal.lift.{u, v} (sepDegree F ↥⊥) = Cardinal.lift.{v, u} (sepDegree F F)

Tactic:
have := lift_sepDegree_eq_of_equiv _ _ _ (botEquiv F E)
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
this : Cardinal.lift.{u, v} (sepDegree F ↥⊥) = Cardinal.lift.{v, u} (sepDegree F F)
rwa : ∀ (this : Cardinal.lift.{u, v} (sepDegree F ↥⊥) = Cardinal.lift.{v, u} 1), sepDegree F ↥⊥ = 1
rwa₁ : ∀ (this : Cardinal.lift.{u, v} (sepDegree F ↥⊥) = 1), sepDegree F ↥⊥ = 1
rwa₂ : ∀ (this : Cardinal.lift.{u, v} (sepDegree F ↥⊥) = Cardinal.lift.{u, v} 1), sepDegree F ↥⊥ = 1
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (this : sepDegree F ↥⊥ = 1), sepDegree F ↥⊥ = 1
⊢ sepDegree F ↥⊥ = 1

Tactic:
rwa [sepDegree_self, Cardinal.lift_one, ← Cardinal.lift_one.{v, u}, Cardinal.lift_inj] at this

Premises used: Field.sepDegree_self, Cardinal.lift_inj, Cardinal.lift_one
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ Cardinal.lift.{u, v} (insepDegree F ↥⊥) = Cardinal.lift.{v, u} (insepDegree F F)

Tactic:
have := lift_insepDegree_eq_of_equiv _ _ _ (botEquiv F E)
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
this : Cardinal.lift.{u, v} (insepDegree F ↥⊥) = Cardinal.lift.{v, u} (insepDegree F F)
rwa : ∀ (this : Cardinal.lift.{u, v} (insepDegree F ↥⊥) = Cardinal.lift.{v, u} 1), insepDegree F ↥⊥ = 1
rwa₁ : ∀ (this : Cardinal.lift.{u, v} (insepDegree F ↥⊥) = 1), insepDegree F ↥⊥ = 1
rwa₂ : ∀ (this : Cardinal.lift.{u, v} (insepDegree F ↥⊥) = Cardinal.lift.{u, v} 1), insepDegree F ↥⊥ = 1
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (this : insepDegree F ↥⊥ = 1), insepDegree F ↥⊥ = 1
⊢ insepDegree F ↥⊥ = 1

Tactic:
rwa [insepDegree_self, Cardinal.lift_one, ← Cardinal.lift_one.{v, u}, Cardinal.lift_inj] at this

Premises used: Cardinal.lift_inj, Field.insepDegree_self, Cardinal.lift_one
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rw : finInsepDegree F F = 1
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ finInsepDegree.{u, v} F ↥⊥ = 1

Tactic:
rw [finInsepDegree_eq_of_equiv _ _ _ (botEquiv F E), finInsepDegree_self]

Premises used: Field.finInsepDegree_self, Field.finInsepDegree_eq_of_equiv, IntermediateField.botEquiv
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
⊢ Cardinal.lift.{v, w} (sepDegree F ↥⊥) = Cardinal.lift.{w, v} (sepDegree F E)

Tactic:
lift_sepDegree_eq_of_equiv _ _ _ ((botEquiv E K).restrictScalars F)

Premises used: AlgEquiv.restrictScalars, Field.lift_sepDegree_eq_of_equiv, IntermediateField.botEquiv
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
⊢ Cardinal.lift.{v, w} (insepDegree F ↥⊥) = Cardinal.lift.{w, v} (insepDegree F E)

Tactic:
lift_insepDegree_eq_of_equiv _ _ _ ((botEquiv E K).restrictScalars F)

Premises used: AlgEquiv.restrictScalars, Field.lift_insepDegree_eq_of_equiv, IntermediateField.botEquiv
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
⊢ finInsepDegree.{u, w} F ↥⊥ = finInsepDegree F E

Tactic:
simpa only [Cardinal.toNat_lift] using congr_arg Cardinal.toNat (lift_insepDegree_bot' F E K)

Premises used: IntermediateField.lift_insepDegree_bot', Cardinal.toNat, Cardinal.toNat_lift, congr_arg, DFunLike.coe
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
⊢ sepDegree F ↥⊤ = sepDegree F K

Tactic:
sepDegree_eq_of_equiv _ _ _ ((topEquiv (F := E) (E := K)).restrictScalars F)

Premises used: AlgEquiv.restrictScalars, Field.sepDegree_eq_of_equiv, IntermediateField.topEquiv
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
⊢ insepDegree F ↥⊤ = insepDegree F K

Tactic:
insepDegree_eq_of_equiv _ _ _ ((topEquiv (F := E) (E := K)).restrictScalars F)

Premises used: Field.insepDegree_eq_of_equiv, AlgEquiv.restrictScalars, IntermediateField.topEquiv
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
rw : (Cardinal.toNat : (a : Cardinal.{w}) → ℕ) (insepDegree F ↥⊤) = finInsepDegree F K
rw₁ : (Cardinal.toNat : (a : Cardinal.{w}) → ℕ) (insepDegree F K) = finInsepDegree F K
rw₂ rw₃ : finInsepDegree F K = finInsepDegree F K
⊢ finInsepDegree.{u, w} F ↥⊤ = finInsepDegree F K

Tactic:
rw [finInsepDegree_def', insepDegree_top, ← finInsepDegree_def']

Premises used: Field.finInsepDegree_def', IntermediateField.insepDegree_top
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type v
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
⊢ sepDegree F ↥⊥ = sepDegree F E

Tactic:
sepDegree_eq_of_equiv _ _ _ ((botEquiv E K).restrictScalars F)

Premises used: AlgEquiv.restrictScalars, IntermediateField.botEquiv, Field.sepDegree_eq_of_equiv
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type v
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
⊢ insepDegree F ↥⊥ = insepDegree F E

Tactic:
insepDegree_eq_of_equiv _ _ _ ((botEquiv E K).restrictScalars F)

Premises used: Field.insepDegree_eq_of_equiv, AlgEquiv.restrictScalars, IntermediateField.botEquiv
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type v
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
this : Algebra ↥(separableClosure F K) ↥(restrictScalars F (separableClosure E K)) :=
  RingHom.toAlgebra (AlgHom.toRingHom (inclusion ⋯))
⊢ IsScalarTower (↥(separableClosure F K)) (↥(restrictScalars F (separableClosure E K))) K

Tactic:
have : IsScalarTower (separableClosure F K) ((separableClosure E K).restrictScalars F) K :=
    .of_algebraMap_eq' rfl
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type v
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
this_1 : Algebra ↥(separableClosure F K) ↥(restrictScalars F (separableClosure E K)) :=
  RingHom.toAlgebra (AlgHom.toRingHom (inclusion ⋯))
this : IsScalarTower (↥(separableClosure F K)) (↥(restrictScalars F (separableClosure E K))) K
⊢ insepDegree E K ≤ insepDegree F K

Tactic:
Module.rank_top_le_rank_of_isScalarTower
    (separableClosure F K) ((separableClosure E K).restrictScalars F) K

Premises used: IntermediateField.restrictScalars, Set.Mem, setOf, Module.rank_top_le_rank_of_isScalarTower, Membership.mem, Field.insepDegree, Subtype, IsSeparable, Polynomial.Separable, separableClosure, IsCoprime
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type v
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
this_1 : Algebra ↥(separableClosure F K) ↥(restrictScalars F (separableClosure E K)) :=
  RingHom.toAlgebra (AlgHom.toRingHom (inclusion ⋯))
this : IsScalarTower (↥(separableClosure F K)) (↥(restrictScalars F (separableClosure E K))) K
⊢ insepDegree E K ≤ insepDegree F K

Tactic:
exact Module.rank_top_le_rank_of_isScalarTower
    (separableClosure F K) ((separableClosure E K).restrictScalars F) K

Premises used: IntermediateField.restrictScalars, Module.rank_top_le_rank_of_isScalarTower, Membership.mem, Subtype, separableClosure
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
E₁ E₂ : IntermediateField F K
H : E₁ ≤ E₂
this : Algebra ↥E₁ ↥E₂ := (inclusion H).toAlgebra
⊢ IsScalarTower (↥E₁) (↥E₂) K

Tactic:
have : IsScalarTower E₁ E₂ K := .of_algebraMap_eq' rfl
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
E₁ E₂ : IntermediateField F K
H : E₁ ≤ E₂
this_1 : Algebra ↥E₁ ↥E₂ := (inclusion H).toAlgebra
this : IsScalarTower (↥E₁) (↥E₂) K
⊢ insepDegree (↥E₂) K ≤ insepDegree (↥E₁) K

Tactic:
insepDegree_top_le_insepDegree_of_isScalarTower _ _ _

Premises used: Field.insepDegree_top_le_insepDegree_of_isScalarTower
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
E₁ E₂ : IntermediateField F K
H : E₁ ≤ E₂
this_1 : Algebra ↥E₁ ↥E₂ := (inclusion H).toAlgebra
this : IsScalarTower (↥E₁) (↥E₂) K
⊢ insepDegree (↥E₂) K ≤ insepDegree (↥E₁) K

Tactic:
exact insepDegree_top_le_insepDegree_of_isScalarTower _ _ _

Premises used: Field.insepDegree_top_le_insepDegree_of_isScalarTower
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type v
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Module.Finite F K
this : Algebra ↥(separableClosure F K) ↥(restrictScalars F (separableClosure E K)) :=
  RingHom.toAlgebra (AlgHom.toRingHom (inclusion ⋯))
⊢ IsScalarTower (↥(separableClosure F K)) (↥(restrictScalars F (separableClosure E K))) K

Tactic:
have : IsScalarTower (separableClosure F K) ((separableClosure E K).restrictScalars F) K :=
    .of_algebraMap_eq' rfl
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type v
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Module.Finite F K
this_1 : Algebra ↥(separableClosure F K) ↥(restrictScalars F (separableClosure E K)) :=
  RingHom.toAlgebra (AlgHom.toRingHom (inclusion ⋯))
this : IsScalarTower (↥(separableClosure F K)) (↥(restrictScalars F (separableClosure E K))) K
⊢ finInsepDegree E K ≤ finInsepDegree F K

Tactic:
exact Module.finrank_top_le_finrank_of_isScalarTower
    (separableClosure F K) ((separableClosure E K).restrictScalars F) K

Premises used: IntermediateField.restrictScalars, Module.finrank_top_le_finrank_of_isScalarTower, Membership.mem, Subtype, separableClosure
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
E₁ E₂ : IntermediateField F K
H : E₁ ≤ E₂
inst_3 : Module.Finite (↥E₁) K
this : Algebra ↥E₁ ↥E₂ := (inclusion H).toAlgebra
⊢ IsScalarTower (↥E₁) (↥E₂) K

Tactic:
have : IsScalarTower E₁ E₂ K := .of_algebraMap_eq' rfl
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
E₁ E₂ : IntermediateField F K
H : E₁ ≤ E₂
inst_3 : Module.Finite (↥E₁) K
this_1 : Algebra ↥E₁ ↥E₂ := (inclusion H).toAlgebra
this : IsScalarTower (↥E₁) (↥E₂) K
⊢ finInsepDegree (↥E₂) K ≤ finInsepDegree (↥E₁) K

Tactic:
finInsepDegree_top_le_finInsepDegree_of_isScalarTower _ _ _

Premises used: Field.finInsepDegree_top_le_finInsepDegree_of_isScalarTower
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
E₁ E₂ : IntermediateField F K
H : E₁ ≤ E₂
inst_3 : Module.Finite (↥E₁) K
this_1 : Algebra ↥E₁ ↥E₂ := (inclusion H).toAlgebra
this : IsScalarTower (↥E₁) (↥E₂) K
⊢ finInsepDegree (↥E₂) K ≤ finInsepDegree (↥E₁) K

Tactic:
exact finInsepDegree_top_le_finInsepDegree_of_isScalarTower _ _ _

Premises used: Field.finInsepDegree_top_le_finInsepDegree_of_isScalarTower
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
rw : Module.rank F ↥(separableClosure F E) = Module.rank F E
rw₁ : Module.rank F ↥⊤ = Module.rank F E
rw₂ rw₃ : Module.rank F E = Module.rank F E
⊢ sepDegree F E = Module.rank F E

Tactic:
rw [sepDegree, (separableClosure.eq_top_iff F E).2 ‹_›, IntermediateField.rank_top']

Premises used: Iff.mpr, Field.sepDegree, separableClosure.eq_top_iff, IntermediateField.rank_top'
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
rw : Module.rank (↥(separableClosure F E)) E = 1
rw₁ : Module.rank (↥⊤) E = 1
rw₂ rw₃ : Eq.{v + 2} (α := Cardinal.{v}) 1 1
⊢ insepDegree F E = 1

Tactic:
rw [insepDegree, (separableClosure.eq_top_iff F E).2 ‹_›, IntermediateField.rank_top]

Premises used: Iff.mpr, Field.insepDegree, IntermediateField.rank_top, separableClosure.eq_top_iff
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
⊢ finInsepDegree F E = 1

Tactic:
Cardinal.one_toNat ▸ congr(Cardinal.toNat $(insepDegree_eq F E))

Premises used: congrArg, Cardinal.toNat, Eq.rec, id, Algebra.IsSeparable.insepDegree_eq, DFunLike.coe, Cardinal.one_toNat
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : FiniteDimensional F E
⊢ NeZero (finSepDegree F E)

Tactic:
⟨Nat.card_ne_zero.2 ⟨inferInstance, Fintype.finite <| minpoly.AlgHom.fintype _ _ _⟩⟩

Premises used: Iff.mpr, NeZero.mk, Fintype.finite, inferInstance, minpoly.AlgHom.fintype, And.intro, Nat.card_ne_zero
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E ≃ₐ[F] K
x : Algebra E K := (↑i : E →ₐ[F] K).toAlgebra
isAlgebraic : ∀ (x_1 : K), IsAlgebraic E x_1
⊢ Algebra.IsAlgebraic E K

Tactic:
constructor
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E ≃ₐ[F] K
x_1 : Algebra E K := (↑i : E →ₐ[F] K).toAlgebra
x : K
⊢ IsAlgebraic.{v, w} E (A := K) ((algebraMap E K : (a : E) → K) (((↑i.symm : K →ₐ[F] E) : (a : K) → E) x : E) : K)

Tactic:
have h := isAlgebraic_algebraMap (R := E) (A := K) (i.symm.toAlgHom x)
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E ≃ₐ[F] K
x_1 : Algebra E K := (↑i : E →ₐ[F] K).toAlgebra
x : K
h : IsAlgebraic.{v, w} E (A := K) ((algebraMap E K : (a : E) → K) (((↑i.symm : K →ₐ[F] E) : (a : K) → E) x : E) : K)
⊢ IsAlgebraic.{v, w} E (A := K) (((↑i : E →ₐ[F] K) : (a : E) → K) (((↑i.symm : K →ₐ[F] E) : (a : K) → E) x : E) : K)

Tactic:
rw [show ∀ y : E, (algebraMap E K) y = i.toAlgHom y from fun y ↦ rfl] at h

Premises used: rfl
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E ≃ₐ[F] K
x_1 : Algebra E K := (↑i : E →ₐ[F] K).toAlgebra
x : K
h : IsAlgebraic.{v, w} E (A := K) (((↑i : E →ₐ[F] K) : (a : E) → K) (((↑i.symm : K →ₐ[F] E) : (a : K) → E) x : E) : K)
⊢ IsAlgebraic E x

Tactic:
simpa only [AlgEquiv.coe_algHom, AlgEquiv.apply_symm_apply] using h

Premises used: AlgEquiv.apply_symm_apply, AlgEquiv.coe_algHom
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E ≃ₐ[F] K
x : Algebra E K := (↑i : E →ₐ[F] K).toAlgebra
⊢ Algebra.IsAlgebraic E K

Tactic:
have : Algebra.IsAlgebraic E K := by
    constructor
    intro x
    have h := isAlgebraic_algebraMap (R := E) (A := K) (i.symm.toAlgHom x)
    rw [show ∀ y : E, (algebraMap E K) y = i.toAlgHom y from fun y ↦ rfl] at h
    simpa only [AlgEquiv.coe_algHom, AlgEquiv.apply_symm_apply] using h
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E ≃ₐ[F] K
x : Algebra E K := (↑i : E →ₐ[F] K).toAlgebra
this : Algebra.IsAlgebraic E K
apply : AlgEquiv.{v, w, v} E (AlgebraicClosure K) (AlgebraicClosure E)
⊢ AlgEquiv.{u, w, v} F (AlgebraicClosure K) (AlgebraicClosure E)

Tactic:
apply AlgEquiv.restrictScalars (R := F) (S := E)

Premises used: AlgEquiv.restrictScalars
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E ≃ₐ[F] K
x : Algebra E K := (↑i : E →ₐ[F] K).toAlgebra
this : Algebra.IsAlgebraic E K
⊢ AlgEquiv.{v, w, v} E (AlgebraicClosure K) (AlgebraicClosure E)

Tactic:
exact IsAlgClosure.equivOfAlgebraic E K (AlgebraicClosure K) (AlgebraicClosure E)

Premises used: IsAlgClosure.equivOfAlgebraic, AlgebraicClosure
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E ≃ₐ[F] K
⊢ finSepDegree F E = finSepDegree F K

Tactic:
Nat.card_congr (embEquivOfEquiv F E K i)

Premises used: Field.embEquivOfEquiv, Field.finSepDegree, Nat.card_congr
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
rw : Subsingleton.{u + 1} (Emb F F) ∧ Nonempty.{u + 1} (Emb F F)
⊢ finSepDegree F F = 1

Tactic:
rw [finSepDegree, Nat.card_eq_one_iff_unique]

Premises used: Field.finSepDegree, Nat.card_eq_one_iff_unique
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
left : Subsingleton.{u + 1} (Emb F F)
right : Nonempty.{u + 1} (Emb F F)
⊢ Subsingleton.{u + 1} (Emb F F) ∧ Nonempty.{u + 1} (Emb F F)

Tactic:
constructor
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
⊢ Subsingleton.{u + 1} (Emb F F)

Tactic:
infer_instance
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
⊢ Nonempty.{u + 1} (Emb F F)

Tactic:
infer_instance
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rw : finSepDegree F F = 1
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ finSepDegree.{u, v} F ↥⊥ = 1

Tactic:
rw [finSepDegree_eq_of_equiv _ _ _ (botEquiv F E), finSepDegree_self]

Premises used: Field.finSepDegree_eq_of_equiv, Field.finSepDegree_self, IntermediateField.botEquiv
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
⊢ finSepDegree.{u, w} F ↥⊥ = finSepDegree F E

Tactic:
finSepDegree_eq_of_equiv _ _ _ ((botEquiv E K).restrictScalars F)

Premises used: Field.finSepDegree_eq_of_equiv, AlgEquiv.restrictScalars, IntermediateField.botEquiv
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
⊢ finSepDegree.{u, w} F ↥⊤ = finSepDegree F K

Tactic:
finSepDegree_eq_of_equiv _ _ _ ((topEquiv (F := E) (E := K)).restrictScalars F)

Premises used: Field.finSepDegree_eq_of_equiv, AlgEquiv.restrictScalars, IntermediateField.topEquiv
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
S : Set E
hS : Eq (α := IntermediateField F E) (adjoin F S) ⊤
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (Polynomial.map (algebraMap F K) (minpoly F s))
⊢ finSepDegree F E = Nat.card (E →ₐ[F] K)

Tactic:
Nat.card_congr (embEquivOfAdjoinSplits F E K hS hK)

Premises used: Field.finSepDegree, Nat.card_congr, Field.embEquivOfAdjoinSplits