awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Finite
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet.{u_1} (α := α) (⋃ b ∈ s, f b)

Tactic:
.biUnion hs.countable h

Premises used: MeasurableSet.biUnion, Set.Finite.countable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Finset β
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet.{u_1} (α := α) (⋃ b ∈ s, f b)

Tactic:
s.finite_toSet.measurableSet_biUnion h

Premises used: Set.Finite.measurableSet_biUnion, Finset.finite_toSet
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
rw : MeasurableSet.{u_1} (α := α) (⋃ i ∈ s, i)
⊢ MeasurableSet (⋃₀ s)

Tactic:
rw [sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet.{u_1} (α := α) (⋃ i ∈ s, i)

Tactic:
.biUnion hs h

Premises used: MeasurableSet.biUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet.{u_1} (α := α) (⋃ i ∈ s, i)

Tactic:
exact .biUnion hs h
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Finite
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet (⋃₀ s)

Tactic:
MeasurableSet.sUnion hs.countable h

Premises used: MeasurableSet.sUnion, Set.Finite.countable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
rw : MeasurableSet.{u_1} (α := α) (⋃ (i : ι), (f i)ᶜ)
⊢ MeasurableSet.{u_1} (α := α) (⋂ (b : ι), f b)ᶜ

Tactic:
rw [compl_iInter]

Premises used: Set.compl_iInter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ι), (f i)ᶜ)

Tactic:
.iUnion fun b => (h b).compl

Premises used: MeasurableSet.compl, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ι), (f i)ᶜ)

Tactic:
exact .iUnion fun b => (h b).compl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
rw : MeasurableSet.{u_1} (α := α) (⋃ i ∈ s, (f i)ᶜ)
⊢ MeasurableSet.{u_1} (α := α) (⋂ b ∈ s, f b)ᶜ

Tactic:
rw [compl_iInter₂]

Premises used: Set.compl_iInter₂
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet.{u_1} (α := α) (⋃ i ∈ s, (f i)ᶜ)

Tactic:
.biUnion hs fun b hb => (h b hb).compl

Premises used: MeasurableSet.compl, MeasurableSet.biUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet.{u_1} (α := α) (⋃ i ∈ s, (f i)ᶜ)

Tactic:
exact .biUnion hs fun b hb => (h b hb).compl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Finite
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet.{u_1} (α := α) (⋂ b ∈ s, f b)

Tactic:
.biInter hs.countable h

Premises used: MeasurableSet.biInter, Set.Finite.countable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Finset β
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet.{u_1} (α := α) (⋂ b ∈ s, f b)

Tactic:
s.finite_toSet.measurableSet_biInter h

Premises used: Set.Finite.measurableSet_biInter, Finset.finite_toSet
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
rw : MeasurableSet.{u_1} (α := α) (⋂ i ∈ s, i)
⊢ MeasurableSet (⋂₀ s)

Tactic:
rw [sInter_eq_biInter]

Premises used: Set.sInter_eq_biInter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet.{u_1} (α := α) (⋂ i ∈ s, i)

Tactic:
MeasurableSet.biInter hs h

Premises used: MeasurableSet.biInter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet.{u_1} (α := α) (⋂ i ∈ s, i)

Tactic:
exact MeasurableSet.biInter hs h

Premises used: MeasurableSet.biInter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Finite
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet (⋂₀ s)

Tactic:
MeasurableSet.sInter hs.countable h

Premises used: MeasurableSet.sInter, Set.Finite.countable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
rw : MeasurableSet.{u_1} (α := α) (⋃ (b : Bool), bif b then s₁ else s₂)
⊢ MeasurableSet (s₁ ∪ s₂)

Tactic:
rw [union_eq_iUnion]

Premises used: Set.union_eq_iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet.{u_1} (α := α) (⋃ (b : Bool), bif b then s₁ else s₂)

Tactic:
.iUnion (Bool.forall_bool.2 ⟨h₂, h₁⟩)

Premises used: Iff.mpr, Bool.forall_bool, And.intro, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet.{u_1} (α := α) (⋃ (b : Bool), bif b then s₁ else s₂)

