awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
s : Set (Set α)
P : Finset (Set α)
hP : P.Nonempty
PC : (↑P : Set (Set α)) ⊆ s
⊢ MeasurableSet (⋃₀ (↑P : Set (Set α)))

Tactic:
exact MeasurableSet.sUnion (Finset.countable_toSet P)
    (fun s hs ↦ measurableSet_generateFrom (PC hs))

Premises used: MeasurableSet.sUnion, MeasurableSpace.measurableSet_generateFrom, Finset.countable_toSet
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : Subsingleton α
⊢ Measurable f

Tactic:
fun _ _ =>
  @Subsingleton.measurableSet α _ _ _

Premises used: Subsingleton.measurableSet, Measurable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : Subsingleton β
f : α → β
⊢ Measurable f

Tactic:
fun s _ => Subsingleton.set_cases MeasurableSet.empty MeasurableSet.univ s

Premises used: Measurable, Subsingleton.set_cases
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : One α
⊢ Measurable.{u_2, u_1} (α := β) (β := α) 1

Tactic:
@measurable_const _ _ _ _ 1

Premises used: measurable_const
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : IsEmpty α
f : α → β
⊢ Measurable f

Tactic:
Subsingleton.measurable

Premises used: Subsingleton.measurable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : IsEmpty β
f : α → β
⊢ Measurable f

Tactic:
measurable_of_subsingleton_codomain f

Premises used: measurable_of_subsingleton_codomain
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : β → α
hf : ∀ (x y : β), f x = f y
⊢ Nontrivial β

Tactic:
nontriviality β
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : β → α
hf : ∀ (x y : β), f x = f y
h : Nontrivial β
inhabit : ∀ (inhabited_h : Inhabited β), Measurable f
⊢ Measurable f

Tactic:
inhabit β
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : β → α
hf : ∀ (x y : β), f x = f y
h : Nontrivial β
inhabited_h : Inhabited β
⊢ Measurable.{u_2, u_1} (β := α) fun (x : β) ↦ f default

Tactic:
@measurable_const α β _ _ (f default)

Premises used: measurable_const
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : β → α
hf : ∀ (x y : β), f x = f y
h_1 : Nontrivial β
inhabited_h : Inhabited β
h : ∀ (x : β), f x = f default
⊢ Measurable f

Tactic:
convert! @measurable_const α β _ _ (f default) using 2

Premises used: measurable_const
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : β → α
hf : ∀ (x y : β), f x = f y
h : Nontrivial β
inhabited_h : Inhabited β
x : β
⊢ f x = f default

Tactic:
apply hf
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : NatCast α
n : ℕ
⊢ Measurable.{u_2, u_1} (α := β) (β := α) (↑n : β → α)

Tactic:
@measurable_const α _ _ _ n

Premises used: measurable_const
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : IntCast α
n : ℤ
⊢ Measurable.{u_2, u_1} (α := β) (β := α) (↑n : β → α)

Tactic:
@measurable_const α _ _ _ n

Premises used: measurable_const
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : Countable α
inst_3 : MeasurableSingletonClass α
f : α → β
⊢ Measurable f

