awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
a : (Module.rank F E).ord.ToType
hi : IsSuccPrelimit (↑a : WithTop (Module.rank F E).ord.ToType)
j : (Module.rank F E).ord.ToType
hj : j ∈ Iio a
coe :
  Membership.mem (γ := Set E) ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio (j⁺))
    (((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ) j)
coe₁ : (↑j : WithTop (Module.rank F E).ord.ToType)⁺ ∈ Iio (↑a : WithTop (Module.rank F E).ord.ToType)
⊢ ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ) j ∈
    (↑(⨆ (j : (↑(Iio (↑a : WithTop (Module.rank F E).ord.ToType)) : Type v)),
          (filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
            (↑j : WithTop (Module.rank F E).ord.ToType)) :
      Set E)

Tactic:
refine le_iSup (α := IntermediateField F E) _ ⟨j⁺, ?_⟩ (subset_adjoin F _ ?_)

Premises used: le_iSup, IntermediateField.subset_adjoin
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
a : (Module.rank F E).ord.ToType
hi : IsSuccPrelimit (↑a : WithTop (Module.rank F E).ord.ToType)
j : (Module.rank F E).ord.ToType
hj : j ∈ Iio a
⊢ Membership.mem (γ := Set E) ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio (j⁺))
    (((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ) j)

Tactic:
⟨j, lt_succ j, rfl⟩

Premises used: Set.Mem, setOf, Order.lt_succ, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
a : (Module.rank F E).ord.ToType
hi : IsSuccPrelimit (↑a : WithTop (Module.rank F E).ord.ToType)
j : (Module.rank F E).ord.ToType
hj : j ∈ Iio a
⊢ (↑j : WithTop (Module.rank F E).ord.ToType)⁺ ∈ Iio (↑a : WithTop (Module.rank F E).ord.ToType)

Tactic:
hi.succ_lt (coe_lt_coe.mpr hj)

Premises used: Iff.mpr, Set.Mem, setOf, WithTop.coe_lt_coe, Order.IsSuccPrelimit.succ_lt, Set.Iio
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
a : (Module.rank F E).ord.ToType
hi : IsSuccPrelimit (↑a : WithTop (Module.rank F E).ord.ToType)
j : (Module.rank F E).ord.ToType
hj : j ∈ Iio a
⊢ Membership.mem (γ := Set E) ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio (j⁺))
    (((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ) j)

Tactic:
exacts [⟨j, lt_succ j, rfl⟩, hi.succ_lt (coe_lt_coe.mpr hj)]

Premises used: Iff.mpr, WithTop.coe_lt_coe, Order.IsSuccPrelimit.succ_lt
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
hi_1 : IsSuccPrelimit i
hi : ¬Nonempty.{v + 1} (↑(Iio i) : Type v)
top :
  ∀ (hi : IsSuccPrelimit.{v} (α := WithTop (Module.rank F E).ord.ToType) ⊤)
    (hi : ¬Nonempty.{v + 1} (↑(Iio ⊤) : Type v)),
    Eq.{v + 1} (α := IntermediateField F E)
      ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) ⊤ : IntermediateField F E)
      (⊥ : IntermediateField F E)
coe :
  ∀ (a : (Module.rank F E).ord.ToType) (hi : IsSuccPrelimit (↑a : WithTop (Module.rank F E).ord.ToType))
    (hi : ¬Nonempty.{v + 1} (↑(Iio (↑a : WithTop (Module.rank F E).ord.ToType)) : Type v)),
    Eq (α := IntermediateField F E)
      ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
          (↑a : WithTop (Module.rank F E).ord.ToType) :
        IntermediateField F E)
      (⊥ : IntermediateField F E)
⊢ Eq (α := IntermediateField F E)
    ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i : IntermediateField F E)
    (⊥ : IntermediateField F E)

