-- Mathlib/Order/Filter/AtTopBot/Defs.lean
lemma atTop_eq_generate_of_forall_exists_le [LinearOrder α] {s : Set α} (hs : ∀ x, ∃ y ∈ s, x ≤ y) :
    (atTop : Filter α) = generate (Ici '' s)

Proof state:
case a
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ range Ici ⊆ (generate (Ici '' s)).sets

Tactic:
rintro - ⟨x, -, -, rfl⟩

Result:
case a.intro.refl
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
x : α
⊢ Ici x ∈ (generate (Ici '' s)).sets

Proof state:
case a.intro.refl.intro.intro
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
x y : α
ys : y ∈ s
hy : x ≤ y
A : Ici y ∈ generate (Ici '' s)
B : Ici y ⊆ Ici x
⊢ Ici x ∈ (generate (Ici '' s)).sets

Tactic:
exact sets_of_superset (generate (Ici '' s)) A B

Result:
no goals

Proof state:
case a.intro.refl.intro.intro
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
x y : α
ys : y ∈ s
hy : x ≤ y
A : Ici y ∈ generate (Ici '' s)
⊢ Ici x ∈ (generate (Ici '' s)).sets

Tactic:
have B : Ici y ⊆ Ici x := Ici_subset_Ici.2 hy

Result:
case a.intro.refl.intro.intro
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
x y : α
ys : y ∈ s
hy : x ≤ y
A : Ici y ∈ generate (Ici '' s)
B : Ici y ⊆ Ici x
⊢ Ici x ∈ (generate (Ici '' s)).sets

Proof state:
case a.intro.refl
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
x : α
⊢ Ici x ∈ (generate (Ici '' s)).sets

Tactic:
rcases hs x with ⟨y, ys, hy⟩

Result:
case a.intro.refl.intro.intro
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
x y : α
ys : y ∈ s
hy : x ≤ y
⊢ Ici x ∈ (generate (Ici '' s)).sets

Proof state:
case a.intro.refl.intro.intro
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
x y : α
ys : y ∈ s
hy : x ≤ y
⊢ Ici x ∈ (generate (Ici '' s)).sets

Tactic:
have A : Ici y ∈ generate (Ici '' s) := mem_generate_of_mem (mem_image_of_mem _ ys)

Result:
case a.intro.refl.intro.intro
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
x y : α
ys : y ∈ s
hy : x ≤ y
A : Ici y ∈ generate (Ici '' s)
⊢ Ici x ∈ (generate (Ici '' s)).sets

Proof state:
case a
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ Ici '' s ⊆ (generate (range Ici)).sets

Tactic:
rintro - ⟨y, -, rfl⟩

Result:
case a.intro.intro
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
y : α
⊢ Ici y ∈ (generate (range Ici)).sets

Proof state:
case a
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ generate (range Ici) ≤ generate (Ici '' s)

Tactic:
rw [le_generate_iff]

Result:
case a
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ Ici '' s ⊆ (generate (range Ici)).sets

Proof state:
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ generate (range Ici) = generate (Ici '' s)

Tactic:
apply le_antisymm

Result:
case a
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ generate (range Ici) ≤ generate (Ici '' s)

case a
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ generate (Ici '' s) ≤ generate (range Ici)

Proof state:
case a.intro.intro
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
y : α
⊢ Ici y ∈ (generate (range Ici)).sets

Tactic:
exact mem_generate_of_mem ⟨y, rfl⟩

Result:
no goals

Proof state:
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ atTop = generate (Ici '' s)

Tactic:
rw [atTop_eq_generate_Ici]

Result:
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ generate (range Ici) = generate (Ici '' s)

Proof state:
case a
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ generate (Ici '' s) ≤ generate (range Ici)

Tactic:
rw [le_generate_iff]

Result:
case a
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ range Ici ⊆ (generate (Ici '' s)).sets