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

! This file was ported from Lean 3 source module data.set_like.basic
! leanprover-community/mathlib commit feb99064803fd3108e37c18b0f77d0a8344677a3
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Set.Basic
import Mathlib.Tactic.Monotonicity.Attr

/-!
# Typeclass for types with a set-like extensionality property

The `Membership` typeclass is used to let terms of a type have elements.
Many instances of `Membership` have a set-like extensionality property:
things are equal iff they have the same elements.  The `SetLike`
typeclass provides a unified interface to define a `Membership` that is
extensional in this way.

The main use of `SetLike` is for algebraic subobjects (such as
`Submonoid` and `Submodule`), whose non-proof data consists only of a
carrier set.  In such a situation, the projection to the carrier set
is injective.

In general, a type `A` is `SetLike` with elements of type `B` if it
has an injective map to `Set B`.  This module provides standard
boilerplate for every `SetLike`: a `coe_sort`, a `coe` to set, a
`PartialOrder`, and various extensionality and simp lemmas.

A typical subobject should be declared as:
```
structure MySubobject (X : Type _) [ObjectTypeclass X] :=
(carrier : Set X)
(op_mem' : βˆ€ {x : X}, x ∈ carrier β†’ sorry ∈ carrier)

namespace MySubobject

variables {X : Type _} [ObjectTypeclass X] {x : X}

instance : SetLike (MySubobject X) X :=
⟨MySubobject.carrier, λ p q h, by cases p; cases q; congr'⟩

@[simp] lemma mem_carrier {p : MySubobject X} : x ∈ p.carrier ↔ x ∈ (p : Set X) := Iff.rfl

@[ext] theorem ext {p q : MySubobject X} (h : βˆ€ x, x ∈ p ↔ x ∈ q) : p = q := SetLike.ext h

/-- Copy of a `MySubobject` with a new `carrier` equal to the old one. Useful to fix definitional
equalities. See Note [range copy pattern]. -/
protected def copy (p : MySubobject X) (s : Set X) (hs : s = ↑p) : MySubobject X :=
{ carrier := s,
  op_mem' := hs.symm β–Έ p.op_mem' }

@[simp] lemma coe_copy (p : MySubobject X) (s : Set X) (hs : s = ↑p) :
  (p.copy s hs : Set X) = s := rfl

lemma copy_eq (p : MySubobject X) (s : Set X) (hs : s = ↑p) : p.copy s hs = p :=
SetLike.coe_injective hs

end MySubobject
```

An alternative to `SetLike` could have been an extensional `Membership` typeclass:
```
class ExtMembership (Ξ± : out_param $ Type u) (Ξ² : Type v) extends Membership Ξ± Ξ² :=
(ext_iff : βˆ€ {s t : Ξ²}, s = t ↔ βˆ€ (x : Ξ±), x ∈ s ↔ x ∈ t)
```
While this is equivalent, `SetLike` conveniently uses a carrier set projection directly.

## Tags

subobjects
-/


/-- A class to indicate that there is a canonical injection between `A` and `Set B`.

This has the effect of giving terms of `A` elements of type `B` (through a `Membership`
instance) and a compatible coercion to `Type _` as a subtype.

Note: if `SetLike.coe` is a projection, implementers should create a simp lemma such as
```
@[simp] lemma mem_carrier {p : MySubobject X} : x ∈ p.carrier ↔ x ∈ (p : Set X) := Iff.rfl
```
to normalize terms.

If you declare an unbundled subclass of `SetLike`, for example:
```
class MulMemClass (S : Type _) (M : Type _) [Mul M] [SetLike S M] where
  ...
```
Then you should *not* repeat the `outParam` declaration so `SetLike` will supply the value instead.
This ensures your subclass will not have issues with synthesis of the `[Mul M]` parameter starting
before the value of `M` is known.
-/
@[notation_class * carrier Simps.findCoercionArgs]
class 
SetLike: Type u_1 β†’ outParam (Type u_2) β†’ Type (maxu_1u_2)
SetLike (
A: Type ?u.2
A : 
Type _: Type (?u.2+1)
Type _) (
B: outParam (Type ?u.6)
B : 
outParam: Sort ?u.5 β†’ Sort ?u.5
outParam <| 
Type _: Type (?u.6+1)
Type _) where
  /-- The coercion from a term of a `SetLike` to its corresponding `Set`. -/
  protected 