Tactic:
cases i
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
hi_1 : IsSuccPrelimit.{v} (α := WithTop (Module.rank F E).ord.ToType) ⊤
hi : ¬Nonempty.{v + 1} (↑(Iio ⊤) : Type v)
⊢ Nonempty.{v + 1} (Module.rank F E).ord.ToType

Tactic:
have := mk_ne_zero_iff.mp (rank_pos.trans_eq (mk_ord_toType <| Module.rank F E).symm).ne'
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
hi_1 : IsSuccPrelimit.{v} (α := WithTop (Module.rank F E).ord.ToType) ⊤
hi : ¬Nonempty.{v + 1} (↑(Iio ⊤) : Type v)
this : Nonempty.{v + 1} (Module.rank F E).ord.ToType
⊢ ¬Nonempty.{v + 1} (↑(range WithTop.some) : Type v)

Tactic:
rw [← range_coe] at hi

Premises used: WithTop.range_coe
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
hi_1 : IsSuccPrelimit.{v} (α := WithTop (Module.rank F E).ord.ToType) ⊤
hi : ¬Nonempty.{v + 1} (↑(Iio ⊤) : Type v)
this : Nonempty.{v + 1} (Module.rank F E).ord.ToType
hi₁ : ¬Nonempty.{v + 1} (↑(range WithTop.some) : Type v)
⊢ Nonempty.{v + 1} (Module.rank F E).ord.ToType

Tactic:
rw [← range_coe] at hi

Premises used: WithTop.range_coe
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
hi_1 : IsSuccPrelimit.{v} (α := WithTop (Module.rank F E).ord.ToType) ⊤
hi : ¬Nonempty.{v + 1} (↑(range WithTop.some) : Type v)
this : Nonempty.{v + 1} (Module.rank F E).ord.ToType
⊢ Eq.{v + 1} (α := IntermediateField F E)
    ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) ⊤ : IntermediateField F E)
    (⊥ : IntermediateField F E)

Tactic:
(hi inferInstance).elim

Premises used: False.elim, inferInstance
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
hi_1 : IsSuccPrelimit.{v} (α := WithTop (Module.rank F E).ord.ToType) ⊤
hi : ¬Nonempty.{v + 1} (↑(range WithTop.some) : Type v)
this : Nonempty.{v + 1} (Module.rank F E).ord.ToType
⊢ Eq.{v + 1} (α := IntermediateField F E)
    ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) ⊤ : IntermediateField F E)
    (⊥ : IntermediateField F E)

Tactic:
exact (hi inferInstance).elim

Premises used: False.elim, inferInstance
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
a : (Module.rank F E).ord.ToType
hi_1 : IsSuccPrelimit (↑a : WithTop (Module.rank F E).ord.ToType)
hi : ¬Nonempty.{v + 1} (↑(Iio (↑a : WithTop (Module.rank F E).ord.ToType)) : Type v)
⊢ Eq (α := IntermediateField F E)
    ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
        (↑a : WithTop (Module.rank F E).ord.ToType) :
      IntermediateField F E)
    (⊥ : IntermediateField F E)

Tactic:
bot_unique <| adjoin_le_iff.mpr fun _ ⟨j, hj, _⟩ ↦ (hi ⟨j, coe_lt_coe.mpr hj⟩).elim

Premises used: _private.0.Field.Emb.Cardinal.eq_bot_of_not_nonempty.match_1, Iff.mpr, IntermediateField.adjoin_le_iff, False.elim, Membership.mem, Bot.bot, Nonempty.intro, WithTop.some, Subtype.mk, WithTop.coe_lt_coe, SetLike.coe, bot_unique
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
a : (Module.rank F E).ord.ToType
hi_1 : IsSuccPrelimit (↑a : WithTop (Module.rank F E).ord.ToType)
hi : ¬Nonempty.{v + 1} (↑(Iio (↑a : WithTop (Module.rank F E).ord.ToType)) : Type v)
⊢ Eq (α := IntermediateField F E)
    ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
        (↑a : WithTop (Module.rank F E).ord.ToType) :
      IntermediateField F E)
    (⊥ : IntermediateField F E)

