-- Mathlib/FieldTheory/CardinalEmb.lean
theorem iSup_filtration : ⨆ j : Iio i, filtration j = filtration i

Proof state:
case coe.intro.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
a✝ : (Module.rank F E).ord.toType
hi : IsSuccPrelimit ↑a✝
j : (Module.rank F E).ord.toType
hj : j ∈ Iio a✝
⊢ (⇑b ∘ φ) j ∈ ↑(⨆ j, filtration ↑j)

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

Result:
case coe.intro.intro.refine_1
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
a✝ : (Module.rank F E).ord.toType
hi : IsSuccPrelimit ↑a✝
j : (Module.rank F E).ord.toType
hj : j ∈ Iio a✝
⊢ (⇑b ∘ φ) j ∈ ⇑b ∘ φ '' Iio (j⁺)

case coe.intro.intro.refine_2
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
a✝ : (Module.rank F E).ord.toType
hi : IsSuccPrelimit ↑a✝
j : (Module.rank F E).ord.toType
hj : j ∈ Iio a✝
⊢ ↑j⁺ ∈ Iio ↑a✝

Proof state:
case top
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
hi : IsSuccPrelimit ⊤
⊢ ⨆ j, filtration ↑j = filtration ⊤

Tactic:
rw [← range_coe, iSup_range']

Result:
case top
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
hi : IsSuccPrelimit ⊤
⊢ ⨆ i, filtration ↑i = filtration ⊤

Proof state:
case coe
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
a✝ : (Module.rank F E).ord.toType
hi : IsSuccPrelimit ↑a✝
⊢ ⨆ j, filtration ↑j = filtration ↑a✝

Tactic:
refine (iSup_le fun j ↦ filtration.monotone (mem_Iio.1 j.2).le).antisymm (adjoin_le_iff.2 ?_)

Result:
case coe
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
a✝ : (Module.rank F E).ord.toType
hi : IsSuccPrelimit ↑a✝
⊢ ⇑b ∘ φ '' Iio a✝ ⊆ ↑(⨆ j, filtration ↑j)

Proof state:
case coe.intro.intro.refine_1
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
a✝ : (Module.rank F E).ord.toType
hi : IsSuccPrelimit ↑a✝
j : (Module.rank F E).ord.toType
hj : j ∈ Iio a✝
⊢ (⇑b ∘ φ) j ∈ ⇑b ∘ φ '' Iio (j⁺)

case coe.intro.intro.refine_2
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
a✝ : (Module.rank F E).ord.toType
hi : IsSuccPrelimit ↑a✝
j : (Module.rank F E).ord.toType
hj : j ∈ Iio a✝
⊢ ↑j⁺ ∈ Iio ↑a✝

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

Result:
no goals

Proof state:
case top
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
hi : IsSuccPrelimit ⊤
⊢ ⨆ i, filtration ↑i = filtration ⊤

Tactic:
exact iSup_adjoin_eq_top

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 : WithTop (Module.rank F E).ord.toType
hi : IsSuccPrelimit i
⊢ ⨆ j, filtration ↑j = filtration i

Tactic:
cases i

Result:
case top
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
hi : IsSuccPrelimit ⊤
⊢ ⨆ j, filtration ↑j = filtration ⊤

case coe
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
a✝ : (Module.rank F E).ord.toType
hi : IsSuccPrelimit ↑a✝
⊢ ⨆ j, filtration ↑j = filtration ↑a✝

Proof state:
case coe
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
a✝ : (Module.rank F E).ord.toType
hi : IsSuccPrelimit ↑a✝
⊢ ⇑b ∘ φ '' Iio a✝ ⊆ ↑(⨆ j, filtration ↑j)

Tactic:
rintro _ ⟨j, hj, rfl⟩

Result:
case coe.intro.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
a✝ : (Module.rank F E).ord.toType
hi : IsSuccPrelimit ↑a✝
j : (Module.rank F E).ord.toType
hj : j ∈ Iio a✝
⊢ (⇑b ∘ φ) j ∈ ↑(⨆ j, filtration ↑j)