α : Type u_1
β : Type ?u.3498865
γ : Type ?u.3498868
δ : Type ?u.3498871
ι : Type ?u.3498874
R : Type ?u.3498877
R' : Type ?u.3498880
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
m₁ m₂ : MeasurableSpace α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m0
t : Set α
ht : MeasurableSet t
⊢ ↑↑(trim (trim μ hm₂) hm₁₂) t = ↑↑(trim μ (_ : m₁ ≤ m0)) t
α : Type u_1
β : Type ?u.3498865
γ : Type ?u.3498868
δ : Type ?u.3498871
ι : Type ?u.3498874
R : Type ?u.3498877
R' : Type ?u.3498880
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
m₁ m₂ : MeasurableSpace α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m0
⊢ trim (trim μ hm₂) hm₁₂ = trim μ (_ : m₁ ≤ m0)
refine @Measure.ext _ m₁ _ _ (fun t ht => ?_)
no goals
α : Type u_1
β : Type ?u.3498865
γ : Type ?u.3498868
δ : Type ?u.3498871
ι : Type ?u.3498874
R : Type ?u.3498877
R' : Type ?u.3498880
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
m₁ m₂ : MeasurableSpace α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m0
t : Set α
ht : MeasurableSet t
⊢ ↑↑(trim (trim μ hm₂) hm₁₂) t = ↑↑(trim μ (_ : m₁ ≤ m0)) t
rw [trim_measurableSet_eq hm₁₂ ht, trim_measurableSet_eq (hm₁₂.trans hm₂) ht,
  trim_measurableSet_eq hm₂ (hm₁₂ t ht)]