awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ Membership.mem (γ := Filter (Fin (finrank ℝ E) → ℝ)) (Filter.map (⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) (𝓝 x))
    ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s)

Tactic:
image_mem_map h

Premises used: Filter.image_mem_map
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ Membership.mem (γ := Filter (Fin (finrank ℝ E) → ℝ)) (Filter.map (⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) (𝓝 x))
    ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s)

Tactic:
exact image_mem_map h

Premises used: Filter.image_mem_map
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ Membership.mem (γ := Filter (Fin (finrank ℝ E) → ℝ))
    (𝓝 ((e : (a : E) → Fin (finrank ℝ E) → ℝ) x) : Filter (Fin (finrank ℝ E) → ℝ))
    ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s)

Tactic:
have : e '' s ∈ 𝓝 (e x) := by rw [← e.map_nhds_eq]; exact image_mem_map h
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
this :
  Membership.mem (γ := Filter (Fin (finrank ℝ E) → ℝ))
    (𝓝 ((e : (a : E) → Fin (finrank ℝ E) → ℝ) x) : Filter (Fin (finrank ℝ E) → ℝ))
    ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s)
refine_2 :
  ∀ (r : ℝ) (hr0 : 0 < r)
    (hr :
      Subset (α := Set (Fin (finrank ℝ E) → ℝ))
        (Metric.ball ((e : (a : E) → Fin (finrank ℝ E) → ℝ) x) r : Set (Fin (finrank ℝ E) → ℝ))
        ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s : Set (Fin (finrank ℝ E) → ℝ))),
    (↑(finrank ℝ E) : ℝ≥0∞) ≤ dimH (X := Fin (finrank ℝ E) → ℝ) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s)
⊢ (↑(finrank ℝ E) : ℝ≥0∞) ≤ dimH (X := Fin (finrank ℝ E) → ℝ) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s)

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

Premises used: Filter.HasBasis.mem_iff, Iff.mp, Metric.nhds_basis_ball
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
this :
  Membership.mem (γ := Filter (Fin (finrank ℝ E) → ℝ))
    (𝓝 ((e : (a : E) → Fin (finrank ℝ E) → ℝ) x) : Filter (Fin (finrank ℝ E) → ℝ))
    ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s)
r : ℝ
hr0 : 0 < r
hr :
  Subset (α := Set (Fin (finrank ℝ E) → ℝ))
    (Metric.ball ((e : (a : E) → Fin (finrank ℝ E) → ℝ) x) r : Set (Fin (finrank ℝ E) → ℝ))
    ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s : Set (Fin (finrank ℝ E) → ℝ))
⊢ (↑(finrank ℝ E) : ℝ≥0∞) ≤ dimH (X := Fin (finrank ℝ E) → ℝ) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' s)

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

Premises used: dimH_mono, Real.dimH_ball_pi_fin, DFunLike.coe
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
h : (interior s).Nonempty
⊢ dimH s = (↑(finrank ℝ E) : ℝ≥0∞)

Tactic:
let ⟨_, hx⟩ := h
  dimH_of_mem_nhds (mem_interior_iff_mem_nhds.1 hx)

Premises used: Real.dimH_of_mem_nhds, Real, mem_interior_iff_mem_nhds, _private.0.Real.dimH_of_nonempty_interior.match_1, Nat.cast, Iff.mp, Eq, dimH, Module.finrank
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hcvx : Convex ℝ s
hne : s.Nonempty
⊢ Nonempty.{u_4 + 1} (↑s : Type u_4)

Tactic:
have := hne.to_subtype
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hcvx : Convex ℝ s
hne : s.Nonempty
this : Nonempty.{u_4 + 1} (↑s : Type u_4)
φ : ↥(affineSpan ℝ s) ≃ᵃⁱ[ℝ] ↥(AffineSubspace.direction (affineSpan ℝ s)) :=
  AffineIsometryEquiv.constVSub ℝ
    (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x) (hne.some (s := s)) ⋯)
⊢ s =
    image (α := ↥(affineSpan ℝ s))
      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x))
      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x) ⁻¹' s)

Tactic:
have hs_eq : s = (↑) '' ((↑) ⁻¹' s : Set (affineSpan ℝ s)) :=
    (image_preimage_eq_of_subset <| (subset_affineSpan ℝ s).trans Subtype.range_coe.superset).symm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hcvx : Convex ℝ s
hne : s.Nonempty
this : Nonempty.{u_4 + 1} (↑s : Type u_4)
φ : ↥(affineSpan ℝ s) ≃ᵃⁱ[ℝ] ↥(AffineSubspace.direction (affineSpan ℝ s)) :=
  AffineIsometryEquiv.constVSub ℝ
    (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x) (hne.some (s := s)) ⋯)
