awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)

Tactic:
have : ∀ᵐ x ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t) := by
    apply ae_imp_of_ae_restrict
    filter_upwards [t't] with x hx using by simpa using hx
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
h₁ : ∀ (x : α) (hx : x ∈ s → (x ∈ t' ↔ x ∈ t)), t' x = t x
⊢ t' =ᶠ[ae μ] t

Tactic:
filter_upwards [this] with x hx
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
x : α
hx : x ∈ s → (x ∈ t' ↔ x ∈ t)
h₁ : (x ∈ t') = (x ∈ t)
⊢ t' x = t x

Tactic:
change (x ∈ t') = (x ∈ t)

Premises used: Membership.mem
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
x : α
hx : x ∈ s → (x ∈ t' ↔ x ∈ t)
h₁ : x ∈ t' ↔ x ∈ t
⊢ (x ∈ t') = (x ∈ t)

Tactic:
simp only [eq_iff_iff]

Premises used: eq_iff_iff
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
x : α
hx : x ∈ s → (x ∈ t' ↔ x ∈ t)
h₁ : ∀ (hx : x ∉ s), x ∈ t' ↔ x ∈ t
h₂ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' ↔ x ∈ t
h₃ : ∀ (hx : x ∉ s), x ∈ t' ↔ x ∈ t
h₄ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' ↔ x ∈ t
h₅ : ∀ (hx : x ∉ s), x ∈ t' → x ∈ t
h₆ : ∀ (hx : x ∉ s), x ∈ t → x ∈ t'
h₇ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' → x ∈ t
h₈ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t → x ∈ t'
h₉ h₁₀ h₁₁ : ∀ (hx : x ∉ s), x ∈ t' → x ∈ t
h₁₂ h₁₃ h₁₄ : ∀ (hx : x ∉ s), x ∈ t → x ∈ t'
h₁₅ : x ∈ t' → x ∈ t' → x ∈ t → x ∈ t
h₁₆ : x ∈ t' → x ∉ t' → x ∉ t → x ∈ t
h₁₇ h₁₈ : x ∈ t' → x ∈ t' → x ∈ t → x ∈ t
h₁₉ : x ∈ t → x ∈ t' → x ∈ t → x ∈ t'
h₂₀ : x ∈ t → x ∉ t' → x ∉ t → x ∈ t'
h₂₁ h₂₂ : x ∈ t → x ∈ t' → x ∈ t → x ∈ t'
h₂₃ h₂₄ h₂₅ : ∀ (hx : x ∉ s), x ∈ t' → x ∈ t
h₂₆ h₂₇ h₂₈ : ∀ (hx : x ∉ s), x ∈ t → x ∈ t'
h₂₉ h₃₀ : ∀ (hx : x ∉ s), x ∈ t' → x ∈ t
h₃₁ h₃₂ : ∀ (hx : x ∉ s), x ∈ t → x ∈ t'
⊢ x ∈ t' ↔ x ∈ t

Tactic:
tauto
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
⊢ t' =ᶠ[ae μ] t

Tactic:
have : t' =ᵐ[μ] t := by
    filter_upwards [this] with x hx
    change (x ∈ t') = (x ∈ t)
    simp only [eq_iff_iff]
    tauto
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this_1 : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
this : t' =ᶠ[ae μ] t
⊢ NullMeasurableSet t μ

Tactic:
ht'.nullMeasurableSet.congr this

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.NullMeasurableSet.congr
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this_1 : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
this : t' =ᶠ[ae μ] t
⊢ NullMeasurableSet t μ

Tactic:
exact ht'.nullMeasurableSet.congr this

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.NullMeasurableSet.congr
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set (↑s : Type u_2)
hs : NullMeasurableSet s μ
ht : MeasurableSet t
⊢ MeasurableSet t

Tactic:
rw [Subtype.instMeasurableSpace, comap_eq_generateFrom] at ht

Premises used: MeasurableSpace.comap_eq_generateFrom, Subtype.instMeasurableSpace
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set (↑s : Type u_2)
hs : NullMeasurableSet s μ
t' : Set (↑s : Type u_2)
ht' :
  Membership.mem (γ := Set (Set (↑s : Type u_2)))
    {t : Set { x : α // x ∈ s } |
      ∃ (s_1 : Set α), MeasurableSet s_1 ∧ Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s_1 = t}
    t'
ht : MeasurableSet t'
hC :
  ∀ (s' : Set α) (hs' : MeasurableSet s'),
    MeasurableSet (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s') →
      NullMeasurableSet
        (image (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
          (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s'))
        μ
⊢ NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t') μ

Tactic:
obtain ⟨s', hs', rfl⟩ := ht'

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set (↑s : Type u_2)
hs : NullMeasurableSet s μ
s' : Set α
hs' : MeasurableSet s'
ht : MeasurableSet (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s')
hC : NullMeasurableSet (s ∩ s') μ
⊢ NullMeasurableSet
    (image (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s'))
    μ

Tactic:
rw [Subtype.image_preimage_coe]

Premises used: Subtype.image_preimage_coe
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set (↑s : Type u_2)
hs : NullMeasurableSet s μ
s' : Set α
hs' : MeasurableSet s'
ht : MeasurableSet (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s')
⊢ NullMeasurableSet (s ∩ s') μ

Tactic:
hs.inter (hs'.nullMeasurableSet)

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.NullMeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set (↑s : Type u_2)
hs : NullMeasurableSet s μ
s' : Set α
hs' : MeasurableSet s'
ht : MeasurableSet (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s')
⊢ NullMeasurableSet (s ∩ s') μ

Tactic:
exact hs.inter (hs'.nullMeasurableSet)

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.NullMeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set (↑s : Type u_2)
hs : NullMeasurableSet s μ
⊢ NullMeasurableSet (image (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) ∅) μ

Tactic:
simp only [image_empty, nullMeasurableSet_empty]

Premises used: MeasureTheory.nullMeasurableSet_empty, Set.image_empty
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set (↑s : Type u_2)
hs : NullMeasurableSet s μ
t' : Set (↑s : Type u_2)
ht : MeasurableSet t'
ht' : NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t') μ
compl : NullMeasurableSet (s \ (fun (a : { x : α // x ∈ s }) ↦ (↑a : α)) '' t') μ
⊢ NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t'ᶜ) μ

Tactic:
simp only [← range_diff_image Subtype.coe_injective, Subtype.range_coe_subtype, setOf_mem_eq]

Premises used: Set.range_diff_image, Subtype.range_coe_subtype, Subtype.coe_injective, Set.setOf_mem_eq
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set (↑s : Type u_2)
hs : NullMeasurableSet s μ
t' : Set (↑s : Type u_2)
ht : MeasurableSet t'
ht' : NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t') μ
⊢ NullMeasurableSet (s \ (fun (a : { x : α // x ∈ s }) ↦ (↑a : α)) '' t') μ

Tactic:
hs.diff ht'

Premises used: MeasureTheory.NullMeasurableSet.diff
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set (↑s : Type u_2)
hs : NullMeasurableSet s μ
t' : Set (↑s : Type u_2)
ht : MeasurableSet t'
ht' : NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t') μ
⊢ NullMeasurableSet (s \ (fun (a : { x : α // x ∈ s }) ↦ (↑a : α)) '' t') μ

Tactic:
exact hs.diff ht'

Premises used: MeasureTheory.NullMeasurableSet.diff
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set (↑s : Type u_2)
hs : NullMeasurableSet s μ
f : ℕ → Set (↑s : Type u_2)
hs_1 : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' f n) μ
iUnion : NullMeasurableSet (⋃ (i : ℕ), Subtype.val (p := fun (x : α) ↦ x ∈ s) '' f i) μ
⊢ NullMeasurableSet (image (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (⋃ (i : ℕ), f i)) μ

Tactic:
rw [image_iUnion]

Premises used: Set.image_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set (↑s : Type u_2)
hs : NullMeasurableSet s μ
f : ℕ → Set (↑s : Type u_2)
hs_1 : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' f n) μ
⊢ NullMeasurableSet (⋃ (i : ℕ), Subtype.val (p := fun (x : α) ↦ x ∈ s) '' f i) μ

Tactic:
.iUnion hf

Premises used: MeasureTheory.NullMeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set (↑s : Type u_2)
hs : NullMeasurableSet s μ
f : ℕ → Set (↑s : Type u_2)
hs_1 : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' f n) μ
⊢ NullMeasurableSet (⋃ (i : ℕ), Subtype.val (p := fun (x : α) ↦ x ∈ s) '' f i) μ

Tactic:
exact .iUnion hf
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set (↑s : Type u_2)
hs : NullMeasurableSet s μ
ht : MeasurableSet t
hC :
  ∀ (t' : Set (↑s : Type u_2))
    (ht' :
      Membership.mem (γ := Set (Set (↑s : Type u_2)))
        {t : Set { x : α // x ∈ s } |
          ∃ (s_1 : Set α), MeasurableSet s_1 ∧ Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s_1 = t}
        t'),
    MeasurableSet t' → NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t') μ
empty : NullMeasurableSet (image (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) ∅) μ
compl :
  ∀ (t' : Set (↑s : Type u_2)),
    MeasurableSet t' →
      ∀ (ht' : NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t') μ),
        NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t'ᶜ) μ
iUnion :
  ∀ (f : ℕ → Set (↑s : Type u_2)),
    (∀ (n : ℕ), MeasurableSet (f n)) →
      ∀ (hf : ∀ (n : ℕ), NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' f n) μ),
        NullMeasurableSet (image (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (⋃ (i : ℕ), f i)) μ
⊢ NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) μ

Tactic:
induction t, ht using generateFrom_induction with
  | hC t' ht' =>
    obtain ⟨s', hs', rfl⟩ := ht'
    rw [Subtype.image_preimage_coe]
    exact hs.inter (hs'.nullMeasurableSet)
  | empty => simp only [image_empty, nullMeasurableSet_empty]
  | compl t' _ ht' =>
    simp only [← range_diff_image Subtype.coe_injective, Subtype.range_coe_subtype, setOf_mem_eq]
    exact hs.diff ht'
  | iUnion f _ hf =>
    dsimp only []
    rw [image_iUnion]
    exact .iUnion hf

Premises used: Compl.compl, Subtype.image_preimage_coe, Set.range_diff_image, MeasureTheory.nullMeasurableSet_empty, Subtype.range_coe_subtype, Set.image_iUnion, Subtype.coe_injective, Set.setOf_mem_eq, Set.iUnion, rfl, Set.image_empty
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set (↑s : Type u_2)
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ)
⊢ NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) μ

Tactic:
NullMeasurableSet.image _ μ Subtype.coe_injective
    (fun _ => MeasurableSet.nullMeasurableSet_subtype_coe hs) ht

Premises used: MeasureTheory.Measure.MeasurableSet.nullMeasurableSet_subtype_coe, Subtype.coe_injective, MeasureTheory.Measure.NullMeasurableSet.image
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set (↑s : Type u_2)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) : ℝ≥0∞)
    (((comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ : Measure { x : α // x ∈ s }) :
          (a : Set { x : α // x ∈ s }) → ℝ≥0∞)
        t :
      ℝ≥0∞)

Tactic:
le_comap_apply _ _ Subtype.coe_injective (fun _ =>
    MeasurableSet.nullMeasurableSet_subtype_coe hs) _

Premises used: MeasureTheory.Measure.le_comap_apply, MeasureTheory.Measure.MeasurableSet.nullMeasurableSet_subtype_coe, Subtype.coe_injective
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set (↑s : Type u_2)
ht :
  Eq (α := ℝ≥0∞)
    (((comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ : Measure { x : α // x ∈ s }) :
          (a : Set { x : α // x ∈ s }) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
eq_bot_iff.mpr <| (measure_subtype_coe_le_comap hs t).trans ht.le

Premises used: Iff.mpr, MeasureTheory.Measure.measure_subtype_coe_le_comap, Eq.le, LE.le.trans, eq_bot_iff
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
δ : Type u_4
u : Set δ
inst : MeasureSpace δ
⊢ Eq.{u_4 + 1} (α := Measure (↑u : Type u_4)) volume (comap (Subtype.val (p := fun (x : δ) ↦ x ∈ u)) volume)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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))
rw₂ :
  ∀ (s : Set { x : δ // x ∈ u }),
    MeasurableSet s → NullMeasurableSet (Subtype.val (p := fun (x : δ) ↦ x ∈ u) '' s) volume
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (↑u : Type u_4)) : (a : Set (↑u : Type u_4)) → ℝ≥0∞) univ : ℝ≥0∞)
    (((volume : Measure δ) : (a : Set δ) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
rw [Subtype.volume_def, comap_apply₀ _ _ _ _ MeasurableSet.univ.nullMeasurableSet]

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.Measure.Subtype.volume_def, MeasureTheory.Measure.comap_apply₀, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
δ : Type u_4
u : Set δ
inst : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ 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∞)

Tactic:
simp only [image_univ, Subtype.range_coe_subtype, setOf_mem_eq]

Premises used: Set.image_univ, Subtype.range_coe_subtype, Set.setOf_mem_eq
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
δ : Type u_4
u : Set δ
inst : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ Injective.{u_4 + 1, u_4 + 1} (α := { x : δ // x ∈ u }) (Subtype.val (p := fun (x : δ) ↦ x ∈ u))

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
δ : Type u_4
u : Set δ
inst : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ Injective.{u_4 + 1, u_4 + 1} (α := { x : δ // x ∈ u }) (Subtype.val (p := fun (x : δ) ↦ x ∈ u))

Tactic:
exact Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
δ : Type u_4
u : Set δ
inst : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ ∀ (s : Set { x : δ // x ∈ u }),
    MeasurableSet s → NullMeasurableSet (Subtype.val (p := fun (x : δ) ↦ x ∈ u) '' s) volume

Tactic:
fun t => MeasurableSet.nullMeasurableSet_subtype_coe hu

Premises used: MeasureTheory.Measure.MeasurableSet.nullMeasurableSet_subtype_coe
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
δ : Type u_4
u : Set δ
inst : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ ∀ (s : Set { x : δ // x ∈ u }),
    MeasurableSet s → NullMeasurableSet (Subtype.val (p := fun (x : δ) ↦ x ∈ u) '' s) volume

Tactic:
exact fun t => MeasurableSet.nullMeasurableSet_subtype_coe hu

Premises used: MeasureTheory.Measure.MeasurableSet.nullMeasurableSet_subtype_coe
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
δ : Type u_4
u : Set δ
inst : MeasureSpace δ
hu : NullMeasurableSet u volume
t : Set (↑u : Type u_4)
⊢ LE.le (α := ℝ≥0∞) (((volume : Measure δ) : (a : Set δ) → ℝ≥0∞) (Subtype.val (p := fun (x : δ) ↦ x ∈ u) '' t) : ℝ≥0∞)
    (((volume : Measure (↑u : Type u_4)) : (a : Set (↑u : Type u_4)) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
measure_subtype_coe_le_comap hu t

Premises used: MeasureTheory.Measure.measure_subtype_coe_le_comap
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
δ : Type u_4
u : Set δ
inst : MeasureSpace δ
hu : NullMeasurableSet u volume
t : Set (↑u : Type u_4)
ht : Eq (α := ℝ≥0∞) (((volume : Measure (↑u : Type u_4)) : (a : Set (↑u : Type u_4)) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((volume : Measure δ) : (a : Set δ) → ℝ≥0∞) (Subtype.val (p := fun (x : δ) ↦ x ∈ u) '' t) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
measure_subtype_coe_eq_zero_of_comap_eq_zero hu ht

Premises used: MeasureTheory.Measure.measure_subtype_coe_eq_zero_of_comap_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
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∞)
⊢ Measure.map f (Measure.comap f μ) = μ.restrict (range f)

Tactic:
ext1 t ht
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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∞)
h₃ h₄ : Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (t ∩ range f) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (t ∩ range f) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.map f (Measure.comap f μ) : Measure β) : (a : Set β) → ℝ≥0∞) 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]

Premises used: MeasureTheory.Measure.restrict_apply, MeasurableEmbedding.measurableSet_image', MeasureTheory.Measure.comap_apply, Set.image_preimage_eq_inter_range, MeasurableEmbedding.injective, MeasurableEmbedding.map_apply, MeasurableEmbedding.measurable
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set α
rw rw₁ :
  Eq (α := ℝ≥0∞) (((Measure.comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' s) : ℝ≥0∞)

Tactic:
rw [hf.injective.preimage_image]

Premises used: MeasurableEmbedding.injective, Function.Injective.preimage_image
-- 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∞) ((μ.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∞)
rw₂ rw₃ : Eq (α := ℝ≥0∞) ((μ : (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∞)

Tactic:
rw [hf.map_comap, restrict_apply' hf.measurableSet_range,
        inter_eq_self_of_subset_left (image_subset_range _ _)]

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

Tactic:
ext t _
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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∞)
h₂ h₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) 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∞)

Tactic:
rw [hf.comap_apply, hf.map_apply, preimage_image_eq _ hf.injective]

Premises used: MeasurableEmbedding.comap_apply, MeasurableEmbedding.injective, MeasurableEmbedding.map_apply, Set.preimage_image_eq
-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
p : β → Prop
μ : Measure α
⊢ (∀ᵐ (x : β) ∂Measure.map f μ, p x) ↔ ∀ᵐ (x : α) ∂μ, p (f x)

Tactic:
simp only [ae_iff, hf.map_apply, preimage_setOf_eq]

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

Tactic:
simp [hf.map_apply, ht, hf.measurable ht]

Premises used: MeasurableEmbedding.map_apply, MeasurableEmbedding.measurable