H✝ : Type u
H'✝ : Type ?u.49184
M : Type ?u.49187
M' : Type ?u.49190
M'' : Type ?u.49193
H : Type u_1
H' : Type u_2
α : Type u_3
f : H → α
⊢ (range fun p => (f p.fst, p.snd)) = range fun p => (f p.fst, p.snd)
H✝ : Type u
H'✝ : Type ?u.49184
M : Type ?u.49187
M' : Type ?u.49190
M'' : Type ?u.49193
H : Type u_1
H' : Type u_2
α : Type u_3
f : H → α
⊢ (range fun p => (f p.fst, p.snd)) = range f ×ˢ univ
rw [prod_range_univ_eq]
no goals
H✝ : Type u
H'✝ : Type ?u.49184
M : Type ?u.49187
M' : Type ?u.49190
M'' : Type ?u.49193
H : Type u_1
H' : Type u_2
α : Type u_3
f : H → α
⊢ (range fun p => (f p.fst, p.snd)) = range fun p => (f p.fst, p.snd)
rfl