awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
f : α → β
s : Set α
hs : s.Finite
hf : Measurable (sᶜ.restrict (π := fun (a : α) ↦ β) f)
⊢ Measurable f

Tactic:
have := hs.to_subtype
  measurable_of_restrict_of_restrict_compl hs.measurableSet (measurable_of_finite _) hf

Premises used: Set.Finite.to_subtype, measurable_of_finite, Set.restrict, Set.Finite.measurableSet, measurable_of_restrict_of_restrict_compl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
f : α → β
a : α
hf : Measurable (α := (↑{x : α | x ≠ a} : Type u_1)) (restrict (π := fun (a : α) ↦ β) {x : α | x ≠ a} f)
⊢ Measurable f

Tactic:
measurable_of_measurable_on_compl_finite {a} (finite_singleton a) hf

Premises used: measurable_of_measurable_on_compl_finite, Singleton.singleton, Set.finite_singleton
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x : β
⊢ x ∈ measurableAtom x

Tactic:
simp +contextual [measurableAtom]

Premises used: measurableAtom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
h : y ∈ measurableAtom x
s : Set β
hs : MeasurableSet s
hxs : x ∈ s
⊢ ∀ (i : Set β) (i_1 : x ∈ i) (i_2 : MeasurableSet i), y ∈ i

Tactic:
simp only [measurableAtom, mem_iInter] at h

Premises used: Set.mem_iInter, measurableAtom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
s : Set β
hs : MeasurableSet s
hxs : x ∈ s
h : ∀ (i : Set β) (i_1 : x ∈ i) (i_2 : MeasurableSet i), y ∈ i
⊢ y ∈ s

Tactic:
h s hxs hs
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
s : Set β
hs : MeasurableSet s
hxs : x ∈ s
h : ∀ (i : Set β) (i_1 : x ∈ i) (i_2 : MeasurableSet i), y ∈ i
⊢ y ∈ s

Tactic:
exact h s hxs hs
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
s : Set β
x : β
hs : MeasurableSet s
hx : x ∈ s
a : β
⊢ Membership.mem (γ := Set β) (⋂ (_ : MeasurableSet s), s) a → a ∈ s

Tactic:
simp [hs]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
x : β
⊢ {x} ⊆ measurableAtom x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x y : β
hy : y ∉ measurableAtom x
⊢ ∃ (s : Set β), x ∈ s ∧ MeasurableSet s ∧ y ∉ s

Tactic:
simpa [measurableAtom] using hy

Premises used: measurableAtom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x : β
⊢ ∀ y ∉ measurableAtom x, ∃ (s : Set β), x ∈ s ∧ MeasurableSet s ∧ y ∉ s

Tactic:
have : ∀ (y : β), y ∉ measurableAtom x → ∃ s, x ∈ s ∧ MeasurableSet s ∧ y ∉ s :=
    fun y hy ↦ by simpa [measurableAtom] using hy
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x : β
this : ∀ y ∉ measurableAtom x, ∃ (s : Set β), x ∈ s ∧ MeasurableSet s ∧ y ∉ s
choose! :
  ∀ (s : (y : β) → Set β) (hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y),
    MeasurableSet (measurableAtom x)
⊢ MeasurableSet (measurableAtom x)

Tactic:
choose! s hs using this
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x : β
s : (y : β) → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
h₁ : measurableAtom x ⊆ ⋂ y ∈ (measurableAtom x)ᶜ, s y
h₂ : ⋂ y ∈ (measurableAtom x)ᶜ, s y ⊆ measurableAtom x
⊢ measurableAtom x = ⋂ y ∈ (measurableAtom x)ᶜ, s y

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x : β
s : (y : β) → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
z : β
hz : z ∈ measurableAtom x
h₁ : ∀ (i : β) (i_1 : i ∉ measurableAtom x), z ∈ s i
⊢ Membership.mem (γ := Set β) (⋂ y ∈ (measurableAtom x)ᶜ, s y) z

Tactic:
simp only [mem_iInter, mem_compl_iff]

Premises used: Set.mem_iInter, Set.mem_compl_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x : β
s : (y : β) → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
z : β
hz : z ∈ measurableAtom x
i : β
hi : i ∉ measurableAtom x
⊢ z ∈ s i

Tactic:
mem_of_mem_measurableAtom hz (hs i hi).2.1 (hs i hi).1

