awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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∞)
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∞)
⊢ t ∈ Filter.map (s.indicator f) (ae μ) ↔ 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]

Premises used: Set.compl_union, Set.ite, Set.preimage_const, Compl.compl, Set.inter_univ, if_false, Set.compl_inter, Inter.inter, SDiff.sdiff, Set.preimage, Set.indicator_preimage, Set.compl_empty, MeasureTheory.mem_ae_iff, Union.union, OfNat.ofNat, Set.empty_diff, DFunLike.coe, Filter.mem_map
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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))
neg : ∀ (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))

Tactic:
by_cases ht : (0 : β) ∈ t

Premises used: OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∈ t
pos : t ∈ Filter.map f (ae (μ.restrict s)) → t ∈ Filter.map f (ae (μ.restrict s))
⊢ t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))

Tactic:
rw [mem_map_indicator_ae_iff_mem_map_restrict_ae_of_zero_mem ht hs]

Premises used: mem_map_indicator_ae_iff_mem_map_restrict_ae_of_zero_mem
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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 f (ae (μ.restrict s)) → t ∈ Filter.map f (ae (μ.restrict s))

Tactic:
id

Premises used: id
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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 f (ae (μ.restrict s)) → t ∈ Filter.map f (ae (μ.restrict s))

Tactic:
exact id

Premises used: id
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∉ t
neg :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))

Tactic:
rw [mem_map_indicator_ae_iff_of_zero_notMem ht, mem_map_restrict_ae_iff hs]

Premises used: MeasureTheory.mem_map_restrict_ae_iff, mem_map_indicator_ae_iff_of_zero_notMem
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∉ t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
fun h => measure_mono_null (Set.inter_subset_left.trans Set.subset_union_left) h

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, MeasureTheory.measure_mono_null, Set.subset_union_left
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∉ t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact fun h => measure_mono_null (Set.inter_subset_left.trans Set.subset_union_left) h

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, MeasureTheory.measure_mono_null, Set.subset_union_left
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
hs : MeasurableSet s
⊢ s.indicator f =ᶠ[ae (μ.restrict s)] f

Tactic:
piecewise_ae_eq_restrict hs

Premises used: Set.indicator, piecewise_ae_eq_restrict
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
hs : MeasurableSet s
⊢ s.indicator f =ᶠ[ae (μ.restrict s)] f

Tactic:
exact piecewise_ae_eq_restrict hs

Premises used: piecewise_ae_eq_restrict
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
hs : MeasurableSet s
⊢ s.indicator f =ᶠ[ae (μ.restrict s)] f

Tactic:
classical exact piecewise_ae_eq_restrict hs
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
hs : MeasurableSet s
⊢ s.indicator f =ᶠ[ae (μ.restrict sᶜ)] 0

Tactic:
piecewise_ae_eq_restrict_compl hs

Premises used: Set.indicator, piecewise_ae_eq_restrict_compl
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
hs : MeasurableSet s
⊢ s.indicator f =ᶠ[ae (μ.restrict sᶜ)] 0

Tactic:
exact piecewise_ae_eq_restrict_compl hs

Premises used: piecewise_ae_eq_restrict_compl
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
hs : MeasurableSet s
⊢ s.indicator f =ᶠ[ae (μ.restrict sᶜ)] 0

Tactic:
classical exact piecewise_ae_eq_restrict_compl hs
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
⊢ ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → f x = 0 x

