chore(*): bump to lean 3.19.0c, fin is now a subtype (#3955)

* Some `decidable.*` order theorems have been moved to core.

* `fin` is now a subtype. 
This means that the whnf of `fin n` is now `{i // i < n}`.
Also, the coercion `fin n → nat` is now preferred over `subtype.val`.
The entire library has been refactored accordingly. (Although I probably missed some cases.)

* `in_current_file'` was removed since the bug in 
`in_current_file` was fixed in core.

* The syntax of `guard_hyp` in core was changed from
`guard_hyp h := t` to `guard_hyp h : t`, so the syntax
for the related `guard_hyp'`, `match_hyp` and
`guard_hyp_strict` tactics in `tactic.interactive` was changed as well.



Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Author: jcommelin

archive/100-theorems-list/73_ascending_descending_sequences.lean

@@ -104,7 +104,8 @@ begin
         refine ⟨_, _, _⟩,
         { rw mem_powerset, apply subset_univ },
         -- It ends at `j` since `i < j`.
-        { rw [max_insert, ht₁.2.1, option.lift_or_get_some_some, max_eq_left, with_top.some_eq_coe],
+        { convert max_insert,
+          rw [ht₁.2.1, option.lift_or_get_some_some, max_eq_left, with_top.some_eq_coe],
           apply le_of_lt ‹i < j› },
         -- To show it's increasing (i.e., `f` is monotone increasing on `t.insert j`), we do cases on
         -- what the possibilities could be - either in `t` or equals `j`.

archive/100-theorems-list/82_cubing_a_cube.lean

@@ -264,7 +264,7 @@ begin
   rcases v.1 c.b_mem_bottom with ⟨_, ⟨i, rfl⟩, hi⟩,
   have h2i : i ∈ bcubes cs c := ⟨hi.1.symm, v.2.1 i hi.1.symm ⟨tail c.b, hi.2, λ j, c.b_mem_side j.succ⟩⟩,
   let j : fin (n+1) := ⟨2, h.2.2.2.2⟩,
-  have hj : 0 ≠ j := by { intro h', have := congr_arg fin.val h', contradiction },
+  have hj : 0 ≠ j := by { simp only [fin.ext_iff, ne.def], contradiction },
   let p : fin (n+1) → ℝ := λ j', if j' = j then c.b j + (cs i).w else c.b j',
   have hp : p ∈ c.bottom,
   { split, { simp only [bottom, p, if_neg hj] },

leanpkg.toml

@@ -1,7 +1,7 @@
 [package]
 name = "mathlib"
 version = "0.1"
-lean_version = "leanprover-community/lean:3.18.4"
+lean_version = "leanprover-community/lean:3.19.0"
 path = "src"
 
 [dependencies]

src/algebra/category/Mon/basic.lean

@@ -105,7 +105,7 @@ example (R : CommMon.{u}) : R ⟶ R :=
 { to_fun := λ x,
   begin
     match_target (R : Type u),
-    match_hyp x := (R : Type u),
+    match_hyp x : (R : Type u),
     exact x * x
   end ,
   map_one' := by simp,

src/algebra/linear_recurrence.lean

@@ -62,7 +62,7 @@ def is_solution (u : ℕ → α) :=
   We will prove this is the only such solution. -/
 def mk_sol (init : fin E.order → α) : ℕ → α
 | n := if h : n < E.order then init ⟨n, h⟩ else
-  ∑ k : fin E.order, have n - E.order + k.1 < n, by have := k.2; omega,
+  ∑ k : fin E.order, have n - E.order + k < n, by have := k.is_lt; omega,
     E.coeffs k * mk_sol (n - E.order + k)
 
 /-- `E.mk_sol` indeed gives solutions to `E`. -/
@@ -71,7 +71,7 @@ lemma is_sol_mk_sol (init : fin E.order → α) : E.is_solution (E.mk_sol init)
 
 /-- `E.mk_sol init`'s first `E.order` terms are `init`. -/
 lemma mk_sol_eq_init (init : fin E.order → α) : ∀ n : fin E.order, E.mk_sol init n = init n :=
-  λ n, by rw mk_sol; simp [fin.coe_eq_val, n.2]
+  λ n, by { rw mk_sol, simp only [n.is_lt, dif_pos, fin.mk_coe] }
 
 /-- If `u` is a solution to `E` and `init` designates its first `E.order` values,
   then `∀ n, u n = E.mk_sol init n`. -/
@@ -84,7 +84,7 @@ lemma eq_mk_of_is_sol_of_eq_init {u : ℕ → α} {init : fin E.order → α}
     rw [mk_sol, ← nat.sub_add_cancel (le_of_not_lt h'), h (n-E.order)],
     simp [h'],
     congr' with k,
-    exact have wf : n - E.order + k.1 < n, by have := k.2; omega,
+    exact have wf : n - E.order + k < n, by have := k.is_lt; omega,
       by rw eq_mk_of_is_sol_of_eq_init
   end
 
@@ -140,7 +140,7 @@ end
 /-- `E.tuple_succ` maps `![s₀, s₁, ..., sₙ]` to `![s₁, ..., sₙ, ∑ (E.coeffs i) * sᵢ]`,
   where `n := E.order`. -/
 def tuple_succ : (fin E.order → α) →ₗ[α] (fin E.order → α) :=
-{ to_fun := λ X i, if h : i.1 + 1 < E.order then X ⟨i+1, h⟩ else (∑ i, E.coeffs i * X i),
+{ to_fun := λ X i, if h : (i : ℕ) + 1 < E.order then X ⟨i+1, h⟩ else (∑ i, E.coeffs i * X i),
   map_add' := λ x y,
     begin
       ext i,

src/algebra/order.lean

@@ -117,12 +117,8 @@ lemma lt_of_not_ge' [linear_order α] {a b : α} (h : ¬ b ≤ a) : a < b :=
 lemma lt_iff_not_ge' [linear_order α] {x y : α} : x < y ↔ ¬ y ≤ x :=
 ⟨not_le_of_gt, lt_of_not_ge'⟩
 
-@[simp] lemma not_lt [linear_order α] {a b : α} : ¬ a < b ↔ b ≤ a := ⟨le_of_not_gt, not_lt_of_ge⟩
-
 lemma le_of_not_lt [linear_order α] {a b : α} : ¬ a < b → b ≤ a := not_lt.1
 
-@[simp] lemma not_le [linear_order α] {a b : α} : ¬ a ≤ b ↔ b < a := lt_iff_not_ge'.symm
-
 lemma lt_or_le [linear_order α] : ∀ a b : α, a < b ∨ b ≤ a := lt_or_ge
 lemma le_or_lt [linear_order α] : ∀ a b : α, a ≤ b ∨ b < a := le_or_gt
 
@@ -208,62 +204,6 @@ calc  c
 
 namespace decidable
 
--- See Note [decidable namespace]
-lemma lt_or_eq_of_le [partial_order α] [@decidable_rel α (≤)] {a b : α} (hab : a ≤ b) : a < b ∨ a = b :=
-if hba : b ≤ a then or.inr (le_antisymm hab hba)
-else or.inl (lt_of_le_not_le hab hba)
-
--- See Note [decidable namespace]
-lemma eq_or_lt_of_le [partial_order α] [@decidable_rel α (≤)] {a b : α} (hab : a ≤ b) : a = b ∨ a < b :=
-(lt_or_eq_of_le hab).swap
-
--- See Note [decidable namespace]
-lemma le_iff_lt_or_eq [partial_order α] [@decidable_rel α (≤)] {a b : α} : a ≤ b ↔ a < b ∨ a = b :=
-⟨lt_or_eq_of_le, le_of_lt_or_eq⟩
-
--- See Note [decidable namespace]
-lemma le_of_not_lt [decidable_linear_order α] {a b : α} (h : ¬ b < a) : a ≤ b :=
-decidable.by_contradiction $ λ h', h $ lt_of_le_not_le ((le_total _ _).resolve_right h') h'
-
--- See Note [decidable namespace]
-lemma not_lt [decidable_linear_order α] {a b : α} : ¬ a < b ↔ b ≤ a :=
-⟨le_of_not_lt, not_lt_of_ge⟩
-
--- See Note [decidable namespace]
-lemma lt_or_le [decidable_linear_order α] (a b : α) : a < b ∨ b ≤ a :=
-if hba : b ≤ a then or.inr hba else or.inl $ not_le.1 hba
-
--- See Note [decidable namespace]
-lemma le_or_lt [decidable_linear_order α] (a b : α) : a ≤ b ∨ b < a :=
-(lt_or_le b a).swap
-
--- See Note [decidable namespace]
-lemma lt_trichotomy [decidable_linear_order α] (a b : α) : a < b ∨ a = b ∨ b < a :=
-(lt_or_le _ _).imp_right $ λ h, (eq_or_lt_of_le h).imp_left eq.symm
-
--- See Note [decidable namespace]
-lemma lt_or_gt_of_ne [decidable_linear_order α] {a b : α} (h : a ≠ b) : a < b ∨ b < a :=
-(lt_trichotomy a b).imp_right $ λ h', h'.resolve_left h
-
-/-- Perform a case-split on the ordering of `x` and `y` in a decidable linear order. -/
--- See Note [decidable namespace]
-def lt_by_cases [decidable_linear_order α] (x y : α) {P : Sort*}
-  (h₁ : x < y → P) (h₂ : x = y → P) (h₃ : y < x → P) : P :=
-begin
-  by_cases h : x < y, { exact h₁ h },
-  by_cases h' : y < x, { exact h₃ h' },
-  apply h₂, apply le_antisymm; apply le_of_not_gt; assumption
-end
-
--- See Note [decidable namespace]
-lemma ne_iff_lt_or_gt [decidable_linear_order α] {a b : α} : a ≠ b ↔ a < b ∨ b < a :=
-⟨lt_or_gt_of_ne, λo, o.elim ne_of_lt ne_of_gt⟩
-
--- See Note [decidable namespace]
-lemma le_imp_le_of_lt_imp_lt {β} [preorder α] [decidable_linear_order β]
-  {a b : α} {c d : β} (H : d < c → b < a) (h : a ≤ b) : c ≤ d :=
-le_of_not_lt $ λ h', (H h').not_le h
-
 -- See Note [decidable namespace]
 lemma le_imp_le_iff_lt_imp_lt {β} [linear_order α] [decidable_linear_order β]
   {a b : α} {c d : β} : (a ≤ b → c ≤ d) ↔ (d < c → b < a) :=

src/analysis/analytic/composition.lean

@@ -101,7 +101,7 @@ begin
   intros j hjn hj1,
   obtain rfl : j = 0, { linarith },
   refine congr_arg v _,
-  rw [fin.ext_iff, fin.cast_le_val, composition.ones_embedding],
+  rw [fin.ext_iff, fin.coe_cast_le, composition.ones_embedding, fin.coe_mk],
 end
 
 /-- Technical lemma stating how `p.apply_composition` commutes with updating variables. This
@@ -295,7 +295,7 @@ begin
     intros,
     rw apply_composition_ones,
     refine congr_arg v _,
-    rw [fin.ext_iff, fin.cast_le_val], },
+    rw [fin.ext_iff, fin.coe_cast_le, fin.coe_mk, fin.coe_mk], },
   show ∀ (b : composition n),
     b ∈ finset.univ → b ≠ composition.ones n → comp_along_composition p (id 𝕜 E) b = 0,
   { assume b _ hb,
@@ -520,13 +520,13 @@ end
 lemma comp_change_of_variables_blocks_fun
   (N : ℕ) {i : Σ n, (fin n) → ℕ} (hi : i ∈ comp_partial_sum_source N) (j : fin i.1) :
   (comp_change_of_variables N i hi).2.blocks_fun
-    ⟨j.val, (comp_change_of_variables_length N hi).symm ▸ j.2⟩ = i.2 j :=
+    ⟨j, (comp_change_of_variables_length N hi).symm ▸ j.2⟩ = i.2 j :=
 begin
   rcases i with ⟨n, f⟩,
   dsimp [composition.blocks_fun, composition.blocks, comp_change_of_variables],
   simp only [map_of_fn, nth_le_of_fn', function.comp_app],
   apply congr_arg,
-  rw fin.ext_iff
+  rw [fin.ext_iff, fin.mk_coe]
 end
 
 /-- Target set in the change of variables to compute the composition of partial sums of formal
@@ -546,7 +546,8 @@ begin
   { dsimp [comp_change_of_variables],
     rw composition.sigma_eq_iff_blocks_eq,
     simp only [composition.blocks_fun, composition.blocks, subtype.coe_eta, nth_le_map'],
-    conv_lhs { rw ← of_fn_nth_le c.blocks } }
+    conv_lhs { rw ← of_fn_nth_le c.blocks },
+    simp only [fin.val_eq_coe], refl, /- where does this fin.val come from? -/ }
 end
 
 /-- Target set in the change of variables to compute the composition of partial sums of formal
@@ -861,8 +862,8 @@ begin
   induction h,
   simp only [true_and, eq_self_iff_true, heq_iff_eq],
   ext i : 2,
-  have : nth_le (of_fn (λ (i : fin (composition.length a)), (b i).blocks)) i.1 (by simp [i.2]) =
-         nth_le (of_fn (λ (i : fin (composition.length a)), (b' i).blocks)) i.1 (by simp [i.2]) :=
+  have : nth_le (of_fn (λ (i : fin (composition.length a)), (b i).blocks)) i (by simp [i.is_lt]) =
+         nth_le (of_fn (λ (i : fin (composition.length a)), (b' i).blocks)) i (by simp [i.is_lt]) :=
     nth_le_of_eq H _,
   rwa [nth_le_of_fn, nth_le_of_fn] at this
 end
@@ -899,22 +900,23 @@ two compositions `a` of `n` and `b` of `a.length`, and an index `i` bounded by t
 def sigma_composition_aux (a : composition n) (b : composition a.length)
   (i : fin (a.gather b).length) :
   composition ((a.gather b).blocks_fun i) :=
-{ blocks := nth_le (a.blocks.split_wrt_composition b) i.val
+{ blocks := nth_le (a.blocks.split_wrt_composition b) i
     (by { rw [length_split_wrt_composition, ← length_gather], exact i.2 }),
   blocks_pos := assume i hi, a.blocks_pos
     (by { rw ← a.blocks.join_split_wrt_composition b, exact mem_join_of_mem (nth_le_mem _ _ _) hi }),
-  blocks_sum := by simp only [composition.blocks_fun, nth_le_map', composition.gather] }
+  blocks_sum := by simp only [composition.blocks_fun, nth_le_map', composition.gather, fin.val_eq_coe] }
+  /- Where did the fin.val come from in the proof on the preceding line? -/
 
 lemma length_sigma_composition_aux (a : composition n) (b : composition a.length) (i : fin b.length) :
-  composition.length (composition.sigma_composition_aux a b ⟨i.val, (length_gather a b).symm ▸ i.2⟩) =
+  composition.length (composition.sigma_composition_aux a b ⟨i, (length_gather a b).symm ▸ i.2⟩) =
   composition.blocks_fun b i :=
-show list.length (nth_le (split_wrt_composition a.blocks b) i.val _) = blocks_fun b i,
+show list.length (nth_le (split_wrt_composition a.blocks b) i _) = blocks_fun b i,
 by { rw [nth_le_map_rev list.length, nth_le_of_eq (map_length_split_wrt_composition _ _)], refl }
 
 lemma blocks_fun_sigma_composition_aux (a : composition n) (b : composition a.length)
   (i : fin b.length) (j : fin (blocks_fun b i)) :
-  blocks_fun (sigma_composition_aux a b ⟨i.val, (length_gather a b).symm ▸ i.2⟩)
-      ⟨j.val, (length_sigma_composition_aux a b i).symm ▸ j.2⟩ = blocks_fun a (embedding b i j) :=
+  blocks_fun (sigma_composition_aux a b ⟨i, (length_gather a b).symm ▸ i.2⟩)
+      ⟨j, (length_sigma_composition_aux a b i).symm ▸ j.2⟩ = blocks_fun a (embedding b i j) :=
 show nth_le (nth_le _ _ _) _ _ = nth_le a.blocks _ _,
 by { rw [nth_le_of_eq (nth_le_split_wrt_composition _ _ _), nth_le_drop', nth_le_take'], refl }
 
@@ -951,14 +953,14 @@ begin
       rw [take_append_drop] } },
   { have A : j < blocks_fun b ⟨i, hi⟩ := lt_trans (lt_add_one j) hj,
     have B : j < length (sigma_composition_aux a b ⟨i, (length_gather a b).symm ▸ hi⟩),
-      by { convert A, rw ← length_sigma_composition_aux },
+      by { convert A, rw [← length_sigma_composition_aux], refl },
     have C : size_up_to b i + j < size_up_to b (i + 1),
     { simp only [size_up_to_succ b hi, add_lt_add_iff_left],
       exact A },
     have D : size_up_to b i + j < length a := lt_of_lt_of_le C (b.size_up_to_le _),
     have : size_up_to b i + nat.succ j = (size_up_to b i + j).succ := rfl,
     rw [this, size_up_to_succ _ D, IHj A, size_up_to_succ _ B],
-    simp only [sigma_composition_aux, add_assoc, add_left_inj],
+    simp only [sigma_composition_aux, add_assoc, add_left_inj, fin.coe_mk],
     rw [nth_le_of_eq (nth_le_split_wrt_composition _ _ _), nth_le_drop', nth_le_take _ _ C] }
 end
 
@@ -1014,7 +1016,7 @@ def sigma_equiv_sigma_pi (n : ℕ) :
       { exact B },
       { apply (fin.heq_fun_iff B).2 (λ i, _),
         rw [sigma_composition_aux, composition.length, nth_le_map_rev list.length,
-            nth_le_of_eq (map_length_split_wrt_composition _ _)] } }
+            nth_le_of_eq (map_length_split_wrt_composition _ _)], refl } }
   end,
   right_inv :=
   begin