awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
⊢ MeasurableSet (limsup s atTop)

Tactic:
simpa only [← blimsup_true] using measurableSet_blimsup fun n _ => hs n

Premises used: Filter.blimsup_true, MeasurableSet.measurableSet_blimsup
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
inst : MeasurableSpace α
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
⊢ MeasurableSet (liminf s atTop)

Tactic:
simpa only [← bliminf_true] using measurableSet_bliminf fun n _ => hs n

Premises used: Filter.bliminf_true, MeasurableSet.measurableSet_bliminf
-- Module: Mathlib.MeasureTheory.MeasurableSpace.NCard
Goal:
α : Type u_1
inst : Countable α
⊢ Measurable.{u_1, 0} (α := Set α) encard

Tactic:
ENat.measurable_iff.2 fun _n ↦ Countable.measurableSet <| Countable.setOf_finite.mono fun _s hs ↦
    finite_of_encard_eq_coe hs

Premises used: Iff.mpr, ENat.measurable_iff, Set.Countable.measurableSet, Set.Countable.setOf_finite, Set.finite_of_encard_eq_coe, Set.Countable.mono
-- Module: Mathlib.MeasureTheory.MeasurableSpace.NCard
Goal:
α : Type u_1
inst : Countable α
⊢ Measurable.{u_1, 0} (α := Set α) ncard

Tactic:
Measurable.of_discrete.comp measurable_encard

Premises used: Measurable.comp, Measurable.of_discrete, measurable_encard, ENat.toNat, WithTop.untopD, Set.ncard, WithTop.recTopCoe
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
⊢ Eq (α := MeasurableSpace ((a : ι) → α a)) (pi (X := α))
    (generateFrom {B : Set ((x : ι) → α x) | ∃ (i : ι) (A : Set (α i)), MeasurableSet A ∧ eval (β := α) i ⁻¹' A = B})

Tactic:
simp only [pi, ← generateFrom_iUnion_measurableSet, iUnion_setOf, measurableSet_comap]

Premises used: MeasurableSpace.generateFrom_iUnion_measurableSet, MeasurableSpace.measurableSet_comap, MeasurableSpace.pi, Set.iUnion_setOf
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
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
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
⊢ Set.pi (α := α) univ s₁ ∩ Set.pi (α := α) univ s₂ ∈
    Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C

Tactic:
rw [← pi_inter_distrib] at hst ⊢

Premises used: Set.pi_inter_distrib
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
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)
⊢ ∀ (i : ι), (s₁ i ∩ s₂ i).Nonempty

Tactic:
rw [univ_pi_nonempty_iff] at hst

Premises used: Set.univ_pi_nonempty_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
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 : ∀ (i : ι), (s₁ i ∩ s₂ i).Nonempty
⊢ (Set.pi (α := α) univ fun (i : ι) ↦ s₁ i ∩ s₂ i) ∈
    Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C

Tactic:
mem_image_of_mem _ fun i _ => hC i _ (hs₁ i (mem_univ i)) _ (hs₂ i (mem_univ i)) (hst i)

Premises used: Set.Mem, Set.mem_image_of_mem, Set.mem_univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
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 : ∀ (i : ι), (s₁ i ∩ s₂ i).Nonempty
⊢ (Set.pi (α := α) univ fun (i : ι) ↦ s₁ i ∩ s₂ i) ∈
    Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C

Tactic:
exact mem_image_of_mem _ fun i _ => hC i _ (hs₁ i (mem_univ i)) _ (hs₂ i (mem_univ i)) (hst i)
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
⊢ IsPiSystem (α := (i : ι) → α i)
    (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s})

Tactic:
IsPiSystem.pi fun _ => isPiSystem_measurableSet

Premises used: MeasurableSpace.isPiSystem_measurableSet, IsPiSystem.pi
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
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)
⊢ IsCountablySpanning (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)

Tactic:
choose s h1s h2s using hC
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
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
intro :
  ∀ (val : Encodable (ι → ℕ)),
    IsCountablySpanning (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
⊢ IsCountablySpanning (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)

Tactic:
cases nonempty_encodable (ι → ℕ)

Premises used: nonempty_encodable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
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)

Tactic:
⟨fun n => Set.pi univ fun i => s i (e n i), fun n =>
    mem_image_of_mem _ fun i _ => h1s i _, ?_⟩

