Skip to content

Commit a821dcb

Browse files
leodemouraleodemoura
committed
chore: enforce naming convention for theorems
see issue #402 fix: `ElabTerm.lean`
1 parent a0c2142 commit a821dcb

37 files changed

+580
-549
lines changed

‎src/Init/Classical.lean‎

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop) (h : ∃
2121
noncomputable def choose {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α :=
2222
(indefiniteDescription p h).val
2323

24-
theorem chooseSpec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (choose h) :=
24+
theorem choose_spec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (choose h) :=
2525
(indefiniteDescription p h).property
2626

2727
/- Diaconescu's theorem: excluded middle from choice, Function extensionality and propositional extensionality. -/
@@ -32,14 +32,14 @@ theorem em (p : Prop) : p ∨ ¬p :=
3232
have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩;
3333
let u : Prop := choose exU;
3434
let v : Prop := choose exV;
35-
have uDef : U u := chooseSpec exU;
36-
have vDef : V v := chooseSpec exV;
35+
have uDef : U u := choose_spec exU;
36+
have vDef : V v := choose_spec exV;
3737
have notUvOrP : u ≠ v ∨ p :=
3838
match uDef, vDef with
3939
| Or.inr h, _ => Or.inr h
4040
| _, Or.inr h => Or.inr h
4141
| Or.inl hut, Or.inl hvf =>
42-
have hne : u ≠ v := hvf.symm ▸ hut.symm ▸ trueNeFalse
42+
have hne : u ≠ v := hvf.symm ▸ hut.symm ▸ true_ne_false
4343
Or.inl hne
4444
have pImpliesUv : p → u = v :=
4545
fun hp =>
@@ -58,14 +58,14 @@ theorem em (p : Prop) : p ∨ ¬p :=
5858
| Or.inl hne => Or.inr (mt pImpliesUv hne)
5959
| Or.inr h => Or.inl h
6060

61-
theorem existsTrueOfNonempty {α : Sort u} : Nonempty α → ∃ x : α, True
61+
theorem exists_true_of_nonempty {α : Sort u} : Nonempty α → ∃ x : α, True
6262
| ⟨x⟩ => ⟨x, trivial⟩
6363

64-
noncomputable def inhabitedOfNonempty {α : Sort u} (h : Nonempty α) : Inhabited α :=
64+
noncomputable def inhabited_of_nonempty {α : Sort u} (h : Nonempty α) : Inhabited α :=
6565
⟨choice h⟩
6666

67-
noncomputable def inhabitedOfExists {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : Inhabited α :=
68-
inhabitedOfNonempty (Exists.elim h (fun w hw => ⟨w⟩))
67+
noncomputable def inhabited_of_exists {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : Inhabited α :=
68+
inhabited_of_nonempty (Exists.elim h (fun w hw => ⟨w⟩))
6969

7070
/- all propositions are Decidable -/
7171
noncomputable scoped instance (priority := low) propDecidable (a : Prop) : Decidable a :=
@@ -81,7 +81,7 @@ noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α :=
8181

8282
noncomputable def typeDecidable (α : Sort u) : PSum α (α → False) :=
8383
match (propDecidable (Nonempty α)) with
84-
| (isTrue hp) => PSum.inl (@arbitrary _ (inhabitedOfNonempty hp))
84+
| (isTrue hp) => PSum.inl (@arbitrary _ (inhabited_of_nonempty hp))
8585
| (isFalse hn) => PSum.inr (fun a => absurd (Nonempty.intro a) hn)
8686

8787
noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop) (h : Nonempty α) : {x : α // (∃ y : α, p y) → p x} :=
@@ -97,19 +97,19 @@ noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop) (h
9797
noncomputable def epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α :=
9898
(strongIndefiniteDescription p h).val
9999

100-
theorem epsilonSpecAux {α : Sort u} (h : Nonempty α) (p : α → Prop) : (∃ y, p y) → p (@epsilon α h p) :=
100+
theorem epsilon_spec_aux {α : Sort u} (h : Nonempty α) (p : α → Prop) : (∃ y, p y) → p (@epsilon α h p) :=
101101
(strongIndefiniteDescription p h).property
102102

103-
theorem epsilonSpec {α : Sort u} {p : α → Prop} (hex : ∃ y, p y) : p (@epsilon α (nonemptyOfExists hex) p) :=
104-
epsilonSpecAux (nonemptyOfExists hex) p hex
103+
theorem epsilon_spec {α : Sort u} {p : α → Prop} (hex : ∃ y, p y) : p (@epsilon α (nonempty_of_exists hex) p) :=
104+
epsilon_spec_aux (nonempty_of_exists hex) p hex
105105

106-
theorem epsilonSingleton {α : Sort u} (x : α) : @epsilon α ⟨x⟩ (fun y => y = x) = x :=
107-
@epsilonSpec α (fun y => y = x) ⟨x, rfl⟩
106+
theorem epsilon_singleton {α : Sort u} (x : α) : @epsilon α ⟨x⟩ (fun y => y = x) = x :=
107+
@epsilon_spec α (fun y => y = x) ⟨x, rfl⟩
108108

109109
/- the axiom of choice -/
110110

111111
theorem axiomOfChoice {α : Sort u} {β : α → Sort v} {r : ∀ x, β x → Prop} (h : ∀ x, ∃ y, r x y) : ∃ (f : ∀ x, β x), ∀ x, r x (f x) :=
112-
⟨_, fun x => chooseSpec (h x)⟩
112+
⟨_, fun x => choose_spec (h x)⟩
113113

114114
theorem skolem {α : Sort u} {b : α → Sort v} {p : ∀ x, b x → Prop} : (∀ x, ∃ y, p x y) ↔ ∃ (f : ∀ x, b x), ∀ x, p x (f x) :=
115115
⟨axiomOfChoice, fun ⟨f, hw⟩ (x) => ⟨f x, hw x⟩⟩

‎src/Init/Control/Id.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,9 @@ instance : Monad Id where
1919
bind x f := f x
2020
map f x := f x
2121

22+
def hasBind : Bind Id :=
23+
inferInstance
24+
2225
@[inline] protected def run (x : Id α) : α := x
2326

2427
instance [OfNat α n] : OfNat (Id α) n :=

‎src/Init/Core.lean‎

Lines changed: 55 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -152,9 +152,9 @@ structure NonScalar where
152152
inductive PNonScalar : Type u where
153153
| mk (v : Nat) : PNonScalar
154154

155-
theorem natAddZero (n : Nat) : n + 0 = n := rfl
155+
@[simp] theorem Nat.add_zero (n : Nat) : n + 0 = n := rfl
156156

157-
theorem optParamEq (α : Sort u) (default : α) : optParam α default = α := rfl
157+
theorem optParam_eq (α : Sort u) (default : α) : optParam α default = α := rfl
158158

159159
/- Boolean operators -/
160160

@@ -178,7 +178,7 @@ def trivial : True := ⟨⟩
178178
theorem mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) : ¬a :=
179179
fun ha => h₂ (h₁ ha)
180180

181-
theorem notFalse : ¬False := id
181+
theorem not_false : ¬False := id
182182

183183
-- proof irrelevance is built in
184184
theorem proofIrrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ := rfl
@@ -194,7 +194,7 @@ theorem id.def {α : Sort u} (a : α) : id a = a := rfl
194194
theorem Eq.substr {α : Sort u} {p : α → Prop} {a b : α} (h₁ : b = a) (h₂ : p a) : p b :=
195195
h₁ ▸ h₂
196196

197-
theorem castEq {α : Sort u} (h : α = α) (a : α) : cast h a = a :=
197+
theorem cast_eq {α : Sort u} (h : α = α) (a : α) : cast h a = a :=
198198
rfl
199199

200200
@[reducible] def Ne {α : Sort u} (a b : α) :=
@@ -215,18 +215,18 @@ theorem Ne.irrefl (h : a ≠ a) : False := h rfl
215215
theorem Ne.symm (h : a ≠ b) : b ≠ a :=
216216
fun h₁ => h (h₁.symm)
217217

218-
theorem falseOfNe : a ≠ a → False := Ne.irrefl
218+
theorem false_of_ne : a ≠ a → False := Ne.irrefl
219219

220-
theorem neFalseOfSelf : p → p ≠ False :=
220+
theorem ne_false_of_self : p → p ≠ False :=
221221
fun (hp : p) (h : p = False) => h ▸ hp
222222

223-
theorem neTrueOfNot : ¬p → p ≠ True :=
223+
theorem ne_true_of_not : ¬p → p ≠ True :=
224224
fun (hnp : ¬p) (h : p = True) =>
225225
have : ¬True := h ▸ hnp
226226
this trivial
227227

228-
theorem trueNeFalse : ¬True = False :=
229-
neFalseOfSelf trivial
228+
theorem true_ne_false : ¬True = False :=
229+
ne_false_of_self trivial
230230

231231
end Ne
232232

@@ -248,37 +248,37 @@ theorem HEq.subst {p : (T : Sort u) → T → Prop} (h₁ : a ≅ b) (h₂ : p
248248
theorem HEq.symm (h : a ≅ b) : b ≅ a :=
249249
HEq.ndrecOn (motive := fun x => x ≅ a) h (HEq.refl a)
250250

251-
theorem heqOfEq (h : a = a') : a ≅ a' :=
251+
theorem heq_of_eq (h : a = a') : a ≅ a' :=
252252
Eq.subst h (HEq.refl a)
253253

254254
theorem HEq.trans (h₁ : a ≅ b) (h₂ : b ≅ c) : a ≅ c :=
255255
HEq.subst h₂ h₁
256256

257-
theorem heqOfHEqOfEq (h₁ : a ≅ b) (h₂ : b = b') : a ≅ b' :=
258-
HEq.trans h₁ (heqOfEq h₂)
257+
theorem heq_of_heq_of_eq (h₁ : a ≅ b) (h₂ : b = b') : a ≅ b' :=
258+
HEq.trans h₁ (heq_of_eq h₂)
259259

260-
theorem heqOfEqOfHEq (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b :=
261-
HEq.trans (heqOfEq h₁) h₂
260+
theorem heq_of_eq_of_heq (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b :=
261+
HEq.trans (heq_of_eq h₁) h₂
262262

263-
def typeEqOfHEq (h : a ≅ b) : α = β :=
263+
def type_eq_of_heq (h : a ≅ b) : α = β :=
264264
HEq.ndrecOn (motive := @fun (x : Sort u) _ => α = x) h (Eq.refl α)
265265

266266
end
267267

268-
theorem eqRecHEq {α : Sort u} {φ : α → Sort v} {a a' : α} : (h : a = a') → (p : φ a) → (Eq.recOn (motive := fun x _ => φ x) h p) ≅ p
268+
theorem eqRec_heq {α : Sort u} {φ : α → Sort v} {a a' : α} : (h : a = a') → (p : φ a) → (Eq.recOn (motive := fun x _ => φ x) h p) ≅ p
269269
| rfl, p => HEq.refl p
270270

271-
theorem heqOfEqRecEq {α β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ : Eq.rec (motive := fun α _ => α) a h₁ = b) : a ≅ b := by
271+
theorem heq_of_eqRec_eq {α β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ : Eq.rec (motive := fun α _ => α) a h₁ = b) : a ≅ b := by
272272
subst h₁
273-
apply heqOfEq
273+
apply heq_of_eq
274274
exact h₂
275275

276-
theorem castHEq {α β : Sort u} : (h : α = β) → (a : α) → cast h a ≅ a
276+
theorem cast_heq {α β : Sort u} : (h : α = β) → (a : α) → cast h a ≅ a
277277
| rfl, a => HEq.refl a
278278

279279
variable {a b c d : Prop}
280280

281-
theorem iffIffImpliesAndImplies (a b : Prop) : (a ↔ b) ↔ (a → b) ∧ (b → a) :=
281+
theorem iff_iff_implies_and_implies (a b : Prop) : (a ↔ b) ↔ (a → b) ∧ (b → a) :=
282282
Iff.intro (fun h => And.intro h.mp h.mpr) (fun h => Iff.intro h.left h.right)
283283

284284
theorem Iff.refl (a : Prop) : a ↔ a :=
@@ -306,12 +306,12 @@ theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop}
306306

307307
/- Decidable -/
308308

309-
theorem decideTrueEqTrue (h : Decidable True) : @decide True h = true :=
309+
theorem decide_true_eq_true (h : Decidable True) : @decide True h = true :=
310310
match h with
311311
| isTrue h => rfl
312312
| isFalse h => False.elim <| h ⟨⟩
313313

314-
theorem decideFalseEqFalse (h : Decidable False) : @decide False h = false :=
314+
theorem decide_false_eq_false (h : Decidable False) : @decide False h = false :=
315315
match h with
316316
| isFalse h => rfl
317317
| isTrue h => False.elim h
@@ -320,20 +320,20 @@ theorem decideFalseEqFalse (h : Decidable False) : @decide False h = false :=
320320
@[inline] def toBoolUsing {p : Prop} (d : Decidable p) : Bool :=
321321
decide p (h := d)
322322

323-
theorem toBoolUsingEqTrue {p : Prop} (d : Decidable p) (h : p) : toBoolUsing d = true :=
324-
decideEqTrue (s := d) h
323+
theorem toBoolUsing_eq_true {p : Prop} (d : Decidable p) (h : p) : toBoolUsing d = true :=
324+
decide_eq_true (s := d) h
325325

326-
theorem ofBoolUsingEqTrue {p : Prop} {d : Decidable p} (h : toBoolUsing d = true) : p :=
327-
ofDecideEqTrue (s := d) h
326+
theorem ofBoolUsing_eq_true {p : Prop} {d : Decidable p} (h : toBoolUsing d = true) : p :=
327+
of_decide_eq_true (s := d) h
328328

329-
theorem ofBoolUsingEqFalse {p : Prop} {d : Decidable p} (h : toBoolUsing d = false) : ¬ p :=
330-
ofDecideEqFalse (s := d) h
329+
theorem ofBoolUsing_eq_false {p : Prop} {d : Decidable p} (h : toBoolUsing d = false) : ¬ p :=
330+
of_decide_eq_false (s := d) h
331331

332332
instance : Decidable True :=
333333
isTrue trivial
334334

335335
instance : Decidable False :=
336-
isFalse notFalse
336+
isFalse not_false
337337

338338
namespace Decidable
339339
variable {p q : Prop}
@@ -349,10 +349,10 @@ theorem em (p : Prop) [Decidable p] : p ∨ ¬p :=
349349
theorem byContradiction [dec : Decidable p] (h : ¬p → False) : p :=
350350
byCases id (fun np => False.elim (h np))
351351

352-
theorem ofNotNot [Decidable p] : ¬ ¬ p → p :=
352+
theorem of_not_not [Decidable p] : ¬ ¬ p → p :=
353353
fun hnn => byContradiction (fun hn => absurd hn hnn)
354354

355-
theorem notAndIffOrNot (p q : Prop) [d₁ : Decidable p] [d₂ : Decidable q] : ¬ (p ∧ q) ↔ ¬ p ∨ ¬ q :=
355+
theorem not_and_iff_or_not (p q : Prop) [d₁ : Decidable p] [d₂ : Decidable q] : ¬ (p ∧ q) ↔ ¬ p ∨ ¬ q :=
356356
Iff.intro
357357
(fun h => match d₁, d₂ with
358358
| isTrue h₁, isTrue h₂ => absurd (And.intro h₁ h₂) h
@@ -396,28 +396,36 @@ instance {p q} [Decidable p] [Decidable q] : Decidable (p ↔ q) :=
396396

397397
/- if-then-else expression theorems -/
398398

399-
theorem ifPos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t e : α} : (ite c t e) = t :=
399+
theorem if_pos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t e : α} : (ite c t e) = t :=
400400
match h with
401401
| isTrue hc => rfl
402402
| isFalse hnc => absurd hc hnc
403403

404-
theorem ifNeg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t e : α} : (ite c t e) = e :=
404+
-- TODO: delete
405+
theorem ifPos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t e : α} : (ite c t e) = t :=
406+
if_pos hc
407+
408+
theorem if_neg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t e : α} : (ite c t e) = e :=
405409
match h with
406410
| isTrue hc => absurd hc hnc
407411
| isFalse hnc => rfl
408412

409-
theorem difPos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t : c → α} {e : ¬ c → α} : (dite c t e) = t hc :=
413+
-- TODO: delete
414+
theorem ifNeg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t e : α} : (ite c t e) = e :=
415+
if_neg hnc
416+
417+
theorem dif_pos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t : c → α} {e : ¬ c → α} : (dite c t e) = t hc :=
410418
match h with
411419
| isTrue hc => rfl
412420
| isFalse hnc => absurd hc hnc
413421

414-
theorem difNeg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t : c → α} {e : ¬ c → α} : (dite c t e) = e hnc :=
422+
theorem dif_neg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t : c → α} {e : ¬ c → α} : (dite c t e) = e hnc :=
415423
match h with
416424
| isTrue hc => absurd hc hnc
417425
| isFalse hnc => rfl
418426

