awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : MeasurableSet s
⊢ (μ.restrict s).toOuterMeasure = (OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure
have simp_rw : Eq.{u_2 + 1} (α := OuterMeasure α) (toOuterMeasure ((restrictₗ s : (a : Measure α) → Measure α) μ))
  ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
Tactic: simp_rw [restrict, restrictₗ, liftLinear, LinearMap.coe_mk, AddHom.coe_mk,
    toMeasure_toOuterMeasure, OuterMeasure.restrict_trim h, μ.trimmed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : MeasurableSet s
simp_rw :
  Eq.{u_2 + 1} (α := OuterMeasure α) (toOuterMeasure ((restrictₗ s : (a : Measure α) → Measure α) μ))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
⊢ (μ.restrict s).toOuterMeasure = (OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure
have simp_rw₁ : Eq.{u_2 + 1} (α := OuterMeasure α)
  (toOuterMeasure ((liftLinear (OuterMeasure.restrict s) sorry : (a : Measure α) → Measure α) μ))
  ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
Tactic: simp_rw [restrict, restrictₗ, liftLinear, LinearMap.coe_mk, AddHom.coe_mk,
    toMeasure_toOuterMeasure, OuterMeasure.restrict_trim h, μ.trimmed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : MeasurableSet s
simp_rw :
  Eq.{u_2 + 1} (α := OuterMeasure α) (toOuterMeasure ((restrictₗ s : (a : Measure α) → Measure α) μ))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
simp_rw₁ :
  Eq.{u_2 + 1} (α := OuterMeasure α)
    (toOuterMeasure ((liftLinear (OuterMeasure.restrict s) ⋯ : (a : Measure α) → Measure α) μ))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
⊢ (μ.restrict s).toOuterMeasure = (OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure
have simp_rw₂ : Eq.{u_2 + 1} (α := OuterMeasure α)
  (toOuterMeasure
    (({
          toFun := fun (μ : Measure α) ↦
            OuterMeasure.toMeasure ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
              sorry,
          map_add' := sorry, map_smul' := sorry } :
        (a : Measure α) → Measure α)
      μ))
  ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
Tactic: simp_rw [restrict, restrictₗ, liftLinear, LinearMap.coe_mk, AddHom.coe_mk,
    toMeasure_toOuterMeasure, OuterMeasure.restrict_trim h, μ.trimmed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : MeasurableSet s
simp_rw :
  Eq.{u_2 + 1} (α := OuterMeasure α) (toOuterMeasure ((restrictₗ s : (a : Measure α) → Measure α) μ))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
simp_rw₁ :
  Eq.{u_2 + 1} (α := OuterMeasure α)
    (toOuterMeasure ((liftLinear (OuterMeasure.restrict s) ⋯ : (a : Measure α) → Measure α) μ))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
simp_rw₂ :
  Eq.{u_2 + 1} (α := OuterMeasure α)
    (toOuterMeasure
      (({
            toFun := fun (μ : Measure α) ↦
              OuterMeasure.toMeasure
                ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure) ⋯,
            map_add' := ⋯, map_smul' := ⋯ } :
          (a : Measure α) → Measure α)
        μ))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
⊢ (μ.restrict s).toOuterMeasure = (OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure
have simp_rw₃ : Eq.{u_2 + 1} (α := OuterMeasure α)
  (toOuterMeasure
    (({
          toFun := fun (μ : Measure α) ↦
            OuterMeasure.toMeasure ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
              sorry,
          map_add' := sorry } :
        (a : Measure α) → Measure α)
      μ))
  ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
Tactic: simp_rw [restrict, restrictₗ, liftLinear, LinearMap.coe_mk, AddHom.coe_mk,
    toMeasure_toOuterMeasure, OuterMeasure.restrict_trim h, μ.trimmed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : MeasurableSet s
simp_rw :
  Eq.{u_2 + 1} (α := OuterMeasure α) (toOuterMeasure ((restrictₗ s : (a : Measure α) → Measure α) μ))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
simp_rw₁ :
  Eq.{u_2 + 1} (α := OuterMeasure α)
    (toOuterMeasure ((liftLinear (OuterMeasure.restrict s) ⋯ : (a : Measure α) → Measure α) μ))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
simp_rw₂ :
  Eq.{u_2 + 1} (α := OuterMeasure α)
    (toOuterMeasure
      (({
            toFun := fun (μ : Measure α) ↦
              OuterMeasure.toMeasure
                ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure) ⋯,
            map_add' := ⋯, map_smul' := ⋯ } :
          (a : Measure α) → Measure α)
        μ))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
simp_rw₃ :
  Eq.{u_2 + 1} (α := OuterMeasure α)
    (toOuterMeasure
      (({
            toFun := fun (μ : Measure α) ↦
              OuterMeasure.toMeasure
                ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure) ⋯,
            map_add' := ⋯ } :
          (a : Measure α) → Measure α)
        μ))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
⊢ (μ.restrict s).toOuterMeasure = (OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure
have simp_rw₄ : Eq.{u_2 + 1} (α := OuterMeasure α)
  (toOuterMeasure
    (OuterMeasure.toMeasure ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure) sorry))
  ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
Tactic: simp_rw [restrict, restrictₗ, liftLinear, LinearMap.coe_mk, AddHom.coe_mk,
    toMeasure_toOuterMeasure, OuterMeasure.restrict_trim h, μ.trimmed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : MeasurableSet s
simp_rw :
  Eq.{u_2 + 1} (α := OuterMeasure α) (toOuterMeasure ((restrictₗ s : (a : Measure α) → Measure α) μ))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
simp_rw₁ :
  Eq.{u_2 + 1} (α := OuterMeasure α)
    (toOuterMeasure ((liftLinear (OuterMeasure.restrict s) ⋯ : (a : Measure α) → Measure α) μ))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
simp_rw₂ :
  Eq.{u_2 + 1} (α := OuterMeasure α)
    (toOuterMeasure
      (({
            toFun := fun (μ : Measure α) ↦
              OuterMeasure.toMeasure
                ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure) ⋯,
            map_add' := ⋯, map_smul' := ⋯ } :
          (a : Measure α) → Measure α)
        μ))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
simp_rw₃ :
  Eq.{u_2 + 1} (α := OuterMeasure α)
    (toOuterMeasure
      (({
            toFun := fun (μ : Measure α) ↦
              OuterMeasure.toMeasure
                ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure) ⋯,
            map_add' := ⋯ } :
          (a : Measure α) → Measure α)
        μ))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
simp_rw₄ :
  Eq.{u_2 + 1} (α := OuterMeasure α)
    (toOuterMeasure
      (OuterMeasure.toMeasure ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure) ⋯))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
⊢ (μ.restrict s).toOuterMeasure = (OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure
have simp_rw₅ : Eq.{u_2 + 1} (α := OuterMeasure α)
  (OuterMeasure.trim ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure))
  ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
Tactic: simp_rw [restrict, restrictₗ, liftLinear, LinearMap.coe_mk, AddHom.coe_mk,
    toMeasure_toOuterMeasure, OuterMeasure.restrict_trim h, μ.trimmed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : MeasurableSet s
simp_rw :
  Eq.{u_2 + 1} (α := OuterMeasure α) (toOuterMeasure ((restrictₗ s : (a : Measure α) → Measure α) μ))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
simp_rw₁ :
  Eq.{u_2 + 1} (α := OuterMeasure α)
    (toOuterMeasure ((liftLinear (OuterMeasure.restrict s) ⋯ : (a : Measure α) → Measure α) μ))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
simp_rw₂ :
  Eq.{u_2 + 1} (α := OuterMeasure α)
    (toOuterMeasure
      (({
            toFun := fun (μ : Measure α) ↦
              OuterMeasure.toMeasure
                ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure) ⋯,
            map_add' := ⋯, map_smul' := ⋯ } :
          (a : Measure α) → Measure α)
        μ))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
simp_rw₃ :
  Eq.{u_2 + 1} (α := OuterMeasure α)
    (toOuterMeasure
      (({
            toFun := fun (μ : Measure α) ↦
              OuterMeasure.toMeasure
                ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure) ⋯,
            map_add' := ⋯ } :
          (a : Measure α) → Measure α)
        μ))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
simp_rw₄ :
  Eq.{u_2 + 1} (α := OuterMeasure α)
    (toOuterMeasure
      (OuterMeasure.toMeasure ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure) ⋯))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
simp_rw₅ :
  Eq.{u_2 + 1} (α := OuterMeasure α)
    (OuterMeasure.trim ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure))
    ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure)
⊢ (μ.restrict s).toOuterMeasure = (OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure
have simp_rw₆ : Eq (α := OuterMeasure α) ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.trim : OuterMeasure α)
  ((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α)
Tactic: simp_rw [restrict, restrictₗ, liftLinear, LinearMap.coe_mk, AddHom.coe_mk,
    toMeasure_toOuterMeasure, OuterMeasure.restrict_trim h, μ.trimmed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (hypothesis)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t (μ.restrict s)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have ht₁ : NullMeasurableSet t ((liftLinear (OuterMeasure.restrict s) sorry : (a : Measure α) → Measure α) μ)
Tactic: rw [restrict, restrictₗ] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t ((liftLinear (OuterMeasure.restrict s) ⋯ : (a : Measure α) → Measure α) μ)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((((restrictₗ s : (a : Measure α) → Measure α) μ : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [← restrictₗ_apply, restrictₗ, liftLinear_apply₀ _ ht, OuterMeasure.restrict_apply,
    coe_toOuterMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t ((liftLinear (OuterMeasure.restrict s) ⋯ : (a : Measure α) → Measure α) μ)
rw :
  Eq (α := ℝ≥0∞) ((((restrictₗ s : (a : Measure α) → Measure α) μ : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞)
  ((((liftLinear (OuterMeasure.restrict s) sorry : (a : Measure α) → Measure α) μ : Measure α) : (a : Set α) → ℝ≥0∞) t :
    ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [← restrictₗ_apply, restrictₗ, liftLinear_apply₀ _ ht, OuterMeasure.restrict_apply,
    coe_toOuterMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t ((liftLinear (OuterMeasure.restrict s) ⋯ : (a : Measure α) → Measure α) μ)
rw :
  Eq (α := ℝ≥0∞) ((((restrictₗ s : (a : Measure α) → Measure α) μ : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    ((((liftLinear (OuterMeasure.restrict s) ⋯ : (a : Measure α) → Measure α) μ : Measure α) : (a : Set α) → ℝ≥0∞) t :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞)
  ((((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
        (a : Set α) → ℝ≥0∞)
      t :
    ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [← restrictₗ_apply, restrictₗ, liftLinear_apply₀ _ ht, OuterMeasure.restrict_apply,
    coe_toOuterMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t ((liftLinear (OuterMeasure.restrict s) ⋯ : (a : Measure α) → Measure α) μ)
rw :
  Eq (α := ℝ≥0∞) ((((restrictₗ s : (a : Measure α) → Measure α) μ : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    ((((liftLinear (OuterMeasure.restrict s) ⋯ : (a : Measure α) → Measure α) μ : Measure α) : (a : Set α) → ℝ≥0∞) t :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞)
    ((((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞) ((μ.toOuterMeasure : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [← restrictₗ_apply, restrictₗ, liftLinear_apply₀ _ ht, OuterMeasure.restrict_apply,
    coe_toOuterMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t ((liftLinear (OuterMeasure.restrict s) ⋯ : (a : Measure α) → Measure α) μ)
rw :
  Eq (α := ℝ≥0∞) ((((restrictₗ s : (a : Measure α) → Measure α) μ : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    ((((liftLinear (OuterMeasure.restrict s) ⋯ : (a : Measure α) → Measure α) μ : Measure α) : (a : Set α) → ℝ≥0∞) t :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞)
    ((((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₃ : Eq (α := ℝ≥0∞) ((μ.toOuterMeasure : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have rw₄ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [← restrictₗ_apply, restrictₗ, liftLinear_apply₀ _ ht, OuterMeasure.restrict_apply,
    coe_toOuterMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((μ.restrict s).toOuterMeasure : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [← toOuterMeasure_apply,
    Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict hs,
    OuterMeasure.restrict_apply s t _, toOuterMeasure_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) (((μ.restrict s).toOuterMeasure : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞)
  ((((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
        (a : Set α) → ℝ≥0∞)
      t :
    ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [← toOuterMeasure_apply,
    Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict hs,
    OuterMeasure.restrict_apply s t _, toOuterMeasure_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) (((μ.restrict s).toOuterMeasure : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    ((((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ.toOuterMeasure : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [← toOuterMeasure_apply,
    Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict hs,
    OuterMeasure.restrict_apply s t _, toOuterMeasure_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) (((μ.restrict s).toOuterMeasure : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    ((((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₂ : Eq (α := ℝ≥0∞) ((μ.toOuterMeasure : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [← toOuterMeasure_apply,
    Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict hs,
    OuterMeasure.restrict_apply s t _, toOuterMeasure_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
hC : IsCountablySpanning C
ht : ∀ t ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have obtain : ∀ (t : ℕ → Set α) (ht1 : ∀ (n : ℕ), t n ∈ C) (ht2 : Eq.{u_2 + 1} (α := Set α) (⋃ (n : ℕ), t n) univ),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: obtain ⟨t, ht1, ht2⟩ := hC
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
ht : ∀ t ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
t : ℕ → Set α
ht1 : ∀ (n : ℕ), t n ∈ C
ht2 : Eq.{u_2 + 1} (α := Set α) (⋃ (n : ℕ), t n) univ
⊢ s = ⋃ (n : ℕ), s ∩ t n
have rw : s = s ∩ ⋃ (i : ℕ), t i
Tactic: rw [← inter_iUnion, ht2, inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
ht : ∀ t ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
t : ℕ → Set α
ht1 : ∀ (n : ℕ), t n ∈ C
ht2 : Eq.{u_2 + 1} (α := Set α) (⋃ (n : ℕ), t n) univ
rw : s = s ∩ ⋃ (i : ℕ), t i
⊢ s = ⋃ (n : ℕ), s ∩ t n
have rw₁ : s = s ∩ univ
Tactic: rw [← inter_iUnion, ht2, inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
ht : ∀ t ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
t : ℕ → Set α
ht1 : ∀ (n : ℕ), t n ∈ C
ht2 : Eq.{u_2 + 1} (α := Set α) (⋃ (n : ℕ), t n) univ
rw : s = s ∩ ⋃ (i : ℕ), t i
rw₁ : s = s ∩ univ
⊢ s = ⋃ (n : ℕ), s ∩ t n
have rw₂ : s = s
Tactic: rw [← inter_iUnion, ht2, inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
ht : ∀ t ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
t : ℕ → Set α
ht1 : ∀ (n : ℕ), t n ∈ C
ht2 : Eq.{u_2 + 1} (α := Set α) (⋃ (n : ℕ), t n) univ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : ∀ (i : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t i) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [show s = ⋃ n, s ∩ t n by rw [← inter_iUnion, ht2, inter_univ], measure_iUnion_null_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
hC : IsCountablySpanning C
hm : C ⊆ MeasurableSet
ht : ∀ t ∈ C, Eq (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : ∀ t ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← forall_measure_inter_isCountablySpanning_eq_zero hC]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ.restrict (toMeasurable μ s) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [← restrict_congr_set hs.toMeasurable_ae_eq,
    restrict_apply' (measurableSet_toMeasurable _ _),
    measure_congr ((ae_eq_refl t).inter hs.toMeasurable_ae_eq)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
rw :
  Eq (α := ℝ≥0∞) ((μ.restrict (toMeasurable μ s) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ toMeasurable μ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [← restrict_congr_set hs.toMeasurable_ae_eq,
    restrict_apply' (measurableSet_toMeasurable _ _),
    measure_congr ((ae_eq_refl t).inter hs.toMeasurable_ae_eq)]