awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
C : (i : ι) → Set (Set (α i))
val : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), Eq.{u_2 + 1} (α := Set (α i)) (⋃ (n : ℕ), t i n) univ
this :
  Eq (α := Set ((i : ι) → α i))
    (Set.pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (i' : ι) ↦ iUnion (t i')) i (⋃ (x : ℕ), s)))
    (Set.pi (α := α) univ fun (k : ι) ↦
      ⋃ (j : ℕ), update (β := fun (i' : ι) ↦ Set (α i')) (fun (i' : ι) ↦ t i' j) i s k)
n : (a : ι) → ℕ
intro :
  (Set.pi (α := α) univ fun (a : ι) ↦ update (β := fun (i' : ι) ↦ Set (α i')) (fun (i' : ι) ↦ t i' (n a)) i s a) ∈
    Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
⊢ MeasurableSet (α := (a : ι) → α a)
    (Set.pi (α := α) univ fun (a : ι) ↦ update (β := fun (i' : ι) ↦ Set (α i')) (fun (i' : ι) ↦ t i' (n a)) i s a)

Tactic:
apply measurableSet_generateFrom

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
C : (i : ι) → Set (Set (α i))
val : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), Eq.{u_2 + 1} (α := Set (α i)) (⋃ (n : ℕ), t i n) univ
this :
  Eq (α := Set ((i : ι) → α i))
    (Set.pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (i' : ι) ↦ iUnion (t i')) i (⋃ (x : ℕ), s)))
    (Set.pi (α := α) univ fun (k : ι) ↦
      ⋃ (j : ℕ), update (β := fun (i' : ι) ↦ Set (α i')) (fun (i' : ι) ↦ t i' j) i s k)
n : (a : ι) → ℕ
intro :
  (fun (a : ι) ↦ update (β := fun (i' : ι) ↦ Set (α i')) (fun (i' : ι) ↦ t i' (n a)) i s a) ∈
    Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
⊢ (Set.pi (α := α) univ fun (a : ι) ↦ update (β := fun (i' : ι) ↦ Set (α i')) (fun (i' : ι) ↦ t i' (n a)) i s a) ∈
    Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C

Tactic:
apply mem_image_of_mem

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
C : (i : ι) → Set (Set (α i))
val : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), Eq.{u_2 + 1} (α := Set (α i)) (⋃ (n : ℕ), t i n) univ
this :
  Eq (α := Set ((i : ι) → α i))
    (Set.pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (i' : ι) ↦ iUnion (t i')) i (⋃ (x : ℕ), s)))
    (Set.pi (α := α) univ fun (k : ι) ↦
      ⋃ (j : ℕ), update (β := fun (i' : ι) ↦ Set (α i')) (fun (i' : ι) ↦ t i' j) i s k)
n : (a : ι) → ℕ
⊢ (fun (a : ι) ↦ update (β := fun (i' : ι) ↦ Set (α i')) (fun (i' : ι) ↦ t i' (n a)) i s a) ∈
    Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C

Tactic:
grind
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val : Encodable ι
intro : ∀ t ∈ Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C, MeasurableSet t
⊢ generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C) ≤ MeasurableSpace.pi (X := α)

Tactic:
apply generateFrom_le

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
intro : MeasurableSet (α := (i : ι) → α i) (⋂ (i : ι), eval (β := α) i ⁻¹' s i)
⊢ MeasurableSet (Set.pi (α := α) univ s)

Tactic:
rw [univ_pi_eq_iInter]

Premises used: Set.univ_pi_eq_iInter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
intro : ∀ (b : ι), MeasurableSet (eval (β := α) b ⁻¹' s b)
⊢ MeasurableSet (α := (i : ι) → α i) (⋂ (i : ι), eval (β := α) i ⁻¹' s i)

Tactic:
apply MeasurableSet.iInter

Premises used: MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
i : ι
intro : MeasurableSet (s i)
⊢ MeasurableSet (eval (β := α) i ⁻¹' s i)

Tactic:
apply @measurable_pi_apply _ _ (fun i => generateFrom (C i))

Premises used: measurable_pi_apply
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
i : ι
⊢ MeasurableSet (s i)

Tactic:
measurableSet_generateFrom (hs i (mem_univ i))

Premises used: MeasurableSpace.measurableSet_generateFrom, Set.mem_univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
i : ι
⊢ MeasurableSet (s i)

Tactic:
exact measurableSet_generateFrom (hs i (mem_univ i))

Premises used: MeasurableSpace.measurableSet_generateFrom, Set.mem_univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
intro :
  ∀ (val : Encodable ι),
    MeasurableSpace.pi (X := α) = generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
intro₁ :
  ∀ (val : Encodable ι),
    MeasurableSpace.pi (X := α) ≤ generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
intro₂ intro₃ :
  ∀ (val : Encodable ι),
    generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C) ≤ MeasurableSpace.pi (X := α)
⊢ MeasurableSpace.pi (X := α) = generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)

Tactic:
classical
  cases nonempty_encodable ι
  apply le_antisymm
  · refine iSup_le ?_; intro i; rw [comap_generateFrom]
    apply generateFrom_le; rintro _ ⟨s, hs, rfl⟩
    choose t h1t h2t using hC
    simp_rw [eval_preimage, ← h2t]
    rw [← @iUnion_const _ ℕ _ s]
    have : Set.pi univ (update (fun i' : ι => iUnion (t i')) i (⋃ _ : ℕ, s)) =
        Set.pi univ fun k => ⋃ j : ℕ,
        @update ι (fun i' => Set (α i')) _ (fun i' => t i' j) i s k := by
      ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
      by_cases h : i' = i
      · subst h; simp
      · simp [h]
    rw [this, ← iUnion_univ_pi]
    apply MeasurableSet.iUnion
    intro n; apply measurableSet_generateFrom
    -- `grind` can close the goal alone, but is slow
    apply mem_image_of_mem
    grind
  · apply generateFrom_le; rintro _ ⟨s, hs, rfl⟩
    rw [univ_pi_eq_iInter]; apply MeasurableSet.iInter; intro i
    apply @measurable_pi_apply _ _ (fun i => generateFrom (C i))
    exact measurableSet_generateFrom (hs i (mem_univ i))

Premises used: Set.univ_pi_eq_iInter, Set.eval_preimage, MeasurableSpace.measurableSet_generateFrom, measurable_pi_apply, nonempty_encodable, le_antisymm, Set.mem_image_of_mem, iSup_le, MeasurableSet.iUnion, Set.iUnion_univ_pi, MeasurableSpace.comap_generateFrom, MeasurableSet.iInter, rfl, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
h : (i : ι) → MeasurableSpace (α i)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = h i
h2C : ∀ (i : ι), IsCountablySpanning (C i)
⊢ generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C) = MeasurableSpace.pi (X := α)

