awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : (↑t : Type uι) → Set α
hVf : ∀ (i : (↑t : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
U : (i : (↑t : Type uι)) → Set α
hUf : ∀ (i : (↑t : Type uι)), U i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
hU : ∀ (i : (↑t : Type uι)), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), f i) (⋂ (i : (↑t : Type uι)), U i)
have refine_1 : ∃ (I : Set (PLift ι)),
  I.Finite ∧
    ∃ (V : (↑I : Type uι) → Set α),
      (∀ (i : (↑I : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))) ∧
        Eq.{u_1 + 1} (α := Set α) (⋂ (i : (↑t : Type uι)), U i) (⋂ (i : (↑I : Type uι)), V i)
Tactic: rw [← Equiv.plift.surjective.iInf_comp, mem_iInf]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst : MeasurableSpace α
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : (↑t : Type uι) → Set α
hVf : ∀ (i : (↑t : Type uι)), V i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
U : (i : (↑t : Type uι)) → Set α
hUf : ∀ (i : (↑t : Type uι)), U i ∈ f ((Equiv.plift : (a : PLift ι) → ι) (↑i : PLift ι))
hU : ∀ (i : (↑t : Type uι)), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ MeasurableSet.{u_1} (α := α) (⋂ (i : (↑t : Type uι)), U i)
have this : Countable.{uι + 1} (↑t : Type uι)
Tactic: haveI := ht.countable.toEncodable.countable
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
x : MeasurableSpace β
inst : MeasurableSpace γ
inst_1 : Countable δ
l : Filter δ
inst_2 : l.IsCountablyGenerated
l' : Filter γ
inst_3 : l'.IsCountablyGenerated
hl' : l'.IsMeasurablyGenerated
f : δ → β → γ
hf : ∀ (i : δ), Measurable (f i)
⊢ MeasurableSet.{u_2} (α := β) {x : β | Tendsto (fun (n : δ) ↦ f n x) l l'}
have rcases : ∀ (u : ℕ → Set δ) (hu : l.HasAntitoneBasis u), MeasurableSet.{u_2} (α := β) {x : β | Tendsto (fun (n : δ) ↦ f n x) l l'}
Tactic: rcases l.exists_antitone_basis with ⟨u, hu⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
x : MeasurableSpace β
inst : MeasurableSpace γ
inst_1 : Countable δ
l : Filter δ
inst_2 : l.IsCountablyGenerated
l' : Filter γ
inst_3 : l'.IsCountablyGenerated
hl' : l'.IsMeasurablyGenerated
f : δ → β → γ
hf : ∀ (i : δ), Measurable (f i)
u : ℕ → Set δ
hu : l.HasAntitoneBasis u
⊢ MeasurableSet.{u_2} (α := β) {x : β | Tendsto (fun (n : δ) ↦ f n x) l l'}
have rcases : ∀ (v : ℕ → Set γ) (v_meas : ∀ (i : ℕ), v i ∈ l' ∧ MeasurableSet (v i))
  (hv : l'.HasAntitoneBasis fun (i : ℕ) ↦ id (v i)),
  MeasurableSet.{u_2} (α := β) {x : β | Tendsto (fun (n : δ) ↦ f n x) l l'}
Tactic: rcases (Filter.hasBasis_self.mpr hl'.exists_measurable_subset).exists_antitone_subbasis with
    ⟨v, v_meas, hv⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
x : MeasurableSpace β
inst : MeasurableSpace γ
inst_1 : Countable δ
l : Filter δ
inst_2 : l.IsCountablyGenerated
l' : Filter γ
inst_3 : l'.IsCountablyGenerated
hl' : l'.IsMeasurablyGenerated
f : δ → β → γ
hf : ∀ (i : δ), Measurable (f i)
u : ℕ → Set δ
hu : l.HasAntitoneBasis u
v : ℕ → Set γ
v_meas : ∀ (i : ℕ), v i ∈ l' ∧ MeasurableSet (v i)
hv : l'.HasAntitoneBasis fun (i : ℕ) ↦ id (v i)
⊢ MeasurableSet.{u_2} (α := β) {x : β | Tendsto (fun (n : δ) ↦ f n x) l l'}
have simp : MeasurableSet.{u_2} (α := β) (⋂ (i : ℕ), ⋃ (i_1 : ℕ), ⋂ i_2 ∈ u i_1, {x : β | f i_2 x ∈ id (v i)})
Tactic: simp only [hu.tendsto_iff hv.toHasBasis, true_imp_iff, true_and, setOf_forall, setOf_exists]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hsm : Monotone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ι), s i)
have rcases : ∀ (x : ℕ → ι) (hx : Tendsto x atTop atTop) (hxm : ∀ (n : ℕ), MeasurableSet (s (x n))),
  MeasurableSet.{u_1} (α := α) (⋃ (i : ι), s i)
Tactic: rcases exists_seq_forall_of_frequently hs with ⟨x, hx, hxm⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hsm : Monotone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
x : ℕ → ι
hx : Tendsto x atTop atTop
hxm : ∀ (n : ℕ), MeasurableSet (s (x n))
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ι), s i)
have rw : MeasurableSet.{u_1} (α := α) (⋃ (a : ℕ), s (x a))
Tactic: rw [← hsm.iUnion_comp_tendsto_atTop hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hsm : Antitone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
⊢ MeasurableSet.{u_1} (α := α) (⋂ (i : ι), s i)
have rw : MeasurableSet.{u_1} (α := α) (⋃ (i : ι), (s i)ᶜ)
Tactic: rw [← compl_iff, compl_iInter]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hsm : Monotone s
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ι), s i)
have x : IsEmpty ι ∨ Nonempty ι
Tactic: cases isEmpty_or_nonempty ι with
  | inl _ => simp
  | inr _ => exact .iUnion_of_monotone_of_frequently hsm <| .of_forall hs
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set α
hsm : Antitone s
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ MeasurableSet.{u_1} (α := α) (⋂ (i : ι), s i)
have rw : MeasurableSet.{u_1} (α := α) (⋃ (i : ι), (s i)ᶜ)
Tactic: rw [← compl_iff, compl_iInter]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (blimsup s atTop p)
have simp : MeasurableSet.{u_1} (α := α) (⋂ (i : ℕ), ⋃ (j : ℕ), ⋃ (_ : p j ∧ i ≤ j), s j)
Tactic: simp only [blimsup_eq_iInf_biSup_of_nat, iSup_eq_iUnion, iInf_eq_iInter]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (bliminf s atTop p)
have simp : MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), ⋂ (j : ℕ), ⋂ (_ : p j ∧ i ≤ j), s j)
Tactic: simp only [Filter.bliminf_eq_iSup_biInf_of_nat, iInf_eq_iInter, iSup_eq_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
s₁ : (i : ι) → Set (α i)
hs₁ : s₁ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
s₂ : (i : ι) → Set (α i)
hs₂ : s₂ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
hst : (Set.pi (α := α) univ s₁ ∩ Set.pi (α := α) univ s₂).Nonempty
⊢ Set.pi (α := α) univ s₁ ∩ Set.pi (α := α) univ s₂ ∈
    Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
have rw : ∀ (hst : Set.Nonempty (α := (i : ι) → α i) (Set.pi (α := α) univ fun (i : ι) ↦ s₁ i ∩ s₂ i)),
  (Set.pi (α := α) univ fun (i : ι) ↦ s₁ i ∩ s₂ i) ∈
    Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
Tactic: rw [← pi_inter_distrib] at hst ⊢
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Pi (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
s₁ : (i : ι) → Set (α i)
hs₁ : s₁ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
s₂ : (i : ι) → Set (α i)
hs₂ : s₂ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
hst : Set.Nonempty (α := (i : ι) → α i) (Set.pi (α := α) univ fun (i : ι) ↦ s₁ i ∩ s₂ i)
⊢ (Set.pi (α := α) univ fun (i : ι) ↦ s₁ i ∩ s₂ i) ∈
    Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
have hst₁ : ∀ (i : ι), (s₁ i ∩ s₂ i).Nonempty
Tactic: rw [univ_pi_nonempty_iff] at hst
Cleared hypotheses: hst
-- 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)
⊢ IsCountablySpanning (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
have choose : ∀ (s : (i : ι) → ℕ → Set (α i)) (h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i)
  (h2s : ∀ (i : ι), Eq.{u_2 + 1} (α := Set (α i)) (⋃ (n : ℕ), s i n) univ),
  IsCountablySpanning (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
Tactic: choose s h1s h2s using hC
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), Eq.{u_2 + 1} (α := Set (α i)) (⋃ (n : ℕ), s i n) univ
⊢ IsCountablySpanning (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
have intro : ∀ (val : Encodable (ι → ℕ)), IsCountablySpanning (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
Tactic: cases nonempty_encodable (ι → ℕ)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), Eq.{u_2 + 1} (α := Set (α i)) (⋃ (n : ℕ), s i n) univ
val : Encodable (ι → ℕ)
e : ℕ → ι → ℕ := fun (n : ℕ) ↦ Option.getD (decode n) default
⊢ IsCountablySpanning (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
have intro : Eq (α := Set ((i : ι) → α i))
  (⋃ (n : ℕ), (fun (n : ℕ) ↦ (Set.pi (α := α) univ fun (i : ι) ↦ s i (e n i) : Set ((i : ι) → α i))) n) univ
Tactic: refine ⟨fun n => Set.pi univ fun i => s i (e n i), fun n =>
    mem_image_of_mem _ fun i _ => h1s 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))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), Eq.{u_2 + 1} (α := Set (α i)) (⋃ (n : ℕ), s i n) univ
val : Encodable (ι → ℕ)
e : ℕ → ι → ℕ := fun (n : ℕ) ↦ Option.getD (decode n) default
intro intro₁ : Eq (α := Set ((i : ι) → α i)) (⋃ (n : ℕ), Set.pi (α := α) univ fun (i : ι) ↦ s i (e n i)) univ
intro₂ :
  Eq (α := Set ((i : ι) → α i)) (⋃ (n : ℕ), Set.pi (α := α) univ fun (i : ι) ↦ s i (Option.getD (decode n) default i))
    univ
⊢ Eq (α := Set ((i : ι) → α i))
    (⋃ (n : ℕ), (fun (n : ℕ) ↦ (Set.pi (α := α) univ fun (i : ι) ↦ s i (e n i) : Set ((i : ι) → α i))) n) univ
have intro₃ : Eq (α := Set ((i : ι) → α i)) (⋃ (y : ι → ℕ), Set.pi (α := α) univ fun (i : ι) ↦ s i (y i)) univ
Tactic: simp_rw [e,
    (surjective_decode_getD (ι → ℕ) default).iUnion_comp fun x => Set.pi univ fun i => s i (x i),
    iUnion_univ_pi s, h2s, pi_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), Eq.{u_2 + 1} (α := Set (α i)) (⋃ (n : ℕ), s i n) univ
val : Encodable (ι → ℕ)
e : ℕ → ι → ℕ := fun (n : ℕ) ↦ Option.getD (decode n) default
intro intro₁ : Eq (α := Set ((i : ι) → α i)) (⋃ (n : ℕ), Set.pi (α := α) univ fun (i : ι) ↦ s i (e n i)) univ
intro₂ :
  Eq (α := Set ((i : ι) → α i)) (⋃ (n : ℕ), Set.pi (α := α) univ fun (i : ι) ↦ s i (Option.getD (decode n) default i))
    univ
intro₃ : Eq (α := Set ((i : ι) → α i)) (⋃ (y : ι → ℕ), Set.pi (α := α) univ fun (i : ι) ↦ s i (y i)) univ
⊢ Eq (α := Set ((i : ι) → α i))
    (⋃ (n : ℕ), (fun (n : ℕ) ↦ (Set.pi (α := α) univ fun (i : ι) ↦ s i (e n i) : Set ((i : ι) → α i))) n) univ
have intro₄ : Eq (α := Set ((i : ι) → α i)) (Set.pi (α := α) univ fun (a : ι) ↦ ⋃ (j : ℕ), s a j) univ
Tactic: simp_rw [e,
    (surjective_decode_getD (ι → ℕ) default).iUnion_comp fun x => Set.pi univ fun i => s i (x i),
    iUnion_univ_pi s, h2s, pi_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), Eq.{u_2 + 1} (α := Set (α i)) (⋃ (n : ℕ), s i n) univ
val : Encodable (ι → ℕ)
e : ℕ → ι → ℕ := fun (n : ℕ) ↦ Option.getD (decode n) default
intro intro₁ : Eq (α := Set ((i : ι) → α i)) (⋃ (n : ℕ), Set.pi (α := α) univ fun (i : ι) ↦ s i (e n i)) univ
intro₂ :
  Eq (α := Set ((i : ι) → α i)) (⋃ (n : ℕ), Set.pi (α := α) univ fun (i : ι) ↦ s i (Option.getD (decode n) default i))
    univ
intro₃ : Eq (α := Set ((i : ι) → α i)) (⋃ (y : ι → ℕ), Set.pi (α := α) univ fun (i : ι) ↦ s i (y i)) univ
intro₄ : Eq (α := Set ((i : ι) → α i)) (Set.pi (α := α) univ fun (a : ι) ↦ ⋃ (j : ℕ), s a j) univ
⊢ Eq (α := Set ((i : ι) → α i))
    (⋃ (n : ℕ), (fun (n : ℕ) ↦ (Set.pi (α := α) univ fun (i : ι) ↦ s i (e n i) : Set ((i : ι) → α i))) n) univ
have intro₅ : Eq (α := Set ((i : ι) → α i)) (Set.pi (α := α) univ fun (a : ι) ↦ univ) univ
Tactic: simp_rw [e,
    (surjective_decode_getD (ι → ℕ) default).iUnion_comp fun x => Set.pi univ fun i => s i (x i),
    iUnion_univ_pi s, h2s, pi_univ]
-- 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: cases nonempty_encodable ι
-- 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 ι
⊢ MeasurableSpace.pi (X := α) = generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
have intro : MeasurableSpace.pi (X := α) ≤ generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
Tactic: apply le_antisymm
-- 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 ι
intro :
  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₁ : generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C) ≤ MeasurableSpace.pi (X := α)
Tactic: apply le_antisymm
-- 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 ι
⊢ MeasurableSpace.pi (X := α) ≤ generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
have intro : ∀ (i : ι),
  MeasurableSpace.comap (β := α i) (fun (b : (a : ι) → α a) ↦ b i) ((fun (i : ι) ↦ generateFrom (C i)) i) ≤
    generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
Tactic: refine iSup_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 ι
i : ι
⊢ MeasurableSpace.comap (β := α i) (fun (b : (a : ι) → α a) ↦ b i) ((fun (i : ι) ↦ generateFrom (C i)) i) ≤
    generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
have intro : generateFrom ((preimage fun (b : (a : ι) → α a) ↦ b i) '' C i) ≤
  generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
Tactic: rw [comap_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))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val : Encodable ι
i : ι
⊢ generateFrom ((preimage fun (b : (a : ι) → α a) ↦ b i) '' C i) ≤
    generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
