awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (i : δ) → MeasurableSpace (X i)
inst_1 : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : ¬j = i
neg : Measurable (β := X j) fun (v : TProd X (i :: is)) ↦ TProd.elim (α := X) v.2 ⋯
⊢ Measurable (β := X j) fun (v : TProd X (i :: is)) ↦ v.elim (α := X) hj

Tactic:
simp only [TProd.elim_of_ne _ hji]

Premises used: List.TProd.elim_of_ne
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (i : δ) → MeasurableSpace (X i)
inst_1 : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : ¬j = i
neg :
  ∀ (hj_1 : j = i ∨ j ∈ is) (hji : ¬j = i),
    Measurable (β := X j) fun (v : TProd X (i :: is)) ↦ TProd.elim (α := X) v.2 ⋯
⊢ Measurable (β := X j) fun (v : TProd X (i :: is)) ↦ TProd.elim (α := X) v.2 ⋯

Tactic:
rw [mem_cons] at hj

Premises used: List.mem_cons
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (i : δ) → MeasurableSpace (X i)
inst_1 : DecidableEq δ
i : δ
is : List δ
j : δ
hj_1 : j ∈ i :: is
hj : j = i ∨ j ∈ is
hji : ¬j = i
⊢ Measurable (β := X j) fun (v : TProd X (i :: is)) ↦ TProd.elim (α := X) v.2 ⋯

Tactic:
(measurable_tProd_elim (hj.resolve_left hji)).comp measurable_snd

Premises used: Measurable.comp, Or.resolve_left, measurable_snd
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (i : δ) → MeasurableSpace (X i)
inst_1 : DecidableEq δ
i : δ
is : List δ
j : δ
hj_1 : j ∈ i :: is
hj : j = i ∨ j ∈ is
hji : ¬j = i
⊢ Measurable (β := X j) fun (v : TProd X (i :: is)) ↦ TProd.elim (α := X) v.2 ⋯

Tactic:
exact (measurable_tProd_elim (hj.resolve_left hji)).comp measurable_snd

