Extra facts about PProd

@[simp]

theorem PProd.mk.eta {α : Sort u_1} {β : Sort u_2} {p : PProd α β} : { fst := p.fst, snd := p.snd } = p

@[simp]

theorem PProd.forall {α : Sort u_1} {β : Sort u_2} {p : PProd α β → Prop} : ((x : PProd α β) → p x) ↔ (a : α) → (b : β) → p { fst := a, snd := b }

@[simp]

theorem PProd.exists {α : Sort u_1} {β : Sort u_2} {p : PProd α β → Prop} : (∃ x, p x) ↔ ∃ a b, p { fst := a, snd := b }

theorem PProd.forall' {α : Sort u_1} {β : Sort u_2} {p : α → β → Prop} : ((x : PProd α β) → p x.fst x.snd) ↔ (a : α) → (b : β) → p a b

theorem PProd.exists' {α : Sort u_1} {β : Sort u_2} {p : α → β → Prop} : (∃ x, p x.fst x.snd) ↔ ∃ a b, p a b

theorem Function.Injective.pprod_map {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {f : α → β} {g : γ → δ} (hf : Function.Injective f) (hg : Function.Injective g) : Function.Injective fun x => { fst := f x.fst, snd := g x.snd }