-- Mathlib/MeasureTheory/OuterMeasure/Induced.lean
theorem trim_iSup {ι} [Countable ι] (μ : ι → OuterMeasure α) :
    trim (⨆ i, μ i) = ⨆ i, trim (μ i)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
⊢ (⨆ i, μ i.down).trim = ⨆ i, (μ i.down).trim

Tactic:
ext1 s

Result:
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
⊢ (⨆ i, μ i.down).trim s = (⨆ i, (μ i.down).trim) s

Proof state:
case h.intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s t : Set α
left✝¹ : s ⊆ t
left✝ : MeasurableSet t
hμt :
  ∀ (i : Option (PLift ι)),
    (Option.elim' (⨆ i, μ i.down) (μ ∘ PLift.down) i) t = (Option.elim' (⨆ i, μ i.down) (μ ∘ PLift.down) i).trim s
⊢ (⨆ i, μ i.down).trim s = (⨆ i, (μ i.down).trim) s

Tactic:
simp only [Option.forall, Option.elim'] at hμt

Result:
case h.intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s t : Set α
left✝¹ : s ⊆ t
left✝ : MeasurableSet t
hμt : (⨆ i, μ i.down) t = (⨆ i, μ i.down).trim s ∧ ∀ (x : PLift ι), ((μ ∘ PLift.down) x) t = ((μ ∘ PLift.down) x).trim s
⊢ (⨆ i, μ i.down).trim s = (⨆ i, (μ i.down).trim) s

Proof state:
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
⊢ (⨆ i, μ i.down).trim s = (⨆ i, (μ i.down).trim) s

Tactic:
obtain ⟨t, _, _, hμt⟩ :=
  exists_measurable_superset_forall_eq_trim
    (Option.elim' (⨆ i, μ (PLift.down i)) (μ ∘ PLift.down)) s

Result:
case h.intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s t : Set α
left✝¹ : s ⊆ t
left✝ : MeasurableSet t
hμt :
  ∀ (i : Option (PLift ι)),
    (Option.elim' (⨆ i, μ i.down) (μ ∘ PLift.down) i) t = (Option.elim' (⨆ i, μ i.down) (μ ∘ PLift.down) i).trim s
⊢ (⨆ i, μ i.down).trim s = (⨆ i, (μ i.down).trim) s

Proof state:
case h.intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s t : Set α
left✝¹ : s ⊆ t
left✝ : MeasurableSet t
hμt : (⨆ i, μ i.down) t = (⨆ i, μ i.down).trim s ∧ ∀ (x : PLift ι), ((μ ∘ PLift.down) x) t = ((μ ∘ PLift.down) x).trim s
⊢ (⨆ i, μ i.down).trim s = (⨆ i, (μ i.down).trim) s

Tactic:
simp only [iSup_apply, ← hμt.1]

Result:
case h.intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s t : Set α
left✝¹ : s ⊆ t
left✝ : MeasurableSet t
hμt : (⨆ i, μ i.down) t = (⨆ i, μ i.down).trim s ∧ ∀ (x : PLift ι), ((μ ∘ PLift.down) x) t = ((μ ∘ PLift.down) x).trim s
⊢ ⨆ i, (μ i.down) t = ⨆ i, (μ i.down).trim s

Proof state:
case h.intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s t : Set α
left✝¹ : s ⊆ t
left✝ : MeasurableSet t
hμt : (⨆ i, μ i.down) t = (⨆ i, μ i.down).trim s ∧ ∀ (x : PLift ι), ((μ ∘ PLift.down) x) t = ((μ ∘ PLift.down) x).trim s
⊢ ⨆ i, (μ i.down) t = ⨆ i, (μ i.down).trim s

Tactic:
exact iSup_congr hμt.2

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
⊢ (⨆ i, μ i).trim = ⨆ i, (μ i).trim

Tactic:
simp_rw [← @iSup_plift_down _ ι]

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
⊢ (⨆ i, μ i.down).trim = ⨆ i, (μ i.down).trim