α : Type u_2
α' : Type ?u.22051
β : Type u_3
β' : Type ?u.22057
γ : Type u_1
γ' : Type ?u.22063
δ : Type ?u.22066
δ' : Type ?u.22069
ε : Type ?u.22072
ε' : Type ?u.22075
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
⊢ (∃ s t, s ∈ f ∧ t ∈ g ∧ (s = ∅ ∨ t = ∅)) ↔ ∅ ∈ f ∨ ∅ ∈ g
α : Type u_2
α' : Type ?u.22051
β : Type u_3
β' : Type ?u.22057
γ : Type u_1
γ' : Type ?u.22063
δ : Type ?u.22066
δ' : Type ?u.22069
ε : Type ?u.22072
ε' : Type ?u.22075
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
⊢ map₂ m f g = ⊥ ↔ f = ⊥ ∨ g = ⊥
simp only [← empty_mem_iff_bot, mem_map₂_iff, subset_empty_iff, image2_eq_empty_iff]
case mp
α : Type u_2
α' : Type ?u.22051
β : Type u_3
β' : Type ?u.22057
γ : Type u_1
γ' : Type ?u.22063
δ : Type ?u.22066
δ' : Type ?u.22069
ε : Type ?u.22072
ε' : Type ?u.22075
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
⊢ (∃ s t, s ∈ f ∧ t ∈ g ∧ (s = ∅ ∨ t = ∅)) → ∅ ∈ f ∨ ∅ ∈ g

case mpr
α : Type u_2
α' : Type ?u.22051
β : Type u_3
β' : Type ?u.22057
γ : Type u_1
γ' : Type ?u.22063
δ : Type ?u.22066
δ' : Type ?u.22069
ε : Type ?u.22072
ε' : Type ?u.22075
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
⊢ ∅ ∈ f ∨ ∅ ∈ g → ∃ s t, s ∈ f ∧ t ∈ g ∧ (s = ∅ ∨ t = ∅)
α : Type u_2
α' : Type ?u.22051
β : Type u_3
β' : Type ?u.22057
γ : Type u_1
γ' : Type ?u.22063
δ : Type ?u.22066
δ' : Type ?u.22069
ε : Type ?u.22072
ε' : Type ?u.22075
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
⊢ (∃ s t, s ∈ f ∧ t ∈ g ∧ (s = ∅ ∨ t = ∅)) ↔ ∅ ∈ f ∨ ∅ ∈ g
constructor
case mp.intro.intro.intro.intro.inl
α : Type u_2
α' : Type ?u.22051
β : Type u_3
β' : Type ?u.22057
γ : Type u_1
γ' : Type ?u.22063
δ : Type ?u.22066
δ' : Type ?u.22069
ε : Type ?u.22072
ε' : Type ?u.22075
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
t : Set β
ht : t ∈ g
hs : ∅ ∈ f
⊢ ∅ ∈ f ∨ ∅ ∈ g

case mp.intro.intro.intro.intro.inr
α : Type u_2
α' : Type ?u.22051
β : Type u_3
β' : Type ?u.22057
γ : Type u_1
γ' : Type ?u.22063
δ : Type ?u.22066
δ' : Type ?u.22069
ε : Type ?u.22072
ε' : Type ?u.22075
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
s : Set α
hs : s ∈ f
ht : ∅ ∈ g
⊢ ∅ ∈ f ∨ ∅ ∈ g
case mp
α : Type u_2
α' : Type ?u.22051
β : Type u_3
β' : Type ?u.22057
γ : Type u_1
γ' : Type ?u.22063
δ : Type ?u.22066
δ' : Type ?u.22069
ε : Type ?u.22072
ε' : Type ?u.22075
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
⊢ (∃ s t, s ∈ f ∧ t ∈ g ∧ (s = ∅ ∨ t = ∅)) → ∅ ∈ f ∨ ∅ ∈ g
rintro ⟨s, t, hs, ht, rfl | rfl⟩
no goals
case mp.intro.intro.intro.intro.inl
α : Type u_2
α' : Type ?u.22051
β : Type u_3
β' : Type ?u.22057
γ : Type u_1
γ' : Type ?u.22063
δ : Type ?u.22066
δ' : Type ?u.22069
ε : Type ?u.22072
ε' : Type ?u.22075
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
t : Set β
ht : t ∈ g
hs : ∅ ∈ f
⊢ ∅ ∈ f ∨ ∅ ∈ g
exact Or.inl hs
no goals
case mp.intro.intro.intro.intro.inr
α : Type u_2
α' : Type ?u.22051
β : Type u_3
β' : Type ?u.22057
γ : Type u_1
γ' : Type ?u.22063
δ : Type ?u.22066
δ' : Type ?u.22069
ε : Type ?u.22072
ε' : Type ?u.22075
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
s : Set α
hs : s ∈ f
ht : ∅ ∈ g
⊢ ∅ ∈ f ∨ ∅ ∈ g
exact Or.inr ht
case mpr.inl
α : Type u_2
α' : Type ?u.22051
β : Type u_3
β' : Type ?u.22057
γ : Type u_1
γ' : Type ?u.22063
δ : Type ?u.22066
δ' : Type ?u.22069
ε : Type ?u.22072
ε' : Type ?u.22075
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h✝ h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
h : ∅ ∈ f
⊢ ∃ s t, s ∈ f ∧ t ∈ g ∧ (s = ∅ ∨ t = ∅)

case mpr.inr
α : Type u_2
α' : Type ?u.22051
β : Type u_3
β' : Type ?u.22057
γ : Type u_1
γ' : Type ?u.22063
δ : Type ?u.22066
δ' : Type ?u.22069
ε : Type ?u.22072
ε' : Type ?u.22075
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h✝ h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
h : ∅ ∈ g
⊢ ∃ s t, s ∈ f ∧ t ∈ g ∧ (s = ∅ ∨ t = ∅)
case mpr
α : Type u_2
α' : Type ?u.22051
β : Type u_3
β' : Type ?u.22057
γ : Type u_1
γ' : Type ?u.22063
δ : Type ?u.22066
δ' : Type ?u.22069
ε : Type ?u.22072
ε' : Type ?u.22075
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
⊢ ∅ ∈ f ∨ ∅ ∈ g → ∃ s t, s ∈ f ∧ t ∈ g ∧ (s = ∅ ∨ t = ∅)
rintro (h | h)
no goals
case mpr.inl
α : Type u_2
α' : Type ?u.22051
β : Type u_3
β' : Type ?u.22057
γ : Type u_1
γ' : Type ?u.22063
δ : Type ?u.22066
δ' : Type ?u.22069
ε : Type ?u.22072
ε' : Type ?u.22075
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h✝ h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
h : ∅ ∈ f
⊢ ∃ s t, s ∈ f ∧ t ∈ g ∧ (s = ∅ ∨ t = ∅)
exact ⟨_, _, h, univ_mem, Or.inl rfl⟩
no goals
case mpr.inr
α : Type u_2
α' : Type ?u.22051
β : Type u_3
β' : Type ?u.22057
γ : Type u_1
γ' : Type ?u.22063
δ : Type ?u.22066
δ' : Type ?u.22069
ε : Type ?u.22072
ε' : Type ?u.22075
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h✝ h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
h : ∅ ∈ g
⊢ ∃ s t, s ∈ f ∧ t ∈ g ∧ (s = ∅ ∨ t = ∅)
exact ⟨_, _, univ_mem, h, Or.inr rfl⟩