awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K r : ℝ
hr :
  ∀ (x : α),
    ∀ t ≤ K,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (t * r)) ≤
        HMul.hMul (β := ℝ≥0∞)
          (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
                ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
                  ∀ (x_1 : α),
                    ∀ t ≤ K,
                      (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                        HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
                ⋯) :
            ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
x : α
h :
  HMul.hMul (β := ℝ≥0∞)
      (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
            ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
              ∀ (x_1 : α),
                ∀ t ≤ K,
                  (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                    HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
            ⋯) :
        ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall x (K * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
have h₁ : HMul.hMul (β := ℝ≥0∞)
    (↑(Classical.choose (p := fun (x : ℝ≥0) ↦
          ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
            ∀ (x_1 : α),
              ∀ t ≤ K,
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
          sorry) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ≤
  HMul.hMul (β := ℝ≥0∞)
    (↑(max
          (Classical.choose (p := fun (x : ℝ≥0) ↦
            ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
              ∀ (x_1 : α),
                ∀ t ≤ K,
                  (μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 (t * ε)) ≤
                    HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x_1 ε) : ℝ≥0∞))
            sorry)
          1) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
Tactic: grw [hr x K le_rfl, scalingConstantOf, ← le_max_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Doubling (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
K : ℝ
hK : 0 < K
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0,
    ∀ (x : α),
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x r) ≤
        HMul.hMul (β := ℝ≥0∞) (↑(scalingConstantOf μ K⁻¹) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (K * r)) : ℝ≥0∞)
have h : ∀ (x : ℝ) (a : α), x = K⁻¹ * (K * x)
Tactic: convert! eventually_nhdsGT_zero_mul_left hK (eventually_measure_le_scaling_constant_mul μ K⁻¹)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ.everywherePosSubset s = s \ {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)}
have h : ∀ (x : α),
  x ∈ μ.everywherePosSubset s ↔
    x ∈ s \ {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)}
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ μ.everywherePosSubset s = s \ u
have refine : IsOpen[inst] {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)}
Tactic: refine ⟨{x | ∃ n ∈ 𝓝[s] x, μ n = 0}, ?_, by ext x; simp [everywherePosSubset, pos_iff_ne_zero]⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ IsOpen[inst] {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)}
have rw : ∀ (x : α),
  Membership.mem (γ := Set α) {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} x →
    {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} ∈ 𝓝 x
Tactic: rw [isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
x : α
⊢ Membership.mem (γ := Set α) {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} x →
    {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} ∈ 𝓝 x
have this : ∀ (n : Set α) (ns : n ∈ 𝓝[s] x) (hx : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)),
  {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} ∈ 𝓝 x
Tactic: ⟨n, ns, hx⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} ∈ 𝓝 x
have rcases : ∀ (v : Set α) (vx : v ∈ 𝓝 x) (hv : v ∩ s ⊆ n),
  {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} ∈ 𝓝 x
Tactic: rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.1 ns with ⟨v, vx, hv⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
⊢ {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} ∈ 𝓝 x
have rcases : ∀ (w : Set α) (wv : w ⊆ v) (w_open : IsOpen[inst] w) (xw : x ∈ w),
  {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} ∈ 𝓝 x
