case intro
α : Type u_2
α' : Type ?u.55415
β : Type u_1
β' : Type ?u.55421
γ : Type u_3
γ' : Type ?u.55427
δ : Type ?u.55430
δ' : Type ?u.55433
ε : Type ?u.55436
ε' : Type ?u.55439
ζ : Type ?u.55442
ζ' : Type ?u.55445
ν : Type ?u.55448
inst✝⁷ : DecidableEq α'
inst✝⁶ : DecidableEq β'
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq γ'
inst✝³ : DecidableEq δ
inst✝² : DecidableEq δ'
inst✝¹ : DecidableEq ε
inst✝ : DecidableEq ε'
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Finset α
t✝ t' : Finset β
u u' : Finset γ
a a' : α
b✝ b' : β
c : γ
t : Finset β
hf : ∀ (b : β), Injective fun a => f a b
b : β
hb : b ∈ t
⊢ card s ≤ card (image₂ f s t)
α : Type u_2
α' : Type ?u.55415
β : Type u_1
β' : Type ?u.55421
γ : Type u_3
γ' : Type ?u.55427
δ : Type ?u.55430
δ' : Type ?u.55433
ε : Type ?u.55436
ε' : Type ?u.55439
ζ : Type ?u.55442
ζ' : Type ?u.55445
ν : Type ?u.55448
inst✝⁷ : DecidableEq α'
inst✝⁶ : DecidableEq β'
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq γ'
inst✝³ : DecidableEq δ
inst✝² : DecidableEq δ'
inst✝¹ : DecidableEq ε
inst✝ : DecidableEq ε'
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Finset α
t✝ t' : Finset β
u u' : Finset γ
a a' : α
b b' : β
c : γ
t : Finset β
ht : Finset.Nonempty t
hf : ∀ (b : β), Injective fun a => f a b
⊢ card s ≤ card (image₂ f s t)
obtain ⟨b, hb⟩ := ht
case intro
α : Type u_2
α' : Type ?u.55415
β : Type u_1
β' : Type ?u.55421
γ : Type u_3
γ' : Type ?u.55427
δ : Type ?u.55430
δ' : Type ?u.55433
ε : Type ?u.55436
ε' : Type ?u.55439
ζ : Type ?u.55442
ζ' : Type ?u.55445
ν : Type ?u.55448
inst✝⁷ : DecidableEq α'
inst✝⁶ : DecidableEq β'
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq γ'
inst✝³ : DecidableEq δ
inst✝² : DecidableEq δ'
inst✝¹ : DecidableEq ε
inst✝ : DecidableEq ε'
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Finset α
t✝ t' : Finset β
u u' : Finset γ
a a' : α
b✝ b' : β
c : γ
t : Finset β
hf : ∀ (b : β), Injective fun a => f a b
b : β
hb : b ∈ t
⊢ card (image₂ (fun a => f a) s {b}) ≤ card (image₂ f s t)
case intro
α : Type u_2
α' : Type ?u.55415
β : Type u_1
β' : Type ?u.55421
γ : Type u_3
γ' : Type ?u.55427
δ : Type ?u.55430
δ' : Type ?u.55433
ε : Type ?u.55436
ε' : Type ?u.55439
ζ : Type ?u.55442
ζ' : Type ?u.55445
ν : Type ?u.55448
inst✝⁷ : DecidableEq α'
inst✝⁶ : DecidableEq β'
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq γ'
inst✝³ : DecidableEq δ
inst✝² : DecidableEq δ'
inst✝¹ : DecidableEq ε
inst✝ : DecidableEq ε'
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Finset α
t✝ t' : Finset β
u u' : Finset γ
a a' : α
b✝ b' : β
c : γ
t : Finset β
hf : ∀ (b : β), Injective fun a => f a b
b : β
hb : b ∈ t
⊢ card s ≤ card (image₂ f s t)
rw [← card_image₂_singleton_right _ (hf b)]
no goals
case intro
α : Type u_2
α' : Type ?u.55415
β : Type u_1
β' : Type ?u.55421
γ : Type u_3
γ' : Type ?u.55427
δ : Type ?u.55430
δ' : Type ?u.55433
ε : Type ?u.55436
ε' : Type ?u.55439
ζ : Type ?u.55442
ζ' : Type ?u.55445
ν : Type ?u.55448
inst✝⁷ : DecidableEq α'
inst✝⁶ : DecidableEq β'
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq γ'
inst✝³ : DecidableEq δ
inst✝² : DecidableEq δ'
inst✝¹ : DecidableEq ε
inst✝ : DecidableEq ε'
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Finset α
t✝ t' : Finset β
u u' : Finset γ
a a' : α
b✝ b' : β
c : γ
t : Finset β
hf : ∀ (b : β), Injective fun a => f a b
b : β
hb : b ∈ t
⊢ card (image₂ (fun a => f a) s {b}) ≤ card (image₂ f s t)
exact card_le_of_subset (image₂_subset_left <| singleton_subset_iff.2 hb)