Tactic:
exact bot_unique <| adjoin_le_iff.mpr fun _ ⟨j, hj, _⟩ ↦ (hi ⟨j, coe_lt_coe.mpr hj⟩).elim

Premises used: bot_unique
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
f :
  (↑(limit (F := fun (j : WithTop (Module.rank F E).ord.ToType) ↦
        ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) j :
              IntermediateField F E) →ₐ[F]
          Ē)
        (embFunctor F E) i) :
    Type v)
h : Nonempty.{v + 1} (↑(Iio i) : Type v)
rw :
  LE.le.{v} (α := Subalgebra F E)
    (toSubalgebra
      (⨆ (j : (↑(Iio i) : Type v)),
        (filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
          (↑j : WithTop (Module.rank F E).ord.ToType)))
    (⨆ (x : (↑(Iio i) : Type v)),
      toSubalgebra
        ((fun (j : (↑(Iio i) : Type v)) ↦
            ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                (↑j : WithTop (Module.rank F E).ord.ToType) :
              IntermediateField F E))
          x))
rw₁ rw₂ :
  LE.le.{v} (α := Subalgebra F E)
    (⨆ (i_1 : (↑(Iio i) : Type v)),
      toSubalgebra
        ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
          (↑i_1 : WithTop (Module.rank F E).ord.ToType)))
    (⨆ (i_1 : (↑(Iio i) : Type v)),
      toSubalgebra
        ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
          (↑i_1 : WithTop (Module.rank F E).ord.ToType)))
⊢ LE.le.{v} (α := Subalgebra F E)
    (toSubalgebra ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i))
    (⨆ (x : (↑(Iio i) : Type v)),
      toSubalgebra
        ((fun (j : (↑(Iio i) : Type v)) ↦
            ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                (↑j : WithTop (Module.rank F E).ord.ToType) :
              IntermediateField F E))
          x))

Tactic:
rw [← iSup_filtration hi, toSubalgebra_iSup_of_directed directed_filtration]

Premises used: Field.Emb.Cardinal.directed_filtration, IntermediateField.toSubalgebra_iSup_of_directed, Field.Emb.Cardinal.iSup_filtration
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
f :
  ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i : IntermediateField F E) →ₐ[F] Ē
h : Nonempty.{v + 1} (↑(Iio i) : Type v)
x : E
hx :
  Membership.mem (γ := Subalgebra F E)
    (toSubalgebra ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i)) x
⊢ ∃ (i_1 : (↑(Iio i) : Type v)),
    x ∈
      (↑((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
              (↑i_1 : WithTop (Module.rank F E).ord.ToType) :
            IntermediateField F E) :
        Set E)

Tactic:
rw [← iSup_filtration hi, mem_toSubalgebra, ← SetLike.mem_coe,
          coe_iSup_of_directed directed_filtration, mem_iUnion] at hx

Premises used: Field.Emb.Cardinal.directed_filtration, IntermediateField.coe_iSup_of_directed, Set.mem_iUnion, SetLike.mem_coe, IntermediateField.mem_toSubalgebra, Field.Emb.Cardinal.iSup_filtration
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
f :
  ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i : IntermediateField F E) →ₐ[F] Ē
h : Nonempty.{v + 1} (↑(Iio i) : Type v)
x : E
hx_1 :
  Membership.mem (γ := Subalgebra F E)
    (toSubalgebra ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i)) x