hs_eq :
  s =
    image (α := ↥(affineSpan ℝ s))
      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x))
      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x) ⁻¹' s)
rw :
  Set.Nonempty (α := ↥(AffineSubspace.direction (affineSpan ℝ s)))
    (interior
      (image (α := ↥(affineSpan ℝ s)) (⇑φ : (a : ↥(affineSpan ℝ s)) → ↥(affineSpan ℝ s).direction)
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x) ⁻¹' s)))
⊢ dimH s = (↑(finrank.{0, u_4} ℝ ↥(vectorSpan ℝ s)) : ℝ≥0∞)

Tactic:
rw [hs_eq, isometry_subtype_coe.dimH_image, ← φ.isometry.dimH_image,
      Real.dimH_of_nonempty_interior, direction_affineSpan ℝ s, ← hs_eq]

Premises used: direction_affineSpan, Real, Real.dimH_of_nonempty_interior, AffineIsometryEquiv.isometry, Isometry.dimH_image
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hcvx : Convex ℝ s
hne : s.Nonempty
this : Nonempty.{u_4 + 1} (↑s : Type u_4)
φ : ↥(affineSpan ℝ s) ≃ᵃⁱ[ℝ] ↥(AffineSubspace.direction (affineSpan ℝ s)) :=
  AffineIsometryEquiv.constVSub ℝ
    (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x) (hne.some (s := s)) ⋯)
hs_eq :
  s =
    image (α := ↥(affineSpan ℝ s))
      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x))
      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x) ⁻¹' s)
simp_rw :
  Set.Nonempty (α := ↥(affineSpan ℝ s))
    (interior (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x) ⁻¹' s))
⊢ Set.Nonempty (α := ↥(AffineSubspace.direction (affineSpan ℝ s)))
    (interior
      (image (α := ↥(affineSpan ℝ s)) (⇑φ : (a : ↥(affineSpan ℝ s)) → ↥(affineSpan ℝ s).direction)
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AffineSubspace ℝ E) (affineSpan ℝ s) x) ⁻¹' s)))

Tactic:
simp_rw [← AffineIsometryEquiv.coe_toHomeomorph, ← φ.toHomeomorph.image_interior, image_nonempty]

Premises used: Set.image_nonempty, Homeomorph.image_interior, AffineIsometryEquiv.coe_toHomeomorph, AffineIsometryEquiv.toHomeomorph
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
⊢ dimH.{u_4} (X := E) univ = (↑(finrank ℝ E) : ℝ≥0∞)

Tactic:
dimH_of_mem_nhds (@univ_mem _ (𝓝 0))

Premises used: Real.dimH_of_mem_nhds, Filter.univ_mem
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
rw : Eq (α := ℝ≥0∞) (↑(finrank ℝ ℝ) : ℝ≥0∞) 1
rw₁ : Eq (α := ℝ≥0∞) (↑1 : ℝ≥0∞) 1
rw₂ rw₃ : Eq (α := ℝ≥0∞) 1 1
⊢ dimH (X := ℝ) univ = 1

Tactic:
rw [dimH_univ_eq_finrank ℝ, Module.finrank_self, Nat.cast_one]

Premises used: Real, Real.dimH_univ_eq_finrank, Module.finrank_self, Nat.cast_one
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
⊢ dimH s ≤ dimH.{u_4} (X := E) univ

Tactic:
dimH_mono (subset_univ s)

Premises used: Set.subset_univ, dimH_mono
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
⊢ dimH.{u_4} (X := E) univ = (↑(finrank ℝ E) : ℝ≥0∞)

Tactic:
dimH_univ_eq_finrank E

Premises used: Real.dimH_univ_eq_finrank
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
⊢ LT.lt (α := ℝ≥0∞) (↑(finrank ℝ E) : ℝ≥0∞) ∞

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
dimH : LT.lt (α := ℝ≥0∞) (↑(finrank ℝ E) : ℝ≥0∞) ∞
⊢ _root_.dimH s < ∞

Tactic:
calc
  dimH s ≤ dimH (univ : Set E) := dimH_mono (subset_univ s)
  _ = finrank ℝ E := dimH_univ_eq_finrank E
  _ < ⊤ := by simp

Premises used: Real, Real.dimH_univ_eq_finrank, Set.subset_univ, Set.univ, dimH_mono, dimH, Module.finrank
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
⊢ dimH s ≠ ∞

Tactic:
(dimH_lt_top s).ne

Premises used: Real.dimH_lt_top, LT.lt.ne
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
d : ℝ
hd : (↑(finrank ℝ E) : ℝ) < d
⊢ 0 ≤ d

Tactic:
(Nat.cast_nonneg _).trans hd.le

Premises used: Nat.cast_nonneg, LT.lt.le, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
d : ℝ
hd : (↑(finrank ℝ E) : ℝ) < d
lift : ∀ (d : ℝ≥0) (hd : (↑(finrank ℝ E) : ℝ) < (↑d : ℝ)), Eq.{u_4 + 1} (α := Measure E) μH[(↑d : ℝ)] 0
⊢ Eq.{u_4 + 1} (α := Measure E) μH[d] 0

Tactic:
lift d to ℝ≥0 using (Nat.cast_nonneg _).trans hd.le

Premises used: Nat.cast_nonneg, LT.lt.le, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
d : ℝ≥0
hd : (↑(finrank ℝ E) : ℝ) < (↑d : ℝ)
rw : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure E) : (a : Set E) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq.{u_4 + 1} (α := Measure E) μH[(↑d : ℝ)] 0

