α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i ≤ g i
i : ι
this : f i ≤ g i
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g (↑(Embedding.refl ι) i)))
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i ≤ g i
i : ι
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g (↑(Embedding.refl ι) i)))
have := H i
no goals
α β : Type u
ι : Type u_1
f g : ι → Cardinal
H : ∀ (i : ι), f i ≤ g i
i : ι
this : f i ≤ g i
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g (↑(Embedding.refl ι) i)))
rwa [← Quot.out_eq (f i), ← Quot.out_eq (g i)] at this