/-
Copyright (c) 2020 Eric Wieser. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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

/-!
# Extra facts about `PProd`
-/


open Function

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

namespace PProd

@[simp]
theorem 
mk.eta: ∀ {α : Sort u_1} {β : Sort u_2} {p : PProd α β}, { fst := p.fst, snd := p.snd } = p
mk.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 t
PProd.casesOn 
p: PProd α β
p fun 
_: ?m.81
_ 
_: ?m.84
_ ↦ 
rfl: ∀ {α : Sort ?u.86} {a : α}, a = a
rfl
#align pprod.mk.eta 
PProd.mk.eta: ∀ {α : Sort u_1} {β : Sort u_2} {p : PProd α β}, { fst := p.fst, snd := p.snd } = p
PProd.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 α β → Prop
p : 
PProd: Sort ?u.131 → Sort ?u.130 → Sort (max(max1?u.131)?u.130)
PProd 
α: Sort ?u.117
α 
β: Sort ?u.120
β → 
Prop: Type
Prop} : (∀ 
x: ?m.136
x, 
p: PProd α β → Prop
p 
x: ?m.136
x) ↔ ∀ 
a: ?m.141
a 
b: ?m.144
b, 
p: PProd α β → Prop
p ⟨
a: ?m.141
a, 
b: ?m.144
b⟩ :=
  ⟨fun 
h: ?m.173
h 
a: ?m.176
a 
b: ?m.179
b ↦ 
h: ?m.173
h ⟨
a: ?m.176
a, 
b: ?m.179
b⟩, fun 
h: ?m.199
h ⟨
a: α
a, 
b: β
b⟩ ↦ 
h: ?m.199
h 
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 α β → Prop
p : 
PProd: Sort ?u.334 → Sort ?u.333 → Sort (max(max1?u.334)?u.333)
PProd 
α: Sort ?u.320
α 
β: Sort ?u.323
β → 
Prop: Type
Prop} : (∃ 
x: ?m.341
x, 
p: PProd α β → Prop
p 
x: ?m.341
x) ↔ ∃ 
a: ?m.348
a 
b: ?m.353
b, 
p: PProd α β → Prop
p ⟨
a: ?m.348
a, 
b: ?m.353
b⟩ :=
  ⟨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 b
forall' {
p: α → β → Prop
p : 
α: Sort ?u.782
α → 
β: Sort ?u.785
β → 
Prop: Type
Prop} : (∀ 
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: α → β → Prop
p 
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.817
a 
b: ?m.820
b, 
p: α → β → Prop
p 
a: ?m.817
a 
b: ?m.820
b :=
  
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 b
PProd.forall'

theorem 
exists': ∀ {α : Sort u_1} {β : Sort u_2} {p : α → β → Prop}, (∃ x, p x.fst x.snd) ↔ ∃ a b, p a b
exists' {
p: α → β → Prop
p : 
α: Sort ?u.852
α → 
β: Sort ?u.855
β → 
Prop: Type
Prop} : (∃ 
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: α → β → Prop
p 
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.891
a 
b: ?m.896
b, 
p: α → β → Prop
p 
a: ?m.891
a 
b: ?m.896
b :=
  
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 b
PProd.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 f
hf : 
Injective: {α : Sort ?u.959} → {β : Sort ?u.958} → (α → β) → Prop
Injective 
f: α → β
f) (
hg: Injective g
hg : 
Injective: {α : Sort ?u.968} → {β : Sort ?u.967} → (α → β) → Prop
Injective 
g: γ → δ
g) :
    
Injective: {α : Sort ?u.977} → {β : Sort ?u.976} → (α → β) → Prop
Injective (fun 
x: ?m.988
x ↦ ⟨
f: α → β
f 
x: ?m.988
x.
1: {α : Sort ?u.1001} → {β : Sort ?u.1000} → PProd α β → α
1, 
g: γ → δ
g 
x: ?m.988
x.
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.1030
h ↦
  have 
A: ?m.1033
A := 
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.1030
h
  have 
B: ?m.1061
B := 
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.1030
h
  
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 f
hf 
A: ?m.1033
A) (
hg: Injective g
hg 
B: ?m.1061
B)
#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