case h.mk
α : Type u_1
β : Type u_2
γ : Type ?u.274480
ι : Sort ?u.274483
ι' : Sort ?u.274486
ι₂ : Sort ?u.274489
κ : ι → Sort ?u.274494
κ₁ : ι → Sort ?u.274499
κ₂ : ι → Sort ?u.274504
κ' : ι' → Sort ?u.274509
s : Set α
t : Set β
a : α
b : β
⊢ (a, b) ∈ s ×ˢ t ↔ (a, b) ∈ seq (Prod.mk '' s) t
α : Type u_1
β : Type u_2
γ : Type ?u.274480
ι : Sort ?u.274483
ι' : Sort ?u.274486
ι₂ : Sort ?u.274489
κ : ι → Sort ?u.274494
κ₁ : ι → Sort ?u.274499
κ₂ : ι → Sort ?u.274504
κ' : ι' → Sort ?u.274509
s : Set α
t : Set β
⊢ s ×ˢ t = seq (Prod.mk '' s) t
ext ⟨a, b⟩
case h.mk.mp
α : Type u_1
β : Type u_2
γ : Type ?u.274480
ι : Sort ?u.274483
ι' : Sort ?u.274486
ι₂ : Sort ?u.274489
κ : ι → Sort ?u.274494
κ₁ : ι → Sort ?u.274499
κ₂ : ι → Sort ?u.274504
κ' : ι' → Sort ?u.274509
s : Set α
t : Set β
a : α
b : β
⊢ (a, b) ∈ s ×ˢ t → (a, b) ∈ seq (Prod.mk '' s) t

case h.mk.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.274480
ι : Sort ?u.274483
ι' : Sort ?u.274486
ι₂ : Sort ?u.274489
κ : ι → Sort ?u.274494
κ₁ : ι → Sort ?u.274499
κ₂ : ι → Sort ?u.274504
κ' : ι' → Sort ?u.274509
s : Set α
t : Set β
a : α
b : β
⊢ (a, b) ∈ seq (Prod.mk '' s) t → (a, b) ∈ s ×ˢ t
case h.mk
α : Type u_1
β : Type u_2
γ : Type ?u.274480
ι : Sort ?u.274483
ι' : Sort ?u.274486
ι₂ : Sort ?u.274489
κ : ι → Sort ?u.274494
κ₁ : ι → Sort ?u.274499
κ₂ : ι → Sort ?u.274504
κ' : ι' → Sort ?u.274509
s : Set α
t : Set β
a : α
b : β
⊢ (a, b) ∈ s ×ˢ t ↔ (a, b) ∈ seq (Prod.mk '' s) t
constructor
case h.mk.mp.intro
α : Type u_1
β : Type u_2
γ : Type ?u.274480
ι : Sort ?u.274483
ι' : Sort ?u.274486
ι₂ : Sort ?u.274489
κ : ι → Sort ?u.274494
κ₁ : ι → Sort ?u.274499
κ₂ : ι → Sort ?u.274504
κ' : ι' → Sort ?u.274509
s : Set α
t : Set β
a : α
b : β
ha : (a, b).fst ∈ s
hb : (a, b).snd ∈ t
⊢ (a, b) ∈ seq (Prod.mk '' s) t
case h.mk.mp
α : Type u_1
β : Type u_2
γ : Type ?u.274480
ι : Sort ?u.274483
ι' : Sort ?u.274486
ι₂ : Sort ?u.274489
κ : ι → Sort ?u.274494
κ₁ : ι → Sort ?u.274499
κ₂ : ι → Sort ?u.274504
κ' : ι' → Sort ?u.274509
s : Set α
t : Set β
a : α
b : β
⊢ (a, b) ∈ s ×ˢ t → (a, b) ∈ seq (Prod.mk '' s) t
rintro ⟨ha, hb⟩
no goals
case h.mk.mp.intro
α : Type u_1
β : Type u_2
γ : Type ?u.274480
ι : Sort ?u.274483
ι' : Sort ?u.274486
ι₂ : Sort ?u.274489
κ : ι → Sort ?u.274494
κ₁ : ι → Sort ?u.274499
κ₂ : ι → Sort ?u.274504
κ' : ι' → Sort ?u.274509
s : Set α
t : Set β
a : α
b : β
ha : (a, b).fst ∈ s
hb : (a, b).snd ∈ t
⊢ (a, b) ∈ seq (Prod.mk '' s) t
exact ⟨Prod.mk a, ⟨a, ha, rfl⟩, b, hb, rfl⟩
case h.mk.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.274480
ι : Sort ?u.274483
ι' : Sort ?u.274486
ι₂ : Sort ?u.274489
κ : ι → Sort ?u.274494
κ₁ : ι → Sort ?u.274499
κ₂ : ι → Sort ?u.274504
κ' : ι' → Sort ?u.274509
s : Set α
t : Set β
a : α
b : β
x : α
hx : x ∈ s
y : β
hy : y ∈ t
eq : (x, y) = (a, b)
⊢ (a, b) ∈ s ×ˢ t
case h.mk.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.274480
ι : Sort ?u.274483
ι' : Sort ?u.274486
ι₂ : Sort ?u.274489
κ : ι → Sort ?u.274494
κ₁ : ι → Sort ?u.274499
κ₂ : ι → Sort ?u.274504
κ' : ι' → Sort ?u.274509
s : Set α
t : Set β
a : α
b : β
⊢ (a, b) ∈ seq (Prod.mk '' s) t → (a, b) ∈ s ×ˢ t
rintro ⟨f, ⟨x, hx, rfl⟩, y, hy, eq⟩
case h.mk.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.274480
ι : Sort ?u.274483
ι' : Sort ?u.274486
ι₂ : Sort ?u.274489
κ : ι → Sort ?u.274494
κ₁ : ι → Sort ?u.274499
κ₂ : ι → Sort ?u.274504
κ' : ι' → Sort ?u.274509
s : Set α
t : Set β
a : α
b : β
x : α
hx : x ∈ s
y : β
hy : y ∈ t
eq : (x, y) = (a, b)
⊢ (x, y) ∈ s ×ˢ t
case h.mk.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.274480
ι : Sort ?u.274483
ι' : Sort ?u.274486
ι₂ : Sort ?u.274489
κ : ι → Sort ?u.274494
κ₁ : ι → Sort ?u.274499
κ₂ : ι → Sort ?u.274504
κ' : ι' → Sort ?u.274509
s : Set α
t : Set β
a : α
b : β
x : α
hx : x ∈ s
y : β
hy : y ∈ t
eq : (x, y) = (a, b)
⊢ (a, b) ∈ s ×ˢ t
rw [← eq]
no goals
case h.mk.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.274480
ι : Sort ?u.274483
ι' : Sort ?u.274486
ι₂ : Sort ?u.274489
κ : ι → Sort ?u.274494
κ₁ : ι → Sort ?u.274499
κ₂ : ι → Sort ?u.274504
κ' : ι' → Sort ?u.274509
s : Set α
t : Set β
a : α
b : β
x : α
hx : x ∈ s
y : β
hy : y ∈ t
eq : (x, y) = (a, b)
⊢ (x, y) ∈ s ×ˢ t
exact ⟨hx, hy⟩