Tactic:
rw [← measure_univ_eq_zero]

Premises used: MeasureTheory.Measure.measure_univ_eq_zero
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
d : ℝ≥0
hd : (↑(finrank ℝ E) : ℝ) < (↑d : ℝ)
h : dimH.{u_4} (X := E) univ < (↑d : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure E) : (a : Set E) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
apply hausdorffMeasure_of_dimH_lt

Premises used: hausdorffMeasure_of_dimH_lt
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
d : ℝ≥0
hd : (↑(finrank ℝ E) : ℝ) < (↑d : ℝ)
h : (↑(finrank ℝ E) : ℝ≥0∞) < (↑d : ℝ≥0∞)
⊢ dimH.{u_4} (X := E) univ < (↑d : ℝ≥0∞)

Tactic:
rw [dimH_univ_eq_finrank]

Premises used: Real.dimH_univ_eq_finrank
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
d : ℝ≥0
hd : (↑(finrank ℝ E) : ℝ) < (↑d : ℝ)
⊢ (↑(finrank ℝ E) : ℝ≥0∞) < (↑d : ℝ≥0∞)

Tactic:
mod_cast hd

Premises used: Real, ENNReal.ofNNReal, congrArg, NNReal.coe_lt_coe._simp_1, cast, NNReal.coe_natCast, WithTop.some, ENNReal.coe_lt_coe._simp_1, LT.lt, Eq.symm, NNReal.toReal, Module.finrank, Eq.trans
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
d : ℝ≥0
hd : (↑(finrank ℝ E) : ℝ) < (↑d : ℝ)
⊢ (↑(finrank ℝ E) : ℝ≥0∞) < (↑d : ℝ≥0∞)

Tactic:
exact mod_cast hd
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x y : E
h : x ≠ y
rw : Eq (α := ℝ≥0∞) (↑(finrank.{0, u_4} ℝ ↥(ℝ ∙ (y -ᵥ x))) : ℝ≥0∞) 1
⊢ dimH (segment ℝ x y) = 1

Tactic:
rw [Convex.dimH_eq_finrank_vectorSpan (convex_segment x y) ⟨x, left_mem_segment ℝ x y⟩,
      vectorSpan_segment]

Premises used: Real, left_mem_segment, vectorSpan_segment, Real.Convex.dimH_eq_finrank_vectorSpan, Exists.intro, convex_segment
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x y : E
h : x ≠ y
⊢ Eq (α := ℝ≥0∞) (↑(finrank.{0, u_4} ℝ ↥(ℝ ∙ (y -ᵥ x))) : ℝ≥0∞) 1

Tactic:
simp [finrank_span_singleton (sub_ne_zero.mpr h.symm)]

Premises used: Iff.mpr, sub_ne_zero, Ne.symm, finrank_span_singleton
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hs : dimH s < (↑(finrank ℝ E) : ℝ≥0∞)
⊢ Dense sᶜ

Tactic:
fun x => mem_closure_iff_nhds.2 fun t ht => nonempty_iff_ne_empty.2 fun he => hs.not_ge ?_

Premises used: Iff.mpr, mem_closure_iff_nhds, Dense, Set.nonempty_iff_ne_empty, LT.lt.not_ge
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hs : dimH s < (↑(finrank ℝ E) : ℝ≥0∞)
refine : ∀ (x : E) (t : Set E) (ht : t ∈ 𝓝 x) (he : t ∩ sᶜ = ∅), (↑(finrank ℝ E) : ℝ≥0∞) ≤ dimH s
⊢ Dense sᶜ