Premises used: Measurable.comp, Or.resolve_left, measurable_snd
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (i : δ) → MeasurableSpace (X i)
inst_1 : DecidableEq δ
l : List δ
h : ∀ (i : δ), i ∈ l
⊢ Measurable (α := TProd X l) (TProd.elim' (α := X) h)

Tactic:
measurable_pi_lambda _ fun i => measurable_tProd_elim (h i)

Premises used: measurable_pi_lambda, measurable_tProd_elim
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (i : δ) → MeasurableSpace (X i)
s : (i : δ) → Set (X i)
hs : ∀ (i : δ), MeasurableSet (s i)
⊢ MeasurableSet (α := TProd X []) (Set.tprod (α := X) [] s)

Tactic:
MeasurableSet.univ

Premises used: Set.tprod, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (i : δ) → MeasurableSpace (X i)
s : (i : δ) → Set (X i)
hs : ∀ (i : δ), MeasurableSet (s i)
⊢ MeasurableSet (α := TProd X []) (Set.tprod (α := X) [] s)

Tactic:
exact MeasurableSet.univ

Premises used: MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (i : δ) → MeasurableSpace (X i)
s : (i : δ) → Set (X i)
hs : ∀ (i : δ), MeasurableSet (s i)
i : δ
l : List δ
ih : MeasurableSet (Set.tprod (α := X) l s)
⊢ MeasurableSet (Set.tprod (α := X) (i :: l) s)

Tactic:
(hs i).prod ih

Premises used: Set.tprod, MeasurableSet.prod, List.foldr
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (i : δ) → MeasurableSpace (X i)
s : (i : δ) → Set (X i)
hs : ∀ (i : δ), MeasurableSet (s i)
i : δ
l : List δ
ih : MeasurableSet (Set.tprod (α := X) l s)
⊢ MeasurableSet (Set.tprod (α := X) (i :: l) s)

Tactic:
exact (hs i).prod ih

Premises used: MeasurableSet.prod
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (i : δ) → MeasurableSpace (X i)
l : List δ
s : (i : δ) → Set (X i)
hs : ∀ (i : δ), MeasurableSet (s i)
nil : MeasurableSet (α := TProd X []) (Set.tprod (α := X) [] s)
cons :
  ∀ (i : δ) (l : List δ) (ih : MeasurableSet (Set.tprod (α := X) l s)), MeasurableSet (Set.tprod (α := X) (i :: l) s)
⊢ MeasurableSet (Set.tprod (α := X) l s)

Tactic:
induction l with
  | nil => exact MeasurableSet.univ
  | cons i l ih => exact (hs i).prod ih

Premises used: List.cons, MeasurableSet.univ, List.nil
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
⊢ Measurable (α := α) (β := α ⊕ β) Sum.inl

Tactic:
Measurable.of_le_map inf_le_left

Premises used: Measurable.of_le_map, inf_le_left
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
⊢ Measurable (α := β) (β := α ⊕ β) Sum.inr

Tactic:
Measurable.of_le_map inf_le_right

Premises used: Measurable.of_le_map, inf_le_right
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set (α ⊕ β)
⊢ MeasurableSet s ↔ MeasurableSet (Sum.inl ⁻¹' s) ∧ MeasurableSet (Sum.inr ⁻¹' s)

Tactic:
Iff.rfl

Premises used: MeasurableSet, Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
x : MeasurableSpace γ
f : α ⊕ β → γ
hl : Measurable (f ∘ Sum.inl)
hr : Measurable (f ∘ Sum.inr)
⊢ Measurable f

Tactic:
Measurable.of_comap_le <|
    le_inf (MeasurableSpace.comap_le_iff_le_map.2 <| hl)
      (MeasurableSpace.comap_le_iff_le_map.2 <| hr)

Premises used: Iff.mpr, Measurable.of_comap_le, le_inf, MeasurableSpace.comap_le_iff_le_map
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
x : MeasurableSpace γ
f : α → γ
g : β → γ
hf : Measurable f
hg : Measurable g
⊢ Measurable (Sum.elim f g)

Tactic:
measurable_fun_sum hf hg

Premises used: measurable_fun_sum
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
mβ : MeasurableSpace β
x : MeasurableSpace γ
x_1 : MeasurableSpace δ
f : α → β
g : γ → δ
hf : Measurable f
hg : Measurable g
⊢ Measurable (Sum.map f g)

Tactic:
(measurable_inl.comp hf).sumElim (measurable_inr.comp hg)

Premises used: measurable_inl, Sum.map, Measurable.comp, measurable_inr, Measurable.sumElim
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
⊢ MeasurableSet (α := α ⊕ β) (Sum.inl '' s) ↔ MeasurableSet s

Tactic:
simp [measurableSet_sum_iff, Sum.inl_injective.preimage_image]

Premises used: Sum.inl_injective, measurableSet_sum_iff, Function.Injective.preimage_image
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set β
⊢ MeasurableSet (α := α ⊕ β) (Sum.inr '' s) ↔ MeasurableSet s

Tactic:
simp [measurableSet_sum_iff, Sum.inr_injective.preimage_image]

Premises used: Sum.inr_injective, measurableSet_sum_iff, Function.Injective.preimage_image
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace α
rw : MeasurableSet (α := α ⊕ β) (Sum.inl '' univ)
⊢ MeasurableSet (α := α ⊕ β) (range Sum.inl)

Tactic:
rw [← image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace α
⊢ MeasurableSet (α := α ⊕ β) (Sum.inl '' univ)

Tactic:
MeasurableSet.univ.inl_image

Premises used: MeasurableSet.inl_image, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace α
⊢ MeasurableSet (α := α ⊕ β) (Sum.inl '' univ)

Tactic:
exact MeasurableSet.univ.inl_image

Premises used: MeasurableSet.inl_image, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace α
rw : MeasurableSet (α := α ⊕ β) (Sum.inr '' univ)
⊢ MeasurableSet (α := α ⊕ β) (range Sum.inr)

Tactic:
rw [← image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace α
⊢ MeasurableSet (α := α ⊕ β) (Sum.inr '' univ)

Tactic:
MeasurableSet.univ.inr_image

Premises used: MeasurableSet.inr_image, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace α
⊢ MeasurableSet (α := α ⊕ β) (Sum.inr '' univ)

Tactic:
exact MeasurableSet.univ.inr_image

Premises used: MeasurableSet.inr_image, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : MeasurableSpace α
p : α → Prop
h : MeasurableSet.{u_1} (α := α) {a : α | p a}
⊢ MeasurableSet (p ⁻¹' {True})

Tactic:
simpa only [preimage_singleton_true]

Premises used: Set.preimage_singleton_true
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : MeasurableSpace α
p : α → Prop
h : Measurable p
⊢ MeasurableSet.{u_1} (α := α) {a : α | p a}

Tactic:
simpa using h (measurableSet_singleton True)

Premises used: MeasurableSingletonClass.measurableSet_singleton, True
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
s : Set α
inst : MeasurableSpace α
⊢ (Measurable (β := Prop) fun (x : α) ↦ x ∈ s) ↔ MeasurableSet s

Tactic:
measurableSet_setOf.symm

Premises used: measurableSet_setOf, Set.Mem, setOf, Iff.symm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : MeasurableSpace α
p : α → Prop
hp : Measurable p
⊢ Measurable (β := Prop) fun (x : α) ↦ ¬p x

Tactic:
measurableSet_setOf.1 hp.setOf.compl

Premises used: measurableSet_setOf, Measurable.setOf, MeasurableSet.compl, Iff.mp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : MeasurableSpace α
p q : α → Prop
hp : Measurable p
hq : Measurable q
⊢ Measurable (β := Prop) fun (a : α) ↦ p a ∧ q a

Tactic:
measurableSet_setOf.1 <| hp.setOf.inter hq.setOf

Premises used: measurableSet_setOf, Measurable.setOf, Iff.mp, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : MeasurableSpace α
p q : α → Prop
hp : Measurable p
hq : Measurable q
⊢ Measurable (β := Prop) fun (a : α) ↦ p a ∨ q a

Tactic:
measurableSet_setOf.1 <| hp.setOf.union hq.setOf

Premises used: measurableSet_setOf, Measurable.setOf, MeasurableSet.union, Iff.mp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : MeasurableSpace α
p q : α → Prop
hp : Measurable p
hq : Measurable q
⊢ Measurable (β := Prop) fun (a : α) ↦ p a → q a

Tactic:
measurableSet_setOf.1 <| hp.setOf.himp hq.setOf

Premises used: measurableSet_setOf, Measurable.setOf, MeasurableSet.himp, Iff.mp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : MeasurableSpace α
p q : α → Prop
hp : Measurable p
hq : Measurable q
simp_rw : MeasurableSet.{u_1} (α := α) {a : α | (p a → q a) ∧ (q a → p a)}
⊢ MeasurableSet.{u_1} (α := α) {a : α | p a ↔ q a}

Tactic:
simp_rw [iff_iff_implies_and_implies]

Premises used: iff_iff_implies_and_implies
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : MeasurableSpace α
p q : α → Prop
hp : Measurable p
hq : Measurable q
⊢ MeasurableSet.{u_1} (α := α) {a : α | (p a → q a) ∧ (q a → p a)}

Tactic:
hq.setOf.bihimp hp.setOf

Premises used: Set.Mem, setOf, Measurable.setOf, Set.inter, MeasurableSet.bihimp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : MeasurableSpace α
p q : α → Prop
hp : Measurable p
hq : Measurable q
⊢ MeasurableSet.{u_1} (α := α) {a : α | (p a → q a) ∧ (q a → p a)}

Tactic:
exact hq.setOf.bihimp hp.setOf

Premises used: Measurable.setOf, MeasurableSet.bihimp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
ι : Sort uι
inst : MeasurableSpace α
inst_1 : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
rw : MeasurableSet.{u_1} (α := α) (⋂ (i : ι), {x : α | p i x})
⊢ MeasurableSet.{u_1} (α := α) {a : α | ∀ (i : ι), p i a}

Tactic:
rw [setOf_forall]

Premises used: Set.setOf_forall
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
ι : Sort uι
inst : MeasurableSpace α
inst_1 : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet.{u_1} (α := α) (⋂ (i : ι), {x : α | p i x})

Tactic:
MeasurableSet.iInter fun i ↦ (hp i).setOf

Premises used: Measurable.setOf, MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
ι : Sort uι
inst : MeasurableSpace α
inst_1 : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet.{u_1} (α := α) (⋂ (i : ι), {x : α | p i x})

Tactic:
exact MeasurableSet.iInter fun i ↦ (hp i).setOf

Premises used: Measurable.setOf, MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
ι : Sort uι
inst : MeasurableSpace α
inst_1 : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
rw : MeasurableSet.{u_1} (α := α) (⋃ (i : ι), {x : α | p i x})
⊢ MeasurableSet.{u_1} (α := α) {a : α | ∃ (i : ι), p i a}

Tactic:
rw [setOf_exists]

Premises used: Set.setOf_exists
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
ι : Sort uι
inst : MeasurableSpace α
inst_1 : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ι), {x : α | p i x})

Tactic:
MeasurableSet.iUnion fun i ↦ (hp i).setOf

Premises used: Measurable.setOf, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
ι : Sort uι
inst : MeasurableSpace α
inst_1 : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ι), {x : α | p i x})

