awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun (i : ℕ) ↦ ⋃ (j : ℕ), ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) W : ℝ≥0∞) (0 : ℝ≥0∞)
d : α
hd' :
  ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι) ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (W ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set α) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : (j : ℕ) → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (M * r₁ (f j))
B : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (r₁ (f j))
h₁ : ∀ (j : ℕ), b j ⊆ B j
h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j
h₃ : ∀ᶠ (j : ℕ) in atTop, Disjoint (b j) (W ∩ B j)
h₄ :
  ∀ᶠ (j : ℕ) in atTop,
    (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
j : ℕ
hj₀ :
  Disjoint (b j) (W ∩ B j) ∧
    (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
inl :
  ∀ (hB : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≤
      (↑(1 - C⁻¹) : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≤
    (↑(1 - C⁻¹) : ℝ≥0∞)
have inr : ∀ (hB : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≤
    (↑(1 - C⁻¹) : ℝ≥0∞)
Tactic: rcases eq_or_ne (μ (B j)) ∞ with (hB | hB)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun (i : ℕ) ↦ ⋃ (j : ℕ), ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) W : ℝ≥0∞) (0 : ℝ≥0∞)
d : α
hd' :
  ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι) ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (W ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set α) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : (j : ℕ) → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (M * r₁ (f j))
B : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (r₁ (f j))
h₁ : ∀ (j : ℕ), b j ⊆ B j
h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j
h₃ : ∀ᶠ (j : ℕ) in atTop, Disjoint (b j) (W ∩ B j)
h₄ :
  ∀ᶠ (j : ℕ) in atTop,
    (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
j : ℕ
hj₀ :
  Disjoint (b j) (W ∩ B j) ∧
    (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
hB : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≤
    (↑(1 - C⁻¹) : ℝ≥0∞)
have inr : (μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑(1 - C⁻¹) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞)
Tactic: apply ENNReal.div_le_of_le_mul
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun (i : ℕ) ↦ ⋃ (j : ℕ), ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) W : ℝ≥0∞) (0 : ℝ≥0∞)
d : α
hd' :
  ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι) ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (W ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set α) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : (j : ℕ) → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (M * r₁ (f j))
B : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (r₁ (f j))
h₁ : ∀ (j : ℕ), b j ⊆ B j
h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j
h₃ : ∀ᶠ (j : ℕ) in atTop, Disjoint (b j) (W ∩ B j)
h₄ :
  ∀ᶠ (j : ℕ) in atTop,
    (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
j : ℕ
hj₀ :
  Disjoint (b j) (W ∩ B j) ∧
    (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
hB : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑(1 - C⁻¹) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞)
have inr : (μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) ≤
  HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞)
    (HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞))
Tactic: rw [ENNReal.coe_sub, ENNReal.coe_one, ENNReal.sub_mul fun _ _ => hB, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun (i : ℕ) ↦ ⋃ (j : ℕ), ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) W : ℝ≥0∞) (0 : ℝ≥0∞)
d : α
hd' :
  ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι) ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (W ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set α) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : (j : ℕ) → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (M * r₁ (f j))
B : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (r₁ (f j))
h₁ : ∀ (j : ℕ), b j ⊆ B j
h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j
h₃ : ∀ᶠ (j : ℕ) in atTop, Disjoint (b j) (W ∩ B j)
h₄ :
  ∀ᶠ (j : ℕ) in atTop,
    (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
j : ℕ
hj₀ :
  Disjoint (b j) (W ∩ B j) ∧
    (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
hB : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) ≤
    HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞))
have hB₁ : HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≠ ∞
Tactic: replace hB : ↑C⁻¹ * μ (B j) ≠ ∞ := by finiteness
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun (i : ℕ) ↦ ⋃ (j : ℕ), ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) W : ℝ≥0∞) (0 : ℝ≥0∞)
d : α
hd' :
  ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι) ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (W ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set α) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : (j : ℕ) → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (M * r₁ (f j))
B : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (r₁ (f j))
h₁ : ∀ (j : ℕ), b j ⊆ B j
h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j
h₃ : ∀ᶠ (j : ℕ) in atTop, Disjoint (b j) (W ∩ B j)
h₄ :
  ∀ᶠ (j : ℕ) in atTop,
    (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
j : ℕ
hj₀ :
  Disjoint (b j) (W ∩ B j) ∧
    (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
hB : HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≠ ∞
⊢ (μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) ≤
    HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞))
