awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
u : Set α
hu : u ∈ range t
⊢ ∃ (y : ℕ), t y = u

Tactic:
simp only [mem_range] at hu

Premises used: Set.mem_range
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
u : Set α
hu : ∃ (y : ℕ), t y = u
refine_2 : ∀ (n : ℕ), MeasurableSet (t n)
⊢ MeasurableSet u

Tactic:
obtain ⟨n, rfl⟩ := hu

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ MeasurableSet (t n)

Tactic:
generateFrom_mono (subset_iUnion _ _) _ (measurableSet_generateFrom_memPartition t n)

Premises used: MeasurableSpace.generateFrom_mono, Set.subset_iUnion, MeasurableSpace.measurableSet_generateFrom_memPartition
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ MeasurableSet (t n)

Tactic:
exact generateFrom_mono (subset_iUnion _ _) _ (measurableSet_generateFrom_memPartition t n)

Premises used: MeasurableSpace.generateFrom_mono, Set.subset_iUnion, MeasurableSpace.measurableSet_generateFrom_memPartition
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
rw : generateFrom (⋃ (n : ℕ), memPartition t n)
| generateFrom (range t)

Tactic:
rw [← generateFrom_iUnion_memPartition t]

Premises used: MeasurableSpace.generateFrom_iUnion_memPartition
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
conv_rhs : generateFrom (memPartition t n) ≤ generateFrom (⋃ (n : ℕ), memPartition t n)
⊢ generateFrom (memPartition t n) ≤ generateFrom (range t)

Tactic:
conv_rhs => rw [← generateFrom_iUnion_memPartition t]

Premises used: MeasurableSpace.generateFrom_iUnion_memPartition
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ generateFrom (memPartition t n) ≤ generateFrom (⋃ (n : ℕ), memPartition t n)

Tactic:
generateFrom_mono (subset_iUnion _ _)

Premises used: MeasurableSpace.generateFrom_mono, Set.subset_iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ generateFrom (memPartition t n) ≤ generateFrom (⋃ (n : ℕ), memPartition t n)

Tactic:
exact generateFrom_mono (subset_iUnion _ _)

Premises used: MeasurableSpace.generateFrom_mono, Set.subset_iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
⊢ generateFrom (⋃ (n : ℕ), memPartition t n) ≤ m

Tactic:
(generateFrom_iUnion_memPartition t).trans_le (generateFrom_le ?_)

Premises used: Eq.trans_le, MeasurableSpace.generateFrom_iUnion_memPartition, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
refine : ∀ t_1 ∈ range t, MeasurableSet t_1
⊢ generateFrom (⋃ (n : ℕ), memPartition t n) ≤ m

Tactic:
refine (generateFrom_iUnion_memPartition t).trans_le (generateFrom_le ?_)

Premises used: Eq.trans_le, MeasurableSpace.generateFrom_iUnion_memPartition, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
i : ℕ
⊢ MeasurableSet (t i)

Tactic:
ht i
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
i : ℕ
⊢ MeasurableSet (t i)

Tactic:
exact ht i
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
⊢ generateFrom (memPartition t n) ≤ m

Tactic:
(generateFrom_mono (subset_iUnion _ _)).trans (generateFrom_iUnion_memPartition_le ht)

Premises used: MeasurableSpace.generateFrom_mono, Set.subset_iUnion, LE.le.trans, MeasurableSpace.generateFrom_iUnion_memPartition_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet s

Tactic:
generateFrom_memPartition_le ht n _ (measurableSet_generateFrom hs)

Premises used: MeasurableSpace.generateFrom_memPartition_le, MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
a : α
⊢ MeasurableSet (memPartitionSet t n a)

Tactic:
measurableSet_memPartition ht n (memPartitionSet_mem t n a)

Premises used: MeasurableSpace.measurableSet_memPartition, memPartitionSet_mem
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_3
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
n : ℕ
⊢ MeasurableSet.{u_3} (α := α) (enumerateCountable (s := countableGeneratingSet α) ⋯ ∅ n)

Tactic:
measurableSet_countableGeneratingSet
    (enumerateCountable_mem _ (empty_mem_countableGeneratingSet) n)

Premises used: MeasurableSpace.measurableSet_countableGeneratingSet, Set.enumerateCountable_mem, MeasurableSpace.empty_mem_countableGeneratingSet
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_3
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
n : ℕ
⊢ (countablePartition α n).Finite