Premises used: And.right, And.left, mem_of_mem_measurableAtom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x : β
s : (y : β) → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
z : β
hz : z ∈ measurableAtom x
i : β
hi : i ∉ measurableAtom x
⊢ z ∈ s i

Tactic:
exact mem_of_mem_measurableAtom hz (hs i hi).2.1 (hs i hi).1

Premises used: And.right, And.left, mem_of_mem_measurableAtom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x : β
s : (y : β) → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
h₂ : (measurableAtom x)ᶜ ⊆ (⋂ y ∈ (measurableAtom x)ᶜ, s y)ᶜ
⊢ ⋂ y ∈ (measurableAtom x)ᶜ, s y ⊆ measurableAtom x

Tactic:
apply compl_subset_compl.1

Premises used: Set.compl_subset_compl, Iff.mp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x : β
s : (y : β) → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
z : β
hz : z ∈ (measurableAtom x)ᶜ
h₂ : ∃ i ∉ measurableAtom x, z ∉ s i
⊢ Membership.mem (γ := Set β) (⋂ y ∈ (measurableAtom x)ᶜ, s y)ᶜ z

Tactic:
simp only [compl_iInter, mem_iUnion, mem_compl_iff, exists_prop]

Premises used: Set.compl_iInter, Set.mem_iUnion, exists_prop, Set.mem_compl_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x : β
s : (y : β) → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
z : β
hz : z ∈ (measurableAtom x)ᶜ
⊢ ∃ i ∉ measurableAtom x, z ∉ s i

Tactic:
⟨z, hz, (hs z hz).2.2⟩

Premises used: And.right, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x : β
s : (y : β) → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
z : β
hz : z ∈ (measurableAtom x)ᶜ
⊢ ∃ i ∉ measurableAtom x, z ∉ s i

Tactic:
exact ⟨z, hz, (hs z hz).2.2⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x : β
s : (y : β) → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
⊢ measurableAtom x = ⋂ y ∈ (measurableAtom x)ᶜ, s y

Tactic:
have : measurableAtom x = ⋂ (y ∈ (measurableAtom x)ᶜ), s y := by
    apply Subset.antisymm
    · intro z hz
      simp only [mem_iInter, mem_compl_iff]
      intro i hi
      exact mem_of_mem_measurableAtom hz (hs i hi).2.1 (hs i hi).1
    · apply compl_subset_compl.1
      intro z hz
      simp only [compl_iInter, mem_iUnion, mem_compl_iff, exists_prop]
      exact ⟨z, hz, (hs z hz).2.2⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x : β
s : (y : β) → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
this : measurableAtom x = ⋂ y ∈ (measurableAtom x)ᶜ, s y
rw : MeasurableSet.{u_2} (α := β) (⋂ y ∈ (measurableAtom x)ᶜ, s y)
⊢ MeasurableSet (measurableAtom x)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x : β
s : (y : β) → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
this : measurableAtom x = ⋂ y ∈ (measurableAtom x)ᶜ, s y
⊢ MeasurableSet.{u_2} (α := β) (⋂ y ∈ (measurableAtom x)ᶜ, s y)

Tactic:
MeasurableSet.biInter (to_countable (measurableAtom x)ᶜ) (fun i hi ↦ (hs i hi).2.1)

Premises used: Compl.compl, And.right, And.left, MeasurableSet.biInter, measurableAtom, Set.to_countable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
inst_1 : Countable β
x : β
s : (y : β) → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
this : measurableAtom x = ⋂ y ∈ (measurableAtom x)ᶜ, s y
⊢ MeasurableSet.{u_2} (α := β) (⋂ y ∈ (measurableAtom x)ᶜ, s y)

Tactic:
exact MeasurableSet.biInter (to_countable (measurableAtom x)ᶜ) (fun i hi ↦ (hs i hi).2.1)

Premises used: Compl.compl, And.right, And.left, MeasurableSet.biInter, measurableAtom, Set.to_countable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
z : β
hz : z ∈ measurableAtom x
simp :
  ∀ (hz : ∀ (i : Set β) (i_1 : x ∈ i) (i_2 : MeasurableSet i), z ∈ i)
    (hx : ∀ (i : Set β) (i_1 : y ∈ i) (i_2 : MeasurableSet i), x ∈ i) (i : Set β) (i_1 : y ∈ i) (i_2 : MeasurableSet i),
    z ∈ i