Tactic:
exact .iUnion (Bool.forall_bool.2 ⟨h₂, h₁⟩)
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
rw : MeasurableSet (s₁ᶜ ∪ s₂ᶜ)ᶜ
⊢ MeasurableSet (s₁ ∩ s₂)

Tactic:
rw [inter_eq_compl_compl_union_compl]

Premises used: Set.inter_eq_compl_compl_union_compl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ᶜ ∪ s₂ᶜ)ᶜ

Tactic:
(h₁.compl.union h₂.compl).compl

Premises used: MeasurableSet.compl, MeasurableSet.union
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ᶜ ∪ s₂ᶜ)ᶜ

Tactic:
exact (h₁.compl.union h₂.compl).compl

Premises used: MeasurableSet.compl, MeasurableSet.union
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ \ s₂)

Tactic:
h₁.inter h₂.compl

Premises used: Set.Mem, Set.diff, setOf, MeasurableSet.compl, Not, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
rw : MeasurableSet (s₂ ⊔ s₁ᶜ)
⊢ MeasurableSet (s₁ ⇨ s₂)

Tactic:
rw [himp_eq]

Premises used: himp_eq
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₂ ⊔ s₁ᶜ)

Tactic:
h₂.union h₁.compl

Premises used: MeasurableSet.compl, MeasurableSet.union
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₂ ⊔ s₁ᶜ)

Tactic:
exact h₂.union h₁.compl

Premises used: MeasurableSet.compl, MeasurableSet.union
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ ∆ s₂)

Tactic:
(h₁.diff h₂).union (h₂.diff h₁)

Premises used: MeasurableSet.diff, MeasurableSet.union, symmDiff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ ⇔ s₂)

Tactic:
(h₂.himp h₁).inter (h₁.himp h₂)

Premises used: MeasurableSet.himp, bihimp, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
t s₁ s₂ : Set α
ht : MeasurableSet t
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (t.ite s₁ s₂)

Tactic:
(h₁.inter ht).union (h₂.diff ht)

Premises used: MeasurableSet.diff, Set.ite, MeasurableSet.union, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s t : Set α
p : Prop
hs : p → MeasurableSet s
ht : ¬p → MeasurableSet t
pos : ∀ (h : p), MeasurableSet s
neg : ∀ (h : ¬p), MeasurableSet t
⊢ MeasurableSet (if p then s else t)

Tactic:
split_ifs with h
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s t : Set α
p : Prop
hs : p → MeasurableSet s
ht : ¬p → MeasurableSet t
h : p
⊢ MeasurableSet s

Tactic:
hs h
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s t : Set α
p : Prop
hs : p → MeasurableSet s
ht : ¬p → MeasurableSet t
h : ¬p
⊢ MeasurableSet t

Tactic:
ht h
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s t : Set α
p : Prop
hs : p → MeasurableSet s
ht : ¬p → MeasurableSet t
h : p
⊢ MeasurableSet s

Tactic:
exacts [hs h, ht h]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
i : Bool
false : MeasurableSet (bif Bool.false then s₁ else s₂)
true : MeasurableSet (bif Bool.true then s₁ else s₂)
⊢ MeasurableSet (bif i then s₁ else s₂)

Tactic:
cases i
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (bif false then s₁ else s₂)

Tactic:
h₂

Premises used: cond
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (bif true then s₁ else s₂)

Tactic:
h₁

Premises used: cond
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (bif false then s₁ else s₂)

Tactic:
exacts [h₂, h₁]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
p : Prop
pos : p → MeasurableSet.{u_1} (α := α) {_a : α | p}
neg : ¬p → MeasurableSet.{u_1} (α := α) {_a : α | p}
⊢ MeasurableSet.{u_1} (α := α) {_a : α | p}

Tactic:
by_cases p
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
p : Prop
h : p
⊢ MeasurableSet.{u_1} (α := α) {_a : α | p}

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
p : Prop
h : ¬p
⊢ MeasurableSet.{u_1} (α := α) {_a : α | p}

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet.{u_1} (α := α) {x : α | p x}
ht : MeasurableSet.{u_1} (α := α) {x : α | q x}
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | p x → q x} ({x : α | p x}ᶜ ∪ {x : α | q x})