Tactic: rcases mem_nhds_iff.1 vx with ⟨w, wv, w_open, xw⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen[inst] w
xw : x ∈ w
y : α
yw : y ∈ w
⊢ Membership.mem (γ := Set α) {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} y
have refine : s ∩ w ⊆ n
Tactic: refine ⟨s ∩ w, inter_mem_nhdsWithin _ (w_open.mem_nhds yw), measure_mono_null ?_ hx⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen[inst] w
xw : x ∈ w
y : α
yw : y ∈ w
⊢ s ∩ w ⊆ n
have rw : w ∩ s ⊆ n
Tactic: rw [inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen[inst] w
xw : x ∈ w
⊢ {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} ∈ 𝓝 x
have A : w ⊆ {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)}
Tactic: have A : w ⊆ {x | ∃ n ∈ 𝓝[s] x, μ n = 0} := by
    intro y yw
    refine ⟨s ∩ w, inter_mem_nhdsWithin _ (w_open.mem_nhds yw), measure_mono_null ?_ hx⟩
    rw [inter_comm]
    exact (inter_subset_inter_left _ wv).trans hv
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen[inst] w
xw : x ∈ w
A : w ⊆ {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)}
⊢ {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} ∈ 𝓝 x
have B : w ∈ 𝓝 x
Tactic: have B : w ∈ 𝓝 x := w_open.mem_nhds xw
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
hs : MeasurableSet s
⊢ MeasurableSet (μ.everywherePosSubset s)
have rcases : ∀ (u : Set α) (u_open : IsOpen[inst] u) (hu : μ.everywherePosSubset s = s \ u), MeasurableSet (μ.everywherePosSubset s)
Tactic: rcases exists_isOpen_everywherePosSubset_eq_diff μ s with ⟨u, u_open, hu⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
hs : MeasurableSet s
u : Set α
u_open : IsOpen[inst] u
hu : μ.everywherePosSubset s = s \ u
⊢ MeasurableSet (μ.everywherePosSubset s)
have rw : MeasurableSet (s \ u)
Tactic: rw [hu]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsClosed[inst] s
⊢ IsClosed[inst] (μ.everywherePosSubset s)
have rcases : ∀ (u : Set α) (u_open : IsOpen[inst] u) (hu : μ.everywherePosSubset s = s \ u), IsClosed[inst] (μ.everywherePosSubset s)
Tactic: rcases exists_isOpen_everywherePosSubset_eq_diff μ s with ⟨u, u_open, hu⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsClosed[inst] s
u : Set α
u_open : IsOpen[inst] u
hu : μ.everywherePosSubset s = s \ u
⊢ IsClosed[inst] (μ.everywherePosSubset s)
have rw : IsClosed[inst] (s \ u)
Tactic: rw [hu]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsCompact s
⊢ IsCompact (μ.everywherePosSubset s)
have rcases : ∀ (u : Set α) (u_open : IsOpen[inst] u) (hu : μ.everywherePosSubset s = s \ u), IsCompact (μ.everywherePosSubset s)
Tactic: rcases exists_isOpen_everywherePosSubset_eq_diff μ s with ⟨u, u_open, hu⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsCompact s
u : Set α
u_open : IsOpen[inst] u
hu : μ.everywherePosSubset s = s \ u
⊢ IsCompact (μ.everywherePosSubset s)
have rw : IsCompact (s \ u)
Tactic: rw [hu]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s k : Set α
hk : IsCompact k
h'k : k ⊆ s \ μ.everywherePosSubset s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) k : ℝ≥0∞) (0 : ℝ≥0∞)
have he : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply hk.induction_on (p := fun t ↦ μ t = 0)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s k : Set α
hk : IsCompact k
h'k : k ⊆ s \ μ.everywherePosSubset s
he : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) k : ℝ≥0∞) (0 : ℝ≥0∞)
have hmono : ∀ ⦃s t : Set α⦄,
  s ⊆ t →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply hk.induction_on (p := fun t ↦ μ t = 0)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s k : Set α
