case refine'_1
R : Type ?u.778047
R' : Type ?u.778050
𝕜 : Type u_2
𝕜₂ : Type ?u.778056
𝕜₃ : Type ?u.778059
𝕝 : Type ?u.778062
E : Type u_1
E₂ : Type ?u.778068
E₃ : Type ?u.778071
F : Type ?u.778074
G : Type ?u.778077
ι : Type ?u.778080
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : Set.Nonempty s
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
this : Nonempty ↑s
⊢ ↑p x ≤ ⨆ (i : ↑s), ↑↑i x

case refine'_2
R : Type ?u.778047
R' : Type ?u.778050
𝕜 : Type u_2
𝕜₂ : Type ?u.778056
𝕜₃ : Type ?u.778059
𝕝 : Type ?u.778062
E : Type u_1
E₂ : Type ?u.778068
E₃ : Type ?u.778071
F : Type ?u.778074
G : Type ?u.778077
ι : Type ?u.778080
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : Set.Nonempty s
p : Seminorm 𝕜 E
hp : p ∈ upperBounds s
x : E
this : Nonempty ↑s
⊢ (⨆ (i : ↑s), ↑↑i x) ≤ ↑p x
R : Type ?u.778047
R' : Type ?u.778050
𝕜 : Type u_2
𝕜₂ : Type ?u.778056
𝕜₃ : Type ?u.778059
𝕝 : Type ?u.778062
E : Type u_1
E₂ : Type ?u.778068
E₃ : Type ?u.778071
F : Type ?u.778074
G : Type ?u.778077
ι : Type ?u.778080
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x : E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : Set.Nonempty s
⊢ IsLUB s (sSup s)
refine' ⟨fun p hp x => _, fun p hp x => _⟩ <;> haveI : Nonempty ↑s := hs₂.coe_sort <;>
  dsimp <;> rw [Seminorm.coe_sSup_eq hs₁, iSup_apply]
case refine'_1.intro
R : Type ?u.778047
R' : Type ?u.778050
𝕜 : Type u_2
𝕜₂ : Type ?u.778056
𝕜₃ : Type ?u.778059
𝕝 : Type ?u.778062
E : Type u_1
E₂ : Type ?u.778068
E₃ : Type ?u.778071
F : Type ?u.778074
G : Type ?u.778077
ι : Type ?u.778080
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q✝ : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
hs₂ : Set.Nonempty s
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
this : Nonempty ↑s
q : Seminorm 𝕜 E
hq : q ∈ upperBounds s
⊢ ↑p x ≤ ⨆ (i : ↑s), ↑↑i x
case refine'_1
R : Type ?u.778047
R' : Type ?u.778050
𝕜 : Type u_2
𝕜₂ : Type ?u.778056
𝕜₃ : Type ?u.778059
𝕝 : Type ?u.778062
E : Type u_1
E₂ : Type ?u.778068
E₃ : Type ?u.778071
F : Type ?u.778074
G : Type ?u.778077
ι : Type ?u.778080
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : Set.Nonempty s
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
this : Nonempty ↑s
⊢ ↑p x ≤ ⨆ (i : ↑s), ↑↑i x
rcases hs₁ with ⟨q, hq⟩
no goals
case refine'_1.intro
R : Type ?u.778047
R' : Type ?u.778050
𝕜 : Type u_2
𝕜₂ : Type ?u.778056
𝕜₃ : Type ?u.778059
𝕝 : Type ?u.778062
E : Type u_1
E₂ : Type ?u.778068
E₃ : Type ?u.778071
F : Type ?u.778074
G : Type ?u.778077
ι : Type ?u.778080
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q✝ : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
hs₂ : Set.Nonempty s
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
this : Nonempty ↑s
q : Seminorm 𝕜 E
hq : q ∈ upperBounds s
⊢ ↑p x ≤ ⨆ (i : ↑s), ↑↑i x
exact le_ciSup ⟨q x, forall_range_iff.mpr fun i : s => hq i.2 x⟩ ⟨p, hp⟩
no goals
case refine'_2
R : Type ?u.778047
R' : Type ?u.778050
𝕜 : Type u_2
𝕜₂ : Type ?u.778056
𝕜₃ : Type ?u.778059
𝕝 : Type ?u.778062
E : Type u_1
E₂ : Type ?u.778068
E₃ : Type ?u.778071
F : Type ?u.778074
G : Type ?u.778077
ι : Type ?u.778080
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : Set.Nonempty s
p : Seminorm 𝕜 E
hp : p ∈ upperBounds s
x : E
this : Nonempty ↑s
⊢ (⨆ (i : ↑s), ↑↑i x) ≤ ↑p x
exact ciSup_le fun q => hp q.2 x