awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Sort u_2
inst_1 : Countable ι
μ : ι → OuterMeasure α
s : Set α
⊢ ∃ (t : Set α),
    s ⊆ t ∧
      MeasurableSet t ∧
        ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (((μ i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
Tactic: choose t hst ht hμt using fun i => (μ i).exists_measurable_superset_eq_trim s
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (hypothesis)
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∞)
⊢ ∃ (t : Set α),
    s ⊆ t ∧
      MeasurableSet t ∧
        ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (((μ i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have hst₁ : s ⊆ ⋂ (i : ι), t i
Tactic: replace hst := subset_iInter hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (hypothesis)
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
⊢ ∃ (t : Set α),
    s ⊆ t ∧
      MeasurableSet t ∧
        ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (((μ i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have ht₁ : MeasurableSet.{u_1} (α := α) (⋂ (b : ι), t b)
Tactic: replace ht := MeasurableSet.iInter ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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∞)
have refine_1 : ∀ (i : ι),
  LE.le (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), t i) : ℝ≥0∞) (((μ i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine ⟨⋂ i, t i, hst, ht, fun i => le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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∞)
⊢ ∃ (t : Set α),
    s ⊆ t ∧
      MeasurableSet t ∧
        ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (((μ i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have refine_2 : ∀ (i : ι),
  LE.le (α := ℝ≥0∞) (((μ i).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), t i) : ℝ≥0∞)
Tactic: refine ⟨⋂ i, t i, hst, ht, fun i => le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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 α
⊢ (m₁.trim : (a : Set α) → ℝ≥0∞) s = op ((m₂.trim : (a : Set α) → ℝ≥0∞) s) ((m₃.trim : (a : Set α) → ℝ≥0∞) s)
have 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)
Tactic: rcases exists_measurable_superset_forall_eq_trim ![m₁, m₂, m₃] s with ⟨t, _hst, _ht, htm⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (hypothesis)
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∞)
⊢ (m₁.trim : (a : Set α) → ℝ≥0∞) s = op ((m₂.trim : (a : Set α) → ℝ≥0∞) s) ((m₃.trim : (a : Set α) → ℝ≥0∞) s)
have 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∞)
Tactic: simp only [Fin.forall_iff_succ, Matrix.cons_val_zero, Matrix.cons_val_succ] at htm
Cleared hypotheses: htm
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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∞)
⊢ (m₁.trim : (a : Set α) → ℝ≥0∞) s = op ((m₂.trim : (a : Set α) → ℝ≥0∞) s) ((m₃.trim : (a : Set α) → ℝ≥0∞) s)
have rw : (m₁ : (a : Set α) → ℝ≥0∞) t = 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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)
⊢ (m₁.trim : (a : Set α) → ℝ≥0∞) s = op ((m₂.trim : (a : Set α) → ℝ≥0∞) s) ((m₃.trim : (a : Set α) → ℝ≥0∞) s)
have rw₁ : (m₁ : (a : Set α) → ℝ≥0∞) t = op ((m₂ : (a : Set α) → ℝ≥0∞) t) ((m₃.trim : (a : Set α) → ℝ≥0∞) s)
Tactic: rw [← htm.1, ← htm.2.1, ← htm.2.2.1, h]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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)
⊢ (m₁.trim : (a : Set α) → ℝ≥0∞) s = op ((m₂.trim : (a : Set α) → ℝ≥0∞) s) ((m₃.trim : (a : Set α) → ℝ≥0∞) s)
have rw₂ : (m₁ : (a : Set α) → ℝ≥0∞) t = op ((m₂ : (a : Set α) → ℝ≥0∞) t) ((m₃ : (a : Set α) → ℝ≥0∞) t)
Tactic: rw [← htm.1, ← htm.2.1, ← htm.2.2.1, h]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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)
⊢ (m₁.trim : (a : Set α) → ℝ≥0∞) s = op ((m₂.trim : (a : Set α) → ℝ≥0∞) s) ((m₃.trim : (a : Set α) → ℝ≥0∞) s)
have rw₃ : op ((m₂ : (a : Set α) → ℝ≥0∞) t) ((m₃ : (a : Set α) → ℝ≥0∞) t) =
  op ((m₂ : (a : Set α) → ℝ≥0∞) t) ((m₃ : (a : Set α) → ℝ≥0∞) t)
Tactic: rw [← htm.1, ← htm.2.1, ← htm.2.2.1, h]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Sort u_2
inst_1 : Countable ι
μ : ι → OuterMeasure α
⊢ Eq.{u_1 + 1} (α := OuterMeasure α) (trim (⨆ (i : ι), μ i)) (⨆ (i : ι), (μ i).trim)
have simp_rw : Eq.{u_1 + 1} (α := OuterMeasure α) (trim (⨆ (i : PLift ι), μ i.down)) (⨆ (i : PLift ι), (μ i.down).trim)
Tactic: simp_rw [← @iSup_plift_down _ ι]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Sort u_2
inst_1 : Countable ι
μ : ι → OuterMeasure α
⊢ Eq.{u_1 + 1} (α := OuterMeasure α) (trim (⨆ (i : PLift ι), μ i.down)) (⨆ (i : PLift ι), (μ i.down).trim)
have 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∞)
Tactic: ext1 s
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Sort u_2
inst_1 : Countable ι
μ : ι → OuterMeasure α
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∞)
have 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∞)
Tactic: obtain ⟨t, _, _, hμt⟩ :=
    exists_measurable_superset_forall_eq_trim
      (Option.elim' (⨆ i, μ (PLift.down i)) (μ ∘ PLift.down)) s
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (hypothesis)
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∞) (((trim (⨆ (i : PLift ι), μ i.down) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((⨆ (i : PLift ι), (μ i.down).trim : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
Tactic: simp only [Option.forall, Option.elim'] at hμt
Cleared hypotheses: hμt
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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∞) (((trim (⨆ (i : PLift ι), μ i.down) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((⨆ (i : PLift ι), (μ i.down).trim : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (⨆ (i : PLift ι), (μ i.down : (a : Set α) → ℝ≥0∞) t)
  (⨆ (i : PLift ι), ((μ i.down).trim : (a : Set α) → ℝ≥0∞) s)
Tactic: simp only [iSup_apply, ← hμt.1]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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)
have 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∞)
Tactic: refine le_antisymm (fun t => ?_) (le_trim_iff.2 fun t ht => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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∞)
⊢ Eq.{u_1 + 1} (α := OuterMeasure α) (trim ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ))
    ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.trim)
have 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∞)
Tactic: refine le_antisymm (fun t => ?_) (le_trim_iff.2 fun t ht => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
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∞)
have refine_1 : LE.le (α := ℝ≥0∞)
  (((trim ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
  ((μ.trim : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [restrict_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ LE.le (α := ℝ≥0∞)
    (((trim ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ.trim : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have 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∞)
Tactic: rcases μ.exists_measurable_superset_eq_trim (t ∩ s) with ⟨t', htt', ht', hμt'⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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∞)
⊢ LE.le (α := ℝ≥0∞)
    (((trim ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ.trim : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have refine_1 : LE.le (α := ℝ≥0∞)
  (((trim ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞)
Tactic: rw [← hμt']
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (hypothesis)
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∞)
⊢ LE.le (α := ℝ≥0∞)
    (((trim ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞)
have htt'₁ : t ⊆ sᶜ ∪ t'
Tactic: rw [inter_subset] at htt'
Cleared hypotheses: htt', ht', hμt'
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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∞)
⊢ LE.le (α := ℝ≥0∞)
    (((trim ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞)
have refine_1 : LE.le (α := ℝ≥0∞)
  (((trim ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (sᶜ ∪ t') :
    ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞)
Tactic: refine (measure_mono htt').trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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∞)
⊢ LE.le (α := ℝ≥0∞)
    (((trim ((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (sᶜ ∪ t') :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞)
have refine_1 : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t' : ℝ≥0∞)
Tactic: rw [trim_eq _ (hs.compl.union ht'), restrict_apply, union_inter_distrib_right, compl_inter_self,
      Set.empty_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
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∞)
have refine_2 : LE.le (α := ℝ≥0∞) ((μ.trim : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
  ((((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [restrict_apply, trim_eq _ (ht.inter hs), restrict_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
refine_2 :
  LE.le (α := ℝ≥0∞) ((μ.trim : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    ((((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ 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∞)
have refine_2₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
  ((((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [restrict_apply, trim_eq _ (ht.inter hs), restrict_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
refine_2 :
  LE.le (α := ℝ≥0∞) ((μ.trim : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    ((((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
refine_2₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    ((((restrict s : (a : OuterMeasure α) → OuterMeasure α) μ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ 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∞)
have refine_2₂ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [restrict_apply, trim_eq _ (ht.inter hs), restrict_apply]