Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Eric Wieser

! This file was ported from Lean 3 source module data.prod.pprod
! leanprover-community/mathlib commit c4658a649d216f57e99621708b09dcb3dcccbd23
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Logic.Basic

/-!
-/

open Function

variable {α: Sort ?u.320α β: Sort ?u.17β γ: Sort ?u.788γ δ: Sort ?u.23δ : Sort _: Type ?u.11SortSort _: Type ?u.11 _}

namespace PProd

@[simp]
theorem mk.eta: ∀ {α : Sort u_1} {β : Sort u_2} {p : PProd α β}, { fst := p.fst, snd := p.snd } = pmk.eta {p: PProd α βp : PProd: Sort ?u.27 → Sort ?u.26 → Sort (max(max1?u.27)?u.26)PProd α: Sort ?u.14α β: Sort ?u.17β} : PProd.mk: {α : Sort ?u.32} → {β : Sort ?u.31} → α → β → PProd α βPProd.mk p: PProd α βp.1: {α : Sort ?u.36} → {β : Sort ?u.35} → PProd α β → α1 p: PProd α βp.2: {α : Sort ?u.42} → {β : Sort ?u.41} → PProd α β → β2 = p: PProd α βp :=
PProd.casesOn: ∀ {α : Sort ?u.49} {β : Sort ?u.48} {motive : PProd α β → Sort ?u.50} (t : PProd α β),
(∀ (fst : α) (snd : β), motive { fst := fst, snd := snd }) → motive tPProd.casesOn p: PProd α βp fun _: ?m.81_ _: ?m.84_ ↦ rfl: ∀ {α : Sort ?u.86} {a : α}, a = arfl
#align pprod.mk.eta PProd.mk.eta: ∀ {α : Sort u_1} {β : Sort u_2} {p : PProd α β}, { fst := p.fst, snd := p.snd } = pPProd.mk.eta

@[simp]
theorem «forall»: ∀ {α : Sort u_1} {β : Sort u_2} {p : PProd α β → Prop},
(∀ (x : PProd α β), p x) ↔ ∀ (a : α) (b : β), p { fst := a, snd := b }«forall» {p: PProd α β → Propp : PProd: Sort ?u.131 → Sort ?u.130 → Sort (max(max1?u.131)?u.130)PProd α: Sort ?u.117α β: Sort ?u.120β → Prop: TypeProp} : (∀ x: ?m.136x, p: PProd α β → Propp x: ?m.136x) ↔ ∀ a: ?m.141a b: ?m.144b, p: PProd α β → Propp ⟨a: ?m.141a, b: ?m.144b⟩ :=
⟨fun h: ?m.173h a: ?m.176a b: ?m.179b ↦ h: ?m.173h ⟨a: ?m.176a, b: ?m.179b⟩, fun h: ?m.199h ⟨a: αa, b: βb⟩ ↦ h: ?m.199h a: αa b: βb⟩
#align pprod.forall PProd.forall: ∀ {α : Sort u_1} {β : Sort u_2} {p : PProd α β → Prop},
(∀ (x : PProd α β), p x) ↔ ∀ (a : α) (b : β), p { fst := a, snd := b }PProd.forall

@[simp]
theorem «exists»: ∀ {α : Sort u_1} {β : Sort u_2} {p : PProd α β → Prop}, (∃ x, p x) ↔ ∃ a b, p { fst := a, snd := b }«exists» {p: PProd α β → Propp : PProd: Sort ?u.334 → Sort ?u.333 → Sort (max(max1?u.334)?u.333)PProd α: Sort ?u.320α β: Sort ?u.323β → Prop: TypeProp} : (∃ x: ?m.341x, p: PProd α β → Propp x: ?m.341x) ↔ ∃ a: ?m.348a b: ?m.353b, p: PProd α β → Propp ⟨a: ?m.348a, b: ?m.353b⟩ :=
⟨fun ⟨⟨a: αa, b: βb⟩, h: p { fst := a, snd := b }h⟩ ↦ ⟨a: αa, b: βb, h: p { fst := a, snd := b }h⟩, fun ⟨a: αa, b: βb, h: p { fst := a, snd := b }h⟩ ↦ ⟨⟨a: αa, b: βb⟩, h: p { fst := a, snd := b }h⟩⟩
#align pprod.exists PProd.exists: ∀ {α : Sort u_1} {β : Sort u_2} {p : PProd α β → Prop}, (∃ x, p x) ↔ ∃ a b, p { fst := a, snd := b }PProd.exists

