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

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)} = 0

Tactic:
specialize h (mem_bot (s := sᶜ))

Result:
α : 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

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₂ᶜ = 0

Tactic:
exact ht₂

Result:
no goals

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₂
⊢ sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)} = 0

Tactic:
have h_eq : s = t₁ᶜ ∪ t₂ᶜ := by
  rw [union_eq_compl_compl_inter_compl, compl_compl, compl_compl, ← h_eq', compl_compl]

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₂
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
t₁ : Set α
ht₁ : t₁ ∈ ae μ
t₂ : Set α
ht₂ : t₂ ∈ ae ν
h_eq' : sᶜ = t₁ ∩ t₂
⊢ s = t₁ᶜ ∪ t₂ᶜ

Tactic:
rw [union_eq_compl_compl_inter_compl, compl_compl, compl_compl, ← h_eq', compl_compl]

Result:
no goals

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 ∩ (t₁ᶜ ∪ t₂ᶜ)) + ν (tᶜ ∩ (t₁ᶜ ∪ t₂ᶜ))}

Tactic:
refine ⟨t₁ᶜ ∩ t₂, Eq.symm ?_⟩

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₂ᶜ)) + ν ((t₁ᶜ ∩ t₂)ᶜ ∩ (t₁ᶜ ∪ t₂ᶜ)) = 0

Proof state:
α : 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

Tactic:
have : (⊥ : Measure α) = 0 := rfl

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)} ≤ ⊥ 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₂ᶜ
⊢ sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)} ≤ 0

Tactic:
refine sInf_le_of_le (a := 0) (b := 0) ?_ le_rfl

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 ∩ s) + ν (tᶜ ∩ s)}