awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
δ : Type u_4
u : Set δ
inst : MeasureSpace δ
hu : NullMeasurableSet u volume
rw :
  Eq (α := ℝ≥0∞)
    (((volume : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (image (α := { x : δ // x ∈ u }) (Subtype.val (p := fun (x : δ) ↦ x ∈ u)) univ) :
      ℝ≥0∞)
    (((volume : Measure δ) : (a : Set δ) → ℝ≥0∞) u : ℝ≥0∞)
rw₁ : Injective.{u_4 + 1, u_4 + 1} (α := { x : δ // x ∈ u }) (Subtype.val (p := fun (x : δ) ↦ x ∈ u))
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (↑u : Type u_4)) : (a : Set (↑u : Type u_4)) → ℝ≥0∞) univ : ℝ≥0∞)
    (((volume : Measure δ) : (a : Set δ) → ℝ≥0∞) u : ℝ≥0∞)
have rw₂ : ∀ (s : Set { x : δ // x ∈ u }), MeasurableSet s → NullMeasurableSet (Subtype.val (p := fun (x : δ) ↦ x ∈ u) '' s) volume
Tactic: rw [Subtype.volume_def, comap_apply₀ _ _ _ _ MeasurableSet.univ.nullMeasurableSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
⊢ Measure.map f (Measure.comap f μ) = μ.restrict (range f)
have h : ∀ (t : Set β) (ht : MeasurableSet t),
  Eq (α := ℝ≥0∞) (((Measure.map f (Measure.comap f μ) : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ.restrict (range f) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: ext1 t ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
t : Set β
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) (((Measure.map f (Measure.comap f μ) : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ.restrict (range f) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (((Measure.comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
  ((μ.restrict (range f) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [hf.map_apply, comap_apply f hf.injective hf.measurableSet_image' _ (hf.measurable ht),
    image_preimage_eq_inter_range, Measure.restrict_apply ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
t : Set β
ht : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) (((Measure.comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
    ((μ.restrict (range f) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.map f (Measure.comap f μ) : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ.restrict (range f) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' t) : ℝ≥0∞) ((μ.restrict (range f) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [hf.map_apply, comap_apply f hf.injective hf.measurableSet_image' _ (hf.measurable ht),
    image_preimage_eq_inter_range, Measure.restrict_apply ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
t : Set β
ht : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) (((Measure.comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
    ((μ.restrict (range f) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' t) : ℝ≥0∞) ((μ.restrict (range f) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.map f (Measure.comap f μ) : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ.restrict (range f) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
have h₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (t ∩ range f) : ℝ≥0∞) ((μ.restrict (range f) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [hf.map_apply, comap_apply f hf.injective hf.measurableSet_image' _ (hf.measurable ht),
    image_preimage_eq_inter_range, Measure.restrict_apply ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
t : Set β
ht : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) (((Measure.comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
    ((μ.restrict (range f) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' t) : ℝ≥0∞) ((μ.restrict (range f) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (t ∩ range f) : ℝ≥0∞) ((μ.restrict (range f) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.map f (Measure.comap f μ) : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ.restrict (range f) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
have h₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (t ∩ range f) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (t ∩ range f) : ℝ≥0∞)
Tactic: rw [hf.map_apply, comap_apply f hf.injective hf.measurableSet_image' _ (hf.measurable ht),
    image_preimage_eq_inter_range, Measure.restrict_apply ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set α
⊢ Eq (α := ℝ≥0∞) (((Measure.comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' s) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((Measure.comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  (((Measure.comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [hf.injective.preimage_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set α
⊢ Eq (α := ℝ≥0∞) (((Measure.map f (Measure.comap f μ) : Measure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ.restrict (range f) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
Tactic: rw [hf.map_comap, restrict_apply' hf.measurableSet_range,
        inter_eq_self_of_subset_left (image_subset_range _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set α
rw :
  Eq (α := ℝ≥0∞) ((μ.restrict (range f) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.map f (Measure.comap f μ) : Measure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s ∩ range f) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
Tactic: rw [hf.map_comap, restrict_apply' hf.measurableSet_range,
        inter_eq_self_of_subset_left (image_subset_range _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set α
rw :
  Eq (α := ℝ≥0∞) ((μ.restrict (range f) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s ∩ range f) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.map f (Measure.comap f μ) : Measure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
Tactic: rw [hf.map_comap, restrict_apply' hf.measurableSet_range,
        inter_eq_self_of_subset_left (image_subset_range _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
⊢ Measure.comap f (Measure.map f μ) = μ
have h : ∀ (t : Set α),
  MeasurableSet t →
    Eq (α := ℝ≥0∞) (((Measure.comap f (Measure.map f μ) : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: ext t _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
t : Set α
h : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) (((Measure.comap f (Measure.map f μ) : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (f '' t) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [hf.comap_apply, hf.map_apply, preimage_image_eq _ hf.injective]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
t : Set α
h_1 : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (f '' t) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.comap f (Measure.map f μ) : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [hf.comap_apply, hf.map_apply, preimage_image_eq _ hf.injective]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
t : Set α
h_1 : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (f '' t) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
h₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.comap f (Measure.map f μ) : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [hf.comap_apply, hf.map_apply, preimage_image_eq _ hf.injective]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set β
⊢ Eq (α := ℝ≥0∞) (((Measure.comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((Measure.map f (Measure.comap f μ) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  ((μ : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
Tactic: rw [← hf.map_apply, hf.map_comap, restrict_apply' hf.measurableSet_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ.restrict (range f) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
Tactic: rw [← hf.map_apply, hf.map_comap, restrict_apply' hf.measurableSet_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
Tactic: rw [← hf.map_apply, hf.map_comap, restrict_apply' hf.measurableSet_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set β
⊢ Eq (α := Measure α) (Measure.comap f (μ.restrict s)) (Measure.restrict (Measure.comap f μ) (f ⁻¹' s))
have 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∞)
Tactic: ext t ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set β
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∞)
have 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∞)
Tactic: rw [Measure.restrict_apply ht, comap_apply hf, comap_apply hf,
    Measure.restrict_apply (hf.measurableSet_image.2 ht), image_inter_preimage]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞)
⊢ 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∞)
have h₁ : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set β) → ℝ≥0∞) (f '' t) : ℝ≥0∞)
  (((Measure.comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (t ∩ f ⁻¹' s) : ℝ≥0∞)
Tactic: rw [Measure.restrict_apply ht, comap_apply hf, comap_apply hf,
    Measure.restrict_apply (hf.measurableSet_image.2 ht), image_inter_preimage]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞)
⊢ 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∞)
have h₂ : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set β) → ℝ≥0∞) (f '' t) : ℝ≥0∞)
  ((μ : (a : Set β) → ℝ≥0∞) (f '' (t ∩ f ⁻¹' s)) : ℝ≥0∞)
Tactic: rw [Measure.restrict_apply ht, comap_apply hf, comap_apply hf,
    Measure.restrict_apply (hf.measurableSet_image.2 ht), image_inter_preimage]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞)
⊢ 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∞)
have h₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' t ∩ s) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' (t ∩ f ⁻¹' s)) : ℝ≥0∞)
Tactic: rw [Measure.restrict_apply ht, comap_apply hf, comap_apply hf,
    Measure.restrict_apply (hf.measurableSet_image.2 ht), image_inter_preimage]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞)
⊢ 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∞)
have h₄ : Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' t ∩ s) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (f '' t ∩ s) : ℝ≥0∞)
Tactic: rw [Measure.restrict_apply ht, comap_apply hf, comap_apply hf,
    Measure.restrict_apply (hf.measurableSet_image.2 ht), image_inter_preimage]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set α
⊢ Eq (α := Measure α) (Measure.restrict (Measure.comap f μ) s) (Measure.comap f (μ.restrict (f '' s)))
have rw : Eq (α := Measure α) (Measure.restrict (Measure.comap f μ) s) (Measure.restrict (Measure.comap f μ) (f ⁻¹' f '' s))
Tactic: rw [comap_restrict hf, preimage_image_eq _ hf.injective]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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))
⊢ Eq (α := Measure α) (Measure.restrict (Measure.comap f μ) s) (Measure.comap f (μ.restrict (f '' s)))
have rw₁ : Eq (α := Measure α) (Measure.restrict (Measure.comap f μ) s) (Measure.restrict (Measure.comap f μ) s)
Tactic: rw [comap_restrict hf, preimage_image_eq _ hf.injective]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
e : α ≃ᵐ β
μ : Measure β
s : Set α
⊢ Eq (α := ℝ≥0∞) (((Measure.comap (⇑e : (a : α) → β) μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) ((⇑e.symm : (a : β) → α) ⁻¹' s) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) ((⇑e : (a : α) → β) '' s) : ℝ≥0∞)
  ((μ : (a : Set β) → ℝ≥0∞) ((⇑e.symm : (a : β) → α) ⁻¹' s) : ℝ≥0∞)
Tactic: rw [e.measurableEmbedding.comap_apply, e.image_eq_preimage_symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.comap (⇑e : (a : α) → β) μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set β) → ℝ≥0∞) ((⇑e.symm : (a : β) → α) ⁻¹' s) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) ((⇑e.symm : (a : β) → α) ⁻¹' s) : ℝ≥0∞)
  ((μ : (a : Set β) → ℝ≥0∞) ((⇑e.symm : (a : β) → α) ⁻¹' s) : ℝ≥0∞)
Tactic: rw [e.measurableEmbedding.comap_apply, e.image_eq_preimage_symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ Eq (α := Measure β) (map f μ) (comap g μ)
have h : ∀ (s : Set β) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((comap g μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((comap g μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s \ {x : α | (fun (a : α) ↦ a ∈ range g) x}ᶜ) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (g '' s) : ℝ≥0∞)
Tactic: rw [map_apply hf hs, hg.comap_apply, ← measure_diff_null hμg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s \ {x : α | (fun (a : α) ↦ a ∈ range g) x}ᶜ) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (g '' s) : ℝ≥0∞)
have h : f ⁻¹' s \ {x : α | (fun (a : α) ↦ a ∈ range g) x}ᶜ = g '' s
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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 : α | (fun (a : α) ↦ a ∈ range g) x}ᶜ = g '' s
have h : f ⁻¹' s ∩ {x : α | ∃ (y : β), g y = x} = g '' s
Tactic: simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
s : Set α
hs : MeasurableSet s
μ : Measure α
⊢ Measure.map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ) =
    μ.restrict s
have rw : μ.restrict (range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) = μ.restrict s
Tactic: rw [(MeasurableEmbedding.subtype_coe hs).map_comap, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ Measure.map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ) =
    μ.restrict s
have rw₁ : μ.restrict s = μ.restrict s
Tactic: rw [(MeasurableEmbedding.subtype_coe hs).map_comap, Subtype.range_coe]