-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem bsupr_limsup_dimH (s : Set X) : ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets = dimH s

Proof state:
case refine_2
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
⊢ r ≤ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets

Tactic:
rcases exists_mem_nhdsWithin_lt_dimH_of_lt_dimH hr with ⟨x, hxs, hxr⟩

Result:
case refine_2.intro.intro
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ t ∈ 𝓝[s] x, r < dimH t
⊢ r ≤ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets

Proof state:
case refine_1
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
x : X
x✝ : x ∈ s
⊢ ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ dimH s

Tactic:
exact eventually_smallSets.2 ⟨s, self_mem_nhdsWithin, fun t => dimH_mono⟩

Result:
no goals

Proof state:
case refine_2.intro.intro
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ t ∈ 𝓝[s] x, r < dimH t
b : ℝ≥0∞
hb : b ∈ {a | ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ a}
⊢ r ≤ b

Tactic:
rcases eventually_smallSets.1 hb with ⟨t, htx, ht⟩

Result:
case refine_2.intro.intro.intro.intro
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ t ∈ 𝓝[s] x, r < dimH t
b : ℝ≥0∞
hb : b ∈ {a | ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ a}
t : Set X
htx : t ∈ 𝓝[s] x
ht : ∀ t_1 ⊆ t, dimH t_1 ≤ b
⊢ r ≤ b

Proof state:
case refine_2.intro.intro
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ t ∈ 𝓝[s] x, r < dimH t
⊢ r ≤ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets

Tactic:
refine le_iSup₂_of_le x hxs ?_

Result:
case refine_2.intro.intro
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ t ∈ 𝓝[s] x, r < dimH t
⊢ r ≤ limsup dimH (𝓝[s] x).smallSets

Proof state:
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
⊢ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets = dimH s

Tactic:
refine le_antisymm (iSup₂_le fun x _ => ?_) ?_

Result:
case refine_1
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
x : X
x✝ : x ∈ s
⊢ limsup dimH (𝓝[s] x).smallSets ≤ dimH s

case refine_2
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
⊢ dimH s ≤ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets

Proof state:
case refine_2.intro.intro.intro.intro
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ t ∈ 𝓝[s] x, r < dimH t
b : ℝ≥0∞
hb : b ∈ {a | ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ a}
t : Set X
htx : t ∈ 𝓝[s] x
ht : ∀ t_1 ⊆ t, dimH t_1 ≤ b
⊢ r ≤ b

Tactic:
exact (hxr t htx).le.trans (ht t Subset.rfl)

Result:
no goals

Proof state:
case refine_2.intro.intro
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ t ∈ 𝓝[s] x, r < dimH t
⊢ r ≤ sInf {a | ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ a}

Tactic:
refine le_sInf fun b hb => ?_

Result:
case refine_2.intro.intro
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ t ∈ 𝓝[s] x, r < dimH t
b : ℝ≥0∞
hb : b ∈ {a | ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ a}
⊢ r ≤ b

Proof state:
case refine_1
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
x : X
x✝ : x ∈ s
⊢ limsup dimH (𝓝[s] x).smallSets ≤ dimH s

Tactic:
refine limsup_le_of_le isCobounded_le_of_bot ?_

Result:
case refine_1
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
x : X
x✝ : x ∈ s
⊢ ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ dimH s

Proof state:
case refine_2
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
⊢ dimH s ≤ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun r hr => ?_

Result:
case refine_2
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
⊢ r ≤ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets

Proof state:
case refine_2.intro.intro
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ t ∈ 𝓝[s] x, r < dimH t
⊢ r ≤ limsup dimH (𝓝[s] x).smallSets

Tactic:
rw [limsup_eq]

Result:
case refine_2.intro.intro
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ t ∈ 𝓝[s] x, r < dimH t
⊢ r ≤ sInf {a | ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ a}