Tactic:
exact MeasurableSet.iUnion fun i ↦ (hp i).setOf

Premises used: Measurable.setOf, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
⊢ Measurable (β := Prop) fun (x : α) ↦ f x = a

Tactic:
measurableSet_setOf.mp (measurableSet_eq.preimage hf)

Premises used: MeasurableSet.preimage, measurableSet_setOf, measurableSet_eq, Iff.mp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
h : ∀ (x : α), a = f x
| Measurable (β := Prop) fun (x : α) ↦ a = f x

Tactic:
enter [1, x]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
x_1 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
x : α
h : f x = a
| a = f x

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
h : ∀ (x : α), f x = a
| Measurable (β := Prop) fun (x : α) ↦ a = f x

Tactic:
enter [1, x]; rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
conv : Measurable (β := Prop) fun (x : α) ↦ f x = a
⊢ Measurable (β := Prop) fun (x : α) ↦ a = f x

Tactic:
conv => enter [1, x]; rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
⊢ Measurable (β := Prop) fun (x : α) ↦ f x = a

Tactic:
.eq_const hf a

Premises used: Measurable.eq_const
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
⊢ Measurable (β := Prop) fun (x : α) ↦ f x = a

Tactic:
exact .eq_const hf a
-- 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 β
g : β → Set α
inst_1 : Countable α
⊢ MeasurableSingletonClass.{u_1} (Set α)

