awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | p x k}
k : ℕ
hk : k ≤ N
simp :
  MeasurableSet.{u_1} (α := α)
    ({a : α | k ≤ N} ∩ ((⋂ (_ : k ≠ 0), {x : α | p x k}) ∩ ⋂ (i : ℕ), ⋂ (_ : k < i), ⋂ (_ : i ≤ N), {a : α | p a i}ᶜ))
⊢ MeasurableSet.{u_1} (α := α) {x : α | Nat.findGreatest (p x) N = k}

Tactic:
simp only [Nat.findGreatest_eq_iff, setOf_and, setOf_forall, ← compl_setOf]

Premises used: Set.setOf_and, Set.setOf_forall, Nat.findGreatest_eq_iff, Set.compl_setOf
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | p x k}
k : ℕ
hk : k ≤ N
h₂ : ∀ (b : k ≠ 0), MeasurableSet.{u_1} (α := α) {x : α | p x k}
h₃ : ∀ (b : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
⊢ MeasurableSet.{u_1} (α := α)
    ({a : α | k ≤ N} ∩ ((⋂ (_ : k ≠ 0), {x : α | p x k}) ∩ ⋂ (i : ℕ), ⋂ (_ : k < i), ⋂ (_ : i ≤ N), {a : α | p a i}ᶜ))

Tactic:
apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter,
    MeasurableSet.compl, hN]

Premises used: MeasurableSet.compl, MeasurableSet.const, MeasurableSet.iInter, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | p x k}
k : ℕ
hk : k ≤ N
h₂ : k ≠ 0 → MeasurableSet.{u_1} (α := α) {x : α | p x k}
⊢ ∀ (b : k ≠ 0), MeasurableSet.{u_1} (α := α) {x : α | p x k}

Tactic:
try intros
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | p x k}
k : ℕ
hk : k ≤ N
h₂ : ∀ (b : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
⊢ ∀ (b : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)

Tactic:
try intros
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | p x k}
k : ℕ
hk : k ≤ N
b : k ≠ 0
⊢ MeasurableSet.{u_1} (α := α) {x : α | p x k}

Tactic:
apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter,
    MeasurableSet.compl, hN]

Premises used: MeasurableSet.compl, MeasurableSet.const, MeasurableSet.iInter, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | p x k}
k : ℕ
hk : k ≤ N
b : ℕ
h₂ : ∀ (b_1 : k < b), MeasurableSet.{u_1} (α := α) (⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
⊢ MeasurableSet.{u_1} (α := α) (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)

Tactic:
apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter,
    MeasurableSet.compl, hN]

Premises used: MeasurableSet.compl, MeasurableSet.const, MeasurableSet.iInter, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | p x k}
k : ℕ
hk : k ≤ N
b : ℕ
h₂ : k < b → MeasurableSet.{u_1} (α := α) (⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
⊢ ∀ (b_1 : k < b), MeasurableSet.{u_1} (α := α) (⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)

Tactic:
try intros
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | p x k}
k : ℕ
hk : k ≤ N
b : ℕ
b_1 : k < b
h₂ : ∀ (b_2 : b ≤ N), MeasurableSet.{u_1} (α := α) {a : α | p a b}ᶜ
⊢ MeasurableSet.{u_1} (α := α) (⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)

Tactic:
apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter,
    MeasurableSet.compl, hN]

Premises used: MeasurableSet.compl, MeasurableSet.const, MeasurableSet.iInter, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | p x k}
k : ℕ
hk : k ≤ N
b : ℕ
b_1 : k < b
h₂ : b ≤ N → MeasurableSet.{u_1} (α := α) {a : α | p a b}ᶜ
⊢ ∀ (b_2 : b ≤ N), MeasurableSet.{u_1} (α := α) {a : α | p a b}ᶜ

Tactic:
try intros
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | p x k}
k : ℕ
hk : k ≤ N
b : ℕ
b_1 : k < b
b_2 : b ≤ N
⊢ MeasurableSet.{u_1} (α := α) {a : α | p a b}ᶜ