Tactic:
finite_memPartition _ n

Premises used: finite_memPartition, MeasurableSpace.countablePartition
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
h : CountablyGenerated α
n : ℕ
⊢ Finite.{u_1 + 1} (↑(countablePartition α n) : Type u_1)

Tactic:
Set.finite_coe_iff.mp (finite_countablePartition _ _)

Premises used: Set.Finite, Set.finite_coe_iff, MeasurableSpace.finite_countablePartition, Iff.mp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m : MeasurableSpace α
h : CountablyGenerated α
n : ℕ
s t : Set α
hs : s ∈ countablePartition α n
ht : t ∈ countablePartition α n
hst : s ≠ t
⊢ Disjoint s t

Tactic:
disjoint_memPartition _ n hs ht hst

Premises used: disjoint_memPartition
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_3
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
n : ℕ
⊢ ⋃₀ countablePartition α n = univ

Tactic:
sUnion_memPartition _ n

Premises used: sUnion_memPartition, MeasurableSpace.countablePartition
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m : MeasurableSpace α
h : CountablyGenerated α
n : ℕ
s : Set α
⊢ MeasurableSet s ↔ ∃ (S : Finset (Set α)), (↑S : Set (Set α)) ⊆ countablePartition α n ∧ s = ⋃₀ (↑S : Set (Set α))

Tactic:
measurableSet_generateFrom_memPartition_iff _ n s

Premises used: MeasurableSpace.measurableSet_generateFrom_memPartition_iff, MeasurableSpace.countablePartition
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m : MeasurableSpace α
h : CountablyGenerated α
n : ℕ
s : Set α
hs : s ∈ countablePartition α n
⊢ MeasurableSet s

Tactic:
measurableSet_succ_memPartition _ _ hs

Premises used: MeasurableSpace.measurableSet_succ_memPartition, MeasurableSpace.countablePartition
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_3
inst : MeasurableSpace α
inst_1 : CountablyGenerated α
n : ℕ
⊢ generateFrom (countablePartition α n) ≤ generateFrom (countablePartition α (n + 1))

Tactic:
generateFrom_memPartition_le_succ _ _

Premises used: MeasurableSpace.generateFrom_memPartition_le_succ, MeasurableSpace.countablePartition
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_3
m : MeasurableSpace α
inst : CountablyGenerated α
rw : generateFrom (⋃ (n : ℕ), memPartition (enumerateCountable (s := countableGeneratingSet α) ⋯ ∅) n) = m
rw₁ : generateFrom (range (enumerateCountable (s := countableGeneratingSet α) ⋯ ∅)) = m
rw₂ : generateFrom (countableGeneratingSet α) = m
rw₃ rw₄ : m = m
⊢ generateFrom (⋃ (n : ℕ), countablePartition α n) = m

Tactic:
rw [countablePartition, generateFrom_iUnion_memPartition,
    range_enumerateCountable_of_mem _ empty_mem_countableGeneratingSet,
    generateFrom_countableGeneratingSet]

Premises used: Set.range_enumerateCountable_of_mem, MeasurableSpace.empty_mem_countableGeneratingSet, MeasurableSpace.generateFrom_countableGeneratingSet, MeasurableSpace.generateFrom_iUnion_memPartition, MeasurableSpace.countablePartition
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_3
m : MeasurableSpace α
inst : CountablyGenerated α
n : ℕ
⊢ generateFrom (countablePartition α n) ≤ m

Tactic:
generateFrom_memPartition_le (measurableSet_enumerateCountable_countableGeneratingSet α) n

Premises used: MeasurableSpace.generateFrom_memPartition_le, MeasurableSpace.measurableSet_enumerateCountable_countableGeneratingSet, MeasurableSpace.countablePartition
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m : MeasurableSpace α
h : CountablyGenerated α
n : ℕ
s : Set α
hs : s ∈ countablePartition α n
⊢ MeasurableSet s

Tactic:
generateFrom_countablePartition_le α n _ (measurableSet_generateFrom hs)

Premises used: MeasurableSpace.measurableSet_generateFrom, MeasurableSpace.generateFrom_countablePartition_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m : MeasurableSpace α
h : CountablyGenerated α
n : ℕ
a : α
⊢ countablePartitionSet n a ∈ countablePartition α n

Tactic:
memPartitionSet_mem _ _ _

