α : Type u_1
β : Type ?u.307809
γ : Type ?u.307812
δ : Type ?u.307815
ι : Type ?u.307818
R : Type ?u.307821
R' : Type ?u.307824
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
⊢ restrict μ s = restrict ν s ∧ restrict μ t = restrict ν t → restrict μ (s ∪ t) = restrict ν (s ∪ t)
α : Type u_1
β : Type ?u.307809
γ : Type ?u.307812
δ : Type ?u.307815
ι : Type ?u.307818
R : Type ?u.307821
R' : Type ?u.307824
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
⊢ restrict μ (s ∪ t) = restrict ν (s ∪ t) ↔ restrict μ s = restrict ν s ∧ restrict μ t = restrict ν t
refine'
  ⟨fun h =>
    ⟨restrict_congr_mono (subset_union_left _ _) h,
      restrict_congr_mono (subset_union_right _ _) h⟩,
    _⟩
case intro
α : Type u_1
β : Type ?u.307809
γ : Type ?u.307812
δ : Type ?u.307815
ι : Type ?u.307818
R : Type ?u.307821
R' : Type ?u.307824
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
hs : restrict μ s = restrict ν s
ht : restrict μ t = restrict ν t
⊢ restrict μ (s ∪ t) = restrict ν (s ∪ t)
α : Type u_1
β : Type ?u.307809
γ : Type ?u.307812
δ : Type ?u.307815
ι : Type ?u.307818
R : Type ?u.307821
R' : Type ?u.307824
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
⊢ restrict μ s = restrict ν s ∧ restrict μ t = restrict ν t → restrict μ (s ∪ t) = restrict ν (s ∪ t)
rintro ⟨hs, ht⟩
case intro.h
α : Type u_1
β : Type ?u.307809
γ : Type ?u.307812
δ : Type ?u.307815
ι : Type ?u.307818
R : Type ?u.307821
R' : Type ?u.307824
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s 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
case intro
α : Type u_1
β : Type ?u.307809
γ : Type ?u.307812
δ : Type ?u.307815
ι : Type ?u.307818
R : Type ?u.307821
R' : Type ?u.307824
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
hs : restrict μ s = restrict ν s
ht : restrict μ t = restrict ν t
⊢ restrict μ (s ∪ t) = restrict ν (s ∪ t)
ext1 u hu
case intro.h
α : Type u_1
β : Type ?u.307809
γ : Type ?u.307812
δ : Type ?u.307815
ι : Type ?u.307818
R : Type ?u.307821
R' : Type ?u.307824
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s 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)
case intro.h
α : Type u_1
β : Type ?u.307809
γ : Type ?u.307812
δ : Type ?u.307815
ι : Type ?u.307818
R : Type ?u.307821
R' : Type ?u.307824
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s 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
simp only [restrict_apply hu, inter_union_distrib_left]
case intro.h.intro.intro.intro.intro
α : Type u_1
β : Type ?u.307809
γ : Type ?u.307812
δ : Type ?u.307815
ι : Type ?u.307818
R : Type ?u.307821
R' : Type ?u.307824
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s 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)
case intro.h
α : Type u_1
β : Type ?u.307809
γ : Type ?u.307812
δ : Type ?u.307815
ι : Type ?u.307818
R : Type ?u.307821
R' : Type ?u.307824
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s 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)
rcases exists_measurable_superset₂ μ ν (u ∩ s) with ⟨US, hsub, hm, hμ, hν⟩
no goals
case intro.h.intro.intro.intro.intro
α : Type u_1
β : Type ?u.307809
γ : Type ?u.307812
δ : Type ?u.307815
ι : Type ?u.307818
R : Type ?u.307821
R' : Type ?u.307824
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s 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)
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 _).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 _)
  _ = ν (u ∩ s ∪ u ∩ t) := Eq.symm <| measure_union_congr_of_subset hsub hν.le Subset.rfl le_rfl
no goals
α : Type u_1
β : Type ?u.307809
γ : Type ?u.307812
δ : Type ?u.307815
ι : Type ?u.307818
R : Type ?u.307821
R' : Type ?u.307824
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s 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)
simp only [restrict_apply, hu, hu.diff hm, hμ, ← inter_comm t, inter_diff_assoc]
no goals
α : Type u_1
β : Type ?u.307809
γ : Type ?u.307812
δ : Type ?u.307815
ι : Type ?u.307818
R : Type ?u.307821
R' : Type ?u.307824
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s 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)
rw [hs, ht]
no goals
α : Type u_1
β : Type ?u.307809
γ : Type ?u.307812
δ : Type ?u.307815
ι : Type ?u.307818
R : Type ?u.307821
R' : Type ?u.307824
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s 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)
simp only [restrict_apply, hu, hu.diff hm, hν, ← inter_comm t, inter_diff_assoc]