awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set α), p K ∧ (μ : (a : Set α) → ℝ≥0∞) Kᶜ < ε
A : Set α
hA : q A
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
K : Set α
hK : p K
hK_subset : K ⊆ A
h_lt : (μ : (a : Set α) → ℝ≥0∞) (A \ K) < HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) r
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) <
    HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) r

Tactic:
have h_lt' : μ A - μ K < μ A - r := le_measure_diff.trans_lt h_lt
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set α), p K ∧ (μ : (a : Set α) → ℝ≥0∞) Kᶜ < ε
A : Set α
hA : q A
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
K : Set α
hK : p K
hK_subset : K ⊆ A
h_lt : (μ : (a : Set α) → ℝ≥0∞) (A \ K) < HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) r
h_lt' :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) <
    HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) r
⊢ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
lt_of_tsub_lt_tsub_left h_lt'

Premises used: lt_of_tsub_lt_tsub_left
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set α), p K ∧ (μ : (a : Set α) → ℝ≥0∞) Kᶜ < ε
A : Set α
hA : q A
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
K : Set α
hK : p K
hK_subset : K ⊆ A
h_lt : (μ : (a : Set α) → ℝ≥0∞) (A \ K) < HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) r
h_lt' :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) <
    HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) r
⊢ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
exact lt_of_tsub_lt_tsub_left h_lt'

Premises used: lt_of_tsub_lt_tsub_left
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set α), IsCompact (closure K) ∧ (μ : (a : Set α) → ℝ≥0∞) Kᶜ < ε
⊢ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed

Tactic:
innerRegularWRT_of_exists_compl_lt (fun s t hs ht ↦ ?_) hμ

Premises used: MeasureTheory.innerRegularWRT_of_exists_compl_lt
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set α), IsCompact (closure K) ∧ (μ : (a : Set α) → ℝ≥0∞) Kᶜ < ε
refine : ∀ (s t : Set α) (hs : (IsCompact ∘ closure) s) (ht : IsClosed t), (IsCompact ∘ closure) (s ∩ t)
⊢ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed

Tactic:
refine innerRegularWRT_of_exists_compl_lt (fun s t hs ht ↦ ?_) hμ

Premises used: MeasureTheory.innerRegularWRT_of_exists_compl_lt
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set α), IsCompact (closure K) ∧ (μ : (a : Set α) → ℝ≥0∞) Kᶜ < ε
s t : Set α
hs : (IsCompact ∘ closure) s
ht : IsClosed t
⊢ IsCompact (closure s ∩ t)

Tactic:
have : IsCompact (closure s ∩ t) := hs.inter_right ht
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set α), IsCompact (closure K) ∧ (μ : (a : Set α) → ℝ≥0∞) Kᶜ < ε
s t : Set α
hs : (IsCompact ∘ closure) s
ht : IsClosed t
this : IsCompact (closure s ∩ t)
⊢ (IsCompact ∘ closure) (s ∩ t)

Tactic:
this.of_isClosed_subset isClosed_closure ?_

Premises used: IsCompact.of_isClosed_subset, isClosed_closure, IsCompact
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set α), IsCompact (closure K) ∧ (μ : (a : Set α) → ℝ≥0∞) Kᶜ < ε
s t : Set α
hs : (IsCompact ∘ closure) s
ht : IsClosed t
this : IsCompact (closure s ∩ t)
refine : closure (s ∩ t) ⊆ closure s ∩ t
⊢ (IsCompact ∘ closure) (s ∩ t)

Tactic:
refine this.of_isClosed_subset isClosed_closure ?_

Premises used: IsCompact.of_isClosed_subset, isClosed_closure
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set α), IsCompact (closure K) ∧ (μ : (a : Set α) → ℝ≥0∞) Kᶜ < ε
s t : Set α
hs : (IsCompact ∘ closure) s
ht : IsClosed t
this : IsCompact (closure s ∩ t)
⊢ closure (s ∩ t) ⊆ closure s ∩ t

Tactic:
(closure_inter_subset_inter_closure _ _).trans_eq ?_

Premises used: LE.le.trans_eq, closure_inter_subset_inter_closure
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set α), IsCompact (closure K) ∧ (μ : (a : Set α) → ℝ≥0∞) Kᶜ < ε
s t : Set α
hs : (IsCompact ∘ closure) s
ht : IsClosed t
this : IsCompact (closure s ∩ t)
refine : closure s ∩ closure t = closure s ∩ t
⊢ closure (s ∩ t) ⊆ closure s ∩ t

Tactic:
refine (closure_inter_subset_inter_closure _ _).trans_eq ?_

Premises used: LE.le.trans_eq, closure_inter_subset_inter_closure
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set α), IsCompact (closure K) ∧ (μ : (a : Set α) → ℝ≥0∞) Kᶜ < ε
s t : Set α
hs : (IsCompact ∘ closure) s
ht : IsClosed t
this : IsCompact (closure s ∩ t)
rw rw₁ : closure s ∩ t = closure s ∩ t
⊢ closure s ∩ closure t = closure s ∩ t