hx :
  ∃ (i_1 : (↑(Iio i) : Type v)),
    x ∈
      (↑((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
              (↑i_1 : WithTop (Module.rank F E).ord.ToType) :
            IntermediateField F E) :
        Set E)
⊢ Membership.mem (γ := Subalgebra F E)
    (toSubalgebra
      ((fun (j : (↑(Iio i) : Type v)) ↦
          ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
              (↑j : WithTop (Module.rank F E).ord.ToType) :
            IntermediateField F E))
        (hx.choose (p := fun (i_1 : (↑(Iio i) : Type v)) ↦
          x ∈
            (↑((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                    (↑i_1 : WithTop (Module.rank F E).ord.ToType) :
                  IntermediateField F E) :
              Set E)))))
    (↑(Subtype.mk (p := fun (x : E) ↦
          Membership.mem (γ := Subalgebra F E)
            (toSubalgebra ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i)) x)
          x hx_1) :
      E)

Tactic:
hx.choose_spec

Premises used: Exists.choose_spec, Set.Mem
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
f :
  ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i : IntermediateField F E) →ₐ[F] Ē
h : Nonempty.{v + 1} (↑(Iio i) : Type v)
x : E
hx_1 :
  Membership.mem (γ := Subalgebra F E)
    (toSubalgebra ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i)) x
hx :
  ∃ (i_1 : (↑(Iio i) : Type v)),
    x ∈
      (↑((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
              (↑i_1 : WithTop (Module.rank F E).ord.ToType) :
            IntermediateField F E) :
        Set E)
⊢ Membership.mem (γ := Subalgebra F E)
    (toSubalgebra
      ((fun (j : (↑(Iio i) : Type v)) ↦
          ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
              (↑j : WithTop (Module.rank F E).ord.ToType) :
            IntermediateField F E))
        (hx.choose (p := fun (i_1 : (↑(Iio i) : Type v)) ↦
          x ∈
            (↑((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                    (↑i_1 : WithTop (Module.rank F E).ord.ToType) :
                  IntermediateField F E) :
              Set E)))))
    (↑(Subtype.mk (p := fun (x : E) ↦
          Membership.mem (γ := Subalgebra F E)
            (toSubalgebra ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i)) x)
          x hx_1) :
      E)

Tactic:
exact hx.choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
f :
  (↑(limit (F := fun (j : WithTop (Module.rank F E).ord.ToType) ↦
        ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) j :
              IntermediateField F E) →ₐ[F]
          Ē)
        (embFunctor F E) i) :
    Type v)
j : (↑(Iio i) : Type v)
⊢ Nonempty.{v + 1} (↑(Iio i) : Type v)

Tactic:
have := Nonempty.intro j
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
f :
  (↑(limit (F := fun (j : WithTop (Module.rank F E).ord.ToType) ↦
        ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) j :
              IntermediateField F E) →ₐ[F]
          Ē)
        (embFunctor F E) i) :
    Type v)
j : (↑(Iio i) : Type v)
this : Nonempty.{v + 1} (↑(Iio i) : Type v)
⊢ embFunctor F E ⋯
      (Subalgebra.iSupLift
        (fun (x : (↑(Iio i) : Type v)) ↦
          toSubalgebra
            ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
              (↑x : WithTop (Module.rank F E).ord.ToType)))
        ⋯
        (↑f :
          (l : (↑(Iio i) : Type v)) →
            ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                  (↑l : WithTop (Module.rank F E).ord.ToType)) →ₐ[F]
              Ē)
        ⋯ (toSubalgebra ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i)) ⋯) =
    (↑f :
        (l : (↑(Iio i) : Type v)) →
          ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                (↑l : WithTop (Module.rank F E).ord.ToType)) →ₐ[F]
            Ē)
      j

Tactic:
apply Subalgebra.iSupLift_comp_inclusion

Premises used: Subalgebra.iSupLift_comp_inclusion
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
x :
  ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i : IntermediateField F E) →ₐ[F] Ē
