-- Mathlib/Data/Set/Prod.lean
theorem sumPiEquivProdPi_symm_preimage_univ_pi (π : ι ⊕ ι' → Type*) (t : ∀ i, Set (π i)) :
    (sumPiEquivProdPi π).symm ⁻¹' univ.pi t =
    univ.pi (fun i => t (.inl i)) ×ˢ univ.pi fun i => t (.inr i)

Proof state:
case h
ι : Type u_1
ι' : Type u_2
π : ι ⊕ ι' → Type u_4
t : (i : ι ⊕ ι') → Set (π i)
x✝ : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))
⊢ (∀ (i : ι ⊕ ι'), Sum.rec x✝.1 x✝.2 i ∈ t i) ↔ (∀ (i : ι), x✝.1 i ∈ t (Sum.inl i)) ∧ ∀ (i : ι'), x✝.2 i ∈ t (Sum.inr i)

Tactic:
constructor

Result:
case h.mp
ι : Type u_1
ι' : Type u_2
π : ι ⊕ ι' → Type u_4
t : (i : ι ⊕ ι') → Set (π i)
x✝ : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))
⊢ (∀ (i : ι ⊕ ι'), Sum.rec x✝.1 x✝.2 i ∈ t i) → (∀ (i : ι), x✝.1 i ∈ t (Sum.inl i)) ∧ ∀ (i : ι'), x✝.2 i ∈ t (Sum.inr i)

case h.mpr
ι : Type u_1
ι' : Type u_2
π : ι ⊕ ι' → Type u_4
t : (i : ι ⊕ ι') → Set (π i)
x✝ : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))
⊢ ((∀ (i : ι), x✝.1 i ∈ t (Sum.inl i)) ∧ ∀ (i : ι'), x✝.2 i ∈ t (Sum.inr i)) → ∀ (i : ι ⊕ ι'), Sum.rec x✝.1 x✝.2 i ∈ t i

Proof state:
case h.mpr
ι : Type u_1
ι' : Type u_2
π : ι ⊕ ι' → Type u_4
t : (i : ι ⊕ ι') → Set (π i)
x✝ : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))
⊢ ((∀ (i : ι), x✝.1 i ∈ t (Sum.inl i)) ∧ ∀ (i : ι'), x✝.2 i ∈ t (Sum.inr i)) → ∀ (i : ι ⊕ ι'), Sum.rec x✝.1 x✝.2 i ∈ t i

Tactic:
rintro ⟨h₁, h₂⟩ (i|i) <;> simp <;> apply_assumption

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
π : ι ⊕ ι' → Type u_4
t : (i : ι ⊕ ι') → Set (π i)
⊢ ⇑(sumPiEquivProdPi π).symm ⁻¹' univ.pi t = (univ.pi fun i => t (Sum.inl i)) ×ˢ univ.pi fun i => t (Sum.inr i)

Tactic:
ext

Result:
case h
ι : Type u_1
ι' : Type u_2
π : ι ⊕ ι' → Type u_4
t : (i : ι ⊕ ι') → Set (π i)
x✝ : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))
⊢ x✝ ∈ ⇑(sumPiEquivProdPi π).symm ⁻¹' univ.pi t ↔
    x✝ ∈ (univ.pi fun i => t (Sum.inl i)) ×ˢ univ.pi fun i => t (Sum.inr i)

Proof state:
case h
ι : Type u_1
ι' : Type u_2
π : ι ⊕ ι' → Type u_4
t : (i : ι ⊕ ι') → Set (π i)
x✝ : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))
⊢ x✝ ∈ ⇑(sumPiEquivProdPi π).symm ⁻¹' univ.pi t ↔
    x✝ ∈ (univ.pi fun i => t (Sum.inl i)) ×ˢ univ.pi fun i => t (Sum.inr i)

Tactic:
simp_rw [mem_preimage, mem_prod, mem_univ_pi, sumPiEquivProdPi_symm_apply]

Result:
case h
ι : Type u_1
ι' : Type u_2
π : ι ⊕ ι' → Type u_4
t : (i : ι ⊕ ι') → Set (π i)
x✝ : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))
⊢ (∀ (i : ι ⊕ ι'), Sum.rec x✝.1 x✝.2 i ∈ t i) ↔ (∀ (i : ι), x✝.1 i ∈ t (Sum.inl i)) ∧ ∀ (i : ι'), x✝.2 i ∈ t (Sum.inr i)

Proof state:
case h.mp
ι : Type u_1
ι' : Type u_2
π : ι ⊕ ι' → Type u_4
t : (i : ι ⊕ ι') → Set (π i)
x✝ : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))
h : ∀ (i : ι ⊕ ι'), Sum.rec x✝.1 x✝.2 i ∈ t i
⊢ (∀ (i : ι), x✝.1 i ∈ t (Sum.inl i)) ∧ ∀ (i : ι'), x✝.2 i ∈ t (Sum.inr i)

Tactic:
constructor <;> intro i <;> apply h

Result:
no goals

Proof state:
case h.mp
ι : Type u_1
ι' : Type u_2
π : ι ⊕ ι' → Type u_4
t : (i : ι ⊕ ι') → Set (π i)
x✝ : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))
⊢ (∀ (i : ι ⊕ ι'), Sum.rec x✝.1 x✝.2 i ∈ t i) → (∀ (i : ι), x✝.1 i ∈ t (Sum.inl i)) ∧ ∀ (i : ι'), x✝.2 i ∈ t (Sum.inr i)

Tactic:
intro h

Result:
case h.mp
ι : Type u_1
ι' : Type u_2
π : ι ⊕ ι' → Type u_4
t : (i : ι ⊕ ι') → Set (π i)
x✝ : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))
h : ∀ (i : ι ⊕ ι'), Sum.rec x✝.1 x✝.2 i ∈ t i
⊢ (∀ (i : ι), x✝.1 i ∈ t (Sum.inl i)) ∧ ∀ (i : ι'), x✝.2 i ∈ t (Sum.inr i)