-- Mathlib/MeasureTheory/Measure/MutuallySingular.lean
lemma exists_null_set_measure_lt_of_disjoint (h : Disjoint μ ν) {ε : ℝ≥0} (hε : 0 < ε) :
    ∃ s, μ s = 0 ∧ ν sᶜ ≤ 2 * ε

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
n : ℕ
⊢ ∃ x ∈ {m | ∃ t, m = μ t + ν tᶜ}, x < ↑ε * (1 / 2) ^ n

Tactic:
refine exists_lt_of_csInf_lt ⟨ν univ, ∅, by simp⟩ <| h₁ ▸ ENNReal.mul_pos ?_ (by simp)

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
n : ℕ
⊢ ↑ε ≠ 0

Proof state:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
t : ℕ → Set α
ht₂ : ∀ (n : ℕ), μ (t n) + ν (t n)ᶜ < ↑ε * (1 / 2) ^ n
⊢ ν (⋂ n, t n)ᶜ ≤ 2 * ↑ε

Tactic:
rw [compl_iInter, (by simp [ENNReal.tsum_mul_left, mul_comm] :
  2 * (ε : ℝ≥0∞) = ∑' (n : ℕ), ε * (1 / 2 : ℝ≥0∞) ^ n)]

Result:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
t : ℕ → Set α
ht₂ : ∀ (n : ℕ), μ (t n) + ν (t n)ᶜ < ↑ε * (1 / 2) ^ n
⊢ ν (⋃ i, (t i)ᶜ) ≤ ∑' (n : ℕ), ↑ε * (1 / 2) ^ n

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
n : ℕ
⊢ (1 / 2) ^ n ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
t : ℕ → Set α
ht₂ : ∀ (n : ℕ), μ (t n) + ν (t n)ᶜ < ↑ε * (1 / 2) ^ n
⊢ μ (⋂ n, t n) = 0

Tactic:
refine eq_zero_of_le_mul_pow (by norm_num)
  fun n ↦ ((measure_mono <| iInter_subset_of_subset n fun _ ht ↦ ht).trans
  (le_add_right le_rfl)).trans (ht₂ n).le

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
n : ℕ
⊢ ↑ε ≠ 0

Tactic:
norm_cast

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
n : ℕ
⊢ ¬ε = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
n : ℕ
⊢ ν univ = μ ∅ + ν ∅ᶜ

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
t : ℕ → Set α
ht₂ : ∀ (n : ℕ), μ (t n) + ν (t n)ᶜ < ↑ε * (1 / 2) ^ n
⊢ 2 * ↑ε = ∑' (n : ℕ), ↑ε * (1 / 2) ^ n

Tactic:
simp [ENNReal.tsum_mul_left, mul_comm]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
h₂ : ∀ (n : ℕ), ∃ t, μ t + ν tᶜ < ↑ε * (1 / 2) ^ n
⊢ ∃ s, μ s = 0 ∧ ν sᶜ ≤ 2 * ↑ε

Tactic:
choose t ht₂ using h₂

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
t : ℕ → Set α
ht₂ : ∀ (n : ℕ), μ (t n) + ν (t n)ᶜ < ↑ε * (1 / 2) ^ n
⊢ ∃ s, μ s = 0 ∧ ν sᶜ ≤ 2 * ↑ε

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : (μ ⊓ ν) univ = 0
⊢ ∃ s, μ s = 0 ∧ ν sᶜ ≤ 2 * ↑ε

Tactic:
simp_rw [Measure.inf_apply MeasurableSet.univ, inter_univ] at h₁

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
⊢ ∃ s, μ s = 0 ∧ ν sᶜ ≤ 2 * ↑ε

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
⊢ ∃ s, μ s = 0 ∧ ν sᶜ ≤ 2 * ↑ε

Tactic:
have h₂ : ∀ n : ℕ, ∃ t, μ t + ν tᶜ < ε * (1 / 2) ^ n := by
  intro n
  obtain ⟨m, ⟨t, ht₁, rfl⟩, hm₂⟩ :
      ∃ x ∈ {m | ∃ t, m = μ t + ν tᶜ}, x < ε * (1 / 2 : ℝ≥0∞) ^ n := by
    refine exists_lt_of_csInf_lt ⟨ν univ, ∅, by simp⟩ <| h₁ ▸ ENNReal.mul_pos ?_ (by simp)
    norm_cast
    exact hε.ne.symm
  exact ⟨t, hm₂⟩

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
h₂ : ∀ (n : ℕ), ∃ t, μ t + ν tᶜ < ↑ε * (1 / 2) ^ n
⊢ ∃ s, μ s = 0 ∧ ν sᶜ ≤ 2 * ↑ε

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
t : ℕ → Set α
ht₂ : ∀ (n : ℕ), μ (t n) + ν (t n)ᶜ < ↑ε * (1 / 2) ^ n
⊢ 1 / 2 < 1

Tactic:
norm_num

Result:
no goals

Proof state:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
t : ℕ → Set α
ht₂ : ∀ (n : ℕ), μ (t n) + ν (t n)ᶜ < ↑ε * (1 / 2) ^ n
⊢ ∑' (i : ℕ), ν (t i)ᶜ ≤ ∑' (n : ℕ), ↑ε * (1 / 2) ^ n

Tactic:
exact tsum_le_tsum (fun n ↦ (le_add_left le_rfl).trans (ht₂ n).le)
  ENNReal.summable ENNReal.summable

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
⊢ ∃ s, μ s = 0 ∧ ν sᶜ ≤ 2 * ↑ε

Tactic:
have h₁ : (μ ⊓ ν) univ = 0 := le_bot_iff.1 (h (inf_le_left (b := ν)) inf_le_right) ▸ rfl

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : (μ ⊓ ν) univ = 0
⊢ ∃ s, μ s = 0 ∧ ν sᶜ ≤ 2 * ↑ε

Proof state:
case intro.intro.intro.refl
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
n : ℕ
t : Set α
hm₂ : μ t + ν tᶜ < ↑ε * (1 / 2) ^ n
⊢ ∃ t, μ t + ν tᶜ < ↑ε * (1 / 2) ^ n

Tactic:
exact ⟨t, hm₂⟩

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
n : ℕ
⊢ ¬ε = 0

Tactic:
exact hε.ne.symm

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
n : ℕ
⊢ ∃ t, μ t + ν tᶜ < ↑ε * (1 / 2) ^ n

Tactic:
obtain ⟨m, ⟨t, ht₁, rfl⟩, hm₂⟩ :
    ∃ x ∈ {m | ∃ t, m = μ t + ν tᶜ}, x < ε * (1 / 2 : ℝ≥0∞) ^ n := by
  refine exists_lt_of_csInf_lt ⟨ν univ, ∅, by simp⟩ <| h₁ ▸ ENNReal.mul_pos ?_ (by simp)
  norm_cast
  exact hε.ne.symm

Result:
case intro.intro.intro.refl
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
n : ℕ
t : Set α
hm₂ : μ t + ν tᶜ < ↑ε * (1 / 2) ^ n
⊢ ∃ t, μ t + ν tᶜ < ↑ε * (1 / 2) ^ n

Proof state:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
t : ℕ → Set α
ht₂ : ∀ (n : ℕ), μ (t n) + ν (t n)ᶜ < ↑ε * (1 / 2) ^ n
⊢ ν (⋃ i, (t i)ᶜ) ≤ ∑' (n : ℕ), ↑ε * (1 / 2) ^ n

Tactic:
refine (measure_iUnion_le _).trans ?_

Result:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
t : ℕ → Set α
ht₂ : ∀ (n : ℕ), μ (t n) + ν (t n)ᶜ < ↑ε * (1 / 2) ^ n
⊢ ∑' (i : ℕ), ν (t i)ᶜ ≤ ∑' (n : ℕ), ↑ε * (1 / 2) ^ n

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
⊢ ∀ (n : ℕ), ∃ t, μ t + ν tᶜ < ↑ε * (1 / 2) ^ n

Tactic:
intro n

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
n : ℕ
⊢ ∃ t, μ t + ν tᶜ < ↑ε * (1 / 2) ^ n