From ba6fcd7b74196b523c48d29533a9ef5286730404 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 7 Aug 2021 13:23:41 -0700
Subject: [PATCH] chore: update stage0

---
 stage0/src/Init/Core.lean             | 12 ++----------
 stage0/src/Init/Data/Array/Basic.lean |  5 -----
 stage0/src/Init/Prelude.lean          |  8 --------
 stage0/src/Init/SimpLemmas.lean       | 18 +-----------------
 4 files changed, 3 insertions(+), 40 deletions(-)

diff --git a/stage0/src/Init/Core.lean b/stage0/src/Init/Core.lean
index c17b6600bc..e9e8779135 100644
--- a/stage0/src/Init/Core.lean
+++ b/stage0/src/Init/Core.lean
@@ -240,7 +240,7 @@ theorem HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} 
   @HEq.rec α a (fun b _ => motive b) m β b h
 
 theorem HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≅ b) (h₂ : p a) : p b :=
-  eqOfHEq h₁ ▸ h₂
+  eq_of_heq h₁ ▸ h₂
 
 theorem HEq.subst {p : (T : Sort u) → T → Prop} (h₁ : a ≅ b) (h₂ : p α a) : p β b :=
   HEq.ndrecOn h₁ h₂
@@ -401,19 +401,11 @@ theorem if_pos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t e : α} :
   | isTrue  hc  => rfl
   | isFalse hnc => absurd hc hnc
 
--- TODO: delete
-theorem ifPos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t e : α} : (ite c t e) = t :=
-  if_pos hc
-
 theorem if_neg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t e : α} : (ite c t e) = e :=
   match h with
   | isTrue hc   => absurd hc hnc
   | isFalse hnc => rfl
 
--- TODO: delete
-theorem ifNeg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t e : α} : (ite c t e) = e :=
-  if_neg hnc
-
 theorem dif_pos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t : c → α} {e : ¬ c → α} : (dite c t e) = t hc :=
   match h with
   | isTrue  hc  => rfl
@@ -758,7 +750,7 @@ protected abbrev hrecOn
     (f : (a : α) → motive (Quot.mk r a))
     (c : (a b : α) → (p : r a b) → f a ≅ f b)
     : motive q :=
-  Quot.recOn q f fun a b p => eqOfHEq <|
+  Quot.recOn q f fun a b p => eq_of_heq <|
     have p₁ : Eq.ndrec (f a) (sound p) ≅ f a := eqRec_heq (sound p) (f a)
     HEq.trans p₁ (c a b p)
 
diff --git a/stage0/src/Init/Data/Array/Basic.lean b/stage0/src/Init/Data/Array/Basic.lean
index 2407672b85..8accb2c22f 100644
--- a/stage0/src/Init/Data/Array/Basic.lean
+++ b/stage0/src/Init/Data/Array/Basic.lean
@@ -727,11 +727,6 @@ theorem toArrayLit_eq (a : Array α) (n : Nat) (hsz : a.size = n) : a = toArrayL
   Then using Array.extLit, we have that a = List.toArray <| toListLitAux a n hsz n _ []
   -/
 
--- TODO: delete
-theorem toArrayLitEq (a : Array α) (n : Nat) (hsz : a.size = n) : a = toArrayLit a n hsz :=
-  -- TODO: this is painful to prove without proper automation
-  sorry
-
 partial def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) : Nat → Bool
   | i =>
     if h : i < as.size then
diff --git a/stage0/src/Init/Prelude.lean b/stage0/src/Init/Prelude.lean
index 234bd12d32..c26993f12f 100644
--- a/stage0/src/Init/Prelude.lean
+++ b/stage0/src/Init/Prelude.lean
@@ -118,10 +118,6 @@ theorem eq_of_heq {α : Sort u} {a a' : α} (h : HEq a a') : Eq a a' :=
         h₁
   this α α a a' h rfl
 
--- TODO: delete
-theorem eqOfHEq {α : Sort u} {a a' : α} (h : HEq a a') : Eq a a' :=
-  eq_of_heq h
-
 structure Prod (α : Type u) (β : Type v) where
   fst : α
   snd : β
@@ -270,10 +266,6 @@ theorem of_decide_eq_true [s : Decidable p] : Eq (decide p) true → p := fun h
   | isTrue  h₁ => h₁
   | isFalse h₁ => absurd h (ne_true_of_eq_false (decide_eq_false h₁))
 
--- TODO: delete
-theorem ofDecideEqTrue [s : Decidable p] : Eq (decide p) true → p :=
-  of_decide_eq_true
-
 theorem of_decide_eq_false [s : Decidable p] : Eq (decide p) false → Not p := fun h =>
   match (generalizing := false) s with
   | isTrue  h₁ => absurd h (ne_false_of_eq_true (decide_eq_true h₁))
diff --git a/stage0/src/Init/SimpLemmas.lean b/stage0/src/Init/SimpLemmas.lean
index c87e6a47aa..b5ce6742cf 100644
--- a/stage0/src/Init/SimpLemmas.lean
+++ b/stage0/src/Init/SimpLemmas.lean
@@ -14,29 +14,17 @@ import Init.Core
 theorem of_eq_true (h : p = True) : p :=
   h ▸ trivial
 
--- TODO: delete
-theorem ofEqTrue (h : p = True) : p :=
-  of_eq_true h
-
 theorem eq_true (h : p) : p = True :=
   propext <| Iff.intro (fun _ => trivial) (fun _ => h)
 
 theorem eq_false (h : ¬ p) : p = False :=
   propext <| Iff.intro (fun h' => absurd h' h) (fun h' => False.elim h')
 
--- TODO: delete
-theorem eqFalse (h : ¬ p) : p = False :=
-  propext <| Iff.intro (fun h' => absurd h' h) (fun h' => False.elim h')
-
 theorem eq_false' (h : p → False) : p = False :=
   propext <| Iff.intro (fun h' => absurd h' h) (fun h' => False.elim h')
 
 theorem eq_true_of_decide {p : Prop} {s : Decidable p} (h : decide p = true) : p = True :=
-  propext <| Iff.intro (fun h => trivial) (fun _ => ofDecideEqTrue h)
-
--- TODO: delete
-theorem eqTrueOfDecide {p : Prop} {s : Decidable p} (h : decide p = true) : p = True :=
-  propext <| Iff.intro (fun h => trivial) (fun _ => ofDecideEqTrue h)
+  propext <| Iff.intro (fun h => trivial) (fun _ => of_decide_eq_true h)
 
 theorem eq_false_of_decide {p : Prop} {s : Decidable p} (h : decide p = false) : p = False :=
   propext <| Iff.intro (fun h' => absurd h' (of_decide_eq_false h)) (fun h => False.elim h)
@@ -44,10 +32,6 @@ theorem eq_false_of_decide {p : Prop} {s : Decidable p} (h : decide p = false) :
 theorem implies_congr {p₁ p₂ : Sort u} {q₁ q₂ : Sort v} (h₁ : p₁ = p₂) (h₂ : q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂) :=
   h₁ ▸ h₂ ▸ rfl
 
--- TODO: delete
-theorem impCongr {p₁ p₂ : Sort u} {q₁ q₂ : Sort v} (h₁ : p₁ = p₂) (h₂ : q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂) :=
-  h₁ ▸ h₂ ▸ rfl
-
 theorem implies_congr_ctx {p₁ p₂ q₁ q₂ : Prop} (h₁ : p₁ = p₂) (h₂ : p₂ → q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂) :=
   propext <| Iff.intro
     (fun h hp₂ =>