-- Mathlib/Data/Set/Prod.lean
theorem union_pi_inter
    (ht₁ : ∀ i ∉ s₁, t₁ i = univ) (ht₂ : ∀ i ∉ s₂, t₂ i = univ) :
    (s₁ ∪ s₂).pi (fun i ↦ t₁ i ∩ t₂ i) = s₁.pi t₁ ∩ s₂.pi t₂

Proof state:
case h.inl
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
h : (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i
i : ι
hi : i ∈ s₁
⊢ x i ∈ t₁ i ∧ x i ∈ t₂ i

Tactic:
by_cases hi2 : i ∈ s₂

Result:
case pos
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
h : (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i
i : ι
hi : i ∈ s₁
hi2 : i ∈ s₂
⊢ x i ∈ t₁ i ∧ x i ∈ t₂ i

case neg
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
h : (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i
i : ι
hi : i ∈ s₁
hi2 : i ∉ s₂
⊢ x i ∈ t₁ i ∧ x i ∈ t₂ i

Proof state:
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
⊢ ((s₁ ∪ s₂).pi fun i => t₁ i ∩ t₂ i) = s₁.pi t₁ ∩ s₂.pi t₂

Tactic:
ext x

Result:
case h
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
⊢ (x ∈ (s₁ ∪ s₂).pi fun i => t₁ i ∩ t₂ i) ↔ x ∈ s₁.pi t₁ ∩ s₂.pi t₂

Proof state:
case pos
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
h : (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i
i : ι
hi : i ∈ s₁
hi2 : i ∈ s₂
⊢ x i ∈ t₁ i ∧ x i ∈ t₂ i

Tactic:
exact ⟨h.1 i hi, h.2 i hi2⟩

Result:
no goals

Proof state:
case neg
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
h : (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i
i : ι
hi : i ∈ s₁
hi2 : i ∉ s₂
⊢ x i ∈ univ

Tactic:
exact mem_univ _

Result:
no goals

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
h : (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i
i : ι
hi : i ∈ s₁ ∨ i ∈ s₂
⊢ x i ∈ t₁ i ∧ x i ∈ t₂ i

Tactic:
rcases hi with hi | hi

Result:
case h.inl
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
h : (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i
i : ι
hi : i ∈ s₁
⊢ x i ∈ t₁ i ∧ x i ∈ t₂ i

case h.inr
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
h : (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i
i : ι
hi : i ∈ s₂
⊢ x i ∈ t₁ i ∧ x i ∈ t₂ i

Proof state:
case neg
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
h : (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i
i : ι
hi : i ∈ s₁
hi2 : i ∉ s₂
⊢ x i ∈ t₂ i

Tactic:
rw [ht₂ i hi2]

Result:
case neg
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
h : (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i
i : ι
hi : i ∈ s₁
hi2 : i ∉ s₂
⊢ x i ∈ univ

Proof state:
case pos
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
h : (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i
i : ι
hi : i ∈ s₂
hi1 : i ∈ s₁
⊢ x i ∈ t₁ i ∧ x i ∈ t₂ i

Tactic:
exact ⟨h.1 i hi1, h.2 i hi⟩

Result:
no goals

Proof state:
case neg
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
h : (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i
i : ι
hi : i ∈ s₂
hi1 : i ∉ s₁
⊢ x i ∈ t₁ i ∧ x i ∈ t₂ i

Tactic:
refine ⟨?_, h.2 i hi⟩

Result:
case neg
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
h : (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i
i : ι
hi : i ∈ s₂
hi1 : i ∉ s₁
⊢ x i ∈ t₁ i

Proof state:
case h.inr
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
h : (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i
i : ι
hi : i ∈ s₂
⊢ x i ∈ t₁ i ∧ x i ∈ t₂ i

Tactic:
by_cases hi1 : i ∈ s₁

Result:
case pos
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
h : (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i
i : ι
hi : i ∈ s₂
hi1 : i ∈ s₁
⊢ x i ∈ t₁ i ∧ x i ∈ t₂ i

case neg
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
h : (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i
i : ι
hi : i ∈ s₂
hi1 : i ∉ s₁
⊢ x i ∈ t₁ i ∧ x i ∈ t₂ i

Proof state:
case neg
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
h : (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i
i : ι
hi : i ∈ s₂
hi1 : i ∉ s₁
⊢ x i ∈ t₁ i

Tactic:
rw [ht₁ i hi1]

Result:
case neg
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
h : (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i
i : ι
hi : i ∈ s₂
hi1 : i ∉ s₁
⊢ x i ∈ univ

Proof state:
case neg
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
h : (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i
i : ι
hi : i ∈ s₂
hi1 : i ∉ s₁
⊢ x i ∈ univ

Tactic:
exact mem_univ _

Result:
no goals

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
⊢ (x ∈ (s₁ ∪ s₂).pi fun i => t₁ i ∩ t₂ i) ↔ x ∈ s₁.pi t₁ ∩ s₂.pi t₂

Tactic:
simp only [mem_pi, mem_union, mem_inter_iff]

Result:
case h
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
⊢ (∀ (i : ι), i ∈ s₁ ∨ i ∈ s₂ → x i ∈ t₁ i ∧ x i ∈ t₂ i) ↔ (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i

Proof state:
case neg
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
h : (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i
i : ι
hi : i ∈ s₁
hi2 : i ∉ s₂
⊢ x i ∈ t₁ i ∧ x i ∈ t₂ i

Tactic:
refine ⟨h.1 i hi, ?_⟩

Result:
case neg
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
h : (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i
i : ι
hi : i ∈ s₁
hi2 : i ∉ s₂
⊢ x i ∈ t₂ i

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
⊢ (∀ (i : ι), i ∈ s₁ ∨ i ∈ s₂ → x i ∈ t₁ i ∧ x i ∈ t₂ i) ↔ (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i

Tactic:
refine ⟨fun h ↦ ⟨fun i his₁ ↦ (h i (Or.inl his₁)).1, fun i his₂ ↦ (h i (Or.inr his₂)).2⟩,
  fun h i hi ↦ ?_⟩

Result:
case h
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ i ∉ s₁, t₁ i = univ
ht₂ : ∀ i ∉ s₂, t₂ i = univ
x : (i : ι) → α i
h : (∀ i ∈ s₁, x i ∈ t₁ i) ∧ ∀ i ∈ s₂, x i ∈ t₂ i
i : ι
hi : i ∈ s₁ ∨ i ∈ s₂
⊢ x i ∈ t₁ i ∧ x i ∈ t₂ i