l : (↑(Iio i) : Type v)
⊢ (↑((equivLim hi :
              (a : ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i) →ₐ[F] Ē) →
                (↑(limit (embFunctor F E) i) : Type v))
            x) :
        (l : (↑(Iio i) : Type v)) →
          ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                (↑l : WithTop (Module.rank F E).ord.ToType)) →ₐ[F]
            Ē)
      l =
    embFunctor F E ⋯ x

Tactic:
rfl

Premises used: Field.Emb.Cardinal.embFunctor, AlgHom.comp, rfl
-- Module: Mathlib.FieldTheory.CardinalEmb
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
rank_inf : ℵ₀ ≤ Module.rank F E
⊢ Fact (ℵ₀ ≤ Module.rank F E)

Tactic:
haveI := Fact.mk rank_inf
-- Module: Mathlib.FieldTheory.CardinalEmb
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
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
rw :
  (Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
      #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))) =
    HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E)
⊢ #(Emb F E) = HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E)

Tactic:
rw [Emb.Cardinal.embEquivPi.cardinal_eq, mk_pi]

Premises used: Cardinal.mk_pi, Field.Emb.Cardinal.embEquivPi, Equiv.cardinal_eq
-- Module: Mathlib.FieldTheory.CardinalEmb
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
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
a :
  (Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
      #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))) ≤
    HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E)
a₁ :
  HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E) ≤
    Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
      #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))
⊢ (Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
      #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))) =
    HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.FieldTheory.CardinalEmb
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
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
a :
  (Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
      #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))) ≤
    ℵ₀ ^ Module.rank F E
⊢ (Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
      #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))) ≤
    HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E)

Tactic:
rw [← power_eq_two_power rank_inf natCast_le_aleph0 rank_inf]

Premises used: Cardinal.natCast_le_aleph0, Cardinal.power_eq_two_power
-- Module: Mathlib.FieldTheory.CardinalEmb
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
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
rw : Cardinal.prod fun (x : (Module.rank F E).ord.ToType) ↦ ℵ₀
| ℵ₀ ^ Module.rank F E

Tactic:
rw [← mk_ord_toType (Module.rank F E), ← prod_const']

Premises used: Cardinal.prod_const', Cardinal.mk_ord_toType, Module.rank
-- Module: Mathlib.FieldTheory.CardinalEmb
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
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
a :
  (Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
      #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))) ≤
    Cardinal.prod fun (x : (Module.rank F E).ord.ToType) ↦ ℵ₀
⊢ (Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
      #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))) ≤
    ℵ₀ ^ Module.rank F E

Tactic:
conv_rhs => rw [← mk_ord_toType (Module.rank F E), ← prod_const']

Premises used: Cardinal.prod_const', Cardinal.mk_ord_toType, Module.rank
-- Module: Mathlib.FieldTheory.CardinalEmb
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
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ (Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
      #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))) ≤
    Cardinal.prod fun (x : (Module.rank F E).ord.ToType) ↦ ℵ₀

Tactic:
prod_le_prod _ _ fun i ↦ (Emb.Cardinal.deg_lt_aleph0 _).le

Premises used: LT.lt.le, Field.Emb.Cardinal.deg_lt_aleph0, Cardinal.prod_le_prod
-- Module: Mathlib.FieldTheory.CardinalEmb
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
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ (Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
      #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))) ≤
    Cardinal.prod fun (x : (Module.rank F E).ord.ToType) ↦ ℵ₀

Tactic:
exact prod_le_prod _ _ fun i ↦ (Emb.Cardinal.deg_lt_aleph0 _).le

Premises used: LT.lt.le, Field.Emb.Cardinal.deg_lt_aleph0, Cardinal.prod_le_prod
-- Module: Mathlib.FieldTheory.CardinalEmb
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
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
rw : Cardinal.prod fun (x : (Module.rank F E).ord.ToType) ↦ 2
| HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E)

Tactic:
rw [← mk_ord_toType (Module.rank F E), ← prod_const']

Premises used: Cardinal.prod_const', Cardinal.mk_ord_toType, Module.rank