case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.237166
ι' : Sort ?u.237169
ι₂ : Sort ?u.237172
κ : ι → Sort ?u.237177
κ₁ : ι → Sort ?u.237182
κ₂ : ι → Sort ?u.237187
κ' : ι' → Sort ?u.237192
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ ((z, w) ∈ ⋃ (x : α), s x ×ˢ t x) ↔ (z, w) ∈ (⋃ (x : α), s x) ×ˢ ⋃ (x : α), t x
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.237166
ι' : Sort ?u.237169
ι₂ : Sort ?u.237172
κ : ι → Sort ?u.237177
κ₁ : ι → Sort ?u.237182
κ₂ : ι → Sort ?u.237187
κ' : ι' → Sort ?u.237192
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
⊢ (⋃ (x : α), s x ×ˢ t x) = (⋃ (x : α), s x) ×ˢ ⋃ (x : α), t x
ext ⟨z, w⟩
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.237166
ι' : Sort ?u.237169
ι₂ : Sort ?u.237172
κ : ι → Sort ?u.237177
κ₁ : ι → Sort ?u.237182
κ₂ : ι → Sort ?u.237187
κ' : ι' → Sort ?u.237192
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ (∀ (x : α), z ∈ s x → w ∈ t x → (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i) ∧
    ∀ (x : α), z ∈ s x → ∀ (x : α), w ∈ t x → ∃ i, z ∈ s i ∧ w ∈ t i
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.237166
ι' : Sort ?u.237169
ι₂ : Sort ?u.237172
κ : ι → Sort ?u.237177
κ₁ : ι → Sort ?u.237182
κ₂ : ι → Sort ?u.237187
κ' : ι' → Sort ?u.237192
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ ((z, w) ∈ ⋃ (x : α), s x ×ˢ t x) ↔ (z, w) ∈ (⋃ (x : α), s x) ×ˢ ⋃ (x : α), t x
simp only [mem_prod, mem_iUnion, exists_imp, and_imp, iff_def]
case h.mk.left
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.237166
ι' : Sort ?u.237169
ι₂ : Sort ?u.237172
κ : ι → Sort ?u.237177
κ₁ : ι → Sort ?u.237182
κ₂ : ι → Sort ?u.237187
κ' : ι' → Sort ?u.237192
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ ∀ (x : α), z ∈ s x → w ∈ t x → (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i

case h.mk.right
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.237166
ι' : Sort ?u.237169
ι₂ : Sort ?u.237172
κ : ι → Sort ?u.237177
κ₁ : ι → Sort ?u.237182
κ₂ : ι → Sort ?u.237187
κ' : ι' → Sort ?u.237192
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ ∀ (x : α), z ∈ s x → ∀ (x : α), w ∈ t x → ∃ i, z ∈ s i ∧ w ∈ t i
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.237166
ι' : Sort ?u.237169
ι₂ : Sort ?u.237172
κ : ι → Sort ?u.237177
κ₁ : ι → Sort ?u.237182
κ₂ : ι → Sort ?u.237187
κ' : ι' → Sort ?u.237192
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ (∀ (x : α), z ∈ s x → w ∈ t x → (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i) ∧
    ∀ (x : α), z ∈ s x → ∀ (x : α), w ∈ t x → ∃ i, z ∈ s i ∧ w ∈ t i
constructor
case h.mk.left
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.237166
ι' : Sort ?u.237169
ι₂ : Sort ?u.237172
κ : ι → Sort ?u.237177
κ₁ : ι → Sort ?u.237182
κ₂ : ι → Sort ?u.237187
κ' : ι' → Sort ?u.237192
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
x : α
hz : z ∈ s x
hw : w ∈ t x
⊢ (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i
case h.mk.left
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.237166
ι' : Sort ?u.237169
ι₂ : Sort ?u.237172
κ : ι → Sort ?u.237177
κ₁ : ι → Sort ?u.237182
κ₂ : ι → Sort ?u.237187
κ' : ι' → Sort ?u.237192
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ ∀ (x : α), z ∈ s x → w ∈ t x → (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i
intro x hz hw
no goals
case h.mk.left
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.237166
ι' : Sort ?u.237169
ι₂ : Sort ?u.237172
κ : ι → Sort ?u.237177
κ₁ : ι → Sort ?u.237182
κ₂ : ι → Sort ?u.237187
κ' : ι' → Sort ?u.237192
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
x : α
hz : z ∈ s x
hw : w ∈ t x
⊢ (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i
exact ⟨⟨x, hz⟩, x, hw⟩
case h.mk.right
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.237166
ι' : Sort ?u.237169
ι₂ : Sort ?u.237172
κ : ι → Sort ?u.237177
κ₁ : ι → Sort ?u.237182
κ₂ : ι → Sort ?u.237187
κ' : ι' → Sort ?u.237192
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
x : α
hz : z ∈ s x
x' : α
hw : w ∈ t x'
⊢ ∃ i, z ∈ s i ∧ w ∈ t i
case h.mk.right
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.237166
ι' : Sort ?u.237169
ι₂ : Sort ?u.237172
κ : ι → Sort ?u.237177
κ₁ : ι → Sort ?u.237182
κ₂ : ι → Sort ?u.237187
κ' : ι' → Sort ?u.237192
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ ∀ (x : α), z ∈ s x → ∀ (x : α), w ∈ t x → ∃ i, z ∈ s i ∧ w ∈ t i
intro x hz x' hw
no goals
case h.mk.right
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.237166
ι' : Sort ?u.237169
ι₂ : Sort ?u.237172
κ : ι → Sort ?u.237177
κ₁ : ι → Sort ?u.237182
κ₂ : ι → Sort ?u.237187
κ' : ι' → Sort ?u.237192
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
x : α
hz : z ∈ s x
x' : α
hw : w ∈ t x'
⊢ ∃ i, z ∈ s i ∧ w ∈ t i
exact ⟨x ⊔ x', hs le_sup_left hz, ht le_sup_right hw⟩