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 α
hs : MeasurableSet s
p : α → Prop
⊢ (∀ᵐ (x : α) ∂μ.restrict s, p x) ↔
    ∀ᵐ (x : (↑s : Type u_2)) ∂Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ, p (↑x : α)
have 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 : α)
Tactic: rw [← map_comap_subtype_coe hs, (MeasurableEmbedding.subtype_coe hs).ae_map_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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 : α)
⊢ (∀ᵐ (x : α) ∂μ.restrict s, p x) ↔
    ∀ᵐ (x : (↑s : Type u_2)) ∂Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ, p (↑x : α)
have 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 : α)
Tactic: rw [← map_comap_subtype_coe hs, (MeasurableEmbedding.subtype_coe hs).ae_map_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
inst : MeasureSpace α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := Measure α) (Measure.map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) volume)
    (Measure.restrict volume s)
have 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)
Tactic: rw [volume_set_coe_def, (MeasurableEmbedding.subtype_coe hs).map_comap volume, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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)
⊢ Eq (α := Measure α) (Measure.map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) volume)
    (Measure.restrict volume s)
have rw₁ : Eq (α := Measure α) (Measure.restrict volume (range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))))
  (Measure.restrict volume s)
Tactic: rw [volume_set_coe_def, (MeasurableEmbedding.subtype_coe hs).map_comap volume, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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)
⊢ Eq (α := Measure α) (Measure.map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) volume)
    (Measure.restrict volume s)
have rw₂ : Eq (α := Measure α) (Measure.restrict volume s) (Measure.restrict volume s)
Tactic: rw [volume_set_coe_def, (MeasurableEmbedding.subtype_coe hs).map_comap volume, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
inst : MeasureSpace α
s t : Set α
hs : NullMeasurableSet s volume
ht : MeasurableSet t
⊢ 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∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞)
⊢ 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∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞)
⊢ 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∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞)
⊢ 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∞)
have rw₃ : Eq (α := ℝ≥0∞) (((volume : Measure α) : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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 (μ.restrict s)] f
have rw : s.piecewise (β := fun (a : α) ↦ β) f g =ᶠ[ae μ ⊓ 𝓟 s] f
Tactic: rw [ae_restrict_eq hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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 (μ.restrict sᶜ)] g
have rw : s.piecewise (β := fun (a : α) ↦ β) f g =ᶠ[ae μ ⊓ 𝓟 sᶜ] g
Tactic: rw [ae_restrict_eq hs.compl]
-- 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
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s.indicator f ⁻¹' t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) (f ⁻¹' t)ᶜ : ℝ≥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: rw [Measure.restrict_apply' hs, Set.indicator_preimage, Set.ite]
-- 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
hs : MeasurableSet s
⊢ 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∞)
have 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∞)
Tactic: simp_rw [Set.compl_union, Set.compl_inter]
-- 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
hs : MeasurableSet s
⊢ 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∞)
have 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∞)
Tactic: change μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun _ => (0 : β)) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0
-- 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
hs : MeasurableSet s
⊢ 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∞)
have simp : 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 only [ht, ← Set.compl_eq_univ_diff, compl_compl, if_true,
    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
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
have 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∞)
Tactic: simp_rw [Set.union_inter_distrib_right, Set.compl_inter_self s, Set.union_empty]
-- 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
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
have simp_rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ 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]
-- 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
hs : MeasurableSet s
⊢ t ∈ Filter.map (s.indicator f) (ae μ) ↔ t ∈ Filter.map f (ae (μ.restrict s))
have simp_rw : s.indicator f ⁻¹' t ∈ ae μ ↔ f ⁻¹' t ∈ 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]
-- 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
hs : MeasurableSet s
simp_rw : s.indicator f ⁻¹' t ∈ ae μ ↔ f ⁻¹' t ∈ ae (μ.restrict s)
⊢ t ∈ Filter.map (s.indicator f) (ae μ) ↔ t ∈ Filter.map f (ae (μ.restrict s))
have 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∞)
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]
-- 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
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∞)
⊢ t ∈ Filter.map (s.indicator f) (ae μ) ↔ t ∈ Filter.map f (ae (μ.restrict s))
have 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∞)
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]
-- 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
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∞)
⊢ t ∈ Filter.map (s.indicator f) (ae μ) ↔ t ∈ Filter.map f (ae (μ.restrict s))
have 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∞)
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]
-- 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
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∞)
⊢ t ∈ Filter.map (s.indicator f) (ae μ) ↔ t ∈ Filter.map f (ae (μ.restrict s))
have 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∞)
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]
-- 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
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∞)
⊢ t ∈ Filter.map (s.indicator f) (ae μ) ↔ t ∈ Filter.map f (ae (μ.restrict s))
have 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∞)
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]
-- 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
⊢ 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: rw [mem_map, mem_ae_iff, Set.indicator_preimage, Set.ite, Set.compl_union, Set.compl_inter]
-- 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
⊢ 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∞)
have 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∞)
Tactic: change μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun _ => (0 : β)) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0
-- 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
⊢ t ∈ Filter.map (s.indicator f) (ae μ) ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : s.indicator f ⁻¹' t ∈ 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]