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: 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.5644SortSort _: Type ?u.5644 _} {p: Ξ± β Propp q: Ξ± β Propq : Ξ±: Sort ?u.5644Ξ± β Prop: TypeProp}

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 βxprop (x: Subtype px : Subtype: {Ξ± : Sort ?u.212} β (Ξ± β Prop) β Sort (max1?u.212)Subtype p: Ξ± β Propp) : p: Ξ± β Propp x: Subtype px :=
x: Subtype px.2: β {Ξ± : Sort ?u.340} {p : Ξ± β Prop} (self : Subtype p), p βself2
#align subtype.prop Subtype.prop: β {Ξ± : Sort u_1} {p : Ξ± β Prop} (x : Subtype p), p βxSubtype.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 } β Propq : { a: ?m.373a // p: Ξ± β Propp a: ?m.373a } β Prop: TypeProp} : (β x: ?m.381x, q: { a // p a } β Propq x: ?m.381x) β β a: ?m.386a b: ?m.389b, q: { a // p a } β Propq β¨a: ?m.386a, b: ?m.389bβ© :=
β¨fun h: ?m.419h a: ?m.422a b: ?m.425b β¦ h: ?m.419h β¨a: ?m.422a, b: ?m.425bβ©, fun h: ?m.446h β¨a: Ξ±a, b: p abβ© β¦ h: ?m.446h a: Ξ±a b: p abβ©
#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 β Propq : β x: ?m.595x, p: Ξ± β Propp x: ?m.595x β Prop: TypeProp} : (β x: ?m.603x h: ?m.606h, q: (x : Ξ±) β p x β Propq x: ?m.603x h: ?m.606h) β β x: { a // p a }x : { a: ?m.615a // p: Ξ± β Propp a: ?m.615a }, q: (x : Ξ±) β p x β Propq x: { a // p a }x x: { a // p a }x.2: β {Ξ± : Sort ?u.742} {p : Ξ± β Prop} (self : Subtype p), p βself2 :=
(@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.753x β¦ q: (x : Ξ±) β p x β Propq x: ?m.753x.1: {Ξ± : Sort ?u.755} β {p : Ξ± β Prop} β Subtype p β Ξ±1 x: ?m.753x.2: β {Ξ± : Sort ?u.764} {p : Ξ± β Prop} (self : Subtype p), p βself2).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 } β Propq : { a: ?m.829a // p: Ξ± β Propp a: ?m.829a } β Prop: TypeProp} : (β x: ?m.839x, q: { a // p a } β Propq x: ?m.839x) β β a: ?m.846a b: ?m.851b, q: { a // p a } β Propq β¨a: ?m.846a, b: ?m.851bβ© :=
β¨fun β¨β¨a: Ξ±a, b: p abβ©, h: q { val := a, property := b }hβ© β¦ β¨a: Ξ±a, b: p ab, h: q { val := a, property := b }hβ©, fun β¨a: Ξ±a, b: p ab, h: q { val := a, property := b }hβ© β¦ β¨β¨a: Ξ±a, b: p abβ©, 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 β Propq : β x: ?m.1326x, p: Ξ± β Propp x: ?m.1326x β Prop: TypeProp} : (β x: ?m.1336x h: ?m.1341h, q: (x : Ξ±) β p x β Propq x: ?m.1336x h: ?m.1341h) β β x: { a // p a }x : { a: ?m.1353a // p: Ξ± β Propp a: ?m.1353a }, q: (x : Ξ±) β p x β Propq x: { a // p a }x x: { a // p a }x.2: β {Ξ± : Sort ?u.1479} {p : Ξ± β Prop} (self : Subtype p), p βself2 :=
(@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.1491x β¦ q: (x : Ξ±) β p x β Propq x: ?m.1491x.1: {Ξ± : Sort ?u.1493} β {p : Ξ± β Prop} β Subtype p β Ξ±1 x: ?m.1491x.2: β {Ξ± : Sort ?u.1502} {p : Ξ± β Prop} (self : Subtype p), p βself2).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 = a2ext : β {a1: { x // p x }a1 a2: { x // p x }a2 : { x: ?m.1569x // p: Ξ± β Propp x: ?m.1569x }}, (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 = arfl => rfl: β {Ξ± : Sort ?u.1892} {a : Ξ±}, a = arfl
#align subtype.ext Subtype.ext: β {Ξ± : Sort u_1} {p : Ξ± β Prop} {a1 a2 : { x // p x }}, βa1 = βa2 β a1 = a2Subtype.ext

theorem ext_iff: β {Ξ± : Sort u_1} {p : Ξ± β Prop} {a1 a2 : { x // p x }}, a1 = a2 β βa1 = βa2ext_iff {a1: { x // p x }a1 a2: { x // p x }a2 : { x: ?m.2187x // p: Ξ± β Propp x: ?m.2196x }} : 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 = a2Subtype.extβ©
#align subtype.ext_iff Subtype.ext_iff: β {Ξ± : Sort u_1} {p : Ξ± β Prop} {a1 a2 : { x // p x }}, a1 = a2 β βa1 = βa2Subtype.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 = βa2heq_iff_coe_eq (h: β (x : Ξ±), p x β q xh : β x: ?m.2485x, p: Ξ± β Propp x: ?m.2485x β q: Ξ± β Propq x: ?m.2485x) {a1: { x // p x }a1 : { x: ?m.2493x // p: Ξ± β Propp x: ?m.2493x }} {a2: { x // q x }a2 : { x: ?m.2502x // q: Ξ± β Propq x: ?m.2502x }} :
HEq: {Ξ± : Sort ?u.2508} β Ξ± β {Ξ² : Sort ?u.2508} β Ξ² β PropHEq 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 tEq.rec (motive := Ξ» (pp: Ξ± β Proppp: (Ξ±: Sort ?u.2467Ξ± β Prop: TypeProp)) _: ?m.2751_ => β a2': { x // pp x }a2' : {x: ?m.2757x // pp: Ξ± β Proppp x: ?m.2757x}, HEq: {Ξ± : Sort ?u.2763} β Ξ± β {Ξ² : Sort ?u.2763} β Ξ² β PropHEq 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 = bheq_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 = βa2ext_iff) (funext: β {Ξ± : Sort ?u.3026} {Ξ² : Ξ± β Sort ?u.3025} {f g : (x : Ξ±) β Ξ² x}, (β (x : Ξ±), f x = g x) β f = gfunext \$ Ξ» x: ?m.3037x => propext: β {a b : Prop}, (a β b) β a = bpropext (h: β (x : Ξ±), p x β q xh x: ?m.3037x)) 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 = βa2Subtype.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.3087SortSort _: Type ?u.3087 _} {p: Ξ± β Propp : Ξ±: Sort ?u.3087Ξ± β Prop: TypeProp} {q: Ξ² β Propq : Ξ²: Sort ?u.3090Ξ² β Prop: TypeProp} {a: { x // p x }a : {x: ?m.3104x // p: Ξ± β Propp x: ?m.3104x}}
{b: { y // q y }b : {y: ?m.3113y // q: Ξ² β Propq y: ?m.3113y}} (h: Ξ± = Ξ²h : Ξ±: Sort ?u.3087Ξ± = Ξ²: Sort ?u.3090Ξ²) (h': HEq p qh' : HEq: {Ξ± : Sort ?u.3141} β Ξ± β {Ξ² : Sort ?u.3141} β Ξ² β PropHEq p: Ξ± β Propp q: Ξ² β Propq) : HEq: {Ξ± : Sort ?u.3150} β Ξ± β {Ξ² : Sort ?u.3150} β Ξ² β PropHEq a: { x // p x }a b: { y // q y }b β HEq: {Ξ± : Sort ?u.3156} β Ξ± β {Ξ² : Sort ?u.3156} β Ξ² β PropHEq (a: { x // p x }a : Ξ±: Sort ?u.3087Ξ±) (b: { y // q y }b : Ξ²: Sort ?u.3090Ξ²) := byGoals accomplished! π
Ξ±β: Sort ?u.3070Ξ²β: Sort ?u.3073Ξ³: Sort ?u.3076pβ, qβ: Ξ±β β PropΞ±, Ξ²: Sort u_1p: Ξ± β Propq: Ξ² β Propa: { x // p x }b: { y // q y }h: Ξ± = Ξ²h': HEq p qHEq a b β HEq βa βbsubst h: Ξ± = Ξ²hΞ±β: Sort ?u.3070Ξ²: Sort ?u.3073Ξ³: Sort ?u.3076pβ, qβ: Ξ±β β PropΞ±: Sort u_1p: Ξ± β Propa: { x // p x }q: Ξ± β Propb: { y // q y }h': HEq p qHEq a b β HEq βa βb
Ξ±β: Sort ?u.3070Ξ²β: Sort ?u.3073Ξ³: Sort ?u.3076pβ, qβ: Ξ±β β PropΞ±, Ξ²: Sort u_1p: Ξ± β Propq: Ξ² β Propa: { x // p x }b: { y // q y }h: Ξ± = Ξ²h': HEq p qHEq a b β HEq βa βbsubst h': HEq p qh'Ξ±β: Sort ?u.3070Ξ²: Sort ?u.3073Ξ³: Sort ?u.3076pβ, q: Ξ±β β PropΞ±: Sort u_1p: Ξ± β Propa, b: { y // p y }HEq a b β HEq βa βb
Ξ±β: Sort ?u.3070Ξ²β: Sort ?u.3073Ξ³: Sort ?u.3076pβ, qβ: Ξ±β β PropΞ±, Ξ²: Sort u_1p: Ξ± β Propq: Ξ² β Propa: { x // p x }b: { y // q y }h: Ξ± = Ξ²h': HEq p qHEq a b β HEq βa βbrw [Ξ±β: Sort ?u.3070Ξ²: Sort ?u.3073Ξ³: Sort ?u.3076pβ, q: Ξ±β β PropΞ±: Sort u_1p: Ξ± β Propa, b: { y // p y }HEq a b β HEq βa βbheq_iff_eq: β {Ξ± : Sort ?u.3414} {a b : Ξ±}, HEq a b β a = bheq_iff_eq,Ξ±β: Sort ?u.3070Ξ²: Sort ?u.3073Ξ³: Sort ?u.3076pβ, q: Ξ±β β PropΞ±: Sort u_1p: Ξ± β Propa, b: { y // p y }a = b β HEq βa βb Ξ±β: Sort ?u.3070Ξ²: Sort ?u.3073Ξ³: Sort ?u.3076pβ, q: Ξ±β β PropΞ±: Sort u_1p: Ξ± β Propa, b: { y // p y }HEq a b β HEq βa βbheq_iff_eq: β {Ξ± : Sort ?u.3433} {a b : Ξ±}, HEq a b β a = bheq_iff_eq,Ξ±β: Sort ?u.3070Ξ²: Sort ?u.3073Ξ³: Sort ?u.3076pβ, q: Ξ±β β PropΞ±: Sort u_1p: Ξ± β Propa, b: { y // p y }a = b β βa = βb Ξ±β: Sort ?u.3070Ξ²: Sort ?u.3073Ξ³: Sort ?u.3076pβ, q: Ξ±β β PropΞ±: Sort u_1p: Ξ± β Propa, b: { y // p y }HEq a b β HEq βa βbext_iff: β {Ξ± : Sort ?u.3442} {p : Ξ± β Prop} {a1 a2 : { x // p x }}, a1 = a2 β βa1 = βa2ext_iffΞ±β: Sort ?u.3070Ξ²: Sort ?u.3073Ξ³: Sort ?u.3076pβ, q: Ξ±β β PropΞ±: Sort u_1p: Ξ± β Propa, 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 = a2ext_val {a1: { x // p x }a1 a2: { x // p x }a2 : { x: ?m.3530x // p: Ξ± β Propp x: ?m.3521x }} : 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 = a2Subtype.ext
#align subtype.ext_val Subtype.ext_val: β {Ξ± : Sort u_1} {p : Ξ± β Prop} {a1 a2 : { x // p x }}, βa1 = βa2 β a1 = a2Subtype.ext_val

theorem ext_iff_val: β {Ξ± : Sort u_1} {p : Ξ± β Prop} {a1 a2 : { x // p x }}, a1 = a2 β βa1 = βa2ext_iff_val {a1: { x // p x }a1 a2: { x // p x }a2 : { x: ?m.3605x // p: Ξ± β Propp x: ?m.3614x }} : 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 = βa2ext_iff
#align subtype.ext_iff_val Subtype.ext_iff_val: β {Ξ± : Sort u_1} {p : Ξ± β Prop} {a1 a2 : { x // p x }}, a1 = a2 β βa1 = βa2Subtype.ext_iff_val

@[simp]
theorem coe_eta: β {Ξ± : Sort u_1} {p : Ξ± β Prop} (a : { a // p a }) (h : p βa), { val := βa, property := h } = acoe_eta (a: { a // p a }a : { a: ?m.3682a // p: Ξ± β Propp a: ?m.3682a }) (h: p βah : p: Ξ± β Propp a: { a // p a }a) : mk: {Ξ± : Sort ?u.3812} β {p : Ξ± β Prop} β (val : Ξ±) β p val β Subtype pmk (βa: { a // p a }a) h: p βah = a: { a // p a }a :=
Subtype.ext: β {Ξ± : Sort ?u.3840} {p : Ξ± β Prop} {a1 a2 : { x // p x }}, βa1 = βa2 β a1 = a2Subtype.ext rfl: β {Ξ± : Sort ?u.3857} {a : Ξ±}, a = arfl
#align subtype.coe_eta Subtype.coe_eta: β {Ξ± : Sort u_1} {p : Ξ± β Prop} (a : { a // p a }) (h : p βa), { val := βa, property := h } = aSubtype.coe_eta

theorem coe_mk: β (a : Ξ±) (h : p a), β{ val := a, property := h } = acoe_mk (a: Ξ±a h: p ah) : (@mk: {Ξ± : Sort ?u.3909} β {p : Ξ± β Prop} β (val : Ξ±) β p val β Subtype pmk Ξ±: Sort ?u.3884Ξ± p: Ξ± β Propp a: ?m.3901a h: ?m.3904h : Ξ±: Sort ?u.3884Ξ±) = a: ?m.3901a :=
rfl: β {Ξ± : Sort ?u.4028} {a : Ξ±}, a = arfl
#align subtype.coe_mk Subtype.coe_mk: β {Ξ± : Sort u_1} {p : Ξ± β Prop} (a : Ξ±) (h : p a), β{ val := a, property := h } = aSubtype.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.4057a h: ?m.4060h a': Ξ±a' h': ?m.4066h'} : @mk: {Ξ± : Sort ?u.4070} β {p : Ξ± β Prop} β (val : Ξ±) β p val β Subtype pmk Ξ±: Sort ?u.4040Ξ± p: Ξ± β Propp a: ?m.4057a h: ?m.4060h = @mk: {Ξ± : Sort ?u.4072} β {p : Ξ± β Prop} β (val : Ξ±) β p val β Subtype pmk Ξ±: Sort ?u.4040Ξ± p: Ξ± β Propp a': ?m.4063a' h': ?m.4066h' β a: ?m.4057a = a': ?m.4063a' :=
ext_iff: β {Ξ± : Sort ?u.4085} {p : Ξ± β Prop} {a1 a2 : { x // p x }}, a1 = a2 β βa1 = βa2ext_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.4136a // p: Ξ± β Propp a: ?m.4136a }} {b: Ξ±b : Ξ±: Sort ?u.4116Ξ±} (h: ?m.4147 = bh : βa: { a // p a }a = b: Ξ±b) : a: { a // p a }a = β¨b: Ξ±b, h: ?m.4147 = bh βΈ a: { a // p a }a.2: β {Ξ± : Sort ?u.4285} {p : Ξ± β Prop} (self : Subtype p), p βself2β© :=
Subtype.ext: β {Ξ± : Sort ?u.4300} {p : Ξ± β Prop} {a1 a2 : { x // p x }}, βa1 = βa2 β a1 = a2Subtype.ext h: βa = bh
#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.4348a // p: Ξ± β Propp a: ?m.4348a }} {b: Ξ±b : Ξ±: Sort ?u.4328Ξ±} : βa: { a // p a }a = b: Ξ±b β β h: ?m.4485h, a: { a // p a }a = β¨b: Ξ±b, h: ?m.4485hβ© :=
β¨fun h: ?m.4514h β¦ h: ?m.4514h βΈ β¨a: { a // p a }a.2: β {Ξ± : Sort ?u.4528} {p : Ξ± β Prop} (self : Subtype p), p βself2, (coe_eta: β {Ξ± : Sort ?u.4535} {p : Ξ± β Prop} (a : { a // p a }) (h : p βa), { val := βa, property := h } = acoe_eta _: { a // ?m.4537 a }_ _: ?m.4537 β?m.4538_).symm: β {Ξ± : Sort ?u.4540} {a b : Ξ±}, a = b β b = asymmβ©, fun β¨_, ha: a = { val := b, property := wβ }haβ© β¦ ha: a = { val := b, property := wβ }ha.symm: β {Ξ± : Sort ?u.4619} {a b : Ξ±}, a = b β b = asymm βΈ rfl: β {Ξ± : Sort ?u.4627} {a : Ξ±}, a = arflβ©
#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 => βacoe_injective : Injective: {Ξ± : Sort ?u.4749} β {Ξ² : Sort ?u.4748} β (Ξ± β Ξ²) β PropInjective (fun (a: Subtype pa : Subtype: {Ξ± : Sort ?u.4753} β (Ξ± β Prop) β Sort (max1?u.4753)Subtype p: Ξ± β Propp) β¦ (a: Subtype pa : Ξ±: Sort ?u.4731Ξ±)) := fun _: ?m.4883_ _: ?m.4886_ β¦ Subtype.ext: β {Ξ± : Sort ?u.4888} {p : Ξ± β Prop} {a1 a2 : { x // p x }}, βa1 = βa2 β a1 = a2Subtype.ext
#align subtype.coe_injective Subtype.coe_injective: β {Ξ± : Sort u_1} {p : Ξ± β Prop}, Injective fun a => βaSubtype.coe_injective

theorem val_injective: Injective valval_injective : Injective: {Ξ± : Sort ?u.4943} β {Ξ² : Sort ?u.4942} β (Ξ± β Ξ²) β PropInjective (@val: {Ξ± : Sort ?u.4946} β {p : Ξ± β Prop} β Subtype p β Ξ±val _: Sort ?u.4946_ p: Ξ± β Propp) :=
coe_injective: β {Ξ± : Sort ?u.4957} {p : Ξ± β Prop}, Injective fun a => βacoe_injective
#align subtype.val_injective Subtype.val_injective: β {Ξ± : Sort u_1} {p : Ξ± β Prop}, Injective valSubtype.val_injective

theorem coe_inj: β {Ξ± : Sort u_1} {p : Ξ± β Prop} {a b : Subtype p}, βa = βb β a = bcoe_inj {a: Subtype pa b: Subtype pb : Subtype: {Ξ± : Sort ?u.4990} β (Ξ± β Prop) β Sort (max1?u.4990)Subtype p: Ξ± β Propp} : (a: Subtype pa : Ξ±: Sort ?u.4973Ξ±) = b: Subtype pb β a: Subtype pa = b: Subtype pb :=
coe_injective: β {Ξ± : Sort ?u.5302} {p : Ξ± β Prop}, Injective fun a => βacoe_injective.eq_iff: β {Ξ± : Sort ?u.5305} {Ξ² : Sort ?u.5306} {f : Ξ± β Ξ²}, Injective f β β {a b : Ξ±}, f a = f b β a = beq_iff
#align subtype.coe_inj Subtype.coe_inj: β {Ξ± : Sort u_1} {p : Ξ± β Prop} {a b : Subtype p}, βa = βb β a = bSubtype.coe_inj

theorem val_inj: β {a b : Subtype p}, βa = βb β a = bval_inj {a: Subtype pa b: Subtype pb : Subtype: {Ξ± : Sort ?u.5361} β (Ξ± β Prop) β Sort (max1?u.5361)Subtype p: Ξ± β Propp} : a: Subtype pa.val: {Ξ± : Sort ?u.5376} β {p : Ξ± β Prop} β Subtype p β Ξ±val = b: Subtype pb.val: {Ξ± : Sort ?u.5383} β {p : Ξ± β Prop} β Subtype p β Ξ±val β a: Subtype pa = b: Subtype pb :=
coe_inj: β {Ξ± : Sort ?u.5393} {p : Ξ± β Prop} {a b : Subtype p}, βa = βb β a = bcoe_inj
#align subtype.val_inj Subtype.val_inj: β {Ξ± : Sort u_1} {p : Ξ± β Prop} {a b : Subtype p}, βa = βb β a = bSubtype.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.LintersimpNF]
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 pa : Subtype: {Ξ± : Sort ?u.5437} β (Ξ± β Prop) β Sort (max1?u.5437)Subtype p: Ξ± β Propp} {b: Ξ±b : Ξ±: Sort ?u.5420Ξ±} :
(β h: p bh : p: Ξ± β Propp b: Ξ±b, a: Subtype pa = Subtype.mk: {Ξ± : Sort ?u.5451} β {p : Ξ± β Prop} β (val : Ξ±) β p val β Subtype pSubtype.mk b: Ξ±b h: p bh) β βa: Subtype pa = 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 = bexists_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.LintersimpNF]
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 pa : Subtype: {Ξ± : Sort ?u.5661} β (Ξ± β Prop) β Sort (max1?u.5661)Subtype p: Ξ± β Propp} {b: Ξ±b : Ξ±: Sort ?u.5644Ξ±} :
(β h: p bh : p: Ξ± β Propp b: Ξ±b, Subtype.mk: {Ξ± : Sort ?u.5675} β {p : Ξ± β Prop} β (val : Ξ±) β p val β Subtype pSubtype.mk b: Ξ±b h: p bh = a: Subtype pa) β b: Ξ±b = a: Subtype pa := byGoals accomplished! π
Ξ±: Sort u_1Ξ²: Sort ?u.5647Ξ³: Sort ?u.5650p, q: Ξ± β Propa: Subtype pb: Ξ±(β h, { val := b, property := h } = a) β b = βasimp only [@eq_comm: β {Ξ± : Sort ?u.5906} {a b : Ξ±}, a = b β b = aeq_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 = bexists_eq_subtype_mk_iff, @eq_comm: β {Ξ± : Sort ?u.5933} {a b : Ξ±}, a = b β b = aeq_comm _: Sort ?u.5933_ _: ?m.5934_ a: Subtype pa]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 = βaexists_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) β Ξ² βxrestrict {Ξ±: Sort ?u.6133Ξ±} {Ξ²: Ξ± β Type ?u.6135Ξ² : Ξ±: ?m.6130Ξ± β Type _: Type (?u.6135+1)Type _} (p: Ξ± β Propp : Ξ±: ?m.6130Ξ± β Prop: TypeProp) (f: (x : Ξ±) β Ξ² xf : β x: ?m.6143x, Ξ²: Ξ± β Type ?u.6135Ξ² x: ?m.6143x) (x: Subtype px : Subtype: {Ξ± : Sort ?u.6148} β (Ξ± β Prop) β Sort (max1?u.6148)Subtype p: Ξ± β Propp) : Ξ²: Ξ± β Type ?u.6135Ξ² x: Subtype px.1: {Ξ± : Sort ?u.6155} β {p : Ξ± β Prop} β Subtype p β Ξ±1 :=
f: (x : Ξ±) β Ξ² xf x: Subtype px
#align subtype.restrict Subtype.restrict: {Ξ± : Sort u_1} β {Ξ² : Ξ± β Type u_2} β (p : Ξ± β Prop) β ((x : Ξ±) β Ξ² x) β (x : Subtype p) β Ξ² βxSubtype.restrict

theorem restrict_apply: β {Ξ± : Sort u_1} {Ξ² : Ξ± β Type u_2} (f : (x : Ξ±) β Ξ² x) (p : Ξ± β Prop) (x : Subtype p), restrict p f x = f βxrestrict_apply {Ξ±: ?m.6419Ξ±} {Ξ²: Ξ± β Type ?u.6424Ξ² : Ξ±: ?m.6419Ξ± β Type _: Type (?u.6424+1)Type _} (f: (x : Ξ±) β Ξ² xf : β x: ?m.6428x, Ξ²: Ξ± β Type ?u.6424Ξ² x: ?m.6428x) (p: Ξ± β Propp : Ξ±: ?m.6419Ξ± β Prop: TypeProp) (x: Subtype px : Subtype: {Ξ± : Sort ?u.6437} β (Ξ± β Prop) β Sort (max1?u.6437)Subtype p: Ξ± β Propp) :
restrict: {Ξ± : Sort ?u.6446} β {Ξ² : Ξ± β Type ?u.6445} β (p : Ξ± β Prop) β ((x : Ξ±) β Ξ² x) β (x : Subtype p) β Ξ² βxrestrict p: Ξ± β Propp f: (x : Ξ±) β Ξ² xf x: Subtype px = f: (x : Ξ±) β Ξ² xf x: Subtype px.1: {Ξ± : Sort ?u.6460} β {p : Ξ± β Prop} β Subtype p β Ξ±1 := byGoals accomplished! π
Ξ±β: Sort ?u.6402Ξ²β: Sort ?u.6405Ξ³: Sort ?u.6408pβ, q: Ξ±β β PropΞ±: Sort u_1Ξ²: Ξ± β Type u_2f: (x : Ξ±) β Ξ² xp: Ξ± β Propx: Subtype prestrict p f x = f βxrflGoals 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 βxSubtype.restrict_apply

theorem restrict_def: β {Ξ± : Sort u_1} {Ξ² : Type u_2} (f : Ξ± β Ξ²) (p : Ξ± β Prop), restrict p f = f β fun a => βarestrict_def {Ξ±: ?m.6505Ξ± Ξ²: Type u_2Ξ²} (f: Ξ± β Ξ²f : Ξ±: ?m.6505Ξ± β Ξ²: ?m.6508Ξ²) (p: Ξ± β Propp : Ξ±: ?m.6505Ξ± β Prop: TypeProp) :
restrict: {Ξ± : Sort ?u.6521} β {Ξ² : Ξ± β Type ?u.6520} β (p : Ξ± β Prop) β ((x : Ξ±) β Ξ² x) β (x : Subtype p) β Ξ² βxrestrict p: Ξ± β Propp f: Ξ± β Ξ²f = f: Ξ± β Ξ²f β (fun (a: Subtype pa : Subtype: {Ξ± : Sort ?u.6543} β (Ξ± β Prop) β Sort (max1?u.6543)Subtype p: Ξ± β Propp) β¦ a: Subtype pa) := rfl: β {Ξ± : Sort ?u.6679} {a : Ξ±}, a = arfl
#align subtype.restrict_def Subtype.restrict_def: β {Ξ± : Sort u_1} {Ξ² : Type u_2} (f : Ξ± β Ξ²) (p : Ξ± β Prop), restrict p f = f β fun a => βaSubtype.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: Ξ± β Propp : Ξ±: ?m.6716Ξ± β Prop: TypeProp) (h: Injective fh : Injective: {Ξ± : Sort ?u.6731} β {Ξ² : Sort ?u.6730} β (Ξ± β Ξ²) β PropInjective f: Ξ± β Ξ²f) :
Injective: {Ξ± : Sort ?u.6740} β {Ξ² : Sort ?u.6739} β (Ξ± β Ξ²) β PropInjective (restrict: {Ξ± : Sort ?u.6744} β {Ξ² : Ξ± β Type ?u.6743} β (p : Ξ± β Prop) β ((x : Ξ±) β Ξ² x) β (x : Subtype p) β Ξ² βxrestrict p: Ξ± β Propp f: Ξ± β Ξ²f) :=
h: Injective fh.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 => βacoe_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 fsurjective_restrict {Ξ±: ?m.6848Ξ±} {Ξ²: Ξ± β Type ?u.6853Ξ² : Ξ±: ?m.6848Ξ± β Type _: Type (?u.6853+1)Type _} [ne: β (a : Ξ±), Nonempty (Ξ² a)ne : β a: ?m.6857a, Nonempty: Sort ?u.6860 β PropNonempty (Ξ²: Ξ± β Type ?u.6853Ξ² a: ?m.6857a)] (p: Ξ± β Propp : Ξ±: ?m.6848Ξ± β Prop: TypeProp) :
Surjective: {Ξ± : Sort ?u.6869} β {Ξ² : Sort ?u.6868} β (Ξ± β Ξ²) β PropSurjective fun f: (x : Ξ±) β Ξ² xf : β x: ?m.6874x, Ξ²: Ξ± β Type ?u.6853Ξ² x: ?m.6874x β¦ restrict: {Ξ± : Sort ?u.6880} β {Ξ² : Ξ± β Type ?u.6879} β (p : Ξ± β Prop) β ((x : Ξ±) β Ξ² x) β (x : Subtype p) β Ξ² βxrestrict p: Ξ± β Propp f: (x : Ξ±) β Ξ² xf := byGoals accomplished! π
Ξ±β: Sort ?u.6831Ξ²β: Sort ?u.6834Ξ³: Sort ?u.6837pβ, q: Ξ±β β PropΞ±: Sort u_1Ξ²: Ξ± β Type u_2ne: β (a : Ξ±), Nonempty (Ξ² a)p: Ξ± β PropSurjective fun f => restrict p fletI := Classical.decPred: {Ξ± : Sort ?u.6918} β (p : Ξ± β Prop) β DecidablePred pClassical.decPred p: Ξ± β ProppΞ±β: Sort ?u.6831Ξ²β: Sort ?u.6834Ξ³: Sort ?u.6837pβ, q: Ξ±β β PropΞ±: Sort u_1Ξ²: Ξ± β Type u_2ne: β (a : Ξ±), Nonempty (Ξ² a)p: Ξ± β Propthis:= Classical.decPred p: DecidablePred pSurjective fun f => restrict p f
Ξ±β: Sort ?u.6831Ξ²β: Sort ?u.6834Ξ³: Sort ?u.6837pβ, q: Ξ±β β PropΞ±: Sort u_1Ξ²: Ξ± β Type u_2ne: β (a : Ξ±), Nonempty (Ξ² a)p: Ξ± β PropSurjective fun f => restrict p frefine' fun f: ?m.6929f β¦ β¨fun x: ?m.6946x β¦ if h: ?m.6959h : p: Ξ± β Propp x: ?m.6946x then f: ?m.6929f β¨x: ?m.6946x, h: ?m.6959hβ© else Nonempty.some: {Ξ± : Sort ?u.6978} β Nonempty Ξ± β Ξ±Nonempty.some (ne: β (a : Ξ±), Nonempty (Ξ² a)ne x: ?m.6946x), funext: β {Ξ± : Sort ?u.6986} {Ξ² : Ξ± β Sort ?u.6985} {f g : (x : Ξ±) β Ξ² x}, (β (x : Ξ±), f x = g x) β f = gfunext <| _: β (x : ?m.6987), ?m.6989 x = ?m.6990 x_β©Ξ±β: Sort ?u.6831Ξ²β: Sort ?u.6834Ξ³: Sort ?u.6837pβ, q: Ξ±β β PropΞ±: Sort u_1Ξ²: Ξ± β Type u_2ne: β (a : Ξ±), Nonempty (Ξ² a)p: Ξ± β Propthis:= Classical.decPred p: DecidablePred pf: (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.6837pβ, q: Ξ±β β PropΞ±: Sort u_1Ξ²: Ξ± β Type u_2ne: β (a : Ξ±), Nonempty (Ξ² a)p: Ξ± β PropSurjective fun f => restrict p frintro β¨x, hxβ©: ?m.6987β¨x: Ξ±xβ¨x, hxβ©: ?m.6987, hx: p xhxβ¨x, hxβ©: ?m.6987β©Ξ±β: Sort ?u.6831Ξ²β: Sort ?u.6834Ξ³: Sort ?u.6837pβ, q: Ξ±β β PropΞ±: Sort u_1Ξ²: Ξ± β Type u_2ne: β (a : Ξ±), Nonempty (Ξ² a)p: Ξ± β Propthis:= Classical.decPred p: DecidablePred pf: (x : Subtype p) β Ξ² βxx: Ξ±hx: p xmk(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.6837pβ, q: Ξ±β β PropΞ±: Sort u_1Ξ²: Ξ± β Type u_2ne: β (a : Ξ±), Nonempty (Ξ² a)p: Ξ± β PropSurjective 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 hcdif_pos hx: p xhxGoals 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 fSubtype.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 asimps]
def coind: {Ξ± : Sort ?u.7124} β {Ξ² : Sort ?u.7125} β (f : Ξ± β Ξ²) β {p : Ξ² β Prop} β (β (a : Ξ±), p (f a)) β Ξ± β Subtype pcoind {Ξ±: Sort ?u.7124Ξ± Ξ²: ?m.7121Ξ²} (f: Ξ± β Ξ²f : Ξ±: ?m.7118Ξ± β Ξ²: ?m.7121Ξ²) {p: Ξ² β Propp : Ξ²: ?m.7121Ξ² β Prop: TypeProp} (h: β (a : Ξ±), p (f a)h : β a: ?m.7133a, p: Ξ² β Propp (f: Ξ± β Ξ²f a: ?m.7133a)) : Ξ±: ?m.7118Ξ± β Subtype: {Ξ± : Sort ?u.7140} β (Ξ± β Prop) β Sort (max1?u.7140)Subtype p: Ξ² β Propp := fun a: ?m.7152a β¦ β¨f: Ξ± β Ξ²f a: ?m.7152a, h: β (a : Ξ±), p (f a)h a: ?m.7152aβ©
#align subtype.coind Subtype.coind: {Ξ± : Sort u_1} β {Ξ² : Sort u_2} β (f : Ξ± β Ξ²) β {p : Ξ² β Prop} β (β (a : Ξ±), p (f a)) β Ξ± β Subtype pSubtype.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 aSubtype.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: Ξ² β Propp : Ξ²: ?m.7300Ξ² β Prop: TypeProp} (h: β (a : Ξ±), p (f a)h : β a: ?m.7312a, p: Ξ² β Propp (f: Ξ± β Ξ²f a: ?m.7312a)) (hf: Injective fhf : Injective: {Ξ± : Sort ?u.7318} β {Ξ² : Sort ?u.7317} β (Ξ± β Ξ²) β PropInjective f: Ξ± β Ξ²f) :
Injective: {Ξ± : Sort ?u.7327} β {Ξ² : Sort ?u.7326} β (Ξ± β Ξ²) β PropInjective (coind: {Ξ± : Sort ?u.7331} β {Ξ² : Sort ?u.7330} β (f : Ξ± β Ξ²) β {p : Ξ² β Prop} β (β (a : Ξ±), p (f a)) β Ξ± β Subtype pcoind f: Ξ± β Ξ²f h: β (a : Ξ±), p (f a)h) := fun x: ?m.7364x y: ?m.7367y hxy: ?m.7370hxy β¦ hf: Injective fhf <| byGoals accomplished! π Ξ±β: Sort ?u.7280Ξ²β: Sort ?u.7283Ξ³: Sort ?u.7286pβ, q: Ξ±β β PropΞ±: Sort u_1Ξ²: Sort u_2f: Ξ± β Ξ²p: Ξ² β Proph: β (a : Ξ±), p (f a)hf: Injective fx, y: Ξ±hxy: coind f h x = coind f h yf 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 yhxyGoals 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: Ξ² β Propp : Ξ²: ?m.7441Ξ² β Prop: TypeProp} (h: β (a : Ξ±), p (f a)h : β a: ?m.7453a, p: Ξ² β Propp (f: Ξ± β Ξ²f a: ?m.7453a)) (hf: Surjective fhf : Surjective: {Ξ± : Sort ?u.7459} β {Ξ² : Sort ?u.7458} β (Ξ± β Ξ²) β PropSurjective f: Ξ± β Ξ²f) :
Surjective: {Ξ± : Sort ?u.7469} β {Ξ² : Sort ?u.7468} β (Ξ± β Ξ²) β PropSurjective (coind: {Ξ± : Sort ?u.7473} β {Ξ² : Sort ?u.7472} β (f : Ξ± β Ξ²) β {p : Ξ² β Prop} β (β (a : Ξ±), p (f a)) β Ξ± β Subtype pcoind f: Ξ± β Ξ²f h: β (a : Ξ±), p (f a)h) := fun x: ?m.7509x β¦
let β¨a: Ξ±a, ha: f a = βxhaβ© := hf: Surjective fhf x: ?m.7509x
β¨a: Ξ±a, coe_injective: β {Ξ± : Sort ?u.7665} {p : Ξ± β Prop}, Injective fun a => βacoe_injective ha: f a = βxhaβ©
#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: Ξ² β Propp : Ξ²: ?m.7788Ξ² β Prop: TypeProp} (h: β (a : Ξ±), p (f a)h : β a: ?m.7800a, p: Ξ² β Propp (f: Ξ± β Ξ²f a: ?m.7800a)) (hf: Bijective fhf : Bijective: {Ξ± : Sort ?u.7806} β {Ξ² : Sort ?u.7805} β (Ξ± β Ξ²) β PropBijective f: Ξ± β Ξ²f) :
Bijective: {Ξ± : Sort ?u.7815} β {Ξ² : Sort ?u.7814} β (Ξ± β Ξ²) β PropBijective (coind: {Ξ± : Sort ?u.7819} β {Ξ² : Sort ?u.7818} β (f : Ξ± β Ξ²) β {p : Ξ² β Prop} β (β (a : Ξ±), p (f a)) β Ξ± β Subtype pcoind 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 fhf.1: β {a b : Prop}, a β§ b β a1, 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 fhf.2: β {a b : Prop}, a β§ b β b2β©
#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 βasimps]
def map: {p : Ξ± β Prop} β {q : Ξ² β Prop} β (f : Ξ± β Ξ²) β (β (a : Ξ±), p a β q (f a)) β Subtype p β Subtype qmap {p: Ξ± β Propp : Ξ±: Sort ?u.7927Ξ± β Prop: TypeProp} {q: Ξ² β Propq : Ξ²: Sort ?u.7930Ξ² β Prop: TypeProp} (f: Ξ± β Ξ²f : Ξ±: Sort ?u.7927Ξ± β Ξ²: Sort ?u.7930Ξ²) (h: β (a : Ξ±), p a β q (f a)h : β a: ?m.7957a, p: Ξ± β Propp a: ?m.7957a β q: Ξ² β Propq (f: Ξ± β Ξ²f a: ?m.7957a)) :
Subtype: {Ξ± : Sort ?u.7965} β (Ξ± β Prop) β Sort (max1?u.7965)Subtype p: Ξ± β Propp β Subtype: {Ξ± : Sort ?u.7971} β (Ξ± β Prop) β Sort (max1?u.7971)Subtype q: Ξ² β Propq :=
fun x: ?m.7982x β¦ β¨f: Ξ± β Ξ²f x: ?m.7982x, h: β (a : Ξ±), p a β q (f a)h x: ?m.7982x x: ?m.7982x.prop: β {Ξ± : Sort ?u.8108} {p : Ξ± β Prop} (x : Subtype p), p βxpropβ©
#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 qSubtype.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 βaSubtype.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))) xmap_comp {p: Ξ± β Propp : Ξ±: Sort ?u.8288Ξ± β Prop: TypeProp} {q: Ξ² β Propq : Ξ²: Sort ?u.8291Ξ² β Prop: TypeProp} {r: Ξ³ β Propr : Ξ³: Sort ?u.8294Ξ³ β Prop: TypeProp} {x: Subtype px : Subtype: {Ξ± : Sort ?u.8317} β (Ξ± β Prop) β Sort (max1?u.8317)Subtype p: Ξ± β Propp}
(f: Ξ± β Ξ²f : Ξ±: Sort ?u.8288Ξ± β Ξ²: Sort ?u.8291Ξ²) (h: β (a : Ξ±), p a β q (f a)h : β a: ?m.8329a, p: Ξ± β Propp a: ?m.8329a β q: Ξ² β Propq (f: Ξ± β Ξ²f a: ?m.8329a)) (g: Ξ² β Ξ³g : Ξ²: Sort ?u.8291Ξ² β Ξ³: Sort ?u.8294Ξ³) (l: β (a : Ξ²), q a β r (g a)l : β a: ?m.8341a, q: Ξ² β Propq a: ?m.8341a β r: Ξ³ β Propr (g: Ξ² β Ξ³g a: ?m.8341a)) :
map: {Ξ± : Sort ?u.8350} β
{Ξ² : Sort ?u.8349} β
{p : Ξ± β Prop} β {q : Ξ² β Prop} β (f : Ξ± β Ξ²) β (β (a : Ξ±), p a β q (f a)) β Subtype p β Subtype qmap 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 qmap f: Ξ± β Ξ²f h: β (a : Ξ±), p a β q (f a)h x: Subtype px) = map: {Ξ± : Sort ?u.8392} β
{Ξ² : Sort ?u.8391} β
{p : Ξ± β Prop} β {q : Ξ² β Prop} β (f : Ξ± β Ξ²) β (β (a : Ξ±), p a β q (f a)) β Subtype p β Subtype qmap (g: Ξ² β Ξ³g β f: Ξ± β Ξ²f) (fun a: ?m.8415a ha: ?m.8418ha β¦ l: β (a : Ξ²), q a β r (g a)l (f: Ξ± β Ξ²f a: ?m.8415a) <| h: β (a : Ξ±), p a β q (f a)h a: ?m.8415a ha: ?m.8418ha) x: Subtype px :=
rfl: β {Ξ± : Sort ?u.8440} {a : Ξ±}, a = arfl
#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))) xSubtype.map_comp

theorem map_id: β {p : Ξ± β Prop} {h : β (a : Ξ±), p a β p (id a)}, map id h = idmap_id {p: Ξ± β Propp : Ξ±: Sort ?u.8501Ξ± β Prop: TypeProp} {h: β (a : Ξ±), p a β p (id a)h : β a: ?m.8523a, p: Ξ± β Propp a: ?m.8523a β p: Ξ± β Propp (id: {Ξ± : Sort ?u.8528} β Ξ± β Ξ±id a: ?m.8523a)} : map: {Ξ± : Sort ?u.8534} β
{Ξ² : Sort ?u.8533} β
{p : Ξ± β Prop} β {q : Ξ² β Prop} β (f : Ξ± β Ξ²) β (β (a : Ξ±), p a β q (f a)) β Subtype p β Subtype qmap (@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 = gfunext fun _: ?m.8619_ β¦ rfl: β {Ξ± : Sort ?u.8621} {a : Ξ±}, a = arfl
#align subtype.map_id Subtype.map_id: β {Ξ± : Sort u_1} {p : Ξ± β Prop} {h : β (a : Ξ±), p a β p (id a)}, map id h = idSubtype.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: Ξ± β Propp : Ξ±: Sort ?u.8636Ξ± β Prop: TypeProp} {q: Ξ² β Propq : Ξ²: Sort ?u.8639Ξ² β Prop: TypeProp} {f: Ξ± β Ξ²f : Ξ±: Sort ?u.8636Ξ± β Ξ²: Sort ?u.8639Ξ²} (h: β (a : Ξ±), p a β q (f a)h : β a: ?m.8666a, p: Ξ± β Propp a: ?m.8666a β q: Ξ² β Propq (f: Ξ± β Ξ²f a: ?m.8666a))
(hf: Injective fhf : Injective: {Ξ± : Sort ?u.8674} β {Ξ² : Sort ?u.8673} β (Ξ± β Ξ²) β PropInjective f: Ξ± β Ξ²f) : Injective: {Ξ± : Sort ?u.8683} β {Ξ² : Sort ?u.8682} β (Ξ± β Ξ²) β PropInjective (map: {Ξ± : Sort ?u.8687} β
{Ξ² : Sort ?u.8686} β
{p : Ξ± β Prop} β {q : Ξ² β Prop} β (f : Ξ± β Ξ²) β (β (a : Ξ±), p a β q (f a)) β Subtype p β Subtype qmap 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 fhf.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 => βacoe_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: Ξ± β Propp : Ξ±: Sort ?u.8822Ξ± β Prop: TypeProp} {f: Ξ± β Ξ±f : Ξ±: Sort ?u.8822Ξ± β Ξ±: Sort ?u.8822Ξ±} (h: β (a : Ξ±), p a β p (f a)h : β a: ?m.8848a, p: Ξ± β Propp a: ?m.8848a β p: Ξ± β Propp (f: Ξ± β Ξ±f a: ?m.8848a))
(hf: Involutive fhf : Involutive: {Ξ± : Sort ?u.8855} β (Ξ± β Ξ±) β PropInvolutive f: Ξ± β Ξ±f) : Involutive: {Ξ± : Sort ?u.8862} β (Ξ± β Ξ±) β PropInvolutive (map: {Ξ± : Sort ?u.8865} β
{Ξ² : Sort ?u.8864} β
{p : Ξ± β Prop} β {q : Ξ² β Prop} β (f : Ξ± β Ξ²) β (β (a : Ξ±), p a β q (f a)) β Subtype p β Subtype qmap f: Ξ± β Ξ±f h: β (a : Ξ±), p a β p (f a)h) :=
fun x: ?m.8903x β¦ Subtype.ext: β {Ξ± : Sort ?u.8905} {p : Ξ± β Prop} {a1 a2 : { x // p x }}, βa1 = βa2 β a1 = a2Subtype.ext (hf: Involutive fhf x: ?m.8903x)
#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: Ξ± β Propp : Ξ±: Sort ?u.9053Ξ± β Prop: TypeProp) : HasEquiv: Sort ?u.9079 β Sort (max?u.9079(?u.9078+1))HasEquiv (Subtype: {Ξ± : Sort ?u.9080} β (Ξ± β Prop) β Sort (max1?u.9080)Subtype p: Ξ± β Propp) :=
β¨fun s: ?m.9095s t: ?m.9098t β¦ (s: ?m.9095s : Ξ±: Sort ?u.9053Ξ±) β (t: ?m.9098t : Ξ±: Sort ?u.9053Ξ±)β©

theorem equiv_iff: β [inst : HasEquiv Ξ±] {p : Ξ± β Prop} {s t : Subtype p}, s β t β βs β βtequiv_iff [HasEquiv: Sort ?u.9398 β Sort (max?u.9398(?u.9397+1))HasEquiv Ξ±: Sort ?u.9380Ξ±] {p: Ξ± β Propp : Ξ±: Sort ?u.9380Ξ± β Prop: TypeProp} {s: Subtype ps t: Subtype pt : Subtype: {Ξ± : Sort ?u.9405} β (Ξ± β Prop) β Sort (max1?u.9405)Subtype p: Ξ± β Propp} : s: Subtype ps β t: Subtype pt β (s: Subtype ps : Ξ±: Sort ?u.9380Ξ±) β (t: Subtype pt : Ξ±: Sort ?u.9380Ξ±) :=
Iff.rfl: β {a : Prop}, a β aIff.rfl
#align subtype.equiv_iff Subtype.equiv_iff: β {Ξ± : Sort u_1} [inst : HasEquiv Ξ±] {p : Ξ± β Prop} {s t : Subtype p}, s β t β βs β βtSubtype.equiv_iff

variable [Setoid: Sort ?u.9806 β Sort (max1?u.9806)Setoid Ξ±: Sort ?u.9669Ξ±]

protected theorem refl: β (s : Subtype p), s β srefl (s: Subtype ps : Subtype: {Ξ± : Sort ?u.9709} β (Ξ± β Prop) β Sort (max1?u.9709)Subtype p: Ξ± β Propp) : s: Subtype ps β s: Subtype ps :=
Setoid.refl: β {Ξ± : Sort ?u.9757} [inst : Setoid Ξ±] (a : Ξ±), a β aSetoid.refl _: ?m.9758_
#align subtype.refl Subtype.refl: β {Ξ± : Sort u_1} {p : Ξ± β Prop} [inst : Setoid Ξ±] (s : Subtype p), s β sSubtype.refl

protected theorem symm: β {Ξ± : Sort u_1} {p : Ξ± β Prop} [inst : Setoid Ξ±] {s t : Subtype p}, s β t β t β ssymm {s: Subtype ps t: Subtype pt : Subtype: {Ξ± : Sort ?u.9816} β (Ξ± β Prop) β Sort (max1?u.9816)Subtype p: Ξ± β Propp} (h: s β th : s: Subtype ps β t: Subtype pt) : t: Subtype pt β s: Subtype ps :=
Setoid.symm: β {Ξ± : Sort ?u.9897} [inst : Setoid Ξ±] {a b : Ξ±}, a β b β b β aSetoid.symm h: s β th
#align subtype.symm Subtype.symm: β {Ξ± : Sort u_1} {p : Ξ± β Prop} [inst : Setoid Ξ±] {s t : Subtype p}, s β t β t β sSubtype.symm

protected theorem trans: β {Ξ± : Sort u_1} {p : Ξ± β Prop} [inst : Setoid Ξ±] {s t u : Subtype p}, s β t β t β u β s β utrans {s: Subtype ps t: Subtype pt u: Subtype pu : Subtype: {Ξ± : Sort ?u.9966} β (Ξ± β Prop) β Sort (max1?u.9966)Subtype p: Ξ± β Propp} (hβ: s β thβ : s: Subtype ps β t: Subtype pt) (hβ: t β uhβ : t: Subtype pt β u: Subtype pu) : s: Subtype ps β u: Subtype pu :=
Setoid.trans: β {Ξ± : Sort ?u.10080} [inst : Setoid Ξ±] {a b c : Ξ±}, a β b β b β c β a β cSetoid.trans hβ: s β thβ hβ: t β uhβ
#align subtype.trans Subtype.trans: β {Ξ± : Sort u_1} {p : Ξ± β Prop} [inst : Setoid Ξ±] {s t u : Subtype p}, s β t β t β u β s β uSubtype.trans

theorem equivalence: β {Ξ± : Sort u_1} [inst : Setoid Ξ±] (p : Ξ± β Prop), Equivalence HasEquiv.Equivequivalence (p: Ξ± β Propp : Ξ±: Sort ?u.10122Ξ± β Prop: TypeProp) : Equivalence: {Ξ± : Sort ?u.10146} β (Ξ± β Ξ± β Prop) β PropEquivalence (@HasEquiv.Equiv: {Ξ± : Sort ?u.10149} β [self : HasEquiv Ξ±] β Ξ± β Ξ± β Sort ?u.10148HasEquiv.Equiv (Subtype: {Ξ± : Sort ?u.10150} β (Ξ± β Prop) β Sort (max1?u.10150)Subtype p: Ξ± β Propp) _) :=
.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 β sSubtype.refl) (@Subtype.symm: β {Ξ± : Sort ?u.10223} {p : Ξ± β Prop} [inst : Setoid Ξ±] {s t : Subtype p}, s β t β t β sSubtype.symm _: Sort ?u.10223_ p: Ξ± β Propp _) (@Subtype.trans: β {Ξ± : Sort ?u.10235} {p : Ξ± β Prop} [inst : Setoid Ξ±] {s t u : Subtype p}, s β t β t β u β s β uSubtype.trans _: Sort ?u.10235_ p: Ξ± β Propp _)
#align subtype.equivalence Subtype.equivalence: β {Ξ± : Sort u_1} [inst : Setoid Ξ±] (p : Ξ± β Prop), Equivalence HasEquiv.EquivSubtype.equivalence

instance: {Ξ± : Sort u_1} β [inst : Setoid Ξ±] β (p : Ξ± β Prop) β Setoid (Subtype p)instance (p: Ξ± β Propp : Ξ±: Sort ?u.10256Ξ± β Prop: TypeProp) : Setoid: Sort ?u.10280 β Sort (max1?u.10280)Setoid (Subtype: {Ξ± : Sort ?u.10281} β (Ξ± β Prop) β Sort (max1?u.10281)Subtype p: Ξ± β Propp) :=
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.Equivequivalence p: Ξ± β Propp)

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: Ξ± β Propp : Ξ±: Type ?u.10401Ξ± β Prop: TypeProp}

@[simp]
theorem coe_prop: β {Ξ± : Type u_1} {S : Set Ξ±} (a : { a // a β S }), βa β Scoe_prop {S: Set Ξ±S : Set: Type ?u.10427 β Type ?u.10427Set Ξ±: Type ?u.10414Ξ±} (a: { a // a β S }a : { a: ?m.10433a // a: ?m.10433a β 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 βxprop
#align subtype.coe_prop Subtype.coe_prop: β {Ξ± : Type u_1} {S : Set Ξ±} (a : { a // a β S }), βa β SSubtype.coe_prop

theorem val_prop: β {Ξ± : Type u_1} {S : Set Ξ±} (a : { a // a β S }), βa β Sval_prop {S: Set Ξ±S : Set: Type ?u.10653 β Type ?u.10653Set Ξ±: Type ?u.10640Ξ±} (a: { a // a β S }a : { a: ?m.10659a // a: ?m.10659a β 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 βselfproperty
#align subtype.val_prop Subtype.val_prop: β {Ξ± : Type u_1} {S : Set Ξ±} (a : { a // a β S }), βa β SSubtype.val_prop

end Subtype
```