awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : IsEmpty α
⊢ (P : (a : Set α) → ℝ≥0∞) ∅ᶜ < ε
have rwa : (P : (a : Set α) → ℝ≥0∞) ∅ < ε
Tactic: rwa [Set.eq_empty_of_isEmpty ∅ᶜ, measure_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : Nonempty α
seq : ℕ → α := denseSeq α
⊢ ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
have hseq_dense : DenseRange seq
Tactic: have hseq_dense : DenseRange seq := TopologicalSpace.denseRange_denseSeq α
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
⊢ ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
have obtain : ∀ (t : ℕ → SetRel α α) (ht : ∀ (i : ℕ), t i ∈ 𝓤 α ∧ IsOpen (t i) ∧ (t i).IsSymm) (h_basis : (𝓤 α).HasAntitoneBasis t),
  ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
Tactic: obtain ⟨t : ℕ → SetRel α α,
        ht : ∀ i, t i ∈ 𝓤 α ∧ IsOpen (t i) ∧ (t i).IsSymm,
        h_basis : (uniformity α).HasAntitoneBasis t⟩ :=
      (@uniformity_hasBasis_open_symmetric α _).exists_antitone_subbasis
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
ht : ∀ (i : ℕ), t i ∈ 𝓤 α ∧ IsOpen (t i) ∧ (t i).IsSymm
h_basis : (𝓤 α).HasAntitoneBasis t
⊢ ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
have htu : ∀ (i : ℕ), t i ∈ 𝓤 α
Tactic: choose htu hto _ using ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
ht : ∀ (i : ℕ), t i ∈ 𝓤 α ∧ IsOpen (t i) ∧ (t i).IsSymm
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
⊢ ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
have hto : ∀ (i : ℕ), IsOpen (t i)
Tactic: choose htu hto _ using ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
ht : ∀ (i : ℕ), t i ∈ 𝓤 α ∧ IsOpen (t i) ∧ (t i).IsSymm
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
⊢ ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
have a : ∀ (i : ℕ), (t i).IsSymm
Tactic: choose htu hto _ using ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
h_1 : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ UniformSpace.ball (seq m) (t n)
⊢ ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
have h_univ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := Set α) (⋃ (m : ℕ), f n m) univ
Tactic: have h_univ n : (⋃ m, f n m) = univ := hseq_dense.iUnion_uniformity_ball (htu n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε_1 : ℝ≥0∞
hε_1 : 0 < ε_1
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
h_1 : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := Set α) (⋃ (m : ℕ), f n m) univ
n : ℕ
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ (m : ℕ), (P : (a : Set α) → ℝ≥0∞) (⋂ (m' : ℕ), ⋂ (_ : m' ≤ m), (f n m')ᶜ) < ε
have refine_1 : ∀ (m : ℕ), NullMeasurableSet (f n m)ᶜ P
Tactic: refine exists_measure_iInter_lt (fun m ↦ ?_) hε ⟨0, measure_ne_top P _⟩ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε_1 : ℝ≥0∞
hε_1 : 0 < ε_1
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
h_1 : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := Set α) (⋃ (m : ℕ), f n m) univ
n : ℕ
ε : ℝ≥0∞
hε : 0 < ε
refine_1 : ∀ (m : ℕ), NullMeasurableSet (f n m)ᶜ P
⊢ ∃ (m : ℕ), (P : (a : Set α) → ℝ≥0∞) (⋂ (m' : ℕ), ⋂ (_ : m' ≤ m), (f n m')ᶜ) < ε
have refine_2 : Eq.{u_1 + 1} (α := Set α) (⋂ (n_1 : ℕ), (f n n_1)ᶜ) ∅
Tactic: refine exists_measure_iInter_lt (fun m ↦ ?_) hε ⟨0, measure_ne_top P _⟩ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε_1 : ℝ≥0∞
hε_1 : 0 < ε_1
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
h_1 : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := Set α) (⋃ (m : ℕ), f n m) univ
n : ℕ
ε : ℝ≥0∞
hε : 0 < ε
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (n_1 : ℕ), (f n n_1)ᶜ) ∅
have refine_2 : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f n i)ᶜ ∅
Tactic: rw [← compl_iUnion, h_univ, compl_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε_1 : ℝ≥0∞
hε_1 : 0 < ε_1
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
h_1 : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := Set α) (⋃ (m : ℕ), f n m) univ
n : ℕ
ε : ℝ≥0∞
hε : 0 < ε
refine_2 : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f n i)ᶜ ∅
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (n_1 : ℕ), (f n n_1)ᶜ) ∅
have refine_2₁ : Eq.{u_1 + 1} (α := Set α) univᶜ ∅
Tactic: rw [← compl_iUnion, h_univ, compl_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε_1 : ℝ≥0∞
hε_1 : 0 < ε_1
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
h_1 : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := Set α) (⋃ (m : ℕ), f n m) univ
n : ℕ
ε : ℝ≥0∞
hε : 0 < ε
refine_2 : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), f n i)ᶜ ∅
refine_2₁ : Eq.{u_1 + 1} (α := Set α) univᶜ ∅
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (n_1 : ℕ), (f n n_1)ᶜ) ∅
have refine_2₂ : Eq.{u_1 + 1} (α := Set α) ∅ ∅
Tactic: rw [← compl_iUnion, h_univ, compl_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
h_1 : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := Set α) (⋃ (m : ℕ), f n m) univ
⊢ ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
have h3 : ∀ (n : ℕ) (ε : ℝ≥0∞) (hε : 0 < ε), ∃ (m : ℕ), (P : (a : Set α) → ℝ≥0∞) (⋂ (m' : ℕ), ⋂ (_ : m' ≤ m), (f n m')ᶜ) < ε
Tactic: have h3 n (ε : ℝ≥0∞) (hε : 0 < ε) : ∃ m, P (⋂ m' ≤ m, (f n m')ᶜ) < ε := by
      refine exists_measure_iInter_lt (fun m ↦ ?_) hε ⟨0, measure_ne_top P _⟩ ?_
      · exact (measurable_prodMk_left (hto n).measurableSet).compl.nullMeasurableSet
      · rw [← compl_iUnion, h_univ, compl_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
h_1 : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := Set α) (⋃ (m : ℕ), f n m) univ
h3 : ∀ (n : ℕ) (ε : ℝ≥0∞) (hε : 0 < ε), ∃ (m : ℕ), (P : (a : Set α) → ℝ≥0∞) (⋂ (m' : ℕ), ⋂ (_ : m' ≤ m), (f n m')ᶜ) < ε
⊢ ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
have choose! : ∀ (s' : (n : ℕ) → (ε : ℝ≥0∞) → ℕ)
  (s'bound :
    ∀ (n : ℕ) (ε : ℝ≥0∞) (hε : 0 < ε), (P : (a : Set α) → ℝ≥0∞) (⋂ (m' : ℕ), ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε),
  ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
Tactic: choose! s' s'bound using h3
Cleared hypotheses: h3
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
h_1 : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := Set α) (⋃ (m : ℕ), f n m) univ
s' : (n : ℕ) → (ε : ℝ≥0∞) → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞) (hε : 0 < ε), (P : (a : Set α) → ℝ≥0∞) (⋂ (m' : ℕ), ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
⊢ ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
have rcases : ∀ (δ : ℕ → ℝ≥0∞) (hδ1 : ∀ (i : ℕ), 0 < δ i) (hδ2 : ∑' (i : ℕ), δ i < ε),
  ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
Tactic: rcases ENNReal.exists_pos_sum_of_countable' (ne_of_gt hε) ℕ with ⟨δ, hδ1, hδ2⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
h_1 : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := Set α) (⋃ (m : ℕ), f n m) univ
s' : (n : ℕ) → (ε : ℝ≥0∞) → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞) (hε : 0 < ε), (P : (a : Set α) → ℝ≥0∞) (⋂ (m' : ℕ), ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
δ : ℕ → ℝ≥0∞
hδ1 : ∀ (i : ℕ), 0 < δ i
hδ2 : ∑' (i : ℕ), δ i < ε
u : ℕ → ℕ := fun (n : ℕ) ↦ s' n (δ n)
⊢ ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
have refine : (P : (a : Set α) → ℝ≥0∞) (interUnionBalls seq u t)ᶜ < ε
Tactic: refine ⟨interUnionBalls seq u t, isCompact_closure_interUnionBalls h_basis.toHasBasis seq u, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
h_1 : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := Set α) (⋃ (m : ℕ), f n m) univ
s' : (n : ℕ) → (ε : ℝ≥0∞) → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞) (hε : 0 < ε), (P : (a : Set α) → ℝ≥0∞) (⋂ (m' : ℕ), ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
δ : ℕ → ℝ≥0∞
hδ1 : ∀ (i : ℕ), 0 < δ i
hδ2 : ∑' (i : ℕ), δ i < ε
u : ℕ → ℕ := fun (n : ℕ) ↦ s' n (δ n)
⊢ (P : (a : Set α) → ℝ≥0∞) (interUnionBalls seq u t)ᶜ < ε
have rw : (P : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), (⋃ (m : ℕ), ⋃ (_ : m ≤ u i), UniformSpace.ball (seq m) (Prod.swap ⁻¹' t i))ᶜ) < ε
Tactic: rw [interUnionBalls, Set.compl_iInter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
h_1 : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := Set α) (⋃ (m : ℕ), f n m) univ
s' : (n : ℕ) → (ε : ℝ≥0∞) → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞) (hε : 0 < ε), (P : (a : Set α) → ℝ≥0∞) (⋂ (m' : ℕ), ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
δ : ℕ → ℝ≥0∞
hδ1 : ∀ (i : ℕ), 0 < δ i
hδ2 : ∑' (i : ℕ), δ i < ε
u : ℕ → ℕ := fun (n : ℕ) ↦ s' n (δ n)
⊢ (P : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), (⋃ (m : ℕ), ⋃ (_ : m ≤ u i), UniformSpace.ball (seq m) (Prod.swap ⁻¹' t i))ᶜ) < ε
have refine : LE.le (α := ℝ≥0∞)
  (∑' (i : ℕ), (P : (a : Set α) → ℝ≥0∞) (⋃ (m : ℕ), ⋃ (_ : m ≤ u i), UniformSpace.ball (seq m) (Prod.swap ⁻¹' t i))ᶜ)
  (∑' (i : ℕ), δ i)
Tactic: refine ((measure_iUnion_le _).trans ?_).trans_lt hδ2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
h_1 : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := Set α) (⋃ (m : ℕ), f n m) univ
s' : (n : ℕ) → (ε : ℝ≥0∞) → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞) (hε : 0 < ε), (P : (a : Set α) → ℝ≥0∞) (⋂ (m' : ℕ), ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
δ : ℕ → ℝ≥0∞
hδ1 : ∀ (i : ℕ), 0 < δ i
hδ2 : ∑' (i : ℕ), δ i < ε
u : ℕ → ℕ := fun (n : ℕ) ↦ s' n (δ n)
⊢ LE.le (α := ℝ≥0∞)
    (∑' (i : ℕ), (P : (a : Set α) → ℝ≥0∞) (⋃ (m : ℕ), ⋃ (_ : m ≤ u i), UniformSpace.ball (seq m) (Prod.swap ⁻¹' t i))ᶜ)
    (∑' (i : ℕ), δ i)
have refine : ∀ (n : ℕ), (P : (a : Set α) → ℝ≥0∞) (⋃ (m : ℕ), ⋃ (_ : m ≤ u n), UniformSpace.ball (seq m) (Prod.swap ⁻¹' t n))ᶜ ≤ δ n
Tactic: refine ENNReal.tsum_le_tsum (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
h_1 : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := Set α) (⋃ (m : ℕ), f n m) univ
s' : (n : ℕ) → (ε : ℝ≥0∞) → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞) (hε : 0 < ε), (P : (a : Set α) → ℝ≥0∞) (⋂ (m' : ℕ), ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
δ : ℕ → ℝ≥0∞
hδ1 : ∀ (i : ℕ), 0 < δ i
hδ2 : ∑' (i : ℕ), δ i < ε
u : ℕ → ℕ := fun (n : ℕ) ↦ s' n (δ n)
n_1 n : ℕ
⊢ Prod.swap ⁻¹' t n = t n
have h : ∀ (x : α × α), x ∈ Prod.swap ⁻¹' t n ↔ x ∈ t n
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
h_1 : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := Set α) (⋃ (m : ℕ), f n m) univ
s' : (n : ℕ) → (ε : ℝ≥0∞) → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞) (hε : 0 < ε), (P : (a : Set α) → ℝ≥0∞) (⋂ (m' : ℕ), ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
δ : ℕ → ℝ≥0∞
hδ1 : ∀ (i : ℕ), 0 < δ i
hδ2 : ∑' (i : ℕ), δ i < ε
u : ℕ → ℕ := fun (n : ℕ) ↦ s' n (δ n)
n : ℕ
⊢ (P : (a : Set α) → ℝ≥0∞) (⋃ (m : ℕ), ⋃ (_ : m ≤ u n), UniformSpace.ball (seq m) (Prod.swap ⁻¹' t n))ᶜ ≤ δ n
have h'' : ∀ (n : ℕ), Prod.swap ⁻¹' t n = t n
Tactic: have h'' n : Prod.swap ⁻¹' t n = t n := by ext; exact (t n).comm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
h_1 : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := Set α) (⋃ (m : ℕ), f n m) univ
s' : (n : ℕ) → (ε : ℝ≥0∞) → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞) (hε : 0 < ε), (P : (a : Set α) → ℝ≥0∞) (⋂ (m' : ℕ), ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
δ : ℕ → ℝ≥0∞
hδ1 : ∀ (i : ℕ), 0 < δ i
hδ2 : ∑' (i : ℕ), δ i < ε
u : ℕ → ℕ := fun (n : ℕ) ↦ s' n (δ n)
n : ℕ
h'' : ∀ (n : ℕ), Prod.swap ⁻¹' t n = t n
⊢ (P : (a : Set α) → ℝ≥0∞) (⋃ (m : ℕ), ⋃ (_ : m ≤ u n), UniformSpace.ball (seq m) (Prod.swap ⁻¹' t n))ᶜ ≤ δ n
have simp : (P : (a : Set α) → ℝ≥0∞) (⋂ (i : ℕ), ⋂ (_ : i ≤ u n), (UniformSpace.ball (seq i) (t n))ᶜ) ≤ δ n
Tactic: simp only [h'', compl_iUnion, ge_iff_le]