419427
-- Remark: dite and ite are "defally equal" when we ignore the proofs.
420-
theorem difEqIf (c : Prop) [h : Decidable c] {α : Sort u} (t : α) (e : α) : dite c (fun h => t) (fun h => e) = ite c t e :=
428+
theorem dif_eq_if (c : Prop) [h : Decidable c] {α : Sort u} (t : α) (e : α) : dite c (fun h => t) (fun h => e) = ite c t e :=
421429
match h with
422430
| isTrue hc => rfl
423431
| isFalse hnc => rfl
@@ -448,7 +456,7 @@ protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂
448456
instance {α : Sort u} [Inhabited α] : Nonempty α :=
449457
⟨arbitrary⟩
450458

451-
theorem nonemptyOfExists {α : Sort u} {p : α → Prop} : Exists (fun x => p x) → Nonempty α
459+
theorem nonempty_of_exists {α : Sort u} {p : α → Prop} : Exists (fun x => p x) → Nonempty α
452460
| ⟨w, h⟩ => ⟨w⟩
453461

454462
/- Subsingleton -/
@@ -461,7 +469,7 @@ protected def Subsingleton.elim {α : Sort u} [h : Subsingleton α] : (a b : α)
461469

462470
protected def Subsingleton.helim {α β : Sort u} [h₁ : Subsingleton α] (h₂ : α = β) (a : α) (b : β) : a ≅ b := by
463471
subst h₂
464-
apply heqOfEq
472+
apply heq_of_eq
465473
apply Subsingleton.elim
466474

