case intro
α : Type u_1
α' : Type ?u.54713
β : Type u_2
β' : Type ?u.54719
γ : Type u_3
γ' : Type ?u.54725
δ : Type ?u.54728
δ' : Type ?u.54731
ε : Type ?u.54734
ε' : Type ?u.54737
ζ : Type ?u.54740
ζ' : Type ?u.54743
ν : Type ?u.54746
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 : γ
s : Finset α
hf : ∀ (a : α), Injective (f a)
a : α
ha : a ∈ s
⊢ card t ≤ card (image₂ f s t)
α : Type u_1
α' : Type ?u.54713
β : Type u_2
β' : Type ?u.54719
γ : Type u_3
γ' : Type ?u.54725
δ : Type ?u.54728
δ' : Type ?u.54731
ε : Type ?u.54734
ε' : Type ?u.54737
ζ : Type ?u.54740
ζ' : Type ?u.54743
ν : Type ?u.54746
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 : γ
s : Finset α
hs : Finset.Nonempty s
hf : ∀ (a : α), Injective (f a)
⊢ card t ≤ card (image₂ f s t)
obtain ⟨a, ha⟩ := hs
case intro
α : Type u_1
α' : Type ?u.54713
β : Type u_2
β' : Type ?u.54719
γ : Type u_3
γ' : Type ?u.54725
δ : Type ?u.54728
δ' : Type ?u.54731
ε : Type ?u.54734
ε' : Type ?u.54737
ζ : Type ?u.54740
ζ' : Type ?u.54743
ν : Type ?u.54746
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 : γ
s : Finset α
hf : ∀ (a : α), Injective (f a)
a : α
ha : a ∈ s
⊢ card (image₂ f {a} t) ≤ card (image₂ f s t)
case intro
α : Type u_1
α' : Type ?u.54713
β : Type u_2
β' : Type ?u.54719
γ : Type u_3
γ' : Type ?u.54725
δ : Type ?u.54728
δ' : Type ?u.54731
ε : Type ?u.54734
ε' : Type ?u.54737
ζ : Type ?u.54740
ζ' : Type ?u.54743
ν : Type ?u.54746
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 : γ
s : Finset α
hf : ∀ (a : α), Injective (f a)
a : α
ha : a ∈ s
⊢ card t ≤ card (image₂ f s t)
rw [← card_image₂_singleton_left _ (hf a)]
no goals
case intro
α : Type u_1
α' : Type ?u.54713
β : Type u_2
β' : Type ?u.54719
γ : Type u_3
γ' : Type ?u.54725
δ : Type ?u.54728
δ' : Type ?u.54731
ε : Type ?u.54734
ε' : Type ?u.54737
ζ : Type ?u.54740
ζ' : Type ?u.54743
ν : Type ?u.54746
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 : γ
s : Finset α
hf : ∀ (a : α), Injective (f a)
a : α
ha : a ∈ s
⊢ card (image₂ f {a} t) ≤ card (image₂ f s t)
exact card_le_of_subset (image₂_subset_right <| singleton_subset_iff.2 ha)