-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem exists_positive_of_not_mutuallySingular (μ ν : Measure α) [IsFiniteMeasure μ]
    [IsFiniteMeasure ν] (h : ¬ μ ⟂ₘ ν) :
    ∃ ε : ℝ≥0, 0 < ε ∧
      ∃ E : Set α, MeasurableSet E ∧ 0 < ν E
        ∧ ∀ A, MeasurableSet A → ε * ν (A ∩ E) ≤ μ (A ∩ E)

Proof state:
case intro
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
hf₃ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ (f n)ᶜ)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)
hA₃ : ∀ (n : ℕ), μ A ≤ ↑(1 / (↑n + 1)) * ν A
hμ : μ A = 0
h : ∀ (s : Set α), MeasurableSet s → μ s = 0 → ν sᶜ ≠ 0
this : ν (⋃ i, f i) ≠ 0
n : ℕ
hn : 0 < ν (f n)
⊢ ∃ ε, 0 < ε ∧ ∃ E, MeasurableSet E ∧ 0 < ν E ∧ ∀ (A : Set α), MeasurableSet A → ↑ε * ν (A ∩ E) ≤ μ (A ∩ E)

Tactic:
exact ⟨1 / (n + 1), by simp, f n, hf₁ n, hn, hf₂ n⟩

Result:
no goals

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
hf₃ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ (f n)ᶜ)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)
μA : ℝ≥0
hA₃✝¹ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ν A
νA : ℝ≥0
hA₃✝ hA₃ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ↑νA
hb : 0 < νA
c : ℝ≥0
hc : 0 < c
⊢ μA ≤ c

Tactic:
have : ∃ n : ℕ, 1 / (n + 1 : ℝ) < c * (νA : ℝ)⁻¹ := by
  refine exists_nat_one_div_lt ?_
  positivity

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
hf₃ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ (f n)ᶜ)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)
μA : ℝ≥0
hA₃✝¹ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ν A
νA : ℝ≥0
hA₃✝ hA₃ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ↑νA
hb : 0 < νA
c : ℝ≥0
hc : 0 < c
this : ∃ n, 1 / (↑n + 1) < ↑c * (↑νA)⁻¹
⊢ μA ≤ c

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
hf₃ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ (f n)ᶜ)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)
μA : ℝ≥0
hA₃✝¹ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ν A
νA : ℝ≥0
hA₃✝ hA₃ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ↑νA
hb : νA = 0
⊢ μA = 0

Tactic:
specialize hA₃ 0

Result:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
hf₃ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ (f n)ᶜ)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)
μA : ℝ≥0
hA₃✝¹ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ν A
νA : ℝ≥0
hA₃✝ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ↑νA
hb : νA = 0
hA₃ : ↑μA ≤ ↑(1 / (↑0 + 1)) * ↑νA
⊢ μA = 0

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
hf₃ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ (f n)ᶜ)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)
μA : ℝ≥0
hA₃✝¹ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ν A
νA : ℝ≥0
hA₃✝ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ↑νA
hb : νA = 0
hA₃ : ↑μA ≤ ↑(1 / (↑0 + 1)) * ↑νA
⊢ μA = 0

Tactic:
simp only [CharP.cast_eq_zero, zero_add, ne_eq, one_ne_zero, not_false_eq_true, div_self,
  ENNReal.coe_one, hb, ENNReal.coe_zero, mul_zero, nonpos_iff_eq_zero,
  ENNReal.coe_eq_zero] at hA₃

Result:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
hf₃ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ (f n)ᶜ)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)
μA : ℝ≥0
hA₃✝¹ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ν A
νA : ℝ≥0
hA₃✝ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ↑νA
hb : νA = 0
hA₃ : μA = 0
⊢ μA = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
hf₃ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ (f n)ᶜ)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)
hA₃ : ∀ (n : ℕ), μ A ≤ ↑(1 / (↑n + 1)) * ν A
⊢ μ A = 0

Tactic:
lift μ A to ℝ≥0 using measure_ne_top _ _ with μA

Result:
case intro
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
hf₃ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ (f n)ᶜ)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)
μA : ℝ≥0
hA₃✝ hA₃ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ν A
⊢ ↑μA = 0