Tactic:
rw [IsClosed.closure_eq ht]

Premises used: IsClosed.closure_eq
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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 α
cases : IsEmpty α → ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
cases₁ : Nonempty α → ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
⊢ ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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 α
⊢ IsCompact.{u_1} (X := α) (closure ∅)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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 α
refine : (P : (a : Set α) → ℝ≥0∞) ∅ᶜ < ε
⊢ ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε

Tactic:
refine ⟨∅, by simp, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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 α
rwa : (P : (a : Set α) → ℝ≥0∞) ∅ < ε
rwa₁ rwa₂ rwa₃ rwa₄ : 0 < ε
⊢ (P : (a : Set α) → ℝ≥0∞) ∅ᶜ < ε

Tactic:
rwa [Set.eq_empty_of_isEmpty ∅ᶜ, measure_empty]

Premises used: Compl.compl, MeasureTheory.measure_empty, EmptyCollection.emptyCollection, Set.eq_empty_of_isEmpty
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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 α
⊢ ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε

Tactic:
case inl =>
    refine ⟨∅, by simp, ?_⟩
    rwa [Set.eq_empty_of_isEmpty ∅ᶜ, measure_empty]

Premises used: Compl.compl, MeasureTheory.measure_empty, EmptyCollection.emptyCollection, Set.eq_empty_of_isEmpty
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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 α
⊢ DenseRange seq

Tactic:
have hseq_dense : DenseRange seq := TopologicalSpace.denseRange_denseSeq α
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
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ᶜ < ε
⊢ ∃ (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

Premises used: Filter.HasBasis.exists_antitone_subbasis, uniformity_hasBasis_open_symmetric
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
⊢ ∀ (i : ℕ), t i ∈ 𝓤 α

Tactic:
choose htu hto _ using ht
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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 ∈ 𝓤 α
⊢ ∀ (i : ℕ), IsOpen (t i)

Tactic:
choose htu hto _ using ht
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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)
⊢ ∀ (i : ℕ), (t i).IsSymm

Tactic:
choose htu hto _ using ht
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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)
⊢ ∀ (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)
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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')ᶜ) < ε

Tactic:
exists_measure_iInter_lt (fun m ↦ ?_) hε ⟨0, measure_ne_top P _⟩ ?_

Premises used: MeasureTheory.measure_ne_top, Exists.intro, OfNat.ofNat, MeasureTheory.exists_measure_iInter_lt
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
refine_2 : Eq.{u_1 + 1} (α := Set α) (⋂ (n_1 : ℕ), (f n n_1)ᶜ) ∅
⊢ ∃ (m : ℕ), (P : (a : Set α) → ℝ≥0∞) (⋂ (m' : ℕ), ⋂ (_ : m' ≤ m), (f n m')ᶜ) < ε

Tactic:
refine exists_measure_iInter_lt (fun m ↦ ?_) hε ⟨0, measure_ne_top P _⟩ ?_

Premises used: MeasureTheory.measure_ne_top, Exists.intro, OfNat.ofNat, MeasureTheory.exists_measure_iInter_lt
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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 : ℕ
⊢ NullMeasurableSet (f n m)ᶜ P

Tactic:
(measurable_prodMk_left (hto n).measurableSet).compl.nullMeasurableSet

Premises used: Set.Mem, MeasurableSet.nullMeasurableSet, setOf, IsOpen.measurableSet, MeasurableSet.compl, UniformSpace.ball, measurable_prodMk_left
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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 : ℕ
⊢ NullMeasurableSet (f n m)ᶜ P

Tactic:
exact (measurable_prodMk_left (hto n).measurableSet).compl.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, IsOpen.measurableSet, MeasurableSet.compl, measurable_prodMk_left
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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ᶜ ∅
refine_2₂ refine_2₃ : Eq.{u_1 + 1} (α := Set α) ∅ ∅
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (n_1 : ℕ), (f n n_1)ᶜ) ∅

Tactic:
rw [← compl_iUnion, h_univ, compl_univ]

Premises used: Set.compl_univ, Set.compl_iUnion
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
⊢ ∀ (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]
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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')ᶜ) < ε
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ᶜ < ε
⊢ ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε

Tactic:
choose! s' s'bound using h3
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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')ᶜ) < ε
rcases :
  ∀ (δ : ℕ → ℝ≥0∞) (hδ1 : ∀ (i : ℕ), 0 < δ i) (hδ2 : ∑' (i : ℕ), δ i < ε),
    ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
⊢ ∃ (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⟩

Premises used: ENNReal.exists_pos_sum_of_countable', ne_of_gt, Nat
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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ᶜ < ε

Tactic:
⟨interUnionBalls seq u t, isCompact_closure_interUnionBalls h_basis.toHasBasis seq u, ?_⟩

Premises used: isCompact_closure_interUnionBalls, Filter.HasAntitoneBasis.toHasBasis, interUnionBalls, And.intro, Exists.intro