-- Mathlib/FieldTheory/CardinalEmb.lean
theorem adjoin_image_leastExt (i : ι) : E⟮<i⟯ = adjoin F (b '' Iio (φ i))

Proof state:
case refine_1.h.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
i j : (Module.rank F E).ord.toType
hj : j ∈ Iio i
⊢ φ j ∈ Iio (φ i)

Tactic:
exact strictMono_leastExt hj

Result:
no goals

Proof state:
case refine_2.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
i j : (Module.rank F E).ord.toType
hj : b j ∉ ↑(adjoin F (⇑b ∘ φ '' Iio i))
⊢ j ∉ Iio (φ i)

Tactic:
exact ((isLeast_leastExt i).2 hj).not_lt

Result:
no goals

Proof state:
case refine_2.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
i j : (Module.rank F E).ord.toType
hj : j ∈ Iio (φ i)
⊢ b j ∈ ↑(adjoin F (⇑b ∘ φ '' Iio i))

Tactic:
contrapose! hj

Result:
case refine_2.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
i j : (Module.rank F E).ord.toType
hj : b j ∉ ↑(adjoin F (⇑b ∘ φ '' Iio i))
⊢ j ∉ Iio (φ i)

Proof state:
case refine_1.h
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 : (Module.rank F E).ord.toType
⊢ φ '' Iio i ⊆ Iio (φ i)

Tactic:
rintro _ ⟨j, hj, rfl⟩

Result:
case refine_1.h.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
i j : (Module.rank F E).ord.toType
hj : j ∈ Iio i
⊢ φ j ∈ Iio (φ i)

Proof state:
case 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
i : (Module.rank F E).ord.toType
⊢ ⇑b ∘ φ '' Iio i ⊆ ⇑b '' Iio (φ i)

Tactic:
rw [image_comp]

Result:
case 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
i : (Module.rank F E).ord.toType
⊢ ⇑b '' (φ '' Iio i) ⊆ ⇑b '' Iio (φ 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
i : (Module.rank F E).ord.toType
⊢ adjoin F (⇑b ∘ φ '' Iio i) = adjoin F (⇑b '' Iio (φ i))

Tactic:
refine le_antisymm (adjoin.mono _ _ _ ?_) (adjoin_le_iff.mpr ?_)

Result:
case 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
i : (Module.rank F E).ord.toType
⊢ ⇑b ∘ φ '' Iio i ⊆ ⇑b '' Iio (φ i)

case 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
i : (Module.rank F E).ord.toType
⊢ ⇑b '' Iio (φ i) ⊆ ↑(adjoin F (⇑b ∘ φ '' Iio i))

Proof state:
case 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
i : (Module.rank F E).ord.toType
⊢ ⇑b '' Iio (φ i) ⊆ ↑(adjoin F (⇑b ∘ φ '' Iio i))

Tactic:
rintro _ ⟨j, hj, rfl⟩

Result:
case refine_2.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
i j : (Module.rank F E).ord.toType
hj : j ∈ Iio (φ i)
⊢ b j ∈ ↑(adjoin F (⇑b ∘ φ '' Iio i))

Proof state:
case 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
i : (Module.rank F E).ord.toType
⊢ ⇑b '' (φ '' Iio i) ⊆ ⇑b '' Iio (φ i)

Tactic:
apply image_mono

Result:
case refine_1.h
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 : (Module.rank F E).ord.toType
⊢ φ '' Iio i ⊆ Iio (φ i)