-- Mathlib/MeasureTheory/MeasurableSpace/Pi.lean
theorem generateFrom_pi_eq {C : ∀ i, Set (Set (α i))} (hC : ∀ i, IsCountablySpanning (C i)) :
    (@MeasurableSpace.pi _ _ fun i => generateFrom (C i)) =
    generateFrom (pi univ '' pi univ C)

Proof state:
case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ generateFrom (univ.pi '' univ.pi C) ≤ MeasurableSpace.pi

Tactic:
apply generateFrom_le

Result:
case intro.a.h
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ ∀ t ∈ univ.pi '' univ.pi C, MeasurableSet t

Proof state:
case intro.a.h.intro.intro
ι : 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 : ι), ⋃ n, t i n = univ
⊢ MeasurableSet (univ.pi (update (fun x => ⋃ n, t x n) i s))

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

Result:
case intro.a.h.intro.intro
ι : 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 : ι), ⋃ n, t i n = univ
⊢ MeasurableSet (univ.pi (update (fun x => ⋃ n, t x n) i (⋃ x, s)))

Proof state:
case neg
ι : 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 : ι), ⋃ n, t i n = univ
this : univ.pi (update (fun i' => iUnion (t i')) i (⋃ x, s)) = univ.pi fun k => ⋃ j, update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
h : ¬j = i
⊢ t j (n j) ∈ C j

Tactic:
apply h1t

Result:
no goals

Proof state:
case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
⊢ MeasurableSpace.comap (fun b => b i) ((fun i => generateFrom (C i)) i) ≤ generateFrom (univ.pi '' univ.pi C)

Tactic:
rw [comap_generateFrom]

Result:
case intro.a
ι : 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 => b i) '' C i) ≤ generateFrom (univ.pi '' univ.pi C)

Proof state:
case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ ∀ (i : ι),
    MeasurableSpace.comap (fun b => b i) ((fun i => generateFrom (C i)) i) ≤ generateFrom (univ.pi '' univ.pi C)

Tactic:
intro i

Result:
case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
⊢ MeasurableSpace.comap (fun b => b i) ((fun i => generateFrom (C i)) i) ≤ generateFrom (univ.pi '' univ.pi C)

Proof state:
case pos
ι : 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 : ι), ⋃ n, t i n = univ
this : univ.pi (update (fun i' => iUnion (t i')) i (⋃ x, s)) = univ.pi fun k => ⋃ j, update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
h : j = i
⊢ update (fun i' => t i' (n j)) i s j ∈ C j

Tactic:
subst h

Result:
case pos
ι : 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 : ι), ⋃ n, t i n = univ
n : ι → ℕ
j : ι
a✝ : j ∈ univ
s : Set (α j)
hs : s ∈ C j
this : univ.pi (update (fun i' => iUnion (t i')) j (⋃ x, s)) = univ.pi fun k => ⋃ j_1, update (fun i' => t i' j_1) j s k
⊢ update (fun i' => t i' (n j)) j s j ∈ C j

Proof state:
case intro.a.h.intro.intro
ι : 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 ((fun b => b i) ⁻¹' s)

Tactic:
choose t h1t h2t using hC

Result:
case intro.a.h.intro.intro
ι : 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 : ι), ⋃ n, t i n = univ
⊢ MeasurableSet ((fun b => b i) ⁻¹' s)

Proof state:
case h
ι : 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 : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
⊢ x✝ ∈ univ.pi (update (fun i' => iUnion (t i')) i (⋃ x, s)) ↔
    x✝ ∈ univ.pi fun k => ⋃ j, update (fun i' => t i' j) i s k

Tactic:
simp_rw [mem_univ_pi]

Result:
case h
ι : 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 : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
⊢ (∀ (i_1 : ι), x✝ i_1 ∈ update (fun i' => iUnion (t i')) i (⋃ x, s) i_1) ↔
    ∀ (i_1 : ι), x✝ i_1 ∈ ⋃ j, update (fun i' => t i' j) i s i_1

Proof state:
case intro.a.h.intro.intro.h.ht.h
ι : 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 : ι), ⋃ n, t i n = univ
this : univ.pi (update (fun i' => iUnion (t i')) i (⋃ x, s)) = univ.pi fun k => ⋃ j, update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
⊢ (fun a => update (fun i' => t i' (n a)) i s a) j ∈ C j

Tactic:
dsimp only

Result:
case intro.a.h.intro.intro.h.ht.h
ι : 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 : ι), ⋃ n, t i n = univ
this : univ.pi (update (fun i' => iUnion (t i')) i (⋃ x, s)) = univ.pi fun k => ⋃ j, update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
⊢ update (fun i' => t i' (n j)) i s j ∈ C j

Proof state:
case intro.a.h
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ ∀ t ∈ univ.pi '' univ.pi C, MeasurableSet t

Tactic:
rintro _ ⟨s, hs, rfl⟩

Result:
case intro.a.h.intro.intro
ι : 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 ∈ univ.pi C
⊢ MeasurableSet (univ.pi s)

Proof state:
case intro.a.h
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
⊢ ∀ t ∈ (preimage fun b => b i) '' C i, MeasurableSet t

Tactic:
rintro _ ⟨s, hs, rfl⟩

Result:
case intro.a.h.intro.intro
ι : 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 ((fun b => b i) ⁻¹' s)