awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
t : Set β
ht : 0 ∉ t
rw : s.indicator f ⁻¹' t ∈ ae μ ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ t ∈ Filter.map (s.indicator f) (ae μ) ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s.indicator f ⁻¹' t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: classical
  rw [mem_map, mem_ae_iff, Set.indicator_preimage, Set.ite, Set.compl_union, Set.compl_inter]
  change μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun _ => (0 : β)) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0
  simp only [ht, if_false, Set.compl_empty, Set.empty_diff, Set.inter_univ, Set.preimage_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
t : Set β
ht : 0 ∉ t
rw : s.indicator f ⁻¹' t ∈ ae μ ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s.indicator f ⁻¹' t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ t ∈ Filter.map (s.indicator f) (ae μ) ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s.ite (f ⁻¹' t) (0 ⁻¹' t))ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: classical
  rw [mem_map, mem_ae_iff, Set.indicator_preimage, Set.ite, Set.compl_union, Set.compl_inter]
  change μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun _ => (0 : β)) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0
  simp only [ht, if_false, Set.compl_empty, Set.empty_diff, Set.inter_univ, Set.preimage_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
t : Set β
ht : 0 ∉ t
rw : s.indicator f ⁻¹' t ∈ ae μ ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s.indicator f ⁻¹' t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s.ite (f ⁻¹' t) (0 ⁻¹' t))ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ t ∈ Filter.map (s.indicator f) (ae μ) ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s ∪ 0 ⁻¹' t \ s)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: classical
  rw [mem_map, mem_ae_iff, Set.indicator_preimage, Set.ite, Set.compl_union, Set.compl_inter]
  change μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun _ => (0 : β)) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0
  simp only [ht, if_false, Set.compl_empty, Set.empty_diff, Set.inter_univ, Set.preimage_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
t : Set β
ht : 0 ∉ t
rw : s.indicator f ⁻¹' t ∈ ae μ ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s.indicator f ⁻¹' t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s.ite (f ⁻¹' t) (0 ⁻¹' t))ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₃ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s ∪ 0 ⁻¹' t \ s)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ t ∈ Filter.map (s.indicator f) (ae μ) ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₄ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t ∩ s)ᶜ ∩ (0 ⁻¹' t \ s)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: classical
  rw [mem_map, mem_ae_iff, Set.indicator_preimage, Set.ite, Set.compl_union, Set.compl_inter]
  change μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun _ => (0 : β)) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0
  simp only [ht, if_false, Set.compl_empty, Set.empty_diff, Set.inter_univ, Set.preimage_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
t : Set β
ht : 0 ∉ t
rw : s.indicator f ⁻¹' t ∈ ae μ ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s.indicator f ⁻¹' t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s.ite (f ⁻¹' t) (0 ⁻¹' t))ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₃ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s ∪ 0 ⁻¹' t \ s)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₄ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t ∩ s)ᶜ ∩ (0 ⁻¹' t \ s)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ t ∈ Filter.map (s.indicator f) (ae μ) ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ (0 ⁻¹' t \ s)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: classical
  rw [mem_map, mem_ae_iff, Set.indicator_preimage, Set.ite, Set.compl_union, Set.compl_inter]
  change μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun _ => (0 : β)) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0
  simp only [ht, if_false, Set.compl_empty, Set.empty_diff, Set.inter_univ, Set.preimage_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
t : Set β
ht : 0 ∉ t
rw : s.indicator f ⁻¹' t ∈ ae μ ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s.indicator f ⁻¹' t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s.ite (f ⁻¹' t) (0 ⁻¹' t))ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₃ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s ∪ 0 ⁻¹' t \ s)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₄ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t ∩ s)ᶜ ∩ (0 ⁻¹' t \ s)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₅ rw₆ rw₇ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ (0 ⁻¹' t \ s)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ t ∈ Filter.map (s.indicator f) (ae μ) ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₈ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun (x : α) ↦ 0) ⁻¹' t \ s)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: classical
  rw [mem_map, mem_ae_iff, Set.indicator_preimage, Set.ite, Set.compl_union, Set.compl_inter]
  change μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun _ => (0 : β)) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0
  simp only [ht, if_false, Set.compl_empty, Set.empty_diff, Set.inter_univ, Set.preimage_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
hs : MeasurableSet s
t : Set β
⊢ t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))
have pos : ∀ (ht : 0 ∈ t), t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))
Tactic: by_cases ht : (0 : β) ∈ t
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
hs : MeasurableSet s
t : Set β
pos : ∀ (ht : 0 ∈ t), t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))
⊢ t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))
have neg : ∀ (ht : 0 ∉ t), t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))
Tactic: by_cases ht : (0 : β) ∈ t
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∈ t
⊢ t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))
have pos : t ∈ Filter.map f (ae (μ.restrict s)) → t ∈ Filter.map f (ae (μ.restrict s))
Tactic: rw [mem_map_indicator_ae_iff_mem_map_restrict_ae_of_zero_mem ht hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∉ t
⊢ t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))
have neg : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞) →
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [mem_map_indicator_ae_iff_of_zero_notMem ht, mem_map_restrict_ae_iff hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
⊢ s.indicator f =ᶠ[ae μ] f
have hf₁ : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → f x = 0 x
Tactic: rw [Filter.EventuallyEq, ae_restrict_iff' hs.compl] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → f x = 0 x
⊢ s.indicator f =ᶠ[ae μ] f
have h : ∀ (x : α) (hx : x ∈ sᶜ → f x = 0 x), s.indicator f x = f x
Tactic: filter_upwards [hf] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → f x = 0 x
x : α
hx : x ∈ sᶜ → f x = 0 x
⊢ s.indicator f x = f x
have pos : ∀ (hxs : x ∈ s), s.indicator f x = f x
Tactic: by_cases hxs : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → f x = 0 x
x : α
hx : x ∈ sᶜ → f x = 0 x
pos : ∀ (hxs : x ∈ s), s.indicator f x = f x
⊢ s.indicator f x = f x
have neg : ∀ (hxs : x ∉ s), s.indicator f x = f x
Tactic: by_cases hxs : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
⊢ s.indicator f =ᶠ[ae μ] 0
have hf₁ : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0 x
Tactic: rw [Filter.EventuallyEq, ae_restrict_iff' hs] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0 x
⊢ s.indicator f =ᶠ[ae μ] 0
have h : ∀ (x : α) (hx : x ∈ s → f x = 0 x), s.indicator f x = 0 x
Tactic: filter_upwards [hf] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0 x
x : α
hx : x ∈ s → f x = 0 x
⊢ s.indicator f x = 0 x
have pos : ∀ (hxs : x ∈ s), s.indicator f x = 0 x
Tactic: by_cases hxs : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0 x
x : α
hx : x ∈ s → f x = 0 x
pos : ∀ (hxs : x ∈ s), s.indicator f x = 0 x
⊢ s.indicator f x = 0 x
have neg : ∀ (hxs : x ∉ s), s.indicator f x = 0 x
Tactic: by_cases hxs : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
g : α → β
hs : MeasurableSet s
⊢ f =ᶠ[ae (μ.restrict s)] g ↔ s.indicator f =ᶠ[ae μ] s.indicator g
have rw : (∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) ↔ s.indicator f =ᶠ[ae μ] s.indicator g
Tactic: rw [Filter.EventuallyEq, ae_restrict_iff' hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
g : α → β
hs : MeasurableSet s
⊢ (∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) ↔ s.indicator f =ᶠ[ae μ] s.indicator g
have refine_1 : ∀ (h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x), s.indicator f =ᶠ[ae μ] s.indicator g
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
g : α → β
hs : MeasurableSet s
refine_1 : ∀ (h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x), s.indicator f =ᶠ[ae μ] s.indicator g
⊢ (∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) ↔ s.indicator f =ᶠ[ae μ] s.indicator g
have refine_2 : ∀ (h : s.indicator f =ᶠ[ae μ] s.indicator g), ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
g : α → β
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ s.indicator f =ᶠ[ae μ] s.indicator g
have h₁ : ∀ (x : α) (hx : x ∈ s → f x = g x), s.indicator f x = s.indicator g x
Tactic: filter_upwards [h] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
g : α → β
hs : MeasurableSet s
h : s.indicator f =ᶠ[ae μ] s.indicator g
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
have h₁ : ∀ (x : α) (hx : s.indicator f x = s.indicator g x), x ∈ s → f x = g x
Tactic: filter_upwards [h] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
g : α → β
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
x : α
hx : x ∈ s → f x = g x
⊢ s.indicator f x = s.indicator g x
have pos : ∀ (hxs : x ∈ s), s.indicator f x = s.indicator g x
Tactic: by_cases hxs : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
g : α → β
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
x : α
hx : x ∈ s → f x = g x
pos : ∀ (hxs : x ∈ s), s.indicator f x = s.indicator g x
⊢ s.indicator f x = s.indicator g x
have neg : ∀ (hxs : x ∉ s), s.indicator f x = s.indicator g x
Tactic: by_cases hxs : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
x : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), encard.{u_6} (α := ι) {i : ι | y ∈ s i} ≤ (↑M : ℕ∞)
⊢ (sum fun (i : ι) ↦ μ.restrict (s i)) ≤ M • μ.restrict (⋃ (i : ι), s i)
have refine : ∀ (t : Set α) (ht : MeasurableSet t),
  LE.le (α := ℝ≥0∞) (∑' (i : ι), (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((M • μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: refine le_iff.mpr (fun t ht ↦ le_of_eq_of_le (sum_apply _ ht) ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
x : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), encard.{u_6} (α := ι) {i : ι | y ∈ s i} ≤ (↑M : ℕ∞)
t : Set α
ht : MeasurableSet t
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ι), (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((M • μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have refine : ∀ (F : Finset ι),
  LE.le (α := ℝ≥0∞) (∑ i ∈ F, (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((M • μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: refine ENNReal.summable.tsum_le_of_sum_le (fun F ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (hypothesis)
Goal:
α : Type u_2
ι : Type u_6
x : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), encard.{u_6} (α := ι) {i : ι | y ∈ s i} ≤ (↑M : ℕ∞)
t : Set α
ht : MeasurableSet t
F : Finset ι
P : (C : Finset ι) → Set α := fun (C : Finset ι) ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : (i : ι) → Set (Finset ι) := fun (i : ι) ↦ {C : Finset ι | C ∈ F.powerset ∧ i ∈ C}
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ F, (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((M • μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
Tactic: have P_meas C : MeasurableSet (P C) :=
    measurableSet_biInter C (fun i _ ↦ hs_meas i) |>.inter <|
      measurableSet_biInter _ (fun i _ ↦ (hs_meas i).compl)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
x : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), encard.{u_6} (α := ι) {i : ι | y ∈ s i} ≤ (↑M : ℕ∞)
t : Set α
ht : MeasurableSet t
F : Finset ι
P : (C : Finset ι) → Set α := fun (C : Finset ι) ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : (i : ι) → Set (Finset ι) := fun (i : ι) ↦ {C : Finset ι | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
i : ι
hi : i ∈ F
⊢ s i ⊆ ⋃ C ∈ G i, P C
have refine_1 : ∀ (x : α) (hx : x ∈ s i), {x_1 ∈ F | x ∈ s x_1} ∈ G i
Tactic: refine fun x hx ↦ Set.mem_biUnion (x := F.filter (x ∈ s ·)) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
x : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), encard.{u_6} (α := ι) {i : ι | y ∈ s i} ≤ (↑M : ℕ∞)
t : Set α
ht : MeasurableSet t
F : Finset ι
P : (C : Finset ι) → Set α := fun (C : Finset ι) ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : (i : ι) → Set (Finset ι) := fun (i : ι) ↦ {C : Finset ι | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
i : ι
hi : i ∈ F
refine_1 : ∀ (x : α) (hx : x ∈ s i), {x_1 ∈ F | x ∈ s x_1} ∈ G i
⊢ s i ⊆ ⋃ C ∈ G i, P C
have refine_2 : ∀ (x : α) (hx : x ∈ s i), x ∈ P ({x_1 ∈ F | x ∈ s x_1})
Tactic: refine fun x hx ↦ Set.mem_biUnion (x := F.filter (x ∈ s ·)) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
x_1 : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), encard.{u_6} (α := ι) {i : ι | y ∈ s i} ≤ (↑M : ℕ∞)
t : Set α
ht : MeasurableSet t
F : Finset ι
P : (C : Finset ι) → Set α := fun (C : Finset ι) ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : (i : ι) → Set (Finset ι) := fun (i : ι) ↦ {C : Finset ι | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
i : ι
hi : i ∈ F
x : α
hx : x ∈ s i
⊢ x ∈ P ({x_2 ∈ F | x ∈ s x_2})
have refine_2 : (∀ (i : ι) (i_1 : i ∈ F ∧ x ∈ s i), x ∈ s i) ∧ ∀ (i : ι) (i_1 : i ∈ F ∧ ¬(i ∈ F ∧ x ∈ s i)), x ∈ (s i)ᶜ
Tactic: simp_rw [P, mem_inter_iff, mem_iInter, Finset.mem_sdiff, mem_filter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
x_1 : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), encard.{u_6} (α := ι) {i : ι | y ∈ s i} ≤ (↑M : ℕ∞)
t : Set α
ht : MeasurableSet t
F : Finset ι
P : (C : Finset ι) → Set α := fun (C : Finset ι) ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : (i : ι) → Set (Finset ι) := fun (i : ι) ↦ {C : Finset ι | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
i : ι
hi : i ∈ F
x : α
hx : x ∈ s i
⊢ (∀ (i : ι) (i_1 : i ∈ F ∧ x ∈ s i), x ∈ s i) ∧ ∀ (i : ι) (i_1 : i ∈ F ∧ ¬(i ∈ F ∧ x ∈ s i)), x ∈ (s i)ᶜ
have refine_2 : ∀ (i : ι) (i_1 : i ∈ F ∧ x ∈ s i), x ∈ s i
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
x_1 : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), encard.{u_6} (α := ι) {i : ι | y ∈ s i} ≤ (↑M : ℕ∞)
t : Set α
ht : MeasurableSet t
F : Finset ι
P : (C : Finset ι) → Set α := fun (C : Finset ι) ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : (i : ι) → Set (Finset ι) := fun (i : ι) ↦ {C : Finset ι | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
i : ι
hi : i ∈ F
x : α
hx : x ∈ s i
refine_2 : ∀ (i : ι) (i_1 : i ∈ F ∧ x ∈ s i), x ∈ s i
⊢ (∀ (i : ι) (i_1 : i ∈ F ∧ x ∈ s i), x ∈ s i) ∧ ∀ (i : ι) (i_1 : i ∈ F ∧ ¬(i ∈ F ∧ x ∈ s i)), x ∈ (s i)ᶜ
have refine_2₁ : ∀ (i : ι) (i_1 : i ∈ F ∧ ¬(i ∈ F ∧ x ∈ s i)), x ∈ (s i)ᶜ
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
x_1 : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), encard.{u_6} (α := ι) {i : ι | y ∈ s i} ≤ (↑M : ℕ∞)
t : Set α
ht : MeasurableSet t
F : Finset ι
P : (C : Finset ι) → Set α := fun (C : Finset ι) ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : (i : ι) → Set (Finset ι) := fun (i : ι) ↦ {C : Finset ι | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
i : ι
hi : i ∈ F
x : α
hx : x ∈ s i
refine_2 : ∀ (i : ι) (i_1 : i ∈ F ∧ x ∈ s i), x ∈ s i
refine_2₁ : ∀ (i : ι) (i_1 : i ∈ F ∧ ¬(i ∈ F ∧ x ∈ s i)), x ∈ (s i)ᶜ
refine_2₂ refine_2₃ refine_2₄ : ∀ (i : ι), i ∈ F ∧ x ∈ s i → x ∈ s i
refine_2₅ refine_2₆ refine_2₇ : ∀ (i : ι), i ∈ F ∧ ¬(i ∈ F ∧ x ∈ s i) → x ∈ (s i)ᶜ
⊢ (∀ (i : ι) (i_1 : i ∈ F ∧ x ∈ s i), x ∈ s i) ∧ ∀ (i : ι) (i_1 : i ∈ F ∧ ¬(i ∈ F ∧ x ∈ s i)), x ∈ (s i)ᶜ
have refine_2₈ : ∀ i ∈ F, x ∈ s i → x ∈ s i
Tactic: tauto