awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
refine : (P : (a : Set α) → ℝ≥0∞) (interUnionBalls seq u t)ᶜ < ε
⊢ ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε

Tactic:
refine ⟨interUnionBalls seq u t, isCompact_closure_interUnionBalls h_basis.toHasBasis seq u, ?_⟩
-- 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)
rw :
  (P : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), (⋃ (m : ℕ), ⋃ (_ : m ≤ u i), UniformSpace.ball (seq m) (Prod.swap ⁻¹' t i))ᶜ) < ε
⊢ (P : (a : Set α) → ℝ≥0∞) (interUnionBalls seq u t)ᶜ < ε

Tactic:
rw [interUnionBalls, Set.compl_iInter]

Premises used: Set.compl_iInter, interUnionBalls
-- 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)
⊢ (P : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), (⋃ (m : ℕ), ⋃ (_ : m ≤ u i), UniformSpace.ball (seq m) (Prod.swap ⁻¹' t i))ᶜ) < ε

Tactic:
((measure_iUnion_le _).trans ?_).trans_lt hδ2

Premises used: MeasureTheory.measure_iUnion_le, LE.le.trans, LE.le.trans_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
ε : ℝ≥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)
refine :
  LE.le (α := ℝ≥0∞)
    (∑' (i : ℕ), (P : (a : Set α) → ℝ≥0∞) (⋃ (m : ℕ), ⋃ (_ : m ≤ u i), UniformSpace.ball (seq m) (Prod.swap ⁻¹' t i))ᶜ)
    (∑' (i : ℕ), δ i)
⊢ (P : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), (⋃ (m : ℕ), ⋃ (_ : m ≤ u i), UniformSpace.ball (seq m) (Prod.swap ⁻¹' t i))ᶜ) < ε

Tactic:
refine ((measure_iUnion_le _).trans ?_).trans_lt hδ2

Premises used: MeasureTheory.measure_iUnion_le, LE.le.trans, LE.le.trans_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
ε : ℝ≥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)

Tactic:
ENNReal.tsum_le_tsum (fun n ↦ ?_)

Premises used: ENNReal.tsum_le_tsum
-- 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)
refine :
  ∀ (n : ℕ), (P : (a : Set α) → ℝ≥0∞) (⋃ (m : ℕ), ⋃ (_ : m ≤ u n), UniformSpace.ball (seq m) (Prod.swap ⁻¹' t n))ᶜ ≤ δ n
⊢ LE.le (α := ℝ≥0∞)
    (∑' (i : ℕ), (P : (a : Set α) → ℝ≥0∞) (⋃ (m : ℕ), ⋃ (_ : m ≤ u i), UniformSpace.ball (seq m) (Prod.swap ⁻¹' t i))ᶜ)
    (∑' (i : ℕ), δ i)

Tactic:
refine ENNReal.tsum_le_tsum (fun n ↦ ?_)

Premises used: ENNReal.tsum_le_tsum
-- 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_1 : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
h_2 : ∀ (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 : ℕ
h : ∀ (x : α × α), x ∈ Prod.swap ⁻¹' t n ↔ x ∈ t n
⊢ Prod.swap ⁻¹' t n = t n

Tactic:
ext
-- 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)
n_1 n : ℕ
x : α × α
⊢ x ∈ Prod.swap ⁻¹' t n ↔ x ∈ t n

Tactic:
(t n).comm

Premises used: Set.Mem, setOf, Set.preimage, SetRel.comm, Prod.swap
-- 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)
n_1 n : ℕ
x : α × α
⊢ x ∈ Prod.swap ⁻¹' t n ↔ x ∈ t n

Tactic:
exact (t n).comm

Premises used: SetRel.comm
-- 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)
n : ℕ
⊢ ∀ (n : ℕ), Prod.swap ⁻¹' t n = t n

