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) 2023 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johan Commelin
-/
import Mathlib.Mathport.Rename

/-!
# Quot

Some induction principles tagged with `elab_as_elim`, since the attribute is missing in core.
-/
#align quotient.induction_on 
Quotient.inductionOn: ∀ {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop} (q : Quotient s), (∀ (a : α), motive (Quotient.mk s a)) → motive q
Quotient.inductionOn
#align quot.induction_on
Quot.inductionOn: ∀ {α : Sort u} {r : α → α → Prop} {motive : Quot r → Prop} (q : Quot r), (∀ (a : α), motive (Quot.mk r a)) → motive q
Quot.inductionOn
variable {
α: Sort u
α
:
Sort u: Type u
Sort
Sort u: Type u
u
} {
r: α → α → Prop
r
:
α: Sort u
α
→
α: Sort u
α
→
Prop: Type
Prop
} {
motive: Quot r → Sort v
motive
:
Quot: {α : Sort ?u.325} → (α → α → Prop) → Sort ?u.325
Quot
r: α → α → Prop
r
→
Sort v: Type v
Sort
Sort v: Type v
v
} @[inherit_doc
Quot.rec: {α : Sort u} → {r : α → α → Prop} → {motive : Quot r → Sort v} → (f : (a : α) → motive (mk r a)) → (∀ (a b : α) (p : r a b), (_ : mk r a = mk r b) ▸ f a = f b) → (q : Quot r) → motive q
Quot.rec
, elab_as_elim] -- Porting note: adding `elab_as_elim` protected abbrev
Quot.recOn': (q : Quot r) → (f : (a : α) → motive (mk r a)) → (∀ (a b : α) (p : r a b), (_ : mk r a = mk r b) ▸ f a = f b) → motive q
Quot.recOn'
(
q: Quot r
q
:
Quot: {α : Sort ?u.42} → (α → α → Prop) → Sort ?u.42
Quot
r: α → α → Prop
r
) (
f: (a : α) → motive (mk r a)
f
: (
a: α
a
:
α: Sort u
α
) →
motive: Quot r → Sort v
motive
(
Quot.mk: {α : Sort ?u.55} → (r : α → α → Prop) → α → Quot r
Quot.mk
r: α → α → Prop
r
a: α
a
)) (
h: ∀ (a b : α) (p : r a b), (_ : mk r a = mk r b) ▸ f a = f b
h
: (
a: α
a
b: α
b
:
α: Sort u
α
) → (
p: r a b
p
:
r: α → α → Prop
r
a: α
a
b: α
b
) →
Eq.ndrec: {α : Sort ?u.78} → {a : α} → {motive : α → Sort ?u.79} → motive a → {b : α} → a = b → motive b
Eq.ndrec
(
f: (a : α) → motive (mk r a)
f
a: α
a
) (
Quot.sound: ∀ {α : Sort ?u.86} {r : α → α → Prop} {a b : α}, r a b → mk r a = mk r b
Quot.sound
p: r a b
p
) =
f: (a : α) → motive (mk r a)
f
b: α
b
) :
motive: Quot r → Sort v
motive
q: Quot r
q
:=
q: Quot r
q
.
rec: {α : Sort ?u.111} → {r : α → α → Prop} → {motive : Quot r → Sort ?u.110} → (f : (a : α) → motive (mk r a)) → (∀ (a b : α) (p : r a b), (_ : mk r a = mk r b) ▸ f a = f b) → (q : Quot r) → motive q
rec
f: (a : α) → motive (mk r a)
f
h: ∀ (a b : α) (p : r a b), (_ : mk r a = mk r b) ▸ f a = f b
h
#align quot.rec_on
Quot.recOn': {α : Sort u} → {r : α → α → Prop} → {motive : Quot r → Sort v} → (q : Quot r) → (f : (a : α) → motive (Quot.mk r a)) → (∀ (a b : α) (p : r a b), (_ : Quot.mk r a = Quot.mk r b) ▸ f a = f b) → motive q
Quot.recOn'
-- expected token /-- Version of `Quot.recOnSubsingleton` tagged with `elab_as_elim` -/ @[elab_as_elim] -- Porting note: this attribute is missing in core protected abbrev
Quot.recOnSubsingleton': {α : Sort u} → {r : α → α → Prop} → {motive : Quot r → Sort v} → [h : ∀ (a : α), Subsingleton (motive (mk r a))] → (q : Quot r) → ((a : α) → motive (mk r a)) → motive q
Quot.recOnSubsingleton'
[
h: ∀ (a : α), Subsingleton (motive (mk r a))
h
: (
a: α
a
:
α: Sort u
α
) →
Subsingleton: Sort ?u.339 → Prop
Subsingleton
(
motive: Quot r → Sort v
motive
(
Quot.mk: {α : Sort ?u.340} → (r : α → α → Prop) → α → Quot r
Quot.mk
r: α → α → Prop
r
a: α
a
))] (
q: Quot r
q
:
Quot: {α : Sort ?u.355} → (α → α → Prop) → Sort ?u.355
Quot
r: α → α → Prop
r
) (
f: (a : α) → motive (mk r a)
f
: (
a: α
a
:
α: Sort u
α
) →
motive: Quot r → Sort v
motive
(
Quot.mk: {α : Sort ?u.368} → (r : α → α → Prop) → α → Quot r
Quot.mk
r: α → α → Prop
r
a: α
a
)) :
motive: Quot r → Sort v
motive
q: Quot r
q
:=

Goals accomplished! 🐙
α: Sort u

r: α → α → Prop

motive: Quot r → Sort v

h: ∀ (a : α), Subsingleton (motive (mk r a))

q: Quot r

f: (a : α) → motive (mk r a)


motive q
α: Sort u

r: α → α → Prop

motive: Quot r → Sort v

h: ∀ (a : α), Subsingleton (motive (mk r a))

f: (a : α) → motive (mk r a)

a✝: α


f
motive (mk r a✝)
α: Sort u

r: α → α → Prop

motive: Quot r → Sort v

h: ∀ (a : α), Subsingleton (motive (mk r a))

q: Quot r

f: (a : α) → motive (mk r a)

a✝, b✝: α

p✝: r a✝ b✝


h
(_ : mk r a✝ = mk r b✝) ▸ ?m.421 a✝ = ?m.421 b✝
α: Sort u

r: α → α → Prop

motive: Quot r → Sort v

h: ∀ (a : α), Subsingleton (motive (mk r a))

q: Quot r

f: (a : α) → motive (mk r a)


motive q
α: Sort u

r: α → α → Prop

motive: Quot r → Sort v

h: ∀ (a : α), Subsingleton (motive (mk r a))

q: Quot r

f: (a : α) → motive (mk r a)

a✝, b✝: α

p✝: r a✝ b✝


h
(_ : mk r a✝ = mk r b✝) ▸ f a✝ = f b✝
α: Sort u

r: α → α → Prop

motive: Quot r → Sort v

h: ∀ (a : α), Subsingleton (motive (mk r a))

q: Quot r

f: (a : α) → motive (mk r a)


motive q

Goals accomplished! 🐙
#align quot.rec_on_subsingleton
Quot.recOnSubsingleton': {α : Sort u} → {r : α → α → Prop} → {motive : Quot r → Sort v} → [h : ∀ (a : α), Subsingleton (motive (Quot.mk r a))] → (q : Quot r) → ((a : α) → motive (Quot.mk r a)) → motive q
Quot.recOnSubsingleton'