α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
⊢ ∀ (a : α), a ∈ upperBounds (Set.range ↑(partialSups f)) ↔ a ∈ upperBounds (Set.range f)
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
⊢ BddAbove (Set.range ↑(partialSups f)) ↔ BddAbove (Set.range f)
apply exists_congr fun a => _
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
a : α
⊢ a ∈ upperBounds (Set.range ↑(partialSups f)) ↔ a ∈ upperBounds (Set.range f)
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
⊢ ∀ (a : α), a ∈ upperBounds (Set.range ↑(partialSups f)) ↔ a ∈ upperBounds (Set.range f)
intro a
case mp
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
a : α
⊢ a ∈ upperBounds (Set.range ↑(partialSups f)) → a ∈ upperBounds (Set.range f)

case mpr
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
a : α
⊢ a ∈ upperBounds (Set.range f) → a ∈ upperBounds (Set.range ↑(partialSups f))
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
a : α
⊢ a ∈ upperBounds (Set.range ↑(partialSups f)) ↔ a ∈ upperBounds (Set.range f)
constructor
case mp.intro
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
a : α
h : a ∈ upperBounds (Set.range ↑(partialSups f))
i : ℕ
⊢ f i ≤ a
case mp
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
a : α
⊢ a ∈ upperBounds (Set.range ↑(partialSups f)) → a ∈ upperBounds (Set.range f)
rintro h b ⟨i, rfl⟩
no goals
case mp.intro
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
a : α
h : a ∈ upperBounds (Set.range ↑(partialSups f))
i : ℕ
⊢ f i ≤ a
exact (le_partialSups _ _).trans (h (Set.mem_range_self i))
case mpr.intro
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
a : α
h : a ∈ upperBounds (Set.range f)
i : ℕ
⊢ ↑(partialSups f) i ≤ a
case mpr
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
a : α
⊢ a ∈ upperBounds (Set.range f) → a ∈ upperBounds (Set.range ↑(partialSups f))
rintro h b ⟨i, rfl⟩
no goals
case mpr.intro
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
a : α
h : a ∈ upperBounds (Set.range f)
i : ℕ
⊢ ↑(partialSups f) i ≤ a
exact partialSups_le _ _ _ fun _ _ => h (Set.mem_range_self _)