no goals
ι : Type ?u.862077
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq β
s : Finset α
t : α → Finset β
this : DecidableEq α
⊢ card (Finset.biUnion ∅ t) ≤ ∑ a in ∅, card (t a)
simp
ι : Type ?u.862077
β : Type u
α : Type v
γ : Type w
s✝¹ s₁ s₂ : Finset α
a✝ : α
f g : α → β
inst✝ : DecidableEq β
s✝ : Finset α
t : α → Finset β
this : DecidableEq α
a : α
s : Finset α
has : ¬a ∈ s
ih : card (Finset.biUnion s t) ≤ ∑ a in s, card (t a)
⊢ card (t a) + card (Finset.biUnion s t) ≤ card (t a) + ∑ x in s, card (t x)
ι : Type ?u.862077
β : Type u
α : Type v
γ : Type w
s✝¹ s₁ s₂ : Finset α
a✝ : α
f g : α → β
inst✝ : DecidableEq β
s✝ : Finset α
t : α → Finset β
this : DecidableEq α
a : α
s : Finset α
has : ¬a ∈ s
ih : card (Finset.biUnion s t) ≤ ∑ a in s, card (t a)
⊢ card (t a) + card (Finset.biUnion s t) ≤ ∑ a in insert a s, card (t a)
rw [sum_insert has]
no goals
ι : Type ?u.862077
β : Type u
α : Type v
γ : Type w
s✝¹ s₁ s₂ : Finset α
a✝ : α
f g : α → β
inst✝ : DecidableEq β
s✝ : Finset α
t : α → Finset β
this : DecidableEq α
a : α
s : Finset α
has : ¬a ∈ s
ih : card (Finset.biUnion s t) ≤ ∑ a in s, card (t a)
⊢ card (t a) + card (Finset.biUnion s t) ≤ card (t a) + ∑ x in s, card (t x)
exact add_le_add_left ih _