Premises used: Set.Mem, MeasurableSpace.countablePartitionSet, MeasurableSpace.countablePartition, memPartitionSet_mem
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m : MeasurableSpace α
h : CountablyGenerated α
n : ℕ
a : α
⊢ a ∈ countablePartitionSet n a

Tactic:
mem_memPartitionSet _ _ _

Premises used: Set.Mem, MeasurableSpace.countablePartitionSet, mem_memPartitionSet
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m : MeasurableSpace α
h : CountablyGenerated α
n : ℕ
a : α
s : Set α
hs : s ∈ countablePartition α n
⊢ countablePartitionSet n a = s ↔ a ∈ s

Tactic:
memPartitionSet_eq_iff _ hs

Premises used: memPartitionSet_eq_iff, MeasurableSpace.countablePartitionSet
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m : MeasurableSpace α
h : CountablyGenerated α
n : ℕ
a : α
s : Set α
hs : s ∈ countablePartition α n
ha : a ∈ s
⊢ countablePartitionSet n a = s

Tactic:
memPartitionSet_of_mem hs ha

Premises used: MeasurableSpace.countablePartitionSet, memPartitionSet_of_mem
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α : Type u_1
m : MeasurableSpace α
h : CountablyGenerated α
n : ℕ
a : α
⊢ MeasurableSet (countablePartitionSet n a)

Tactic:
measurableSet_countablePartition n (countablePartitionSet_mem n a)

Premises used: MeasurableSpace.countablePartitionSet_mem, MeasurableSpace.measurableSet_countablePartition
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α_1 : Type u_1
β : Type u_2
m : MeasurableSpace α_1
h : CountablyGenerated α_1
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
h1 : Countable α
inst_1 : MeasurableSpace β
⊢ CountableOrCountablyGenerated α β

Tactic:
⟨Or.inl h1⟩

Premises used: MeasurableSpace.CountableOrCountablyGenerated.mk, Or.inl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α_1 : Type u_1
β : Type u_2
m : MeasurableSpace α_1
h_1 : CountablyGenerated α_1
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
inst_1 : MeasurableSpace β
h : CountablyGenerated β
⊢ CountableOrCountablyGenerated α β

Tactic:
⟨Or.inr h⟩

Premises used: MeasurableSpace.CountableOrCountablyGenerated.mk, Or.inr
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α_1 : Type u_1
β : Type u_2
m : MeasurableSpace α_1
h : CountablyGenerated α_1
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
hα : CountableOrCountablyGenerated α γ
hβ : CountableOrCountablyGenerated β γ
inl : ∀ (hα : Countable α), CountableOrCountablyGenerated (α × β) γ
inr : ∀ (hα : CountablyGenerated γ), CountableOrCountablyGenerated (α × β) γ
⊢ CountableOrCountablyGenerated (α × β) γ

Tactic:
rcases hα with (hα | hα)
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α_1 : Type u_1
β : Type u_2
m : MeasurableSpace α_1
h : CountablyGenerated α_1
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
hβ : CountableOrCountablyGenerated β γ
hα : Countable α
inl : ∀ (hβ : Countable β), CountableOrCountablyGenerated (α × β) γ
inl₁ : ∀ (hβ : CountablyGenerated γ), CountableOrCountablyGenerated (α × β) γ
⊢ CountableOrCountablyGenerated (α × β) γ

Tactic:
rcases hβ with (hβ | hβ)
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α_1 : Type u_1
β : Type u_2
m : MeasurableSpace α_1
h : CountablyGenerated α_1
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
hβ : CountableOrCountablyGenerated β γ
hα : CountablyGenerated γ
inr : ∀ (hβ : Countable β), CountableOrCountablyGenerated (α × β) γ
inr₁ : ∀ (hβ : CountablyGenerated γ), CountableOrCountablyGenerated (α × β) γ
⊢ CountableOrCountablyGenerated (α × β) γ

