case intro.intro.intro.intro.intro
α : Type u_3
β : Type u_1
γ : Type u_2
f✝ : α → β
s✝ t✝ : Set α
f : β → α
g : γ → α
s : Set β
t : Set γ
h : ∀ (b : β), b ∈ s → ∀ (c : γ), c ∈ t → f b ≠ g c
b : β
hb : b ∈ s
c : γ
hc : c ∈ t
eq : f b = g c
⊢ g c ∈ ⊥
α : Type u_3
β : Type u_1
γ : Type u_2
f✝ : α → β
s✝ t✝ : Set α
f : β → α
g : γ → α
s : Set β
t : Set γ
h : ∀ (b : β), b ∈ s → ∀ (c : γ), c ∈ t → f b ≠ g c
⊢ f '' s ⊓ g '' t ≤ ⊥
rintro a ⟨⟨b, hb, eq⟩, c, hc, rfl⟩
no goals
case intro.intro.intro.intro.intro
α : Type u_3
β : Type u_1
γ : Type u_2
f✝ : α → β
s✝ t✝ : Set α
f : β → α
g : γ → α
s : Set β
t : Set γ
h : ∀ (b : β), b ∈ s → ∀ (c : γ), c ∈ t → f b ≠ g c
b : β
hb : b ∈ s
c : γ
hc : c ∈ t
eq : f b = g c
⊢ g c ∈ ⊥
exact h b hb c hc eq