From 2558b3b31d33969bb3ef330982ff131533eebfdd Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 27 Jun 2022 16:25:11 +0000 Subject: [PATCH] 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 | 2 +- leanpkg.toml | 2 +- src/algebra/geom_sum.lean | 2 +- src/algebraic_geometry/gluing.lean | 2 +- src/algebraic_topology/simplex_category.lean | 4 ++-- .../simple_graph/regularity/bound.lean | 2 +- src/data/fin/tuple/basic.lean | 8 +++---- src/data/fin/vec_notation.lean | 6 +++--- src/data/int/basic.lean | 6 +++--- src/data/list/basic.lean | 3 +-- src/data/list/sigma.lean | 2 +- src/data/matrix/pequiv.lean | 2 +- src/data/nat/basic.lean | 14 ++++++------- src/data/nat/log.lean | 12 +++++------ src/data/nat/pow.lean | 4 ++-- src/data/num/lemmas.lean | 2 +- src/data/opposite.lean | 8 ++++--- src/data/rat/defs.lean | 4 ++-- src/data/sigma/basic.lean | 4 ++-- src/data/vector/basic.lean | 8 +++---- src/dynamics/periodic_pts.lean | 2 +- .../projective_space/basic.lean | 2 +- src/meta/univs.lean | 21 ++++++++++--------- src/number_theory/dioph.lean | 4 ++-- .../gauss_eisenstein_lemmas.lean | 4 ++-- .../quadratic_reciprocity.lean | 4 ++-- src/number_theory/primorial.lean | 2 +- src/number_theory/sum_four_squares.lean | 2 +- src/order/bounded_order.lean | 8 +++++++ src/order/filter/at_top_bot.lean | 2 +- src/order/galois_connection.lean | 2 +- src/set_theory/ordinal/arithmetic.lean | 2 +- src/tactic/core.lean | 2 +- src/tactic/doc_commands.lean | 4 ++-- src/tactic/fix_reflect_string.lean | 2 +- src/tactic/linarith/datatypes.lean | 2 +- src/tactic/local_cache.lean | 11 +++++----- src/tactic/omega/term.lean | 2 ++ src/tactic/replacer.lean | 10 ++++----- src/topology/discrete_quotient.lean | 7 +------ src/topology/uniform_space/basic.lean | 6 +++--- 41 files changed, 103 insertions(+), 95 deletions(-) diff --git a/archive/100-theorems-list/45_partition.lean b/archive/100-theorems-list/45_partition.lean index 81fe29b72b700..8661c762b129b 100644 --- a/archive/100-theorems-list/45_partition.lean +++ b/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, diff --git a/leanpkg.toml b/leanpkg.toml index 67db622a61ddd..1f16346c8e401 100644 --- a/leanpkg.toml +++ b/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] diff --git a/src/algebra/geom_sum.lean b/src/algebra/geom_sum.lean index 11869808506c3..c8e04e68c6fae 100644 --- a/src/algebra/geom_sum.lean +++ b/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 _ }, diff --git a/src/algebraic_geometry/gluing.lean b/src/algebraic_geometry/gluing.lean index 490a5954802d5..8e7a89c701c99 100644 --- a/src/algebraic_geometry/gluing.lean +++ b/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 }, diff --git a/src/algebraic_topology/simplex_category.lean b/src/algebraic_topology/simplex_category.lean index bc8ef54bb9de0..36815db57f061 100644 --- a/src/algebraic_topology/simplex_category.lean +++ b/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 diff --git a/src/combinatorics/simple_graph/regularity/bound.lean b/src/combinatorics/simple_graph/regularity/bound.lean index 518ca84f2b074..9a3bae790ba1a 100644 --- a/src/combinatorics/simple_graph/regularity/bound.lean +++ b/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 diff --git a/src/data/fin/tuple/basic.lean b/src/data/fin/tuple/basic.lean index df33e28b1fc94..1d386bb12ce71 100644 --- a/src/data/fin/tuple/basic.lean +++ b/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, diff --git a/src/data/fin/vec_notation.lean b/src/data/fin/vec_notation.lean index a38cd8fca5713..63077a0b51a3f 100644 --- a/src/data/fin/vec_notation.lean +++ b/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 diff --git a/src/data/int/basic.lean b/src/data/int/basic.lean index 9e95a98cfdc4a..54efb2d87b1f1 100644 --- a/src/data/int/basic.lean +++ b/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 diff --git a/src/data/list/basic.lean b/src/data/list/basic.lean index 30517897df135..dd71d86937723 100644 --- a/src/data/list/basic.lean +++ b/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) : diff --git a/src/data/list/sigma.lean b/src/data/list/sigma.lean index 55082854cef6f..46a0917c60e95 100644 --- a/src/data/list/sigma.lean +++ b/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 β), diff --git a/src/data/matrix/pequiv.lean b/src/data/matrix/pequiv.lean index 9e602fb011eac..66d9cb41ffc1a 100644 --- a/src/data/matrix/pequiv.lean +++ b/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] diff --git a/src/data/nat/basic.lean b/src/data/nat/basic.lean index ef02595c31619..fc300ce55c8df 100644 --- a/src/data/nat/basic.lean +++ b/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 := diff --git a/src/data/nat/log.lean b/src/data/nat/log.lean index 1d4a5049bf512..654dddd1c3b06 100644 --- a/src/data/nat/log.lean +++ b/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 diff --git a/src/data/nat/pow.lean b/src/data/nat/pow.lean index d8201c1f32127..68dfb89da3adf 100644 --- a/src/data/nat/pow.lean +++ b/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 diff --git a/src/data/num/lemmas.lean b/src/data/num/lemmas.lean index 082e965896329..e37619a4f3844 100644 --- a/src/data/num/lemmas.lean +++ b/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 diff --git a/src/data/opposite.lean b/src/data/opposite.lean index 356e4876a73d8..985150bd4faf6 100644 --- a/src/data/opposite.lean +++ b/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, diff --git a/src/data/rat/defs.lean b/src/data/rat/defs.lean index 555ad1ce08fbf..0b20525a663ae 100644 --- a/src/data/rat/defs.lean +++ b/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, _⟩, diff --git a/src/data/sigma/basic.lean b/src/data/sigma/basic.lean index a3559b01740d3..922e4b666e916 100644 --- a/src/data/sigma/basic.lean +++ b/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 diff --git a/src/data/vector/basic.lean b/src/data/vector/basic.lean index e1ecbfdd96e1e..f7b6bf1a661e7 100644 --- a/src/data/vector/basic.lean +++ b/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 diff --git a/src/dynamics/periodic_pts.lean b/src/dynamics/periodic_pts.lean index a57d88eba196a..499fd5bfb137f 100644 --- a/src/dynamics/periodic_pts.lean +++ b/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 diff --git a/src/linear_algebra/projective_space/basic.lean b/src/linear_algebra/projective_space/basic.lean index b5b6228c1f277..b9d8b4656ce04 100644 --- a/src/linear_algebra/projective_space/basic.lean +++ b/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⟩, diff --git a/src/meta/univs.lean b/src/meta/univs.lean index ae6cd60f2d694..48bb6413bf941 100644 --- a/src/meta/univs.lean +++ b/src/meta/univs.lean @@ -61,14 +61,14 @@ local attribute [semireducible] reflected /-- This definition circumvents the protection that `reflected` tried to enforce; so is private such that it is only used by `tactic.interactive.reflect_name` where we have enforced the protection manually. -/ -private meta def reflected.of {α : Sort*} {a : α} (e : expr) : reflected a := e +private meta def reflected.of {α : Sort*} {a : α} (e : expr) : reflected _ a := e end /-- Reflect a universe-polymorphic name, by searching for `reflected_univ` instances. -/ meta def tactic.interactive.reflect_name : tactic unit := do tgt ← tactic.target, - `(reflected %%x) ← pure tgt, + `(reflected _ %%x) ← pure tgt, expr.const name levels ← pure x, levels ← levels.mmap (λ l, do inst ← tactic.mk_instance (expr.const `reflected_univ [l]), @@ -82,21 +82,22 @@ do /-- Convenience helper for two consecutive `reflected.subst` applications -/ meta def reflected.subst₂ {α : Sort u} {β : α → Sort v} {γ : Π a, β a → Sort w} {f : Π a b, γ a b} {a : α} {b : β a} : - reflected f → reflected a → reflected b → reflected (f a b) := + reflected _ f → reflected _ a → reflected _ b → reflected _ (f a b) := (∘) reflected.subst ∘ reflected.subst /-- Convenience helper for three consecutive `reflected.subst` applications -/ meta def reflected.subst₃ {α : Sort u} {β : α → Sort v} {γ : Π a, β a → Sort w} {δ : Π a b, γ a b → Sort x} {f : Π a b c, δ a b c} {a : α} {b : β a} {c : γ a b}: - reflected f → reflected a → reflected b → reflected c → reflected (f a b c) := + reflected _ f → reflected _ a → reflected _ b → reflected _ c → reflected _ (f a b c) := (∘) reflected.subst₂ ∘ reflected.subst /-- Convenience helper for four consecutive `reflected.subst` applications -/ meta def reflected.subst₄ {α : Sort u} {β : α → Sort v} {γ : Π a, β a → Sort w} {δ : Π a b, γ a b → Sort x} {ε : Π a b c, δ a b c → Sort y} {f : Π a b c d, ε a b c d} {a : α} {b : β a} {c : γ a b} {d : δ a b c} : - reflected f → reflected a → reflected b → reflected c → reflected d → reflected (f a b c d) := + reflected _ f → reflected _ a → reflected _ b → reflected _ c → reflected _ d → + reflected _ (f a b c d) := (∘) reflected.subst₃ ∘ reflected.subst /-! ### Universe-polymorphic `has_reflect` instances -/ @@ -106,11 +107,11 @@ meta instance punit.reflect' [reflected_univ.{u}] : has_reflect punit.{u} | punit.star := by reflect_name /-- Universe polymorphic version of the builtin `list.reflect`. -/ -meta instance list.reflect' [reflected_univ.{u}] {α : Type u} [has_reflect α] [reflected α] : +meta instance list.reflect' [reflected_univ.{u}] {α : Type u} [has_reflect α] [reflected _ α] : has_reflect (list α) -| [] := (by reflect_name : reflected @list.nil.{u}).subst `(α) -| (h::t) := (by reflect_name : reflected @list.cons.{u}).subst₃ `(α) `(h) (list.reflect' t) +| [] := (by reflect_name : reflected _ @list.nil.{u}).subst `(α) +| (h::t) := (by reflect_name : reflected _ @list.cons.{u}).subst₃ `(α) `(h) (list.reflect' t) meta instance ulift.reflect' [reflected_univ.{u}] [reflected_univ.{v}] {α : Type v} - [reflected α] [has_reflect α] : has_reflect (ulift.{u v} α) -| (ulift.up x) := (by reflect_name : reflected @ulift.up.{u v}).subst₂ `(α) `(x) + [reflected _ α] [has_reflect α] : has_reflect (ulift.{u v} α) +| (ulift.up x) := (by reflect_name : reflected _ @ulift.up.{u v}).subst₂ `(α) `(x) diff --git a/src/number_theory/dioph.lean b/src/number_theory/dioph.lean index 95c94a71e666a..e6e2bea2e78a0 100644 --- a/src/number_theory/dioph.lean +++ b/src/number_theory/dioph.lean @@ -490,8 +490,8 @@ by refine iff.trans _ eq_comm; exact y.eq_zero_or_pos.elim (λ y0, by rw [y0, nat.div_zero]; exact ⟨λ o, (o.resolve_right $ λ ⟨_, h2⟩, nat.not_lt_zero _ h2).right, λ z0, or.inl ⟨rfl, z0⟩⟩) (λ ypos, iff.trans ⟨λ o, o.resolve_left $ λ ⟨h1, _⟩, ne_of_gt ypos h1, or.inr⟩ - (le_antisymm_iff.trans $ and_congr (nat.le_div_iff_mul_le _ _ ypos) $ - iff.trans ⟨lt_succ_of_le, le_of_lt_succ⟩ (div_lt_iff_lt_mul _ _ ypos)).symm) + (le_antisymm_iff.trans $ and_congr (nat.le_div_iff_mul_le ypos) $ + iff.trans ⟨lt_succ_of_le, le_of_lt_succ⟩ (div_lt_iff_lt_mul ypos)).symm) localized "infix ` D/ `:80 := dioph.div_dioph" in dioph omit df dg diff --git a/src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean b/src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean index be4dcb44bc93b..bd60ea818edcf 100644 --- a/src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean +++ b/src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean @@ -200,8 +200,8 @@ calc a / b = (Ico 1 (a / b).succ).card : by simp ... = ((Ico 1 c.succ).filter (λ x, x * b ≤ a)).card : congr_arg _ $ finset.ext $ λ x, have x * b ≤ a → x ≤ c, - from λ h, le_trans (by rwa [le_div_iff_mul_le _ _ hb0]) hc, - by simp [lt_succ_iff, le_div_iff_mul_le _ _ hb0]; tauto + from λ h, le_trans (by rwa [le_div_iff_mul_le hb0]) hc, + by simp [lt_succ_iff, le_div_iff_mul_le hb0]; tauto /-- The given sum is the number of integer points in the triangle formed by the diagonal of the rectangle `(0, p/2) × (0, q/2)` -/ diff --git a/src/number_theory/legendre_symbol/quadratic_reciprocity.lean b/src/number_theory/legendre_symbol/quadratic_reciprocity.lean index 75306fbd57277..9aca5e1c254d2 100644 --- a/src/number_theory/legendre_symbol/quadratic_reciprocity.lean +++ b/src/number_theory/legendre_symbol/quadratic_reciprocity.lean @@ -308,8 +308,8 @@ lemma exists_sq_eq_prime_iff_of_mod_four_eq_one (hp1 : p % 4 = 1) (hq1 : q ≠ 2 is_square (q : zmod p) ↔ is_square (p : zmod q) := if hpq : p = q then by substI hpq else have h1 : ((p / 2) * (q / 2)) % 2 = 0, - from (dvd_iff_mod_eq_zero _ _).1 - (dvd_mul_of_dvd_left ((dvd_iff_mod_eq_zero _ _).2 $ + from dvd_iff_mod_eq_zero.1 + (dvd_mul_of_dvd_left (dvd_iff_mod_eq_zero.2 $ by rw [← mod_mul_right_div_self, show 2 * 2 = 4, from rfl, hp1]; refl) _), begin have hp_odd : p ≠ 2 := by { by_contra, simp [h] at hp1, norm_num at hp1, }, diff --git a/src/number_theory/primorial.lean b/src/number_theory/primorial.lean index 2c4354995fe52..bcb4485006754 100644 --- a/src/number_theory/primorial.lean +++ b/src/number_theory/primorial.lean @@ -33,7 +33,7 @@ lemma primorial_succ {n : ℕ} (n_big : 1 < n) (r : n % 2 = 1) : (n + 1)# = n# : begin refine prod_congr _ (λ _ _, rfl), rw [range_succ, filter_insert, if_neg (λ h, _)], - have two_dvd : 2 ∣ n + 1 := (dvd_iff_mod_eq_zero _ _).mpr (by rw [← mod_add_mod, r, mod_self]), + have two_dvd : 2 ∣ n + 1 := dvd_iff_mod_eq_zero.mpr (by rw [← mod_add_mod, r, mod_self]), linarith [(h.dvd_iff_eq (nat.bit0_ne_one 1)).mp two_dvd], end diff --git a/src/number_theory/sum_four_squares.lean b/src/number_theory/sum_four_squares.lean index bbcb27382da57..32861b6225eb6 100644 --- a/src/number_theory/sum_four_squares.lean +++ b/src/number_theory/sum_four_squares.lean @@ -120,7 +120,7 @@ by haveI hm0 : _root_.fact (0 < m) := ⟨(nat.find_spec hm).snd.1⟩; exact have hmp : m < p, from (nat.find_spec hm).fst, m.mod_two_eq_zero_or_one.elim (λ hm2 : m % 2 = 0, - let ⟨k, hk⟩ := (nat.dvd_iff_mod_eq_zero _ _).2 hm2 in + let ⟨k, hk⟩ := nat.dvd_iff_mod_eq_zero.2 hm2 in have hk0 : 0 < k, from nat.pos_of_ne_zero $ λ _, by { simp [*, lt_irrefl] at * }, have hkm : k < m, { rw [hk, two_mul], exact (lt_add_iff_pos_left _).2 hk0 }, false.elim $ nat.find_min hm hkm ⟨lt_trans hkm hmp, hk0, diff --git a/src/order/bounded_order.lean b/src/order/bounded_order.lean index 885fda70a49e1..0486f5f961c63 100644 --- a/src/order/bounded_order.lean +++ b/src/order/bounded_order.lean @@ -529,6 +529,10 @@ instance [has_repr α] : has_repr (with_bot α) := instance : has_coe_t α (with_bot α) := ⟨some⟩ instance : has_bot (with_bot α) := ⟨none⟩ +meta instance {α : Type} [reflected _ α] [has_reflect α] : has_reflect (with_bot α) +| ⊥ := `(⊥) +| (a : α) := `(coe : α → with_bot α).subst `(a) + instance : inhabited (with_bot α) := ⟨⊥⟩ lemma none_eq_bot : (none : with_bot α) = (⊥ : with_bot α) := rfl @@ -816,6 +820,10 @@ instance [has_repr α] : has_repr (with_top α) := instance : has_coe_t α (with_top α) := ⟨some⟩ instance : has_top (with_top α) := ⟨none⟩ +meta instance {α : Type} [reflected _ α] [has_reflect α] : has_reflect (with_top α) +| ⊤ := `(⊤) +| (a : α) := `(coe : α → with_top α).subst `(a) + instance : inhabited (with_top α) := ⟨⊤⟩ lemma none_eq_top : (none : with_top α) = (⊤ : with_top α) := rfl diff --git a/src/order/filter/at_top_bot.lean b/src/order/filter/at_top_bot.lean index 81c71e0908929..f9a13935bbe18 100644 --- a/src/order/filter/at_top_bot.lean +++ b/src/order/filter/at_top_bot.lean @@ -1212,7 +1212,7 @@ map_at_top_eq_of_gc (λb, b * k + (k - 1)) 1 (assume a b h, nat.div_le_div_right h) (assume a b _, calc a / k ≤ b ↔ a / k < b + 1 : by rw [← nat.succ_eq_add_one, nat.lt_succ_iff] - ... ↔ a < (b + 1) * k : nat.div_lt_iff_lt_mul _ _ hk + ... ↔ a < (b + 1) * k : nat.div_lt_iff_lt_mul hk ... ↔ _ : begin cases k, diff --git a/src/order/galois_connection.lean b/src/order/galois_connection.lean index 0151dc99de750..b20318067762b 100644 --- a/src/order/galois_connection.lean +++ b/src/order/galois_connection.lean @@ -382,7 +382,7 @@ end order_iso namespace nat lemma galois_connection_mul_div {k : ℕ} (h : 0 < k) : galois_connection (λ n, n * k) (λ n, n / k) := -λ x y, (le_div_iff_mul_le x y h).symm +λ x y, (le_div_iff_mul_le h).symm end nat diff --git a/src/set_theory/ordinal/arithmetic.lean b/src/set_theory/ordinal/arithmetic.lean index 5b31a9960d9ac..917dfa177a163 100644 --- a/src/set_theory/ordinal/arithmetic.lean +++ b/src/set_theory/ordinal/arithmetic.lean @@ -2154,7 +2154,7 @@ le_antisymm (by rw [le_div n0', ← nat_cast_mul, nat_cast_le, mul_comm]; apply nat.div_mul_le_self) (by rw [div_le n0', ←add_one_eq_succ, ← nat.cast_succ, ← nat_cast_mul, - nat_cast_lt, mul_comm, ← nat.div_lt_iff_lt_mul _ _ (nat.pos_of_ne_zero n0)]; + nat_cast_lt, mul_comm, ← nat.div_lt_iff_lt_mul (nat.pos_of_ne_zero n0)]; apply nat.lt_succ_self) @[simp] theorem nat_cast_mod {m n : ℕ} : ((m % n : ℕ) : ordinal) = m % n := diff --git a/src/tactic/core.lean b/src/tactic/core.lean index bbb5d8368de7a..39561c296c32f 100644 --- a/src/tactic/core.lean +++ b/src/tactic/core.lean @@ -405,7 +405,7 @@ do ((), body) ← solve_aux type tac, /-- `eval_expr' α e` attempts to evaluate the expression `e` in the type `α`. This is a variant of `eval_expr` in core. Due to unexplained behavior in the VM, in rare situations the latter will fail but the former will succeed. -/ -meta def eval_expr' (α : Type*) [_inst_1 : reflected α] (e : expr) : tactic α := +meta def eval_expr' (α : Type*) [_inst_1 : reflected _ α] (e : expr) : tactic α := mk_app ``id [e] >>= eval_expr α /-- `mk_fresh_name` returns identifiers starting with underscores, diff --git a/src/tactic/doc_commands.lean b/src/tactic/doc_commands.lean index f51df2877e074..721a9e477b84b 100644 --- a/src/tactic/doc_commands.lean +++ b/src/tactic/doc_commands.lean @@ -77,8 +77,8 @@ output. -/ Example: ``mk_reflected_definition `foo 17`` constructs the definition declaration corresponding to `def foo : ℕ := 17` -/ -meta def mk_reflected_definition (decl_name : name) {type} [reflected type] - (body : type) [reflected body] : declaration := +meta def mk_reflected_definition (decl_name : name) {type} [reflected _ type] + (body : type) [reflected _ body] : declaration := mk_definition decl_name (reflect type).collect_univ_params (reflect type) (reflect body) /-- If `note_name` and `note` are `pexpr`s representing strings, diff --git a/src/tactic/fix_reflect_string.lean b/src/tactic/fix_reflect_string.lean index 2657700a5d25e..02b4a038288ae 100644 --- a/src/tactic/fix_reflect_string.lean +++ b/src/tactic/fix_reflect_string.lean @@ -38,5 +38,5 @@ let chunk_size := 256 in if s.length ≤ chunk_size then reflect s else have ts : list (thunk string), from (s.to_chunks chunk_size).map (λ s _, s), have h : s = string.join (ts.map (λ t, t ())), from undefined, -suffices reflected (string.join $ ts.map (λ t, t ())), by rwa h, +suffices reflected _ (string.join $ ts.map (λ t, t ())), by rwa h, `(string.join $ list.map _ _) diff --git a/src/tactic/linarith/datatypes.lean b/src/tactic/linarith/datatypes.lean index 0dde18107ad40..e1edff788486d 100644 --- a/src/tactic/linarith/datatypes.lean +++ b/src/tactic/linarith/datatypes.lean @@ -311,7 +311,7 @@ list comp → ℕ → tactic (rb_map ℕ ℕ) meta structure linarith_config : Type := (discharger : tactic unit := `[ring]) (restrict_type : option Type := none) -(restrict_type_reflect : reflected restrict_type . tactic.apply_instance) +(restrict_type_reflect : reflected _ restrict_type . tactic.apply_instance) (exfalso : bool := tt) (transparency : tactic.transparency := reducible) (split_hypotheses : bool := tt) diff --git a/src/tactic/local_cache.lean b/src/tactic/local_cache.lean index aa6f053801c64..5ff10222b7834 100644 --- a/src/tactic/local_cache.lean +++ b/src/tactic/local_cache.lean @@ -10,11 +10,11 @@ namespace local_cache namespace internal -variables {α : Type} [reflected α] [has_reflect α] +variables {α : Type} [reflected _ α] [has_reflect α] meta def mk_full_namespace (ns : name) : name := `local_cache ++ ns -meta def save_data (dn : name) (a : α) [reflected a] : tactic unit := +meta def save_data (dn : name) (a : α) [reflected _ a] : tactic unit := tactic.add_decl $ mk_definition dn [] (reflect α) (reflect a) meta def load_data (dn : name) : tactic α := @@ -26,7 +26,7 @@ meta def poke_data (dn : name) : tactic bool := do e ← tactic.get_env, return (e.get dn).to_bool -meta def run_once_under_name {α : Type} [reflected α] [has_reflect α] (t : tactic α) +meta def run_once_under_name {α : Type} [reflected _ α] [has_reflect α] (t : tactic α) (cache_name : name) : tactic α := do load_data cache_name <|> do @@ -190,7 +190,8 @@ meta def clear (ns : name) (s : cache_scope := block_local) : tactic unit := s.clear ns /-- Gets the (optionally present) value-in-cache for `ns`. -/ -meta def get (ns : name) (α : Type) [reflected α] [has_reflect α] (s : cache_scope := block_local) : +meta def get (ns : name) (α : Type) [reflected _ α] [has_reflect α] + (s : cache_scope := block_local) : tactic (option α) := do dn ← some <$> s.try_get_name ns <|> return none, match dn with @@ -217,7 +218,7 @@ open local_cache local_cache.internal If `α` is just `unit`, this means we just run `t` once each tactic block. -/ -meta def run_once {α : Type} [reflected α] [has_reflect α] (ns : name) (t : tactic α) +meta def run_once {α : Type} [reflected _ α] [has_reflect α] (ns : name) (t : tactic α) (s : cache_scope := cache_scope.block_local) : tactic α := s.get_name ns >>= run_once_under_name t diff --git a/src/tactic/omega/term.lean b/src/tactic/omega/term.lean index 3362b50a80f17..8b48371ce4446 100644 --- a/src/tactic/omega/term.lean +++ b/src/tactic/omega/term.lean @@ -18,6 +18,8 @@ namespace omega @[derive inhabited] def term : Type := int × list int +meta instance : has_reflect term := prod.has_reflect _ _ + namespace term /-- Evaluate a term using the valuation v. -/ diff --git a/src/tactic/replacer.lean b/src/tactic/replacer.lean index 4d4d394475367..f5c16ce185cff 100644 --- a/src/tactic/replacer.lean +++ b/src/tactic/replacer.lean @@ -14,8 +14,8 @@ meaning is defined incrementally through attributes. namespace tactic -meta def replacer_core {α : Type} [reflected α] - (ntac : name) (eval : ∀ β [reflected β], expr → tactic β) : +meta def replacer_core {α : Type} [reflected _ α] + (ntac : name) (eval : ∀ β [reflected _ β], expr → tactic β) : list name → tactic α | [] := fail ("no implementation defined for " ++ to_string ntac) | (n::ns) := do d ← get_decl n, let t := d.type, @@ -26,8 +26,8 @@ meta def replacer_core {α : Type} [reflected α] return (tac (guard (ns ≠ []) >> some (replacer_core ns))) }, tac -meta def replacer (ntac : name) {α : Type} [reflected α] - (F : Type → Type) (eF : ∀ β, reflected β → reflected (F β)) +meta def replacer (ntac : name) {α : Type} [reflected _ α] + (F : Type → Type) (eF : ∀ β, reflected _ β → reflected _ (F β)) (R : ∀ β, F β → β) : tactic α := attribute.get_instances ntac >>= replacer_core ntac (λ β eβ e, R β <$> @eval_expr' (F β) (eF β eβ) e) @@ -47,7 +47,7 @@ meta def mk_replacer₂ (ntac : name) (v : expr × expr) : expr → nat → opti reflect ntac, β, reflect β, expr.lam `γ binder_info.default `(Type) v.1, expr.lam `γ binder_info.default `(Type) $ - expr.lam `eγ binder_info.inst_implicit ((`(@reflected Type) : expr) β) v.2, + expr.lam `eγ binder_info.inst_implicit ((`(reflected Type) : expr) β) v.2, expr.lam `γ binder_info.default `(Type) $ expr.lam `f binder_info.default v.1 $ (list.range i).foldr (λ i e', e' (expr.var (i+2))) (expr.var 0) diff --git a/src/topology/discrete_quotient.lean b/src/topology/discrete_quotient.lean index f7b952645ee47..bded7b0c1086e 100644 --- a/src/topology/discrete_quotient.lean +++ b/src/topology/discrete_quotient.lean @@ -309,12 +309,7 @@ begin (λ (Q : discrete_quotient X), Q.proj ⁻¹' {Qs _}) (λ A B, _) (λ i, _) (λ i, (fiber_closed _ _).is_compact) (λ i, fiber_closed _ _), { refine ⟨x, λ Q, _⟩, - specialize hx _ ⟨Q,rfl⟩, - dsimp at hx, - rcases proj_surjective _ (Qs Q) with ⟨y,hy⟩, - rw ← hy at *, - rw fiber_eq at hx, - exact quotient.sound' (Q.symm y x hx) }, + exact hx _ ⟨Q,rfl⟩ }, { refine ⟨A ⊓ B, λ a ha, _, λ a ha, _⟩, { dsimp only, erw ← compat (A ⊓ B) A inf_le_left, diff --git a/src/topology/uniform_space/basic.lean b/src/topology/uniform_space/basic.lean index 39e762e866478..d04fb61c22a88 100644 --- a/src/topology/uniform_space/basic.lean +++ b/src/topology/uniform_space/basic.lean @@ -1122,11 +1122,11 @@ lemma uniformity_comap [uniform_space α] [uniform_space β] {f : α → β} by { rw h, refl } lemma uniform_space_comap_id {α : Type*} : uniform_space.comap (id : α → α) = id := -by ext u ; dsimp [uniform_space.comap] ; rw [prod.id_prod, filter.comap_id] +by ext u ; dsimp only [uniform_space.comap, id] ; rw [prod.id_prod, filter.comap_id] lemma uniform_space.comap_comap {α β γ} [uγ : uniform_space γ] {f : α → β} {g : β → γ} : uniform_space.comap (g ∘ f) uγ = uniform_space.comap f (uniform_space.comap g uγ) := -by ext ; dsimp [uniform_space.comap] ; rw filter.comap_comap +by ext ; dsimp only [uniform_space.comap] ; rw filter.comap_comap lemma uniform_space.comap_inf {α γ} {u₁ u₂ : uniform_space γ} {f : α → γ} : (u₁ ⊓ u₂).comap f = u₁.comap f ⊓ u₂.comap f := @@ -1524,7 +1524,7 @@ begin apply (𝓤 α).sets_of_superset hm', rintros ⟨x, y⟩ hp rfl, refine ⟨i, m', hm', λ z hz, h (monotone_comp_rel monotone_id monotone_const mm' _)⟩, - dsimp at hz ⊢, rw comp_rel_assoc, + dsimp [-mem_comp_rel] at hz ⊢, rw comp_rel_assoc, exact ⟨y, hp, hz⟩ }, have hu₂ : s ⊆ ⋃ n ∈ 𝓤 α, u n, { intros x hx,