-- Mathlib/FieldTheory/CardinalEmb.lean
theorem strictMono_leastExt : StrictMono φ := fun i j h ↦ by
  have least := isLeast_leastExt (F := F) (E := E)
  by_contra!
  obtain eq | lt := this.eq_or_lt
  · exact (least j).1 (subset_adjoin _ _ ⟨i, h, congr_arg b eq.symm⟩)
  · refine ((least i).2 <| mt (adjoin.mono _ _ _ (image_mono ?_) ·) (least j).1).not_lt lt
    exact fun k (hk : k < i) ↦ hk.trans h

Proof state:
case inl
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
i j : (Module.rank F E).ord.toType
h : i < j
least : ∀ (i : (Module.rank F E).ord.toType), IsLeast {k | b k ∉ adjoin F (⇑b ∘ φ '' Iio i)} (φ i)
this : φ j ≤ φ i
eq : φ j = φ i
⊢ False

Tactic:
exact (least j).1 (subset_adjoin _ _ ⟨i, h, congr_arg b eq.symm⟩)

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
i j : (Module.rank F E).ord.toType
h : i < j
least : ∀ (i : (Module.rank F E).ord.toType), IsLeast {k | b k ∉ adjoin F (⇑b ∘ φ '' Iio i)} (φ i)
⊢ φ i < φ j

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
i j : (Module.rank F E).ord.toType
h : i < j
least : ∀ (i : (Module.rank F E).ord.toType), IsLeast {k | b k ∉ adjoin F (⇑b ∘ φ '' Iio i)} (φ i)
this : φ j ≤ φ 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
i j : (Module.rank F E).ord.toType
h : i < j
⊢ φ i < φ j

Tactic:
have least := isLeast_leastExt (F := F) (E := E)

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
i j : (Module.rank F E).ord.toType
h : i < j
least : ∀ (i : (Module.rank F E).ord.toType), IsLeast {k | b k ∉ adjoin F (⇑b ∘ φ '' Iio i)} (φ i)
⊢ φ i < φ j

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
i j : (Module.rank F E).ord.toType
h : i < j
least : ∀ (i : (Module.rank F E).ord.toType), IsLeast {k | b k ∉ adjoin F (⇑b ∘ φ '' Iio i)} (φ i)
this : φ j ≤ φ i
⊢ False

Tactic:
obtain eq | lt := this.eq_or_lt

Result:
case inl
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
i j : (Module.rank F E).ord.toType
h : i < j
least : ∀ (i : (Module.rank F E).ord.toType), IsLeast {k | b k ∉ adjoin F (⇑b ∘ φ '' Iio i)} (φ i)
this : φ j ≤ φ i
eq : φ j = φ i
⊢ False

case inr
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
i j : (Module.rank F E).ord.toType
h : i < j
least : ∀ (i : (Module.rank F E).ord.toType), IsLeast {k | b k ∉ adjoin F (⇑b ∘ φ '' Iio i)} (φ i)
this : φ j ≤ φ i
lt : φ j < φ i
⊢ False

Proof state:
case inr
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
i j : (Module.rank F E).ord.toType
h : i < j
least : ∀ (i : (Module.rank F E).ord.toType), IsLeast {k | b k ∉ adjoin F (⇑b ∘ φ '' Iio i)} (φ i)
this : φ j ≤ φ i
lt : φ j < φ i
x✝ : b (φ j) ∈ adjoin F (⇑b ∘ φ '' Iio i)
⊢ Iio i ⊆ Iio j

Tactic:
exact fun k (hk : k < i) ↦ hk.trans h

Result:
no goals