-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_union_congr :
    μ.restrict (s ∪ t) = ν.restrict (s ∪ t) ↔
      μ.restrict s = ν.restrict s ∧ μ.restrict t = ν.restrict t

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
US : Set α
hsub : u ∩ s ⊆ US
hm : MeasurableSet US
hμ : μ US = μ (u ∩ s)
hν : ν US = ν (u ∩ s)
⊢ μ US + μ ((u ∩ t) \ US) = (μ.restrict s) u + (μ.restrict t) (u \ US)

Tactic:
simp only [restrict_apply, hu, hu.diff hm, hμ, ← inter_comm t, inter_diff_assoc]

Result:
no goals

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
⊢ μ.restrict s = ν.restrict s ∧ μ.restrict t = ν.restrict t → μ.restrict (s ∪ t) = ν.restrict (s ∪ t)

Tactic:
rintro ⟨hs, ht⟩

Result:
case intro
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
⊢ μ.restrict (s ∪ t) = ν.restrict (s ∪ t)

Proof state:
case intro
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
⊢ μ.restrict (s ∪ t) = ν.restrict (s ∪ t)

Tactic:
ext1 u hu

Result:
case intro.h
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
⊢ (μ.restrict (s ∪ t)) u = (ν.restrict (s ∪ t)) u

Proof state:
case intro.h
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
⊢ μ (u ∩ s ∪ u ∩ t) = ν (u ∩ s ∪ u ∩ t)

Tactic:
rcases exists_measurable_superset₂ μ ν (u ∩ s) with ⟨US, hsub, hm, hμ, hν⟩

Result:
case intro.h.intro.intro.intro.intro
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
US : Set α
hsub : u ∩ s ⊆ US
hm : MeasurableSet US
hμ : μ US = μ (u ∩ s)
hν : ν US = ν (u ∩ s)
⊢ μ (u ∩ s ∪ u ∩ t) = ν (u ∩ s ∪ u ∩ t)

Proof state:
case intro.h.intro.intro.intro.intro
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
US : Set α
hsub : u ∩ s ⊆ US
hm : MeasurableSet US
hμ : μ US = μ (u ∩ s)
hν : ν US = ν (u ∩ s)
⊢ μ (u ∩ s ∪ u ∩ t) = ν (u ∩ s ∪ u ∩ t)

Tactic:
calc
  μ (u ∩ s ∪ u ∩ t) = μ (US ∪ u ∩ t) :=
    measure_union_congr_of_subset hsub hμ.le Subset.rfl le_rfl
  _ = μ US + μ ((u ∩ t) \ US) := (measure_add_diff hm.nullMeasurableSet _).symm
  _ = restrict μ s u + restrict μ t (u \ US) := by
    simp only [restrict_apply, hu, hu.diff hm, hμ, ← inter_comm t, inter_diff_assoc]
  _ = restrict ν s u + restrict ν t (u \ US) := by rw [hs, ht]
  _ = ν US + ν ((u ∩ t) \ US) := by
    simp only [restrict_apply, hu, hu.diff hm, hν, ← inter_comm t, inter_diff_assoc]
  _ = ν (US ∪ u ∩ t) := measure_add_diff hm.nullMeasurableSet _
  _ = ν (u ∩ s ∪ u ∩ t) := .symm <| measure_union_congr_of_subset hsub hν.le Subset.rfl le_rfl

Result:
no goals

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
US : Set α
hsub : u ∩ s ⊆ US
hm : MeasurableSet US
hμ : μ US = μ (u ∩ s)
hν : ν US = ν (u ∩ s)
⊢ (μ.restrict s) u + (μ.restrict t) (u \ US) = (ν.restrict s) u + (ν.restrict t) (u \ US)

Tactic:
rw [hs, ht]

Result:
no goals

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
⊢ μ.restrict (s ∪ t) = ν.restrict (s ∪ t) ↔ μ.restrict s = ν.restrict s ∧ μ.restrict t = ν.restrict t

Tactic:
refine ⟨fun h ↦ ⟨restrict_congr_mono subset_union_left h,
  restrict_congr_mono subset_union_right h⟩, ?_⟩

Result:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
⊢ μ.restrict s = ν.restrict s ∧ μ.restrict t = ν.restrict t → μ.restrict (s ∪ t) = ν.restrict (s ∪ t)

Proof state:
case intro.h
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
⊢ (μ.restrict (s ∪ t)) u = (ν.restrict (s ∪ t)) u

Tactic:
simp only [restrict_apply hu, inter_union_distrib_left]

Result:
case intro.h
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
⊢ μ (u ∩ s ∪ u ∩ t) = ν (u ∩ s ∪ u ∩ t)

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
US : Set α
hsub : u ∩ s ⊆ US
hm : MeasurableSet US
hμ : μ US = μ (u ∩ s)
hν : ν US = ν (u ∩ s)
⊢ (ν.restrict s) u + (ν.restrict t) (u \ US) = ν US + ν ((u ∩ t) \ US)

Tactic:
simp only [restrict_apply, hu, hu.diff hm, hν, ← inter_comm t, inter_diff_assoc]

Result:
no goals