-- Mathlib/MeasureTheory/Measure/MutuallySingular.lean
lemma disjoint_of_disjoint_ae (h : Disjoint (ae μ) (ae ν)) : Disjoint μ ν

Proof state:
case intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
this : ⊥ = 0
t₁ : Set α
ht₁ : t₁ ∈ ae μ
t₂ : Set α
ht₂ : t₂ ∈ ae ν
h_eq' : sᶜ = t₁ ∩ t₂
h_eq : s = t₁ᶜ ∪ t₂ᶜ
⊢ sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)} = 0

Tactic:
rw [mem_ae_iff] at ht₁ ht₂

Result:
case intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
this : ⊥ = 0
t₁ : Set α
ht₁ : μ t₁ᶜ = 0
t₂ : Set α
ht₂ : ν t₂ᶜ = 0
h_eq' : sᶜ = t₁ ∩ t₂
h_eq : s = t₁ᶜ ∪ t₂ᶜ
⊢ sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)} = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
this : ⊥ = 0
h : ∃ t₁ ∈ ae μ, ∃ t₂ ∈ ae ν, sᶜ = t₁ ∩ t₂
⊢ sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)} = 0

Tactic:
obtain ⟨t₁, ht₁, t₂, ht₂, h_eq'⟩ := h

Result:
case intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
this : ⊥ = 0
t₁ : Set α
ht₁ : t₁ ∈ ae μ
t₂ : Set α
ht₂ : t₂ ∈ ae ν
h_eq' : sᶜ = t₁ ∩ t₂
⊢ sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)} = 0

Proof state:
case intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
this : ⊥ = 0
t₁ : Set α
ht₁ : μ t₁ᶜ = 0
t₂ : Set α
ht₂ : ν t₂ᶜ = 0
h_eq' : sᶜ = t₁ ∩ t₂
h_eq : s = t₁ᶜ ∪ t₂ᶜ
⊢ 0 ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}

Tactic:
rw [h_eq]

Result:
case intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
this : ⊥ = 0
t₁ : Set α
ht₁ : μ t₁ᶜ = 0
t₂ : Set α
ht₂ : ν t₂ᶜ = 0
h_eq' : sᶜ = t₁ ∩ t₂
h_eq : s = t₁ᶜ ∪ t₂ᶜ
⊢ 0 ∈ {m | ∃ t, m = μ (t ∩ (t₁ᶜ ∪ t₂ᶜ)) + ν (tᶜ ∩ (t₁ᶜ ∪ t₂ᶜ))}

Proof state:
case intro.intro.intro.intro.right
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
this : ⊥ = 0
t₁ : Set α
ht₁ : μ t₁ᶜ = 0
t₂ : Set α
ht₂ : ν t₂ᶜ = 0
h_eq' : sᶜ = t₁ ∩ t₂
h_eq : s = t₁ᶜ ∪ t₂ᶜ
⊢ ν ((t₁ᶜ ∩ t₂)ᶜ ∩ (t₁ᶜ ∪ t₂ᶜ)) = 0

Tactic:
rw [compl_inter, compl_compl, union_eq_compl_compl_inter_compl,
  union_eq_compl_compl_inter_compl, ← compl_union, compl_compl, compl_compl, inter_comm,
  inter_comm t₁, union_comm, inter_union_compl]

Result:
case intro.intro.intro.intro.right
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
this : ⊥ = 0
t₁ : Set α
ht₁ : μ t₁ᶜ = 0
t₂ : Set α
ht₂ : ν t₂ᶜ = 0
h_eq' : sᶜ = t₁ ∩ t₂
h_eq : s = t₁ᶜ ∪ t₂ᶜ
⊢ ν t₂ᶜ = 0

Proof state:
case intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
this : ⊥ = 0
t₁ : Set α
ht₁ : μ t₁ᶜ = 0
t₂ : Set α
ht₂ : ν t₂ᶜ = 0
h_eq' : sᶜ = t₁ ∩ t₂
h_eq : s = t₁ᶜ ∪ t₂ᶜ
⊢ μ (t₁ᶜ ∩ t₂ ∩ (t₁ᶜ ∪ t₂ᶜ)) + ν ((t₁ᶜ ∩ t₂)ᶜ ∩ (t₁ᶜ ∪ t₂ᶜ)) = 0

Tactic:
rw [add_eq_zero]

Result:
case intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
this : ⊥ = 0
t₁ : Set α
ht₁ : μ t₁ᶜ = 0
t₂ : Set α
ht₂ : ν t₂ᶜ = 0
h_eq' : sᶜ = t₁ ∩ t₂
h_eq : s = t₁ᶜ ∪ t₂ᶜ
⊢ μ (t₁ᶜ ∩ t₂ ∩ (t₁ᶜ ∪ t₂ᶜ)) = 0 ∧ ν ((t₁ᶜ ∩ t₂)ᶜ ∩ (t₁ᶜ ∪ t₂ᶜ)) = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : ae μ ⊓ ae ν ≤ ⊥
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
⊢ (μ ⊓ ν) s ≤ ⊥ s

Tactic:
rw [Measure.inf_apply hs]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : ae μ ⊓ ae ν ≤ ⊥
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
⊢ sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)} ≤ ⊥ s

