/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl

! This file was ported from Lean 3 source module data.subtype
! 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.Function.Basic

/-!
# Subtypes

This file provides basic API for subtypes, which are defined in core.

A subtype is a type made from restricting another type, say `α`, to its elements that satisfy some
predicate, say `p : α → Prop`. Specifically, it is the type of pairs `⟨val, property⟩` where
`val : α` and `property : p val`. It is denoted `Subtype p` and notation `{val : α // p val}` is
available.

A subtype has a natural coercion to the parent type, by coercing `⟨val, property⟩` to `val`. As
such, subtypes can be thought of as bundled sets, the difference being that elements of a set are
still of type `α` while elements of a subtype aren't.
-/


open Function

namespace Subtype

variable {α: Sort ?u.8288
α β: Sort ?u.3588
β γ: Sort ?u.5650
γ : Sort _: Type ?u.5644
SortSort _: Type ?u.5644
 _} {p: α → Prop
p q: α → Prop
q : α: Sort ?u.5644
α → Prop: Type
Prop}

attribute [coe] Subtype.val: {α : Sort u} → {p : α → Prop} → Subtype p → α
Subtype.val

initialize_simps_projections Subtype: {α : Sort u} → (α → Prop) → Sort (max1u)
Subtype (val: {α : Sort u} → (p : α → Prop) → Subtype p → α
val → coe: {α : Sort u} → (p : α → Prop) → Subtype p → α
coe)

/-- A version of `x.property` or `x.2` where `p` is syntactically applied to the coercion of `x`
  instead of `x.1`. A similar result is `Subtype.mem` in `Data.Set.Basic`. -/
theorem prop: ∀ (x : Subtype p), p ↑x
prop (x: Subtype p
x : Subtype: {α : Sort ?u.212} → (α → Prop) → Sort (max1?u.212)
Subtype p: α → Prop
p) : p: α → Prop
p x: Subtype p
x :=
  x: Subtype p
x.2: ∀ {α : Sort ?u.340} {p : α → Prop} (self : Subtype p), p ↑self
2
#align subtype.prop Subtype.prop: ∀ {α : Sort u_1} {p : α → Prop} (x : Subtype p), p ↑x
Subtype.prop

