-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem comap_eval_le_generateFrom_squareCylinders_singleton
    (α : ι → Type*) [m : ∀ i, MeasurableSpace (α i)] (i : ι) :
    MeasurableSpace.comap (Function.eval i) (m i) ≤
      MeasurableSpace.generateFrom
        ((fun t ↦ ({i} : Set ι).pi t) '' univ.pi fun i ↦ {s : Set (α i) | MeasurableSet s})

Proof state:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ MeasurableSpace.comap (eval i) (m i) ≤
    MeasurableSpace.generateFrom ((fun t => {i}.pi t) '' univ.pi fun i => {s | MeasurableSet s})

Tactic:
simp only [Function.eval, singleton_pi]

Result:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ MeasurableSpace.comap (eval i) (m i) ≤
    MeasurableSpace.generateFrom ((fun a => eval i ⁻¹' a i) '' univ.pi fun i => {s | MeasurableSet s})

Proof state:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
⊢ ∀ (x : Set (α i)), MeasurableSet x → eval i ⁻¹' x = S → ∃ x, (∀ (i : ι), MeasurableSet (x i)) ∧ eval i ⁻¹' x i = S

Tactic:
intro t ht h

Result:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
⊢ ∃ x, (∀ (i : ι), MeasurableSet (x i)) ∧ eval i ⁻¹' x i = S

Proof state:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
⊢ ∃ x, (∀ (i : ι), MeasurableSet (x i)) ∧ eval i ⁻¹' x i = S

Tactic:
refine ⟨fun j ↦ if hji : j = i then by convert t else univ, fun j ↦ ?_, ?_⟩

Result:
case refine_1
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
j : ι
⊢ MeasurableSet ((fun j => if hji : j = i then ⋯.mpr t else univ) j)

case refine_2
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
⊢ eval i ⁻¹' (fun j => if hji : j = i then ⋯.mpr t else univ) i = S

Proof state:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
⊢ S ∈ {t | ∃ s, MeasurableSet s ∧ eval i ⁻¹' s = t} →
    S ∈ (fun a => eval i ⁻¹' a i) '' univ.pi fun i => {s | MeasurableSet s}

Tactic:
simp only [mem_setOf_eq, mem_image, mem_univ_pi, forall_exists_index, and_imp]

Result:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
⊢ ∀ (x : Set (α i)), MeasurableSet x → eval i ⁻¹' x = S → ∃ x, (∀ (i : ι), MeasurableSet (x i)) ∧ eval i ⁻¹' x i = S

Proof state:
case refine_2
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
⊢ (eval i ⁻¹' if h_1 : True then cast ⋯ t else univ) = eval i ⁻¹' t

Tactic:
ext1 x

Result:
case refine_2.h
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
x : (x : ι) → α x
⊢ (x ∈ eval i ⁻¹' if h_1 : True then cast ⋯ t else univ) ↔ x ∈ eval i ⁻¹' t

Proof state:
case refine_1
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
j : ι
⊢ MeasurableSet ((fun j => if hji : j = i then ⋯.mpr t else univ) j)

Tactic:
by_cases hji : j = i

Result:
case pos
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
j : ι
hji : j = i
⊢ MeasurableSet ((fun j => if hji : j = i then ⋯.mpr t else univ) j)

case neg
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
j : ι
hji : ¬j = i
⊢ MeasurableSet ((fun j => if hji : j = i then ⋯.mpr t else univ) j)

Proof state:
case refine_2
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
⊢ eval i ⁻¹' (fun j => if hji : j = i then ⋯.mpr t else univ) i = S

Tactic:
simp only [id_eq, eq_mpr_eq_cast, ← h]

Result:
case refine_2
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
⊢ (eval i ⁻¹' if h_1 : True then cast ⋯ t else univ) = eval i ⁻¹' t

Proof state:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
j : ι
hji : j = i
⊢ Set (α j)

Tactic:
convert t

Result:
no goals

Proof state:
case pos
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
j : ι
hji : j = i
⊢ MeasurableSet (cast ⋯ t)

Tactic:
convert ht

Result:
case h.e'_3
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
j : ι
hji : j = i
e_1✝ : α j = α i
⊢ HEq (cast ⋯ t) t

Proof state:
case pos
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
j : ι
hji : j = i
⊢ MeasurableSet ((fun j => if hji : j = i then ⋯.mpr t else univ) j)

Tactic:
simp only [hji, eq_self_iff_true, eq_mpr_eq_cast, dif_pos]

Result:
case pos
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
j : ι
hji : j = i
⊢ MeasurableSet (cast ⋯ t)

Proof state:
case neg
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
j : ι
hji : ¬j = i
⊢ MeasurableSet ((fun j => if hji : j = i then ⋯.mpr t else univ) j)

Tactic:
simp only [hji, not_false_iff, dif_neg, MeasurableSet.univ]

Result:
no goals

Proof state:
case refine_2.h
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
x : (x : ι) → α x
⊢ (x ∈ eval i ⁻¹' if h_1 : True then cast ⋯ t else univ) ↔ x ∈ eval i ⁻¹' t

Tactic:
simp only [singleton_pi, Function.eval, cast_eq, dite_eq_ite, ite_true, mem_preimage]

Result:
no goals

Proof state:
case h.e'_3
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
j : ι
hji : j = i
e_1✝ : α j = α i
⊢ HEq (cast ⋯ t) t

Tactic:
simp only [id_eq, cast_heq]

Result:
no goals

Proof state:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ MeasurableSpace.generateFrom {t | ∃ s, MeasurableSet s ∧ eval i ⁻¹' s = t} ≤
    MeasurableSpace.generateFrom ((fun a => eval i ⁻¹' a i) '' univ.pi fun i => {s | MeasurableSet s})

Tactic:
refine MeasurableSpace.generateFrom_mono fun S ↦ ?_

Result:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
⊢ S ∈ {t | ∃ s, MeasurableSet s ∧ eval i ⁻¹' s = t} →
    S ∈ (fun a => eval i ⁻¹' a i) '' univ.pi fun i => {s | MeasurableSet s}

Proof state:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ MeasurableSpace.comap (eval i) (m i) ≤
    MeasurableSpace.generateFrom ((fun a => eval i ⁻¹' a i) '' univ.pi fun i => {s | MeasurableSet s})

Tactic:
rw [MeasurableSpace.comap_eq_generateFrom]

Result:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ MeasurableSpace.generateFrom {t | ∃ s, MeasurableSet s ∧ eval i ⁻¹' s = t} ≤
    MeasurableSpace.generateFrom ((fun a => eval i ⁻¹' a i) '' univ.pi fun i => {s | MeasurableSet s})