Tactic:
have h'' n : Prod.swap ⁻¹' t n = t n := by ext; exact (t n).comm
-- 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)
n : ℕ
h'' : ∀ (n : ℕ), Prod.swap ⁻¹' t n = t n
simp : (P : (a : Set α) → ℝ≥0∞) (⋂ (i : ℕ), ⋂ (_ : i ≤ u n), (UniformSpace.ball (seq i) (t n))ᶜ) ≤ δ n
⊢ (P : (a : Set α) → ℝ≥0∞) (⋃ (m : ℕ), ⋃ (_ : m ≤ u n), UniformSpace.ball (seq m) (Prod.swap ⁻¹' t n))ᶜ ≤ δ n

Tactic:
simp only [h'', compl_iUnion, ge_iff_le]

Premises used: ge_iff_le, 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
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∞) (⋂ (i : ℕ), ⋂ (_ : i ≤ u n), (UniformSpace.ball (seq i) (t n))ᶜ) ≤ δ n

Tactic:
(s'bound n (δ n) (hδ1 n)).le

Premises used: Set.Mem, setOf, LT.lt.le
-- 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)
n : ℕ
h'' : ∀ (n : ℕ), Prod.swap ⁻¹' t n = t n
⊢ (P : (a : Set α) → ℝ≥0∞) (⋂ (i : ℕ), ⋂ (_ : i ≤ u n), (UniformSpace.ball (seq i) (t n))ᶜ) ≤ δ n

Tactic:
exact (s'bound n (δ n) (hδ1 n)).le

Premises used: LT.lt.le
-- 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 < ε
let let₁ let₂ : ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
let₃ :
  let u : ℕ → ℕ := fun (n : ℕ) ↦ s' n (δ n);
  (P : (a : Set α) → ℝ≥0∞) (interUnionBalls seq u t)ᶜ < ε
let₄ :
  let u : ℕ → ℕ := fun (n : ℕ) ↦ s' n (δ n);
  (P : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), (⋃ (m : ℕ), ⋃ (_ : m ≤ u i), UniformSpace.ball (seq m) (Prod.swap ⁻¹' t i))ᶜ) < ε
let₅ :
  let 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)
let₆ :
  let u : ℕ → ℕ := fun (n : ℕ) ↦ s' n (δ n);
  ∀ (n : ℕ), (P : (a : Set α) → ℝ≥0∞) (⋃ (m : ℕ), ⋃ (_ : m ≤ u n), UniformSpace.ball (seq m) (Prod.swap ⁻¹' t n))ᶜ ≤ δ n
let₇ :
  let 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
let₈ :
  let u : ℕ → ℕ := fun (n : ℕ) ↦ s' n (δ n);
  ∀ (n : ℕ) (h'' : ∀ (n : ℕ), Prod.swap ⁻¹' t n = t n),
    (P : (a : Set α) → ℝ≥0∞) (⋂ (i : ℕ), ⋂ (_ : i ≤ u n), (UniformSpace.ball (seq i) (t n))ᶜ) ≤ δ n
⊢ ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε

Tactic:
classical
    let u : ℕ → ℕ := fun n ↦ s' n (δ n)
    refine ⟨interUnionBalls seq u t, isCompact_closure_interUnionBalls h_basis.toHasBasis seq u, ?_⟩
    rw [interUnionBalls, Set.compl_iInter]
    refine ((measure_iUnion_le _).trans ?_).trans_lt hδ2
    refine ENNReal.tsum_le_tsum (fun n ↦ ?_)
    have h'' n : Prod.swap ⁻¹' t n = t n := by ext; exact (t n).comm
    simp only [h'', compl_iUnion, ge_iff_le]
    exact (s'bound n (δ n) (hδ1 n)).le

Premises used: Set.compl_iInter, ENNReal.tsum_le_tsum, interUnionBalls, ge_iff_le, Set.compl_iUnion, MeasureTheory.measure_iUnion_le, LE.le.trans, LE.le.trans_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
⊢ P.InnerRegularWRT (IsCompact ∘ closure) IsClosed

Tactic:
innerRegularWRT_isCompact_closure_of_univ
    (exists_isCompact_closure_measure_compl_lt P)

Premises used: MeasureTheory.innerRegularWRT_isCompact_closure_of_univ, MeasureTheory.exists_isCompact_closure_measure_compl_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
rw : P.InnerRegularWRT (IsCompact ∘ closure) IsClosed
⊢ P.InnerRegularWRT (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) IsClosed

Tactic:
rw [innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure]

Premises used: MeasureTheory.innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure
-- 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
⊢ P.InnerRegularWRT (IsCompact ∘ closure) IsClosed

Tactic:
innerRegularWRT_isCompact_closure P

Premises used: MeasureTheory.innerRegularWRT_isCompact_closure
-- 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
⊢ P.InnerRegularWRT (IsCompact ∘ closure) IsClosed

Tactic:
exact innerRegularWRT_isCompact_closure P

Premises used: MeasureTheory.innerRegularWRT_isCompact_closure
-- 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
rw : P.InnerRegularWRT (IsCompact ∘ closure) IsClosed
⊢ P.InnerRegularWRT IsCompact IsClosed

Tactic:
rw [← innerRegularWRT_isCompact_closure_iff]

Premises used: MeasureTheory.innerRegularWRT_isCompact_closure_iff
-- 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
⊢ P.InnerRegularWRT (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) IsOpen

Tactic:
(innerRegularWRT_isCompact_isClosed P).trans
    (Measure.InnerRegularWRT.of_pseudoMetrizableSpace P)

Premises used: MeasureTheory.Measure.InnerRegularWRT.trans, MeasureTheory.innerRegularWRT_isCompact_isClosed, MeasureTheory.Measure.InnerRegularWRT.of_pseudoMetrizableSpace
-- 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
⊢ P.InnerRegularWRT IsCompact IsOpen

Tactic:
(innerRegularWRT_isCompact P).trans
    (Measure.InnerRegularWRT.of_pseudoMetrizableSpace P)

Premises used: MeasureTheory.Measure.InnerRegularWRT.trans, MeasureTheory.innerRegularWRT_isCompact, MeasureTheory.Measure.InnerRegularWRT.of_pseudoMetrizableSpace
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
suffices : P.InnerRegularCompactLTTop
⊢ P.InnerRegular

Tactic:
suffices P.InnerRegularCompactLTTop from inferInstance
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
⊢ P.InnerRegularCompactLTTop

Tactic:
⟨Measure.InnerRegularWRT.measurableSet_of_isOpen ?_ ?_⟩

Premises used: MeasureTheory.Measure.InnerRegularCompactLTTop.mk, MeasureTheory.Measure.InnerRegularWRT.measurableSet_of_isOpen
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : BorelSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
refine_1 : P.InnerRegularWRT IsCompact IsOpen
refine_2 : ∀ ⦃s U : Set α⦄, IsCompact s → IsOpen U → IsCompact (s \ U)
⊢ P.InnerRegularCompactLTTop

Tactic:
refine ⟨Measure.InnerRegularWRT.measurableSet_of_isOpen ?_ ?_⟩