-- Mathlib/MeasureTheory/Measure/Tight.lean
/-- A set of measures `S` is tight if for all `0 < ε`, there exists a compact set `K` such that
for all `μ ∈ S`, `μ Kᶜ ≤ ε`. -/
lemma IsTightMeasureSet_iff_exists_isCompact_measure_compl_le :
    IsTightMeasureSet S ↔ ∀ ε, 0 < ε → ∃ K : Set α, IsCompact K ∧ ∀ μ ∈ S, μ (Kᶜ) ≤ ε

Proof state:
case refine_1.intro.intro.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
mα : MeasurableSpace α
S : Set (Measure α)
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ s, (∃ t, IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ i ∈ S, i t ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
A : Set α
hA : ∀ t ⊆ A, ∀ i ∈ S, i t ≤ ε
K : Set α
h1 : IsCompact K
h2 : Kᶜ ⊆ A
⊢ ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε

Tactic:
exact ⟨K, h1, hA Kᶜ h2⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
mα : MeasurableSpace α
S : Set (Measure α)
⊢ (∀ (ε : ℝ≥0∞), 0 < ε → ∃ s, (∃ t, IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ i ∈ S, i t ≤ ε) ↔
    ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε

Tactic:
refine ⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ?_⟩

Result:
case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
mα : MeasurableSpace α
S : Set (Measure α)
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ s, (∃ t, IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ i ∈ S, i t ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε

case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
mα : MeasurableSpace α
S : Set (Measure α)
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ s, (∃ t, IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ i ∈ S, i t ≤ ε

Proof state:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
mα : MeasurableSpace α
S : Set (Measure α)
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ s, (∃ t, IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ i ∈ S, i t ≤ ε

Tactic:
obtain ⟨K, h1, h2⟩ := h ε hε

Result:
case refine_2.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
mα : MeasurableSpace α
S : Set (Measure α)
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
K : Set α
h1 : IsCompact K
h2 : ∀ μ ∈ S, μ Kᶜ ≤ ε
⊢ ∃ s, (∃ t, IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ i ∈ S, i t ≤ ε

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
mα : MeasurableSpace α
S : Set (Measure α)
⊢ IsTightMeasureSet S ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε

Tactic:
simp only [IsTightMeasureSet, ENNReal.tendsto_nhds ENNReal.zero_ne_top, gt_iff_lt, zero_add,
  iSup_apply, mem_Icc, tsub_le_iff_right, zero_le, iSup_le_iff, true_and, eventually_smallSets,
  mem_cocompact]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
mα : MeasurableSpace α
S : Set (Measure α)
⊢ (∀ (ε : ℝ≥0∞), 0 < ε → ∃ s, (∃ t, IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ i ∈ S, i t ≤ ε) ↔
    ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε

Proof state:
case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
mα : MeasurableSpace α
S : Set (Measure α)
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ s, (∃ t, IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ i ∈ S, i t ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε

Tactic:
obtain ⟨A, ⟨K, h1, h2⟩, hA⟩ := h ε hε

Result:
case refine_1.intro.intro.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
mα : MeasurableSpace α
S : Set (Measure α)
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ s, (∃ t, IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ i ∈ S, i t ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
A : Set α
hA : ∀ t ⊆ A, ∀ i ∈ S, i t ≤ ε
K : Set α
h1 : IsCompact K
h2 : Kᶜ ⊆ A
⊢ ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε

Proof state:
case refine_2.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
mα : MeasurableSpace α
S : Set (Measure α)
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
K : Set α
h1 : IsCompact K
h2 : ∀ μ ∈ S, μ Kᶜ ≤ ε
⊢ ∃ s, (∃ t, IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ i ∈ S, i t ≤ ε

Tactic:
exact ⟨Kᶜ, ⟨K, h1, subset_rfl⟩, fun A hA μ hμS ↦ (μ.mono hA).trans (h2 μ hμS)⟩

Result:
no goals