α : Type ?u.108255
β : Type ?u.108258
γ : Type ?u.108261
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a✝ : α
b✝ c : β
a b : ℕ
⊢ (range (a + b)).val = (range a).val ∪ (map (addLeftEmbedding a) (range b)).val
α : Type ?u.108255
β : Type ?u.108258
γ : Type ?u.108261
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a✝ : α
b✝ c : β
a b : ℕ
⊢ range (a + b) = range a ∪ map (addLeftEmbedding a) (range b)
rw [← val_inj, union_val]
no goals
α : Type ?u.108255
β : Type ?u.108258
γ : Type ?u.108261
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a✝ : α
b✝ c : β
a b : ℕ
⊢ (range (a + b)).val = (range a).val ∪ (map (addLeftEmbedding a) (range b)).val
exact Multiset.range_add_eq_union a b