coe: {A : Type u_1} β†’ {B : outParam (Type u_2)} β†’ [self : SetLike A B] β†’ A β†’ Set B
coe : 
A: Type ?u.2
A β†’ 
Set: Type ?u.13 β†’ Type ?u.13
Set 
B: outParam (Type ?u.6)
B
  /-- The coercion from a term of a `SetLike` to its corresponding `Set` is injective. -/
  protected 
coe_injective': βˆ€ {A : Type u_1} {B : outParam (Type u_2)} [self : SetLike A B], Function.Injective SetLike.coe
coe_injective' : 
Function.Injective: {Ξ± : Sort ?u.18} β†’ {Ξ² : Sort ?u.17} β†’ (Ξ± β†’ Ξ²) β†’ Prop
Function.Injective 
coe: A β†’ Set B
coe
#align set_like 
SetLike: Type u_1 β†’ outParam (Type u_2) β†’ Type (maxu_1u_2)
SetLike

attribute [coe] 
SetLike.coe: {A : Type u_1} β†’ {B : outParam (Type u_2)} β†’ [self : SetLike A B] β†’ A β†’ Set B
SetLike.coe
namespace SetLike

variable {
A: Type ?u.184
A : 
Type _: Type (?u.1608+1)
Type _} {
B: Type ?u.2644
B : 
Type _: Type (?u.1611+1)
Type _} [
i: SetLike A B
i : 
SetLike: Type ?u.1615 β†’ outParam (Type ?u.1614) β†’ Type (max?u.1615?u.1614)
SetLike 
A: Type ?u.184
A 
B: Type ?u.3624
B]


instance: {A : Type u_1} β†’ {B : Type u_2} β†’ [i : SetLike A B] β†’ CoeTC A (Set B)
instance : 
CoeTC: Sort ?u.205 β†’ Sort ?u.204 β†’ Sort (max(max1?u.205)?u.204)
CoeTC 
A: Type ?u.194
A (
Set: Type ?u.206 β†’ Type ?u.206
Set 
B: Type ?u.197
B) where coe := 
SetLike.coe: {A : Type ?u.215} β†’ {B : outParam (Type ?u.214)} β†’ [self : SetLike A B] β†’ A β†’ Set B
SetLike.coe


instance: {A : Type u_1} β†’ {B : Type u_2} β†’ [i : SetLike A B] β†’ Membership B A
instance (priority := 100) : 
Membership: outParam (Type ?u.298) β†’ Type ?u.297 β†’ Type (max?u.298?u.297)
Membership 
B: Type ?u.290
B 
A: Type ?u.287
A :=
  ⟨fun 
x: ?m.310
x 
p: ?m.313
p => 
x: ?m.310
x ∈ (
p: ?m.313
p : 
Set: Type ?u.321 β†’ Type ?u.321
Set 
B: Type ?u.290
B)⟩


instance: {A : Type u_1} β†’ {B : Type u_2} β†’ [i : SetLike A B] β†’ CoeSort A (Type u_2)
instance (priority := 100) : 
CoeSort: Sort ?u.487 β†’ outParam (Sort ?u.486) β†’ Sort (max(max1?u.487)?u.486)
CoeSort 
A: Type ?u.476
A (
Type _: Type (?u.488+1)
Type _) :=
  ⟨fun 
p: ?m.500
p => { 
x: B
x : 
B: Type ?u.479
B // 
x: B
x ∈ 
p: ?m.500
p }⟩

variable (
p: A
p 
q: A
q : 
A: Type ?u.591
A)