Tactic:
fun s _ =>
  (f ⁻¹' s).to_countable.measurableSet

Premises used: Measurable, Set.Countable.measurableSet, Set.preimage, Set.to_countable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : Finite α
inst_3 : MeasurableSingletonClass α
f : α → β
⊢ Measurable f

Tactic:
measurable_of_countable f

Premises used: measurable_of_countable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
t : Set β
hf : Measurable f
ht : MeasurableSet t
⊢ MeasurableSet (f ⁻¹' t)

Tactic:
hf ht
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
t : Set β
ht : MeasurableSet t
hf : Measurable f
⊢ MeasurableSet (f ⁻¹' t)

Tactic:
hf ht
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
s : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
x : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : Measurable f
hg : Measurable g
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (s.piecewise (β := fun (a : α) ↦ β) f g ⁻¹' t)

Tactic:
simpa [piecewise_preimage] using hs.ite (hf ht) (hg ht)

Premises used: MeasurableSet.ite, Set.piecewise_preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
p : α → Prop
x : DecidablePred p
hp : MeasurableSet.{u_1} (α := α) {a : α | p a}
hf : Measurable f
hg : Measurable g
⊢ Measurable.{u_1, u_2} (β := β) fun (x_1 : α) ↦ if p x_1 then f x_1 else g x_1

Tactic:
Measurable.piecewise hp hf hg

Premises used: Set.Mem, Measurable.piecewise, Set.piecewise
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : Zero β
hf : Measurable f
hs : MeasurableSet s
⊢ Measurable (s.indicator f)

Tactic:
hf.piecewise hs measurable_const

Premises used: Set.indicator, Measurable.piecewise, measurable_const
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : Zero β
inst_1 : MeasurableSingletonClass β
b : β
inst_2 : NeZero b
mp : Measurable.{u_1, u_2} (β := β) (s.indicator fun (x : α) ↦ b) → MeasurableSet s
mpr : MeasurableSet s → Measurable.{u_1, u_2} (β := β) (s.indicator fun (x : α) ↦ b)
⊢ Measurable.{u_1, u_2} (β := β) (s.indicator fun (x : α) ↦ b) ↔ MeasurableSet s

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : Zero β
inst_1 : MeasurableSingletonClass β
b : β
inst_2 : NeZero b
h : Measurable.{u_1, u_2} (β := β) (s.indicator fun (x : α) ↦ b)
⊢ MeasurableSet (preimage (β := β) (s.indicator fun (x : α) ↦ b) {0}ᶜ)

Tactic:
h (MeasurableSet.singleton (0 : β)).compl

Premises used: MeasurableSet.singleton, MeasurableSet.compl, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : Zero β
inst_1 : MeasurableSingletonClass β
b : β
inst_2 : NeZero b
h : Measurable.{u_1, u_2} (β := β) (s.indicator fun (x : α) ↦ b)
h₁ : s = preimage (β := β) (s.indicator fun (x : α) ↦ b) {0}ᶜ
⊢ MeasurableSet s

Tactic:
convert! h (MeasurableSet.singleton (0 : β)).compl

Premises used: MeasurableSet.singleton, MeasurableSet.compl, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : Zero β
inst_1 : MeasurableSingletonClass β
b : β
inst_2 : NeZero b
h : Measurable.{u_1, u_2} (β := β) (s.indicator fun (x : α) ↦ b)
h₁ : ∀ (a : α), a ∈ s ↔ a ∈ preimage (β := β) (s.indicator fun (x : α) ↦ b) {0}ᶜ
⊢ s = preimage (β := β) (s.indicator fun (x : α) ↦ b) {0}ᶜ

Tactic:
ext a
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : Zero β
inst_1 : MeasurableSingletonClass β
b : β
inst_2 : NeZero b
h : Measurable.{u_1, u_2} (β := β) (s.indicator fun (x : α) ↦ b)
a : α
⊢ a ∈ s ↔ a ∈ preimage (β := β) (s.indicator fun (x : α) ↦ b) {0}ᶜ

Tactic:
simp [NeZero.ne b]

Premises used: NeZero.ne
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : Zero β
inst_1 : MeasurableSingletonClass β
b : β
inst_2 : NeZero b
h : MeasurableSet s
⊢ Measurable.{u_1, u_2} (β := β) (s.indicator fun (x : α) ↦ b)

Tactic:
measurable_const.indicator h

Premises used: Measurable.indicator, measurable_const
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : Zero β
inst_1 : MeasurableSingletonClass β
b : β
inst_2 : NeZero b
h : MeasurableSet s
⊢ Measurable.{u_1, u_2} (β := β) (s.indicator fun (x : α) ↦ b)

Tactic:
exact measurable_const.indicator h

Premises used: Measurable.indicator, measurable_const
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : One β
inst_1 : MeasurableSingletonClass β
hf : Measurable f
⊢ MeasurableSet (Function.mulSupport f)

Tactic:
hf (measurableSet_singleton 1).compl

Premises used: MeasurableSingletonClass.measurableSet_singleton, Set.Mem, setOf, MeasurableSet.compl, Set.preimage, Set.singleton, Function.mulSupport, OfNat.ofNat, Not
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable.{u_1} (α := α) {x : α | f x ≠ g x}
t : Set β
ht : MeasurableSet t
⊢ g ⁻¹' t = g ⁻¹' t ∩ {x : α | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x : α | f x = g x}

Tactic:
simp [← inter_union_distrib_left]

Premises used: Set.inter_union_distrib_left
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable.{u_1} (α := α) {x : α | f x ≠ g x}
t : Set β
ht : MeasurableSet t
⊢ g ⁻¹' t = g ⁻¹' t ∩ {x : α | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x : α | f x = g x}

Tactic:
have : g ⁻¹' t = g ⁻¹' t ∩ { x | f x = g x }ᶜ ∪ g ⁻¹' t ∩ { x | f x = g x } := by
    simp [← inter_union_distrib_left]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable.{u_1} (α := α) {x : α | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this : g ⁻¹' t = g ⁻¹' t ∩ {x : α | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x : α | f x = g x}
rw : MeasurableSet (g ⁻¹' t ∩ {x : α | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x : α | f x = g x})
⊢ MeasurableSet (g ⁻¹' t)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable.{u_1} (α := α) {x : α | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this : g ⁻¹' t = g ⁻¹' t ∩ {x : α | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x : α | f x = g x}
⊢ MeasurableSet (g ⁻¹' t ∩ {x : α | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x : α | f x = g x})

Tactic:
(h.mono inter_subset_right).measurableSet.union ?_

Premises used: Set.Mem, setOf, Set.Countable.measurableSet, Set.Countable.mono, MeasurableSet.union, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable.{u_1} (α := α) {x : α | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this : g ⁻¹' t = g ⁻¹' t ∩ {x : α | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x : α | f x = g x}
refine : MeasurableSet (g ⁻¹' t ∩ {x : α | f x = g x})
⊢ MeasurableSet (g ⁻¹' t ∩ {x : α | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x : α | f x = g x})

Tactic:
refine (h.mono inter_subset_right).measurableSet.union ?_

Premises used: Set.Countable.measurableSet, Set.Countable.mono, MeasurableSet.union, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable.{u_1} (α := α) {x : α | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this : g ⁻¹' t = g ⁻¹' t ∩ {x : α | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x : α | f x = g x}
h₁ : ∀ (x : α), x ∈ g ⁻¹' t ∩ {x : α | f x = g x} ↔ x ∈ f ⁻¹' t ∩ {x : α | f x = g x}
⊢ g ⁻¹' t ∩ {x : α | f x = g x} = f ⁻¹' t ∩ {x : α | f x = g x}

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable.{u_1} (α := α) {x : α | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this : g ⁻¹' t = g ⁻¹' t ∩ {x : α | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x : α | f x = g x}
x : α
⊢ x ∈ g ⁻¹' t ∩ {x : α | f x = g x} ↔ x ∈ f ⁻¹' t ∩ {x : α | f x = g x}

Tactic:
simp +contextual
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable.{u_1} (α := α) {x : α | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this : g ⁻¹' t = g ⁻¹' t ∩ {x : α | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x : α | f x = g x}
⊢ g ⁻¹' t ∩ {x : α | f x = g x} = f ⁻¹' t ∩ {x : α | f x = g x}

Tactic:
have : g ⁻¹' t ∩ { x : α | f x = g x } = f ⁻¹' t ∩ { x : α | f x = g x } := by
    ext x
    simp +contextual
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable.{u_1} (α := α) {x : α | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this_1 : g ⁻¹' t = g ⁻¹' t ∩ {x : α | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x : α | f x = g x}
this : g ⁻¹' t ∩ {x : α | f x = g x} = f ⁻¹' t ∩ {x : α | f x = g x}
rw : MeasurableSet (f ⁻¹' t ∩ {x : α | f x = g x})
⊢ MeasurableSet (g ⁻¹' t ∩ {x : α | f x = g x})

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable.{u_1} (α := α) {x : α | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this_1 : g ⁻¹' t = g ⁻¹' t ∩ {x : α | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x : α | f x = g x}
this : g ⁻¹' t ∩ {x : α | f x = g x} = f ⁻¹' t ∩ {x : α | f x = g x}
⊢ MeasurableSet (f ⁻¹' t ∩ {x : α | f x = g x})

Tactic:
(hf ht).inter h.measurableSet.of_compl

Premises used: MeasurableSet.of_compl, Set.Countable.measurableSet, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable.{u_1} (α := α) {x : α | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this_1 : g ⁻¹' t = g ⁻¹' t ∩ {x : α | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x : α | f x = g x}
this : g ⁻¹' t ∩ {x : α | f x = g x} = f ⁻¹' t ∩ {x : α | f x = g x}
⊢ MeasurableSet (f ⁻¹' t ∩ {x : α | f x = g x})

Tactic:
exact (hf ht).inter h.measurableSet.of_compl

Premises used: MeasurableSet.of_compl, Set.Countable.measurableSet, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
⊢ IsCountablySpanning.{u_1} (α := α) {s : Set α | MeasurableSet s}

Tactic:
⟨fun _ => univ, fun _ => MeasurableSet.univ, iUnion_const _⟩

Premises used: Set.univ, Set.iUnion_const, And.intro, Exists.intro, IsCountablySpanning, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
rcases :
  ∀ (s : ℕ → Set α) (h1s : ∀ (n : ℕ), s n ∈ C) (h2s : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), s n) univ) (t : ℕ → Set β)
    (h1t : ∀ (n : ℕ), t n ∈ D) (h2t : Eq.{u_2 + 1} (α := Set β) (⋃ (n : ℕ), t n) univ),
    IsCountablySpanning (α := α × β) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D)
⊢ IsCountablySpanning (α := α × β) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D)

Tactic:
rcases hC, hD with ⟨⟨s, h1s, h2s⟩, t, h1t, h2t⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), s n) univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : Eq.{u_2 + 1} (α := Set β) (⋃ (n : ℕ), t n) univ
⊢ IsCountablySpanning (α := α × β) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D)

Tactic:
⟨fun n => s n.unpair.1 ×ˢ t n.unpair.2, fun n => mem_image2_of_mem (h1s _) (h1t _), ?_⟩

Premises used: SProd.sprod, Nat.unpair, Prod.fst, And.intro, Exists.intro, IsCountablySpanning, Set.mem_image2_of_mem, Prod.snd
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), s n) univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : Eq.{u_2 + 1} (α := Set β) (⋃ (n : ℕ), t n) univ
refine : Eq (α := Set (α × β)) (⋃ (n : ℕ), (fun (n : ℕ) ↦ s (Nat.unpair n).1 ×ˢ t (Nat.unpair n).2) n) univ
⊢ IsCountablySpanning (α := α × β) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D)

Tactic:
refine ⟨fun n => s n.unpair.1 ×ˢ t n.unpair.2, fun n => mem_image2_of_mem (h1s _) (h1t _), ?_⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), s n) univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : Eq.{u_2 + 1} (α := Set β) (⋃ (n : ℕ), t n) univ
rw : SProd.sprod (α := Set α) (β := Set β) (⋃ (n : ℕ), s n) (⋃ (n : ℕ), t n) = univ
rw₁ : SProd.sprod (α := Set α) (β := Set β) univ (⋃ (n : ℕ), t n) = univ
rw₂ : SProd.sprod (α := Set α) (β := Set β) univ univ = univ
rw₃ rw₄ : Eq (α := Set (α × β)) univ univ
⊢ Eq (α := Set (α × β)) (⋃ (n : ℕ), (fun (n : ℕ) ↦ s (Nat.unpair n).1 ×ˢ t (Nat.unpair n).2) n) univ

Tactic:
rw [iUnion_unpair_prod, h2s, h2t, univ_prod_univ]

Premises used: Set.iUnion_unpair_prod, Set.univ_prod_univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
unfold :
  s ⊆
    have S : Set (Set α) := ⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < i), generateMeasurableRec s j;
    s ∪ {∅} ∪ compl '' S ∪ range fun (f : ℕ → (↑S : Type u)) ↦ ⋃ (n : ℕ), (↑(f n) : Set α)
⊢ s ⊆ generateMeasurableRec s i

Tactic:
unfold generateMeasurableRec

Premises used: MeasurableSpace.generateMeasurableRec
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
h : s ⊆ s
⊢ s ⊆
    have S : Set (Set α) := ⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < i), generateMeasurableRec s j;
    s ∪ {∅} ∪ compl '' S ∪ range fun (f : ℕ → (↑S : Type u)) ↦ ⋃ (n : ℕ), (↑(f n) : Set α)

Tactic:
apply_rules [subset_union_of_subset_left]

Premises used: Set.subset_union_of_subset_left
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
⊢ s ⊆ s

Tactic:
subset_rfl

Premises used: subset_rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
⊢ s ⊆ s

Tactic:
exact subset_rfl

Premises used: subset_rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
unfold :
  Membership.mem (γ := Set (Set α))
    (have S : Set (Set α) := ⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < i), generateMeasurableRec s j;
    s ∪ {∅} ∪ compl '' S ∪ range fun (f : ℕ → (↑S : Type u)) ↦ ⋃ (n : ℕ), (↑(f n) : Set α))
    ∅
⊢ ∅ ∈ generateMeasurableRec s i

Tactic:
unfold generateMeasurableRec

Premises used: MeasurableSpace.generateMeasurableRec
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
⊢ Membership.mem (γ := Set (Set α))
    (have S : Set (Set α) := ⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < i), generateMeasurableRec s j;
    s ∪ {∅} ∪ compl '' S ∪ range fun (f : ℕ → (↑S : Type u)) ↦ ⋃ (n : ℕ), (↑(f n) : Set α))
    ∅

Tactic:
mem_union_left _ (mem_union_left _ (mem_union_right _ (mem_singleton ∅)))

Premises used: Set.mem_singleton, Set.Mem, Set.mem_union_right, Set.mem_union_left, EmptyCollection.emptyCollection
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
⊢ Membership.mem (γ := Set (Set α))
    (have S : Set (Set α) := ⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < i), generateMeasurableRec s j;
    s ∪ {∅} ∪ compl '' S ∪ range fun (f : ℕ → (↑S : Type u)) ↦ ⋃ (n : ℕ), (↑(f n) : Set α))
    ∅

Tactic:
exact mem_union_left _ (mem_union_left _ (mem_union_right _ (mem_singleton ∅)))

Premises used: Set.mem_singleton, Set.mem_union_right, Set.mem_union_left, EmptyCollection.emptyCollection
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i j : Ordinal.{u_1}
h : j < i
t : Set α
ht : t ∈ generateMeasurableRec s j
unfold :
  Membership.mem (γ := Set (Set α))
    (have S : Set (Set α) := ⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < i), generateMeasurableRec s j;
    s ∪ {∅} ∪ compl '' S ∪ range fun (f : ℕ → (↑S : Type u)) ↦ ⋃ (n : ℕ), (↑(f n) : Set α))
    tᶜ
⊢ tᶜ ∈ generateMeasurableRec s i

Tactic:
unfold generateMeasurableRec

Premises used: MeasurableSpace.generateMeasurableRec
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i j : Ordinal.{u_1}
h : j < i
t : Set α
ht : t ∈ generateMeasurableRec s j
⊢ Membership.mem (γ := Set (Set α))
    (have S : Set (Set α) := ⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < i), generateMeasurableRec s j;
    s ∪ {∅} ∪ compl '' S ∪ range fun (f : ℕ → (↑S : Type u)) ↦ ⋃ (n : ℕ), (↑(f n) : Set α))
    tᶜ

Tactic:
mem_union_left _ (mem_union_right _ ⟨t, mem_iUnion₂.2 ⟨j, h, ht⟩, rfl⟩)

Premises used: Iff.mpr, Set.Mem, Set.mem_union_right, Set.mem_iUnion₂, And.intro, Exists.intro, Set.mem_union_left, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i j : Ordinal.{u_1}
h : j < i
t : Set α
ht : t ∈ generateMeasurableRec s j
⊢ Membership.mem (γ := Set (Set α))
    (have S : Set (Set α) := ⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < i), generateMeasurableRec s j;
    s ∪ {∅} ∪ compl '' S ∪ range fun (f : ℕ → (↑S : Type u)) ↦ ⋃ (n : ℕ), (↑(f n) : Set α))
    tᶜ

Tactic:
exact mem_union_left _ (mem_union_right _ ⟨t, mem_iUnion₂.2 ⟨j, h, ht⟩, rfl⟩)
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
f : ℕ → Set α
hf : ∀ (n : ℕ), ∃ j < i, f n ∈ generateMeasurableRec s j
unfold :
  Membership.mem (γ := Set (Set α))
    (have S : Set (Set α) := ⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < i), generateMeasurableRec s j;
    s ∪ {∅} ∪ compl '' S ∪ range fun (f : ℕ → (↑S : Type u)) ↦ ⋃ (n : ℕ), (↑(f n) : Set α))
    (⋃ (n : ℕ), f n)
⊢ ⋃ (n : ℕ), f n ∈ generateMeasurableRec s i

Tactic:
unfold generateMeasurableRec

Premises used: MeasurableSpace.generateMeasurableRec