Tactic:
rcases hβ with (hβ | hβ)
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α_1 : Type u_1
β : Type u_2
m : MeasurableSpace α_1
h : CountablyGenerated α_1
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
hα : Countable α
hβ : Countable β
⊢ CountableOrCountablyGenerated (α × β) γ

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α_1 : Type u_1
β : Type u_2
m : MeasurableSpace α_1
h : CountablyGenerated α_1
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
hα : Countable α
hβ : CountablyGenerated γ
⊢ CountableOrCountablyGenerated (α × β) γ

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α_1 : Type u_1
β : Type u_2
m : MeasurableSpace α_1
h : CountablyGenerated α_1
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
hα : CountablyGenerated γ
hβ : Countable β
⊢ CountableOrCountablyGenerated (α × β) γ

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
α_1 : Type u_1
β : Type u_2
m : MeasurableSpace α_1
h : CountablyGenerated α_1
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
hα hβ : CountablyGenerated γ
⊢ CountableOrCountablyGenerated (α × β) γ

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
β : Type u_2
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
inst_1 : Nonempty β
h : CountableOrCountablyGenerated (α × β) γ
inl : ∀ (h : Countable (α × β)), CountableOrCountablyGenerated α γ
inr : ∀ (h : CountablyGenerated γ), CountableOrCountablyGenerated α γ
⊢ CountableOrCountablyGenerated α γ

Tactic:
rcases h.countableOrCountablyGenerated with (h | h)

Premises used: MeasurableSpace.CountableOrCountablyGenerated.countableOrCountablyGenerated
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
β : Type u_2
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
inst_1 : Nonempty β
h_1 : CountableOrCountablyGenerated (α × β) γ
h : Countable (α × β)
⊢ Countable α

Tactic:
have := countable_left_of_prod_of_nonempty h
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
β : Type u_2
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
inst_1 : Nonempty β
h_1 : CountableOrCountablyGenerated (α × β) γ
h : Countable (α × β)
this : Countable α
⊢ CountableOrCountablyGenerated α γ

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
β : Type u_2
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
inst_1 : Nonempty β
h_1 : CountableOrCountablyGenerated (α × β) γ
h : CountablyGenerated γ
⊢ CountableOrCountablyGenerated α γ

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
β : Type u_2
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
inst_1 : Nonempty α
h : CountableOrCountablyGenerated (α × β) γ
inl : ∀ (h : Countable (α × β)), CountableOrCountablyGenerated β γ
inr : ∀ (h : CountablyGenerated γ), CountableOrCountablyGenerated β γ
⊢ CountableOrCountablyGenerated β γ

Tactic:
rcases h.countableOrCountablyGenerated with (h | h)

Premises used: MeasurableSpace.CountableOrCountablyGenerated.countableOrCountablyGenerated
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
β : Type u_2
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
inst_1 : Nonempty α
h_1 : CountableOrCountablyGenerated (α × β) γ
h : Countable (α × β)
⊢ Countable β

Tactic:
have := countable_right_of_prod_of_nonempty h
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
β : Type u_2
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
inst_1 : Nonempty α
h_1 : CountableOrCountablyGenerated (α × β) γ
h : Countable (α × β)
this : Countable β
⊢ CountableOrCountablyGenerated β γ

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
β : Type u_2
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
inst_1 : Nonempty α
h_1 : CountableOrCountablyGenerated (α × β) γ
h : CountablyGenerated γ
⊢ CountableOrCountablyGenerated β γ

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
β : Type u_2
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
h : CountableOrCountablyGenerated (α × β) γ
inl : ∀ (h : Countable (α × β)), CountableOrCountablyGenerated (β × α) γ
inr : ∀ (h : CountablyGenerated γ), CountableOrCountablyGenerated (β × α) γ
⊢ CountableOrCountablyGenerated (β × α) γ

Tactic:
rcases h with (h | h)
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
β : Type u_2
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
h : Countable (α × β)
⊢ CountableOrCountablyGenerated (β × α) γ

Tactic:
⟨Or.inl countable_prod_swap⟩

Premises used: MeasurableSpace.CountableOrCountablyGenerated.mk, Or.inl, countable_prod_swap
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
β : Type u_2
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
h : Countable (α × β)
⊢ CountableOrCountablyGenerated (β × α) γ

Tactic:
refine ⟨Or.inl countable_prod_swap⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
β : Type u_2
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
h : CountablyGenerated γ
⊢ CountableOrCountablyGenerated (β × α) γ

Tactic:
⟨Or.inr h⟩

Premises used: MeasurableSpace.CountableOrCountablyGenerated.mk, Or.inr
-- Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
Goal:
β : Type u_2
α : Type u_3
γ : Type u_4
inst : MeasurableSpace γ
h : CountablyGenerated γ
⊢ CountableOrCountablyGenerated (β × α) γ