Tactic:
apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter,
    MeasurableSet.compl, hN]

Premises used: MeasurableSet.compl, MeasurableSet.const, MeasurableSet.iInter, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | p x k}
k : ℕ
hk : k ≤ N
h₂ : ∀ (b : k ≠ 0), MeasurableSet.{u_1} (α := α) {x : α | p x k}
h₃ : ∀ (b : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
h₄ : ∀ (b : k ≠ 0), MeasurableSet.{u_1} (α := α) {x : α | p x k}
h₅ : ∀ (b : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
h₆ : ∀ (b : k ≠ 0), MeasurableSet.{u_1} (α := α) {x : α | p x k}
h₇ : ∀ (b : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
h₈ : ∀ (b : k ≠ 0), MeasurableSet.{u_1} (α := α) {x : α | p x k}
h₉ : ∀ (b : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
h₁₀ : k ≠ 0 → MeasurableSet.{u_1} (α := α) {x : α | p x k}
h₁₁ : ∀ (b : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
h₁₂ : ∀ (b : ℕ), k < b → MeasurableSet.{u_1} (α := α) (⋂ (_ : b ≤ N), {a : α | p a b}ᶜ)
h₁₃ : ∀ (b : ℕ), k < b → b ≤ N → MeasurableSet.{u_1} (α := α) {a : α | p a b}ᶜ
⊢ MeasurableSet.{u_1} (α := α)
    ({a : α | k ≤ N} ∩ ((⋂ (_ : k ≠ 0), {x : α | p x k}) ∩ ⋂ (i : ℕ), ⋂ (_ : k < i), ⋂ (_ : i ≤ N), {a : α | p a i}ᶜ))

Tactic:
repeat' apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter,
    MeasurableSet.compl, hN] <;> try intros

Premises used: MeasurableSet.compl, MeasurableSet.const, MeasurableSet.iInter, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
n : ℕ
⊢ MeasurableSet (disjointed f n)

Tactic:
disjointedRec (fun _ _ ht => MeasurableSet.diff ht <| h _) (h n)

Premises used: MeasurableSet.diff, disjointedRec
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ (N : ℕ), p x N
hm : ∀ (k : ℕ), MeasurableSet.{u_1} (α := α) {x : α | p x k}
⊢ Measurable (β := ℕ) fun (x : α) ↦ Nat.find (p := p x) ⋯

Tactic:
measurable_to_nat fun x => ?_

Premises used: measurable_to_nat
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ (N : ℕ), p x N
hm : ∀ (k : ℕ), MeasurableSet.{u_1} (α := α) {x : α | p x k}
refine :
  ∀ (x : α),
    MeasurableSet.{u_1} (α := α) (preimage (β := ℕ) (fun (x : α) ↦ Nat.find (p := p x) ⋯) {Nat.find (p := p x) ⋯})
⊢ Measurable (β := ℕ) fun (x : α) ↦ Nat.find (p := p x) ⋯

Tactic:
refine measurable_to_nat fun x => ?_

Premises used: measurable_to_nat
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ (N : ℕ), p x N
hm : ∀ (k : ℕ), MeasurableSet.{u_1} (α := α) {x : α | p x k}
x : α
rw : MeasurableSet.{u_1} (α := α) (disjointed (fun (k : ℕ) ↦ {x : α | p x k}) (Nat.find (p := p x) ⋯))
⊢ MeasurableSet.{u_1} (α := α) (preimage (β := ℕ) (fun (x : α) ↦ Nat.find (p := p x) ⋯) {Nat.find (p := p x) ⋯})

Tactic:
rw [preimage_find_eq_disjointed (fun k => {x | p x k})]

Premises used: setOf, preimage_find_eq_disjointed
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ (N : ℕ), p x N
hm : ∀ (k : ℕ), MeasurableSet.{u_1} (α := α) {x : α | p x k}
x : α
⊢ MeasurableSet.{u_1} (α := α) (disjointed (fun (k : ℕ) ↦ {x : α | p x k}) (Nat.find (p := p x) ⋯))

Tactic:
MeasurableSet.disjointed hm _

Premises used: MeasurableSet.disjointed
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ (N : ℕ), p x N
hm : ∀ (k : ℕ), MeasurableSet.{u_1} (α := α) {x : α | p x k}
x : α
⊢ MeasurableSet.{u_1} (α := α) (disjointed (fun (k : ℕ) ↦ {x : α | p x k}) (Nat.find (p := p x) ⋯))

Tactic:
exact MeasurableSet.disjointed hm _

Premises used: MeasurableSet.disjointed
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Setoid α
t : Set (Quotient s)
⊢ MeasurableSet t ↔ MeasurableSet (Quotient.mk'' ⁻¹' t)

Tactic:
Iff.rfl

Premises used: MeasurableSet, Iff.rfl, setOf, Quotient, Set.preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
s : Setoid α
f : Quotient s → β
⊢ Measurable f ↔ Measurable (f ∘ Quotient.mk'')

Tactic:
Iff.rfl

Premises used: MeasurableSet, Set.Mem, Iff.rfl, Measurable, setOf, Quotient, Set.preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Setoid α
⊢ Measurable.{u_1, u_1} (α := α) (β := Quotient s) Quotient.mk'

Tactic:
fun _ => id

Premises used: MeasurableSet, Measurable, setOf, id, Quotient, Set.preimage, Quotient.mk'
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Setoid α
⊢ Measurable.{u_1, u_1} (α := α) (β := Quotient s) Quotient.mk''

Tactic:
fun _ => id

Premises used: MeasurableSet, Measurable, setOf, id, Quotient, Set.preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : MeasurableSpace α
r : α → α → Prop
⊢ Measurable (Quot.mk r)

Tactic:
fun _ => id

Premises used: MeasurableSet, Measurable, setOf, id, Set.preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
G : Type u_6
inst : Group G
inst_1 : MeasurableSpace G
S : Subgroup G
⊢ Measurable.{u_6, u_6} (α := G) (β := G ⧸ S) mk

Tactic:
measurable_quotient_mk''

Premises used: measurable_quotient_mk''
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : MeasurableSpace α
G : Type u_6
inst_1 : Group G
inst_2 : MeasurableSpace G
S : Subgroup G
f : G ⧸ S → α
⊢ Measurable f ↔ Measurable (f ∘ mk)

Tactic:
measurable_from_quotient

Premises used: measurable_from_quotient
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
G : Type u_6
inst_2 : Group G
inst_3 : MeasurableSpace G
inst_4 : DiscreteMeasurableSpace G
S : Subgroup G
⊢ DiscreteMeasurableSpace.{u_6} (G ⧸ S)

Tactic:
Quotient.instDiscreteMeasurableSpace

Premises used: Quotient.instDiscreteMeasurableSpace
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : MeasurableSpace α
p : α → Prop
⊢ Measurable.{u_1, u_1} (α := Subtype p) (Subtype.val (p := p))

Tactic:
MeasurableSpace.le_map_comap

Premises used: MeasurableSet, Measurable, setOf, Set.preimage, MeasurableSpace.le_map_comap
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst : MeasurableSpace α
p : α → Prop
inst_1 : MeasurableSingletonClass α
x : Subtype p
rw : Eq (α := Set (Subtype p)) (val (p := p) ⁻¹' image (α := Subtype p) (val (p := p)) {x}) {x}
rw₁ rw₂ : Eq (α := Set (Subtype p)) {x} {x}
⊢ Eq (α := Set (Subtype p)) (val (p := p) ⁻¹' {(↑x : α)}) {x}

Tactic:
rw [← image_singleton, preimage_image_eq _ Subtype.val_injective]

Premises used: Set.image_singleton, Subtype.val_injective, Set.preimage_image_eq
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
t : Set (↑s : Type u_1)
h : MeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
⊢ MeasurableSet t

Tactic:
⟨_, h, preimage_image_eq _ Subtype.val_injective⟩

Premises used: MeasurableSet, Subtype.val_injective, And.intro, Exists.intro, Set.preimage_image_eq
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
u : Set α
hu : MeasurableSet u
rw : MeasurableSet (s ∩ u)
⊢ MeasurableSet
    (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u))

Tactic:
rw [Subtype.image_preimage_coe]

Premises used: Subtype.image_preimage_coe
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (s ∩ u)

Tactic:
hs.inter hu

Premises used: MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (s ∩ u)

Tactic:
exact hs.inter hu

Premises used: MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
p : β → Prop
f : α → Subtype p
hf : Measurable f
⊢ Measurable.{u_1, u_2} (β := β) fun (a : α) ↦ (↑(f a) : β)

Tactic:
measurable_subtype_coe.comp hf

Premises used: measurable_subtype_coe, Measurable.comp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
p : β → Prop
f : α → β
hf : Measurable f
h : ∀ (x : α), p (f x)
t : Set (Subtype p)
h_1 : MeasurableSet t
s : Set β
hs : MeasurableSet s ∧ Subtype.val (p := p) ⁻¹' s = t
⊢ MeasurableSet.{u_1} (α := α)
    (preimage (β := Subtype p) (fun (x : α) ↦ Subtype.mk (p := p) (f x) ⋯) (Subtype.val (p := p) ⁻¹' s))

Tactic:
simp only [← preimage_comp, Function.comp_def, hf hs.1]

Premises used: Set.preimage_comp, Function.comp_def, And.left
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set β
f : α → β
hf : Measurable f
h : ∀ (y : α), f y ∈ s
⊢ Measurable (Set.codRestrict f s h)

Tactic:
hf.subtype_mk

Premises used: Measurable.subtype_mk, Set.codRestrict
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
⊢ Measurable (rangeFactorization f)

Tactic:
hf.subtype_mk

Premises used: Measurable.subtype_mk, Set.rangeFactorization
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
p : α → Prop
q : β → Prop
hf : Measurable f
hpq : ∀ (x : α), p x → q (f x)
⊢ Measurable (Subtype.map (p := p) (q := q) f hpq)

Tactic:
(hf.comp measurable_subtype_coe).subtype_mk

Premises used: measurable_subtype_coe, Subtype.map, Measurable.comp, Measurable.subtype_mk
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
⊢ Measurable (inclusion (s := s) (t := t) h)

Tactic:
measurable_id.subtype_map h

Premises used: Subtype.map, measurable_id, Measurable.subtype_map
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
u : Set (↑s : Type u_1)
hs : MeasurableSet (α := (↑t : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' s)
hu : MeasurableSet u
rcases :
  ∀ (u : Set α) (hu : MeasurableSet u),
    MeasurableSet (inclusion (s := s) (t := t) h '' Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
⊢ MeasurableSet (inclusion (s := s) (t := t) h '' u)

Tactic:
rcases hu with ⟨u, hu, rfl⟩

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
hs : MeasurableSet (α := (↑t : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' s)
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (α := { x : α // x ∈ t })
    (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' u ∩ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' s)

Tactic:
(measurable_subtype_coe hu).inter hs

Premises used: measurable_subtype_coe, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
hs : MeasurableSet (α := (↑t : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' s)
u : Set α
hu : MeasurableSet u
h₁ :
  inclusion (s := s) (t := t) h '' Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u =
    Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' u ∩ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' s
⊢ MeasurableSet (inclusion (s := s) (t := t) h '' Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)

Tactic:
convert! (measurable_subtype_coe hu).inter hs

Premises used: measurable_subtype_coe, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
hs : MeasurableSet (α := (↑t : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' s)
u : Set α
hu : MeasurableSet u
h₁ :
  ∀ (x : α) (hx : x ∈ t),
    Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hx ∈
        inclusion (s := s) (t := t) h '' Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u ↔
      Membership.mem (γ := Set (↑t : Type u_1))
        (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' u ∩ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' s)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hx)
⊢ inclusion (s := s) (t := t) h '' Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u =
    Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' u ∩ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' s

Tactic:
ext ⟨x, hx⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
hs : MeasurableSet (α := (↑t : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' s)
u : Set α
hu : MeasurableSet u
x : α
hx : x ∈ t
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hx ∈
      inclusion (s := s) (t := t) h '' Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u ↔
    Membership.mem (γ := Set (↑t : Type u_1))
      (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' u ∩ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' s)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hx)

Tactic:
simpa [@and_comm _ (_ = x)] using and_comm

Premises used: and_comm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
u : Set (↑s : Type u_1)
hs : MeasurableSet s
hu : MeasurableSet u
⊢ MeasurableSet (inclusion (s := s) (t := t) h '' u)

Tactic:
(measurable_subtype_coe hs).image_inclusion' h hu

Premises used: measurable_subtype_coe, MeasurableSet.image_inclusion'
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
m : MeasurableSpace α
s t u : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hsu : MeasurableSet (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
htu : MeasurableSet (α := { x : α // x ∈ t }) (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' u)
⊢ MeasurableSet
    (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) ∪
      image (α := { x : α // x ∈ t }) (Subtype.val (p := fun (x : α) ↦ x ∈ t))
        (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' u))

Tactic:
(hs.subtype_image hsu).union (ht.subtype_image htu)

Premises used: MeasurableSet.subtype_image, MeasurableSet.union
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
m : MeasurableSpace α
s t u : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hsu : MeasurableSet (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
htu : MeasurableSet (α := { x : α // x ∈ t }) (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' u)
h₁ :
  u =
    image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) ∪
      image (α := { x : α // x ∈ t }) (Subtype.val (p := fun (x : α) ↦ x ∈ t))
        (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' u)
⊢ MeasurableSet u

Tactic:
convert! (hs.subtype_image hsu).union (ht.subtype_image htu)

Premises used: MeasurableSet.subtype_image, MeasurableSet.union
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
m : MeasurableSpace α
s t u : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hsu : MeasurableSet (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
htu : MeasurableSet (α := { x : α // x ∈ t }) (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' u)
⊢ u =
    image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) ∪
      image (α := { x : α // x ∈ t }) (Subtype.val (p := fun (x : α) ↦ x ∈ t))
        (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' u)

Tactic:
simp [image_preimage_eq_inter_range, ← inter_union_distrib_left, univ_subset_iff.1 h]

Premises used: Set.univ_subset_iff, Set.image_preimage_eq_inter_range, Iff.mp, Set.inter_union_distrib_left
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : Measurable.{u_1, u_2} (β := β) fun (a : (↑s : Type u_1)) ↦ f (↑a : α)
hd : Measurable.{u_1, u_2} (β := β) fun (a : (↑t : Type u_1)) ↦ f (↑a : α)
⊢ Measurable f

Tactic:
fun _u hu =>
  .of_union_cover hs ht h (hc hu) (hd hu)

Premises used: Measurable, MeasurableSet.of_union_cover
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
s : Set α
hs : MeasurableSet s
h₁ : Measurable (s.restrict (π := fun (a : α) ↦ β) f)
h₂ : Measurable (sᶜ.restrict (π := fun (a : α) ↦ β) f)
⊢ Measurable f

Tactic:
measurable_of_measurable_union_cover s sᶜ hs hs.compl (union_compl_self s).ge h₁ h₂

Premises used: Eq.ge, Compl.compl, Set.union_compl_self, MeasurableSet.compl, measurable_of_measurable_union_cover
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : (x : α) → Decidable (x ∈ s)
f : (↑s : Type u_1) → β
hf : Measurable f
g : (↑sᶜ : Type u_1) → β
hg : Measurable g
hs : MeasurableSet s
⊢ Measurable.{u_1, u_2} (α := (↑s : Type u_1)) (β := β)
    (s.restrict (π := fun (a : α) ↦ β) fun (x : α) ↦
      if hx : x ∈ s then f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
      else g (Subtype.mk (p := fun (x : α) ↦ x ∈ sᶜ) x hx))

Tactic:
simpa