mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f '' s) = ∞
this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ∞
Hrd : μH[↑(r * d)] s = ∞
⊢ ↑(r * d) ≤ dimH s

pp: case h0
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f '' s) = ∞
this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ∞
Hrd : μH[↑(r * d)] s = ∞
⊢ ↑r ≠ 0 ∨ dimH s ≠ 0

pp: case ht
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f '' s) = ∞
this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ∞
Hrd : μH[↑(r * d)] s = ∞
⊢ ↑r ≠ ∞ ∨ dimH s ≠ ∞

Tactic:
]

Goal state after:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f '' s) = ∞
this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ∞
Hrd : μH[↑(r * d)] s = ∞
⊢ ↑(r * d) ≤ dimH s

case h0
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f '' s) = ∞
this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ∞
Hrd : μH[↑(r * d)] s = ∞
⊢ ↑r ≠ 0 ∨ dimH s ≠ 0

case ht
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f '' s) = ∞
this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ∞
Hrd : μH[↑(r * d)] s = ∞
⊢ ↑r ≠ ∞ ∨ dimH s ≠ ∞
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
hs : Nonempty ↥s
t : Set P
ht : MeasurableSet t
p : ↥s
x : ↥s.direction
u : Set ↥(mk' (↑(x +ᵥ p)) s.directionᗮ) := Subtype.val ⁻¹' (t ∩ ↑(mk' (↑(x +ᵥ p)) s.directionᗮ))
hu : MeasurableSet u
hinter : t ∩ ↑(mk' (↑(x +ᵥ p)) s.directionᗮ) = Subtype.val '' u
hxp : ↑(x +ᵥ p) ∈ mk' (↑(x +ᵥ p)) s.directionᗮ
⊢ finrank ℝ ↥s.directionᗮ = finrank ℝ ↥s.directionᗮ

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
h : f.ker = ⊥
g : U ≃ₗ[𝕜] ↥f.range := LinearEquiv.ofBijective f.rangeRestrict ⋯
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range := ⋯ ▸ stdOrthonormalBasis 𝕜 ↥f.range
⊢ ¬((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det = 0

Tactic:
]

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
h : f.ker = ⊥
g : U ≃ₗ[𝕜] ↥f.range := LinearEquiv.ofBijective f.rangeRestrict ⋯
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range := ⋯ ▸ stdOrthonormalBasis 𝕜 ↥f.range
⊢ ¬((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det = 0
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
C : X → ℝ≥0
t : X → Set X
htn : ∀ x ∈ s, t x ∈ 𝓝[s] x
hC : ∀ x ∈ s, HolderOnWith (C x) r f (t x)
u : Set X
hus : u ⊆ s
huc : u.Countable
huU : ⋃ i ∈ u, s ∩ t i = s
⊢ dimH (f '' s) ≤ dimH s / ↑r

Tactic:
]

Goal state after:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
C : X → ℝ≥0
t : X → Set X
htn : ∀ x ∈ s, t x ∈ 𝓝[s] x
hC : ∀ x ∈ s, HolderOnWith (C x) r f (t x)
u : Set X
hus : u ⊆ s
huc : u.Countable
huU : ⋃ i ∈ u, s ∩ t i = s
⊢ dimH (f '' s) ≤ dimH s / ↑r
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: case e_f
V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
hs : Nonempty ↥s
t : Set P
ht : MeasurableSet t
p : ↥s
x : ↥s.direction
u : Set ↥(mk' (↑(x +ᵥ p)) s.directionᗮ) := Subtype.val ⁻¹' (t ∩ ↑(mk' (↑(x +ᵥ p)) s.directionᗮ))
hu : MeasurableSet u
hinter : t ∩ ↑(mk' (↑(x +ᵥ p)) s.directionᗮ) = Subtype.val '' u
hxp : ↑(x +ᵥ p) ∈ mk' (↑(x +ᵥ p)) s.directionᗮ
hrank : finrank ℝ ↥s.directionᗮ = finrank ℝ ↥(mk' (↑(x +ᵥ p)) s.directionᗮ).direction
⊢ volume (Prod.mk x ⁻¹' ⇑(s.direction.measurableEquivProd ↑p).symm ⁻¹' t) =
    volume (⇑(IsometryEquiv.vaddConst ⟨↑(x +ᵥ p), hxp⟩) ⁻¹' u)

Tactic:
]

Goal state after:
case e_f
V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
hs : Nonempty ↥s
t : Set P
ht : MeasurableSet t
p : ↥s
x : ↥s.direction
u : Set ↥(mk' (↑(x +ᵥ p)) s.directionᗮ) := Subtype.val ⁻¹' (t ∩ ↑(mk' (↑(x +ᵥ p)) s.directionᗮ))
hu : MeasurableSet u
hinter : t ∩ ↑(mk' (↑(x +ᵥ p)) s.directionᗮ) = Subtype.val '' u
hxp : ↑(x +ᵥ p) ∈ mk' (↑(x +ᵥ p)) s.directionᗮ
hrank : finrank ℝ ↥s.directionᗮ = finrank ℝ ↥(mk' (↑(x +ᵥ p)) s.directionᗮ).direction
⊢ volume (Prod.mk x ⁻¹' ⇑(s.direction.measurableEquivProd ↑p).symm ⁻¹' t) =
    volume (⇑(IsometryEquiv.vaddConst ⟨↑(x +ᵥ p), hxp⟩) ⁻¹' u)
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
C : X → ℝ≥0
t : X → Set X
htn : ∀ x ∈ s, t x ∈ 𝓝[s] x
hC : ∀ x ∈ s, HolderOnWith (C x) r f (t x)
u : Set X
hus : u ⊆ s
huc : u.Countable
huU : ⋃ i ∈ u, s ∩ t i = s
⊢ ⨆ i ∈ u, dimH (f '' (s ∩ t i)) ≤ (⨆ i ∈ u, dimH (s ∩ t i)) / ↑r

Tactic:
]

Goal state after:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
C : X → ℝ≥0
t : X → Set X
htn : ∀ x ∈ s, t x ∈ 𝓝[s] x
hC : ∀ x ∈ s, HolderOnWith (C x) r f (t x)
u : Set X
hus : u ⊆ s
huc : u.Countable
huU : ⋃ i ∈ u, s ∩ t i = s
⊢ ⨆ i ∈ u, dimH (f '' (s ∩ t i)) ≤ (⨆ i ∈ u, dimH (s ∩ t i)) / ↑r
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
tfae_1_iff_2 : f.normDet ≠ 0 ↔ f.ker = ⊥
tfae_1_iff_3 : f.normDet ≠ 0 ↔ finrank 𝕜 ↥f.range = finrank 𝕜 U
h : finrank 𝕜 ↥f.range = finrank 𝕜 U
⊢ Nonempty (OrthonormalBasis (Fin (finrank 𝕜 ↥f.range)) 𝕜 ↥f.range)

Tactic:
]

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
tfae_1_iff_2 : f.normDet ≠ 0 ↔ f.ker = ⊥
tfae_1_iff_3 : f.normDet ≠ 0 ↔ finrank 𝕜 ↥f.range = finrank 𝕜 U
h : finrank 𝕜 ↥f.range = finrank 𝕜 U
⊢ Nonempty (OrthonormalBasis (Fin (finrank 𝕜 ↥f.range)) 𝕜 ↥f.range)
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case neg
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
S : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ∞
r n i j : ℕ
hj : i < j
A : (↑(2 * j + r))⁻¹ < (↑(2 * i + 1 + r))⁻¹
x : X
hx : x ∈ S (2 * i + 1 + r)
y : X
hy : y ∈ s \ S (2 * j + r)
this : infEDist y t < (↑(2 * j + r))⁻¹
z : X
hzt : z ∈ t
hyz : edist y z < (↑(2 * j + r))⁻¹
hxz : (↑(2 * i + 1 + r))⁻¹ ≤ edist x z
⊢ (↑(2 * i + 1 + r))⁻¹ = (↑(2 * i + 1 + r))⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
μ : OuterMeasure X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
hm : μ.IsMetric
⊢ borel X ≤ μ.caratheodory

Tactic:
]

Goal state after:
X : Type u_2
inst✝² : EMetricSpace X
μ : OuterMeasure X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
hm : μ.IsMetric
⊢ borel X ≤ μ.caratheodory
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ Tendsto (fun x ↦ (pre m ↑x) s) atBot (𝓝 ((mkMetric' m) s))

Tactic:
]

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ Tendsto (fun x ↦ (pre m ↑x) s) atBot (𝓝 ((mkMetric' m) s))
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, HolderOnWith C r f s
⊢ dimH (f '' univ) ≤ dimH univ / ↑r

Tactic:
]

Goal state after:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, HolderOnWith C r f s
⊢ dimH (f '' univ) ≤ dimH univ / ↑r
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
⊢ [f.normDet ≠ 0, f.ker = ⊥, finrank 𝕜 ↥f.range = finrank 𝕜 U,
      Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range), Function.Injective ⇑f].TFAE

Tactic:
by
  tfae_have 1 ↔ 2 := f.normDet_eq_zero_iff_ker_ne_bot.not_left
  tfae_have 1 ↔ 3 := f.normDet_eq_zero_iff_rank_range_ne.not_left
  tfae_have 3 → 4 := by
    intro h
    rw [← h]
    exact ⟨stdOrthonormalBasis 𝕜 f.range⟩
  tfae_have 4 → 3 := by
    rintro ⟨b⟩
    simpa using Module.finrank_eq_card_basis b.toBasis
  tfae_have 2 ↔ 5 := ker_eq_bot
  tfae_finish

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ (mkMetric' m) s = ⨆ i, (pre m (↑i)⁻¹) s

Tactic:
]

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ (mkMetric' m) s = ⨆ i, (pre m (↑i)⁻¹) s
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
f : X → Y
hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, LipschitzOnWith C f s
⊢ dimH (f '' univ) ≤ dimH univ

Tactic:
]

Goal state after:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
f : X → Y
hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, LipschitzOnWith C f s
⊢ dimH (f '' univ) ≤ dimH univ
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
m : Set X → ℝ≥0∞
hcl : ∀ (s : Set X), m (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = m s
r : ℝ≥0∞
s : Set X
hs : ediam s ≤ r
⊢ ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (pre m r) t ≤ m s

Tactic:
]

Goal state after:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
m : Set X → ℝ≥0∞
hcl : ∀ (s : Set X), m (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = m s
r : ℝ≥0∞
s : Set X
hs : ediam s ≤ r
⊢ ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (pre m r) t ≤ m s
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
m : Set X → ℝ≥0∞
hcl : ∀ (s : Set X), m (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = m s
r : ℝ≥0∞
s : Set X
hs : ediam s ≤ r
⊢ ediam s ≤ r

Tactic:
]

Goal state after:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
m : Set X → ℝ≥0∞
hcl : ∀ (s : Set X), m (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = m s
r : ℝ≥0∞
s : Set X
hs : ediam s ≤ r
⊢ ediam s ≤ r
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s t : Set X
r : ℝ≥0∞
r0 : 0 < r
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
⊢ (fun r ↦ (mkMetric'.pre m r) (s ∪ t)) =ᶠ[𝓝[>] 0] fun x ↦ (mkMetric'.pre m x) s + (mkMetric'.pre m x) t

Tactic:
]

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s t : Set X
r : ℝ≥0∞
r0 : 0 < r
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
⊢ (fun r ↦ (mkMetric'.pre m r) (s ∪ t)) =ᶠ[𝓝[>] 0] fun x ↦ (mkMetric'.pre m x) s + (mkMetric'.pre m x) t
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
K : ℝ≥0
f : X → Y
hf : AntilipschitzWith K f
s : Set Y
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f ⁻¹' s) = ∞
this : ↑K ^ ↑d * μH[↑d] s = ∞
⊢ μH[↑d] s = ∞

Tactic:
]

Goal state after:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
K : ℝ≥0
f : X → Y
hf : AntilipschitzWith K f
s : Set Y
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f ⁻¹' s) = ∞
this : ↑K ^ ↑d * μH[↑d] s = ∞
⊢ μH[↑d] s = ∞
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
e : X ≃ᵢ Y
s : Set Y
⊢ dimH s = dimH s

Tactic:
]

Goal state after:
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
e : X ≃ᵢ Y
⊢ dimH univ = dimH univ

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
⊢ finrank ℝ ↥(ℝ ∙ v) = 1

Tactic:
]

Goal state after:
V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
⊢ finrank ℝ ↥(ℝ ∙ v) = 1
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: case pos
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 V
this : FiniteDimensional 𝕜 V
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
h : f.range = ⊤
bv' : OrthonormalBasis ι 𝕜 ↥f.range := bv.map (LinearIsometryEquiv.ofTop V f.range h).symm
⊢ ‖((toMatrix bu.toBasis bv'.toBasis) f.rangeRestrict).det‖ = ‖((toMatrix bu.toBasis bv.toBasis) f).det‖

Tactic:
]

Goal state after:
case pos
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 V
this : FiniteDimensional 𝕜 V
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
h : f.range = ⊤
bv' : OrthonormalBasis ι 𝕜 ↥f.range := bv.map (LinearIsometryEquiv.ofTop V f.range h).symm
⊢ ‖((toMatrix bu.toBasis bv'.toBasis) f.rangeRestrict).det‖ = ‖((toMatrix bu.toBasis bv.toBasis) f).det‖
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] F
s : Set F
⊢ dimH s = dimH s

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
hrank : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction = 1
⊢ finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ = finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ

Tactic:
]

Goal state after:
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] F
⊢ dimH univ = dimH univ

Tactic:
]

Goal state after:
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: case inl
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : IsEmpty ι
⊢ IsEmpty ι

pp: case inl
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : IsEmpty ι
⊢ (Metric.ball x r).Subsingleton

Tactic:
]

Goal state after:
case inl
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : IsEmpty ι
⊢ IsEmpty ι

case inl
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : IsEmpty ι
⊢ (Metric.ball x r).Subsingleton
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: case inr
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
⊢ dimH (Metric.ball x r) = ↑↑(Fintype.card ι)

Tactic:
]

Goal state after:
case inr
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
⊢ dimH (Metric.ball x r) = ↑↑(Fintype.card ι)
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
⊢ ENNReal.ofReal ((2 * r) ^ Fintype.card ι) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
r : ℝ≥0∞
hr0 : r ∈ Ioi 0
hr : Ico 0 r ⊆ {x | (fun x ↦ m₁ x ≤ (c • m₂) x) x}
s : Set X
r' : ℝ≥0∞
hr' : r' ∈ Ioo 0 r
⊢ (boundedBy (extend fun s x ↦ m₁ (ediam s))) s ≤ (boundedBy (c • extend fun s x ↦ m₂ (ediam s))) s

Tactic:
]

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
r : ℝ≥0∞
hr0 : r ∈ Ioi 0
hr : Ico 0 r ⊆ {x | (fun x ↦ m₁ x ≤ (c • m₂) x) x}
s : Set X
r' : ℝ≥0∞
hr' : r' ∈ Ioo 0 r
⊢ (boundedBy (extend fun s x ↦ m₁ (ediam s))) s ≤ (boundedBy (c • extend fun s x ↦ m₂ (ediam s))) s
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: case neg
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 V
this : FiniteDimensional 𝕜 V
hrank : finrank 𝕜 U ≠ finrank 𝕜 ↥f.range
⊢ ‖((toMatrix bu.toBasis bv.toBasis) f).det‖ = 0

Tactic:
]

Goal state after:
case neg
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 V
this : FiniteDimensional 𝕜 V
hrank : finrank 𝕜 U ≠ finrank 𝕜 ↥f.range
⊢ ‖((toMatrix bu.toBasis bv.toBasis) f).det‖ = 0
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: case inr.refine_1
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
this : μH[↑(Fintype.card ι)] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
⊢ ENNReal.ofReal ((2 * r) ^ Fintype.card ι) ≠ 0

Tactic:
]

Goal state after:
case inr.refine_1
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
this : μH[↑(Fintype.card ι)] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
⊢ ENNReal.ofReal ((2 * r) ^ Fintype.card ι) ≠ 0
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: case neg
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 V
this : FiniteDimensional 𝕜 V
hdet : ¬‖((toMatrix bu.toBasis bv.toBasis) f).det‖ = 0
h : IsUnit ((toMatrix bu.toBasis bv.toBasis) f).det
f' : U ≃ₗ[𝕜] V := LinearEquiv.ofIsUnitDet h
hf : f.range = ⊤
⊢ finrank 𝕜 U = finrank 𝕜 ↥⊤

Tactic:
]

Goal state after:
case neg
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 V
this : FiniteDimensional 𝕜 V
hdet : ¬‖((toMatrix bu.toBasis bv.toBasis) f).det‖ = 0
h : IsUnit ((toMatrix bu.toBasis bv.toBasis) f).det
f' : U ≃ₗ[𝕜] V := LinearEquiv.ofIsUnitDet h
hf : f.range = ⊤
⊢ finrank 𝕜 U = finrank 𝕜 ↥⊤
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: case inr.refine_2
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
this : μH[↑(Fintype.card ι)] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
⊢ ENNReal.ofReal ((2 * r) ^ Fintype.card ι) ≠ ∞

Tactic:
]

Goal state after:
case inr.refine_2
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
this : μH[↑(Fintype.card ι)] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
⊢ ENNReal.ofReal ((2 * r) ^ Fintype.card ι) ≠ ∞