Tactic:
exact ⟨Or.inr h⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
inst : MeasurableSpace α
⊢ MeasurableSet.{u_1} (α := α) ∅

Tactic:
MeasurableSpace.measurableSet_empty _

Premises used: MeasurableSet, MeasurableSpace.measurableSet_empty
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
s : Set α
m : MeasurableSpace α
⊢ MeasurableSet s → MeasurableSet sᶜ

Tactic:
MeasurableSpace.measurableSet_compl _ s

Premises used: MeasurableSet, MeasurableSpace.measurableSet_compl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
s : Set α
m : MeasurableSpace α
h : MeasurableSet sᶜ
⊢ MeasurableSet s

Tactic:
compl_compl s ▸ h.compl

Premises used: compl_compl, Eq.rec, MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
s : Set α
m : MeasurableSpace α
⊢ MeasurableSet sᶜ ↔ MeasurableSet s

Tactic:
⟨.of_compl, .compl⟩

Premises used: MeasurableSet.of_compl, MeasurableSet.compl, Iff.intro
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
⊢ MeasurableSet.{u_1} (α := α) univᶜ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Subsingleton α
s : Set α
⊢ MeasurableSet s

Tactic:
Subsingleton.set_cases MeasurableSet.empty MeasurableSet.univ s

Premises used: Subsingleton.set_cases
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m : MeasurableSpace α
s t : Set α
hs : MeasurableSet s
h : s = t
rwa rwa₁ rwa₂ rwa₃ : MeasurableSet s
⊢ MeasurableSet t

Tactic:
rwa [← h]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
inl : IsEmpty ι → MeasurableSet.{u_1} (α := α) (⋃ (b : ι), f b)
inr : Nonempty ι → MeasurableSet.{u_1} (α := α) (⋃ (b : ι), f b)
⊢ MeasurableSet.{u_1} (α := α) (⋃ (b : ι), f b)

Tactic:
cases isEmpty_or_nonempty ι

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

Tactic:
simp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h_1 : Nonempty ι
inr : ∀ (e : ℕ → ι) (he : Surjective e), MeasurableSet.{u_1} (α := α) (⋃ (b : ι), f b)
⊢ MeasurableSet.{u_1} (α := α) (⋃ (b : ι), f b)

Tactic:
rcases exists_surjective_nat ι with ⟨e, he⟩

Premises used: exists_surjective_nat
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h_1 : Nonempty ι
e : ℕ → ι
he : Surjective e
inr : MeasurableSet.{u_1} (α := α) (⋃ (x : ℕ), f (e x))
⊢ MeasurableSet.{u_1} (α := α) (⋃ (b : ι), f b)

Tactic:
rw [← iUnion_congr_of_surjective _ he (fun _ => rfl)]

Premises used: Set.iUnion_congr_of_surjective, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h_1 : Nonempty ι
e : ℕ → ι
he : Surjective e
⊢ MeasurableSet.{u_1} (α := α) (⋃ (x : ℕ), f (e x))

Tactic:
m.measurableSet_iUnion _ fun _ => h _

Premises used: MeasurableSet, MeasurableSpace.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)
h_1 : Nonempty ι
e : ℕ → ι
he : Surjective e
⊢ MeasurableSet.{u_1} (α := α) (⋃ (x : ℕ), f (e x))

Tactic:
exact m.measurableSet_iUnion _ fun _ => h _

Premises used: MeasurableSpace.measurableSet_iUnion
-- 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} (α := α) (⋃ (x : (↑s : Type u_2)), f (↑x : β))
⊢ MeasurableSet.{u_1} (α := α) (⋃ b ∈ s, f b)

Tactic:
rw [biUnion_eq_iUnion]

Premises used: Set.biUnion_eq_iUnion
-- 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)
⊢ Countable.{u_2 + 1} (↑s : Type u_2)

Tactic:
have := hs.to_subtype
-- 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)
this : Countable.{u_2 + 1} (↑s : Type u_2)
⊢ ∀ (b : (↑s : Type u_2)), MeasurableSet (f (↑b : β))

Tactic:
simpa using h
-- 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)
this : Countable.{u_2 + 1} (↑s : Type u_2)
⊢ MeasurableSet.{u_1} (α := α) (⋃ (x : (↑s : Type u_2)), f (↑x : β))

Tactic:
exact MeasurableSet.iUnion (by simpa using h)

Premises used: MeasurableSet.iUnion