Tactic:
inferInstanceAs <| MeasurableSingletonClass (α → Prop)

Premises used: _private.0.Set.instMeasurableSingletonClass._proof_1
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
⊢ Measurable (β := Set α) fun (p : α → Prop) ↦ {a : α | p a}

Tactic:
measurable_id

Premises used: measurable_id, setOf, Set.instMeasurableSpace._aux_1, Set
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace β
g : β → Set α
⊢ Measurable g ↔ ∀ (a : α), Measurable (β := Prop) fun (x : β) ↦ a ∈ g x

Tactic:
measurable_pi_iff

Premises used: measurable_pi_iff, Set.Mem, Set.instMeasurableSpace._aux_1, Set
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
a : α
⊢ Measurable (β := Prop) fun (s : Set α) ↦ a ∈ s

Tactic:
measurable_pi_apply _

Premises used: Set.Mem, measurable_pi_apply, Set.instMeasurableSpace._aux_1, Set
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
a : α
⊢ Measurable (β := Prop) fun (s : Set α) ↦ a ∉ s

Tactic:
(Measurable.of_discrete (f := Not)).comp <| measurable_set_mem a

Premises used: Measurable.comp, Measurable.of_discrete, measurable_set_mem
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
a : α
⊢ MeasurableSet.{u_1} (α := Set α) {s : Set α | a ∈ s}

Tactic:
measurableSet_setOf.2 <| measurable_set_mem _

Premises used: Iff.mpr, measurableSet_setOf, measurable_set_mem
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
a : α
⊢ MeasurableSet.{u_1} (α := Set α) {s : Set α | a ∉ s}

Tactic:
measurableSet_setOf.2 <| measurable_set_notMem _

Premises used: Iff.mpr, measurableSet_setOf, measurable_set_notMem
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
⊢ Measurable (β := Set α) fun (x : Set α) ↦ xᶜ

Tactic:
measurable_set_iff.2 fun _ ↦ measurable_set_notMem _

Premises used: Iff.mpr, measurable_set_iff, measurable_set_notMem
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : Countable α
⊢ MeasurableSet.{u_1} (α := Set α) {s : Set α | s.Finite}

Tactic:
Countable.setOf_finite.measurableSet

Premises used: Set.Countable.measurableSet, Set.Countable.setOf_finite
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : Countable α
⊢ MeasurableSet.{u_1} (α := Set α) {s : Set α | s.Infinite}

Tactic:
.setOf_finite |> .compl

Premises used: Set.Mem, setOf, MeasurableSet.setOf_finite, Set.Finite, MeasurableSet.compl, Set.Infinite
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : Countable α
S : Set (Set α)
hS : MeasurableSet S
⊢ MeasurableSet.{u_1} (α := Set α) {s : Set α | s ∈ S ∧ s.Finite}

Tactic:
hS.inter .setOf_finite

Premises used: Set.Mem, setOf, MeasurableSet.setOf_finite, Set.Finite, Set.inter, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : Countable α
S : Set (Set α)
hS : MeasurableSet S
⊢ MeasurableSet.{u_1} (α := Set α) {s : Set α | s ∈ S ∧ s.Infinite}