have hj₁ : Disjoint (b j) (W ∩ B j)
Tactic: obtain ⟨hj₁ : Disjoint (b j) (W ∩ B j), hj₂ : μ (B j) ≤ C * μ (b j)⟩ := hj₀
Cleared hypotheses: hj₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun (i : ℕ) ↦ ⋃ (j : ℕ), ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) W : ℝ≥0∞) (0 : ℝ≥0∞)
d : α
hd' :
  ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι) ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (W ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set α) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : (j : ℕ) → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (M * r₁ (f j))
B : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (r₁ (f j))
h₁ : ∀ (j : ℕ), b j ⊆ B j
h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j
h₃ : ∀ᶠ (j : ℕ) in atTop, Disjoint (b j) (W ∩ B j)
h₄ :
  ∀ᶠ (j : ℕ) in atTop,
    (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
j : ℕ
hj₀ :
  Disjoint (b j) (W ∩ B j) ∧
    (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
hB : HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≠ ∞
hj₁ : Disjoint (b j) (W ∩ B j)
⊢ (μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) ≤
    HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞))
have hj₂ : (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
Tactic: obtain ⟨hj₁ : Disjoint (b j) (W ∩ B j), hj₂ : μ (B j) ≤ C * μ (b j)⟩ := hj₀
Cleared hypotheses: hj₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun (i : ℕ) ↦ ⋃ (j : ℕ), ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) W : ℝ≥0∞) (0 : ℝ≥0∞)
d : α
hd' :
  ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι) ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (W ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set α) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : (j : ℕ) → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (M * r₁ (f j))
B : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (r₁ (f j))
h₁ : ∀ (j : ℕ), b j ⊆ B j
h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j
h₃ : ∀ᶠ (j : ℕ) in atTop, Disjoint (b j) (W ∩ B j)
h₄ :
  ∀ᶠ (j : ℕ) in atTop,
    (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
j : ℕ
hB : HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≠ ∞
hj₁ : Disjoint (b j) (W ∩ B j)
hj₂ : (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≤ (μ : (a : Set α) → ℝ≥0∞) (b j)
have rw : HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) (↑C : ℝ≥0∞) ≤ (μ : (a : Set α) → ℝ≥0∞) (b j)
Tactic: rw [ENNReal.coe_inv hC, ← ENNReal.div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun (i : ℕ) ↦ ⋃ (j : ℕ), ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) W : ℝ≥0∞) (0 : ℝ≥0∞)
d : α
hd' :
  ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι) ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (W ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set α) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : (j : ℕ) → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (M * r₁ (f j))
B : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (r₁ (f j))
h₁ : ∀ (j : ℕ), b j ⊆ B j
h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j
h₃ : ∀ᶠ (j : ℕ) in atTop, Disjoint (b j) (W ∩ B j)
h₄ :
  ∀ᶠ (j : ℕ) in atTop,
    (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
j : ℕ
hB : HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≠ ∞
hj₁ : Disjoint (b j) (W ∩ B j)
hj₂ : (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) ≤
    HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞))
have hj₃ : HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≤ (μ : (a : Set α) → ℝ≥0∞) (b j)
Tactic: replace hj₂ : ↑C⁻¹ * μ (B j) ≤ μ (b j) := by
    rw [ENNReal.coe_inv hC, ← ENNReal.div_eq_inv_mul]
    exact ENNReal.div_le_of_le_mul' hj₂
Cleared hypotheses: hj₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun (i : ℕ) ↦ ⋃ (j : ℕ), ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) W : ℝ≥0∞) (0 : ℝ≥0∞)
d : α
hd' :
  ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι) ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (W ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set α) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : (j : ℕ) → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (M * r₁ (f j))
B : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (r₁ (f j))
h₁ : ∀ (j : ℕ), b j ⊆ B j
h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j
h₃ : ∀ᶠ (j : ℕ) in atTop, Disjoint (b j) (W ∩ B j)
h₄ :
  ∀ᶠ (j : ℕ) in atTop,
    (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
j : ℕ
hB : HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≠ ∞
hj₁ : Disjoint (b j) (W ∩ B j)
hj₂ : HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≤ (μ : (a : Set α) → ℝ≥0∞) (b j)
⊢ HAdd.hAdd (β := ℝ≥0∞) (HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) : ℝ≥0∞) ≤
    (μ : (a : Set α) → ℝ≥0∞) (B j)
have grw : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) : ℝ≥0∞) ≤
  (μ : (a : Set α) → ℝ≥0∞) (B j)
Tactic: grw [hj₂]