α : Type u_1
β : Type ?u.139389
γ : Type ?u.139392
δ : Type ?u.139395
ι : Type ?u.139398
R : Type ?u.139401
R' : Type ?u.139404
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t : Set α
h : ↑↑(ν + μ) t ≠ ⊤
h' : s ⊆ t
h'' : ↑↑(ν + μ) s = ↑↑(ν + μ) t
⊢ ↑↑ν s = ↑↑ν t
α : Type u_1
β : Type ?u.139389
γ : Type ?u.139392
δ : Type ?u.139395
ι : Type ?u.139398
R : Type ?u.139401
R' : Type ?u.139404
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t : Set α
h : ↑↑(μ + ν) t ≠ ⊤
h' : s ⊆ t
h'' : ↑↑(μ + ν) s = ↑↑(μ + ν) t
⊢ ↑↑ν s = ↑↑ν t
rw [add_comm] at h'' h
no goals
α : Type u_1
β : Type ?u.139389
γ : Type ?u.139392
δ : Type ?u.139395
ι : Type ?u.139398
R : Type ?u.139401
R' : Type ?u.139404
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t : Set α
h : ↑↑(ν + μ) t ≠ ⊤
h' : s ⊆ t
h'' : ↑↑(ν + μ) s = ↑↑(ν + μ) t
⊢ ↑↑ν s = ↑↑ν t
exact measure_eq_left_of_subset_of_measure_add_eq h h' h''