Theorem: lowerBounds_range (GlimpseOfLean/Library/Basic.lean)

State before:
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
⊢ x ∈ lowerBounds (Set.range s) ↔ ∀ (i : ι), x ≤ s i
Tactic:
constructor
State after:
case mp
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
⊢ x ∈ lowerBounds (Set.range s) → ∀ (i : ι), x ≤ s i

case mpr
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
⊢ (∀ (i : ι), x ≤ s i) → x ∈ lowerBounds (Set.range s)

State before:
case mp
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
⊢ x ∈ lowerBounds (Set.range s) → ∀ (i : ι), x ≤ s i
Tactic:
intros hx i
State after:
case mp
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
hx : x ∈ lowerBounds (Set.range s)
i : ι
⊢ x ≤ s i

State before:
case mp
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
hx : x ∈ lowerBounds (Set.range s)
i : ι
⊢ x ≤ s i
Tactic:
apply hx
State after:
case mp.a
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
hx : x ∈ lowerBounds (Set.range s)
i : ι
⊢ s i ∈ Set.range s

State before:
case mp.a
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
hx : x ∈ lowerBounds (Set.range s)
i : ι
⊢ s i ∈ Set.range s
Tactic:
exact Set.mem_range_self i
State after:
no goals

State before:
case mpr
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
⊢ (∀ (i : ι), x ≤ s i) → x ∈ lowerBounds (Set.range s)
Tactic:
rintro hx y ⟨i, rfl⟩
State after:
case mpr.intro
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
hx : ∀ (i : ι), x ≤ s i
i : ι
⊢ x ≤ s i

State before:
case mpr.intro
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
hx : ∀ (i : ι), x ≤ s i
i : ι
⊢ x ≤ s i
Tactic:
exact hx i
State after:
no goals