Tactic:
refine fun x => mem_closure_iff_nhds.2 fun t ht => nonempty_iff_ne_empty.2 fun he => hs.not_ge ?_

Premises used: Iff.mpr, mem_closure_iff_nhds, Set.nonempty_iff_ne_empty, LT.lt.not_ge
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hs : dimH s < (↑(finrank ℝ E) : ℝ≥0∞)
x : E
t : Set E
ht : t ∈ 𝓝 x
he : t ∩ sᶜ = ∅
⊢ t ⊆ s

Tactic:
rw [← diff_eq, diff_eq_empty] at he

Premises used: Set.diff_eq, Set.diff_eq_empty
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hs : dimH s < (↑(finrank ℝ E) : ℝ≥0∞)
x : E
t : Set E
ht : t ∈ 𝓝 x
he : t ⊆ s
rw : dimH t ≤ dimH s
⊢ (↑(finrank ℝ E) : ℝ≥0∞) ≤ dimH s

Tactic:
rw [← Real.dimH_of_mem_nhds ht]

Premises used: Real.dimH_of_mem_nhds
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hs : dimH s < (↑(finrank ℝ E) : ℝ≥0∞)
x : E
t : Set E
ht : t ∈ 𝓝 x
he : t ⊆ s
⊢ dimH t ≤ dimH s

Tactic:
dimH_mono he

Premises used: dimH_mono
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hs : dimH s < (↑(finrank ℝ E) : ℝ≥0∞)
x : E
t : Set E
ht : t ∈ 𝓝 x
he : t ⊆ s
⊢ dimH t ≤ dimH s

Tactic:
exact dimH_mono he

Premises used: dimH_mono
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
s t : Set E
hf : ContDiffOn ℝ 1 f s
hc : Convex ℝ s
ht : t ⊆ s
⊢ dimH (f '' t) ≤ dimH t

Tactic:
dimH_image_le_of_locally_lipschitzOn fun x hx =>
    let ⟨C, u, hu, hf⟩ := (hf x (ht hx)).exists_lipschitzOnWith hc
    ⟨C, u, nhdsWithin_mono _ ht hu, hf⟩

Premises used: nhdsWithin, _private.0.ContDiffOn.dimH_image_le.match_1, Membership.mem, Exists, dimH_image_le_of_locally_lipschitzOn, And, And.intro, Exists.intro, LipschitzOnWith, ContDiffWithinAt.exists_lipschitzOnWith, nhdsWithin_mono
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
h : ContDiff ℝ 1 f
rw rw₁ : dimH (range f) = dimH (range f)
⊢ dimH (range f) = dimH (f '' univ)

