α β : Type u
ι : Type u_1
f : ι → Cardinal
i : ι
⊢ Quotient.mk isEquivalent (Quotient.out (f i)) ≤ sum f
α β : Type u
ι : Type u_1
f : ι → Cardinal
i : ι
⊢ f i ≤ sum f
rw [← Quotient.out_eq (f i)]
no goals
α β : Type u
ι : Type u_1
f : ι → Cardinal
i : ι
⊢ Quotient.mk isEquivalent (Quotient.out (f i)) ≤ sum f
exact ⟨⟨fun a => ⟨i, a⟩, fun a b h => by injection h⟩⟩
no goals
α β : Type u
ι : Type u_1
f : ι → Cardinal
i : ι
a b : Quotient.out (f i)
h : (fun a => { fst := i, snd := a }) a = (fun a => { fst := i, snd := a }) b
⊢ a = b
injection h