-- Mathlib/Analysis/Seminorm.lean
theorem closedBall_iSup {ι : Sort*} {p : ι → Seminorm 𝕜 E} (hp : BddAbove (range p)) (e : E)
    {r : ℝ} (hr : 0 < r) : closedBall (⨆ i, p i) e r = ⋂ i, closedBall (p i) e r

Proof state:
case inr.h
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
e : E
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
x : E
⊢ x ∈ (⨆ i, p i).closedBall e r ↔ x ∈ ⋂ i, (p i).closedBall e r

Tactic:
have := Seminorm.bddAbove_range_iff.mp hp (x - e)

Result:
case inr.h
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
e : E
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
x : E
this : BddAbove (range fun i => (p i) (x - e))
⊢ x ∈ (⨆ i, p i).closedBall e r ↔ x ∈ ⋂ i, (p i).closedBall e r

Proof state:
case inr.h
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
e : E
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
x : E
this : BddAbove (range fun i => (p i) (x - e))
⊢ x ∈ (⨆ i, p i).closedBall e r ↔ x ∈ ⋂ i, (p i).closedBall e r

Tactic:
simp only [mem_closedBall, mem_iInter, Seminorm.iSup_apply hp, ciSup_le_iff this]

Result:
no goals

Proof state:
case inl
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
e : E
r : ℝ
hr : 0 < r
h✝ : IsEmpty ι
⊢ ⊥.closedBall e r = univ

Tactic:
exact closedBall_bot _ hr

Result:
no goals

Proof state:
case inl
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
e : E
r : ℝ
hr : 0 < r
h✝ : IsEmpty ι
⊢ (⨆ i, p i).closedBall e r = ⋂ i, (p i).closedBall e r

Tactic:
rw [iSup_of_empty', iInter_of_empty, Seminorm.sSup_empty]

Result:
case inl
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
e : E
r : ℝ
hr : 0 < r
h✝ : IsEmpty ι
⊢ ⊥.closedBall e r = univ

Proof state:
case inr
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
e : E
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
⊢ (⨆ i, p i).closedBall e r = ⋂ i, (p i).closedBall e r

Tactic:
ext x

Result:
case inr.h
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
e : E
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
x : E
⊢ x ∈ (⨆ i, p i).closedBall e r ↔ x ∈ ⋂ i, (p i).closedBall e r

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
e : E
r : ℝ
hr : 0 < r
⊢ (⨆ i, p i).closedBall e r = ⋂ i, (p i).closedBall e r

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
e : E
r : ℝ
hr : 0 < r
h✝ : IsEmpty ι
⊢ (⨆ i, p i).closedBall e r = ⋂ i, (p i).closedBall e r

case inr
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
e : E
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
⊢ (⨆ i, p i).closedBall e r = ⋂ i, (p i).closedBall e r