Tactic:
grind
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet.{u_1} (α := α) {x : α | p x}
ht : MeasurableSet.{u_1} (α := α) {x : α | q x}
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | p x → q x} ({x : α | p x}ᶜ ∪ {x : α | q x})

Tactic:
have h_eq : {x | p x → q x} = {x | p x}ᶜ ∪ {x | q x} := by grind
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet.{u_1} (α := α) {x : α | p x}
ht : MeasurableSet.{u_1} (α := α) {x : α | q x}
h_eq : Eq.{u_1 + 1} (α := Set α) {x : α | p x → q x} ({x : α | p x}ᶜ ∪ {x : α | q x})
rw : MeasurableSet.{u_1} (α := α) ({x : α | p x}ᶜ ∪ {x : α | q x})
⊢ MeasurableSet.{u_1} (α := α) {x : α | p x → q x}

Tactic:
rw [h_eq]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet.{u_1} (α := α) {x : α | p x}
ht : MeasurableSet.{u_1} (α := α) {x : α | q x}
h_eq : Eq.{u_1 + 1} (α := Set α) {x : α | p x → q x} ({x : α | p x}ᶜ ∪ {x : α | q x})
⊢ MeasurableSet.{u_1} (α := α) ({x : α | p x}ᶜ ∪ {x : α | q x})

Tactic:
hs.compl.union ht

Premises used: MeasurableSet.compl, MeasurableSet.union
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet.{u_1} (α := α) {x : α | p x}
ht : MeasurableSet.{u_1} (α := α) {x : α | q x}
h_eq : Eq.{u_1 + 1} (α := Set α) {x : α | p x → q x} ({x : α | p x}ᶜ ∪ {x : α | q x})
⊢ MeasurableSet.{u_1} (α := α) ({x : α | p x}ᶜ ∪ {x : α | q x})

Tactic:
exact hs.compl.union ht

Premises used: MeasurableSet.compl, MeasurableSet.union
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet.{u_1} (α := α) {x : α | p x}
ht : MeasurableSet.{u_1} (α := α) {x : α | q x}
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) {x : α | p x ↔ q x} x ↔
      Membership.mem (γ := Set α) ({x : α | p x → q x} ∩ {x : α | q x → p x}) x
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | p x ↔ q x} ({x : α | p x → q x} ∩ {x : α | q x → p x})

Tactic:
ext
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet.{u_1} (α := α) {x : α | p x}
ht : MeasurableSet.{u_1} (α := α) {x : α | q x}
x : α
⊢ (p x ↔ q x) ↔ (p x → q x) ∧ (q x → p x)

Tactic:
grind
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet.{u_1} (α := α) {x : α | p x}
ht : MeasurableSet.{u_1} (α := α) {x : α | q x}
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | p x ↔ q x} ({x : α | p x → q x} ∩ {x : α | q x → p x})

Tactic:
have h_eq : {x | p x ↔ q x} = {x | p x → q x} ∩ {x | q x → p x} := by ext; simp; grind
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet.{u_1} (α := α) {x : α | p x}
ht : MeasurableSet.{u_1} (α := α) {x : α | q x}
h_eq : Eq.{u_1 + 1} (α := Set α) {x : α | p x ↔ q x} ({x : α | p x → q x} ∩ {x : α | q x → p x})
rw : MeasurableSet.{u_1} (α := α) ({x : α | p x → q x} ∩ {x : α | q x → p x})
⊢ MeasurableSet.{u_1} (α := α) {x : α | p x ↔ q x}

Tactic:
rw [h_eq]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet.{u_1} (α := α) {x : α | p x}
ht : MeasurableSet.{u_1} (α := α) {x : α | q x}
h_eq : Eq.{u_1 + 1} (α := Set α) {x : α | p x ↔ q x} ({x : α | p x → q x} ∩ {x : α | q x → p x})
⊢ MeasurableSet.{u_1} (α := α) ({x : α | p x → q x} ∩ {x : α | q x → p x})

Tactic:
(hs.imp ht).inter (ht.imp hs)

