awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Pi (goal)
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
x : (i : ι) → α i
i' : ι
pos :
  ∀ (h : i' = i),
    Membership.mem (γ := Set (α i'))
        (update (β := fun (i : ι) ↦ Set (α i)) (fun (i' : ι) ↦ iUnion (t i')) i (⋃ (x : ℕ), s : Set (α i)) i' :
          Set (α i'))
        (x i') ↔
      Membership.mem (γ := Set (α i'))
        (⋃ (j : ℕ), update (β := fun (i' : ι) ↦ Set (α i')) (fun (i' : ι) ↦ t i' j) i s i') (x i')
⊢ Membership.mem (γ := Set (α i'))
      (update (β := fun (i : ι) ↦ Set (α i)) (fun (i' : ι) ↦ iUnion (t i')) i (⋃ (x : ℕ), s : Set (α i)) i' :
        Set (α i'))
      (x i') ↔
    Membership.mem (γ := Set (α i')) (⋃ (j : ℕ), update (β := fun (i' : ι) ↦ Set (α i')) (fun (i' : ι) ↦ t i' j) i s i')
      (x i')
have neg : ∀ (h : ¬i' = i),
  Membership.mem (γ := Set (α i'))
      (update (β := fun (i : ι) ↦ Set (α i)) (fun (i' : ι) ↦ iUnion (t i')) i (⋃ (x : ℕ), s : Set (α i)) i' :
        Set (α i'))
      (x i') ↔
    Membership.mem (γ := Set (α i')) (⋃ (j : ℕ), update (β := fun (i' : ι) ↦ Set (α i')) (fun (i' : ι) ↦ t i' j) i s i')
      (x i')
Tactic: by_cases h : i' = i
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Pi (goal)
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
x : (i : ι) → α i
i' : ι
h : i' = i
⊢ Membership.mem (γ := Set (α i'))
      (update (β := fun (i : ι) ↦ Set (α i)) (fun (i' : ι) ↦ iUnion (t i')) i (⋃ (x : ℕ), s : Set (α i)) i' :
        Set (α i'))
      (x i') ↔
    Membership.mem (γ := Set (α i')) (⋃ (j : ℕ), update (β := fun (i' : ι) ↦ Set (α i')) (fun (i' : ι) ↦ t i' j) i s i')
      (x i')
have pos : ∀ (s : Set (α i')) (hs : s ∈ C i'),
  Membership.mem (γ := Set (α i'))
      (update (β := fun (i : ι) ↦ Set (α i)) (fun (i' : ι) ↦ iUnion (t i')) i' (⋃ (x : ℕ), s : Set (α i')) i' :
        Set (α i'))
      (x i') ↔
    Membership.mem (γ := Set (α i'))
      (⋃ (j : ℕ), update (β := fun (i' : ι) ↦ Set (α i')) (fun (i' : ι) ↦ t i' j) i' s i') (x i')
Tactic: subst h
Cleared hypotheses: i, s, hs, h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Pi (hypothesis)
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
⊢ MeasurableSet (α := (a : ι) → α a)
    (Set.pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (x : ι) ↦ ⋃ (n : ℕ), t x n) i (⋃ (x : ℕ), s)))
have 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)
Tactic: 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Pi (goal)
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)
⊢ MeasurableSet (α := (a : ι) → α a)
    (Set.pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (x : ι) ↦ ⋃ (n : ℕ), t x n) i (⋃ (x : ℕ), s)))
have intro : MeasurableSet (α := (a : ι) → α a)
  (⋃ (x : (a : ι) → ℕ),
    Set.pi (α := α) univ fun (a : ι) ↦ update (β := fun (i' : ι) ↦ Set (α i')) (fun (i' : ι) ↦ t i' (x a)) i s a)
Tactic: rw [this, ← iUnion_univ_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Pi (goal)
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)
⊢ MeasurableSet (α := (a : ι) → α a)
    (⋃ (x : (a : ι) → ℕ),
      Set.pi (α := α) univ fun (a : ι) ↦ update (β := fun (i' : ι) ↦ Set (α i')) (fun (i' : ι) ↦ t i' (x a)) i s a)
have intro : ∀ (b : (a : ι) → ℕ),
  MeasurableSet (α := (a : ι) → α a)
    (Set.pi (α := α) univ fun (a : ι) ↦ update (β := fun (i' : ι) ↦ Set (α i')) (fun (i' : ι) ↦ t i' (b a)) i s a)
Tactic: apply MeasurableSet.iUnion
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Pi (goal)
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 : ι) → ℕ
⊢ MeasurableSet (α := (a : ι) → α a)
    (Set.pi (α := α) univ fun (a : ι) ↦ update (β := fun (i' : ι) ↦ Set (α i')) (fun (i' : ι) ↦ t i' (n a)) i s a)
have 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
Tactic: apply measurableSet_generateFrom
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Pi (goal)
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 : ι) → ℕ
⊢ (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
have 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
Tactic: apply mem_image_of_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val : Encodable ι
⊢ generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C) ≤ MeasurableSpace.pi (X := α)
have intro : ∀ t ∈ Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C, MeasurableSet t
Tactic: apply generateFrom_le
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Pi (goal)
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
⊢ MeasurableSet (Set.pi (α := α) univ s)
have intro : MeasurableSet (α := (i : ι) → α i) (⋂ (i : ι), eval (β := α) i ⁻¹' s i)
Tactic: rw [univ_pi_eq_iInter]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Pi (goal)
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
⊢ MeasurableSet (α := (i : ι) → α i) (⋂ (i : ι), eval (β := α) i ⁻¹' s i)
have intro : ∀ (b : ι), MeasurableSet (eval (β := α) b ⁻¹' s b)
Tactic: apply MeasurableSet.iInter
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Pi (goal)
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 (eval (β := α) i ⁻¹' s i)
have intro : MeasurableSet (s i)
Tactic: apply @measurable_pi_apply _ _ (fun i => generateFrom (C i))
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
⊢ MeasurableSpace.pi (X := α) = generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
have intro : ∀ (val : Encodable ι),
  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))
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Pi (goal)
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)
⊢ MeasurableSpace.pi (X := α) = generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
have intro₁ : ∀ (val : Encodable ι),
  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))
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Pi (goal)
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)
⊢ MeasurableSpace.pi (X := α) = generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
have intro₂ : ∀ (val : Encodable ι),
  generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C) ≤ MeasurableSpace.pi (X := α)
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))
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ Eq (α := MeasurableSpace (α × β)) Prod.instMeasurableSpace
    (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
have a : LE.le (α := MeasurableSpace (α × β)) Prod.instMeasurableSpace
  (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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))
⊢ Eq (α := MeasurableSpace (α × β)) Prod.instMeasurableSpace
    (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
have a₁ : LE.le (α := MeasurableSpace (α × β)) (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
  Prod.instMeasurableSpace
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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))
have a : LE.le (α := MeasurableSpace (α × β)) (MeasurableSpace.comap Prod.fst (generateFrom C))
  (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
Tactic: refine sup_le ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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))
⊢ LE.le (α := MeasurableSpace (α × β)) Prod.instMeasurableSpace
    (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
have a₁ : LE.le (α := MeasurableSpace (α × β)) (MeasurableSpace.comap Prod.snd (generateFrom D))
  (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
Tactic: refine sup_le ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ LE.le (α := MeasurableSpace (α × β)) (MeasurableSpace.comap Prod.fst (generateFrom C))
    (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
have a : LE.le (α := MeasurableSpace (α × β)) (generateFrom (preimage Prod.fst '' C))
  (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
Tactic: rw [comap_generateFrom]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ LE.le (α := MeasurableSpace (α × β)) (MeasurableSpace.comap Prod.snd (generateFrom D))
    (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
have a : LE.le (α := MeasurableSpace (α × β)) (generateFrom (preimage Prod.snd '' D))
  (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
Tactic: rw [comap_generateFrom]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ LE.le (α := MeasurableSpace (α × β)) (generateFrom (preimage Prod.fst '' C))
    (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
have a : ∀ (t : Set (α × β)), Membership.mem (γ := Set (Set (α × β))) (preimage Prod.fst '' C) t → MeasurableSet t
Tactic: apply generateFrom_le
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ LE.le (α := MeasurableSpace (α × β)) (generateFrom (preimage Prod.snd '' D))
    (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
have a : ∀ (t : Set (α × β)), Membership.mem (γ := Set (Set (α × β))) (preimage Prod.snd '' D) t → MeasurableSet t
Tactic: apply generateFrom_le
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
hs : s ∈ C
⊢ MeasurableSet (α := α × β) (Prod.fst ⁻¹' s)
have a : ∀ (t : ℕ → Set β) (h1t : ∀ (n : ℕ), t n ∈ D) (h2t : Eq.{u_4 + 1} (α := Set β) (⋃ (n : ℕ), t n) univ),
  MeasurableSet (α := α × β) (Prod.fst ⁻¹' s)
Tactic: rcases hD with ⟨t, h1t, h2t⟩
Cleared hypotheses: hD
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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
⊢ MeasurableSet (α := α × β) (Prod.fst ⁻¹' s)
have a : MeasurableSet (α := α × β) (⋃ (i : ℕ), s ×ˢ t i)
Tactic: rw [← prod_univ, ← h2t, prod_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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
⊢ MeasurableSet (α := α × β) (⋃ (i : ℕ), s ×ˢ t i)
have a : ∀ (b : ℕ), MeasurableSet (s ×ˢ t b)
Tactic: apply MeasurableSet.iUnion
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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 : ℕ
⊢ MeasurableSet (s ×ˢ t n)
have a : Membership.mem (γ := Set (Set (α × β))) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D) (s ×ˢ t n)
Tactic: apply measurableSet_generateFrom
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
⊢ MeasurableSet (α := α × β) (Prod.snd ⁻¹' s)
have a : ∀ (t : ℕ → Set α) (h1t : ∀ (n : ℕ), t n ∈ C) (h2t : Eq.{u_3 + 1} (α := Set α) (⋃ (n : ℕ), t n) univ),
  MeasurableSet (α := α × β) (Prod.snd ⁻¹' s)
Tactic: rcases hC with ⟨t, h1t, h2t⟩
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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
⊢ MeasurableSet (α := α × β) (Prod.snd ⁻¹' s)
have a : MeasurableSet (α := α × β) (⋃ (i : ℕ), t i ×ˢ s)
Tactic: rw [← univ_prod, ← h2t, iUnion_prod_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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
⊢ MeasurableSet (α := α × β) (⋃ (i : ℕ), t i ×ˢ s)
have a : ∀ (b : ℕ), MeasurableSet (t b ×ˢ s)
Tactic: apply MeasurableSet.iUnion
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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 : ℕ
⊢ MeasurableSet (t n ×ˢ s)
have a : Membership.mem (γ := Set (Set (α × β))) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D) (t n ×ˢ s)
Tactic: apply measurableSet_generateFrom
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
Goal:
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ LE.le (α := MeasurableSpace (α × β)) (generateFrom (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D))
    Prod.instMeasurableSpace
have a : ∀ (t : Set (α × β)),
  Membership.mem (γ := Set (Set (α × β))) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D) t → MeasurableSet t
Tactic: apply generateFrom_le
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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 ×ˢ t)
have a : MeasurableSet (Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t)
Tactic: rw [prod_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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 (Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t)
have apply : MeasurableSet s
Tactic: apply (measurable_fst _).inter (measurable_snd _)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Prod (goal)
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
⊢ MeasurableSet (Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t)
have apply₁ : MeasurableSet t
Tactic: apply (measurable_fst _).inter (measurable_snd _)