hk : IsCompact k
h'k : k ⊆ s \ μ.everywherePosSubset s
he : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (0 : ℝ≥0∞)
hmono :
  ∀ ⦃s t : Set α⦄,
    s ⊆ t →
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) k : ℝ≥0∞) (0 : ℝ≥0∞)
have hunion : ∀ ⦃s t : Set α⦄,
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply hk.induction_on (p := fun t ↦ μ t = 0)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s k : Set α
hk : IsCompact k
h'k : k ⊆ s \ μ.everywherePosSubset s
he : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (0 : ℝ≥0∞)
hmono :
  ∀ ⦃s t : Set α⦄,
    s ⊆ t →
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hunion :
  ∀ ⦃s t : Set α⦄,
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) k : ℝ≥0∞) (0 : ℝ≥0∞)
have hnhds : ∀ x ∈ k, ∃ t ∈ 𝓝[k] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply hk.induction_on (p := fun t ↦ μ t = 0)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s k : Set α
hk : IsCompact k
h'k : k ⊆ s \ μ.everywherePosSubset s
x : α
hx : x ∈ k
⊢ ∃ t ∈ 𝓝[k] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
have hnhds : ∀ (u : Set α) (ux : u ∈ 𝓝[s] x) (hu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)),
  ∃ t ∈ 𝓝[k] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: obtain ⟨u, ux, hu⟩ : ∃ u ∈ 𝓝[s] x, μ u = 0 := by
      simpa [everywherePosSubset, (h'k hx).1] using (h'k hx).2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegular
hs : MeasurableSet s
⊢ μ.everywherePosSubset s =ᶠ[ae μ] s
have simp : ∀ (i : Set α) (i_1 : i ⊆ s \ μ.everywherePosSubset s) (i_2 : IsCompact i),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [ae_eq_set, diff_eq_empty.mpr (everywherePosSubset_subset μ s), measure_empty,
    true_and, (hs.diff hs.everywherePosSubset).measure_eq_iSup_isCompact, ENNReal.iSup_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.everywherePosSubset s =ᶠ[ae μ] s
have A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ μ.everywherePosSubset s) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have A : μ (s \ μ.everywherePosSubset s) ≠ ∞ :=
    ((measure_mono diff_subset).trans_lt h's.lt_top).ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ μ.everywherePosSubset s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.everywherePosSubset s =ᶠ[ae μ] s
have simp : ∀ (i : Set α) (i_1 : i ⊆ s \ μ.everywherePosSubset s) (i_2 : IsCompact i),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [ae_eq_set, diff_eq_empty.mpr (everywherePosSubset_subset μ s), measure_empty,
    true_and, (hs.diff hs.everywherePosSubset).measure_eq_iSup_isCompact_of_ne_top A,
    ENNReal.iSup_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegular
hs : MeasurableSet s
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)
have rcases : ∀ (u : Set α) (u_mem : u ∈ 𝓝 x) (hu : u ∩ μ.everywherePosSubset s ⊆ n),
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)
Tactic: rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.1 hn with ⟨u, u_mem, hu⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegular
hs : MeasurableSet s
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
⊢ u ∩ s ∈ 𝓝[s] x
have rw : s ∩ u ∈ 𝓝[s] x
Tactic: rw [inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegular
hs : MeasurableSet s
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
have this : u ∩ s ∈ 𝓝[s] x
Tactic: have : u ∩ s ∈ 𝓝[s] x := by rw [inter_comm]; exact inter_mem_nhdsWithin s u_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegular
hs : MeasurableSet s
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)
have A : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
Tactic: have A : 0 < μ (u ∩ s) := by
    have : u ∩ s ∈ 𝓝[s] x := by rw [inter_comm]; exact inter_mem_nhdsWithin s u_mem
    exact hx.2 _ this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegular
hs : MeasurableSet s
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
A : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)
have B : u ∩ μ.everywherePosSubset s =ᶠ[ae μ] u ∩ s
Tactic: have B : (u ∩ μ.everywherePosSubset s : Set α) =ᵐ[μ] (u ∩ s : Set α) :=
    ae_eq_set_inter (ae_eq_refl _) (everywherePosSubset_ae_eq hs)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegular
hs : MeasurableSet s
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
A : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
B : u ∩ μ.everywherePosSubset s =ᶠ[ae μ] u ∩ s
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)
have A₁ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ μ.everywherePosSubset s) : ℝ≥0∞)
Tactic: rw [← B.measure_eq] at A
Cleared hypotheses: A, B
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)
have rcases : ∀ (u : Set α) (u_mem : u ∈ 𝓝 x) (hu : u ∩ μ.everywherePosSubset s ⊆ n),
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)
Tactic: rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.1 hn with ⟨u, u_mem, hu⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
⊢ u ∩ s ∈ 𝓝[s] x
have rw : s ∩ u ∈ 𝓝[s] x
Tactic: rw [inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
have this : u ∩ s ∈ 𝓝[s] x
Tactic: have : u ∩ s ∈ 𝓝[s] x := by rw [inter_comm]; exact inter_mem_nhdsWithin s u_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)
have A : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
Tactic: have A : 0 < μ (u ∩ s) := by
    have : u ∩ s ∈ 𝓝[s] x := by rw [inter_comm]; exact inter_mem_nhdsWithin s u_mem
    exact hx.2 _ this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
A : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)
have B : u ∩ μ.everywherePosSubset s =ᶠ[ae μ] u ∩ s
Tactic: have B : (u ∩ μ.everywherePosSubset s : Set α) =ᵐ[μ] (u ∩ s : Set α) :=
    ae_eq_set_inter (ae_eq_refl _) (everywherePosSubset_ae_eq_of_measure_ne_top hs h's)