⊢ z ∈ measurableAtom y

Tactic:
simp only [measurableAtom, mem_iInter] at hz hx ⊢

Premises used: Set.mem_iInter, measurableAtom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y z : β
hz : ∀ (i : Set β) (i_1 : x ∈ i) (i_2 : MeasurableSet i), z ∈ i
hx : ∀ (i : Set β) (i_1 : y ∈ i) (i_2 : MeasurableSet i), x ∈ i
⊢ ∀ (i : Set β) (i_1 : y ∈ i) (i_2 : MeasurableSet i), z ∈ i

Tactic:
fun s hys hs ↦ hz s (hx s hys hs) hs
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y z : β
hz : ∀ (i : Set β) (i_1 : x ∈ i) (i_2 : MeasurableSet i), z ∈ i
hx : ∀ (i : Set β) (i_1 : y ∈ i) (i_2 : MeasurableSet i), x ∈ i
⊢ ∀ (i : Set β) (i_1 : y ∈ i) (i_2 : MeasurableSet i), z ∈ i

Tactic:
exact fun s hys hs ↦ hz s (hx s hys hs) hs
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
⊢ measurableAtom x = measurableAtom y

Tactic:
subset_antisymm (measurableAtom_subset_of_mem hx) ?_

Premises used: measurableAtom_subset_of_mem, subset_antisymm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
refine : measurableAtom y ⊆ measurableAtom x
⊢ measurableAtom x = measurableAtom y

Tactic:
refine subset_antisymm (measurableAtom_subset_of_mem hx) ?_

Premises used: measurableAtom_subset_of_mem, subset_antisymm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
pos : ∀ (hy : y ∈ measurableAtom x), measurableAtom y ⊆ measurableAtom x
neg : ∀ (hy : y ∉ measurableAtom x), measurableAtom y ⊆ measurableAtom x
⊢ measurableAtom y ⊆ measurableAtom x

Tactic:
by_cases hy : y ∈ measurableAtom x

Premises used: measurableAtom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
hy : y ∈ measurableAtom x
⊢ measurableAtom y ⊆ measurableAtom x

Tactic:
measurableAtom_subset_of_mem hy

Premises used: measurableAtom_subset_of_mem
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
hy : y ∈ measurableAtom x
⊢ measurableAtom y ⊆ measurableAtom x

Tactic:
exact measurableAtom_subset_of_mem hy

Premises used: measurableAtom_subset_of_mem
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
hy : y ∉ measurableAtom x
neg : False
⊢ measurableAtom y ⊆ measurableAtom x

Tactic:
exfalso
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
hy : y ∉ measurableAtom x
⊢ ∀ (i : Set β) (i_1 : y ∈ i) (i_2 : MeasurableSet i), x ∈ i

Tactic:
simp only [measurableAtom, mem_iInter, not_forall] at hx hy ⊢

Premises used: Set.mem_iInter, measurableAtom, Classical.not_forall
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
hy : y ∉ measurableAtom x
hx₁ : ∀ (i : Set β) (i_1 : y ∈ i) (i_2 : MeasurableSet i), x ∈ i
⊢ ∃ (x_1 : Set β) (_ : x ∈ x_1) (_ : MeasurableSet x_1), y ∉ x_1

Tactic:
simp only [measurableAtom, mem_iInter, not_forall] at hx hy ⊢

Premises used: Set.mem_iInter, measurableAtom, Classical.not_forall
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : ∀ (i : Set β) (i_1 : y ∈ i) (i_2 : MeasurableSet i), x ∈ i
hy : ∃ (x_1 : Set β) (_ : x ∈ x_1) (_ : MeasurableSet x_1), y ∉ x_1
neg : ∀ (s : Set β) (hxs : x ∈ s) (hs : MeasurableSet s) (hys : y ∉ s), False
⊢ False

Tactic:
obtain ⟨s, hxs, hs, hys⟩ := hy
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : ∀ (i : Set β) (i_1 : y ∈ i) (i_2 : MeasurableSet i), x ∈ i
s : Set β
hxs : x ∈ s
hs : MeasurableSet s
hys : y ∉ s
⊢ x ∈ sᶜ

Tactic:
specialize hx sᶜ hys hs.compl

Premises used: Compl.compl, MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
s : Set β
hxs : x ∈ s
hs : MeasurableSet s
hys : y ∉ s
hx : x ∈ sᶜ
⊢ False

