/-
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 := by
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 qinduction 
q: Quot r
q using 
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
α: 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 qapply 
f: (a : α) → motive (mk r a)
f
α: 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 qapply 
Subsingleton.elim: ∀ {α : Sort ?u.436} [h : Subsingleton α] (a b : α), a = b
Subsingleton.elim
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'