Tactic:
hS.inter .setOf_infinite

Premises used: Set.Mem, setOf, Set.inter, MeasurableSet.setOf_infinite, Not, Set.Infinite, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable α
s t : β → Set α
hs_1 : Measurable s
hs : Measurable t
i : α
⊢ Measurable (β := Prop) fun (a : β) ↦ i ∈ s a

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable α
s t : β → Set α
hs_1 : Measurable s
hs : Measurable t
i : α
⊢ Measurable (β := Prop) fun (a : β) ↦ i ∈ t a

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
ι : Type u_6
κ : Type u_7
X : Type u_8
inst : MeasurableSpace X
⊢ Measurable (α := ι × κ → X) curry

Tactic:
measurable_pi_lambda _ fun _ ↦ measurable_pi_lambda _ fun _ ↦ measurable_pi_apply _

Premises used: measurable_pi_lambda, measurable_pi_apply, Prod.mk, Function.curry
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
ι : Type u_6
κ : Type u_7
X : Type u_8
inst : MeasurableSpace X
⊢ Measurable (α := ι → κ → X) uncurry

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
ι : Type u_6
κ : Type u_7
X : Type u_8
inst : MeasurableSpace X
⊢ Measurable (α := ι × κ → X) (β := ι → κ → X) (⇑(Equiv.curry ι κ X) : (a : ι × κ → X) → ι → κ → X)

Tactic:
measurable_curry

Premises used: measurable_curry
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
ι : Type u_6
κ : Type u_7
X : Type u_8
inst : MeasurableSpace X
⊢ Measurable (α := ι → κ → X) (β := ι × κ → X) (⇑(Equiv.curry ι κ X).symm : (a : ι → κ → X) → ι × κ → X)

Tactic:
measurable_uncurry

Premises used: measurable_uncurry
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
ι : Type u_6
κ : ι → Type u_7
X : (i : ι) → κ i → Type u_8
inst : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
⊢ Measurable (α := (x : Sigma κ) → X (x.fst (β := κ)) (x.snd (β := κ))) (Sigma.curry (β := κ) (γ := X))

Tactic:
measurable_pi_lambda _ fun _ ↦ measurable_pi_lambda _ fun _ ↦ measurable_pi_apply _

Premises used: measurable_pi_lambda, measurable_pi_apply, Sigma.curry, Sigma.mk
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
ι : Type u_6
κ : ι → Type u_7
X : (i : ι) → κ i → Type u_8
inst : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
⊢ Measurable (α := (x : ι) → (y : κ x) → X x y) (Sigma.uncurry (β := κ) (γ := X))

Tactic:
measurable_pi_lambda _ fun _ ↦ ?_

Premises used: measurable_pi_lambda
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
ι : Type u_6
κ : ι → Type u_7
X : (i : ι) → κ i → Type u_8
inst : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
refine :
  ∀ (x : Sigma κ),
    Measurable (β := X (x.fst (β := κ)) (x.snd (β := κ))) fun (c : (x : ι) → (y : κ x) → X x y) ↦
      Sigma.uncurry (β := κ) (γ := X) c x
⊢ Measurable (α := (x : ι) → (y : κ x) → X x y) (Sigma.uncurry (β := κ) (γ := X))

Tactic:
refine measurable_pi_lambda _ fun _ ↦ ?_

Premises used: measurable_pi_lambda
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
ι : Type u_6
κ : ι → Type u_7
X : (i : ι) → κ i → Type u_8
inst : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
x : Sigma κ
simp :
  Measurable (β := X (x.fst (β := κ)) (x.snd (β := κ))) fun (c : (x : ι) → (y : κ x) → X x y) ↦
    c (x.fst (β := κ)) (x.snd (β := κ))
⊢ Measurable (β := X (x.fst (β := κ)) (x.snd (β := κ))) fun (c : (x : ι) → (y : κ x) → X x y) ↦
    Sigma.uncurry (β := κ) (γ := X) c x

Tactic:
simp only [Sigma.uncurry]

Premises used: Sigma.uncurry
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
ι : Type u_6
κ : ι → Type u_7
X : (i : ι) → κ i → Type u_8
inst : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
x : Sigma κ
⊢ Measurable (β := X (x.fst (β := κ)) (x.snd (β := κ))) fun (c : (x : ι) → (y : κ x) → X x y) ↦
    c (x.fst (β := κ)) (x.snd (β := κ))

Tactic:
fun_prop