case intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ m₃ : OuterMeasure α
op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞
h : ∀ (s : Set α), ↑m₁ s = op (↑m₂ s) (↑m₃ s)
s t : Set α
_hst : s ⊆ t
_ht : MeasurableSet t
htm :
  ∀ (i : Fin (Nat.succ (Nat.succ (Nat.succ 0)))),
    ↑(Matrix.vecCons m₁ ![m₂, m₃] i) t = ↑(trim (Matrix.vecCons m₁ ![m₂, m₃] i)) s
⊢ ↑(trim m₁) s = op (↑(trim m₂) s) (↑(trim m₃) s)
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ m₃ : OuterMeasure α
op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞
h : ∀ (s : Set α), ↑m₁ s = op (↑m₂ s) (↑m₃ s)
s : Set α
⊢ ↑(trim m₁) s = op (↑(trim m₂) s) (↑(trim m₃) s)
rcases exists_measurable_superset_forall_eq_trim ![m₁, m₂, m₃] s with ⟨t, _hst, _ht, htm⟩
case intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ m₃ : OuterMeasure α
op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞
h : ∀ (s : Set α), ↑m₁ s = op (↑m₂ s) (↑m₃ s)
s t : Set α
_hst : s ⊆ t
_ht : MeasurableSet t
htm : ↑m₁ t = ↑(trim m₁) s ∧ ↑m₂ t = ↑(trim m₂) s ∧ ↑m₃ t = ↑(trim m₃) s ∧ ∀ (i : Fin 0), ↑![] t = ↑(trim ![]) s
⊢ ↑(trim m₁) s = op (↑(trim m₂) s) (↑(trim m₃) s)
case intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ m₃ : OuterMeasure α
op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞
h : ∀ (s : Set α), ↑m₁ s = op (↑m₂ s) (↑m₃ s)
s t : Set α
_hst : s ⊆ t
_ht : MeasurableSet t
htm :
  ∀ (i : Fin (Nat.succ (Nat.succ (Nat.succ 0)))),
    ↑(Matrix.vecCons m₁ ![m₂, m₃] i) t = ↑(trim (Matrix.vecCons m₁ ![m₂, m₃] i)) s
⊢ ↑(trim m₁) s = op (↑(trim m₂) s) (↑(trim m₃) s)
simp only [Fin.forall_fin_succ, Matrix.cons_val_zero, Matrix.cons_val_succ] at htm
no goals
case intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ m₃ : OuterMeasure α
op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞
h : ∀ (s : Set α), ↑m₁ s = op (↑m₂ s) (↑m₃ s)
s t : Set α
_hst : s ⊆ t
_ht : MeasurableSet t
htm : ↑m₁ t = ↑(trim m₁) s ∧ ↑m₂ t = ↑(trim m₂) s ∧ ↑m₃ t = ↑(trim m₃) s ∧ ∀ (i : Fin 0), ↑![] t = ↑(trim ![]) s
⊢ ↑(trim m₁) s = op (↑(trim m₂) s) (↑(trim m₃) s)
rw [← htm.1, ← htm.2.1, ← htm.2.2.1, h]