Premises used: MeasurableSet.imp, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet.{u_1} (α := α) {x : α | p x}
ht : MeasurableSet.{u_1} (α := α) {x : α | q x}
h_eq : Eq.{u_1 + 1} (α := Set α) {x : α | p x ↔ q x} ({x : α | p x → q x} ∩ {x : α | q x → p x})
⊢ MeasurableSet.{u_1} (α := α) ({x : α | p x → q x} ∩ {x : α | q x → p x})

Tactic:
exact (hs.imp ht).inter (ht.imp hs)

Premises used: MeasurableSet.imp, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
⊢ Nonempty.{max 1 (u_1 + 1)} { t : Set α // s ⊆ t ∧ MeasurableSet t }

Tactic:
⟨⟨univ, subset_univ s, MeasurableSet.univ⟩⟩

Premises used: Set.subset_univ, Set.univ, Nonempty.intro, Subtype.mk, And.intro, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
MeasurableSet' : Set α → Prop
measurableSet_empty : MeasurableSet' ∅
measurableSet_compl : ∀ (s : Set α), MeasurableSet' s → MeasurableSet' sᶜ
measurableSet_iUnion : ∀ (f : ℕ → Set α), (∀ (i : ℕ), MeasurableSet' (f i)) → MeasurableSet' (⋃ (i : ℕ), f i)
MeasurableSet'_1 : Set α → Prop
measurableSet_empty_1 : MeasurableSet'_1 ∅
measurableSet_compl_1 : ∀ (s : Set α), MeasurableSet'_1 s → MeasurableSet'_1 sᶜ
measurableSet_iUnion_1 : ∀ (f : ℕ → Set α), (∀ (i : ℕ), MeasurableSet'_1 (f i)) → MeasurableSet'_1 (⋃ (i : ℕ), f i)
h : Eq.{u_1 + 1} (α := (s : Set α) → Prop) MeasurableSet MeasurableSet
⊢ { MeasurableSet' := MeasurableSet', measurableSet_empty := measurableSet_empty,
      measurableSet_compl := measurableSet_compl, measurableSet_iUnion := measurableSet_iUnion : MeasurableSpace α } =
    { MeasurableSet' := MeasurableSet'_1, measurableSet_empty := measurableSet_empty_1,
      measurableSet_compl := measurableSet_compl_1, measurableSet_iUnion := measurableSet_iUnion_1 }

Tactic:
congr
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m₁ m₂ : MeasurableSpace α
h : ∀ (s : Set α), MeasurableSet s ↔ MeasurableSet s
⊢ m₁ = m₂

Tactic:
measurableSet_injective <| funext fun s => propext (h s)

Premises used: funext, propext, MeasurableSpace.measurableSet_injective
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
⊢ MeasurableSet (α := α) {a}

Tactic:
measurableSet_singleton a

Premises used: MeasurableSingletonClass.measurableSet_singleton
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
⊢ MeasurableSet.{u_1} (α := α) {x : α | x = a}

Tactic:
.singleton a

Premises used: MeasurableSet.singleton, setOf, Set.singleton
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
a : α
⊢ MeasurableSet (insert a s)

Tactic:
.union (.singleton a) hs

Premises used: Set.insert, MeasurableSet.singleton, Set.Mem, setOf, MeasurableSet.union
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
s : Set α
h : MeasurableSet (insert a s)
ha : a ∈ s
rwa rwa₁ rwa₂ rwa₃ : MeasurableSet (insert a s)
⊢ MeasurableSet s

Tactic:
rwa [← insert_eq_of_mem ha]

Premises used: Set.insert_eq_of_mem
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
s : Set α
⊢ MeasurableSet (insert a s) ↔ MeasurableSet s

Tactic:
exact ⟨fun h =>
    if ha : a ∈ s then by rwa [← insert_eq_of_mem ha]
    else insert_diff_self_of_notMem ha ▸ h.diff (.singleton _),
    fun h => h.insert a⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
s : Set α
⊢ MeasurableSet (insert a s) ↔ MeasurableSet s

Tactic:
classical
  exact ⟨fun h =>
    if ha : a ∈ s then by rwa [← insert_eq_of_mem ha]
    else insert_diff_self_of_notMem ha ▸ h.diff (.singleton _),
    fun h => h.insert a⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
s : Set α
hs : s.Subsingleton
⊢ MeasurableSet s

Tactic:
hs.induction_on .empty .singleton

Premises used: MeasurableSet.singleton, MeasurableSet.empty, Set.Subsingleton.induction_on
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
s : Set α
hs : s.Finite
⊢ MeasurableSet s

Tactic:
Finite.induction_on _ hs .empty fun _ _ hsm => hsm.insert _

Premises used: Set.Finite.induction_on
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
s : Finset α
⊢ MeasurableSet (↑s : Set α)

Tactic:
s.finite_toSet.measurableSet

Premises used: Finset.finite_toSet, Set.Finite.measurableSet
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
s : Set α
hs : s.Countable
rw : MeasurableSet.{u_1} (α := α) (⋃ x ∈ s, {x})
⊢ MeasurableSet s

Tactic:
rw [← biUnion_of_singleton s]

Premises used: Set.biUnion_of_singleton
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
s : Set α
hs : s.Countable
⊢ MeasurableSet.{u_1} (α := α) (⋃ x ∈ s, {x})

Tactic:
.biUnion hs fun b _ => .singleton b

Premises used: MeasurableSet.singleton, MeasurableSet.biUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
s : Set α
hs : s.Countable
⊢ MeasurableSet.{u_1} (α := α) (⋃ x ∈ s, {x})

Tactic:
exact .biUnion hs fun b _ => .singleton b
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
p : Set α → Prop
h : ∀ (s : Set α), p s ↔ MeasurableSet s
⊢ p ∅

Tactic:
simpa only [h] using m.measurableSet_empty

Premises used: MeasurableSpace.measurableSet_empty
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
p : Set α → Prop
h : ∀ (s : Set α), p s ↔ MeasurableSet s
⊢ ∀ (s : Set α), p s → p sᶜ

Tactic:
simpa only [h] using m.measurableSet_compl

Premises used: MeasurableSpace.measurableSet_compl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
p : Set α → Prop
h : ∀ (s : Set α), p s ↔ MeasurableSet s
⊢ ∀ (f : ℕ → Set α), (∀ (i : ℕ), p (f i)) → p (⋃ (i : ℕ), f i)

Tactic:
simpa only [h] using m.measurableSet_iUnion

Premises used: MeasurableSpace.measurableSet_iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
p : Set α → Prop
h : ∀ (s : Set α), p s ↔ MeasurableSet s
s : Set α
⊢ MeasurableSet s ↔ p s

Tactic:
Iff.rfl

Premises used: MeasurableSet, Iff.rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
p : Set α → Prop
h : ∀ (s : Set α), p s ↔ MeasurableSet s
⊢ m.copy p h = m

Tactic:
ext h

Premises used: MeasurableSpace.ext
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_7
a b : MeasurableSpace α
⊢ a ≤ b ↔ MeasurableSet' a ≤ MeasurableSet' b

Tactic:
Iff.rfl

Premises used: MeasurableSet, Iff.rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
s : Set (Set α)
t : Set α
ht : t ∈ s
⊢ MeasurableSet t

Tactic:
.basic t ht

Premises used: MeasurableSet, MeasurableSpace.GenerateMeasurable.basic
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
C : Set (Set α)
p : (s : Set α) → MeasurableSet s → Prop
hC : ∀ t ∈ C, ∀ (ht : MeasurableSet t), p t ht
empty : p ∅ ⋯
compl : ∀ (t : Set α) (ht : MeasurableSet t), p t ht → p tᶜ ⋯
iUnion : ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ (i : ℕ), s i) ⋯
s : Set α
hs : MeasurableSet s
basic : ∀ (u : Set α) (a : u ∈ C), p u ⋯
empty₁ : p ∅ ⋯
compl₁ : ∀ (t : Set α) (a : GenerateMeasurable C t), p t a → p tᶜ ⋯
iUnion₁ : ∀ (f : ℕ → Set α) (a : ∀ (n : ℕ), GenerateMeasurable C (f n)), (∀ (n : ℕ), p (f n) ⋯) → p (⋃ (i : ℕ), f i) ⋯
⊢ p s hs

Tactic:
induction hs