chore(*): assorted lemmas (#4566)

Non-bc changes:

* make some lemmas use `coe` instead of `subtype.val`;
* make the arguments of `range_comp` explicit, reorder them.

src/data/dfinsupp.lean

@@ -219,7 +219,7 @@ rfl
 
 @[simp] lemma subtype_domain_apply [Π i, has_zero (β i)] {p : ι → Prop} [decidable_pred p]
   {i : subtype p} {v : Π₀ i, β i} :
-  (subtype_domain p v) i = v (i.val) :=
+  (subtype_domain p v) i = v i :=
 quotient.induction_on v $ λ x, rfl
 
 @[simp] lemma subtype_domain_add [Π i, add_monoid (β i)] {p : ι → Prop} [decidable_pred p]
@@ -580,15 +580,13 @@ by ext i; by_cases h1 : p i; by_cases h2 : f i ≠ 0;
 by ext i; by_cases h : p i; simp [h]
 
 lemma subtype_domain_def (f : Π₀ i, β i) :
-  f.subtype_domain p = mk (f.support.subtype p) (λ i, f i.1) :=
-by ext i; cases i with i hi;
-by_cases h1 : p i; by_cases h2 : f i ≠ 0;
-try {simp at h2}; dsimp; simp [h1, h2]
+  f.subtype_domain p = mk (f.support.subtype p) (λ i, f i) :=
+by ext i; by_cases h1 : p i; by_cases h2 : f i ≠ 0;
+try {simp at h2}; dsimp; simp [h1, h2, ← subtype.val_eq_coe]
 
 @[simp] lemma support_subtype_domain {f : Π₀ i, β i} :
   (subtype_domain p f).support = f.support.subtype p :=
-by ext i; cases i with i hi;
-by_cases h1 : p i; by_cases h2 : f i ≠ 0;
+by ext i; by_cases h1 : p i; by_cases h2 : f i ≠ 0;
 try {simp at h2}; dsimp; simp [h1, h2]
 
 end filter_and_subtype_domain
@@ -790,10 +788,9 @@ end
 lemma prod_subtype_domain_index [Π i, has_zero (β i)] [Π i (x : β i), decidable (x ≠ 0)]
   [comm_monoid γ] {v : Π₀ i, β i} {p : ι → Prop} [decidable_pred p]
   {h : Π i, β i → γ} (hp : ∀ x ∈ v.support, p x) :
-  (v.subtype_domain p).prod (λi b, h i.1 b) = v.prod h :=
-finset.prod_bij (λp _, p.val)
-  (by { dsimp, simp })
-  (by simp)
+  (v.subtype_domain p).prod (λi b, h i b) = v.prod h :=
+finset.prod_bij (λp _, p)
+  (by simp) (by simp)
   (assume ⟨a₀, ha₀⟩ ⟨a₁, ha₁⟩, by simp)
   (λ i hi, ⟨⟨i, hp i hi⟩, by simpa using hi, rfl⟩)
 

src/data/equiv/basic.lean

@@ -588,7 +588,7 @@ def pempty_sum (α : Sort*) : pempty ⊕ α ≃ α :=
 @[simp] lemma pempty_sum_apply_inr {α} (a) : pempty_sum α (sum.inr a) = a := rfl
 
 /-- `option α` is equivalent to `α ⊕ punit` -/
-def option_equiv_sum_punit (α : Sort*) : option α ≃ α ⊕ punit.{u+1} :=
+def option_equiv_sum_punit (α : Type*) : option α ≃ α ⊕ punit.{u+1} :=
 ⟨λ o, match o with none := inr punit.star | some a := inl a end,
  λ s, match s with inr _ := none | inl a := some a end,
  λ o, by cases o; refl,
@@ -598,6 +598,14 @@ def option_equiv_sum_punit (α : Sort*) : option α ≃ α ⊕ punit.{u+1} :=
 @[simp] lemma option_equiv_sum_punit_some {α} (a) :
   option_equiv_sum_punit α (some a) = sum.inl a := rfl
 
+@[simp] lemma option_equiv_sum_punit_symm_inl {α} (a) :
+  (option_equiv_sum_punit α).symm (sum.inl a) = a :=
+rfl
+
+@[simp] lemma option_equiv_sum_punit_symm_inr {α} (a) :
+  (option_equiv_sum_punit α).symm (sum.inr a) = none :=
+rfl
+
 /-- The set of `x : option α` such that `is_some x` is equivalent to `α`. -/
 def option_is_some_equiv (α : Type*) : {x : option α // x.is_some} ≃ α :=
 { to_fun := λ o, option.get o.2,

src/data/finset/basic.lean

@@ -1499,17 +1499,21 @@ protected def subtype {α} (p : α → Prop) [decidable_pred p] (s : finset α)
 λ x y H, subtype.eq $ subtype.mk.inj H⟩
 
 @[simp] lemma mem_subtype {p : α → Prop} [decidable_pred p] {s : finset α} :
-  ∀{a : subtype p}, a ∈ s.subtype p ↔ a.val ∈ s
+  ∀{a : subtype p}, a ∈ s.subtype p ↔ (a : α) ∈ s
 | ⟨a, ha⟩ := by simp [finset.subtype, ha]
 
+lemma subtype_eq_empty {p : α → Prop} [decidable_pred p] {s : finset α} :
+  s.subtype p = ∅ ↔ ∀ x, p x → x ∉ s :=
+by simp [ext_iff, subtype.forall, subtype.coe_mk]; refl
+
 /-- `s.subtype p` converts back to `s.filter p` with
 `embedding.subtype`. -/
 @[simp] lemma subtype_map (p : α → Prop) [decidable_pred p] :
   (s.subtype p).map (function.embedding.subtype _) = s.filter p :=
 begin
   ext x,
   rw mem_map,
-  change (∃ a : {x // p x}, ∃ H, a.val = x) ↔ _,
+  change (∃ a : {x // p x}, ∃ H, (a : α) = x) ↔ _,
   split,
   { rintros ⟨y, hy, hyval⟩,
     rw [mem_subtype, hyval] at hy,

src/data/finsupp/basic.lean

@@ -209,14 +209,15 @@ by simp only [single_apply]; ac_refl
 lemma unique_single [unique α] (x : α →₀ β) : x = single (default α) (x (default α)) :=
 by ext i; simp only [unique.eq_default i, single_eq_same]
 
+lemma unique_ext [unique α] {f g : α →₀ β} (h : f (default α) = g (default α)) : f = g :=
+ext $ λ a, by rwa [unique.eq_default a]
+
+lemma unique_ext_iff [unique α] {f g : α →₀ β} : f = g ↔  f (default α) = g (default α) :=
+⟨λ h, h ▸ rfl, unique_ext⟩
+
 @[simp] lemma unique_single_eq_iff [unique α] {b' : β} :
   single a b = single a' b' ↔ b = b' :=
-begin
-  rw [single_eq_single_iff],
-  split,
-  { rintros (⟨_, rfl⟩ | ⟨rfl, rfl⟩); refl },
-  { intro h, left, exact ⟨subsingleton.elim _ _, h⟩ }
-end
+by rw [unique_ext_iff, unique.eq_default a, unique.eq_default a', single_eq_same, single_eq_same]
 
 end single
 
@@ -309,14 +310,14 @@ begin
     { simp only [h, ne.def, ne_self_iff_false] } }
 end
 
-lemma support_emb_domain (f : α₁ ↪ α₂) (v : α₁ →₀ β) :
+@[simp] lemma support_emb_domain (f : α₁ ↪ α₂) (v : α₁ →₀ β) :
   (emb_domain f v).support = v.support.map f :=
 rfl
 
-lemma emb_domain_zero (f : α₁ ↪ α₂) : (emb_domain f 0 : α₂ →₀ β) = 0 :=
+@[simp] lemma emb_domain_zero (f : α₁ ↪ α₂) : (emb_domain f 0 : α₂ →₀ β) = 0 :=
 rfl
 
-lemma emb_domain_apply (f : α₁ ↪ α₂) (v : α₁ →₀ β) (a : α₁) :
+@[simp] lemma emb_domain_apply (f : α₁ ↪ α₂) (v : α₁ →₀ β) (a : α₁) :
   emb_domain f v (f a) = v a :=
 begin
   change dite _ _ _ = _,
@@ -334,10 +335,17 @@ begin
   exact set.mem_range_self a
 end
 
-lemma emb_domain_inj {f : α₁ ↪ α₂} {l₁ l₂ : α₁ →₀ β} :
+lemma emb_domain_injective (f : α₁ ↪ α₂) :
+  function.injective (emb_domain f : (α₁ →₀ β) → (α₂ →₀ β)) :=
+λ l₁ l₂ h, ext $ λ a, by simpa only [emb_domain_apply] using ext_iff.1 h (f a)
+
+@[simp] lemma emb_domain_inj {f : α₁ ↪ α₂} {l₁ l₂ : α₁ →₀ β} :
   emb_domain f l₁ = emb_domain f l₂ ↔ l₁ = l₂ :=
-⟨λ h, ext $ λ a, by simpa only [emb_domain_apply] using ext_iff.1 h (f a),
-  λ h, by rw h⟩
+(emb_domain_injective f).eq_iff
+
+@[simp] lemma emb_domain_eq_zero {f : α₁ ↪ α₂} {l : α₁ →₀ β} :
+  emb_domain f l = 0 ↔ l = 0 :=
+(emb_domain_injective f).eq_iff' $ emb_domain_zero f
 
 lemma emb_domain_map_range
   {β₁ β₂ : Type*} [has_zero β₁] [has_zero β₂]
@@ -1113,7 +1121,7 @@ variables [has_zero β] {v v' : α' →₀ β}
 /-- `subtype_domain p f` is the restriction of the finitely supported function
   `f` to the subtype `p`. -/
 def subtype_domain (p : α → Prop) (f : α →₀ β) : (subtype p →₀ β) :=
-⟨f.support.subtype p, f ∘ subtype.val, λ a, by simp only [mem_subtype, mem_support_iff]⟩
+⟨f.support.subtype p, f ∘ coe, λ a, by simp only [mem_subtype, mem_support_iff]⟩
 
 @[simp] lemma support_subtype_domain {f : α →₀ β} :
   (subtype_domain p f).support = f.support.subtype p :=
@@ -1126,10 +1134,19 @@ rfl
 @[simp] lemma subtype_domain_zero : subtype_domain p (0 : α →₀ β) = 0 :=
 rfl
 
+lemma subtype_domain_eq_zero_iff' {p : α → Prop} {f : α →₀ β} :
+  f.subtype_domain p = 0 ↔ ∀ x, p x → f x = 0 :=
+by simp_rw [← support_eq_empty, support_subtype_domain, subtype_eq_empty, not_mem_support_iff]
+
+lemma subtype_domain_eq_zero_iff {p : α → Prop} {f : α →₀ β} (hf : ∀ x ∈ f.support , p x) :
+  f.subtype_domain p = 0 ↔ f = 0 :=
+subtype_domain_eq_zero_iff'.trans ⟨λ H, ext $ λ x,
+  if hx : p x then H x hx else not_mem_support_iff.1 $ mt (hf x) hx, λ H x _, by simp [H]⟩
+
 @[to_additive]
 lemma prod_subtype_domain_index [comm_monoid γ] {v : α →₀ β}
   {h : α → β → γ} (hp : ∀x∈v.support, p x) :
-  (v.subtype_domain p).prod (λa b, h a.1 b) = v.prod h :=
+  (v.subtype_domain p).prod (λa b, h a b) = v.prod h :=
 prod_bij (λp _, p.val)
   (λ _, mem_subtype.1)
   (λ _ _, rfl)

src/data/option/basic.lean

@@ -195,4 +195,14 @@ def cases_on' : option α → β → (α → β) → β
 | none     n s := n
 | (some a) n s := s a
 
+@[simp] lemma cases_on'_none (x : β) (f : α → β) : cases_on' none x f = x := rfl
+
+@[simp] lemma cases_on'_some (x : β) (f : α → β) (a : α) : cases_on' (some a) x f = f a := rfl
+
+@[simp] lemma cases_on'_coe (x : β) (f : α → β) (a : α) : cases_on' (a : option α) x f = f a := rfl
+
+@[simp] lemma cases_on'_none_coe (f : option α → β) (o : option α) :
+  cases_on' o (f none) (f ∘ coe) = f o :=
+by cases o; refl
+
 end option

src/data/set/basic.lean

@@ -693,6 +693,9 @@ by finish [ext_iff, or_comm]
 @[simp] theorem pair_eq_singleton (a : α) : ({a, a} : set α) = {a} :=
 by finish
 
+theorem pair_comm (a b : α) : ({a, b} : set α) = {b, a} :=
+ext $ λ x, or_comm _ _
+
 @[simp] theorem singleton_nonempty (a : α) : ({a} : set α).nonempty :=
 ⟨a, rfl⟩
 
@@ -1486,21 +1489,27 @@ by simpa only [exists_prop] using exists_range_iff
 theorem range_iff_surjective : range f = univ ↔ surjective f :=
 eq_univ_iff_forall
 
+alias range_iff_surjective ↔ _ function.surjective.range_eq
+
 @[simp] theorem range_id : range (@id α) = univ := range_iff_surjective.2 surjective_id
 
+theorem is_compl_range_inl_range_inr : is_compl (range $ @sum.inl α β) (range sum.inr) :=
+⟨by { rintro y ⟨⟨x₁, rfl⟩, ⟨x₂, _⟩⟩, cc },
+  by { rintro (x|y) -; [left, right]; exact mem_range_self _ }⟩
+
 theorem range_inl_union_range_inr : range (@sum.inl α β) ∪ range sum.inr = univ :=
-by { ext x, cases x; simp }
+is_compl_range_inl_range_inr.sup_eq_top
 
 @[simp] theorem range_quot_mk (r : α → α → Prop) : range (quot.mk r) = univ :=
-range_iff_surjective.2 quot.exists_rep
+(surjective_quot_mk r).range_eq
 
 @[simp] theorem image_univ {ι : Type*} {f : ι → β} : f '' univ = range f :=
 by { ext, simp [image, range] }
 
 theorem image_subset_range {ι : Type*} (f : ι → β) (s : set ι) : f '' s ⊆ range f :=
 by rw ← image_univ; exact image_subset _ (subset_univ _)
 
-theorem range_comp {g : α → β} : range (g ∘ f) = g '' range f :=
+theorem range_comp (g : α → β) (f : ι → α) : range (g ∘ f) = g '' range f :=
 subset.antisymm
   (forall_range_iff.mpr $ assume i, mem_image_of_mem g (mem_range_self _))
   (ball_image_iff.mpr $ forall_range_iff.mpr mem_range_self)
@@ -1699,9 +1708,6 @@ by { intro s, use f ⁻¹' s, rw image_preimage_eq hf }
 lemma injective.image_injective (hf : injective f) : injective (image f) :=
 by { intros s t h, rw [←preimage_image_eq s hf, ←preimage_image_eq t hf, h] }
 
-lemma surjective.range_eq {f : ι → α} (hf : surjective f) : range f = univ :=
-range_iff_surjective.2 hf
-
 lemma surjective.preimage_subset_preimage_iff {s t : set β} (hf : surjective f) :
   f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t :=
 by { apply preimage_subset_preimage_iff, rw [hf.range_eq], apply subset_univ }

src/data/set/function.lean

@@ -49,7 +49,7 @@ lemma restrict_eq (f : α → β) (s : set α) : s.restrict f = f ∘ coe := rfl
 @[simp] lemma restrict_apply (f : α → β) (s : set α) (x : s) : restrict f s x = f x := rfl
 
 @[simp] lemma range_restrict (f : α → β) (s : set α) : set.range (restrict f s) = f '' s :=
-range_comp.trans $ congr_arg (('') f) subtype.range_coe
+(range_comp _ _).trans $ congr_arg (('') f) subtype.range_coe
 
 /-- Restrict codomain of a function `f` to a set `s`. Same as `subtype.coind` but this version
 has codomain `↥s` instead of `subtype s`. -/

src/data/set/lattice.lean

@@ -104,6 +104,9 @@ theorem subset_Inter {t : set β} {s : ι → set β} (h : ∀ i, t ⊆ s i) : t
 -- TODO: should be simpler when sets' order is based on lattices
 @le_infi (set β) _ set.lattice_set _ _ h
 
+theorem subset_Inter_iff {t : set β} {s : ι → set β} : t ⊆ (⋂ i, s i) ↔ ∀ i, t ⊆ s i :=
+@le_infi_iff (set β) _ set.lattice_set _ _
+
 theorem subset_Union : ∀ (s : ι → set β) (i : ι), s i ⊆ (⋃ i, s i) := le_supr
 
 -- This rather trivial consequence is convenient with `apply`,

src/data/sum.lean

@@ -48,6 +48,12 @@ end⟩
 
 namespace sum
 
+lemma injective_inl : function.injective (sum.inl : α → α ⊕ β) :=
+λ x y, sum.inl.inj
+
+lemma injective_inr : function.injective (sum.inr : β → α ⊕ β) :=
+λ x y, sum.inr.inj
+
 /-- Map `α ⊕ β` to `α' ⊕ β'` sending `α` to `α'` and `β` to `β'`. -/
 protected def map (f : α → α') (g : β → β')  : α ⊕ β → α' ⊕ β'
 | (sum.inl x) := sum.inl (f x)

src/logic/nontrivial.lean

@@ -70,6 +70,9 @@ lemma subsingleton_iff : subsingleton α ↔ ∀ (x y : α), x = y :=
 lemma not_nontrivial_iff_subsingleton : ¬(nontrivial α) ↔ subsingleton α :=
 by { rw [nontrivial_iff, subsingleton_iff], push_neg, refl }
 
+lemma not_subsingleton (α) [h : nontrivial α] : ¬subsingleton α :=
+let ⟨⟨x, y, hxy⟩⟩ := h in λ ⟨h'⟩, hxy $ h' x y
+
 /-- A type is either a subsingleton or nontrivial. -/
 lemma subsingleton_or_nontrivial (α : Type*) : subsingleton α ∨ nontrivial α :=
 by { rw [← not_nontrivial_iff_subsingleton, or_comm], exact classical.em _ }

src/measure_theory/simple_func_dense.lean

@@ -137,7 +137,7 @@ begin
   rw [← @subtype.range_coe _ s, ← image_univ, ← dense_seq_dense s] at hx,
   simp only [approx_on, coe_comp],
   refine tendsto_nearest_pt (closure_minimal _ is_closed_closure hx),
-  simp only [nat.range_cases_on, closure_union, @range_comp _ _ _ _ coe],
+  simp only [nat.range_cases_on, closure_union, range_comp coe],
   exact subset.trans (image_closure_subset_closure_image continuous_subtype_coe)
     (subset_union_right _ _)
 end

src/topology/metric_space/gromov_hausdorff.lean

@@ -449,7 +449,7 @@ instance GH_space_metric_space : metric_space GH_space :=
                            ((to_glue_l hΦ hΨ) '' (range (optimal_GH_injr X Y)))
           + Hausdorff_dist ((to_glue_r hΦ hΨ) '' (range (optimal_GH_injl Y Z)))
                            ((to_glue_r hΦ hΨ) '' (range (optimal_GH_injr Y Z))) :
-        by simp only [eq.symm range_comp, Comm, eq_self_iff_true, add_right_inj]
+        by simp only [← range_comp, Comm, eq_self_iff_true, add_right_inj]
       ... = Hausdorff_dist (range (optimal_GH_injl X Y))
                            (range (optimal_GH_injr X Y))
           + Hausdorff_dist (range (optimal_GH_injl Y Z))