-- Mathlib/MeasureTheory/OuterMeasure/Induced.lean
theorem exists_measurable_superset_forall_eq_trim {ι} [Countable ι] (μ : ι → OuterMeasure α)
    (s : Set α) : ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ i, μ i t = (μ i).trim s

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : ι → Set α
hst : ∀ (i : ι), s ⊆ t i
ht : ∀ (i : ι), MeasurableSet (t i)
hμt : ∀ (i : ι), (μ i) (t i) = (μ i).trim s
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), (μ i) t = (μ i).trim s

Tactic:
replace hst := subset_iInter hst

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : ι → Set α
ht : ∀ (i : ι), MeasurableSet (t i)
hμt : ∀ (i : ι), (μ i) (t i) = (μ i).trim s
hst : s ⊆ ⋂ i, t i
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), (μ i) t = (μ i).trim s

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : ι → Set α
hμt : ∀ (i : ι), (μ i) (t i) = (μ i).trim s
hst : s ⊆ ⋂ i, t i
ht : MeasurableSet (⋂ b, t b)
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), (μ i) t = (μ i).trim s

Tactic:
refine ⟨⋂ i, t i, hst, ht, fun i => le_antisymm ?_ ?_⟩

Result:
case refine_1
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : ι → Set α
hμt : ∀ (i : ι), (μ i) (t i) = (μ i).trim s
hst : s ⊆ ⋂ i, t i
ht : MeasurableSet (⋂ b, t b)
i : ι
⊢ (μ i) (⋂ i, t i) ≤ (μ i).trim s

case refine_2
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : ι → Set α
hμt : ∀ (i : ι), (μ i) (t i) = (μ i).trim s
hst : s ⊆ ⋂ i, t i
ht : MeasurableSet (⋂ b, t b)
i : ι
⊢ (μ i).trim s ≤ (μ i) (⋂ i, t i)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : ι → Set α
ht : ∀ (i : ι), MeasurableSet (t i)
hμt : ∀ (i : ι), (μ i) (t i) = (μ i).trim s
hst : s ⊆ ⋂ i, t i
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), (μ i) t = (μ i).trim s

Tactic:
replace ht := MeasurableSet.iInter ht

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : ι → Set α
hμt : ∀ (i : ι), (μ i) (t i) = (μ i).trim s
hst : s ⊆ ⋂ i, t i
ht : MeasurableSet (⋂ b, t b)
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), (μ i) t = (μ i).trim s

Proof state:
case refine_1
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : ι → Set α
hμt : ∀ (i : ι), (μ i) (t i) = (μ i).trim s
hst : s ⊆ ⋂ i, t i
ht : MeasurableSet (⋂ b, t b)
i : ι
⊢ (μ i) (⋂ i, t i) ≤ (μ i).trim s

case refine_2
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : ι → Set α
hμt : ∀ (i : ι), (μ i) (t i) = (μ i).trim s
hst : s ⊆ ⋂ i, t i
ht : MeasurableSet (⋂ b, t b)
i : ι
⊢ (μ i).trim s ≤ (μ i) (⋂ i, t i)

Tactic:
exacts [hμt i ▸ (μ i).mono (iInter_subset _ _), (measure_mono hst).trans_eq ((μ i).trim_eq ht)]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), (μ i) t = (μ i).trim s

Tactic:
choose t hst ht hμt using fun i => (μ i).exists_measurable_superset_eq_trim s

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : ι → Set α
hst : ∀ (i : ι), s ⊆ t i
ht : ∀ (i : ι), MeasurableSet (t i)
hμt : ∀ (i : ι), (μ i) (t i) = (μ i).trim s
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), (μ i) t = (μ i).trim s