feat(*): Upgrade to lean 3.44.1c (#14984)

The changes are:

* `reflected a` is now spelt `reflected _ a`, as the argument was made explicit to resolve type resolution issues. We need to add new instances for `with_top` and `with_bot` as these are no longer found via the `option` instance. These new instances are an improvement, as they can now use `bot` and `top` instead of `none`.
* Some nat order lemmas in core have been renamed or had their argument explicitness adjusted.
* `dsimp` now applies `iff` lemmas, which means it can end up making more progress than it used to. This appears to impact `split_ifs` too.
* `opposite.op_inj_iff` shouldn't be proved until after `opposite` is irreducible (where `iff.rfl` no longer works as a proof), otherwise `dsimp` is tricked into unfolding the irreducibility which puts the goal state in a form where no further lemmas can apply.

We skip Lean 3.44.0c because the support in that version for `iff` lemmas in `dsimp` had some unintended consequences which required many undesirable changes.

archive/100-theorems-list/45_partition.lean

@@ -409,7 +409,7 @@ begin
     rw nat.not_even_iff at hi₂,
     rw [hi₂, add_comm] at this,
     refine ⟨i / 2, _, this⟩,
-    rw nat.div_lt_iff_lt_mul _ _ zero_lt_two,
+    rw nat.div_lt_iff_lt_mul zero_lt_two,
     exact lt_of_le_of_lt hin h },
   { rintro ⟨a, -, rfl⟩,
     rw even_iff_two_dvd,

leanpkg.toml

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

src/algebra/geom_sum.lean

@@ -361,7 +361,7 @@ calc
 lemma nat.geom_sum_le {b : ℕ} (hb : 2 ≤ b) (a n : ℕ) :
   ∑ i in range n, a/b^i ≤ a * b/(b - 1) :=
 begin
-  refine (nat.le_div_iff_mul_le _ _ $ tsub_pos_of_lt hb).2 _,
+  refine (nat.le_div_iff_mul_le $ tsub_pos_of_lt hb).2 _,
   cases n,
   { rw [sum_range_zero, zero_mul],
     exact nat.zero_le _ },

src/algebraic_geometry/gluing.lean

@@ -106,7 +106,7 @@ begin
   refine ⟨_, _ ≫ D.to_LocallyRingedSpace_glue_data.to_glue_data.ι i, _⟩,
   swap, exact (D.U i).affine_cover.map y,
   split,
-  { dsimp,
+  { dsimp [-set.mem_range],
     rw [coe_comp, set.range_comp],
     refine set.mem_image_of_mem _ _,
     exact (D.U i).affine_cover.covers y },

src/algebraic_topology/simplex_category.lean

@@ -190,7 +190,7 @@ begin
   rcases j with ⟨j, _⟩,
   rcases k with ⟨k, _⟩,
   simp only [subtype.mk_le_mk, fin.cast_succ_mk] at H,
-  dsimp, simp only [if_congr, subtype.mk_lt_mk, dif_ctx_congr],
+  dsimp,
   split_ifs,
   -- Most of the goals can now be handled by `linarith`,
   -- but we have to deal with two of them by hand.
@@ -212,7 +212,7 @@ begin
   { dsimp [δ, σ, fin.succ_above, fin.pred_above], simpa [fin.pred_above] with push_cast },
   rcases i with ⟨i, _⟩,
   rcases j with ⟨j, _⟩,
-  dsimp, simp only [if_congr, subtype.mk_lt_mk],
+  dsimp,
   split_ifs; { simp at *; linarith, },
 end
 

src/combinatorics/simple_graph/regularity/bound.lean

@@ -83,7 +83,7 @@ by exact_mod_cast
 lemma a_add_one_le_four_pow_parts_card : a + 1 ≤ 4^P.parts.card :=
 begin
   have h : 1 ≤ 4^P.parts.card := one_le_pow_of_one_le (by norm_num) _,
-  rw [step_bound, ←nat.div_div_eq_div_mul, nat.add_le_to_le_sub _ h, tsub_le_iff_left,
+  rw [step_bound, ←nat.div_div_eq_div_mul, ←nat.le_sub_iff_right h, tsub_le_iff_left,
     ←nat.add_sub_assoc h],
   exact nat.le_pred_of_lt (nat.lt_div_mul_add h),
 end

src/data/fin/tuple/basic.lean

@@ -579,8 +579,8 @@ lemma find_spec : Π {n : ℕ} (p : fin n → Prop) [decidable_pred p] {i : fin
   { rw h at hi,
     dsimp at hi,
     split_ifs at hi with hl hl,
-    { exact option.some_inj.1 hi ▸ hl },
-    { exact option.no_confusion hi } },
+    { exact hi ▸ hl },
+    { exact hi.elim } },
   { rw h at hi,
     rw [← option.some_inj.1 hi],
     exact find_spec _ h }
@@ -625,10 +625,10 @@ lemma find_min : Π {n : ℕ} {p : fin n → Prop} [decidable_pred p] {i : fin n
   cases h : find (λ i : fin n, (p (i.cast_lt (nat.lt_succ_of_lt i.2)))) with k,
   { rw [h] at hi,
     split_ifs at hi with hl hl,
-    { obtain rfl := option.some_inj.1 hi,
+    { subst hi,
       rw [find_eq_none_iff] at h,
       exact h ⟨j, hj⟩ hpj },
-    { exact option.no_confusion hi } },
+    { exact hi.elim } },
   { rw h at hi,
     dsimp at hi,
     obtain rfl := option.some_inj.1 hi,

src/data/fin/vec_notation.lean

@@ -147,12 +147,12 @@ by { refine fin.forall_fin_one.2 _ i, refl }
 lemma cons_fin_one (x : α) (u : fin 0 → α) : vec_cons x u = (λ _, x) :=
 funext (cons_val_fin_one x u)
 
-meta instance _root_.pi_fin.reflect [reflected_univ.{u}] [reflected α] [has_reflect α] :
+meta instance _root_.pi_fin.reflect [reflected_univ.{u}] [reflected _ α] [has_reflect α] :
   Π {n}, has_reflect (fin n → α)
 | 0 v := (subsingleton.elim vec_empty v).rec
-    ((by reflect_name : reflected (@vec_empty.{u})).subst `(α))
+    ((by reflect_name : reflected _ (@vec_empty.{u})).subst `(α))
 | (n + 1) v := (cons_head_tail v).rec $
-    (by reflect_name : reflected @vec_cons.{u}).subst₄ `(α) `(n) `(_) (_root_.pi_fin.reflect _)
+    (by reflect_name : reflected _ @vec_cons.{u}).subst₄ `(α) `(n) `(_) (_root_.pi_fin.reflect _)
 
 /-! ### Numeral (`bit0` and `bit1`) indices
 The following definitions and `simp` lemmas are to allow any

src/data/int/basic.lean

@@ -517,14 +517,14 @@ have ∀ {k n : ℕ} {a : ℤ}, (a + n * k.succ) / k.succ = a / k.succ + n, from
                   n - (m / k.succ + 1 : ℕ), begin
   cases lt_or_ge m (n*k.succ) with h h,
   { rw [← int.coe_nat_sub h,
-        ← int.coe_nat_sub ((nat.div_lt_iff_lt_mul _ _ k.succ_pos).2 h)],
+        ← int.coe_nat_sub ((nat.div_lt_iff_lt_mul k.succ_pos).2 h)],
     apply congr_arg of_nat,
     rw [mul_comm, nat.mul_sub_div], rwa mul_comm },
   { change (↑(n * nat.succ k) - (m + 1) : ℤ) / ↑(nat.succ k) =
            ↑n - ((m / nat.succ k : ℕ) + 1),
     rw [← sub_sub, ← sub_sub, ← neg_sub (m:ℤ), ← neg_sub _ (n:ℤ),
         ← int.coe_nat_sub h,
-        ← int.coe_nat_sub ((nat.le_div_iff_mul_le _ _ k.succ_pos).2 h),
+        ← int.coe_nat_sub ((nat.le_div_iff_mul_le k.succ_pos).2 h),
         ← neg_succ_of_nat_coe', ← neg_succ_of_nat_coe'],
     { apply congr_arg neg_succ_of_nat,
       rw [mul_comm, nat.sub_mul_div], rwa mul_comm } }
@@ -777,7 +777,7 @@ end,
     { change m.succ * n.succ ≤ _,
       rw [mul_left_comm],
       apply nat.mul_le_mul_left,
-      apply (nat.div_lt_iff_lt_mul _ _ k.succ_pos).1,
+      apply (nat.div_lt_iff_lt_mul k.succ_pos).1,
       apply nat.lt_succ_self }
   end
 end

src/data/list/basic.lean

@@ -1560,8 +1560,7 @@ lemma mem_insert_nth {a b : α} : ∀ {n : ℕ} {l : list α} (hi : n ≤ l.leng
 | (n+1) []       h := (nat.not_succ_le_zero _ h).elim
 | (n+1) (a'::as) h := begin
   dsimp [list.insert_nth],
-  erw [list.mem_cons_iff, mem_insert_nth (nat.le_of_succ_le_succ h), list.mem_cons_iff,
-    ← or.assoc, or_comm (a = a'), or.assoc]
+  erw [mem_insert_nth (nat.le_of_succ_le_succ h), ← or.assoc, or_comm (a = a'), or.assoc]
 end
 
 lemma inj_on_insert_nth_index_of_not_mem (l : list α) (x : α) (hx : x ∉ l) :

src/data/list/sigma.lean

@@ -303,7 +303,7 @@ begin
     { subst a', exact ⟨rfl, heq_of_eq $ nd.eq_of_mk_mem h h'⟩ },
     { refl } },
   { rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩, dsimp [option.guard], split_ifs,
-    { subst a₁, rintro ⟨⟩, simp }, { rintro ⟨⟩ } },
+    { exact id }, { rintro ⟨⟩ } },
 end
 
 theorem keys_kreplace (a : α) (b : β a) : ∀ l : list (sigma β),

src/data/matrix/pequiv.lean

@@ -119,7 +119,7 @@ lemma to_matrix_swap [decidable_eq n] [ring α] (i j : n) :
 begin
   ext,
   dsimp [to_matrix, single, equiv.swap_apply_def, equiv.to_pequiv, one_apply],
-  split_ifs; simp * at *
+  split_ifs; {simp * at *} <|> { exfalso, assumption },
 end
 
 @[simp] lemma single_mul_single [fintype n] [decidable_eq k] [decidable_eq m] [decidable_eq n]

src/data/nat/basic.lean

@@ -374,7 +374,7 @@ lt_succ_iff.trans le_zero_iff
 
 lemma div_le_iff_le_mul_add_pred {m n k : ℕ} (n0 : 0 < n) : m / n ≤ k ↔ m ≤ n * k + (n - 1) :=
 begin
-  rw [← lt_succ_iff, div_lt_iff_lt_mul _ _ n0, succ_mul, mul_comm],
+  rw [← lt_succ_iff, div_lt_iff_lt_mul n0, succ_mul, mul_comm],
   cases n, {cases n0},
   exact lt_succ_iff,
 end
@@ -832,13 +832,13 @@ lemma div_lt_self' (n b : ℕ) : (n+1)/(b+2) < n+1 :=
 nat.div_lt_self (nat.succ_pos n) (nat.succ_lt_succ (nat.succ_pos _))
 
 theorem le_div_iff_mul_le' {x y : ℕ} {k : ℕ} (k0 : 0 < k) : x ≤ y / k ↔ x * k ≤ y :=
-le_div_iff_mul_le x y k0
+le_div_iff_mul_le k0
 
 theorem div_lt_iff_lt_mul' {x y : ℕ} {k : ℕ} (k0 : 0 < k) : x / k < y ↔ x < y * k :=
 lt_iff_lt_of_le_iff_le $ le_div_iff_mul_le' k0
 
 lemma one_le_div_iff {a b : ℕ} (hb : 0 < b) : 1 ≤ a / b ↔ b ≤ a :=
-by rw [le_div_iff_mul_le _ _ hb, one_mul]
+by rw [le_div_iff_mul_le hb, one_mul]
 
 lemma div_lt_one_iff {a b : ℕ} (hb : 0 < b) : a / b < 1 ↔ a < b :=
 lt_iff_lt_of_le_iff_le $ one_le_div_iff hb
@@ -864,7 +864,7 @@ lt_of_mul_lt_mul_left
   (nat.zero_le n)
 
 lemma lt_mul_of_div_lt {a b c : ℕ} (h : a / c < b) (w : 0 < c) : a < b * c :=
-lt_of_not_ge $ not_le_of_gt h ∘ (nat.le_div_iff_mul_le _ _ w).2
+lt_of_not_ge $ not_le_of_gt h ∘ (nat.le_div_iff_mul_le w).2
 
 protected lemma div_eq_zero_iff {a b : ℕ} (hb : 0 < b) : a / b = 0 ↔ a < b :=
 ⟨λ h, by rw [← mod_add_div a b, h, mul_zero, add_zero]; exact mod_lt _ hb,
@@ -880,7 +880,7 @@ eq_zero_of_mul_le hb $
 
 lemma mul_div_le_mul_div_assoc (a b c : ℕ) : a * (b / c) ≤ (a * b) / c :=
 if hc0 : c = 0 then by simp [hc0]
-else (nat.le_div_iff_mul_le _ _ (nat.pos_of_ne_zero hc0)).2
+else (nat.le_div_iff_mul_le (nat.pos_of_ne_zero hc0)).2
   (by rw [mul_assoc]; exact nat.mul_le_mul_left _ (nat.div_mul_le_self _ _))
 
 lemma div_mul_div_le_div (a b c : ℕ) : ((a / c) * b) / a ≤ b / c :=
@@ -927,7 +927,7 @@ by rw [mul_comm, mul_comm b, a.mul_div_mul_left b hc]
 
 lemma lt_div_mul_add {a b : ℕ} (hb : 0 < b) : a < a/b*b + b :=
 begin
-  rw [←nat.succ_mul, ←nat.div_lt_iff_lt_mul _ _ hb],
+  rw [←nat.succ_mul, ←nat.div_lt_iff_lt_mul hb],
   exact nat.lt_succ_self _,
 end
 
@@ -1215,7 +1215,7 @@ nat.eq_zero_of_dvd_of_div_eq_zero w
   ((nat.div_eq_zero_iff (lt_of_le_of_lt (zero_le b) h)).elim_right h)
 
 lemma div_le_div_left {a b c : ℕ} (h₁ : c ≤ b) (h₂ : 0 < c) : a / b ≤ a / c :=
-(nat.le_div_iff_mul_le _ _ h₂).2 $
+(nat.le_div_iff_mul_le h₂).2 $
   le_trans (nat.mul_le_mul_left _ h₁) (div_mul_le_self _ _)
 
 lemma div_eq_self {a b : ℕ} : a / b = a ↔ a = 0 ∨ b = 1 :=

src/data/nat/log.lean

@@ -66,11 +66,11 @@ begin
     cases bound with one_lt_b b_le_n,
     refine ⟨_, one_lt_b, b_le_n⟩,
     rw [log_of_one_lt_of_le one_lt_b b_le_n, succ_inj',
-        log_eq_zero_iff, nat.div_lt_iff_lt_mul _ _ (lt_trans zero_lt_one one_lt_b)] at h_log,
+        log_eq_zero_iff, nat.div_lt_iff_lt_mul (lt_trans zero_lt_one one_lt_b)] at h_log,
     exact h_log.resolve_right (λ b_small, lt_irrefl _ (lt_of_lt_of_le one_lt_b b_small)), },
   { rintros ⟨h, one_lt_b, b_le_n⟩,
     rw [log_of_one_lt_of_le one_lt_b b_le_n, succ_inj',
-        log_eq_zero_iff, nat.div_lt_iff_lt_mul _ _ (lt_trans zero_lt_one one_lt_b)],
+        log_eq_zero_iff, nat.div_lt_iff_lt_mul (lt_trans zero_lt_one one_lt_b)],
     exact or.inl h, },
 end
 
@@ -98,7 +98,7 @@ begin
   rw log, split_ifs,
   { have b_pos : 0 < b := zero_le_one.trans_lt hb,
     rw [succ_eq_add_one, add_le_add_iff_right, ←ih (y / b) (div_lt_self hy hb)
-      (nat.div_pos h.1 b_pos), le_div_iff_mul_le _ _ b_pos, pow_succ'] },
+      (nat.div_pos h.1 b_pos), le_div_iff_mul_le b_pos, pow_succ'] },
   { refine iff_of_false (λ hby, h ⟨le_trans _ hby, hb⟩) (not_succ_le_zero _),
     convert pow_mono hb.le (zero_lt_succ x),
     exact (pow_one b).symm }
@@ -177,7 +177,7 @@ eq_of_forall_le_iff (λ z, ⟨λ h, h.trans (log_monotone (div_mul_le_self _ _))
     { apply zero_le },
     rw [←pow_le_iff_le_log, pow_succ'] at h ⊢,
     { rwa [(strict_mono_mul_right_of_pos nat.succ_pos').le_iff_le,
-            nat.le_div_iff_mul_le _ _ nat.succ_pos'] },
+            nat.le_div_iff_mul_le nat.succ_pos'] },
     all_goals { simp [hn, nat.div_pos hb nat.succ_pos'] } },
   { simpa [div_eq_of_lt, hb, log_of_lt] using h }
 end⟩)
@@ -199,7 +199,7 @@ end
 
 private lemma add_pred_div_lt {b n : ℕ} (hb : 1 < b) (hn : 2 ≤ n) : (n + b - 1) / b < n :=
 begin
-  rw [div_lt_iff_lt_mul _ _ (zero_lt_one.trans hb), ←succ_le_iff, ←pred_eq_sub_one,
+  rw [div_lt_iff_lt_mul (zero_lt_one.trans hb), ←succ_le_iff, ←pred_eq_sub_one,
     succ_pred_eq_of_pos (add_pos (zero_lt_one.trans hn) (zero_lt_one.trans hb))],
   exact add_le_mul hn hb,
 end
@@ -244,7 +244,7 @@ lemma clog_eq_one {b n : ℕ} (hn : 2 ≤ n) (h : n ≤ b) : clog b n = 1 :=
 begin
   rw [clog_of_two_le (hn.trans h) hn, clog_of_right_le_one],
   have n_pos : 0 < n := zero_lt_two.trans_le hn,
-  rw [←lt_succ_iff, nat.div_lt_iff_lt_mul _ _ (n_pos.trans_le h), ←succ_le_iff,
+  rw [←lt_succ_iff, nat.div_lt_iff_lt_mul (n_pos.trans_le h), ←succ_le_iff,
     ←pred_eq_sub_one, succ_pred_eq_of_pos (add_pos n_pos (n_pos.trans_le h)), succ_mul, one_mul],
   exact add_le_add_right h _,
 end

src/data/nat/pow.lean

@@ -133,7 +133,7 @@ begin
   cases lt_or_ge p (b^succ w) with h₁ h₁,
   -- base case: p < b^succ w
   { have h₂ : p / b < b^w,
-    { rw [div_lt_iff_lt_mul p _ b_pos],
+    { rw [div_lt_iff_lt_mul b_pos],
       simpa [pow_succ'] using h₁ },
     rw [mod_eq_of_lt h₁, mod_eq_of_lt h₂],
     simp [div_add_mod] },
@@ -150,7 +150,7 @@ begin
     rw [sub_mul_mod _ _ _ h₁, sub_mul_div _ _ _ h₁],
     -- Cancel subtraction inside mod b^w
     have p_b_ge :  b^w ≤ p / b,
-    { rw [le_div_iff_mul_le _ _ b_pos, mul_comm],
+    { rw [le_div_iff_mul_le b_pos, mul_comm],
       exact h₁ },
     rw [eq.symm (mod_eq_sub_mod p_b_ge)] }
 end

src/data/num/lemmas.lean

@@ -1283,7 +1283,7 @@ theorem gcd_to_nat_aux : ∀ {n} {a b : num},
   refine add_le_add_left (nat.mul_le_mul_left _
     (le_trans (le_of_lt (nat.mod_lt _ (pos_num.cast_pos _))) _)) _,
   suffices : 1 ≤ _, simpa using nat.mul_le_mul_left (pos a) this,
-  rw [nat.le_div_iff_mul_le _ _ a.cast_pos, one_mul],
+  rw [nat.le_div_iff_mul_le a.cast_pos, one_mul],
   exact le_to_nat.2 ab
 end
 

src/data/opposite.lean

@@ -58,14 +58,16 @@ def unop : αᵒᵖ → α := id
 lemma op_injective : function.injective (op : α → αᵒᵖ) := λ _ _, id
 lemma unop_injective : function.injective (unop : αᵒᵖ → α) := λ _ _, id
 
-@[simp] lemma op_inj_iff (x y : α) : op x = op y ↔ x = y := iff.rfl
-@[simp] lemma unop_inj_iff (x y : αᵒᵖ) : unop x = unop y ↔ x = y := iff.rfl
-
 @[simp] lemma op_unop (x : αᵒᵖ) : op (unop x) = x := rfl
 @[simp] lemma unop_op (x : α) : unop (op x) = x := rfl
 
 attribute [irreducible] opposite
 
+-- We could prove these by `iff.rfl`, but that would make these eligible for `dsimp`. That would be
+-- a bad idea because `opposite` is irreducible.
+@[simp] lemma op_inj_iff (x y : α) : op x = op y ↔ x = y := op_injective.eq_iff
+@[simp] lemma unop_inj_iff (x y : αᵒᵖ) : unop x = unop y ↔ x = y := unop_injective.eq_iff
+
 /-- The type-level equivalence between a type and its opposite. -/
 def equiv_to_opposite : α ≃ αᵒᵖ :=
 { to_fun := op,

src/data/rat/defs.lean

@@ -82,7 +82,7 @@ rat.ext_iff.mpr ⟨hn, hd⟩
 def mk_pnat (n : ℤ) : ℕ+ → ℚ | ⟨d, dpos⟩ :=
 let n' := n.nat_abs, g := n'.gcd d in
 ⟨n / g, d / g, begin
-  apply (nat.le_div_iff_mul_le _ _ (nat.gcd_pos_of_pos_right _ dpos)).2,
+  apply (nat.le_div_iff_mul_le (nat.gcd_pos_of_pos_right _ dpos)).2,
   rw one_mul, exact nat.le_of_dvd dpos (nat.gcd_dvd_right _ _)
 end, begin
   have : int.nat_abs (n / ↑g) = n' / g,
@@ -208,7 +208,7 @@ begin
     have gb0 := nat.gcd_pos_of_pos_right a hb,
     have gd0 := nat.gcd_pos_of_pos_right c hd,
     apply nat.le_of_dvd,
-    apply (nat.le_div_iff_mul_le _ _ gd0).2,
+    apply (nat.le_div_iff_mul_le gd0).2,
     simp, apply nat.le_of_dvd hd (nat.gcd_dvd_right _ _),
     apply (nat.coprime_div_gcd_div_gcd gb0).symm.dvd_of_dvd_mul_left,
     refine ⟨c / c.gcd d, _⟩,

src/data/sigma/basic.lean

@@ -153,9 +153,9 @@ by cases x; refl
 @[instance]
 protected meta def {u v} sigma.reflect [reflected_univ.{u}] [reflected_univ.{v}]
   {α : Type u} (β : α → Type v)
-  [reflected α] [reflected β] [hα : has_reflect α] [hβ : Π i, has_reflect (β i)] :
+  [reflected _ α] [reflected _ β] [hα : has_reflect α] [hβ : Π i, has_reflect (β i)] :
   has_reflect (Σ a, β a) :=
-λ ⟨a, b⟩, (by reflect_name : reflected @sigma.mk.{u v}).subst₄ `(α) `(β) `(a) `(b)
+λ ⟨a, b⟩, (by reflect_name : reflected _ @sigma.mk.{u v}).subst₄ `(α) `(β) `(a) `(b)
 
 end sigma
 

src/data/vector/basic.lean

@@ -565,10 +565,10 @@ instance : is_lawful_traversable.{u} (flip vector n) :=
   id_map := by intros; cases x; simp! [(<$>)],
   comp_map := by intros; cases x; simp! [(<$>)] }
 
-meta instance reflect [reflected_univ.{u}] {α : Type u} [has_reflect α] [reflected α] {n : ℕ} :
+meta instance reflect [reflected_univ.{u}] {α : Type u} [has_reflect α] [reflected _ α] {n : ℕ} :
   has_reflect (vector α n) :=
-λ v, @vector.induction_on n α (λ n, reflected) v
-  ((by reflect_name : reflected @vector.nil.{u}).subst `(α))
-  (λ n x xs ih, (by reflect_name : reflected @vector.cons.{u}).subst₄ `(α) `(n) `(x) ih)
+λ v, @vector.induction_on n α (λ n, reflected _) v
+  ((by reflect_name : reflected _ @vector.nil.{u}).subst `(α))
+  (λ n x xs ih, (by reflect_name : reflected _ @vector.cons.{u}).subst₄ `(α) `(n) `(x) ih)
 
 end vector

src/dynamics/periodic_pts.lean

@@ -338,7 +338,7 @@ lemma not_is_periodic_pt_of_pos_of_lt_minimal_period :
 
 lemma is_periodic_pt.minimal_period_dvd (hx : is_periodic_pt f n x) : minimal_period f x ∣ n :=
 (eq_or_lt_of_le $ n.zero_le).elim (λ hn0, hn0 ▸ dvd_zero _) $ λ hn0,
-(nat.dvd_iff_mod_eq_zero _ _).2 $
+nat.dvd_iff_mod_eq_zero.2 $
 (hx.mod $ is_periodic_pt_minimal_period f x).eq_zero_of_lt_minimal_period $
 nat.mod_lt _ $ hx.minimal_period_pos hn0
 

src/linear_algebra/projective_space/basic.lean

@@ -150,7 +150,7 @@ begin
     use mk K v this,
     symmetry,
     ext x, revert x, erw ← set.ext_iff, ext x,
-    dsimp,
+    dsimp [-set_like.mem_coe],
     rw [submodule.span_singleton_eq_range],
     refine ⟨λ hh, _, _⟩,
     { obtain ⟨c,hc⟩ := h ⟨x,hh⟩,