Premises used: Set.univ, Set.mem_image_of_mem, And.intro, Exists.intro, Set.pi, IsCountablySpanning
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
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 :
  Eq (α := Set ((i : ι) → α i))
    (⋃ (n : ℕ), (fun (n : ℕ) ↦ (Set.pi (α := α) univ fun (i : ι) ↦ s i (e n i) : Set ((i : ι) → α i))) n) univ
⊢ IsCountablySpanning (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)

Tactic:
refine ⟨fun n => Set.pi univ fun i => s i (e n i), fun n =>
    mem_image_of_mem _ fun i _ => h1s i _, ?_⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
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
intro₅ : Eq (α := Set ((i : ι) → α i)) (Set.pi (α := α) univ fun (a : ι) ↦ univ) univ
⊢ Eq (α := Set ((i : ι) → α i))
    (⋃ (n : ℕ), (fun (n : ℕ) ↦ (Set.pi (α := α) univ fun (i : ι) ↦ s i (e n i) : Set ((i : ι) → α i))) n) 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]

Premises used: Inhabited.default, Set.univ, Function.Surjective.iUnion_comp, Set.pi, Set.iUnion_univ_pi, Set.pi_univ, Encodable.surjective_decode_getD
-- 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)
⊢ MeasurableSpace.pi (X := α) = generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)

Tactic:
cases nonempty_encodable ι

Premises used: nonempty_encodable
-- 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 :
  MeasurableSpace.pi (X := α) ≤ generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
intro₁ :
  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:
apply le_antisymm

Premises used: le_antisymm
-- 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 ι
⊢ MeasurableSpace.pi (X := α) ≤ generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)

Tactic:
iSup_le ?_

Premises used: iSup_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 ι
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)
⊢ MeasurableSpace.pi (X := α) ≤ generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)

Tactic:
refine iSup_le ?_

Premises used: iSup_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 ι
i : ι
intro :
  generateFrom ((preimage fun (b : (a : ι) → α a) ↦ b i) '' C i) ≤
    generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
⊢ 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:
rw [comap_generateFrom]

Premises used: MeasurableSpace.comap_generateFrom
-- 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 ι
i : ι
intro :
  ∀ (t : Set ((a : ι) → α a)),
    Membership.mem (γ := Set (Set ((a : ι) → α a))) ((preimage fun (b : (a : ι) → α a) ↦ b i) '' C i) t →
      MeasurableSet t
⊢ generateFrom ((preimage fun (b : (a : ι) → α a) ↦ b i) '' C i) ≤
    generateFrom (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)

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 ι
i : ι
s : Set (α i)
hs : s ∈ C i
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)
⊢ MeasurableSet (α := (a : ι) → α a) ((fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)

Tactic:
choose t h1t h2t using hC
-- 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
intro :
  MeasurableSet (α := (a : ι) → α a)
    (Set.pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (x : ι) ↦ ⋃ (n : ℕ), t x n) i s))
⊢ MeasurableSet (α := (a : ι) → α a) ((fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)

Tactic:
simp_rw [eval_preimage, ← h2t]

Premises used: Set.eval_preimage
-- 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
intro :
  MeasurableSet (α := (a : ι) → α a)
    (Set.pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (x : ι) ↦ ⋃ (n : ℕ), t x n) i (⋃ (x : ℕ), s)))
⊢ MeasurableSet (α := (a : ι) → α a)
    (Set.pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (x : ι) ↦ ⋃ (n : ℕ), t x n) i s))

Tactic:
rw [← @iUnion_const _ ℕ _ s]

Premises used: Set.iUnion_const
-- 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
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
⊢ 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:
ext
-- 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
x : (i : ι) → α i
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)
⊢ 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:
simp_rw [mem_univ_pi]

Premises used: Set.mem_univ_pi
-- 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
x : (i : ι) → α i
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)
⊢ (∀ (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:
apply forall_congr'

Premises used: forall_congr'
-- 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
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')
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')
⊢ 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
-- 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
x : (i : ι) → α i
i' : ι
h : i' = i
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')
⊢ 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
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
C : (i : ι) → Set (Set (α i))
val : Encodable ι
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' : ι
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:
simp
-- 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
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')

Tactic:
simp [h]
-- 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
⊢ 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]
-- 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)
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)
⊢ MeasurableSet (α := (a : ι) → α a)
    (Set.pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (x : ι) ↦ ⋃ (n : ℕ), t x n) i (⋃ (x : ℕ), s)))

Tactic:
rw [this, ← iUnion_univ_pi]

Premises used: Set.iUnion_univ_pi
-- 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)
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)
⊢ 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:
apply MeasurableSet.iUnion

Premises used: MeasurableSet.iUnion