theorem forall': ∀ {p : α → β → Prop}, (∀ (x : PProd α β), p x.fst x.snd) ↔ ∀ (a : α) (b : β), p a bforall' {p: α → β → Propp : α: Sort ?u.782α → β: Sort ?u.785β → Prop: TypeProp} : (∀ x: PProd α βx : PProd: Sort ?u.802 → Sort ?u.801 → Sort (max(max1?u.802)?u.801)PProd α: Sort ?u.782α β: Sort ?u.785β, p: α → β → Propp x: PProd α βx.1: {α : Sort ?u.806} → {β : Sort ?u.805} → PProd α β → α1 x: PProd α βx.2: {α : Sort ?u.812} → {β : Sort ?u.811} → PProd α β → β2) ↔ ∀ a: ?m.817a b: ?m.820b, p: α → β → Propp a: ?m.817a b: ?m.820b :=
PProd.forall: ∀ {α : Sort ?u.827} {β : Sort ?u.828} {p : PProd α β → Prop},
(∀ (x : PProd α β), p x) ↔ ∀ (a : α) (b : β), p { fst := a, snd := b }PProd.forall
#align pprod.forall' PProd.forall': ∀ {α : Sort u_1} {β : Sort u_2} {p : α → β → Prop}, (∀ (x : PProd α β), p x.fst x.snd) ↔ ∀ (a : α) (b : β), p a bPProd.forall'

theorem exists': ∀ {α : Sort u_1} {β : Sort u_2} {p : α → β → Prop}, (∃ x, p x.fst x.snd) ↔ ∃ a b, p a bexists' {p: α → β → Propp : α: Sort ?u.852α → β: Sort ?u.855β → Prop: TypeProp} : (∃ x: PProd α βx : PProd: Sort ?u.874 → Sort ?u.873 → Sort (max(max1?u.874)?u.873)PProd α: Sort ?u.852α β: Sort ?u.855β, p: α → β → Propp x: PProd α βx.1: {α : Sort ?u.877} → {β : Sort ?u.876} → PProd α β → α1 x: PProd α βx.2: {α : Sort ?u.883} → {β : Sort ?u.882} → PProd α β → β2) ↔ ∃ a: ?m.891a b: ?m.896b, p: α → β → Propp a: ?m.891a b: ?m.896b :=
PProd.exists: ∀ {α : Sort ?u.904} {β : Sort ?u.905} {p : PProd α β → Prop}, (∃ x, p x) ↔ ∃ a b, p { fst := a, snd := b }PProd.exists
#align pprod.exists' PProd.exists': ∀ {α : Sort u_1} {β : Sort u_2} {p : α → β → Prop}, (∃ x, p x.fst x.snd) ↔ ∃ a b, p a bPProd.exists'

end PProd

theorem Function.Injective.pprod_map: ∀ {f : α → β} {g : γ → δ}, Injective f → Injective g → Injective fun x => { fst := f x.fst, snd := g x.snd }Function.Injective.pprod_map {f: α → βf : α: Sort ?u.938α → β: Sort ?u.941β} {g: γ → δg : γ: Sort ?u.944γ → δ: Sort ?u.947δ} (hf: Injective fhf : Injective: {α : Sort ?u.959} → {β : Sort ?u.958} → (α → β) → PropInjective f: α → βf) (hg: Injective ghg : Injective: {α : Sort ?u.968} → {β : Sort ?u.967} → (α → β) → PropInjective g: γ → δg) :
Injective: {α : Sort ?u.977} → {β : Sort ?u.976} → (α → β) → PropInjective (fun x: ?m.988x ↦ ⟨f: α → βf x: ?m.988x.1: {α : Sort ?u.1001} → {β : Sort ?u.1000} → PProd α β → α1, g: γ → δg x: ?m.988x.2: {α : Sort ?u.1007} → {β : Sort ?u.1006} → PProd α β → β2⟩ : PProd: Sort ?u.983 → Sort ?u.982 → Sort (max(max1?u.983)?u.982)PProd α: Sort ?u.938α γ: Sort ?u.944γ → PProd: Sort ?u.986 → Sort ?u.985 → Sort (max(max1?u.986)?u.985)PProd β: Sort ?u.941β δ: Sort ?u.947δ) := fun _: ?m.1024_ _: ?m.1027_ h: ?m.1030h ↦
have A: ?m.1033A := congr_arg: ∀ {α : Sort ?u.1035} {β : Sort ?u.1034} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂congr_arg PProd.fst: {α : Sort ?u.1041} → {β : Sort ?u.1040} → PProd α β → αPProd.fst h: ?m.1030h
have B: ?m.1061B := congr_arg: ∀ {α : Sort ?u.1063} {β : Sort ?u.1062} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂congr_arg PProd.snd: {α : Sort ?u.1069} → {β : Sort ?u.1068} → PProd α β → βPProd.snd h: ?m.1030h
congr_arg₂: ∀ {α : Sort ?u.1084} {β : Sort ?u.1085} {γ : Sort ?u.1086} (f : α → β → γ) {x x' : α} {y y' : β},
x = x' → y = y' → f x y = f x' y'congr_arg₂ PProd.mk: {α : Sort ?u.1091} → {β : Sort ?u.1090} → α → β → PProd α βPProd.mk (hf: Injective fhf A: ?m.1033A) (hg: Injective ghg B: ?m.1061B)
#align function.injective.pprod_map Function.Injective.pprod_map: ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {f : α → β} {g : γ → δ},
Injective f → Injective g → Injective fun x => { fst := f x.fst, snd := g x.snd }Function.Injective.pprod_map
```