-- Mathlib/MeasureTheory/Measure/MutuallySingular.lean
lemma mutuallySingular_of_disjoint (h : Disjoint μ ν) : μ ⟂ₘ ν

Proof state:
case h.e'_2.h.h.e'_2.h.e'_4
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x✝ : Set α
⊢ (1 / 2) ^ n = ↑(1 / 2) * 2 * ↑(1 / 2) ^ n

Tactic:
norm_cast

Result:
case h.e'_2.h.h.e'_2.h.e'_4
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x✝ : Set α
⊢ (1 / 2) ^ n = ↑(1 / 2 * 2 * (1 / 2) ^ n)

Proof state:
case h.e'_2.h.h.e'_2.h.e'_4
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x✝ : Set α
⊢ (1 / 2) ^ n = 2 * ↑((1 / 2) ^ (n + 1))

Tactic:
push_cast

Result:
case h.e'_2.h.h.e'_2.h.e'_4
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x✝ : Set α
⊢ (1 / 2) ^ n = 2 * ↑(1 / 2) ^ (n + 1)

Proof state:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
s : ℕ → Set α
hs₂ : ∀ (n : ℕ), μ (s n) = 0
hs₃ : ∀ (n : ℕ), ν (s n)ᶜ ≤ (1 / 2) ^ n
⊢ ν (⋂ i, (s i)ᶜ) = 0

Tactic:
refine eq_zero_of_le_mul_pow (ε := 1) (by norm_num : (1 / 2 : ℝ≥0∞) < 1) <| fun n ↦ ?_

Result:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
s : ℕ → Set α
hs₂ : ∀ (n : ℕ), μ (s n) = 0
hs₃ : ∀ (n : ℕ), ν (s n)ᶜ ≤ (1 / 2) ^ n
n : ℕ
⊢ ν (⋂ i, (s i)ᶜ) ≤ ↑1 * (1 / 2) ^ n

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
s : ℕ → Set α
hs₂ : ∀ (n : ℕ), μ (s n) = 0
hs₃ : ∀ (n : ℕ), ν (s n)ᶜ ≤ (1 / 2) ^ n
⊢ 1 / 2 < 1

Tactic:
norm_num

Result:
no goals

Proof state:
case h.e'_2.h.h.e'_2.h.e'_4
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x✝ : Set α
⊢ (1 / 2) ^ n = ↑((1 / 2) ^ n)

Tactic:
push_cast

Result:
case h.e'_2.h.h.e'_2.h.e'_4
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x✝ : Set α
⊢ (1 / 2) ^ n = ↑(1 / 2) ^ n

Proof state:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
s : ℕ → Set α
hs₂ : ∀ (n : ℕ), μ (s n) = 0
hs₃ : ∀ (n : ℕ), ν (s n)ᶜ ≤ (1 / 2) ^ n
⊢ ν (⋃ n, s n)ᶜ = 0

Tactic:
rw [compl_iUnion]

Result:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
s : ℕ → Set α
hs₂ : ∀ (n : ℕ), μ (s n) = 0
hs₃ : ∀ (n : ℕ), ν (s n)ᶜ ≤ (1 / 2) ^ n
⊢ ν (⋂ i, (s i)ᶜ) = 0

Proof state:
case h.e'_2.h.h.e'_2.h.e'_4
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x✝ : Set α
⊢ (1 / 2) ^ n = 2 * ↑(1 / 2) ^ (n + 1)

Tactic:
rw [pow_succ, ← mul_assoc, mul_comm, ← mul_assoc]

Result:
case h.e'_2.h.h.e'_2.h.e'_4
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x✝ : Set α
⊢ (1 / 2) ^ n = ↑(1 / 2) * 2 * ↑(1 / 2) ^ n

Proof state:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
s : ℕ → Set α
hs₂ : ∀ (n : ℕ), μ (s n) = 0
hs₃ : ∀ (n : ℕ), ν (s n)ᶜ ≤ (1 / 2) ^ n
⊢ univ ⊆ (⋃ i, s i) ∪ (⋃ n, s n)ᶜ

Tactic:
rw [union_compl_self]

Result:
no goals

