awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set β
rw :
  Eq (α := ℝ≥0∞) (((Measure.map f (Measure.comap f μ) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ.restrict (range f) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
rw₂ rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)

Tactic:
rw [← hf.map_apply, hf.map_comap, restrict_apply' hf.measurableSet_range]

Premises used: MeasurableEmbedding.measurableSet_range, MeasurableEmbedding.map_apply, MeasurableEmbedding.map_comap, MeasureTheory.Measure.restrict_apply'
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set β
h :
  ∀ (t : Set α) (ht : MeasurableSet t),
    Eq (α := ℝ≥0∞) (((Measure.comap f (μ.restrict s) : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
      (((Measure.restrict (Measure.comap f μ) (f ⁻¹' s) : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := Measure α) (Measure.comap f (μ.restrict s)) (Measure.restrict (Measure.comap f μ) (f ⁻¹' s))

Tactic:
ext t ht
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set β
t : Set α
ht : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) (((Measure.comap f (μ.restrict s) : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((Measure.comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (t ∩ f ⁻¹' s) : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set β) → ℝ≥0∞) (f '' t) : ℝ≥0∞)
    (((Measure.comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (t ∩ f ⁻¹' s) : ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set β) → ℝ≥0∞) (f '' t) : ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) (f '' (t ∩ f ⁻¹' s)) : ℝ≥0∞)
h₃ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' t ∩ s) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' (t ∩ f ⁻¹' s)) : ℝ≥0∞)
h₄ h₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' t ∩ s) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' t ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.comap f (μ.restrict s) : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((Measure.restrict (Measure.comap f μ) (f ⁻¹' s) : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [Measure.restrict_apply ht, comap_apply hf, comap_apply hf,
    Measure.restrict_apply (hf.measurableSet_image.2 ht), image_inter_preimage]

Premises used: Iff.mpr, MeasurableEmbedding.measurableSet_image, Set.image_inter_preimage, MeasureTheory.Measure.restrict_apply, MeasurableEmbedding.comap_apply
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set α
rw : Eq (α := Measure α) (Measure.restrict (Measure.comap f μ) s) (Measure.restrict (Measure.comap f μ) (f ⁻¹' f '' s))
rw₁ rw₂ : Eq (α := Measure α) (Measure.restrict (Measure.comap f μ) s) (Measure.restrict (Measure.comap f μ) s)
⊢ Eq (α := Measure α) (Measure.restrict (Measure.comap f μ) s) (Measure.comap f (μ.restrict (f '' s)))

Tactic:
rw [comap_restrict hf, preimage_image_eq _ hf.injective]

Premises used: MeasurableEmbedding.comap_restrict, MeasurableEmbedding.injective, Set.preimage_image_eq
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
e : α ≃ᵐ β
μ : Measure α
s : Set β
⊢ Eq (α := Measure β) (Measure.restrict (Measure.map (⇑e : (a : α) → β) μ) s)
    (Measure.map (⇑e : (a : α) → β) (μ.restrict ((⇑e : (a : α) → β) ⁻¹' s)))

Tactic:
e.measurableEmbedding.restrict_map _ _

Premises used: MeasurableEquiv.measurableEmbedding, MeasurableEmbedding.restrict_map
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
e : α ≃ᵐ β
μ : Measure β
s : Set α
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) ((⇑e : (a : α) → β) '' s) : ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) ((⇑e.symm : (a : β) → α) ⁻¹' s) : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) ((⇑e.symm : (a : β) → α) ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) ((⇑e.symm : (a : β) → α) ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.comap (⇑e : (a : α) → β) μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) ((⇑e.symm : (a : β) → α) ⁻¹' s) : ℝ≥0∞)

Tactic:
rw [e.measurableEmbedding.comap_apply, e.image_eq_preimage_symm]

Premises used: MeasurableEquiv.measurableEmbedding, MeasurableEmbedding.comap_apply, MeasurableEquiv.image_eq_preimage_symm
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
x : MeasurableSpace α
x_1 : MeasurableSpace β
f : α → β
g : β → α
μ : Measure α
hf : Measurable f
hg : MeasurableEmbedding g
hμg : ∀ᵐ (a : α) ∂μ, a ∈ range g
hfg : ∀ (a : β), f (g a) = a
h :
  ∀ (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((comap g μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Measure β) (map f μ) (comap g μ)

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
x : MeasurableSpace α
x_1 : MeasurableSpace β
f : α → β
g : β → α
μ : Measure α
hf : Measurable f
hg : MeasurableEmbedding g
hμg : ∀ᵐ (a : α) ∂μ, a ∈ range g
hfg : ∀ (a : β), f (g a) = a
s : Set β
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s \ {x : α | (fun (a : α) ↦ a ∈ range g) x}ᶜ) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (g '' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((comap g μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [map_apply hf hs, hg.comap_apply, ← measure_diff_null hμg]

Premises used: MeasureTheory.Measure.map_apply, MeasurableEmbedding.comap_apply, MeasureTheory.measure_diff_null
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
x : MeasurableSpace α
x_1 : MeasurableSpace β
f : α → β
g : β → α
μ : Measure α
hf : Measurable f
hg : MeasurableEmbedding g
hμg : ∀ᵐ (a : α) ∂μ, a ∈ range g
hfg : ∀ (a : β), f (g a) = a
s : Set β
hs : MeasurableSet s
h : f ⁻¹' s \ {x : α | (fun (a : α) ↦ a ∈ range g) x}ᶜ = g '' s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s \ {x : α | (fun (a : α) ↦ a ∈ range g) x}ᶜ) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (g '' s) : ℝ≥0∞)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
x : MeasurableSpace α
x_1 : MeasurableSpace β
f : α → β
g : β → α
μ : Measure α
hf : Measurable f
hg : MeasurableEmbedding g
hμg : ∀ᵐ (a : α) ∂μ, a ∈ range g
hfg : ∀ (a : β), f (g a) = a
s : Set β
hs : MeasurableSet s
h : f ⁻¹' s ∩ {x : α | ∃ (y : β), g y = x} = g '' s
⊢ f ⁻¹' s \ {x : α | (fun (a : α) ↦ a ∈ range g) x}ᶜ = g '' s

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
x : MeasurableSpace α
x_1 : MeasurableSpace β
f : α → β
g : β → α
μ : Measure α
hf : Measurable f
hg : MeasurableEmbedding g
hμg : ∀ᵐ (a : α) ∂μ, a ∈ range g
hfg : ∀ (a : β), f (g a) = a
s : Set β
hs : MeasurableSet s
⊢ f ⁻¹' s ∩ {x : α | ∃ (y : β), g y = x} = g '' s

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
_m0 : MeasurableSpace α
s : Set α
hs : MeasurableSet s
μ : Measure α
t : Set (↑s : Type u_2)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ : Measure (↑s : Type u_2)) :
          (a : Set (↑s : Type u_2)) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) : ℝ≥0∞)

Tactic:
(MeasurableEmbedding.subtype_coe hs).comap_apply _ _

Premises used: MeasurableEmbedding.comap_apply, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
s : Set α
hs : MeasurableSet s
μ : Measure α
rw : μ.restrict (range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) = μ.restrict s
rw₁ rw₂ : μ.restrict s = μ.restrict s
⊢ Measure.map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ) =
    μ.restrict s

Tactic:
rw [(MeasurableEmbedding.subtype_coe hs).map_comap, Subtype.range_coe]

Premises used: Subtype.range_coe, MeasurableEmbedding.map_comap, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
p : α → Prop
rw :
  (∀ᵐ (x :
      α) ∂Measure.map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ),
      p x) ↔
    ∀ᵐ (x : (↑s : Type u_2)) ∂Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ, p (↑x : α)
rw₁ rw₂ :
  (∀ᵐ (x : { x : α // x ∈ s }) ∂Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ, p (↑x : α)) ↔
    ∀ᵐ (x : (↑s : Type u_2)) ∂Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ, p (↑x : α)
⊢ (∀ᵐ (x : α) ∂μ.restrict s, p x) ↔
    ∀ᵐ (x : (↑s : Type u_2)) ∂Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ, p (↑x : α)

Tactic:
rw [← map_comap_subtype_coe hs, (MeasurableEmbedding.subtype_coe hs).ae_map_iff]

Premises used: MeasurableEmbedding.ae_map_iff, map_comap_subtype_coe, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
inst : MeasureSpace α
s : Set α
⊢ Eq.{u_2 + 1} (α := Measure (↑s : Type u_2)) volume (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) volume)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
inst : MeasureSpace α
s : Set α
hs : MeasurableSet s
rw :
  Eq (α := Measure α)
    (Measure.map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) volume))
    (Measure.restrict volume s)
rw₁ :
  Eq (α := Measure α)
    (Measure.restrict volume (range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))))
    (Measure.restrict volume s)
rw₂ rw₃ : Eq (α := Measure α) (Measure.restrict volume s) (Measure.restrict volume s)
⊢ Eq (α := Measure α) (Measure.map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) volume)
    (Measure.restrict volume s)

Tactic:
rw [volume_set_coe_def, (MeasurableEmbedding.subtype_coe hs).map_comap volume, Subtype.range_coe]

Premises used: volume_set_coe_def, Subtype.range_coe, MeasureTheory.MeasureSpace.volume, MeasurableEmbedding.map_comap, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
inst : MeasureSpace α
s : Set α
hs : MeasurableSet s
t : Set (↑s : Type u_2)
⊢ Eq (α := ℝ≥0∞) (((volume : Measure α) : (a : Set α) → ℝ≥0∞) (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) : ℝ≥0∞)
    (((volume : Measure (↑s : Type u_2)) : (a : Set (↑s : Type u_2)) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
(comap_subtype_coe_apply hs volume t).symm

Premises used: comap_subtype_coe_apply, MeasureTheory.MeasureSpace.volume, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
inst : MeasureSpace α
s t : Set α
hs : NullMeasurableSet s volume
ht : MeasurableSet t
rw :
  Eq (α := ℝ≥0∞)
    (((Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) volume : Measure { x : α // x ∈ s }) :
          (a : Set { x : α // x ∈ s }) → ℝ≥0∞)
        (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) :
      ℝ≥0∞)
    (((volume : Measure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    (((volume : Measure α) : (a : Set α) → ℝ≥0∞)
        ((fun (a : { x : α // x ∈ s }) ↦ (↑a : α)) '' Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) :
      ℝ≥0∞)
    (((volume : Measure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞)
    (((volume : Measure α) : (a : Set α) → ℝ≥0∞) (t ∩ range fun (a : { x : α // x ∈ s }) ↦ (↑a : α)) : ℝ≥0∞)
    (((volume : Measure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₃ rw₄ :
  Eq (α := ℝ≥0∞) (((volume : Measure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (((volume : Measure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((volume : Measure { x : α // x ∈ s }) : (a : Set { x : α // x ∈ s }) → ℝ≥0∞)
        (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) :
      ℝ≥0∞)
    (((volume : Measure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
rw [volume_set_coe_def,
    comap_apply₀ _ _ Subtype.coe_injective
      (fun h => MeasurableSet.nullMeasurableSet_subtype_coe hs)
      (measurable_subtype_coe ht).nullMeasurableSet,
    image_preimage_eq_inter_range, Subtype.range_coe]

Premises used: measurable_subtype_coe, volume_set_coe_def, MeasurableSet.nullMeasurableSet, MeasureTheory.Measure.MeasurableSet.nullMeasurableSet_subtype_coe, Subtype.range_coe, Set.image_preimage_eq_inter_range, MeasureTheory.Measure.comap_apply₀, Subtype.coe_injective
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → β
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
rw : s.piecewise (β := fun (a : α) ↦ β) f g =ᶠ[ae μ ⊓ 𝓟 s] f
⊢ s.piecewise (β := fun (a : α) ↦ β) f g =ᶠ[ae (μ.restrict s)] f

Tactic:
rw [ae_restrict_eq hs]

Premises used: MeasureTheory.ae_restrict_eq
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → β
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
⊢ s.piecewise (β := fun (a : α) ↦ β) f g =ᶠ[ae μ ⊓ 𝓟 s] f

Tactic:
(piecewise_eqOn s f g).eventuallyEq.filter_mono inf_le_right

Premises used: Filter.EventuallyEq.filter_mono, Set.EqOn.eventuallyEq, inf_le_right, Set.piecewise_eqOn
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → β
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
⊢ s.piecewise (β := fun (a : α) ↦ β) f g =ᶠ[ae μ ⊓ 𝓟 s] f

Tactic:
exact (piecewise_eqOn s f g).eventuallyEq.filter_mono inf_le_right

Premises used: Filter.EventuallyEq.filter_mono, Set.EqOn.eventuallyEq, inf_le_right, Set.piecewise_eqOn
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → β
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
rw : s.piecewise (β := fun (a : α) ↦ β) f g =ᶠ[ae μ ⊓ 𝓟 sᶜ] g
⊢ s.piecewise (β := fun (a : α) ↦ β) f g =ᶠ[ae (μ.restrict sᶜ)] g

Tactic:
rw [ae_restrict_eq hs.compl]

Premises used: MeasurableSet.compl, MeasureTheory.ae_restrict_eq
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → β
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
⊢ s.piecewise (β := fun (a : α) ↦ β) f g =ᶠ[ae μ ⊓ 𝓟 sᶜ] g

Tactic:
(piecewise_eqOn_compl s f g).eventuallyEq.filter_mono inf_le_right

Premises used: Filter.EventuallyEq.filter_mono, Set.EqOn.eventuallyEq, inf_le_right, Set.piecewise_eqOn_compl
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → β
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
⊢ s.piecewise (β := fun (a : α) ↦ β) f g =ᶠ[ae μ ⊓ 𝓟 sᶜ] g

Tactic:
exact (piecewise_eqOn_compl s f g).eventuallyEq.filter_mono inf_le_right

Premises used: Filter.EventuallyEq.filter_mono, Set.EqOn.eventuallyEq, inf_le_right, Set.piecewise_eqOn_compl
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
μ : Measure α
s t : Set α
f g : α → β
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
inst_2 : DecidablePred fun (x : α) ↦ x ∈ t
hst : s =ᶠ[ae μ] t
x : α
hx : x ∈ s ↔ x ∈ t
⊢ s.piecewise (β := fun (a : α) ↦ β) f g x = t.piecewise (β := fun (a : α) ↦ β) f g x

Tactic:
simp [piecewise, hx]

Premises used: Set.piecewise
-- 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
hs : MeasurableSet s
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s.indicator f ⁻¹' t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) (f ⁻¹' t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [Measure.restrict_apply' hs, Set.indicator_preimage, Set.ite]

Premises used: Set.ite, Set.indicator_preimage, MeasureTheory.Measure.restrict_apply'
-- 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
hs : MeasurableSet s
simp_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∞)
⊢ 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:
simp_rw [Set.compl_union, Set.compl_inter]

Premises used: Set.compl_union, Set.compl_inter
-- 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
hs : MeasurableSet s
change :
  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∞)
⊢ 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:
change μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun _ => (0 : β)) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0

Premises used: Compl.compl, Inter.inter, SDiff.sdiff, Set.preimage, Union.union, OfNat.ofNat, DFunLike.coe
-- 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
hs : MeasurableSet s
simp :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ 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:
simp only [ht, ← Set.compl_eq_univ_diff, compl_compl, if_true,
    Set.preimage_const]

Premises used: compl_compl, if_true, Set.preimage_const, Set.compl_eq_univ_diff
-- 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
hs : MeasurableSet s
simp_rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s ∪ sᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s ∪ ∅) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp_rw [Set.union_inter_distrib_right, Set.compl_inter_self s, Set.union_empty]

Premises used: Set.union_empty, Set.compl_inter_self, Set.union_inter_distrib_right
-- 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
hs : MeasurableSet s
simp_rw : s.indicator f ⁻¹' t ∈ ae μ ↔ f ⁻¹' t ∈ ae (μ.restrict s)
simp_rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s.indicator f ⁻¹' t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) (f ⁻¹' t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
simp_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∞)
simp_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∞)
simp_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∞)
simp_rw₅ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ 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:
classical
  simp_rw [mem_map, mem_ae_iff]
  rw [Measure.restrict_apply' hs, Set.indicator_preimage, Set.ite]
  simp_rw [Set.compl_union, Set.compl_inter]
  change μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun _ => (0 : β)) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0
  simp only [ht, ← Set.compl_eq_univ_diff, compl_compl, if_true,
    Set.preimage_const]
  simp_rw [Set.union_inter_distrib_right, Set.compl_inter_self s, Set.union_empty]

Premises used: Set.compl_union, Set.ite, compl_compl, if_true, Set.union_empty, Set.preimage_const, Compl.compl, Set.compl_inter, Inter.inter, SDiff.sdiff, Set.preimage, Set.indicator_preimage, Set.compl_eq_univ_diff, MeasureTheory.mem_ae_iff, Set.compl_inter_self, Union.union, OfNat.ofNat, Set.union_inter_distrib_right, MeasureTheory.Measure.restrict_apply', 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 β
t : Set β
ht : 0 ∉ t
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∞)

Tactic:
rw [mem_map, mem_ae_iff, Set.indicator_preimage, Set.ite, Set.compl_union, Set.compl_inter]

Premises used: Set.compl_union, Set.ite, Set.compl_inter, Set.indicator_preimage, MeasureTheory.mem_ae_iff, Filter.mem_map
-- 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
change :
  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∞)
⊢ 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:
change μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun _ => (0 : β)) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0

Premises used: Compl.compl, Inter.inter, SDiff.sdiff, Set.preimage, Union.union, OfNat.ofNat, DFunLike.coe
-- 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
⊢ 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:
simp only [ht, if_false, Set.compl_empty, Set.empty_diff, Set.inter_univ, Set.preimage_const]

Premises used: Set.preimage_const, Set.inter_univ, if_false, Set.compl_empty, Set.empty_diff