@[simp, norm_cast]
theorem 
coe_sort_coe: βˆ€ {A : Type u_2} {B : Type u_1} [i : SetLike A B] (p : A), ↑↑p = { x // x ∈ p }
coe_sort_coe : ((
p: A
p : 
Set: Type ?u.623 β†’ Type ?u.623
Set 
B: Type ?u.608
B) : 
Type _: Type (?u.621+1)
Type _) = 
p: A
p :=
  
rfl: βˆ€ {Ξ± : Sort ?u.1068} {a : Ξ±}, a = a
rfl
#align set_like.coe_sort_coe 
SetLike.coe_sort_coe: βˆ€ {A : Type u_2} {B : Type u_1} [i : SetLike A B] (p : A), ↑↑p = { x // x ∈ p }
SetLike.coe_sort_coe

variable {
p: ?m.1192
p 
q: ?m.1195
q}

protected theorem 
Β«existsΒ»: βˆ€ {q : { x // x ∈ p } β†’ Prop}, (βˆƒ x, q x) ↔ βˆƒ x h, q { val := x, property := h }
Β«existsΒ» {
q: { x // x ∈ p } β†’ Prop
q : 
p: A
p β†’ 
Prop: Type
Prop} : (βˆƒ 
x: ?m.1244
x, 
q: { x // x ∈ p } β†’ Prop
q 
x: ?m.1244
x) ↔ βˆƒ (
x: B
x : 
B: Type ?u.1201
B) (
h: x ∈ p
h : 
x: B
x ∈ 
p: A
p), 
q: { x // x ∈ p } β†’ Prop
q ⟨
x: B
x, β€Ή_β€ΊβŸ© :=
  
SetCoe.exists: βˆ€ {Ξ± : Type ?u.1310} {s : Set Ξ±} {p : ↑s β†’ Prop}, (βˆƒ x, p x) ↔ βˆƒ x h, p { val := x, property := h }
SetCoe.exists
#align set_like.exists 
SetLike.exists: βˆ€ {A : Type u_2} {B : Type u_1} [i : SetLike A B] {p : A} {q : { x // x ∈ p } β†’ Prop},
  (βˆƒ x, q x) ↔ βˆƒ x h, q { val := x, property := h }
SetLike.exists

protected theorem 
Β«forallΒ»: βˆ€ {A : Type u_2} {B : Type u_1} [i : SetLike A B] {p : A} {q : { x // x ∈ p } β†’ Prop},
  (βˆ€ (x : { x // x ∈ p }), q x) ↔ βˆ€ (x : B) (h : x ∈ p), q { val := x, property := h }
Β«forallΒ» {
q: { x // x ∈ p } β†’ Prop
q : 
p: A
p β†’ 
Prop: Type
Prop} : (βˆ€ 
x: ?m.1407
x, 
q: { x // x ∈ p } β†’ Prop
q 
x: ?m.1407
x) ↔ βˆ€ (
x: B
x : 
B: Type ?u.1366
B) (
h: x ∈ p
h : 
x: B
x ∈ 
p: A
p), 
q: { x // x ∈ p } β†’ Prop
q ⟨
x: B
x, β€Ή_β€ΊβŸ© :=
  
SetCoe.forall: βˆ€ {Ξ± : Type ?u.1467} {s : Set Ξ±} {p : ↑s β†’ Prop},
  (βˆ€ (x : ↑s), p x) ↔ βˆ€ (x : Ξ±) (h : x ∈ s), p { val := x, property := h }
SetCoe.forall
#align set_like.forall 
SetLike.forall: βˆ€ {A : Type u_2} {B : Type u_1} [i : SetLike A B] {p : A} {q : { x // x ∈ p } β†’ Prop},
  (βˆ€ (x : { x // x ∈ p }), q x) ↔ βˆ€ (x : B) (h : x ∈ p), q { val := x, property := h }
SetLike.forall

theorem 
coe_injective: βˆ€ {A : Type u_1} {B : Type u_2} [i : SetLike A B], Function.Injective SetLike.coe
coe_injective : 
Function.Injective: {Ξ± : Sort ?u.1529} β†’ {Ξ² : Sort ?u.1528} β†’ (Ξ± β†’ Ξ²) β†’ Prop
Function.Injective (
SetLike.coe: {A : Type ?u.1537} β†’ {B : outParam (Type ?u.1536)} β†’ [self : SetLike A B] β†’ A β†’ Set B
SetLike.coe : 
A: Type ?u.1514
A β†’ 
Set: Type ?u.1535 β†’ Type ?u.1535
Set 
B: Type ?u.1517
B) := fun 
_: ?m.1559
_ 
_: ?m.1562
_ 
h: ?m.1565
h =>
  
SetLike.coe_injective': βˆ€ {A : Type ?u.1568} {B : outParam (Type ?u.1567)} [self : SetLike A B], Function.Injective SetLike.coe
SetLike.coe_injective' 
h: ?m.1565
h
#align set_like.coe_injective 
SetLike.coe_injective: βˆ€ {A : Type u_1} {B : Type u_2} [i : SetLike A B], Function.Injective SetLike.coe
SetLike.coe_injective

@[simp, norm_cast]
theorem 
coe_set_eq: ↑p = ↑q ↔ p = q
coe_set_eq : (
p: A
p : 
Set: Type ?u.1624 β†’ Type ?u.1624
Set 
B: Type ?u.1611
B) = 
q: A
q ↔ 
p: A
p = 
q: A
q :=
  
coe_injective: βˆ€ {A : Type ?u.1831} {B : Type ?u.1832} [i : SetLike A B], Function.Injective SetLike.coe
coe_injective.
eq_iff: βˆ€ {Ξ± : Sort ?u.1840} {Ξ² : Sort ?u.1841} {f : Ξ± β†’ Ξ²}, Function.Injective f β†’ βˆ€ {a b : Ξ±}, f a = f b ↔ a = b
eq_iff
#align set_like.coe_set_eq 
SetLike.coe_set_eq: βˆ€ {A : Type u_2} {B : Type u_1} [i : SetLike A B] {p q : A}, ↑p = ↑q ↔ p = q
SetLike.coe_set_eq

theorem 
ext': ↑p = ↑q β†’ p = q
ext' (
h: ↑p = ↑q
h : (
p: A
p : 
Set: Type ?u.2006 β†’ Type ?u.2006
Set 
B: Type ?u.1993
B) = 
q: A
q) : 
p: A
p = 
q: A
q :=
  
coe_injective: βˆ€ {A : Type ?u.2216} {B : Type ?u.2217} [i : SetLike A B], Function.Injective SetLike.coe
coe_injective 
h: ↑p = ↑q
h
#align set_like.ext' 
SetLike.ext': βˆ€ {A : Type u_2} {B : Type u_1} [i : SetLike A B] {p q : A}, ↑p = ↑q β†’ p = q
SetLike.ext'

theorem 
ext'_iff: p = q ↔ ↑p = ↑q
ext'_iff : 
p: A
p = 
q: A
q ↔ (
p: A
p : 
Set: Type ?u.2272 β†’ Type ?u.2272
Set 
B: Type ?u.2257
B) = 
q: A
q :=
  
coe_set_eq: βˆ€ {A : Type ?u.2478} {B : Type ?u.2477} [i : SetLike A B] {p q : A}, ↑p = ↑q ↔ p = q
coe_set_eq.
symm: βˆ€ {a b : Prop}, (a ↔ b) β†’ (b ↔ a)
symm
#align set_like.ext'_iff 
SetLike.ext'_iff: βˆ€ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, p = q ↔ ↑p = ↑q
SetLike.ext'_iff

/-- Note: implementers of `SetLike` must copy this lemma in order to tag it with `@[ext]`. -/
theorem 
ext: (βˆ€ (x : B), x ∈ p ↔ x ∈ q) β†’ p = q
ext (
h: βˆ€ (x : B), x ∈ p ↔ x ∈ q
h : βˆ€ 
x: ?m.2533
x, 
x: ?m.2533
x ∈ 
p: A
p ↔ 
x: ?m.2533
x ∈ 
q: A
q) : 
p: A
p = 
q: A
q :=
  
coe_injective: βˆ€ {A : Type ?u.2584} {B : Type ?u.2585} [i : SetLike A B], Function.Injective SetLike.coe
coe_injective <| 
Set.ext: βˆ€ {Ξ± : Type ?u.2598} {a b : Set Ξ±}, (βˆ€ (x : Ξ±), x ∈ a ↔ x ∈ b) β†’ a = b
Set.ext 
h: βˆ€ (x : B), x ∈ p ↔ x ∈ q
h
#align set_like.ext 
SetLike.ext: βˆ€ {A : Type u_2} {B : Type u_1} [i : SetLike A B] {p q : A}, (βˆ€ (x : B), x ∈ p ↔ x ∈ q) β†’ p = q
SetLike.ext

theorem 
ext_iff: p = q ↔ βˆ€ (x : B), x ∈ p ↔ x ∈ q
ext_iff : 
p: A
p = 
q: A
q ↔ βˆ€ 
x: ?m.2658
x, 
x: ?m.2658
x ∈ 
p: A
p ↔ 
x: ?m.2658
x ∈ 
q: A
q :=
  
coe_injective: βˆ€ {A : Type ?u.2705} {B : Type ?u.2706} [i : SetLike A B], Function.Injective SetLike.coe
coe_injective.
eq_iff: βˆ€ {Ξ± : Sort ?u.2714} {Ξ² : Sort ?u.2715} {f : Ξ± β†’ Ξ²}, Function.Injective f β†’ βˆ€ {a b : Ξ±}, f a = f b ↔ a = b
eq_iff.
symm: βˆ€ {a b : Prop}, (a ↔ b) β†’ (b ↔ a)
symm.
trans: βˆ€ {a b c : Prop}, (a ↔ b) β†’ (b ↔ c) β†’ (a ↔ c)
trans 
Set.ext_iff: βˆ€ {Ξ± : Type ?u.2742} {s t : Set Ξ±}, s = t ↔ βˆ€ (x : Ξ±), x ∈ s ↔ x ∈ t
Set.ext_iff
#align set_like.ext_iff 
SetLike.ext_iff: βˆ€ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, p = q ↔ βˆ€ (x : B), x ∈ p ↔ x ∈ q
SetLike.ext_iff

@[simp]
theorem 
mem_coe: βˆ€ {x : B}, x ∈ ↑p ↔ x ∈ p
mem_coe {
x: B
x : 
B: Type ?u.2781
B} : 
x: B
x ∈ (
p: A
p : 
Set: Type ?u.2800 β†’ Type ?u.2800
Set 
B: Type ?u.2781
B) ↔ 
x: B
x ∈ 
p: A
p :=
  
Iff.rfl: βˆ€ {a : Prop}, a ↔ a
Iff.rfl
#align set_like.mem_coe 
SetLike.mem_coe: βˆ€ {A : Type u_2} {B : Type u_1} [i : SetLike A B] {p : A} {x : B}, x ∈ ↑p ↔ x ∈ p
SetLike.mem_coe

@[simp, norm_cast]
theorem 
coe_eq_coe: βˆ€ {x y : { x // x ∈ p }}, ↑x = ↑y ↔ x = y
coe_eq_coe {
x: { x // x ∈ p }
x 
y: { x // x ∈ p }
y : 
p: A
p} : (
x: { x // x ∈ p }
x : 
B: Type ?u.2955
B) = 
y: { x // x ∈ p }
y ↔ 
x: { x // x ∈ p }
x = 
y: { x // x ∈ p }
y :=
  
Subtype.ext_iff_val: βˆ€ {Ξ± : Sort ?u.3259} {p : Ξ± β†’ Prop} {a1 a2 : { x // p x }}, a1 = a2 ↔ ↑a1 = ↑a2
Subtype.ext_iff_val.
symm: βˆ€ {a b : Prop}, (a ↔ b) β†’ (b ↔ a)
symm
#align set_like.coe_eq_coe 
SetLike.coe_eq_coe: βˆ€ {A : Type u_2} {B : Type u_1} [i : SetLike A B] {p : A} {x y : { x // x ∈ p }}, ↑x = ↑y ↔ x = y
SetLike.coe_eq_coe

-- porting note: this is not necessary anymore due to the way coercions work
#noalign set_like.coe_mk

@[simp]
theorem 
coe_mem: βˆ€ {A : Type u_2} {B : Type u_1} [i : SetLike A B] {p : A} (x : { x // x ∈ p }), ↑x ∈ p
coe_mem (
x: { x // x ∈ p }
x : 
p: A
p) : (
x: { x // x ∈ p }
x : 
B: Type ?u.3401
B) ∈ 
p: A
p :=
  
x: { x // x ∈ p }
x.
2: βˆ€ {Ξ± : Sort ?u.3581} {p : Ξ± β†’ Prop} (self : Subtype p), p ↑self
2
#align set_like.coe_mem 
SetLike.coe_mem: βˆ€ {A : Type u_2} {B : Type u_1} [i : SetLike A B] {p : A} (x : { x // x ∈ p }), ↑x ∈ p
SetLike.coe_mem

-- porting note: removed `@[simp]` because `simpNF` linter complained
protected theorem 
eta: βˆ€ {A : Type u_2} {B : Type u_1} [i : SetLike A B] {p : A} (x : { x // x ∈ p }) (hx : ↑x ∈ p),
  { val := ↑x, property := hx } = x
eta (
x: { x // x ∈ p }
x : 
p: A
p) (
hx: ↑x ∈ p
hx : (
x: { x // x ∈ p }
x : 
B: Type ?u.3624
B) ∈ 
p: A
p) : (⟨
x: { x // x ∈ p }
x, 
hx: ↑x ∈ p
hx⟩ : 
p: A
p) = 
x: { x // x ∈ p }
x := 
rfl: βˆ€ {Ξ± : Sort ?u.3840} {a : Ξ±}, a = a
rfl
#align set_like.eta 
SetLike.eta: βˆ€ {A : Type u_2} {B : Type u_1} [i : SetLike A B] {p : A} (x : { x // x ∈ p }) (hx : ↑x ∈ p),
  { val := ↑x, property := hx } = x
SetLike.eta


instance: {A : Type u_1} β†’ {B : Type u_2} β†’ [i : SetLike A B] β†’ PartialOrder A
instance (priority := 100) : 
PartialOrder: Type ?u.3869 β†’ Type ?u.3869
PartialOrder 
A: Type ?u.3855
A :=
  { 
PartialOrder.lift: {Ξ± : Type ?u.3874} β†’ {Ξ² : Type ?u.3873} β†’ [inst : PartialOrder Ξ²] β†’ (f : Ξ± β†’ Ξ²) β†’ Function.Injective f β†’ PartialOrder Ξ±
PartialOrder.lift (
SetLike.coe: {A : Type ?u.3898} β†’ {B : outParam (Type ?u.3897)} β†’ [self : SetLike A B] β†’ A β†’ Set B
SetLike.coe : 
A: Type ?u.3855
A β†’ 
Set: Type ?u.3896 β†’ Type ?u.3896
Set 
B: Type ?u.3858
B) 
coe_injective: βˆ€ {A : Type ?u.3918} {B : Type ?u.3919} [i : SetLike A B], Function.Injective SetLike.coe
coe_injective with
    le := fun 
H: ?m.3987
H 
K: ?m.3990
K => βˆ€ ⦃
x: ?m.3993
x⦄, 
x: ?m.3993
x ∈ 
H: ?m.3987
H β†’ 
x: ?m.3993
x ∈ 
K: ?m.3990
K }

theorem 
le_def: βˆ€ {S T : A}, S ≀ T ↔ βˆ€ ⦃x : B⦄, x ∈ S β†’ x ∈ T
le_def {
S: A
S 
T: A
T : 
A: Type ?u.4309
A} : 
S: A
S ≀ 
T: A
T ↔ βˆ€ ⦃
x: B
x : 
B: Type ?u.4312
B⦄, 
x: B
x ∈ 
S: A
S β†’ 
x: B
x ∈ 
T: A
T :=
  
Iff.rfl: βˆ€ {a : Prop}, a ↔ a
Iff.rfl
#align set_like.le_def 
SetLike.le_def: βˆ€ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {S T : A}, S ≀ T ↔ βˆ€ ⦃x : B⦄, x ∈ S β†’ x ∈ T
SetLike.le_def

@[simp, norm_cast]
theorem 
coe_subset_coe: βˆ€ {S T : A}, ↑S βŠ† ↑T ↔ S ≀ T
coe_subset_coe {
S: A
S 
T: A
T : 
A: Type ?u.4508
A} : (
S: A
S : 
Set: Type ?u.4530 β†’ Type ?u.4530
Set 
B: Type ?u.4511
B) βŠ† 
T: A
T ↔ 
S: A
S ≀ 
T: A
T :=
  
Iff.rfl: βˆ€ {a : Prop}, a ↔ a
Iff.rfl
#align set_like.coe_subset_coe 
SetLike.coe_subset_coe: βˆ€ {A : Type u_2} {B : Type u_1} [i : SetLike A B] {S T : A}, ↑S βŠ† ↑T ↔ S ≀ T
SetLike.coe_subset_coe

@[mono]
theorem 
coe_mono: βˆ€ {A : Type u_1} {B : Type u_2} [i : SetLike A B], Monotone SetLike.coe
coe_mono : 
Monotone: {Ξ± : Type ?u.4936} β†’ {Ξ² : Type ?u.4935} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
Monotone (
SetLike.coe: {A : Type ?u.4972} β†’ {B : outParam (Type ?u.4971)} β†’ [self : SetLike A B] β†’ A β†’ Set B
SetLike.coe : 
A: Type ?u.4921
A β†’ 
Set: Type ?u.4970 β†’ Type ?u.4970
Set 
B: Type ?u.4924
B) := fun 
_: ?m.5148
_ 
_: ?m.5151
_ => 
coe_subset_coe: βˆ€ {A : Type ?u.5154} {B : Type ?u.5153} [i : SetLike A B] {S T : A}, ↑S βŠ† ↑T ↔ S ≀ T
coe_subset_coe.
mpr: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
mpr
#align set_like.coe_mono 
SetLike.coe_mono: βˆ€ {A : Type u_1} {B : Type u_2} [i : SetLike A B], Monotone SetLike.coe
SetLike.coe_mono

@[simp, norm_cast]
theorem 
coe_ssubset_coe: βˆ€ {S T : A}, ↑S βŠ‚ ↑T ↔ S < T
coe_ssubset_coe {
S: A
S 
T: A
T : 
A: Type ?u.5207
A} : (
S: A
S : 
Set: Type ?u.5229 β†’ Type ?u.5229
Set 
B: Type ?u.5210
B) βŠ‚ 
T: A
T ↔ 
S: A
S < 
T: A
T :=
  
Iff.rfl: βˆ€ {a : Prop}, a ↔ a
Iff.rfl
#align set_like.coe_ssubset_coe 
SetLike.coe_ssubset_coe: βˆ€ {A : Type u_2} {B : Type u_1} [i : SetLike A B] {S T : A}, ↑S βŠ‚ ↑T ↔ S < T
SetLike.coe_ssubset_coe

@[mono]
theorem 
coe_strictMono: StrictMono SetLike.coe
coe_strictMono : 
StrictMono: {Ξ± : Type ?u.5631} β†’ {Ξ² : Type ?u.5630} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
StrictMono (
SetLike.coe: {A : Type ?u.5667} β†’ {B : outParam (Type ?u.5666)} β†’ [self : SetLike A B] β†’ A β†’ Set B
SetLike.coe : 
A: Type ?u.5616
A β†’ 
Set: Type ?u.5665 β†’ Type ?u.5665
Set 
B: Type ?u.5619
B) := fun 
_: ?m.5843
_ 
_: ?m.5846
_ => 
coe_ssubset_coe: βˆ€ {A : Type ?u.5849} {B : Type ?u.5848} [i : SetLike A B] {S T : A}, ↑S βŠ‚ ↑T ↔ S < T
coe_ssubset_coe.
mpr: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
mpr
#align set_like.coe_strict_mono 
SetLike.coe_strictMono: βˆ€ {A : Type u_1} {B : Type u_2} [i : SetLike A B], StrictMono SetLike.coe
SetLike.coe_strictMono

theorem 
not_le_iff_exists: βˆ€ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, Β¬p ≀ q ↔ βˆƒ x, x ∈ p ∧ Β¬x ∈ q
not_le_iff_exists : Β¬
p: A
p ≀ 
q: A
q ↔ βˆƒ 
x: ?m.6032
x ∈ 
p: A
p, 
x: ?m.6032
x βˆ‰ 
q: A
q :=
  
Set.not_subset: βˆ€ {Ξ± : Type ?u.6075} {s t : Set Ξ±}, Β¬s βŠ† t ↔ βˆƒ a, a ∈ s ∧ Β¬a ∈ t
Set.not_subset
#align set_like.not_le_iff_exists 
SetLike.not_le_iff_exists: βˆ€ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, Β¬p ≀ q ↔ βˆƒ x, x ∈ p ∧ Β¬x ∈ q
SetLike.not_le_iff_exists

theorem 
exists_of_lt: p < q β†’ βˆƒ x, x ∈ q ∧ Β¬x ∈ p
exists_of_lt : 
p: A
p < 
q: A
q β†’ βˆƒ 
x: ?m.6250
x ∈ 
q: A
q, 
x: ?m.6250
x βˆ‰ 
p: A
p :=
  
Set.exists_of_ssubset: βˆ€ {Ξ± : Type ?u.6293} {s t : Set Ξ±}, s βŠ‚ t β†’ βˆƒ x, x ∈ t ∧ Β¬x ∈ s
Set.exists_of_ssubset
#align set_like.exists_of_lt 
SetLike.exists_of_lt: βˆ€ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, p < q β†’ βˆƒ x, x ∈ q ∧ Β¬x ∈ p
SetLike.exists_of_lt

theorem 
lt_iff_le_and_exists: p < q ↔ p ≀ q ∧ βˆƒ x, x ∈ q ∧ Β¬x ∈ p
lt_iff_le_and_exists : 
p: A
p < 
q: A
q ↔ 
p: A
p ≀ 
q: A
q ∧ βˆƒ 
x: ?m.6544
x ∈ 
q: A
q, 
x: ?m.6544
x βˆ‰ 
p: A
p := 
Goals accomplished! πŸ™
A: Type u_1

B: Type u_2

i: SetLike A B

p, q: A

p < q ↔ p ≀ q ∧ βˆƒ x, x ∈ q ∧ Β¬x ∈ p
A: Type u_1

B: Type u_2

i: SetLike A B

p, q: A

p < q ↔ p ≀ q ∧ βˆƒ x, x ∈ q ∧ Β¬x ∈ p
A: Type u_1

B: Type u_2

i: SetLike A B

p, q: A

p ≀ q ∧ Β¬q ≀ p ↔ p ≀ q ∧ βˆƒ x, x ∈ q ∧ Β¬x ∈ p
A: Type u_1

B: Type u_2

i: SetLike A B

p, q: A

p < q ↔ p ≀ q ∧ βˆƒ x, x ∈ q ∧ Β¬x ∈ p
A: Type u_1

B: Type u_2

i: SetLike A B

p, q: A

(p ≀ q ∧ βˆƒ x, x ∈ q ∧ Β¬x ∈ p) ↔ p ≀ q ∧ βˆƒ x, x ∈ q ∧ Β¬x ∈ p
Goals accomplished! πŸ™

#align set_like.lt_iff_le_and_exists 
SetLike.lt_iff_le_and_exists: βˆ€ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, p < q ↔ p ≀ q ∧ βˆƒ x, x ∈ q ∧ Β¬x ∈ p
SetLike.lt_iff_le_and_exists

end SetLike