467475
instance (p : Prop) : Subsingleton p :=
@@ -580,7 +588,7 @@ instance prodHasDecidableLt
580588
: (s t : α × β) → Decidable (s < t) :=
581589
fun t s => inferInstanceAs (Decidable (_ ∨ _))
582590

583-
theorem Prod.ltDef [LT α] [LT β] (s t : α × β) : (s < t) = (s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)) :=
591+
theorem Prod.lt_def [LT α] [LT β] (s t : α × β) : (s < t) = (s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)) :=
584592
rfl
585593

586594
theorem Prod.ext (p : α × β) : (p.1, p.2) = p := by
@@ -592,7 +600,7 @@ def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂
592600

593601
/- Dependent products -/
594602

595-
theorem exOfPsig {α : Type u} {p : α → Prop} : (PSigma (fun x => p x)) → Exists (fun x => p x)
603+
theorem ex_of_PSigma {α : Type u} {p : α → Prop} : (PSigma (fun x => p x)) → Exists (fun x => p x)
596604
| ⟨x, hx⟩ => ⟨x, hx⟩
597605

598606
protected theorem PSigma.eta {α : Sort u} {β : α → Sort v} {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂}
@@ -669,7 +677,7 @@ gen_injective_theorems% Lean.Syntax
669677
/- Quotients -/
670678