@[simp]
protected theorem «forall»: ∀ {q : { a // p a } → Prop}, (∀ (x : { a // p a }), q x) ↔ ∀ (a : α) (b : p a), q { val := a, property := b }
«forall» {q: { a // p a } → Prop
q : { a: ?m.373
a // p: α → Prop
p a: ?m.373
a } → Prop: Type
Prop} : (∀ x: ?m.381
x, q: { a // p a } → Prop
q x: ?m.381
x) ↔ ∀ a: ?m.386
a b: ?m.389
b, q: { a // p a } → Prop
q ⟨a: ?m.386
a, b: ?m.389
b⟩ :=
  ⟨fun h: ?m.419
h a: ?m.422
a b: ?m.425
b ↦ h: ?m.419
h ⟨a: ?m.422
a, b: ?m.425
b⟩, fun h: ?m.446
h ⟨a: α
a, b: p a
b⟩ ↦ h: ?m.446
h a: α
a b: p a
b⟩
#align subtype.forall Subtype.forall: ∀ {α : Sort u_1} {p : α → Prop} {q : { a // p a } → Prop},
  (∀ (x : { a // p a }), q x) ↔ ∀ (a : α) (b : p a), q { val := a, property := b }
Subtype.forall

/-- An alternative version of `Subtype.forall`. This one is useful if Lean cannot figure out `q`
  when using `Subtype.forall` from right to left. -/
protected theorem forall': ∀ {α : Sort u_1} {p : α → Prop} {q : (x : α) → p x → Prop},
  (∀ (x : α) (h : p x), q x h) ↔ ∀ (x : { a // p a }), q ↑x (_ : p ↑x)
forall' {q: (x : α) → p x → Prop
q : ∀ x: ?m.595
x, p: α → Prop
p x: ?m.595
x → Prop: Type
Prop} : (∀ x: ?m.603
x h: ?m.606
h, q: (x : α) → p x → Prop
q x: ?m.603
x h: ?m.606
h) ↔ ∀ x: { a // p a }
x : { a: ?m.615
a // p: α → Prop
p a: ?m.615
a }, q: (x : α) → p x → Prop
q x: { a // p a }
x x: { a // p a }
x.2: ∀ {α : Sort ?u.742} {p : α → Prop} (self : Subtype p), p ↑self
2 :=
  (@Subtype.forall: ∀ {α : Sort ?u.749} {p : α → Prop} {q : { a // p a } → Prop},
  (∀ (x : { a // p a }), q x) ↔ ∀ (a : α) (b : p a), q { val := a, property := b }
Subtype.forall _: Sort ?u.749
_ _: ?m.750 → Prop
_ fun x: ?m.753
x ↦ q: (x : α) → p x → Prop
q x: ?m.753
x.1: {α : Sort ?u.755} → {p : α → Prop} → Subtype p → α
1 x: ?m.753
x.2: ∀ {α : Sort ?u.764} {p : α → Prop} (self : Subtype p), p ↑self
2).symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)
symm
#align subtype.forall' Subtype.forall': ∀ {α : Sort u_1} {p : α → Prop} {q : (x : α) → p x → Prop},
  (∀ (x : α) (h : p x), q x h) ↔ ∀ (x : { a // p a }), q ↑x (_ : p ↑x)
Subtype.forall'

@[simp]
protected theorem «exists»: ∀ {α : Sort u_1} {p : α → Prop} {q : { a // p a } → Prop}, (∃ x, q x) ↔ ∃ a b, q { val := a, property := b }
«exists» {q: { a // p a } → Prop
q : { a: ?m.829
a // p: α → Prop
p a: ?m.829
a } → Prop: Type
Prop} : (∃ x: ?m.839
x, q: { a // p a } → Prop
q x: ?m.839
x) ↔ ∃ a: ?m.846
a b: ?m.851
b, q: { a // p a } → Prop
q ⟨a: ?m.846
a, b: ?m.851
b⟩ :=
  ⟨fun ⟨⟨a: α
a, b: p a
b⟩, h: q { val := a, property := b }
h⟩ ↦ ⟨a: α
a, b: p a
b, h: q { val := a, property := b }
h⟩, fun ⟨a: α
a, b: p a
b, h: q { val := a, property := b }
h⟩ ↦ ⟨⟨a: α
a, b: p a
b⟩, h: q { val := a, property := b }
h⟩⟩
#align subtype.exists Subtype.exists: ∀ {α : Sort u_1} {p : α → Prop} {q : { a // p a } → Prop}, (∃ x, q x) ↔ ∃ a b, q { val := a, property := b }
Subtype.exists

/-- An alternative version of `Subtype.exists`. This one is useful if Lean cannot figure out `q`
  when using `Subtype.exists` from right to left. -/
protected theorem exists': ∀ {q : (x : α) → p x → Prop}, (∃ x h, q x h) ↔ ∃ x, q ↑x (_ : p ↑x)
exists' {q: (x : α) → p x → Prop
q : ∀ x: ?m.1326
x, p: α → Prop
p x: ?m.1326
x → Prop: Type
Prop} : (∃ x: ?m.1336
x h: ?m.1341
h, q: (x : α) → p x → Prop
q x: ?m.1336
x h: ?m.1341
h) ↔ ∃ x: { a // p a }
x : { a: ?m.1353
a // p: α → Prop
p a: ?m.1353
a }, q: (x : α) → p x → Prop
q x: { a // p a }
x x: { a // p a }
x.2: ∀ {α : Sort ?u.1479} {p : α → Prop} (self : Subtype p), p ↑self
2 :=
  (@Subtype.exists: ∀ {α : Sort ?u.1487} {p : α → Prop} {q : { a // p a } → Prop}, (∃ x, q x) ↔ ∃ a b, q { val := a, property := b }
Subtype.exists _: Sort ?u.1487
_ _: ?m.1488 → Prop
_ fun x: ?m.1491
x ↦ q: (x : α) → p x → Prop
q x: ?m.1491
x.1: {α : Sort ?u.1493} → {p : α → Prop} → Subtype p → α
1 x: ?m.1491
x.2: ∀ {α : Sort ?u.1502} {p : α → Prop} (self : Subtype p), p ↑self
2).symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)
symm
#align subtype.exists' Subtype.exists': ∀ {α : Sort u_1} {p : α → Prop} {q : (x : α) → p x → Prop}, (∃ x h, q x h) ↔ ∃ x, q ↑x (_ : p ↑x)
Subtype.exists'

@[ext]
protected theorem ext: ∀ {α : Sort u_1} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2
ext : ∀ {a1: { x // p x }
a1 a2: { x // p x }
a2 : { x: ?m.1569
x // p: α → Prop
p x: ?m.1569
x }}, (a1: { x // p x }
a1 : α: Sort ?u.1548
α) = (a2: { x // p x }
a2 : α: Sort ?u.1548
α) → a1: { x // p x }
a1 = a2: { x // p x }
a2
  | ⟨_: α
_, _: p val✝
_⟩, ⟨_, _⟩, rfl: ∀ {α : Sort ?u.1813} {a : α}, a = a
rfl => rfl: ∀ {α : Sort ?u.1892} {a : α}, a = a
rfl
#align subtype.ext Subtype.ext: ∀ {α : Sort u_1} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2
Subtype.ext

theorem ext_iff: ∀ {α : Sort u_1} {p : α → Prop} {a1 a2 : { x // p x }}, a1 = a2 ↔ ↑a1 = ↑a2
ext_iff {a1: { x // p x }
a1 a2: { x // p x }
a2 : { x: ?m.2187
x // p: α → Prop
p x: ?m.2196
x }} : a1: { x // p x }
a1 = a2: { x // p x }
a2 ↔ (a1: { x // p x }
a1 : α: Sort ?u.2167
α) = (a2: { x // p x }
a2 : α: Sort ?u.2167
α) :=
  ⟨congr_arg: ∀ {α : Sort ?u.2427} {β : Sort ?u.2426} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg _: ?m.2428 → ?m.2429
_, Subtype.ext: ∀ {α : Sort ?u.2443} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2
Subtype.ext⟩
#align subtype.ext_iff Subtype.ext_iff: ∀ {α : Sort u_1} {p : α → Prop} {a1 a2 : { x // p x }}, a1 = a2 ↔ ↑a1 = ↑a2
Subtype.ext_iff

theorem heq_iff_coe_eq: ∀ {α : Sort u_1} {p q : α → Prop},
  (∀ (x : α), p x ↔ q x) → ∀ {a1 : { x // p x }} {a2 : { x // q x }}, HEq a1 a2 ↔ ↑a1 = ↑a2
heq_iff_coe_eq (h: ∀ (x : α), p x ↔ q x
h : ∀ x: ?m.2485
x, p: α → Prop
p x: ?m.2485
x ↔ q: α → Prop
q x: ?m.2485
x) {a1: { x // p x }
a1 : { x: ?m.2493
x // p: α → Prop
p x: ?m.2493
x }} {a2: { x // q x }
a2 : { x: ?m.2502
x // q: α → Prop
q x: ?m.2502
x }} :
    HEq: {α : Sort ?u.2508} → α → {β : Sort ?u.2508} → β → Prop
HEq a1: { x // p x }
a1 a2: { x // q x }
a2 ↔ (a1: { x // p x }
a1 : α: Sort ?u.2467
α) = (a2: { x // q x }
a2 : α: Sort ?u.2467
α) :=
  Eq.rec: ∀ {α : Sort ?u.2727} {a : α} {motive : (a_1 : α) → a = a_1 → Sort ?u.2728},
  motive a (_ : a = a) → ∀ {a_1 : α} (t : a = a_1), motive a_1 t
Eq.rec (motive := λ (pp: α → Prop
pp: (α: Sort ?u.2467
α → Prop: Type
Prop)) _: ?m.2751
_ => ∀ a2': { x // pp x }
a2' : {x: ?m.2757
x // pp: α → Prop
pp x: ?m.2757
x}, HEq: {α : Sort ?u.2763} → α → {β : Sort ?u.2763} → β → Prop
HEq a1: { x // p x }
a1 a2': { x // pp x }
a2' ↔ (a1: { x // p x }
a1 : α: Sort ?u.2467
α) = (a2': { x // pp x }
a2' : α: Sort ?u.2467
α))
         (λ _: ?m.2988
_ => heq_iff_eq: ∀ {α : Sort ?u.2990} {a b : α}, HEq a b ↔ a = b
heq_iff_eq.trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
trans ext_iff: ∀ {α : Sort ?u.3009} {p : α → Prop} {a1 a2 : { x // p x }}, a1 = a2 ↔ ↑a1 = ↑a2
ext_iff) (funext: ∀ {α : Sort ?u.3026} {β : α → Sort ?u.3025} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext $ λ x: ?m.3037
x => propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext (h: ∀ (x : α), p x ↔ q x
h x: ?m.3037
x)) a2: { x // q x }
a2
#align subtype.heq_iff_coe_eq Subtype.heq_iff_coe_eq: ∀ {α : Sort u_1} {p q : α → Prop},
  (∀ (x : α), p x ↔ q x) → ∀ {a1 : { x // p x }} {a2 : { x // q x }}, HEq a1 a2 ↔ ↑a1 = ↑a2
Subtype.heq_iff_coe_eq

lemma heq_iff_coe_heq: ∀ {α β : Sort u_1} {p : α → Prop} {q : β → Prop} {a : { x // p x }} {b : { y // q y }},
  α = β → HEq p q → (HEq a b ↔ HEq ↑a ↑b)
heq_iff_coe_heq {α: Sort u_1
α β: Sort u_1
β : Sort _: Type ?u.3087
SortSort _: Type ?u.3087
 _} {p: α → Prop
p : α: Sort ?u.3087
α → Prop: Type
Prop} {q: β → Prop
q : β: Sort ?u.3090
β → Prop: Type
Prop} {a: { x // p x }
a : {x: ?m.3104
x // p: α → Prop
p x: ?m.3104
x}}
    {b: { y // q y }
b : {y: ?m.3113
y // q: β → Prop
q y: ?m.3113
y}} (h: α = β
h : α: Sort ?u.3087
α = β: Sort ?u.3090
β) (h': HEq p q
h' : HEq: {α : Sort ?u.3141} → α → {β : Sort ?u.3141} → β → Prop
HEq p: α → Prop
p q: β → Prop
q) : HEq: {α : Sort ?u.3150} → α → {β : Sort ?u.3150} → β → Prop
HEq a: { x // p x }
a b: { y // q y }
b ↔ HEq: {α : Sort ?u.3156} → α → {β : Sort ?u.3156} → β → Prop
HEq (a: { x // p x }
a : α: Sort ?u.3087
α) (b: { y // q y }
b : β: Sort ?u.3090
β) := by
Goals accomplished! 🐙
  α✝: Sort ?u.3070

β✝: Sort ?u.3073

γ: Sort ?u.3076

p✝, q✝: α✝ → Prop

α, β: Sort u_1

p: α → Prop

q: β → Prop

a: { x // p x }

b: { y // q y }

h: α = β

h': HEq p q

HEq a b ↔ HEq ↑a ↑bsubst h: α = β
hα✝: Sort ?u.3070

β: Sort ?u.3073

γ: Sort ?u.3076

p✝, q✝: α✝ → Prop

α: Sort u_1

p: α → Prop

a: { x // p x }

q: α → Prop

b: { y // q y }

h': HEq p q

HEq a b ↔ HEq ↑a ↑b
  α✝: Sort ?u.3070

β✝: Sort ?u.3073

γ: Sort ?u.3076

p✝, q✝: α✝ → Prop

α, β: Sort u_1

p: α → Prop

q: β → Prop

a: { x // p x }

b: { y // q y }

h: α = β

h': HEq p q

HEq a b ↔ HEq ↑a ↑bsubst h': HEq p q
h'α✝: Sort ?u.3070

β: Sort ?u.3073

γ: Sort ?u.3076

p✝, q: α✝ → Prop

α: Sort u_1

p: α → Prop

a, b: { y // p y }

HEq a b ↔ HEq ↑a ↑b
  α✝: Sort ?u.3070

β✝: Sort ?u.3073

γ: Sort ?u.3076

p✝, q✝: α✝ → Prop

α, β: Sort u_1

p: α → Prop

q: β → Prop

a: { x // p x }

b: { y // q y }

h: α = β

h': HEq p q

HEq a b ↔ HEq ↑a ↑brw [α✝: Sort ?u.3070

β: Sort ?u.3073

γ: Sort ?u.3076

p✝, q: α✝ → Prop

α: Sort u_1

p: α → Prop

a, b: { y // p y }

HEq a b ↔ HEq ↑a ↑bheq_iff_eq: ∀ {α : Sort ?u.3414} {a b : α}, HEq a b ↔ a = b
heq_iff_eq,α✝: Sort ?u.3070

β: Sort ?u.3073

γ: Sort ?u.3076

p✝, q: α✝ → Prop

α: Sort u_1

p: α → Prop

a, b: { y // p y }

a = b ↔ HEq ↑a ↑b α✝: Sort ?u.3070

β: Sort ?u.3073

γ: Sort ?u.3076

p✝, q: α✝ → Prop

α: Sort u_1

p: α → Prop

a, b: { y // p y }

HEq a b ↔ HEq ↑a ↑bheq_iff_eq: ∀ {α : Sort ?u.3433} {a b : α}, HEq a b ↔ a = b
heq_iff_eq,α✝: Sort ?u.3070

β: Sort ?u.3073

γ: Sort ?u.3076

p✝, q: α✝ → Prop

α: Sort u_1

p: α → Prop

a, b: { y // p y }

a = b ↔ ↑a = ↑b α✝: Sort ?u.3070

β: Sort ?u.3073

γ: Sort ?u.3076

p✝, q: α✝ → Prop

α: Sort u_1

p: α → Prop

a, b: { y // p y }

HEq a b ↔ HEq ↑a ↑bext_iff: ∀ {α : Sort ?u.3442} {p : α → Prop} {a1 a2 : { x // p x }}, a1 = a2 ↔ ↑a1 = ↑a2
ext_iffα✝: Sort ?u.3070

β: Sort ?u.3073

γ: Sort ?u.3076

p✝, q: α✝ → Prop

α: Sort u_1

p: α → Prop

a, b: { y // p y }

↑a = ↑b ↔ ↑a = ↑b]
Goals accomplished! 🐙
#align subtype.heq_iff_coe_heq Subtype.heq_iff_coe_heq: ∀ {α β : Sort u_1} {p : α → Prop} {q : β → Prop} {a : { x // p x }} {b : { y // q y }},
  α = β → HEq p q → (HEq a b ↔ HEq ↑a ↑b)
Subtype.heq_iff_coe_heq

theorem ext_val: ∀ {α : Sort u_1} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2
ext_val {a1: { x // p x }
a1 a2: { x // p x }
a2 : { x: ?m.3530
x // p: α → Prop
p x: ?m.3521
x }} : a1: { x // p x }
a1.1: {α : Sort ?u.3537} → {p : α → Prop} → Subtype p → α
1 = a2: { x // p x }
a2.1: {α : Sort ?u.3544} → {p : α → Prop} → Subtype p → α
1 → a1: { x // p x }
a1 = a2: { x // p x }
a2 :=
  Subtype.ext: ∀ {α : Sort ?u.3555} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2
Subtype.ext
#align subtype.ext_val Subtype.ext_val: ∀ {α : Sort u_1} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2
Subtype.ext_val

theorem ext_iff_val: ∀ {α : Sort u_1} {p : α → Prop} {a1 a2 : { x // p x }}, a1 = a2 ↔ ↑a1 = ↑a2
ext_iff_val {a1: { x // p x }
a1 a2: { x // p x }
a2 : { x: ?m.3605
x // p: α → Prop
p x: ?m.3614
x }} : a1: { x // p x }
a1 = a2: { x // p x }
a2 ↔ a1: { x // p x }
a1.1: {α : Sort ?u.3625} → {p : α → Prop} → Subtype p → α
1 = a2: { x // p x }
a2.1: {α : Sort ?u.3629} → {p : α → Prop} → Subtype p → α
1 :=
  ext_iff: ∀ {α : Sort ?u.3637} {p : α → Prop} {a1 a2 : { x // p x }}, a1 = a2 ↔ ↑a1 = ↑a2
ext_iff
#align subtype.ext_iff_val Subtype.ext_iff_val: ∀ {α : Sort u_1} {p : α → Prop} {a1 a2 : { x // p x }}, a1 = a2 ↔ ↑a1 = ↑a2
Subtype.ext_iff_val

@[simp]
theorem coe_eta: ∀ {α : Sort u_1} {p : α → Prop} (a : { a // p a }) (h : p ↑a), { val := ↑a, property := h } = a
coe_eta (a: { a // p a }
a : { a: ?m.3682
a // p: α → Prop
p a: ?m.3682
a }) (h: p ↑a
h : p: α → Prop
p a: { a // p a }
a) : mk: {α : Sort ?u.3812} → {p : α → Prop} → (val : α) → p val → Subtype p
mk (↑a: { a // p a }
a) h: p ↑a
h = a: { a // p a }
a :=
  Subtype.ext: ∀ {α : Sort ?u.3840} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2
Subtype.ext rfl: ∀ {α : Sort ?u.3857} {a : α}, a = a
rfl
#align subtype.coe_eta Subtype.coe_eta: ∀ {α : Sort u_1} {p : α → Prop} (a : { a // p a }) (h : p ↑a), { val := ↑a, property := h } = a
Subtype.coe_eta

theorem coe_mk: ∀ (a : α) (h : p a), ↑{ val := a, property := h } = a
coe_mk (a: α
a h: p a
h) : (@mk: {α : Sort ?u.3909} → {p : α → Prop} → (val : α) → p val → Subtype p
mk α: Sort ?u.3884
α p: α → Prop
p a: ?m.3901
a h: ?m.3904
h : α: Sort ?u.3884
α) = a: ?m.3901
a :=
  rfl: ∀ {α : Sort ?u.4028} {a : α}, a = a
rfl
#align subtype.coe_mk Subtype.coe_mk: ∀ {α : Sort u_1} {p : α → Prop} (a : α) (h : p a), ↑{ val := a, property := h } = a
Subtype.coe_mk

-- Porting note: comment out `@[simp, nolint simp_nf]`
-- Porting note: not clear if "built-in reduction doesn't always work" is still relevant
-- built-in reduction doesn't always work
-- @[simp, nolint simp_nf]
theorem mk_eq_mk: ∀ {α : Sort u_1} {p : α → Prop} {a : α} {h : p a} {a' : α} {h' : p a'},
  { val := a, property := h } = { val := a', property := h' } ↔ a = a'
mk_eq_mk {a: ?m.4057
a h: ?m.4060
h a': α
a' h': ?m.4066
h'} : @mk: {α : Sort ?u.4070} → {p : α → Prop} → (val : α) → p val → Subtype p
mk α: Sort ?u.4040
α p: α → Prop
p a: ?m.4057
a h: ?m.4060
h = @mk: {α : Sort ?u.4072} → {p : α → Prop} → (val : α) → p val → Subtype p
mk α: Sort ?u.4040
α p: α → Prop
p a': ?m.4063
a' h': ?m.4066
h' ↔ a: ?m.4057
a = a': ?m.4063
a' :=
  ext_iff: ∀ {α : Sort ?u.4085} {p : α → Prop} {a1 a2 : { x // p x }}, a1 = a2 ↔ ↑a1 = ↑a2
ext_iff
#align subtype.mk_eq_mk Subtype.mk_eq_mk: ∀ {α : Sort u_1} {p : α → Prop} {a : α} {h : p a} {a' : α} {h' : p a'},
  { val := a, property := h } = { val := a', property := h' } ↔ a = a'
Subtype.mk_eq_mk

theorem coe_eq_of_eq_mk: ∀ {α : Sort u_1} {p : α → Prop} {a : { a // p a }} {b : α} (h : ↑a = b), a = { val := b, property := (_ : p b) }
coe_eq_of_eq_mk {a: { a // p a }
a : { a: ?m.4136
a // p: α → Prop
p a: ?m.4136
a }} {b: α
b : α: Sort ?u.4116
α} (h: ?m.4147 = b
h : ↑a: { a // p a }
a = b: α
b) : a: { a // p a }
a = ⟨b: α
b, h: ?m.4147 = b
h ▸ a: { a // p a }
a.2: ∀ {α : Sort ?u.4285} {p : α → Prop} (self : Subtype p), p ↑self
2⟩ :=
  Subtype.ext: ∀ {α : Sort ?u.4300} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2
Subtype.ext h: ↑a = b
h
#align subtype.coe_eq_of_eq_mk Subtype.coe_eq_of_eq_mk: ∀ {α : Sort u_1} {p : α → Prop} {a : { a // p a }} {b : α} (h : ↑a = b), a = { val := b, property := (_ : p b) }
Subtype.coe_eq_of_eq_mk

theorem coe_eq_iff: ∀ {a : { a // p a }} {b : α}, ↑a = b ↔ ∃ h, a = { val := b, property := h }
coe_eq_iff {a: { a // p a }
a : { a: ?m.4348
a // p: α → Prop
p a: ?m.4348
a }} {b: α
b : α: Sort ?u.4328
α} : ↑a: { a // p a }
a = b: α
b ↔ ∃ h: ?m.4485
h, a: { a // p a }
a = ⟨b: α
b, h: ?m.4485
h⟩ :=
  ⟨fun h: ?m.4514
h ↦ h: ?m.4514
h ▸ ⟨a: { a // p a }
a.2: ∀ {α : Sort ?u.4528} {p : α → Prop} (self : Subtype p), p ↑self
2, (coe_eta: ∀ {α : Sort ?u.4535} {p : α → Prop} (a : { a // p a }) (h : p ↑a), { val := ↑a, property := h } = a
coe_eta _: { a // ?m.4537 a }
_ _: ?m.4537 ↑?m.4538
_).symm: ∀ {α : Sort ?u.4540} {a b : α}, a = b → b = a
symm⟩, fun ⟨_, ha: a = { val := b, property := w✝ }
ha⟩ ↦ ha: a = { val := b, property := w✝ }
ha.symm: ∀ {α : Sort ?u.4619} {a b : α}, a = b → b = a
symm ▸ rfl: ∀ {α : Sort ?u.4627} {a : α}, a = a
rfl⟩
#align subtype.coe_eq_iff Subtype.coe_eq_iff: ∀ {α : Sort u_1} {p : α → Prop} {a : { a // p a }} {b : α}, ↑a = b ↔ ∃ h, a = { val := b, property := h }
Subtype.coe_eq_iff

theorem coe_injective: Injective fun a => ↑a
coe_injective : Injective: {α : Sort ?u.4749} → {β : Sort ?u.4748} → (α → β) → Prop
Injective (fun (a: Subtype p
a : Subtype: {α : Sort ?u.4753} → (α → Prop) → Sort (max1?u.4753)
Subtype p: α → Prop
p) ↦ (a: Subtype p
a : α: Sort ?u.4731
α)) := fun _: ?m.4883
_ _: ?m.4886
_ ↦ Subtype.ext: ∀ {α : Sort ?u.4888} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2
Subtype.ext
#align subtype.coe_injective Subtype.coe_injective: ∀ {α : Sort u_1} {p : α → Prop}, Injective fun a => ↑a
Subtype.coe_injective

theorem val_injective: Injective val
val_injective : Injective: {α : Sort ?u.4943} → {β : Sort ?u.4942} → (α → β) → Prop
Injective (@val: {α : Sort ?u.4946} → {p : α → Prop} → Subtype p → α
val _: Sort ?u.4946
_ p: α → Prop
p) :=
  coe_injective: ∀ {α : Sort ?u.4957} {p : α → Prop}, Injective fun a => ↑a
coe_injective
#align subtype.val_injective Subtype.val_injective: ∀ {α : Sort u_1} {p : α → Prop}, Injective val
Subtype.val_injective

theorem coe_inj: ∀ {α : Sort u_1} {p : α → Prop} {a b : Subtype p}, ↑a = ↑b ↔ a = b
coe_inj {a: Subtype p
a b: Subtype p
b : Subtype: {α : Sort ?u.4990} → (α → Prop) → Sort (max1?u.4990)
Subtype p: α → Prop
p} : (a: Subtype p
a : α: Sort ?u.4973
α) = b: Subtype p
b ↔ a: Subtype p
a = b: Subtype p
b :=
  coe_injective: ∀ {α : Sort ?u.5302} {p : α → Prop}, Injective fun a => ↑a
coe_injective.eq_iff: ∀ {α : Sort ?u.5305} {β : Sort ?u.5306} {f : α → β}, Injective f → ∀ {a b : α}, f a = f b ↔ a = b
eq_iff
#align subtype.coe_inj Subtype.coe_inj: ∀ {α : Sort u_1} {p : α → Prop} {a b : Subtype p}, ↑a = ↑b ↔ a = b
Subtype.coe_inj

theorem val_inj: ∀ {a b : Subtype p}, ↑a = ↑b ↔ a = b
val_inj {a: Subtype p
a b: Subtype p
b : Subtype: {α : Sort ?u.5361} → (α → Prop) → Sort (max1?u.5361)
Subtype p: α → Prop
p} : a: Subtype p
a.val: {α : Sort ?u.5376} → {p : α → Prop} → Subtype p → α
val = b: Subtype p
b.val: {α : Sort ?u.5383} → {p : α → Prop} → Subtype p → α
val ↔ a: Subtype p
a = b: Subtype p
b :=
  coe_inj: ∀ {α : Sort ?u.5393} {p : α → Prop} {a b : Subtype p}, ↑a = ↑b ↔ a = b
coe_inj
#align subtype.val_inj Subtype.val_inj: ∀ {α : Sort u_1} {p : α → Prop} {a b : Subtype p}, ↑a = ↑b ↔ a = b
Subtype.val_inj

-- Porting note: it is unclear why the linter doesn't like this.
-- If you understand why, please replace this comment with an explanation, or resolve.
@[simp, nolint simpNF: Std.Tactic.Lint.Linter
simpNF]
theorem _root_.exists_eq_subtype_mk_iff: ∀ {a : Subtype p} {b : α}, (∃ h, a = { val := b, property := h }) ↔ ↑a = b
_root_.exists_eq_subtype_mk_iff {a: Subtype p
a : Subtype: {α : Sort ?u.5437} → (α → Prop) → Sort (max1?u.5437)
Subtype p: α → Prop
p} {b: α
b : α: Sort ?u.5420
α} :
    (∃ h: p b
h : p: α → Prop
p b: α
b, a: Subtype p
a = Subtype.mk: {α : Sort ?u.5451} → {p : α → Prop} → (val : α) → p val → Subtype p
Subtype.mk b: α
b h: p b
h) ↔ ↑a: Subtype p
a = b: α
b :=
  coe_eq_iff: ∀ {α : Sort ?u.5585} {p : α → Prop} {a : { a // p a }} {b : α}, ↑a = b ↔ ∃ h, a = { val := b, property := h }
coe_eq_iff.symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)
symm
#align exists_eq_subtype_mk_iff exists_eq_subtype_mk_iff: ∀ {α : Sort u_1} {p : α → Prop} {a : Subtype p} {b : α}, (∃ h, a = { val := b, property := h }) ↔ ↑a = b
exists_eq_subtype_mk_iff

-- Porting note: it is unclear why the linter doesn't like this.
-- If you understand why, please replace this comment with an explanation, or resolve.
@[simp, nolint simpNF: Std.Tactic.Lint.Linter
simpNF]
theorem _root_.exists_subtype_mk_eq_iff: ∀ {α : Sort u_1} {p : α → Prop} {a : Subtype p} {b : α}, (∃ h, { val := b, property := h } = a) ↔ b = ↑a
_root_.exists_subtype_mk_eq_iff {a: Subtype p
a : Subtype: {α : Sort ?u.5661} → (α → Prop) → Sort (max1?u.5661)
Subtype p: α → Prop
p} {b: α
b : α: Sort ?u.5644
α} :
    (∃ h: p b
h : p: α → Prop
p b: α
b, Subtype.mk: {α : Sort ?u.5675} → {p : α → Prop} → (val : α) → p val → Subtype p
Subtype.mk b: α
b h: p b
h = a: Subtype p
a) ↔ b: α
b = a: Subtype p
a := by
Goals accomplished! 🐙
  α: Sort u_1

β: Sort ?u.5647

γ: Sort ?u.5650

p, q: α → Prop

a: Subtype p

b: α

(∃ h, { val := b, property := h } = a) ↔ b = ↑asimp only [@eq_comm: ∀ {α : Sort ?u.5906} {a b : α}, a = b ↔ b = a
eq_comm _: Sort ?u.5906
_ b: α
b, exists_eq_subtype_mk_iff: ∀ {α : Sort ?u.5913} {p : α → Prop} {a : Subtype p} {b : α}, (∃ h, a = { val := b, property := h }) ↔ ↑a = b
exists_eq_subtype_mk_iff, @eq_comm: ∀ {α : Sort ?u.5933} {a b : α}, a = b ↔ b = a
eq_comm _: Sort ?u.5933
_ _: ?m.5934
_ a: Subtype p
a]
Goals accomplished! 🐙
#align exists_subtype_mk_eq_iff exists_subtype_mk_eq_iff: ∀ {α : Sort u_1} {p : α → Prop} {a : Subtype p} {b : α}, (∃ h, { val := b, property := h } = a) ↔ b = ↑a
exists_subtype_mk_eq_iff

/-- Restrict a (dependent) function to a subtype -/
def restrict: {α : Sort ?u.6133} → {β : α → Type ?u.6135} → (p : α → Prop) → ((x : α) → β x) → (x : Subtype p) → β ↑x
restrict {α: Sort ?u.6133
α} {β: α → Type ?u.6135
β : α: ?m.6130
α → Type _: Type (?u.6135+1)
Type _} (p: α → Prop
p : α: ?m.6130
α → Prop: Type
Prop) (f: (x : α) → β x
f : ∀ x: ?m.6143
x, β: α → Type ?u.6135
β x: ?m.6143
x) (x: Subtype p
x : Subtype: {α : Sort ?u.6148} → (α → Prop) → Sort (max1?u.6148)
Subtype p: α → Prop
p) : β: α → Type ?u.6135
β x: Subtype p
x.1: {α : Sort ?u.6155} → {p : α → Prop} → Subtype p → α
1 :=
  f: (x : α) → β x
f x: Subtype p
x
#align subtype.restrict Subtype.restrict: {α : Sort u_1} → {β : α → Type u_2} → (p : α → Prop) → ((x : α) → β x) → (x : Subtype p) → β ↑x
Subtype.restrict

theorem restrict_apply: ∀ {α : Sort u_1} {β : α → Type u_2} (f : (x : α) → β x) (p : α → Prop) (x : Subtype p), restrict p f x = f ↑x
restrict_apply {α: ?m.6419
α} {β: α → Type ?u.6424
β : α: ?m.6419
α → Type _: Type (?u.6424+1)
Type _} (f: (x : α) → β x
f : ∀ x: ?m.6428
x, β: α → Type ?u.6424
β x: ?m.6428
x) (p: α → Prop
p : α: ?m.6419
α → Prop: Type
Prop) (x: Subtype p
x : Subtype: {α : Sort ?u.6437} → (α → Prop) → Sort (max1?u.6437)
Subtype p: α → Prop
p) :
    restrict: {α : Sort ?u.6446} → {β : α → Type ?u.6445} → (p : α → Prop) → ((x : α) → β x) → (x : Subtype p) → β ↑x
restrict p: α → Prop
p f: (x : α) → β x
f x: Subtype p
x = f: (x : α) → β x
f x: Subtype p
x.1: {α : Sort ?u.6460} → {p : α → Prop} → Subtype p → α
1 := by
Goals accomplished! 🐙
  α✝: Sort ?u.6402

β✝: Sort ?u.6405

γ: Sort ?u.6408

p✝, q: α✝ → Prop

α: Sort u_1

β: α → Type u_2

f: (x : α) → β x

p: α → Prop

x: Subtype p

restrict p f x = f ↑xrfl
Goals accomplished! 🐙
#align subtype.restrict_apply Subtype.restrict_apply: ∀ {α : Sort u_1} {β : α → Type u_2} (f : (x : α) → β x) (p : α → Prop) (x : Subtype p), restrict p f x = f ↑x
Subtype.restrict_apply

theorem restrict_def: ∀ {α : Sort u_1} {β : Type u_2} (f : α → β) (p : α → Prop), restrict p f = f ∘ fun a => ↑a
restrict_def {α: ?m.6505
α β: Type u_2
β} (f: α → β
f : α: ?m.6505
α → β: ?m.6508
β) (p: α → Prop
p : α: ?m.6505
α → Prop: Type
Prop) :
  restrict: {α : Sort ?u.6521} → {β : α → Type ?u.6520} → (p : α → Prop) → ((x : α) → β x) → (x : Subtype p) → β ↑x
restrict p: α → Prop
p f: α → β
f = f: α → β
f ∘ (fun (a: Subtype p
a : Subtype: {α : Sort ?u.6543} → (α → Prop) → Sort (max1?u.6543)
Subtype p: α → Prop
p) ↦ a: Subtype p
a) := rfl: ∀ {α : Sort ?u.6679} {a : α}, a = a
rfl
#align subtype.restrict_def Subtype.restrict_def: ∀ {α : Sort u_1} {β : Type u_2} (f : α → β) (p : α → Prop), restrict p f = f ∘ fun a => ↑a
Subtype.restrict_def

theorem restrict_injective: ∀ {α : Sort u_1} {β : Type u_2} {f : α → β} (p : α → Prop), Injective f → Injective (restrict p f)
restrict_injective {α: ?m.6716
α β: Type u_2
β} {f: α → β
f : α: ?m.6716
α → β: ?m.6719
β} (p: α → Prop
p : α: ?m.6716
α → Prop: Type
Prop) (h: Injective f
h : Injective: {α : Sort ?u.6731} → {β : Sort ?u.6730} → (α → β) → Prop
Injective f: α → β
f) :
    Injective: {α : Sort ?u.6740} → {β : Sort ?u.6739} → (α → β) → Prop
Injective (restrict: {α : Sort ?u.6744} → {β : α → Type ?u.6743} → (p : α → Prop) → ((x : α) → β x) → (x : Subtype p) → β ↑x
restrict p: α → Prop
p f: α → β
f) :=
  h: Injective f
h.comp: ∀ {α : Sort ?u.6776} {β : Sort ?u.6775} {φ : Sort ?u.6774} {g : β → φ} {f : α → β},
  Injective g → Injective f → Injective (g ∘ f)
comp coe_injective: ∀ {α : Sort ?u.6808} {p : α → Prop}, Injective fun a => ↑a
coe_injective
#align subtype.restrict_injective Subtype.restrict_injective: ∀ {α : Sort u_1} {β : Type u_2} {f : α → β} (p : α → Prop), Injective f → Injective (restrict p f)
Subtype.restrict_injective

theorem surjective_restrict: ∀ {α : Sort u_1} {β : α → Type u_2} [ne : ∀ (a : α), Nonempty (β a)] (p : α → Prop), Surjective fun f => restrict p f
surjective_restrict {α: ?m.6848
α} {β: α → Type ?u.6853
β : α: ?m.6848
α → Type _: Type (?u.6853+1)
Type _} [ne: ∀ (a : α), Nonempty (β a)
ne : ∀ a: ?m.6857
a, Nonempty: Sort ?u.6860 → Prop
Nonempty (β: α → Type ?u.6853
β a: ?m.6857
a)] (p: α → Prop
p : α: ?m.6848
α → Prop: Type
Prop) :
    Surjective: {α : Sort ?u.6869} → {β : Sort ?u.6868} → (α → β) → Prop
Surjective fun f: (x : α) → β x
f : ∀ x: ?m.6874
x, β: α → Type ?u.6853
β x: ?m.6874
x ↦ restrict: {α : Sort ?u.6880} → {β : α → Type ?u.6879} → (p : α → Prop) → ((x : α) → β x) → (x : Subtype p) → β ↑x
restrict p: α → Prop
p f: (x : α) → β x
f := by
Goals accomplished! 🐙
  α✝: Sort ?u.6831

β✝: Sort ?u.6834

γ: Sort ?u.6837

p✝, q: α✝ → Prop

α: Sort u_1

β: α → Type u_2

ne: ∀ (a : α), Nonempty (β a)

p: α → Prop

Surjective fun f => restrict p fletI := Classical.decPred: {α : Sort ?u.6918} → (p : α → Prop) → DecidablePred p
Classical.decPred p: α → Prop
pα✝: Sort ?u.6831

β✝: Sort ?u.6834

γ: Sort ?u.6837

p✝, q: α✝ → Prop

α: Sort u_1

β: α → Type u_2

ne: ∀ (a : α), Nonempty (β a)

p: α → Prop

this:= Classical.decPred p: DecidablePred p

Surjective fun f => restrict p f
  α✝: Sort ?u.6831

β✝: Sort ?u.6834

γ: Sort ?u.6837

p✝, q: α✝ → Prop

α: Sort u_1

β: α → Type u_2

ne: ∀ (a : α), Nonempty (β a)

p: α → Prop

Surjective fun f => restrict p frefine' fun f: ?m.6929
f ↦ ⟨fun x: ?m.6946
x ↦ if h: ?m.6959
h : p: α → Prop
p x: ?m.6946
x then f: ?m.6929
f ⟨x: ?m.6946
x, h: ?m.6959
h⟩ else Nonempty.some: {α : Sort ?u.6978} → Nonempty α → α
Nonempty.some (ne: ∀ (a : α), Nonempty (β a)
ne x: ?m.6946
x), funext: ∀ {α : Sort ?u.6986} {β : α → Sort ?u.6985} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext <| _: ∀ (x : ?m.6987), ?m.6989 x = ?m.6990 x
_⟩α✝: Sort ?u.6831

β✝: Sort ?u.6834

γ: Sort ?u.6837

p✝, q: α✝ → Prop

α: Sort u_1

β: α → Type u_2

ne: ∀ (a : α), Nonempty (β a)

p: α → Prop

this:= Classical.decPred p: DecidablePred p

f: (x : Subtype p) → β ↑x

∀ (x : Subtype p),
  (fun f => restrict p f)
      (fun x => if h : p x then f { val := x, property := h } else Nonempty.some (_ : Nonempty (β x))) x =     f x
  α✝: Sort ?u.6831

β✝: Sort ?u.6834

γ: Sort ?u.6837

p✝, q: α✝ → Prop

α: Sort u_1

β: α → Type u_2

ne: ∀ (a : α), Nonempty (β a)

p: α → Prop

Surjective fun f => restrict p frintro ⟨x, hx⟩: ?m.6987
⟨x: α
x⟨x, hx⟩: ?m.6987
, hx: p x
hx⟨x, hx⟩: ?m.6987
⟩α✝: Sort ?u.6831

β✝: Sort ?u.6834

γ: Sort ?u.6837

p✝, q: α✝ → Prop

α: Sort u_1

β: α → Type u_2

ne: ∀ (a : α), Nonempty (β a)

p: α → Prop

this:= Classical.decPred p: DecidablePred p

f: (x : Subtype p) → β ↑x

x: α

hx: p x

mk(fun f => restrict p f) (fun x => if h : p x then f { val := x, property := h } else Nonempty.some (_ : Nonempty (β x)))
    { val := x, property := hx } =   f { val := x, property := hx }
  α✝: Sort ?u.6831

β✝: Sort ?u.6834

γ: Sort ?u.6837

p✝, q: α✝ → Prop

α: Sort u_1

β: α → Type u_2

ne: ∀ (a : α), Nonempty (β a)

p: α → Prop

Surjective fun f => restrict p fexact dif_pos: ∀ {c : Prop} {h : Decidable c} (hc : c) {α : Sort ?u.7032} {t : c → α} {e : ¬c → α}, dite c t e = t hc
dif_pos hx: p x
hx
Goals accomplished! 🐙
#align subtype.surjective_restrict Subtype.surjective_restrict: ∀ {α : Sort u_1} {β : α → Type u_2} [ne : ∀ (a : α), Nonempty (β a)] (p : α → Prop), Surjective fun f => restrict p f
Subtype.surjective_restrict

/-- Defining a map into a subtype, this can be seen as an "coinduction principle" of `Subtype`-/
@[simps: ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β) {p : β → Prop} (h : ∀ (a : α), p (f a)) (a : α), ↑(coind f h a) = f a
simps]
def coind: {α : Sort ?u.7124} → {β : Sort ?u.7125} → (f : α → β) → {p : β → Prop} → (∀ (a : α), p (f a)) → α → Subtype p
coind {α: Sort ?u.7124
α β: ?m.7121
β} (f: α → β
f : α: ?m.7118
α → β: ?m.7121
β) {p: β → Prop
p : β: ?m.7121
β → Prop: Type
Prop} (h: ∀ (a : α), p (f a)
h : ∀ a: ?m.7133
a, p: β → Prop
p (f: α → β
f a: ?m.7133
a)) : α: ?m.7118
α → Subtype: {α : Sort ?u.7140} → (α → Prop) → Sort (max1?u.7140)
Subtype p: β → Prop
p := fun a: ?m.7152
a ↦ ⟨f: α → β
f a: ?m.7152
a, h: ∀ (a : α), p (f a)
h a: ?m.7152
a⟩
#align subtype.coind Subtype.coind: {α : Sort u_1} → {β : Sort u_2} → (f : α → β) → {p : β → Prop} → (∀ (a : α), p (f a)) → α → Subtype p
Subtype.coind
#align subtype.coind_coe Subtype.coind_coe: ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β) {p : β → Prop} (h : ∀ (a : α), p (f a)) (a : α), ↑(coind f h a) = f a
Subtype.coind_coe

theorem coind_injective: ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : β → Prop} (h : ∀ (a : α), p (f a)), Injective f → Injective (coind f h)
coind_injective {α: ?m.7297
α β: Sort u_2
β} {f: α → β
f : α: ?m.7297
α → β: ?m.7300
β} {p: β → Prop
p : β: ?m.7300
β → Prop: Type
Prop} (h: ∀ (a : α), p (f a)
h : ∀ a: ?m.7312
a, p: β → Prop
p (f: α → β
f a: ?m.7312
a)) (hf: Injective f
hf : Injective: {α : Sort ?u.7318} → {β : Sort ?u.7317} → (α → β) → Prop
Injective f: α → β
f) :
    Injective: {α : Sort ?u.7327} → {β : Sort ?u.7326} → (α → β) → Prop
Injective (coind: {α : Sort ?u.7331} → {β : Sort ?u.7330} → (f : α → β) → {p : β → Prop} → (∀ (a : α), p (f a)) → α → Subtype p
coind f: α → β
f h: ∀ (a : α), p (f a)
h) := fun x: ?m.7364
x y: ?m.7367
y hxy: ?m.7370
hxy ↦ hf: Injective f
hf <| by
Goals accomplished! 🐙 α✝: Sort ?u.7280

β✝: Sort ?u.7283

γ: Sort ?u.7286

p✝, q: α✝ → Prop

α: Sort u_1

β: Sort u_2

f: α → β

p: β → Prop

h: ∀ (a : α), p (f a)

hf: Injective f

x, y: α

hxy: coind f h x = coind f h y

f x = f yapply congr_arg: ∀ {α : Sort ?u.7384} {β : Sort ?u.7383} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg Subtype.val: {α : Sort ?u.7389} → {p : α → Prop} → Subtype p → α
Subtype.val hxy: coind f h x = coind f h y
hxy
Goals accomplished! 🐙
#align subtype.coind_injective Subtype.coind_injective: ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : β → Prop} (h : ∀ (a : α), p (f a)), Injective f → Injective (coind f h)
Subtype.coind_injective

theorem coind_surjective: ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : β → Prop} (h : ∀ (a : α), p (f a)),
  Surjective f → Surjective (coind f h)
coind_surjective {α: ?m.7438
α β: Sort u_2
β} {f: α → β
f : α: ?m.7438
α → β: ?m.7441
β} {p: β → Prop
p : β: ?m.7441
β → Prop: Type
Prop} (h: ∀ (a : α), p (f a)
h : ∀ a: ?m.7453
a, p: β → Prop
p (f: α → β
f a: ?m.7453
a)) (hf: Surjective f
hf : Surjective: {α : Sort ?u.7459} → {β : Sort ?u.7458} → (α → β) → Prop
Surjective f: α → β
f) :
    Surjective: {α : Sort ?u.7469} → {β : Sort ?u.7468} → (α → β) → Prop
Surjective (coind: {α : Sort ?u.7473} → {β : Sort ?u.7472} → (f : α → β) → {p : β → Prop} → (∀ (a : α), p (f a)) → α → Subtype p
coind f: α → β
f h: ∀ (a : α), p (f a)
h) := fun x: ?m.7509
x ↦
  let ⟨a: α
a, ha: f a = ↑x
ha⟩ := hf: Surjective f
hf x: ?m.7509
x
  ⟨a: α
a, coe_injective: ∀ {α : Sort ?u.7665} {p : α → Prop}, Injective fun a => ↑a
coe_injective ha: f a = ↑x
ha⟩
#align subtype.coind_surjective Subtype.coind_surjective: ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : β → Prop} (h : ∀ (a : α), p (f a)),
  Surjective f → Surjective (coind f h)
Subtype.coind_surjective

theorem coind_bijective: ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : β → Prop} (h : ∀ (a : α), p (f a)), Bijective f → Bijective (coind f h)
coind_bijective {α: ?m.7785
α β: Sort u_2
β} {f: α → β
f : α: ?m.7785
α → β: ?m.7788
β} {p: β → Prop
p : β: ?m.7788
β → Prop: Type
Prop} (h: ∀ (a : α), p (f a)
h : ∀ a: ?m.7800
a, p: β → Prop
p (f: α → β
f a: ?m.7800
a)) (hf: Bijective f
hf : Bijective: {α : Sort ?u.7806} → {β : Sort ?u.7805} → (α → β) → Prop
Bijective f: α → β
f) :
    Bijective: {α : Sort ?u.7815} → {β : Sort ?u.7814} → (α → β) → Prop
Bijective (coind: {α : Sort ?u.7819} → {β : Sort ?u.7818} → (f : α → β) → {p : β → Prop} → (∀ (a : α), p (f a)) → α → Subtype p
coind f: α → β
f h: ∀ (a : α), p (f a)
h) :=
  ⟨coind_injective: ∀ {α : Sort ?u.7859} {β : Sort ?u.7860} {f : α → β} {p : β → Prop} (h : ∀ (a : α), p (f a)),
  Injective f → Injective (coind f h)
coind_injective h: ∀ (a : α), p (f a)
h hf: Bijective f
hf.1: ∀ {a b : Prop}, a ∧ b → a
1, coind_surjective: ∀ {α : Sort ?u.7892} {β : Sort ?u.7893} {f : α → β} {p : β → Prop} (h : ∀ (a : α), p (f a)),
  Surjective f → Surjective (coind f h)
coind_surjective h: ∀ (a : α), p (f a)
h hf: Bijective f
hf.2: ∀ {a b : Prop}, a ∧ b → b
2⟩
#align subtype.coind_bijective Subtype.coind_bijective: ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : β → Prop} (h : ∀ (a : α), p (f a)), Bijective f → Bijective (coind f h)
Subtype.coind_bijective

/-- Restriction of a function to a function on subtypes. -/
@[simps: ∀ {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ (a : α), p a → q (f a))
  (a : Subtype p), ↑(map f h a) = f ↑a
simps]
def map: {p : α → Prop} → {q : β → Prop} → (f : α → β) → (∀ (a : α), p a → q (f a)) → Subtype p → Subtype q
map {p: α → Prop
p : α: Sort ?u.7927
α → Prop: Type
Prop} {q: β → Prop
q : β: Sort ?u.7930
β → Prop: Type
Prop} (f: α → β
f : α: Sort ?u.7927
α → β: Sort ?u.7930
β) (h: ∀ (a : α), p a → q (f a)
h : ∀ a: ?m.7957
a, p: α → Prop
p a: ?m.7957
a → q: β → Prop
q (f: α → β
f a: ?m.7957
a)) :
    Subtype: {α : Sort ?u.7965} → (α → Prop) → Sort (max1?u.7965)
Subtype p: α → Prop
p → Subtype: {α : Sort ?u.7971} → (α → Prop) → Sort (max1?u.7971)
Subtype q: β → Prop
q :=
  fun x: ?m.7982
x ↦ ⟨f: α → β
f x: ?m.7982
x, h: ∀ (a : α), p a → q (f a)
h x: ?m.7982
x x: ?m.7982
x.prop: ∀ {α : Sort ?u.8108} {p : α → Prop} (x : Subtype p), p ↑x
prop⟩
#align subtype.map Subtype.map: {α : Sort u_1} →
  {β : Sort u_2} → {p : α → Prop} → {q : β → Prop} → (f : α → β) → (∀ (a : α), p a → q (f a)) → Subtype p → Subtype q
Subtype.map
#align subtype.map_coe Subtype.map_coe: ∀ {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ (a : α), p a → q (f a))
  (a : Subtype p), ↑(map f h a) = f ↑a
Subtype.map_coe

theorem map_comp: ∀ {α : Sort u_1} {β : Sort u_3} {γ : Sort u_2} {p : α → Prop} {q : β → Prop} {r : γ → Prop} {x : Subtype p} (f : α → β)
  (h : ∀ (a : α), p a → q (f a)) (g : β → γ) (l : ∀ (a : β), q a → r (g a)),
  map g l (map f h x) = map (g ∘ f) (_ : ∀ (a : α), p a → r (g (f a))) x
map_comp {p: α → Prop
p : α: Sort ?u.8288
α → Prop: Type
Prop} {q: β → Prop
q : β: Sort ?u.8291
β → Prop: Type
Prop} {r: γ → Prop
r : γ: Sort ?u.8294
γ → Prop: Type
Prop} {x: Subtype p
x : Subtype: {α : Sort ?u.8317} → (α → Prop) → Sort (max1?u.8317)
Subtype p: α → Prop
p}
    (f: α → β
f : α: Sort ?u.8288
α → β: Sort ?u.8291
β) (h: ∀ (a : α), p a → q (f a)
h : ∀ a: ?m.8329
a, p: α → Prop
p a: ?m.8329
a → q: β → Prop
q (f: α → β
f a: ?m.8329
a)) (g: β → γ
g : β: Sort ?u.8291
β → γ: Sort ?u.8294
γ) (l: ∀ (a : β), q a → r (g a)
l : ∀ a: ?m.8341
a, q: β → Prop
q a: ?m.8341
a → r: γ → Prop
r (g: β → γ
g a: ?m.8341
a)) :
    map: {α : Sort ?u.8350} →
  {β : Sort ?u.8349} →
    {p : α → Prop} → {q : β → Prop} → (f : α → β) → (∀ (a : α), p a → q (f a)) → Subtype p → Subtype q
map g: β → γ
g l: ∀ (a : β), q a → r (g a)
l (map: {α : Sort ?u.8368} →
  {β : Sort ?u.8367} →
    {p : α → Prop} → {q : β → Prop} → (f : α → β) → (∀ (a : α), p a → q (f a)) → Subtype p → Subtype q
map f: α → β
f h: ∀ (a : α), p a → q (f a)
h x: Subtype p
x) = map: {α : Sort ?u.8392} →
  {β : Sort ?u.8391} →
    {p : α → Prop} → {q : β → Prop} → (f : α → β) → (∀ (a : α), p a → q (f a)) → Subtype p → Subtype q
map (g: β → γ
g ∘ f: α → β
f) (fun a: ?m.8415
a ha: ?m.8418
ha ↦ l: ∀ (a : β), q a → r (g a)
l (f: α → β
f a: ?m.8415
a) <| h: ∀ (a : α), p a → q (f a)
h a: ?m.8415
a ha: ?m.8418
ha) x: Subtype p
x :=
  rfl: ∀ {α : Sort ?u.8440} {a : α}, a = a
rfl
#align subtype.map_comp Subtype.map_comp: ∀ {α : Sort u_1} {β : Sort u_3} {γ : Sort u_2} {p : α → Prop} {q : β → Prop} {r : γ → Prop} {x : Subtype p} (f : α → β)
  (h : ∀ (a : α), p a → q (f a)) (g : β → γ) (l : ∀ (a : β), q a → r (g a)),
  map g l (map f h x) = map (g ∘ f) (_ : ∀ (a : α), p a → r (g (f a))) x
Subtype.map_comp

theorem map_id: ∀ {p : α → Prop} {h : ∀ (a : α), p a → p (id a)}, map id h = id
map_id {p: α → Prop
p : α: Sort ?u.8501
α → Prop: Type
Prop} {h: ∀ (a : α), p a → p (id a)
h : ∀ a: ?m.8523
a, p: α → Prop
p a: ?m.8523
a → p: α → Prop
p (id: {α : Sort ?u.8528} → α → α
id a: ?m.8523
a)} : map: {α : Sort ?u.8534} →
  {β : Sort ?u.8533} →
    {p : α → Prop} → {q : β → Prop} → (f : α → β) → (∀ (a : α), p a → q (f a)) → Subtype p → Subtype q
map (@id: {α : Sort ?u.8539} → α → α
id α: Sort ?u.8501
α) h: ∀ (a : α), p a → p (id a)
h = id: {α : Sort ?u.8555} → α → α
id :=
  funext: ∀ {α : Sort ?u.8602} {β : α → Sort ?u.8601} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun _: ?m.8619
_ ↦ rfl: ∀ {α : Sort ?u.8621} {a : α}, a = a
rfl
#align subtype.map_id Subtype.map_id: ∀ {α : Sort u_1} {p : α → Prop} {h : ∀ (a : α), p a → p (id a)}, map id h = id
Subtype.map_id

theorem map_injective: ∀ {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} {f : α → β} (h : ∀ (a : α), p a → q (f a)),
  Injective f → Injective (map f h)
map_injective {p: α → Prop
p : α: Sort ?u.8636
α → Prop: Type
Prop} {q: β → Prop
q : β: Sort ?u.8639
β → Prop: Type
Prop} {f: α → β
f : α: Sort ?u.8636
α → β: Sort ?u.8639
β} (h: ∀ (a : α), p a → q (f a)
h : ∀ a: ?m.8666
a, p: α → Prop
p a: ?m.8666
a → q: β → Prop
q (f: α → β
f a: ?m.8666
a))
    (hf: Injective f
hf : Injective: {α : Sort ?u.8674} → {β : Sort ?u.8673} → (α → β) → Prop
Injective f: α → β
f) : Injective: {α : Sort ?u.8683} → {β : Sort ?u.8682} → (α → β) → Prop
Injective (map: {α : Sort ?u.8687} →
  {β : Sort ?u.8686} →
    {p : α → Prop} → {q : β → Prop} → (f : α → β) → (∀ (a : α), p a → q (f a)) → Subtype p → Subtype q
map f: α → β
f h: ∀ (a : α), p a → q (f a)
h) :=
  coind_injective: ∀ {α : Sort ?u.8726} {β : Sort ?u.8727} {f : α → β} {p : β → Prop} (h : ∀ (a : α), p (f a)),
  Injective f → Injective (coind f h)
coind_injective _: ∀ (a : ?m.8728), ?m.8731 (?m.8730 a)
_ <| hf: Injective f
hf.comp: ∀ {α : Sort ?u.8756} {β : Sort ?u.8755} {φ : Sort ?u.8754} {g : β → φ} {f : α → β},
  Injective g → Injective f → Injective (g ∘ f)
comp coe_injective: ∀ {α : Sort ?u.8788} {p : α → Prop}, Injective fun a => ↑a
coe_injective
#align subtype.map_injective Subtype.map_injective: ∀ {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} {f : α → β} (h : ∀ (a : α), p a → q (f a)),
  Injective f → Injective (map f h)
Subtype.map_injective

theorem map_involutive: ∀ {p : α → Prop} {f : α → α} (h : ∀ (a : α), p a → p (f a)), Involutive f → Involutive (map f h)
map_involutive {p: α → Prop
p : α: Sort ?u.8822
α → Prop: Type
Prop} {f: α → α
f : α: Sort ?u.8822
α → α: Sort ?u.8822
α} (h: ∀ (a : α), p a → p (f a)
h : ∀ a: ?m.8848
a, p: α → Prop
p a: ?m.8848
a → p: α → Prop
p (f: α → α
f a: ?m.8848
a))
    (hf: Involutive f
hf : Involutive: {α : Sort ?u.8855} → (α → α) → Prop
Involutive f: α → α
f) : Involutive: {α : Sort ?u.8862} → (α → α) → Prop
Involutive (map: {α : Sort ?u.8865} →
  {β : Sort ?u.8864} →
    {p : α → Prop} → {q : β → Prop} → (f : α → β) → (∀ (a : α), p a → q (f a)) → Subtype p → Subtype q
map f: α → α
f h: ∀ (a : α), p a → p (f a)
h) :=
  fun x: ?m.8903
x ↦ Subtype.ext: ∀ {α : Sort ?u.8905} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2
Subtype.ext (hf: Involutive f
hf x: ?m.8903
x)
#align subtype.map_involutive Subtype.map_involutive: ∀ {α : Sort u_1} {p : α → Prop} {f : α → α} (h : ∀ (a : α), p a → p (f a)), Involutive f → Involutive (map f h)
Subtype.map_involutive

instance: {α : Sort u_1} → [inst : HasEquiv α] → (p : α → Prop) → HasEquiv (Subtype p)
instance [HasEquiv: Sort ?u.9071 → Sort (max?u.9071(?u.9070+1))
HasEquiv α: Sort ?u.9053
α] (p: α → Prop
p : α: Sort ?u.9053
α → Prop: Type
Prop) : HasEquiv: Sort ?u.9079 → Sort (max?u.9079(?u.9078+1))
HasEquiv (Subtype: {α : Sort ?u.9080} → (α → Prop) → Sort (max1?u.9080)
Subtype p: α → Prop
p) :=
  ⟨fun s: ?m.9095
s t: ?m.9098
t ↦ (s: ?m.9095
s : α: Sort ?u.9053
α) ≈ (t: ?m.9098
t : α: Sort ?u.9053
α)⟩

theorem equiv_iff: ∀ [inst : HasEquiv α] {p : α → Prop} {s t : Subtype p}, s ≈ t ↔ ↑s ≈ ↑t
equiv_iff [HasEquiv: Sort ?u.9398 → Sort (max?u.9398(?u.9397+1))
HasEquiv α: Sort ?u.9380
α] {p: α → Prop
p : α: Sort ?u.9380
α → Prop: Type
Prop} {s: Subtype p
s t: Subtype p
t : Subtype: {α : Sort ?u.9405} → (α → Prop) → Sort (max1?u.9405)
Subtype p: α → Prop
p} : s: Subtype p
s ≈ t: Subtype p
t ↔ (s: Subtype p
s : α: Sort ?u.9380
α) ≈ (t: Subtype p
t : α: Sort ?u.9380
α) :=
  Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align subtype.equiv_iff Subtype.equiv_iff: ∀ {α : Sort u_1} [inst : HasEquiv α] {p : α → Prop} {s t : Subtype p}, s ≈ t ↔ ↑s ≈ ↑t
Subtype.equiv_iff

variable [Setoid: Sort ?u.9806 → Sort (max1?u.9806)
Setoid α: Sort ?u.9669
α]

protected theorem refl: ∀ (s : Subtype p), s ≈ s
refl (s: Subtype p
s : Subtype: {α : Sort ?u.9709} → (α → Prop) → Sort (max1?u.9709)
Subtype p: α → Prop
p) : s: Subtype p
s ≈ s: Subtype p
s :=
  Setoid.refl: ∀ {α : Sort ?u.9757} [inst : Setoid α] (a : α), a ≈ a
Setoid.refl _: ?m.9758
_
#align subtype.refl Subtype.refl: ∀ {α : Sort u_1} {p : α → Prop} [inst : Setoid α] (s : Subtype p), s ≈ s
Subtype.refl

protected theorem symm: ∀ {α : Sort u_1} {p : α → Prop} [inst : Setoid α] {s t : Subtype p}, s ≈ t → t ≈ s
symm {s: Subtype p
s t: Subtype p
t : Subtype: {α : Sort ?u.9816} → (α → Prop) → Sort (max1?u.9816)
Subtype p: α → Prop
p} (h: s ≈ t
h : s: Subtype p
s ≈ t: Subtype p
t) : t: Subtype p
t ≈ s: Subtype p
s :=
  Setoid.symm: ∀ {α : Sort ?u.9897} [inst : Setoid α] {a b : α}, a ≈ b → b ≈ a
Setoid.symm h: s ≈ t
h
#align subtype.symm Subtype.symm: ∀ {α : Sort u_1} {p : α → Prop} [inst : Setoid α] {s t : Subtype p}, s ≈ t → t ≈ s
Subtype.symm

protected theorem trans: ∀ {α : Sort u_1} {p : α → Prop} [inst : Setoid α] {s t u : Subtype p}, s ≈ t → t ≈ u → s ≈ u
trans {s: Subtype p
s t: Subtype p
t u: Subtype p
u : Subtype: {α : Sort ?u.9966} → (α → Prop) → Sort (max1?u.9966)
Subtype p: α → Prop
p} (h₁: s ≈ t
h₁ : s: Subtype p
s ≈ t: Subtype p
t) (h₂: t ≈ u
h₂ : t: Subtype p
t ≈ u: Subtype p
u) : s: Subtype p
s ≈ u: Subtype p
u :=
  Setoid.trans: ∀ {α : Sort ?u.10080} [inst : Setoid α] {a b c : α}, a ≈ b → b ≈ c → a ≈ c
Setoid.trans h₁: s ≈ t
h₁ h₂: t ≈ u
h₂
#align subtype.trans Subtype.trans: ∀ {α : Sort u_1} {p : α → Prop} [inst : Setoid α] {s t u : Subtype p}, s ≈ t → t ≈ u → s ≈ u
Subtype.trans

theorem equivalence: ∀ {α : Sort u_1} [inst : Setoid α] (p : α → Prop), Equivalence HasEquiv.Equiv
equivalence (p: α → Prop
p : α: Sort ?u.10122
α → Prop: Type
Prop) : Equivalence: {α : Sort ?u.10146} → (α → α → Prop) → Prop
Equivalence (@HasEquiv.Equiv: {α : Sort ?u.10149} → [self : HasEquiv α] → α → α → Sort ?u.10148
HasEquiv.Equiv (Subtype: {α : Sort ?u.10150} → (α → Prop) → Sort (max1?u.10150)
Subtype p: α → Prop
p) _) :=
  .mk: ∀ {α : Sort ?u.10188} {r : α → α → Prop},
  (∀ (x : α), r x x) → (∀ {x y : α}, r x y → r y x) → (∀ {x y z : α}, r x y → r y z → r x z) → Equivalence r
.mk (Subtype.refl: ∀ {α : Sort ?u.10197} {p : α → Prop} [inst : Setoid α] (s : Subtype p), s ≈ s
Subtype.refl) (@Subtype.symm: ∀ {α : Sort ?u.10223} {p : α → Prop} [inst : Setoid α] {s t : Subtype p}, s ≈ t → t ≈ s
Subtype.symm _: Sort ?u.10223
_ p: α → Prop
p _) (@Subtype.trans: ∀ {α : Sort ?u.10235} {p : α → Prop} [inst : Setoid α] {s t u : Subtype p}, s ≈ t → t ≈ u → s ≈ u
Subtype.trans _: Sort ?u.10235
_ p: α → Prop
p _)
#align subtype.equivalence Subtype.equivalence: ∀ {α : Sort u_1} [inst : Setoid α] (p : α → Prop), Equivalence HasEquiv.Equiv
Subtype.equivalence

instance: {α : Sort u_1} → [inst : Setoid α] → (p : α → Prop) → Setoid (Subtype p)
instance (p: α → Prop
p : α: Sort ?u.10256
α → Prop: Type
Prop) : Setoid: Sort ?u.10280 → Sort (max1?u.10280)
Setoid (Subtype: {α : Sort ?u.10281} → (α → Prop) → Sort (max1?u.10281)
Subtype p: α → Prop
p) :=
  Setoid.mk: {α : Sort ?u.10288} → (r : α → α → Prop) → Equivalence r → Setoid α
Setoid.mk (· ≈ ·): Subtype p → Subtype p → Sort ?u.10297
(· ≈ ·) (equivalence: ∀ {α : Sort ?u.10328} [inst : Setoid α] (p : α → Prop), Equivalence HasEquiv.Equiv
equivalence p: α → Prop
p)

end Subtype

namespace Subtype

/-! Some facts about sets, which require that `α` is a type. -/
variable {α: Type ?u.10640
α β: Type ?u.10417
β γ: Type ?u.10407
γ : Type _: Type (?u.10646+1)
Type _} {p: α → Prop
p : α: Type ?u.10401
α → Prop: Type
Prop}

@[simp]
theorem coe_prop: ∀ {α : Type u_1} {S : Set α} (a : { a // a ∈ S }), ↑a ∈ S
coe_prop {S: Set α
S : Set: Type ?u.10427 → Type ?u.10427
Set α: Type ?u.10414
α} (a: { a // a ∈ S }
a : { a: ?m.10433
a // a: ?m.10433
a ∈ S: Set α
S }) : ↑a: { a // a ∈ S }
a ∈ S: Set α
S :=
  a: { a // a ∈ S }
a.prop: ∀ {α : Sort ?u.10608} {p : α → Prop} (x : Subtype p), p ↑x
prop
#align subtype.coe_prop Subtype.coe_prop: ∀ {α : Type u_1} {S : Set α} (a : { a // a ∈ S }), ↑a ∈ S
Subtype.coe_prop

theorem val_prop: ∀ {α : Type u_1} {S : Set α} (a : { a // a ∈ S }), ↑a ∈ S
val_prop {S: Set α
S : Set: Type ?u.10653 → Type ?u.10653
Set α: Type ?u.10640
α} (a: { a // a ∈ S }
a : { a: ?m.10659
a // a: ?m.10659
a ∈ S: Set α
S }) : a: { a // a ∈ S }
a.val: {α : Sort ?u.10698} → {p : α → Prop} → Subtype p → α
val ∈ S: Set α
S :=
  a: { a // a ∈ S }
a.property: ∀ {α : Sort ?u.10718} {p : α → Prop} (self : Subtype p), p ↑self
property
#align subtype.val_prop Subtype.val_prop: ∀ {α : Type u_1} {S : Set α} (a : { a // a ∈ S }), ↑a ∈ S
Subtype.val_prop

end Subtype