awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
Goal:
X : Type u_2
inst : EMetricSpace X
ι : Sort u_4
inst_1 : Countable ι
s : ι → Set X
⊢ dimH.{u_2} (X := X) (⋃ (i : ι), s i) = ⨆ (i : ι), dimH (s i)
have this : let this := borel X;
BorelSpace X
Tactic: borelize X
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
ι : Sort u_4
inst_1 : Countable ι
s : ι → Set X
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
⊢ dimH.{u_2} (X := X) (⋃ (i : ι), s i) = ⨆ (i : ι), dimH (s i)
have refine : ∀ (d : ℝ≥0)
  (hd : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  (↑d : ℝ≥0∞) ≤ ⨆ (i : ι), dimH (s i)
Tactic: refine le_antisymm (dimH_le fun d hd => ?_) (iSup_le fun i => dimH_mono <| subset_iUnion _ _)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
ι : Sort u_4
inst_1 : Countable ι
s : ι → Set X
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
d : ℝ≥0
hd : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (↑d : ℝ≥0∞) ≤ ⨆ (i : ι), dimH (s i)
have contrapose! : ∀ (hd : ⨆ (i : ι), dimH (s i) < (↑d : ℝ≥0∞)),
  Ne (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: contrapose! hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
Goal:
X : Type u_2
inst : EMetricSpace X
ι : Sort u_4
inst_1 : Countable ι
s : ι → Set X
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
d : ℝ≥0
hd : ⨆ (i : ι), dimH (s i) < (↑d : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
have this : ∀ (i : ι), Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have : ∀ i, μH[d] (s i) = 0 := fun i =>
    hausdorffMeasure_of_dimH_lt ((le_iSup (fun i => dimH (s i)) i).trans_lt hd)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
ι : Sort u_4
inst_1 : Countable ι
s : ι → Set X
this_1 : MeasurableSpace X := borel X
this_2 : BorelSpace X
d : ℝ≥0
hd : ⨆ (i : ι), dimH (s i) < (↑d : ℝ≥0∞)
this : ∀ (i : ι), Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : Ne (α := ℝ≥0∞) 0 ∞
Tactic: rw [measure_iUnion_null this]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
s : Set ι
hs : s.Countable
t : ι → Set X
⊢ dimH.{u_2} (X := X) (⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH (t i)
have haveI : ∀ (this : Encodable (↑s : Type u_1)), dimH.{u_2} (X := X) (⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH (t i)
Tactic: haveI := hs.toEncodable
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
s : Set ι
hs : s.Countable
t : ι → Set X
this : Encodable (↑s : Type u_1)
⊢ dimH.{u_2} (X := X) (⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH (t i)
have rw : dimH.{u_2} (X := X) (⋃ (x : (↑s : Type u_1)), t (↑x : ι)) = ⨆ i ∈ s, dimH (t i)
Tactic: rw [biUnion_eq_iUnion, dimH_iUnion, ← iSup_subtype'']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
s : Set ι
hs : s.Countable
t : ι → Set X
this : Encodable (↑s : Type u_1)
rw : dimH.{u_2} (X := X) (⋃ (x : (↑s : Type u_1)), t (↑x : ι)) = ⨆ i ∈ s, dimH (t i)
⊢ dimH.{u_2} (X := X) (⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH (t i)
have rw₁ : Eq (α := ℝ≥0∞) (⨆ (i : (↑s : Type u_1)), dimH (t (↑i : ι))) (⨆ i ∈ s, dimH (t i))
Tactic: rw [biUnion_eq_iUnion, dimH_iUnion, ← iSup_subtype'']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
s : Set ι
hs : s.Countable
t : ι → Set X
this : Encodable (↑s : Type u_1)
rw : dimH.{u_2} (X := X) (⋃ (x : (↑s : Type u_1)), t (↑x : ι)) = ⨆ i ∈ s, dimH (t i)
rw₁ : Eq (α := ℝ≥0∞) (⨆ (i : (↑s : Type u_1)), dimH (t (↑i : ι))) (⨆ i ∈ s, dimH (t i))
⊢ dimH.{u_2} (X := X) (⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH (t i)
have rw₂ : Eq (α := ℝ≥0∞) (⨆ (i : (↑s : Type u_1)), dimH (t (↑i : ι))) (⨆ (i : (↑s : Type u_1)), dimH (t (↑i : ι)))
Tactic: rw [biUnion_eq_iUnion, dimH_iUnion, ← iSup_subtype'']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
S : Set (Set X)
hS : S.Countable
⊢ dimH (⋃₀ S) = ⨆ s ∈ S, dimH s
have rw : dimH.{u_2} (X := X) (⋃ i ∈ S, i) = ⨆ s ∈ S, dimH s
Tactic: rw [sUnion_eq_biUnion, dimH_bUnion hS]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
S : Set (Set X)
hS : S.Countable
rw : dimH.{u_2} (X := X) (⋃ i ∈ S, i) = ⨆ s ∈ S, dimH s
⊢ dimH (⋃₀ S) = ⨆ s ∈ S, dimH s
have rw₁ : Eq (α := ℝ≥0∞) (⨆ i ∈ S, dimH i) (⨆ s ∈ S, dimH s)
Tactic: rw [sUnion_eq_biUnion, dimH_bUnion hS]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
s t : Set X
⊢ dimH (s ∪ t) = max (dimH s) (dimH t)
have rw : dimH.{u_2} (X := X) (⋃ (b : Bool), bif b then s else t) = max (dimH s) (dimH t)
Tactic: rw [union_eq_iUnion, dimH_iUnion, iSup_bool_eq, cond, cond]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
s t : Set X
rw : dimH.{u_2} (X := X) (⋃ (b : Bool), bif b then s else t) = max (dimH s) (dimH t)
⊢ dimH (s ∪ t) = max (dimH s) (dimH t)
have rw₁ : ⨆ (i : Bool), dimH (bif i then s else t) = max (dimH s) (dimH t)
Tactic: rw [union_eq_iUnion, dimH_iUnion, iSup_bool_eq, cond, cond]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
s t : Set X
rw : dimH.{u_2} (X := X) (⋃ (b : Bool), bif b then s else t) = max (dimH s) (dimH t)
rw₁ : ⨆ (i : Bool), dimH (bif i then s else t) = max (dimH s) (dimH t)
⊢ dimH (s ∪ t) = max (dimH s) (dimH t)
have rw₂ : max (dimH (bif true then s else t)) (dimH (bif false then s else t)) = max (dimH s) (dimH t)
Tactic: rw [union_eq_iUnion, dimH_iUnion, iSup_bool_eq, cond, cond]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
s t : Set X
rw : dimH.{u_2} (X := X) (⋃ (b : Bool), bif b then s else t) = max (dimH s) (dimH t)
rw₁ : ⨆ (i : Bool), dimH (bif i then s else t) = max (dimH s) (dimH t)
rw₂ : max (dimH (bif true then s else t)) (dimH (bif false then s else t)) = max (dimH s) (dimH t)
⊢ dimH (s ∪ t) = max (dimH s) (dimH t)
have rw₃ : max (dimH s) (dimH (bif false then s else t)) = max (dimH s) (dimH t)
Tactic: rw [union_eq_iUnion, dimH_iUnion, iSup_bool_eq, cond, cond]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
s t : Set X
rw : dimH.{u_2} (X := X) (⋃ (b : Bool), bif b then s else t) = max (dimH s) (dimH t)
rw₁ : ⨆ (i : Bool), dimH (bif i then s else t) = max (dimH s) (dimH t)
rw₂ : max (dimH (bif true then s else t)) (dimH (bif false then s else t)) = max (dimH s) (dimH t)
rw₃ : max (dimH s) (dimH (bif false then s else t)) = max (dimH s) (dimH t)
⊢ dimH (s ∪ t) = max (dimH s) (dimH t)
have rw₄ : max (dimH s) (dimH t) = max (dimH s) (dimH t)
Tactic: rw [union_eq_iUnion, dimH_iUnion, iSup_bool_eq, cond, cond]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
h : r < dimH s
⊢ ∃ x ∈ s, ∀ t ∈ 𝓝[s] x, r < dimH t
have contrapose! : ∀ (h : ∀ (x : X) (_ : x ∈ s), ∃ t ∈ 𝓝[s] x, dimH t ≤ r), dimH s ≤ r
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
h : ∀ (x : X) (_ : x ∈ s), ∃ t ∈ 𝓝[s] x, dimH t ≤ r
⊢ dimH s ≤ r
have choose! : ∀ (t : (x : X) → Set X) (htx : ∀ (x : X) (_ : x ∈ s), t x ∈ 𝓝[s] x) (htr : ∀ (x : X) (_ : x ∈ s), dimH (t x) ≤ r),
  dimH s ≤ r
Tactic: choose! t htx htr using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
t : (x : X) → Set X
htx : ∀ (x : X) (_ : x ∈ s), t x ∈ 𝓝[s] x
htr : ∀ (x : X) (_ : x ∈ s), dimH (t x) ≤ r
⊢ dimH s ≤ r
have rcases : ∀ (S : Set X) (hSs : S ⊆ s) (hSc : S.Countable) (hSU : s ⊆ ⋃ x ∈ S, t x), dimH s ≤ r
Tactic: rcases countable_cover_nhdsWithin htx with ⟨S, hSs, hSc, hSU⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
⊢ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets = dimH s
have refine_1 : ∀ x ∈ s, limsup dimH (𝓝[s] x).smallSets ≤ dimH s
Tactic: refine le_antisymm (iSup₂_le fun x _ => ?_) ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
refine_1 : ∀ x ∈ s, limsup dimH (𝓝[s] x).smallSets ≤ dimH s
⊢ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets = dimH s
have refine_2 : dimH s ≤ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets
Tactic: refine le_antisymm (iSup₂_le fun x _ => ?_) ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
x : X
h : x ∈ s
⊢ limsup dimH (𝓝[s] x).smallSets ≤ dimH s
have refine_1 : ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ dimH s
Tactic: refine limsup_le_of_le isCobounded_le_of_bot ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
⊢ dimH s ≤ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets
have refine_2 : ∀ (r : ℝ≥0∞) (hr : r < dimH s), r ≤ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets
Tactic: refine le_of_forall_lt_imp_le_of_dense fun r hr => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
⊢ r ≤ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets
have refine_2 : ∀ (x : X) (hxs : x ∈ s) (hxr : ∀ t ∈ 𝓝[s] x, r < dimH t), r ≤ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets
Tactic: rcases exists_mem_nhdsWithin_lt_dimH_of_lt_dimH hr with ⟨x, hxs, hxr⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : 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
have refine_2 : r ≤ limsup dimH (𝓝[s] x).smallSets
Tactic: refine le_iSup₂_of_le x hxs ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : 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
have refine_2 : r ≤ sInf {a : ℝ≥0∞ | ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ a}
Tactic: rw [limsup_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : 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 : ℝ≥0∞ | ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ a}
have refine_2 : ∀ (b : ℝ≥0∞) (hb : Membership.mem (γ := Set ℝ≥0∞) {a : ℝ≥0∞ | ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ a} b),
  r ≤ b
Tactic: refine le_sInf fun b hb => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : 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 : Membership.mem (γ := Set ℝ≥0∞) {a : ℝ≥0∞ | ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ a} b
⊢ r ≤ b
have refine_2 : ∀ (t : Set X) (htx : t ∈ 𝓝[s] x) (ht : ∀ t_1 ⊆ t, dimH t_1 ≤ b), r ≤ b
Tactic: rcases eventually_smallSets.1 hb with ⟨t, htx, ht⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
⊢ ⨆ (x : X), limsup dimH (𝓝[s] x).smallSets = dimH s
have refine_1 : ∀ (x : X), limsup dimH (𝓝[s] x).smallSets ≤ dimH s
Tactic: refine le_antisymm (iSup_le fun x => ?_) ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
refine_1 : ∀ (x : X), limsup dimH (𝓝[s] x).smallSets ≤ dimH s
⊢ ⨆ (x : X), limsup dimH (𝓝[s] x).smallSets = dimH s
have refine_2 : dimH s ≤ ⨆ (x : X), limsup dimH (𝓝[s] x).smallSets
Tactic: refine le_antisymm (iSup_le fun x => ?_) ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
x : X
⊢ limsup dimH (𝓝[s] x).smallSets ≤ dimH s
have refine_1 : ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ dimH s
Tactic: refine limsup_le_of_le isCobounded_le_of_bot ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
inst : EMetricSpace X
inst_1 : SecondCountableTopology X
s : Set X
⊢ dimH s ≤ ⨆ (x : X), limsup dimH (𝓝[s] x).smallSets
have refine_2 : LE.le (α := ℝ≥0∞) (⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets) (⨆ (x : X), limsup dimH (𝓝[s] x).smallSets)
Tactic: rw [← bsupr_limsup_dimH]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
⊢ dimH (f '' s) ≤ dimH s / (↑r : ℝ≥0∞)
have this : let this := borel X;
BorelSpace X
Tactic: borelize X Y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this :
  let this := borel X;
  BorelSpace X
⊢ dimH (f '' s) ≤ dimH s / (↑r : ℝ≥0∞)
have this₁ : let this := borel Y;
BorelSpace Y
Tactic: borelize X Y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : 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_1 : BorelSpace X
this_2 : MeasurableSpace Y := borel Y
this_3 : BorelSpace Y
⊢ dimH (f '' s) ≤ dimH s / (↑r : ℝ≥0∞)
have refine : ∀ (d : ℝ≥0) (hd : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  (↑d : ℝ≥0∞) ≤ dimH s / (↑r : ℝ≥0∞)
Tactic: refine dimH_le fun d hd => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : 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_1 : BorelSpace X
this_2 : MeasurableSpace Y := borel Y
this_3 : BorelSpace Y
d : ℝ≥0
hd : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (↑d : ℝ≥0∞) ≤ dimH s / (↑r : ℝ≥0∞)
have this : ((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) (f '' s) ≤
  HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ (↑d : ℝ)) (((μH[(↑r : ℝ) * (↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: have := h.hausdorffMeasure_image_le hr d.coe_nonneg
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this_1 : MeasurableSpace X := borel X
this_2 : BorelSpace X
this_3 : MeasurableSpace Y := borel Y
this_4 : BorelSpace Y
d : ℝ≥0
hd : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  ((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) (f '' s) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) ^ (↑d : ℝ))
      (((μH[(↑r : ℝ) * (↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (↑d : ℝ≥0∞) ≤ dimH s / (↑r : ℝ≥0∞)
have this₁ : HMul.hMul (β := ℝ≥0∞) (↑(C ^ (↑d : ℝ)) : ℝ≥0∞) (((μH[(↑r : ℝ) * (↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) =
  ∞
Tactic: rw [hd, ← ENNReal.coe_rpow_of_nonneg _ d.coe_nonneg, top_le_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this_1 : MeasurableSpace X := borel X
this_2 : BorelSpace X
this_3 : MeasurableSpace Y := borel Y
this_4 : BorelSpace Y
d : ℝ≥0
hd : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  HMul.hMul (β := ℝ≥0∞) (↑(C ^ (↑d : ℝ)) : ℝ≥0∞)
      (((μH[(↑r : ℝ) * (↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) =
    ∞
⊢ Eq (α := ℝ≥0∞) (((μH[(↑(r * d) : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have contrapose : ∀ (this : ¬Eq (α := ℝ≥0∞) (((μH[(↑(r * d) : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  ¬HMul.hMul (β := ℝ≥0∞) (↑(C ^ (↑d : ℝ)) : ℝ≥0∞)
        (((μH[(↑r : ℝ) * (↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) =
      ∞
Tactic: contrapose this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this_1 : MeasurableSpace X := borel X
this_2 : BorelSpace X
this_3 : MeasurableSpace Y := borel Y
this_4 : BorelSpace Y
d : ℝ≥0
hd : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  HMul.hMul (β := ℝ≥0∞) (↑(C ^ (↑d : ℝ)) : ℝ≥0∞)
      (((μH[(↑r : ℝ) * (↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) =
    ∞
⊢ (↑d : ℝ≥0∞) ≤ dimH s / (↑r : ℝ≥0∞)
have Hrd : Eq (α := ℝ≥0∞) (((μH[(↑(r * d) : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have Hrd : μH[(r * d : ℝ≥0)] s = ⊤ := by
    contrapose this
    finiteness
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this_1 : MeasurableSpace X := borel X
this_2 : BorelSpace X
this_3 : MeasurableSpace Y := borel Y
this_4 : BorelSpace Y
d : ℝ≥0
hd : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  HMul.hMul (β := ℝ≥0∞) (↑(C ^ (↑d : ℝ)) : ℝ≥0∞)
      (((μH[(↑r : ℝ) * (↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) =
    ∞
Hrd : Eq (α := ℝ≥0∞) (((μH[(↑(r * d) : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (↑d : ℝ≥0∞) ≤ dimH s / (↑r : ℝ≥0∞)
have rw : (↑(r * d) : ℝ≥0∞) ≤ dimH s
Tactic: rw [ENNReal.le_div_iff_mul_le, mul_comm, ← ENNReal.coe_mul]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this_1 : MeasurableSpace X := borel X
this_2 : BorelSpace X
this_3 : MeasurableSpace Y := borel Y
this_4 : BorelSpace Y
d : ℝ≥0
hd : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  HMul.hMul (β := ℝ≥0∞) (↑(C ^ (↑d : ℝ)) : ℝ≥0∞)
      (((μH[(↑r : ℝ) * (↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) =
    ∞
Hrd : Eq (α := ℝ≥0∞) (((μH[(↑(r * d) : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : (↑(r * d) : ℝ≥0∞) ≤ dimH s
⊢ (↑d : ℝ≥0∞) ≤ dimH s / (↑r : ℝ≥0∞)
have h0 : (↑r : ℝ≥0∞) ≠ 0 ∨ dimH s ≠ 0
Tactic: rw [ENNReal.le_div_iff_mul_le, mul_comm, ← ENNReal.coe_mul]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this_1 : MeasurableSpace X := borel X
this_2 : BorelSpace X
this_3 : MeasurableSpace Y := borel Y
this_4 : BorelSpace Y
d : ℝ≥0
hd : Eq (α := ℝ≥0∞) (((μH[(↑d : ℝ)] : Measure Y) : (a : Set Y) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  HMul.hMul (β := ℝ≥0∞) (↑(C ^ (↑d : ℝ)) : ℝ≥0∞)
      (((μH[(↑r : ℝ) * (↑d : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) =
    ∞
Hrd : Eq (α := ℝ≥0∞) (((μH[(↑(r * d) : ℝ)] : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : (↑(r * d) : ℝ≥0∞) ≤ dimH s
h0 : (↑r : ℝ≥0∞) ≠ 0 ∨ dimH s ≠ 0
⊢ (↑d : ℝ≥0∞) ≤ dimH s / (↑r : ℝ≥0∞)
have ht : (↑r : ℝ≥0∞) ≠ ∞ ∨ dimH s ≠ ∞
Tactic: rw [ENNReal.le_div_iff_mul_le, mul_comm, ← ENNReal.coe_mul]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
hf : ∀ x ∈ s, ∃ (C : ℝ≥0), ∃ t ∈ 𝓝[s] x, HolderOnWith C r f t
⊢ dimH (f '' s) ≤ dimH s / (↑r : ℝ≥0∞)
have choose! : ∀ (C : (x : X) → ℝ≥0) (t : (x : X) → Set X) (htn : ∀ x ∈ s, t x ∈ 𝓝[s] x) (hC : ∀ x ∈ s, HolderOnWith (C x) r f (t x)),
  dimH (f '' s) ≤ dimH s / (↑r : ℝ≥0∞)
Tactic: choose! C t htn hC using hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
C : (x : X) → ℝ≥0
t : (x : X) → Set X
htn : ∀ x ∈ s, t x ∈ 𝓝[s] x
hC : ∀ x ∈ s, HolderOnWith (C x) r f (t x)
⊢ dimH (f '' s) ≤ dimH s / (↑r : ℝ≥0∞)
have rcases : ∀ (u : Set X) (hus : u ⊆ s) (huc : u.Countable) (huU : s ⊆ ⋃ x ∈ u, t x), dimH (f '' s) ≤ dimH s / (↑r : ℝ≥0∞)
Tactic: rcases countable_cover_nhdsWithin htn with ⟨u, hus, huc, huU⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
C : (x : X) → ℝ≥0
t : (x : 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 : s ⊆ ⋃ x ∈ u, t x
⊢ dimH (f '' s) ≤ dimH s / (↑r : ℝ≥0∞)
have huU₁ : s ∩ ⋃ x ∈ u, t x = s
Tactic: replace huU := inter_eq_self_of_subset_left huU
Cleared hypotheses: huU
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (hypothesis)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
C : (x : X) → ℝ≥0
t : (x : 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 : s ∩ ⋃ x ∈ u, t x = s
⊢ dimH (f '' s) ≤ dimH s / (↑r : ℝ≥0∞)
have huU₁ : ⋃ i ∈ u, s ∩ t i = s
Tactic: rw [inter_iUnion₂] at huU
Cleared hypotheses: huU
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDimension (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
C : (x : X) → ℝ≥0
t : (x : 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 : ℝ≥0∞)
have rw : ⨆ i ∈ u, dimH (f '' (s ∩ t i)) ≤ (⨆ i ∈ u, dimH (s ∩ t i)) / (↑r : ℝ≥0∞)
Tactic: rw [← huU, image_iUnion₂, dimH_bUnion huc, dimH_bUnion huc]