-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem dimH_of_mem_nhds {x : E} {s : Set E} (h : s ∈ 𝓝 x) : dimH s = finrank ℝ E

Proof state:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ ⇑e '' s ∈ Filter.map (⇑e) (𝓝 x)

Tactic:
exact image_mem_map h

Result:
no goals

Proof state:
case refine_2.intro.intro
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
this : ⇑e '' s ∈ 𝓝 (e x)
r : ℝ
hr0 : 0 < r
hr : Metric.ball (e x) r ⊆ ⇑e '' s
⊢ ↑(finrank ℝ E) ≤ dimH (⇑e '' s)

Tactic:
simpa only [dimH_ball_pi_fin (e x) hr0] using dimH_mono hr

Result:
no goals

Proof state:
case refine_2
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
this : ⇑e '' s ∈ 𝓝 (e x)
⊢ ↑(finrank ℝ E) ≤ dimH (⇑e '' s)

Tactic:
rcases Metric.nhds_basis_ball.mem_iff.1 this with ⟨r, hr0, hr⟩

Result:
case refine_2.intro.intro
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
this : ⇑e '' s ∈ 𝓝 (e x)
r : ℝ
hr0 : 0 < r
hr : Metric.ball (e x) r ⊆ ⇑e '' s
⊢ ↑(finrank ℝ E) ≤ dimH (⇑e '' s)

Proof state:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ dimH s = ↑(finrank ℝ E)

Tactic:
rw [← e.dimH_image]

Result:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ dimH (⇑e '' s) = ↑(finrank ℝ E)

Proof state:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
⊢ dimH s = ↑(finrank ℝ E)

Tactic:
have e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ :=
  ContinuousLinearEquiv.ofFinrankEq (Module.finrank_fin_fun ℝ).symm

Result:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ dimH s = ↑(finrank ℝ E)

Proof state:
case refine_2
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ ↑(finrank ℝ E) ≤ dimH (⇑e '' s)

Tactic:
have : e '' s ∈ 𝓝 (e x) := by rw [← e.map_nhds_eq]; exact image_mem_map h

Result:
case refine_2
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
this : ⇑e '' s ∈ 𝓝 (e x)
⊢ ↑(finrank ℝ E) ≤ dimH (⇑e '' s)

Proof state:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ ⇑e '' s ∈ 𝓝 (e x)

Tactic:
rw [← e.map_nhds_eq]

Result:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ ⇑e '' s ∈ Filter.map (⇑e) (𝓝 x)

Proof state:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ dimH (⇑e '' s) = ↑(finrank ℝ E)

Tactic:
refine le_antisymm ?_ ?_

Result:
case refine_1
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ dimH (⇑e '' s) ≤ ↑(finrank ℝ E)

case refine_2
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ ↑(finrank ℝ E) ≤ dimH (⇑e '' s)

Proof state:
case refine_1
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ dimH (⇑e '' s) ≤ ↑(finrank ℝ E)

Tactic:
exact (dimH_mono (subset_univ _)).trans_eq (dimH_univ_pi_fin _)

Result:
no goals