Tactic:
hx hxs
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
s : Set β
hxs : x ∈ s
hs : MeasurableSet s
hys : y ∉ s
hx : x ∈ sᶜ
⊢ False

Tactic:
exact hx hxs
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
rw : measurableAtom x ∩ measurableAtom y = ∅
⊢ Disjoint (measurableAtom x) (measurableAtom y)

Tactic:
rw [Set.disjoint_iff_inter_eq_empty]

Premises used: Set.disjoint_iff_inter_eq_empty
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
h : ∀ (z : β), z ∈ measurableAtom x ∩ measurableAtom y ↔ Membership.mem (γ := Set β) ∅ z
⊢ measurableAtom x ∩ measurableAtom y = ∅

Tactic:
ext z
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
z : β
h : z ∈ measurableAtom x → z ∉ measurableAtom y
⊢ z ∈ measurableAtom x ∩ measurableAtom y ↔ Membership.mem (γ := Set β) ∅ z

Tactic:
simp only [mem_inter_iff, mem_empty_iff_false, iff_false, not_and]

Premises used: iff_false, Set.mem_inter_iff, Set.mem_empty_iff_false, not_and
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
z : β
hzx : z ∈ measurableAtom x
hzy : z ∈ measurableAtom y
⊢ measurableAtom z = measurableAtom x

Tactic:
have h1 := measurableAtom_eq_of_mem hzx
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
z : β
hzx : z ∈ measurableAtom x
hzy : z ∈ measurableAtom y
h1 : measurableAtom z = measurableAtom x
⊢ measurableAtom z = measurableAtom y

Tactic:
have h2 := measurableAtom_eq_of_mem hzy
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
z : β
hzx : z ∈ measurableAtom x
hzy : z ∈ measurableAtom y
h1 : measurableAtom z = measurableAtom x
h2 : measurableAtom z = measurableAtom y
⊢ x ∉ measurableAtom x

Tactic:
rw [← h2, h1] at hx
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
z : β
hzx : z ∈ measurableAtom x
hzy : z ∈ measurableAtom y
h1 : measurableAtom z = measurableAtom x
h2 : measurableAtom z = measurableAtom y
hx₁ : x ∉ measurableAtom x
⊢ z ∈ measurableAtom x

Tactic:
rw [← h2, h1] at hx
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
z : β
hzx : z ∈ measurableAtom x
hzy : z ∈ measurableAtom y
h1 : measurableAtom z = measurableAtom x
h2 : measurableAtom z = measurableAtom y
hx₁ : x ∉ measurableAtom x
hzx₁ : z ∈ measurableAtom x
⊢ z ∈ measurableAtom y

Tactic:
rw [← h2, h1] at hx
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
z : β
hzx : z ∈ measurableAtom x
hzy : z ∈ measurableAtom y
h1 : measurableAtom z = measurableAtom x
h2 : measurableAtom z = measurableAtom y
hx₁ : x ∉ measurableAtom x
hzx₁ : z ∈ measurableAtom x
hzy₁ : z ∈ measurableAtom y
⊢ measurableAtom z = measurableAtom x

Tactic:
rw [← h2, h1] at hx
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
z : β
hzx : z ∈ measurableAtom x
hzy : z ∈ measurableAtom y
h1 : measurableAtom z = measurableAtom x
h2 : measurableAtom z = measurableAtom y
hx₁ : x ∉ measurableAtom x
hzx₁ : z ∈ measurableAtom x
hzy₁ : z ∈ measurableAtom y
h1₁ : measurableAtom z = measurableAtom x
⊢ measurableAtom z = measurableAtom y

Tactic:
rw [← h2, h1] at hx
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y z : β
hx : x ∉ measurableAtom x
hzx : z ∈ measurableAtom x
hzy : z ∈ measurableAtom y
h1 : measurableAtom z = measurableAtom x
h2 : measurableAtom z = measurableAtom y
⊢ False

Tactic:
hx (mem_measurableAtom_self x)

Premises used: mem_measurableAtom_self
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
inst : MeasurableSpace β
x y z : β
hx : x ∉ measurableAtom x
hzx : z ∈ measurableAtom x
hzy : z ∈ measurableAtom y
h1 : measurableAtom z = measurableAtom x
h2 : measurableAtom z = measurableAtom y
⊢ False

