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 : PProd α β), 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 : PProd α β), 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 : PProd α γ) => { fst := f x.fst, snd := g x.snd }