have intro : ∀ (t : Set ((a : ι) → α a)),
  Membership.mem (γ := Set (Set ((a : ι) → α a))) ((preimage fun (b : (a : ι) → α a) ↦ b i) '' C i) t → 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 ι
i : ι
s : Set (α i)
hs : s ∈ C i
⊢ MeasurableSet (α := (a : ι) → α a) ((fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)
have intro : ∀ (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) ((fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)
Tactic: choose t h1t h2t using hC
Cleared hypotheses: hC
-- 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
⊢ MeasurableSet (α := (a : ι) → α a) ((fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)
have intro : MeasurableSet (α := (a : ι) → α a)
  (Set.pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (x : ι) ↦ ⋃ (n : ℕ), t x n) i s))
Tactic: simp_rw [eval_preimage, ← h2t]
-- 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
⊢ MeasurableSet (α := (a : ι) → α a)
    (Set.pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (x : ι) ↦ ⋃ (n : ℕ), t x n) i s))
have intro : MeasurableSet (α := (a : ι) → α a)
  (Set.pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (x : ι) ↦ ⋃ (n : ℕ), t x n) i (⋃ (x : ℕ), s)))
Tactic: rw [← @iUnion_const _ ℕ _ s]
-- 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
⊢ 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)
have h : ∀ (x : (i : ι) → α i),
  Membership.mem (γ := Set ((i : ι) → α i))
      (Set.pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (i' : ι) ↦ iUnion (t i')) i (⋃ (x : ℕ), s))) x ↔
    Membership.mem (γ := Set ((i : ι) → α i))
      (Set.pi (α := α) univ fun (k : ι) ↦
        ⋃ (j : ℕ), update (β := fun (i' : ι) ↦ Set (α i')) (fun (i' : ι) ↦ t i' j) i s k)
      x
Tactic: ext
-- 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
⊢ Membership.mem (γ := Set ((i : ι) → α i))
      (Set.pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (i' : ι) ↦ iUnion (t i')) i (⋃ (x : ℕ), s))) x ↔
    Membership.mem (γ := Set ((i : ι) → α i))
      (Set.pi (α := α) univ fun (k : ι) ↦
        ⋃ (j : ℕ), update (β := fun (i' : ι) ↦ Set (α i')) (fun (i' : ι) ↦ t i' j) i s k)
      x
have h : (∀ (i_1 : ι),
    Membership.mem (γ := Set (α i_1))
      (update (β := fun (i : ι) ↦ Set (α i)) (fun (i' : ι) ↦ iUnion (t i')) i (⋃ (x : ℕ), s : Set (α i)) i_1 :
        Set (α i_1))
      (x i_1)) ↔
  ∀ (i_1 : ι),
    Membership.mem (γ := Set (α i_1))
      (⋃ (j : ℕ), update (β := fun (i' : ι) ↦ Set (α i')) (fun (i' : ι) ↦ t i' j) i s i_1) (x i_1)
Tactic: simp_rw [mem_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
x : (i : ι) → α i
⊢ (∀ (i_1 : ι),
      Membership.mem (γ := Set (α i_1))
        (update (β := fun (i : ι) ↦ Set (α i)) (fun (i' : ι) ↦ iUnion (t i')) i (⋃ (x : ℕ), s : Set (α i)) i_1 :
          Set (α i_1))
        (x i_1)) ↔
    ∀ (i_1 : ι),
      Membership.mem (γ := Set (α i_1))
        (⋃ (j : ℕ), update (β := fun (i' : ι) ↦ Set (α i')) (fun (i' : ι) ↦ t i' j) i s i_1) (x i_1)
have h : ∀ (a : ι),
  Membership.mem (γ := Set (α a))
      (update (β := fun (i : ι) ↦ Set (α i)) (fun (i' : ι) ↦ iUnion (t i')) i (⋃ (x : ℕ), s : Set (α i)) a : Set (α a))
      (x a) ↔
    Membership.mem (γ := Set (α a)) (⋃ (j : ℕ), update (β := fun (i' : ι) ↦ Set (α i')) (fun (i' : ι) ↦ t i' j) i s a)
      (x a)
Tactic: apply forall_congr'
-- 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' : ι
⊢ 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 : ∀ (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