671679
-- Iff can now be used to do substitutions in a calculation
672-
theorem iffSubst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) : p b :=
680+
theorem Iff.subst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) : p b :=
673681
Eq.subst (propext h₁) h₂
674682

675683
namespace Quot
@@ -697,7 +705,7 @@ protected theorem inductionOn {α : Sort u} {r : α → α → Prop} {motive : Q
697705
: motive q :=
698706
ind h q
699707

700-
theorem existsRep {α : Sort u} {r : α → α → Prop} (q : Quot r) : Exists (fun a => (Quot.mk r a) = q) :=
708+
theorem exists_rep {α : Sort u} {r : α → α → Prop} (q : Quot r) : Exists (fun a => (Quot.mk r a) = q) :=
701709
Quot.inductionOn (motive := fun q => Exists (fun a => (Quot.mk r a) = q)) q (fun a => ⟨a, rfl⟩)
702710

703711
section
@@ -751,7 +759,7 @@ protected abbrev hrecOn
751759
(c : (a b : α) → (p : r a b) → f a ≅ f b)
752760
: motive q :=
753761
Quot.recOn q f fun a b p => eqOfHEq <|
754-
have p₁ : Eq.ndrec (f a) (sound p) ≅ f a := eqRecHEq (sound p) (f a)
762+
have p₁ : Eq.ndrec (f a) (sound p) ≅ f a := eqRec_heq (sound p) (f a)
755763
HEq.trans p₁ (c a b p)
756764

757765
end
@@ -784,8 +792,8 @@ protected theorem inductionOn {α : Sort u} [s : Setoid α] {motive : Quotient s
784792
: motive q :=
785793
Quot.inductionOn q h
786794

787-
theorem existsRep {α : Sort u} [s : Setoid α] (q : Quotient s) : Exists (fun (a : α) => Quotient.mk a = q) :=
788-
Quot.existsRep q
795+
theorem exists_rep {α : Sort u} [s : Setoid α] (q : Quotient s) : Exists (fun (a : α) => Quotient.mk a = q) :=
796+
Quot.exists_rep q
789797

790798
section
791799
variable {α : Sort u}
@@ -895,11 +903,11 @@ private def rel [s : Setoid α] (q₁ q₂ : Quotient s) : Prop :=
895903
private theorem rel.refl [s : Setoid α] (q : Quotient s) : rel q q :=
896904
Quot.inductionOn (motive := fun q => rel q q) q (fun a => Setoid.refl a)
897905

898-
private theorem eqImpRel [s : Setoid α] {q₁ q₂ : Quotient s} : q₁ = q₂ → rel q₁ q₂ :=
906+
private theorem rel_of_eq [s : Setoid α] {q₁ q₂ : Quotient s} : q₁ = q₂ → rel q₁ q₂ :=
899907
fun h => Eq.ndrecOn h (rel.refl q₁)
900908

901909
theorem exact [s : Setoid α] {a b : α} : Quotient.mk a = Quotient.mk b → a ≈ b :=
902-
fun h => eqImpRel h
910+
fun h => rel_of_eq h
903911

904912
end Exact
905913

0 commit comments

Comments
 (0)