Proof state:
case h.e'_2.h.h.e'_2.h.e'_4
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x✝ : Set α
⊢ (1 / 2) ^ n = ↑(1 / 2 * 2 * (1 / 2) ^ n)

Tactic:
rw [div_mul_cancel₀, one_mul]

Result:
case h.e'_2.h.h.e'_2.h.e'_4
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x✝ : Set α
⊢ (1 / 2) ^ n = ↑((1 / 2) ^ n)

case h.e'_2.h.h.e'_2.h.e'_4.h
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x✝ : Set α
⊢ 2 ≠ 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
⊢ ∃ s, μ s = 0 ∧ ν sᶜ ≤ (1 / 2) ^ n

Tactic:
convert exists_null_set_measure_lt_of_disjoint h (ε := (1 / 2) ^ (n + 1))
  <| pow_pos (by simp) (n + 1)

Result:
case h.e'_2.h.h.e'_2.h.e'_4
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x✝ : Set α
⊢ (1 / 2) ^ n = 2 * ↑((1 / 2) ^ (n + 1))

Proof state:
case h.e'_2.h.h.e'_2.h.e'_4.h
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x✝ : Set α
⊢ 2 ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
s : ℕ → Set α
hs₂ : ∀ (n : ℕ), μ (s n) = 0
hs₃ : ∀ (n : ℕ), ν (s n)ᶜ ≤ (1 / 2) ^ n
n : ℕ
⊢ ν (⋂ i, (s i)ᶜ) ≤ ↑1 * (1 / 2) ^ n

Tactic:
rw [ENNReal.coe_one, one_mul]

Result:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
s : ℕ → Set α
hs₂ : ∀ (n : ℕ), μ (s n) = 0
hs₃ : ∀ (n : ℕ), ν (s n)ᶜ ≤ (1 / 2) ^ n
n : ℕ
⊢ ν (⋂ i, (s i)ᶜ) ≤ (1 / 2) ^ n

Proof state:
case h.e'_2.h.h.e'_2.h.e'_4
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x✝ : Set α
⊢ (1 / 2) ^ n = ↑(1 / 2) ^ n

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
s : ℕ → Set α
hs₂ : ∀ (n : ℕ), μ (s n) = 0
hs₃ : ∀ (n : ℕ), ν (s n)ᶜ ≤ (1 / 2) ^ n
⊢ μ ⟂ₘ ν

Tactic:
refine Measure.MutuallySingular.mk (t := (⋃ n, s n)ᶜ) (measure_iUnion_null hs₂) ?_ ?_

Result:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
s : ℕ → Set α
hs₂ : ∀ (n : ℕ), μ (s n) = 0
hs₃ : ∀ (n : ℕ), ν (s n)ᶜ ≤ (1 / 2) ^ n
⊢ ν (⋃ n, s n)ᶜ = 0

case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
s : ℕ → Set α
hs₂ : ∀ (n : ℕ), μ (s n) = 0
hs₃ : ∀ (n : ℕ), ν (s n)ᶜ ≤ (1 / 2) ^ n
⊢ univ ⊆ (⋃ i, s i) ∪ (⋃ n, s n)ᶜ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
⊢ 0 < 1 / 2

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
h' : ∀ (n : ℕ), ∃ s, μ s = 0 ∧ ν sᶜ ≤ (1 / 2) ^ n
⊢ μ ⟂ₘ ν

Tactic:
choose s hs₂ hs₃ using h'

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
s : ℕ → Set α
hs₂ : ∀ (n : ℕ), μ (s n) = 0
hs₃ : ∀ (n : ℕ), ν (s n)ᶜ ≤ (1 / 2) ^ n
⊢ μ ⟂ₘ ν

Proof state:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
s : ℕ → Set α
hs₂ : ∀ (n : ℕ), μ (s n) = 0
hs₃ : ∀ (n : ℕ), ν (s n)ᶜ ≤ (1 / 2) ^ n
n : ℕ
⊢ ν (⋂ i, (s i)ᶜ) ≤ (1 / 2) ^ n

Tactic:
exact (measure_mono <| iInter_subset_of_subset n fun _ ht ↦ ht).trans (hs₃ n)

Result:
no goals