Tactic:
rw [Filter.EventuallyEq, ae_restrict_iff' hs.compl] at hf

Premises used: Filter.EventuallyEq, MeasurableSet.compl, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
h : ∀ (x : α) (hx : x ∈ sᶜ → f x = 0 x), s.indicator f x = f x
⊢ s.indicator f =ᶠ[ae μ] f

Tactic:
filter_upwards [hf] with x hx
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
neg : ∀ (hxs : x ∉ s), s.indicator f x = f x
⊢ s.indicator f x = f x

Tactic:
by_cases hxs : x ∈ s
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
hxs : x ∈ s
⊢ s.indicator f x = f x

Tactic:
simp only [hxs, Set.indicator_of_mem]

Premises used: Set.indicator_of_mem
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
hxs : x ∉ s
⊢ s.indicator f x = f x

Tactic:
simp only [hx hxs, Pi.zero_apply, Set.indicator_apply_eq_zero, imp_true_iff]

Premises used: Pi.zero_apply, imp_true_iff, Set.indicator_apply_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0 x

Tactic:
rw [Filter.EventuallyEq, ae_restrict_iff' hs] at hf

Premises used: Filter.EventuallyEq, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
h : ∀ (x : α) (hx : x ∈ s → f x = 0 x), s.indicator f x = 0 x
⊢ s.indicator f =ᶠ[ae μ] 0

Tactic:
filter_upwards [hf] with x hx
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
neg : ∀ (hxs : x ∉ s), s.indicator f x = 0 x
⊢ s.indicator f x = 0 x

Tactic:
by_cases hxs : x ∈ s
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
hxs : x ∈ s
⊢ s.indicator f x = 0 x

Tactic:
simp only [hxs, hx hxs, Set.indicator_of_mem]

Premises used: Set.indicator_of_mem
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
hxs : x ∉ s
⊢ s.indicator f x = 0 x

Tactic:
simp [hxs]
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → β
inst_1 : Zero β
hst : s =ᶠ[ae μ] t
⊢ s.indicator f =ᶠ[ae μ] t.indicator f

Tactic:
piecewise_ae_eq_of_ae_eq_set hst

Premises used: Set.indicator, piecewise_ae_eq_of_ae_eq_set
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → β
inst_1 : Zero β
hst : s =ᶠ[ae μ] t
⊢ s.indicator f =ᶠ[ae μ] t.indicator f

Tactic:
exact piecewise_ae_eq_of_ae_eq_set hst

Premises used: piecewise_ae_eq_of_ae_eq_set
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → β
inst_1 : Zero β
hst : s =ᶠ[ae μ] t
⊢ s.indicator f =ᶠ[ae μ] t.indicator f

Tactic:
classical exact piecewise_ae_eq_of_ae_eq_set hst
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s.indicator f =ᶠ[ae μ] 0

Tactic:
indicator_empty' f ▸ indicator_ae_eq_of_ae_eq_set (ae_eq_empty.2 hs)

Premises used: Iff.mpr, Set.indicator_empty', Eq.rec, MeasureTheory.ae_eq_empty, indicator_ae_eq_of_ae_eq_set
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst_1 : Zero β
g : α → β
hs : MeasurableSet s
rw : (∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) ↔ s.indicator f =ᶠ[ae μ] s.indicator g
⊢ f =ᶠ[ae (μ.restrict s)] g ↔ s.indicator f =ᶠ[ae μ] s.indicator g

Tactic:
rw [Filter.EventuallyEq, ae_restrict_iff' hs]

Premises used: Filter.EventuallyEq, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
refine_2 : ∀ (h : s.indicator f =ᶠ[ae μ] s.indicator g), ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ (∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) ↔ s.indicator f =ᶠ[ae μ] s.indicator g

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
h₁ : ∀ (x : α) (hx : x ∈ s → f x = g x), s.indicator f x = s.indicator g x
⊢ s.indicator f =ᶠ[ae μ] s.indicator g

Tactic:
filter_upwards [h] with x hx
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
h₁ : ∀ (x : α) (hx : s.indicator f x = s.indicator g x), x ∈ s → f x = g x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x

Tactic:
filter_upwards [h] with x hx
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
neg : ∀ (hxs : x ∉ s), s.indicator f x = s.indicator g x
⊢ s.indicator f x = s.indicator g x

Tactic:
by_cases hxs : x ∈ s
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
hxs : x ∈ s
⊢ s.indicator f x = s.indicator g x

Tactic:
simp [hxs, hx hxs]
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
hxs : x ∉ s
⊢ s.indicator f x = s.indicator g x

Tactic:
simp [hxs]
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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 : α
hx : s.indicator f x = s.indicator g x
hxs : x ∈ s
⊢ f x = g x

Tactic:
simpa [hxs] using hx
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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)

Tactic:
le_iff.mpr (fun t ht ↦ le_of_eq_of_le (sum_apply _ ht) ?_)

Premises used: Iff.mpr, MeasureTheory.Measure.sum_apply, MeasureTheory.Measure.restrict, MeasureTheory.Measure.le_iff, le_of_eq_of_le
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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 : ℕ∞)
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∞)
⊢ (sum fun (i : ι) ↦ μ.restrict (s i)) ≤ M • μ.restrict (⋃ (i : ι), s i)

Tactic:
refine le_iff.mpr (fun t ht ↦ le_of_eq_of_le (sum_apply _ ht) ?_)

Premises used: Iff.mpr, MeasureTheory.Measure.sum_apply, MeasureTheory.Measure.le_iff, le_of_eq_of_le
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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∞)

Tactic:
ENNReal.summable.tsum_le_of_sum_le (fun F ↦ ?_)

Premises used: ENNReal.summable, Summable.tsum_le_of_sum_le
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
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∞)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ι), (μ.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 ↦ ?_)

Premises used: ENNReal.summable, Summable.tsum_le_of_sum_le
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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}
⊢ ∀ (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)
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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

Tactic:
fun x hx ↦ Set.mem_biUnion (x := F.filter (x ∈ s ·)) ?_ ?_

Premises used: Set.mem_biUnion, Set.Subset
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
refine_2 : ∀ (x : α) (hx : x ∈ s i), x ∈ P ({x_1 ∈ F | x ∈ s x_1})
⊢ s i ⊆ ⋃ C ∈ G i, P C

Tactic:
refine fun x hx ↦ Set.mem_biUnion (x := F.filter (x ∈ s ·)) ?_ ?_

Premises used: Set.mem_biUnion
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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_2 ∈ F | x ∈ s x_2} ∈ G i

Tactic:
⟨Finset.mem_powerset.mpr (filter_subset _ F), mem_filter.mpr ⟨hi, hx⟩⟩

Premises used: Iff.mpr, Set.Mem, setOf, Finset.filter_subset, Finset.mem_powerset, And.intro, Finset.mem_filter
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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_2 ∈ F | x ∈ s x_2} ∈ G i

Tactic:
exact ⟨Finset.mem_powerset.mpr (filter_subset _ F), mem_filter.mpr ⟨hi, hx⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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 ∧ ¬(i ∈ F ∧ x ∈ s i)), x ∈ (s i)ᶜ
⊢ x ∈ P ({x_2 ∈ F | x ∈ s x_2})

Tactic:
simp_rw [P, mem_inter_iff, mem_iInter, Finset.mem_sdiff, mem_filter]

Premises used: Set.mem_inter_iff, Set.mem_iInter, Finset.mem_sdiff, Finset.mem_filter
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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)ᶜ
refine_2₈ refine_2₉ refine_2₁₀ : ∀ i ∈ F, x ∈ s i → x ∈ s i
refine_2₁₁ refine_2₁₂ refine_2₁₃ : ∀ (i : ι), x ∈ s i → i ∈ F → ¬(i ∈ F ∧ x ∈ s i) → False
refine_2₁₄ : ∀ (i : ι), x ∈ s i → i ∈ F → i ∉ F → False
refine_2₁₅ : ∀ (i : ι), x ∈ s i → i ∈ F → x ∉ s i → False
⊢ (∀ (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:
tauto