feat(*): several @[simp] lemmas (#2579)

Also add an explicit instance for `submodule.has_coe_to_sort`.
This way `rintro ⟨x, hx⟩` results in `(hx : x ∈ p)`.

Also fixes some timeouts introduced by #2363. See Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/partrec_code

src/algebra/group/prod.lean

@@ -46,6 +46,9 @@ lemma fst_one [has_one M] [has_one N] : (1 : M × N).1 = 1 := rfl
 lemma snd_one [has_one M] [has_one N] : (1 : M × N).2 = 1 := rfl
 @[to_additive]
 lemma one_eq_mk [has_one M] [has_one N] : (1 : M × N) = (1, 1) := rfl
+@[simp, to_additive]
+lemma mk_eq_one [has_one M] [has_one N] {x : M} {y : N} : (x, y) = 1 ↔ x = 1 ∧ y = 1 :=
+mk.inj_iff
 
 @[to_additive]
 lemma fst_mul_snd [monoid M] [monoid N] (p : M × N) :

src/algebra/module.lean

@@ -356,14 +356,22 @@ structure submodule (R : Type u) (M : Type v) [ring R]
 (smul : ∀ (c:R) {x}, x ∈ carrier → c • x ∈ carrier)
 
 namespace submodule
-variables [ring R] [add_comm_group M] [add_comm_group M₂]
+variables [ring R] [add_comm_group M]
 
-section
 variables [module R M]
 
 instance : has_coe (submodule R M) (set M) := ⟨submodule.carrier⟩
 instance : has_mem M (submodule R M) := ⟨λ x p, x ∈ (p : set M)⟩
-end
+instance : has_coe_to_sort (submodule R M) := ⟨_, λ p, {x : M // x ∈ p}⟩
+end submodule
+
+protected theorem submodule.exists [ring R] [add_comm_group M] [module R M] {p : submodule R M}
+  {q : p → Prop} :
+  (∃ x, q x) ↔ (∃ x (hx : x ∈ p), q ⟨x, hx⟩) :=
+set_coe.exists
+
+namespace submodule
+variables [ring R] [add_comm_group M] [add_comm_group M₂]
 
 -- We can infer the module structure implicitly from the bundled submodule,
 -- rather than via typeclass resolution.
@@ -418,6 +426,8 @@ instance : inhabited p := ⟨0⟩
 instance : has_neg p := ⟨λx, ⟨-x.1, neg_mem _ x.2⟩⟩
 instance : has_scalar R p := ⟨λ c x, ⟨c • x.1, smul_mem _ c x.2⟩⟩
 
+@[simp] lemma mk_eq_zero (x) (h : x ∈ p) : (⟨x, h⟩ : p) = 0 ↔ x = 0 := subtype.ext
+
 variables {p}
 @[simp, norm_cast] lemma coe_add (x y : p) : (↑(x + y) : M) = ↑x + ↑y := rfl
 @[simp, norm_cast] lemma coe_zero : ((0 : p) : M) = 0 := rfl

src/analysis/convex/cone.lean

@@ -371,7 +371,6 @@ theorem riesz_extension (s : convex_cone E) (f : linear_pmap ℝ E ℝ)
 begin
   rcases riesz_extension.exists_top s f nonneg dense with ⟨⟨g_dom, g⟩, ⟨hpg, hfg⟩, htop, hgs⟩,
   clear hpg,
-  dsimp at hfg hgs htop ⊢,
   refine ⟨g.comp (linear_equiv.of_top _ htop).symm, _, _⟩;
     simp only [comp_apply, linear_equiv.coe_apply, linear_equiv.of_top_symm_apply],
   { intro s, refine (hfg _).symm, refl },

src/computability/partrec.lean

@@ -146,8 +146,8 @@ end⟩
 inductive partrec : (ℕ →. ℕ) → Prop
 | zero : partrec (pure 0)
 | succ : partrec succ
-| left : partrec (λ n, n.unpair.1)
-| right : partrec (λ n, n.unpair.2)
+| left : partrec ↑(λ n : ℕ, n.unpair.1)
+| right : partrec ↑(λ n : ℕ, n.unpair.2)
 | pair {f g} : partrec f → partrec g → partrec (λ n, mkpair <$> f n <*> g n)
 | comp {f g} : partrec f → partrec g → partrec (λ n, g n >>= f)
 | prec {f g} : partrec f → partrec g → partrec (unpaired (λ a n,

src/computability/partrec_code.lean

@@ -482,8 +482,8 @@ end
 def eval : code → ℕ →. ℕ
 | zero         := pure 0
 | succ         := nat.succ
-| left         := λ n, n.unpair.1
-| right        := λ n, n.unpair.2
+| left         := ↑(λ n : ℕ, n.unpair.1)
+| right        := ↑(λ n : ℕ, n.unpair.2)
 | (pair cf cg) := λ n, mkpair <$> eval cf n <*> eval cg n
 | (comp cf cg) := λ n, eval cg n >>= eval cf
 | (prec cf cg) := nat.unpaired (λ a n,
@@ -596,9 +596,7 @@ theorem evaln_mono : ∀ {k₁ k₂ c n x}, k₁ ≤ k₂ → x ∈ evaln k₁ c
   iterate 4 {exact h},
   { -- pair cf cg
     simp [(<*>)] at h ⊢,
-    exact h.imp (λ a, and.imp
-      (Exists.imp (λ b, and.imp_left (hf _ _)))
-      (Exists.imp (λ b, and.imp_left (hg _ _)))) },
+    exact h.imp (λ a, and.imp (hf _ _) $ Exists.imp $ λ b, and.imp_left (hg _ _)) },
   { -- comp cf cg
     simp at h ⊢,
     exact h.imp (λ a, and.imp (hg _ _) (hf _ _)) },
@@ -621,7 +619,7 @@ theorem evaln_sound : ∀ {k c n x}, x ∈ evaln k c n → x ∈ eval c n
     simp [eval, evaln, (>>), (<*>)] at h ⊢; cases h with _ h,
   iterate 4 {simpa [pure, pfun.pure, eq_comm] using h},
   { -- pair cf cg
-    rcases h with ⟨_, ⟨y, ef, rfl⟩, z, eg, rfl⟩,
+    rcases h with ⟨y, ef, z, eg, rfl⟩,
     exact ⟨_, hf _ _ ef, _, hg _ _ eg, rfl⟩ },
   { --comp hf hg
     rcases h with ⟨y, eg, ef⟩,
@@ -663,8 +661,8 @@ theorem evaln_complete {c n x} : x ∈ eval c n ↔ ∃ k, x ∈ evaln k c n :=
     rcases h with ⟨x, hx, y, hy, rfl⟩,
     rcases hf hx with ⟨k₁, hk₁⟩, rcases hg hy with ⟨k₂, hk₂⟩,
     refine ⟨max k₁ k₂, _⟩,
-    exact ⟨le_max_left_of_le $ nat.le_of_lt_succ $ evaln_bound hk₁, _,
-     ⟨_, evaln_mono (nat.succ_le_succ $ le_max_left _ _) hk₁, rfl⟩,
+    refine ⟨le_max_left_of_le $ nat.le_of_lt_succ $ evaln_bound hk₁,
+      _, evaln_mono (nat.succ_le_succ $ le_max_left _ _) hk₁,
       _, evaln_mono (nat.succ_le_succ $ le_max_right _ _) hk₂, rfl⟩ },
   case nat.partrec.code.comp : cf cg hf hg {
     rcases h with ⟨y, hy, hx⟩,

src/data/finset.lean

@@ -1572,9 +1572,8 @@ lemma bind_subset_bind_of_subset_left {α : Type*} {s₁ s₂ : finset α}
   (t : α → finset β) (h : s₁ ⊆ s₂) : s₁.bind t ⊆ s₂.bind t :=
 begin
   intro x,
-  simp only [and_imp, mem_bind, exists_prop, exists_imp_distrib],
-  intros y hy hty,
-  exact ⟨y, h hy, hty⟩
+  simp only [and_imp, mem_bind, exists_prop],
+  exact Exists.imp (λ a ha, ⟨h ha.1, ha.2⟩)
 end
 
 lemma bind_singleton {f : α → β} : s.bind (λa, {f a}) = s.image f :=
@@ -1584,10 +1583,8 @@ lemma image_bind_filter_eq [decidable_eq α] (s : finset β) (g : β → α) :
   (s.image g).bind (λa, s.filter $ (λc, g c = a)) = s :=
 begin
   ext b,
-  simp,
-  split,
-  { rintros ⟨a, ⟨b', _, _⟩, hb, _⟩, exact hb },
-  { rintros hb, exact ⟨g b, ⟨b, hb, rfl⟩, hb, rfl⟩ }
+  suffices : (∃ a, a ∈ s ∧ b ∈ s ∧ g b = g a) ↔ b ∈ s, by simpa,
+  exact ⟨λ ⟨a, ha, hb, hab⟩, hb, λ hb, ⟨b, hb, hb, rfl⟩⟩
 end
 
 end bind

src/data/set/basic.lean

@@ -1000,8 +1000,7 @@ iff.intro
 
 theorem bex_image_iff {f : α → β} {s : set α} {p : β → Prop} :
   (∃ y ∈ f '' s, p y) ↔ (∃ x ∈ s, p (f x)) :=
-⟨λ ⟨y, ⟨x, hx, hxy⟩, hy⟩, ⟨x, hx, hxy.symm ▸ hy⟩,
-  λ ⟨x, hxs, hpx⟩, ⟨f x, mem_image_of_mem f hxs, hpx⟩⟩
+by simp
 
 theorem mem_image_elim {f : α → β} {s : set α} {C : β → Prop} (h : ∀ (x : α), x ∈ s → C (f x)) :
  ∀{y : β}, y ∈ f '' s → C y
@@ -1300,7 +1299,7 @@ theorem forall_range_iff {p : α → Prop} : (∀ a ∈ range f, p a) ↔ (∀ i
 ⟨assume h i, h (f i) (mem_range_self _), assume h a ⟨i, (hi : f i = a)⟩, hi ▸ h i⟩
 
 theorem exists_range_iff {p : α → Prop} : (∃ a ∈ range f, p a) ↔ (∃ i, p (f i)) :=
-⟨assume ⟨a, ⟨i, eq⟩, h⟩, ⟨i, eq.symm ▸ h⟩, assume ⟨i, h⟩, ⟨f i, mem_range_self _, h⟩⟩
+by simp
 
 lemma exists_range_iff' {p : α → Prop} :
   (∃ a, a ∈ range f ∧ p a) ↔ ∃ i, p (f i) :=

src/linear_algebra/basic.lean

@@ -732,10 +732,10 @@ end
 
 lemma mem_span_insert {y} : x ∈ span R (insert y s) ↔ ∃ (a:R) (z ∈ span R s), x = a • y + z :=
 begin
-  rw [← union_singleton, span_union, mem_sup],
-  simp [mem_span_singleton, add_comm, add_left_comm], split,
-  { rintro ⟨z, hz, _, ⟨a, rfl⟩, rfl⟩, exact ⟨a, z, hz, rfl⟩ },
-  { rintro ⟨a, z, hz, rfl⟩, exact ⟨z, hz, _, ⟨a, rfl⟩, rfl⟩ }
+  simp only [← union_singleton, span_union, mem_sup, mem_span_singleton, exists_prop,
+    exists_exists_eq_and],
+  rw [exists_comm],
+  simp only [eq_comm, add_comm, exists_and_distrib_left]
 end
 
 lemma mem_span_insert' {y} : x ∈ span R (insert y s) ↔ ∃(a:R), x + a • y ∈ span R s :=

src/linear_algebra/linear_pmap.lean

@@ -220,7 +220,7 @@ begin
     rw [← add_assoc, add_right_comm (f _), ← map_add, add_assoc, ← map_add],
     apply fg_eq,
     simp only [coe_add, coe_mk, ← add_assoc],
-    rw [add_right_comm (x _), hxy, add_assoc, hxy] },
+    rw [add_right_comm (x _), hxy, add_assoc, hxy, coe_mk, coe_mk] },
   { intros c z,
     rw [smul_add, ← map_smul, ← map_smul],
     apply fg_eq,

src/logic/basic.lean

@@ -584,6 +584,14 @@ by simp [and_comm]
 @[simp] theorem exists_eq_right {a' : α} : (∃ a, p a ∧ a = a') ↔ p a' :=
 (exists_congr $ by exact λ a, and.comm).trans exists_eq_left
 
+@[simp] theorem exists_exists_and_eq_and {f : α → β} {p : α → Prop} {q : β → Prop} :
+  (∃ b, (∃ a, p a ∧ f a = b) ∧ q b) ↔ ∃ a, p a ∧ q (f a) :=
+⟨λ ⟨b, ⟨a, ha, hab⟩, hb⟩, ⟨a, ha, hab.symm ▸ hb⟩, λ ⟨a, hp, hq⟩, ⟨f a, ⟨a, hp, rfl⟩, hq⟩⟩
+
+@[simp] theorem exists_exists_eq_and {f : α → β} {p : β → Prop} :
+  (∃ b, (∃ a, f a = b) ∧ p b) ↔ ∃ a, p (f a) :=
+⟨λ ⟨b, ⟨a, ha⟩, hb⟩, ⟨a, ha.symm ▸ hb⟩, λ ⟨a, ha⟩, ⟨f a, ⟨a, rfl⟩, ha⟩⟩
+
 @[simp] theorem forall_eq' {a' : α} : (∀a, a' = a → p a) ↔ p a' :=
 by simp [@eq_comm _ a']
 
@@ -593,6 +601,9 @@ by simp [@eq_comm _ a']
 @[simp] theorem exists_eq_right' {a' : α} : (∃ a, p a ∧ a' = a) ↔ p a' :=
 by simp [@eq_comm _ a']
 
+theorem exists_comm {p : α → β → Prop} : (∃ a b, p a b) ↔ ∃ b a, p a b :=
+⟨λ ⟨a, b, h⟩, ⟨b, a, h⟩, λ ⟨b, a, h⟩, ⟨a, b, h⟩⟩
+
 theorem forall_or_of_or_forall (h : b ∨ ∀x, p x) (x) : b ∨ p x :=
 h.imp_right $ λ h₂, h₂ x
 

src/set_theory/cofinality.lean

@@ -285,8 +285,8 @@ begin
     apply not_le_of_lt (typein_lt_type r a),
     rw [← e', sup_le],
     intro i,
-    simp [set.range] at h,
-    simpa using le_of_lt ((typein_lt_typein r).2 (h _ i rfl)) },
+    have h : ∀ (x : ι), r (enum r (f x) _) a, { simpa using h },
+    simpa only [typein_enum] using le_of_lt ((typein_lt_typein r).2 (h i)) },
   { exact λ i, ⟨_, set.mem_range_self i.1⟩ },
   { intro a, rcases a with ⟨_, i, rfl⟩, exact ⟨⟨i⟩, by simp⟩ }
 end

src/tactic/converter/binders.lean

@@ -137,10 +137,6 @@ meta def binder_eq_elim.old_conv (b : binder_eq_elim) : old_conv unit := do
   b.check x (bd.instantiate_var x),
   b.adapt_rel b.push
 
-theorem {u v} exists_comm {α : Sort u} {β : Sort v} (p : α → β → Prop) :
-  (∃a b, p a b) ↔ (∃b a, p a b) :=
-⟨λ⟨a, ⟨b, h⟩⟩, ⟨b, ⟨a, h⟩⟩, λ⟨a, ⟨b, h⟩⟩, ⟨b, ⟨a, h⟩⟩⟩
-
 theorem {u v} exists_elim_eq_left {α : Sort u} (a : α) (p : Π(a':α), a' = a → Prop) :
   (∃(a':α)(h : a' = a), p a' h) ↔ p a rfl :=
 ⟨λ⟨a', ⟨h, p_h⟩⟩, match a', h, p_h with ._, rfl, h := h end, λh, ⟨a, rfl, h⟩⟩