-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem MeasurableSet.nullMeasurableSet_subtype_coe {t : Set s} (hs : NullMeasurableSet s μ)
    (ht : MeasurableSet t) : NullMeasurableSet ((↑) '' t) μ

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set ↑s
hs : NullMeasurableSet s μ
ht : MeasurableSet t
⊢ NullMeasurableSet (Subtype.val '' 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

Result:
no goals

Proof state:
case hC
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set ↑s
hs : NullMeasurableSet s μ
t' : Set ↑s
ht' : t' ∈ {t | ∃ s_1, MeasurableSet s_1 ∧ Subtype.val ⁻¹' s_1 = t}
ht✝ : MeasurableSet t'
⊢ NullMeasurableSet (Subtype.val '' t') μ

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

Result:
case hC.intro.intro
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set ↑s
hs : NullMeasurableSet s μ
s' : Set α
hs' : MeasurableSet s'
ht✝ : MeasurableSet (Subtype.val ⁻¹' s')
⊢ NullMeasurableSet (Subtype.val '' (Subtype.val ⁻¹' s')) μ

Proof state:
case compl
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set ↑s
hs : NullMeasurableSet s μ
t' : Set ↑s
ht✝ : MeasurableSet t'
ht' : NullMeasurableSet (Subtype.val '' t') μ
⊢ NullMeasurableSet (Subtype.val '' t'ᶜ) μ

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

Result:
case compl
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set ↑s
hs : NullMeasurableSet s μ
t' : Set ↑s
ht✝ : MeasurableSet t'
ht' : NullMeasurableSet (Subtype.val '' t') μ
⊢ NullMeasurableSet (s \ (fun a => ↑a) '' t') μ

Proof state:
case hC.intro.intro
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set ↑s
hs : NullMeasurableSet s μ
s' : Set α
hs' : MeasurableSet s'
ht✝ : MeasurableSet (Subtype.val ⁻¹' s')
⊢ NullMeasurableSet (s ∩ s') μ

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

Result:
no goals

Proof state:
case compl
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set ↑s
hs : NullMeasurableSet s μ
t' : Set ↑s
ht✝ : MeasurableSet t'
ht' : NullMeasurableSet (Subtype.val '' t') μ
⊢ NullMeasurableSet (s \ (fun a => ↑a) '' t') μ

Tactic:
exact hs.diff ht'

Result:
no goals

Proof state:
case hC.intro.intro
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set ↑s
hs : NullMeasurableSet s μ
s' : Set α
hs' : MeasurableSet s'
ht✝ : MeasurableSet (Subtype.val ⁻¹' s')
⊢ NullMeasurableSet (Subtype.val '' (Subtype.val ⁻¹' s')) μ

Tactic:
rw [Subtype.image_preimage_coe]

Result:
case hC.intro.intro
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set ↑s
hs : NullMeasurableSet s μ
s' : Set α
hs' : MeasurableSet s'
ht✝ : MeasurableSet (Subtype.val ⁻¹' s')
⊢ NullMeasurableSet (s ∩ s') μ

Proof state:
case iUnion
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set ↑s
hs : NullMeasurableSet s μ
f : ℕ → Set ↑s
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), NullMeasurableSet (Subtype.val '' f n) μ
⊢ NullMeasurableSet (⋃ i, Subtype.val '' f i) μ

Tactic:
exact .iUnion hf

Result:
no goals

Proof state:
case iUnion
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set ↑s
hs : NullMeasurableSet s μ
f : ℕ → Set ↑s
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), NullMeasurableSet (Subtype.val '' f n) μ
⊢ NullMeasurableSet (Subtype.val '' ⋃ i, f i) μ

Tactic:
rw [image_iUnion]

Result:
case iUnion
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set ↑s
hs : NullMeasurableSet s μ
f : ℕ → Set ↑s
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), NullMeasurableSet (Subtype.val '' f n) μ
⊢ NullMeasurableSet (⋃ i, Subtype.val '' f i) μ

Proof state:
case empty
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set ↑s
hs : NullMeasurableSet s μ
⊢ NullMeasurableSet (Subtype.val '' ∅) μ

Tactic:
simp only [image_empty, nullMeasurableSet_empty]

Result:
no goals