-- Mathlib/FieldTheory/CardinalEmb.lean
theorem two_le_deg (i : ι) : 2 ≤ #(X i)

Proof state:
case intro
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : Algebra.IsSeparable F E
i : (Module.rank F E).ord.toType
this : Module.finrank ↥(adjoin F (⇑b ∘ φ '' Iio i)) ↥(↥(adjoin F (⇑b ∘ φ '' Iio i)))⟮b (φ i)⟯ ≤ 1
x : ↥(adjoin F (⇑b ∘ φ '' Iio i))
hx : (Algebra.ofId (↥(adjoin F (⇑b ∘ φ '' Iio i))) E).toRingHom x = b (φ i)
⊢ False

Tactic:
refine (isLeast_leastExt i).1 (hx ▸ ?_)

Result:
case intro
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : Algebra.IsSeparable F E
i : (Module.rank F E).ord.toType
this : Module.finrank ↥(adjoin F (⇑b ∘ φ '' Iio i)) ↥(↥(adjoin F (⇑b ∘ φ '' Iio i)))⟮b (φ i)⟯ ≤ 1
x : ↥(adjoin F (⇑b ∘ φ '' Iio i))
hx : (Algebra.ofId (↥(adjoin F (⇑b ∘ φ '' Iio i))) E).toRingHom x = b (φ i)
⊢ (Algebra.ofId (↥(adjoin F (⇑b ∘ φ '' Iio i))) E).toRingHom x ∈ adjoin F (⇑b ∘ φ '' Iio i)

Proof state:
case intro
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : Algebra.IsSeparable F E
i : (Module.rank F E).ord.toType
this : Module.finrank ↥(adjoin F (⇑b ∘ φ '' Iio i)) ↥(↥(adjoin F (⇑b ∘ φ '' Iio i)))⟮b (φ i)⟯ ≤ 1
x : ↥(adjoin F (⇑b ∘ φ '' Iio i))
hx : (Algebra.ofId (↥(adjoin F (⇑b ∘ φ '' Iio i))) E).toRingHom x = b (φ i)
⊢ (Algebra.ofId (↥(adjoin F (⇑b ∘ φ '' Iio i))) E).toRingHom x ∈ adjoin F (⇑b ∘ φ '' Iio i)

Tactic:
exact x.2

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : Algebra.IsSeparable F E
i : (Module.rank F E).ord.toType
⊢ 2 ≤ #(Emb ↥(adjoin F (⇑b ∘ φ '' Iio i)) ↥(↥(adjoin F (⇑b ∘ φ '' Iio i)))⟮b (φ i)⟯)

Tactic:
rw [← Nat.cast_ofNat, ← toNat_le_iff_le_of_lt_aleph0 (nat_lt_aleph0 _) (deg_lt_aleph0 i),
  toNat_natCast, ← Nat.card, ← finSepDegree, finSepDegree_eq_finrank_of_isSeparable, Nat.succ_le]

Result:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : Algebra.IsSeparable F E
i : (Module.rank F E).ord.toType
⊢ 1 < Module.finrank ↥(adjoin F (⇑b ∘ φ '' Iio i)) ↥(↥(adjoin F (⇑b ∘ φ '' Iio i)))⟮b (φ i)⟯

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : Algebra.IsSeparable F E
i : (Module.rank F E).ord.toType
this : Module.finrank ↥(adjoin F (⇑b ∘ φ '' Iio i)) ↥(↥(adjoin F (⇑b ∘ φ '' Iio i)))⟮b (φ i)⟯ ≤ 1
⊢ False

Tactic:
obtain ⟨x, hx⟩ := finrank_adjoin_simple_eq_one_iff.mp (this.antisymm Module.finrank_pos)

Result:
case intro
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : Algebra.IsSeparable F E
i : (Module.rank F E).ord.toType
this : Module.finrank ↥(adjoin F (⇑b ∘ φ '' Iio i)) ↥(↥(adjoin F (⇑b ∘ φ '' Iio i)))⟮b (φ i)⟯ ≤ 1
x : ↥(adjoin F (⇑b ∘ φ '' Iio i))
hx : (Algebra.ofId (↥(adjoin F (⇑b ∘ φ '' Iio i))) E).toRingHom x = b (φ i)
⊢ False

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : Algebra.IsSeparable F E
i : (Module.rank F E).ord.toType
⊢ 1 < Module.finrank ↥(adjoin F (⇑b ∘ φ '' Iio i)) ↥(↥(adjoin F (⇑b ∘ φ '' Iio i)))⟮b (φ i)⟯

Tactic:
by_contra!

Result:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : Algebra.IsSeparable F E
i : (Module.rank F E).ord.toType
this : Module.finrank ↥(adjoin F (⇑b ∘ φ '' Iio i)) ↥(↥(adjoin F (⇑b ∘ φ '' Iio i)))⟮b (φ i)⟯ ≤ 1
⊢ False