Tactic:
simp +instances only [← funext hC, generateFrom_pi_eq h2C]

Premises used: generateFrom_pi_eq, funext
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : (i : ι) → MeasurableSpace (α i)
⊢ Eq (α := MeasurableSpace ((i : ι) → α i))
    (generateFrom
      (Set.pi (α := α) univ ''
        Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
    (MeasurableSpace.pi (X := α))

Tactic:
generateFrom_eq_pi (fun _ => generateFrom_measurableSet) fun _ =>
    isCountablySpanning_measurableSet

Premises used: isCountablySpanning_measurableSet, generateFrom_eq_pi, MeasurableSpace.generateFrom_measurableSet
-- Module: Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict
Goal:
α : Type u_1
inst : Preorder α
X : α → Type u_2
inst_1 : (a : α) → MeasurableSpace (X a)
a : α
⊢ Measurable (α := (a : α) → X a) (β := (a_1 : (↑(Set.Iic a) : Type u_1)) → X (↑a_1 : α)) (restrictLe (π := X) a)

Tactic:
Set.measurable_restrict _

Premises used: Preorder.restrictLe, Set.measurable_restrict
-- Module: Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict
Goal:
α : Type u_1
inst : Preorder α
X : α → Type u_2
inst_1 : (a : α) → MeasurableSpace (X a)
a b : α
hab : a ≤ b
⊢ Measurable (α := (a : (↑(Set.Iic b) : Type u_1)) → X (↑a : α)) (restrictLe₂ (π := X) hab)

Tactic:
Set.measurable_restrict₂ _

Premises used: Preorder.restrictLe₂, Set.measurable_restrict₂
-- Module: Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict
Goal:
α : Type u_1
inst : Preorder α
X : α → Type u_2
inst_1 : (a : α) → MeasurableSpace (X a)
inst_2 : LocallyFiniteOrderBot α
a : α
⊢ Measurable (α := (i : α) → X i) (β := (i : ↥(Finset.Iic a)) → X (↑i : α)) (frestrictLe (π := X) a)

Tactic:
Finset.measurable_restrict _

Premises used: Finset.measurable_restrict, Preorder.frestrictLe
-- Module: Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict
Goal:
α : Type u_1
inst : Preorder α
X : α → Type u_2
inst_1 : (a : α) → MeasurableSpace (X a)
inst_2 : LocallyFiniteOrderBot α
a b : α
hab : a ≤ b
⊢ Measurable (α := (i : ↥(Finset.Iic b)) → X (↑i : α)) (frestrictLe₂ (π := X) hab)

Tactic:
Finset.measurable_restrict₂ _

Premises used: Finset.measurable_restrict₂, Preorder.frestrictLe₂
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
a :
  LE.le (α := MeasurableSpace (α × β)) Prod.instMeasurableSpace
    (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
a₁ :
  LE.le (α := MeasurableSpace (α × β)) (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
    Prod.instMeasurableSpace
⊢ Eq (α := MeasurableSpace (α × β)) Prod.instMeasurableSpace
    (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ LE.le (α := MeasurableSpace (α × β)) Prod.instMeasurableSpace
    (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))

Tactic:
sup_le ?_ ?_

Premises used: sup_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
a :
  LE.le (α := MeasurableSpace (α × β)) (MeasurableSpace.comap Prod.fst (generateFrom C))
    (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
a₁ :
  LE.le (α := MeasurableSpace (α × β)) (MeasurableSpace.comap Prod.snd (generateFrom D))
    (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
⊢ LE.le (α := MeasurableSpace (α × β)) Prod.instMeasurableSpace
    (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))

Tactic:
refine sup_le ?_ ?_

Premises used: sup_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
a :
  LE.le (α := MeasurableSpace (α × β)) (generateFrom (preimage Prod.fst '' C))
    (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
⊢ LE.le (α := MeasurableSpace (α × β)) (MeasurableSpace.comap Prod.fst (generateFrom C))
    (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))

Tactic:
rw [comap_generateFrom]

Premises used: MeasurableSpace.comap_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
a :
  LE.le (α := MeasurableSpace (α × β)) (generateFrom (preimage Prod.snd '' D))
    (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
⊢ LE.le (α := MeasurableSpace (α × β)) (MeasurableSpace.comap Prod.snd (generateFrom D))
    (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))

Tactic:
rw [comap_generateFrom]

Premises used: MeasurableSpace.comap_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
a : ∀ (t : Set (α × β)), Membership.mem (γ := Set (Set (α × β))) (preimage Prod.fst '' C) t → MeasurableSet t
⊢ LE.le (α := MeasurableSpace (α × β)) (generateFrom (preimage Prod.fst '' C))
    (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))

Tactic:
apply generateFrom_le

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
a : ∀ (t : Set (α × β)), Membership.mem (γ := Set (Set (α × β))) (preimage Prod.snd '' D) t → MeasurableSet t
⊢ LE.le (α := MeasurableSpace (α × β)) (generateFrom (preimage Prod.snd '' D))
    (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))

Tactic:
apply generateFrom_le

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
hs : s ∈ C
a :
  ∀ (t : ℕ → Set β) (h1t : ∀ (n : ℕ), t n ∈ D) (h2t : Eq.{u_4 + 1} (α := Set β) (⋃ (n : ℕ), t n) univ),
    MeasurableSet (α := α × β) (Prod.fst ⁻¹' s)
⊢ MeasurableSet (α := α × β) (Prod.fst ⁻¹' s)

Tactic:
rcases hD with ⟨t, h1t, h2t⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
s : Set α
hs : s ∈ C
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : Eq.{u_4 + 1} (α := Set β) (⋃ (n : ℕ), t n) univ
a : MeasurableSet (α := α × β) (⋃ (i : ℕ), s ×ˢ t i)
⊢ MeasurableSet (α := α × β) (Prod.fst ⁻¹' s)

Tactic:
rw [← prod_univ, ← h2t, prod_iUnion]

Premises used: Set.prod_univ, Set.prod_iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
s : Set α
hs : s ∈ C
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : Eq.{u_4 + 1} (α := Set β) (⋃ (n : ℕ), t n) univ
a : ∀ (b : ℕ), MeasurableSet (s ×ˢ t b)
⊢ MeasurableSet (α := α × β) (⋃ (i : ℕ), s ×ˢ t i)

Tactic:
apply MeasurableSet.iUnion

Premises used: MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
s : Set α
hs : s ∈ C
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : Eq.{u_4 + 1} (α := Set β) (⋃ (n : ℕ), t n) univ
n : ℕ
a : Membership.mem (γ := Set (Set (α × β))) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D) (s ×ˢ t n)
⊢ MeasurableSet (s ×ˢ t n)

Tactic:
apply measurableSet_generateFrom

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
s : Set α
hs : s ∈ C
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : Eq.{u_4 + 1} (α := Set β) (⋃ (n : ℕ), t n) univ
n : ℕ
⊢ Membership.mem (γ := Set (Set (α × β))) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D) (s ×ˢ t n)

Tactic:
⟨s, hs, t n, h1t n, rfl⟩

Premises used: Set.Mem, setOf, Set.image2, And.intro, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
s : Set α
hs : s ∈ C
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : Eq.{u_4 + 1} (α := Set β) (⋃ (n : ℕ), t n) univ
n : ℕ
⊢ Membership.mem (γ := Set (Set (α × β))) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D) (s ×ˢ t n)

Tactic:
exact ⟨s, hs, t n, h1t n, rfl⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
a :
  ∀ (t : ℕ → Set α) (h1t : ∀ (n : ℕ), t n ∈ C) (h2t : Eq.{u_3 + 1} (α := Set α) (⋃ (n : ℕ), t n) univ),
    MeasurableSet (α := α × β) (Prod.snd ⁻¹' s)
⊢ MeasurableSet (α := α × β) (Prod.snd ⁻¹' s)

Tactic:
rcases hC with ⟨t, h1t, h2t⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : Eq.{u_3 + 1} (α := Set α) (⋃ (n : ℕ), t n) univ
a : MeasurableSet (α := α × β) (⋃ (i : ℕ), t i ×ˢ s)
⊢ MeasurableSet (α := α × β) (Prod.snd ⁻¹' s)

Tactic:
rw [← univ_prod, ← h2t, iUnion_prod_const]

Premises used: Set.univ_prod, Set.iUnion_prod_const
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : Eq.{u_3 + 1} (α := Set α) (⋃ (n : ℕ), t n) univ
a : ∀ (b : ℕ), MeasurableSet (t b ×ˢ s)
⊢ MeasurableSet (α := α × β) (⋃ (i : ℕ), t i ×ˢ s)

Tactic:
apply MeasurableSet.iUnion

Premises used: MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : Eq.{u_3 + 1} (α := Set α) (⋃ (n : ℕ), t n) univ
n : ℕ
a : Membership.mem (γ := Set (Set (α × β))) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D) (t n ×ˢ s)
⊢ MeasurableSet (t n ×ˢ s)

Tactic:
apply measurableSet_generateFrom

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : Eq.{u_3 + 1} (α := Set α) (⋃ (n : ℕ), t n) univ
n : ℕ
⊢ Membership.mem (γ := Set (Set (α × β))) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D) (t n ×ˢ s)

Tactic:
mem_image2_of_mem (h1t n) hs

Premises used: Set.mem_image2_of_mem
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : Eq.{u_3 + 1} (α := Set α) (⋃ (n : ℕ), t n) univ
n : ℕ
⊢ Membership.mem (γ := Set (Set (α × β))) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D) (t n ×ˢ s)

Tactic:
exact mem_image2_of_mem (h1t n) hs

Premises used: Set.mem_image2_of_mem
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
a :
  ∀ (t : Set (α × β)),
    Membership.mem (γ := Set (Set (α × β))) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D) t → MeasurableSet t
⊢ LE.le (α := MeasurableSpace (α × β)) (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
    Prod.instMeasurableSpace

Tactic:
apply generateFrom_le

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
hs : s ∈ C
t : Set β
ht : t ∈ D
a : MeasurableSet (Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t)
⊢ MeasurableSet (s ×ˢ t)

Tactic:
rw [prod_eq]

Premises used: Set.prod_eq
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
hs : s ∈ C
t : Set β
ht : t ∈ D
apply : MeasurableSet s
apply₁ : MeasurableSet t
⊢ MeasurableSet (Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t)

Tactic:
apply (measurable_fst _).inter (measurable_snd _)

Premises used: measurable_snd, measurable_fst, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
hs : s ∈ C
t : Set β
ht : t ∈ D
⊢ MeasurableSet s

Tactic:
measurableSet_generateFrom hs

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
hs : s ∈ C
t : Set β
ht : t ∈ D
⊢ MeasurableSet s

Tactic:
exact measurableSet_generateFrom hs

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
hs : s ∈ C
t : Set β
ht : t ∈ D
⊢ MeasurableSet t

Tactic:
measurableSet_generateFrom ht

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
hs : s ∈ C
t : Set β
ht : t ∈ D
⊢ MeasurableSet t

Tactic:
exact measurableSet_generateFrom ht

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
C : Set (Set α)
D : Set (Set β)
hC : generateFrom C = inst
hD : generateFrom D = inst_1
h2C : IsCountablySpanning C
h2D : IsCountablySpanning D
rw :
  Eq (α := MeasurableSpace (α × β)) (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
    Prod.instMeasurableSpace
rw₁ :
  Eq (α := MeasurableSpace (α × β)) (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
    Prod.instMeasurableSpace
rw₂ rw₃ :
  Eq (α := MeasurableSpace (α × β)) (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
    (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
⊢ Eq (α := MeasurableSpace (α × β)) (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
    Prod.instMeasurableSpace

Tactic:
rw [← hC, ← hD, generateFrom_prod_eq h2C h2D]

Premises used: generateFrom_prod_eq
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
⊢ Eq (α := MeasurableSpace (α × β))
    (generateFrom
      (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t}))
    Prod.instMeasurableSpace

Tactic:
generateFrom_eq_prod generateFrom_measurableSet generateFrom_measurableSet
    isCountablySpanning_measurableSet isCountablySpanning_measurableSet

Premises used: isCountablySpanning_measurableSet, MeasurableSpace.generateFrom_measurableSet, generateFrom_eq_prod
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
⊢ IsPiSystem (α := α × β)
    (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})

Tactic:
isPiSystem_measurableSet.prod isPiSystem_measurableSet

Premises used: MeasurableSpace.isPiSystem_measurableSet, IsPiSystem.prod