awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ¬ms = ∞
this_1 : ∀ r > ms, ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
t : (n : ℕ) → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t n) < ms + (↑n : ℝ≥0∞)⁻¹
this : Tendsto (fun (n : ℕ) ↦ ms + (↑n : ℝ≥0∞)⁻¹) atTop (𝓝 ms)
⊢ LE.le (α := ℝ≥0∞)
    (⨅ (_ : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), t n)), (m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) : ℝ≥0∞)

Tactic:
iInf_le _ (MeasurableSet.iInter hm)

Premises used: iInf_le, MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ¬ms = ∞
this_1 : ∀ r > ms, ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
t : (n : ℕ) → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t n) < ms + (↑n : ℝ≥0∞)⁻¹
this : Tendsto (fun (n : ℕ) ↦ ms + (↑n : ℝ≥0∞)⁻¹) atTop (𝓝 ms)
⊢ LE.le (α := ℝ≥0∞)
    (⨅ (_ : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), t n)), (m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) : ℝ≥0∞)

Tactic:
exact iInf_le _ (MeasurableSet.iInter hm)

Premises used: iInf_le, MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
h : Eq (α := ℝ≥0∞) ((m.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rcases :
  ∀ (t : Set α) (hst : s ⊆ t) (ht : MeasurableSet t)
    (hm : Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((m.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
    ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rcases exists_measurable_superset_eq_trim m s with ⟨t, hst, ht, hm⟩

Premises used: MeasureTheory.OuterMeasure.exists_measurable_superset_eq_trim
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
h : Eq (α := ℝ≥0∞) ((m.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
hst : s ⊆ t
ht : MeasurableSet t
hm : Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((m.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
⟨t, hst, ht, h ▸ hm⟩

Premises used: Eq.rec, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
h : Eq (α := ℝ≥0∞) ((m.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
hst : s ⊆ t
ht : MeasurableSet t
hm : Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((m.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact ⟨t, hst, ht, h ▸ hm⟩
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Sort u_2
inst_1 : Countable ι
μ : ι → OuterMeasure α
s : Set α
choose :
  ∀ (t : (i : ι) → Set α) (hst : ∀ (i : ι), s ⊆ t i) (ht : ∀ (i : ι), MeasurableSet (t i))
    (hμt :
      ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (((μ i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
    ∃ (t : Set α),
      s ⊆ t ∧
        MeasurableSet t ∧
          ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (((μ i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∃ (t : Set α),
    s ⊆ t ∧
      MeasurableSet t ∧
        ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (((μ i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

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

Premises used: MeasureTheory.OuterMeasure.exists_measurable_superset_eq_trim
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Sort u_2
inst_1 : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : (i : ι) → Set α
hst : ∀ (i : ι), s ⊆ t i
ht : ∀ (i : ι), MeasurableSet (t i)
hμt : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (((μ i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ s ⊆ ⋂ (i : ι), t i

Tactic:
replace hst := subset_iInter hst
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Sort u_2
inst_1 : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : (i : ι) → Set α
ht : ∀ (i : ι), MeasurableSet (t i)
hμt : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (((μ i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
hst : s ⊆ ⋂ (i : ι), t i
⊢ MeasurableSet.{u_1} (α := α) (⋂ (b : ι), t b)

Tactic:
replace ht := MeasurableSet.iInter ht
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Sort u_2
inst_1 : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : (i : ι) → Set α
hμt : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (((μ i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
hst : s ⊆ ⋂ (i : ι), t i
ht : MeasurableSet.{u_1} (α := α) (⋂ (b : ι), t b)
⊢ ∃ (t : Set α),
    s ⊆ t ∧
      MeasurableSet t ∧
        ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (((μ i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

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

Premises used: Set.iInter, le_antisymm, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Sort u_2
inst_1 : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : (i : ι) → Set α
hμt : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (((μ i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
hst : s ⊆ ⋂ (i : ι), t i
ht : MeasurableSet.{u_1} (α := α) (⋂ (b : ι), t b)
refine_1 :
  ∀ (i : ι),
    LE.le (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), t i) : ℝ≥0∞) (((μ i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
refine_2 :
  ∀ (i : ι),
    LE.le (α := ℝ≥0∞) (((μ i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), t i) : ℝ≥0∞)
⊢ ∃ (t : Set α),
    s ⊆ t ∧
      MeasurableSet t ∧
        ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (((μ i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
refine ⟨⋂ i, t i, hst, ht, fun i => le_antisymm ?_ ?_⟩
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Sort u_2
inst_1 : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : (i : ι) → Set α
hμt : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (((μ i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
hst : s ⊆ ⋂ (i : ι), t i
ht : MeasurableSet.{u_1} (α := α) (⋂ (b : ι), t b)
i : ι
⊢ LE.le (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), t i) : ℝ≥0∞) (((μ i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
hμt i ▸ (μ i).mono (iInter_subset _ _)

Premises used: MeasureTheory.OuterMeasure.mono, Eq.rec, Set.iInter_subset
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Sort u_2
inst_1 : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : (i : ι) → Set α
hμt : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (((μ i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
hst : s ⊆ ⋂ (i : ι), t i
ht : MeasurableSet.{u_1} (α := α) (⋂ (b : ι), t b)
i : ι
⊢ LE.le (α := ℝ≥0∞) (((μ i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), t i) : ℝ≥0∞)

Tactic:
(measure_mono hst).trans_eq ((μ i).trim_eq ht)

Premises used: LE.le.trans_eq, MeasureTheory.measure_mono, MeasureTheory.OuterMeasure.trim_eq
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Sort u_2
inst_1 : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : (i : ι) → Set α
hμt : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (((μ i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
hst : s ⊆ ⋂ (i : ι), t i
ht : MeasurableSet.{u_1} (α := α) (⋂ (b : ι), t b)
i : ι
⊢ LE.le (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), t i) : ℝ≥0∞) (((μ i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

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

Premises used: LE.le.trans_eq, MeasureTheory.measure_mono, MeasureTheory.OuterMeasure.trim_eq
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m₁ m₂ m₃ : OuterMeasure α
op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞
h : ∀ (s : Set α), (m₁ : (a : Set α) → ℝ≥0∞) s = op ((m₂ : (a : Set α) → ℝ≥0∞) s) ((m₃ : (a : Set α) → ℝ≥0∞) s)
s : Set α
rcases :
  ∀ (t : Set α) (_hst : s ⊆ t) (_ht : MeasurableSet t)
    (htm :
      ∀ (i : Fin (Nat.succ 0).succ.succ),
        Eq (α := ℝ≥0∞) ((![m₁, m₂, m₃] i : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
          (((![m₁, m₂, m₃] i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
    (m₁.trim : (a : Set α) → ℝ≥0∞) s = op ((m₂.trim : (a : Set α) → ℝ≥0∞) s) ((m₃.trim : (a : Set α) → ℝ≥0∞) s)
⊢ (m₁.trim : (a : Set α) → ℝ≥0∞) s = op ((m₂.trim : (a : Set α) → ℝ≥0∞) s) ((m₃.trim : (a : Set α) → ℝ≥0∞) s)

Tactic:
rcases exists_measurable_superset_forall_eq_trim ![m₁, m₂, m₃] s with ⟨t, _hst, _ht, htm⟩

Premises used: MeasureTheory.OuterMeasure.exists_measurable_superset_forall_eq_trim, Matrix.vecEmpty, Matrix.vecCons
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m₁ m₂ m₃ : OuterMeasure α
op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞
h : ∀ (s : Set α), (m₁ : (a : Set α) → ℝ≥0∞) s = op ((m₂ : (a : Set α) → ℝ≥0∞) s) ((m₃ : (a : Set α) → ℝ≥0∞) s)
s t : Set α
_hst : s ⊆ t
_ht : MeasurableSet t
htm :
  ∀ (i : Fin (Nat.succ 0).succ.succ),
    Eq (α := ℝ≥0∞) ((![m₁, m₂, m₃] i : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
      (((![m₁, m₂, m₃] i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((m₁ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((m₁.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((m₂ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((m₂.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((m₃ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((m₃.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∧
        ∀ (i : Fin 0),
          Eq (α := ℝ≥0∞) (((![] i : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
            (((trim (![] i) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [Fin.forall_iff_succ, Matrix.cons_val_zero, Matrix.cons_val_succ] at htm

Premises used: Matrix.cons_val_zero, Matrix.cons_val_succ, Fin.forall_iff_succ
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m₁ m₂ m₃ : OuterMeasure α
op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞
h : ∀ (s : Set α), (m₁ : (a : Set α) → ℝ≥0∞) s = op ((m₂ : (a : Set α) → ℝ≥0∞) s) ((m₃ : (a : Set α) → ℝ≥0∞) s)
s t : Set α
_hst : s ⊆ t
_ht : MeasurableSet t
htm :
  Eq (α := ℝ≥0∞) ((m₁ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((m₁.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((m₂ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((m₂.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((m₃ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((m₃.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∧
        ∀ (i : Fin 0),
          Eq (α := ℝ≥0∞) (((![] i : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
            (((trim (![] i) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw : (m₁ : (a : Set α) → ℝ≥0∞) t = op ((m₂.trim : (a : Set α) → ℝ≥0∞) s) ((m₃.trim : (a : Set α) → ℝ≥0∞) s)
rw₁ : (m₁ : (a : Set α) → ℝ≥0∞) t = op ((m₂ : (a : Set α) → ℝ≥0∞) t) ((m₃.trim : (a : Set α) → ℝ≥0∞) s)
rw₂ : (m₁ : (a : Set α) → ℝ≥0∞) t = op ((m₂ : (a : Set α) → ℝ≥0∞) t) ((m₃ : (a : Set α) → ℝ≥0∞) t)
rw₃ rw₄ :
  op ((m₂ : (a : Set α) → ℝ≥0∞) t) ((m₃ : (a : Set α) → ℝ≥0∞) t) =
    op ((m₂ : (a : Set α) → ℝ≥0∞) t) ((m₃ : (a : Set α) → ℝ≥0∞) t)
⊢ (m₁.trim : (a : Set α) → ℝ≥0∞) s = op ((m₂.trim : (a : Set α) → ℝ≥0∞) s) ((m₃.trim : (a : Set α) → ℝ≥0∞) s)

Tactic:
rw [← htm.1, ← htm.2.1, ← htm.2.2.1, h]

Premises used: And.right, And.left
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m₁ m₂ : OuterMeasure α
op : ℝ≥0∞ → ℝ≥0∞
h : ∀ (s : Set α), (m₁ : (a : Set α) → ℝ≥0∞) s = op ((m₂ : (a : Set α) → ℝ≥0∞) s)
s : Set α
⊢ (m₁.trim : (a : Set α) → ℝ≥0∞) s = op ((m₂.trim : (a : Set α) → ℝ≥0∞) s)

Tactic:
@trim_binop α _ m₁ m₂ 0 (fun a _b => op a) h s

Premises used: MeasureTheory.OuterMeasure.trim_binop
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m₁ m₂ : OuterMeasure α
⊢ (m₁ + m₂).trim = m₁.trim + m₂.trim

Tactic:
ext <| trim_binop (add_apply m₁ m₂)

Premises used: MeasureTheory.OuterMeasure.add_apply, MeasureTheory.OuterMeasure.trim_binop, MeasureTheory.OuterMeasure.ext
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
R : Type u_2
inst_1 : SMul R ℝ≥0∞
inst_2 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
m : OuterMeasure α
⊢ (c • m).trim = c • m.trim

Tactic:
ext <| trim_op (smul_apply c m)

Premises used: MeasureTheory.OuterMeasure.trim_op, MeasureTheory.OuterMeasure.ext, MeasureTheory.OuterMeasure.smul_apply
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m₁ m₂ : OuterMeasure α
⊢ (m₁ ⊔ m₂).trim = m₁.trim ⊔ m₂.trim

Tactic:
ext fun s => (trim_binop (sup_apply m₁ m₂) s).trans (sup_apply _ _ _).symm

Premises used: MeasureTheory.OuterMeasure.sup_apply, MeasureTheory.OuterMeasure.trim_binop, MeasureTheory.OuterMeasure.trim, Eq.symm, MeasureTheory.OuterMeasure.ext, Eq.trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Sort u_2
inst_1 : Countable ι
μ : ι → OuterMeasure α
simp_rw : Eq.{u_1 + 1} (α := OuterMeasure α) (trim (⨆ (i : PLift ι), μ i.down)) (⨆ (i : PLift ι), (μ i.down).trim)
⊢ Eq.{u_1 + 1} (α := OuterMeasure α) (trim (⨆ (i : ι), μ i)) (⨆ (i : ι), (μ i).trim)

Tactic:
simp_rw [← @iSup_plift_down _ ι]

Premises used: iSup_plift_down
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Sort u_2
inst_1 : Countable ι
μ : ι → OuterMeasure α
h :
  ∀ (s : Set α),
    Eq (α := ℝ≥0∞) (((trim (⨆ (i : PLift ι), μ i.down) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((⨆ (i : PLift ι), (μ i.down).trim : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := OuterMeasure α) (trim (⨆ (i : PLift ι), μ i.down)) (⨆ (i : PLift ι), (μ i.down).trim)

Tactic:
ext1 s
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Sort u_2
inst_1 : Countable ι
μ : ι → OuterMeasure α
s : Set α
h :
  ∀ (t : Set α),
    s ⊆ t →
      MeasurableSet t →
        ∀
          (hμt :
            ∀ (i : Option (PLift ι)),
              Eq (α := ℝ≥0∞)
                ((Option.elim' (⨆ (i : PLift ι), μ i.down) (μ ∘ PLift.down) i : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
                (((Option.elim' (⨆ (i : PLift ι), μ i.down) (μ ∘ PLift.down) i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
          Eq (α := ℝ≥0∞) (((trim (⨆ (i : PLift ι), μ i.down) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
            (((⨆ (i : PLift ι), (μ i.down).trim : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((trim (⨆ (i : PLift ι), μ i.down) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((⨆ (i : PLift ι), (μ i.down).trim : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

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

Premises used: Option.elim', iSup, Function.comp, MeasureTheory.OuterMeasure.exists_measurable_superset_forall_eq_trim, PLift.down
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Sort u_2
inst_1 : Countable ι
μ : ι → OuterMeasure α
s t : Set α
left : s ⊆ t
left_1 : MeasurableSet t
hμt :
  ∀ (i : Option (PLift ι)),
    Eq (α := ℝ≥0∞) ((Option.elim' (⨆ (i : PLift ι), μ i.down) (μ ∘ PLift.down) i : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
      (((Option.elim' (⨆ (i : PLift ι), μ i.down) (μ ∘ PLift.down) i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((⨆ (i : PLift ι), μ i.down : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
      (((trim (⨆ (i : PLift ι), μ i.down) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∧
    ∀ (x : PLift ι),
      Eq (α := ℝ≥0∞) (((μ ∘ PLift.down) x : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
        ((((μ ∘ PLift.down) x).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

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

Premises used: Option.elim', Option.forall
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Sort u_2
inst_1 : Countable ι
μ : ι → OuterMeasure α
s t : Set α
left : s ⊆ t
left_1 : MeasurableSet t
hμt :
  Eq (α := ℝ≥0∞) (((⨆ (i : PLift ι), μ i.down : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
      (((trim (⨆ (i : PLift ι), μ i.down) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∧
    ∀ (x : PLift ι),
      Eq (α := ℝ≥0∞) (((μ ∘ PLift.down) x : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
        ((((μ ∘ PLift.down) x).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h :
  Eq (α := ℝ≥0∞) (⨆ (i : PLift ι), (μ i.down : (a : Set α) → ℝ≥0∞) t)
    (⨆ (i : PLift ι), ((μ i.down).trim : (a : Set α) → ℝ≥0∞) s)
⊢ Eq (α := ℝ≥0∞) (((trim (⨆ (i : PLift ι), μ i.down) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((⨆ (i : PLift ι), (μ i.down).trim : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

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

Premises used: And.left, MeasureTheory.OuterMeasure.iSup_apply
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Sort u_2
inst_1 : Countable ι
μ : ι → OuterMeasure α
s t : Set α
left : s ⊆ t
left_1 : MeasurableSet t
hμt :
  Eq (α := ℝ≥0∞) (((⨆ (i : PLift ι), μ i.down : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
      (((trim (⨆ (i : PLift ι), μ i.down) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∧
    ∀ (x : PLift ι),
      Eq (α := ℝ≥0∞) (((μ ∘ PLift.down) x : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
        ((((μ ∘ PLift.down) x).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (⨆ (i : PLift ι), (μ i.down : (a : Set α) → ℝ≥0∞) t)
    (⨆ (i : PLift ι), ((μ i.down).trim : (a : Set α) → ℝ≥0∞) s)

Tactic:
iSup_congr hμt.2

Premises used: And.right, iSup_congr
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Sort u_2
inst_1 : Countable ι
μ : ι → OuterMeasure α
s t : Set α
left : s ⊆ t
left_1 : MeasurableSet t
hμt :
  Eq (α := ℝ≥0∞) (((⨆ (i : PLift ι), μ i.down : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
      (((trim (⨆ (i : PLift ι), μ i.down) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∧
    ∀ (x : PLift ι),
      Eq (α := ℝ≥0∞) (((μ ∘ PLift.down) x : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
        ((((μ ∘ PLift.down) x).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (⨆ (i : PLift ι), (μ i.down : (a : Set α) → ℝ≥0∞) t)
    (⨆ (i : PLift ι), ((μ i.down).trim : (a : Set α) → ℝ≥0∞) s)

Tactic:
exact iSup_congr hμt.2

Premises used: And.right, iSup_congr
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
⊢ Eq.{u_1 + 1} (α := OuterMeasure α) (trim ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ))
    ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.trim)

Tactic:
le_antisymm (fun t => ?_) (le_trim_iff.2 fun t ht => ?_)

Premises used: Iff.mpr, le_antisymm, MeasureTheory.OuterMeasure.le_trim_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
refine_1 :
  ∀ (t : Set α),
    LE.le (α := ℝ≥0∞)
      (((trim ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
      ((((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.trim : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
refine_2 :
  ∀ (t : Set α) (ht : MeasurableSet t),
    LE.le (α := ℝ≥0∞)
      ((((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.trim : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
      ((((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := OuterMeasure α) (trim ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ))
    ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.trim)

Tactic:
refine le_antisymm (fun t => ?_) (le_trim_iff.2 fun t ht => ?_)

Premises used: Iff.mpr, le_antisymm, MeasureTheory.OuterMeasure.le_trim_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
refine_1 :
  LE.le (α := ℝ≥0∞)
    (((trim ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ.trim : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    (((trim ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.trim : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [restrict_apply]

Premises used: MeasureTheory.OuterMeasure.restrict_apply
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
refine_1 :
  ∀ (t' : Set α) (htt' : t ∩ s ⊆ t') (ht' : MeasurableSet t')
    (hμt' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞) ((μ.trim : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞)
      (((trim ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
      ((μ.trim : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    (((trim ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ.trim : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
rcases μ.exists_measurable_superset_eq_trim (t ∩ s) with ⟨t', htt', ht', hμt'⟩

Premises used: Inter.inter, MeasureTheory.OuterMeasure.exists_measurable_superset_eq_trim
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ∩ s ⊆ t'
ht' : MeasurableSet t'
hμt' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞) ((μ.trim : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
refine_1 :
  LE.le (α := ℝ≥0∞)
    (((trim ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    (((trim ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ.trim : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
rw [← hμt']
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ∩ s ⊆ t'
ht' : MeasurableSet t'
hμt' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞) ((μ.trim : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ t ⊆ sᶜ ∪ t'

Tactic:
rw [inter_subset] at htt'

Premises used: Set.inter_subset
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ∩ s ⊆ t'
ht' : MeasurableSet t'
hμt' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞) ((μ.trim : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
htt'₁ : t ⊆ sᶜ ∪ t'
⊢ MeasurableSet t'

Tactic:
rw [inter_subset] at htt'

Premises used: Set.inter_subset