Tactic:
rw [image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
f : E → F
s t : Set E
h : ContDiffOn ℝ 1 f s
hc : Convex ℝ s
ht : t ⊆ s
htF : dimH t < (↑(finrank ℝ F) : ℝ≥0∞)
⊢ Dense (f '' t)ᶜ

Tactic:
dense_compl_of_dimH_lt_finrank <| (h.dimH_image_le hc ht).trans_lt htF

Premises used: ContDiffOn.dimH_image_le, dense_compl_of_dimH_lt_finrank, LE.le.trans_lt
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
f : E → F
h : ContDiff ℝ 1 f
hEF : finrank ℝ E < finrank ℝ F
⊢ Dense (range f)ᶜ

Tactic:
dense_compl_of_dimH_lt_finrank <| h.dimH_range_le.trans_lt <| Nat.cast_lt.2 hEF

Premises used: Iff.mpr, ContDiff.dimH_range_le, dense_compl_of_dimH_lt_finrank, Nat.cast_lt, LE.le.trans_lt
-- Module: Mathlib.Topology.MetricSpace.HausdorffDimension
Goal:
𝕜 : Type u_6
E : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
s : Set E
⊢ dimH (X := ↥K) ((⇑K.orthogonalProjection : (a : E) → ↥K) '' s) ≤ dimH s

Tactic:
K.lipschitzWith_orthogonalProjection.dimH_image_le s

Premises used: LipschitzWith.dimH_image_le, Submodule.lipschitzWith_orthogonalProjection
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
⊢ infEDist x ∅ = ∞

Tactic:
iInf_emptyset

Premises used: Metric.infEDist, iInf_emptyset
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
d : ℝ≥0∞
⊢ d ≤ infEDist x s ↔ ∀ y ∈ s, d ≤ edist x y

Tactic:
simp only [infEDist, le_iInf_iff]

Premises used: le_iInf_iff, Metric.infEDist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s t : Set α
⊢ infEDist x (s ∪ t) = min (infEDist x s) (infEDist x t)

Tactic:
iInf_union

Premises used: Metric.infEDist, iInf_union
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
ι : Sort u_1
α : Type u
inst : PseudoEMetricSpace α
f : ι → Set α
x : α
⊢ infEDist x (⋃ (i : ι), f i) = ⨅ (i : ι), infEDist x (f i)

Tactic:
iInf_iUnion f _

Premises used: Metric.infEDist, iInf_iUnion
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
ι : Type u_2
f : ι → Set α
I : Set ι
x : α
⊢ infEDist x (⋃ i ∈ I, f i) = ⨅ i ∈ I, infEDist x (f i)

Tactic:
simp only [infEDist_iUnion]

Premises used: Metric.infEDist_iUnion
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
⊢ infEDist x {y} = edist x y

Tactic:
iInf_singleton

Premises used: Metric.infEDist, iInf_singleton
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
s : Set α
h : y ∈ s
⊢ infEDist x s ≤ edist x y

Tactic:
iInf₂_le y h

Premises used: iInf₂_le, Metric.infEDist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
h : x ∈ s
⊢ infEDist x s = 0

Tactic:
nonpos_iff_eq_zero.1 <| @edist_self _ _ x ▸ infEDist_le_edist_of_mem h

Premises used: Iff.mp, nonpos_iff_eq_zero
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s t : Set α
h : s ⊆ t
⊢ infEDist x t ≤ infEDist x s

Tactic:
iInf_le_iInf_of_subset h

Premises used: Metric.infEDist, iInf_le_iInf_of_subset
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
simp_rw : ⨅ y ∈ s, edist x y < r ↔ ∃ y ∈ s, edist x y < r
simp_rw₁ : (∃ (i : α) (_ : i ∈ s), edist x i < r) ↔ ∃ y ∈ s, edist x y < r
⊢ infEDist x s < r ↔ ∃ y ∈ s, edist x y < r

Tactic:
simp_rw [infEDist, iInf_lt_iff, exists_prop]

Premises used: Metric.infEDist, exists_prop, iInf_lt_iff
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
s : Set α
⊢ ⨅ z ∈ s, edist y z + edist x y = (⨅ z ∈ s, edist y z) + edist x y

Tactic:
simp only [ENNReal.iInf_add]

Premises used: ENNReal.iInf_add
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
s : Set α
rw : infEDist x s ≤ infEDist y s + edist x y
⊢ infEDist x s ≤ edist x y + infEDist y s

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
s : Set α
⊢ infEDist x s ≤ infEDist y s + edist x y

Tactic:
infEDist_le_infEDist_add_edist

Premises used: Metric.infEDist_le_infEDist_add_edist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
s : Set α
⊢ infEDist x s ≤ infEDist y s + edist x y

Tactic:
exact infEDist_le_infEDist_add_edist

Premises used: Metric.infEDist_le_infEDist_add_edist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
s : Set α
hy : y ∈ s
simp_rw : edist x y ≤ ⨅ i ∈ s, edist x i + ediam s
⊢ edist x y ≤ infEDist x s + ediam s

Tactic:
simp_rw [infEDist, ENNReal.iInf_add]

Premises used: ENNReal.iInf_add, Metric.infEDist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
s : Set α
hy : y ∈ s
⊢ edist x y ≤ ⨅ i ∈ s, edist x i + ediam s

Tactic:
le_iInf₂ fun i hi => ?_

Premises used: le_iInf₂
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
s : Set α
hy : y ∈ s
refine : ∀ (i : α) (hi : i ∈ s), edist x y ≤ edist x i + ediam s
⊢ edist x y ≤ ⨅ i ∈ s, edist x i + ediam s

Tactic:
refine le_iInf₂ fun i hi => ?_

Premises used: le_iInf₂
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
s : Set α
hy : y ∈ s
i : α
hi : i ∈ s
⊢ edist x y ≤ edist x i + edist i y

Tactic:
edist_triangle _ _ _

Premises used: PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
s : Set α
hy : y ∈ s
i : α
hi : i ∈ s
⊢ edist x i + edist i y ≤ edist x i + ediam s

Tactic:
add_le_add le_rfl (Metric.edist_le_ediam_of_mem hi hy)

Premises used: le_rfl, add_le_add, Metric.edist_le_ediam_of_mem