Proof state:
case intro.intro.intro.intro.left
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
this : ⊥ = 0
t₁ : Set α
ht₁ : μ t₁ᶜ = 0
t₂ : Set α
ht₂ : ν t₂ᶜ = 0
h_eq' : sᶜ = t₁ ∩ t₂
h_eq : s = t₁ᶜ ∪ t₂ᶜ
⊢ μ (t₁ᶜ ∩ t₂) = 0

Tactic:
exact measure_inter_null_of_null_left _ ht₁

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint (ae μ) (ae ν)
⊢ Disjoint μ ν

Tactic:
rw [disjoint_iff_inf_le] at h ⊢

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : ae μ ⊓ ae ν ≤ ⊥
⊢ μ ⊓ ν ≤ ⊥

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : ae μ ⊓ ae ν ≤ ⊥
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
this : ⊥ = 0
⊢ sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)} ≤ ⊥ s

Tactic:
simp only [this, Measure.coe_zero, Pi.zero_apply, nonpos_iff_eq_zero]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : ae μ ⊓ ae ν ≤ ⊥
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
this : ⊥ = 0
⊢ sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)} = 0

Proof state:
case intro.intro.intro.intro.left
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
this : ⊥ = 0
t₁ : Set α
ht₁ : μ t₁ᶜ = 0
t₂ : Set α
ht₂ : ν t₂ᶜ = 0
h_eq' : sᶜ = t₁ ∩ t₂
h_eq : s = t₁ᶜ ∪ t₂ᶜ
⊢ μ (t₁ᶜ ∩ t₂ ∩ (t₁ᶜ ∪ t₂ᶜ)) = 0

Tactic:
refine measure_inter_null_of_null_left _ ?_

Result:
case intro.intro.intro.intro.left
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
this : ⊥ = 0
t₁ : Set α
ht₁ : μ t₁ᶜ = 0
t₂ : Set α
ht₂ : ν t₂ᶜ = 0
h_eq' : sᶜ = t₁ ∩ t₂
h_eq : s = t₁ᶜ ∪ t₂ᶜ
⊢ μ (t₁ᶜ ∩ t₂) = 0

Proof state:
case intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
this : ⊥ = 0
t₁ : Set α
ht₁ : μ t₁ᶜ = 0
t₂ : Set α
ht₂ : ν t₂ᶜ = 0
h_eq' : sᶜ = t₁ ∩ t₂
h_eq : s = t₁ᶜ ∪ t₂ᶜ
⊢ sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)} = 0

Tactic:
refine le_antisymm ?_ zero_le'

Result:
case intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
this : ⊥ = 0
t₁ : Set α
ht₁ : μ t₁ᶜ = 0
t₂ : Set α
ht₂ : ν t₂ᶜ = 0
h_eq' : sᶜ = t₁ ∩ t₂
h_eq : s = t₁ᶜ ∪ t₂ᶜ
⊢ sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)} ≤ 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : ae μ ⊓ ae ν ≤ ⊥
⊢ μ ⊓ ν ≤ ⊥

Tactic:
refine Measure.le_intro fun s hs _ ↦ ?_

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : ae μ ⊓ ae ν ≤ ⊥
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
⊢ (μ ⊓ ν) s ≤ ⊥ s

Proof state:
case intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
this : ⊥ = 0
t₁ : Set α
ht₁ : μ t₁ᶜ = 0
t₂ : Set α
ht₂ : ν t₂ᶜ = 0
h_eq' : sᶜ = t₁ ∩ t₂
h_eq : s = t₁ᶜ ∪ t₂ᶜ
⊢ μ (t₁ᶜ ∩ t₂ ∩ (t₁ᶜ ∪ t₂ᶜ)) = 0 ∧ ν ((t₁ᶜ ∩ t₂)ᶜ ∩ (t₁ᶜ ∪ t₂ᶜ)) = 0

Tactic:
constructor

Result:
case intro.intro.intro.intro.left
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
this : ⊥ = 0
t₁ : Set α
ht₁ : μ t₁ᶜ = 0
t₂ : Set α
ht₂ : ν t₂ᶜ = 0
h_eq' : sᶜ = t₁ ∩ t₂
h_eq : s = t₁ᶜ ∪ t₂ᶜ
⊢ μ (t₁ᶜ ∩ t₂ ∩ (t₁ᶜ ∪ t₂ᶜ)) = 0

case intro.intro.intro.intro.right
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
this : ⊥ = 0
t₁ : Set α
ht₁ : μ t₁ᶜ = 0
t₂ : Set α
ht₂ : ν t₂ᶜ = 0
h_eq' : sᶜ = t₁ ∩ t₂
h_eq : s = t₁ᶜ ∪ t₂ᶜ
⊢ ν ((t₁ᶜ ∩ t₂)ᶜ ∩ (t₁ᶜ ∪ t₂ᶜ)) = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
this : ⊥ = 0
h : sᶜ ∈ ae μ ⊓ ae ν
⊢ sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)} = 0

Tactic:
rw [mem_inf_iff] at h

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
this : ⊥ = 0
h : ∃ t₁ ∈ ae μ, ∃ t₂ ∈ ae ν, sᶜ = t₁ ∩ t₂
⊢ sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)} = 0