Tactic:
exact hx (mem_measurableAtom_self x)

Premises used: mem_measurableAtom_self
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
x_1 : MeasurableSpace β
⊢ Measurable (α := α × β) Prod.fst

Tactic:
Measurable.of_comap_le le_sup_left

Premises used: le_sup_left, Measurable.of_comap_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
x_1 : MeasurableSpace β
⊢ Measurable (α := α × β) Prod.snd

Tactic:
Measurable.of_comap_le le_sup_right

Premises used: Measurable.of_comap_le, le_sup_right
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf : Measurable f
⊢ Measurable.{u_1, u_2} (β := β) fun (a : α) ↦ (f a).1

Tactic:
measurable_fst.comp hf

Premises used: Measurable.comp, measurable_fst
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf : Measurable f
⊢ Measurable.{u_1, u_3} (β := γ) fun (a : α) ↦ (f a).2

Tactic:
measurable_snd.comp hf

Premises used: Measurable.comp, measurable_snd
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable.{u_1, u_2} (β := β) fun (a : α) ↦ (f a).1
hf₂ : Measurable.{u_1, u_3} (β := γ) fun (a : α) ↦ (f a).2
rw : mβ ≤ MeasurableSpace.map (Prod.fst ∘ f) m
⊢ MeasurableSpace.comap Prod.fst mβ ≤ MeasurableSpace.map f m

Tactic:
rw [MeasurableSpace.comap_le_iff_le_map, MeasurableSpace.map_comp]

Premises used: MeasurableSpace.comap_le_iff_le_map, MeasurableSpace.map_comp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable.{u_1, u_2} (β := β) fun (a : α) ↦ (f a).1
hf₂ : Measurable.{u_1, u_3} (β := γ) fun (a : α) ↦ (f a).2
⊢ mβ ≤ MeasurableSpace.map (Prod.fst ∘ f) m

Tactic:
hf₁

Premises used: MeasurableSet, Measurable, setOf, Set.preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable.{u_1, u_2} (β := β) fun (a : α) ↦ (f a).1
hf₂ : Measurable.{u_1, u_3} (β := γ) fun (a : α) ↦ (f a).2
⊢ mβ ≤ MeasurableSpace.map (Prod.fst ∘ f) m

Tactic:
exact hf₁
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable.{u_1, u_2} (β := β) fun (a : α) ↦ (f a).1
hf₂ : Measurable.{u_1, u_3} (β := γ) fun (a : α) ↦ (f a).2
rw : mγ ≤ MeasurableSpace.map (Prod.snd ∘ f) m
⊢ MeasurableSpace.comap Prod.snd mγ ≤ MeasurableSpace.map f m

Tactic:
rw [MeasurableSpace.comap_le_iff_le_map, MeasurableSpace.map_comp]

Premises used: MeasurableSpace.comap_le_iff_le_map, MeasurableSpace.map_comp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable.{u_1, u_2} (β := β) fun (a : α) ↦ (f a).1
hf₂ : Measurable.{u_1, u_3} (β := γ) fun (a : α) ↦ (f a).2
⊢ mγ ≤ MeasurableSpace.map (Prod.snd ∘ f) m

Tactic:
hf₂

Premises used: MeasurableSet, Measurable, setOf, Set.preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable.{u_1, u_2} (β := β) fun (a : α) ↦ (f a).1
hf₂ : Measurable.{u_1, u_3} (β := γ) fun (a : α) ↦ (f a).2
⊢ mγ ≤ MeasurableSpace.map (Prod.snd ∘ f) m

Tactic:
exact hf₂
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
m : MeasurableSpace α
β : Type u_6
γ : Type u_7
x : MeasurableSpace β
x_1 : MeasurableSpace γ
f : α → β
g : α → γ
hf : Measurable f
hg : Measurable g
⊢ Measurable (β := β × γ) fun (a : α) ↦ (f a, g a)

Tactic:
Measurable.prod hf hg

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

Tactic:
(hf.comp measurable_fst).prodMk (hg.comp measurable_snd)

Premises used: Measurable.comp, Measurable.prodMk, Prod.map, measurable_snd, measurable_fst
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
x : α
⊢ Measurable (α := β) (Prod.mk x)

Tactic:
measurable_const.prodMk measurable_id

Premises used: measurable_id, Measurable.prodMk, measurable_const