feat(algebra|data): misc lemmas in low-level files (#16948)

* From the sphere eversion project

Author: fpvandoorn

src/algebra/big_operators/basic.lean

@@ -461,6 +461,23 @@ begin
   {intros b hb, use j b hb, use hj b hb, exact (right_inv b hb).symm,},
 end
 
+/-- Reindexing a product over a finset along an equivalence.
+See `equiv.prod_comp` for the version where `s` and `s'` are `univ`. -/
+@[to_additive /-" Reindexing a sum over a finset along an equivalence.
+See `equiv.sum_comp` for the version where `s` and `s'` are `univ`. "-/]
+lemma equiv.prod_comp_finset {ι'} [decidable_eq ι] (e : ι ≃ ι') (f : ι' → β) {s' : finset ι'}
+  {s : finset ι}
+  (h : s = s'.image e.symm) :
+  ∏ i' in s', f i' = ∏ i in s, f (e i) :=
+begin
+  rw [h],
+  refine finset.prod_bij' (λ i' hi', e.symm i') (λ a ha, finset.mem_image_of_mem _ ha)
+    (λ a ha, by simp_rw [e.apply_symm_apply]) (λ i hi, e i) (λ a ha, _)
+    (λ a ha, e.apply_symm_apply a) (λ a ha, e.symm_apply_apply a),
+  rcases finset.mem_image.mp ha with ⟨i', hi', rfl⟩,
+  rwa [e.apply_symm_apply]
+end
+
 @[to_additive] lemma prod_finset_product
   (r : finset (γ × α)) (s : finset γ) (t : γ → finset α)
   (h : ∀ p : γ × α, p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1) {f : γ × α → β} :

src/algebra/big_operators/finprod.lean

@@ -734,6 +734,10 @@ end
 lemma finprod_comp {g : β → M} (e : α → β) (he₀ : function.bijective e) :
   ∏ᶠ i, g (e i) = ∏ᶠ j, g j := finprod_eq_of_bijective e he₀ (λ x, rfl)
 
+@[to_additive]
+lemma finprod_comp_equiv (e : α ≃ β) {f : β → M} : ∏ᶠ i, f (e i) = ∏ᶠ i', f i' :=
+finprod_comp e e.bijective
+
 @[to_additive] lemma finprod_set_coe_eq_finprod_mem (s : set α) : ∏ᶠ j : s, f j = ∏ᶠ i ∈ s, f i :=
 begin
   rw [← finprod_mem_range, subtype.range_coe],

src/algebra/group/prod.lean

@@ -47,6 +47,16 @@ lemma swap_mul [has_mul M] [has_mul N] (p q : M × N) : (p * q).swap = p.swap *
 @[to_additive]
 lemma mul_def [has_mul M] [has_mul N] (p q : M × N) : p * q = (p.1 * q.1, p.2 * q.2) := rfl
 
+@[to_additive]
+lemma one_mk_mul_one_mk [monoid M] [has_mul N] (b₁ b₂ : N) :
+  ((1 : M), b₁) * (1, b₂) = (1, b₁ * b₂) :=
+by rw [mk_mul_mk, mul_one]
+
+@[to_additive]
+lemma mk_one_mul_mk_one [has_mul M] [monoid N] (a₁ a₂ : M) :
+  (a₁, (1 : N)) * (a₂, 1) = (a₁ * a₂, 1) :=
+by rw [mk_mul_mk, mul_one]
+
 @[to_additive]
 instance [has_one M] [has_one N] : has_one (M × N) := ⟨(1, 1)⟩
 

src/algebra/module/basic.lean

@@ -168,6 +168,10 @@ lemma finset.sum_smul {f : ι → R} {s : finset ι} {x : M} :
   (∑ i in s, f i) • x = (∑ i in s, (f i) • x) :=
 ((smul_add_hom R M).flip x).map_sum f s
 
+@[simp] lemma smul_add_one_sub_smul {R : Type*} [ring R] [module R M]
+  {r : R} {m : M} : r • m + (1 - r) • m = m :=
+by rw [← add_smul, add_sub_cancel'_right, one_smul]
+
 end add_comm_monoid
 
 variables (R)

src/algebra/order/group/basic.lean

@@ -1038,6 +1038,9 @@ max_eq_right $ h.trans (neg_nonneg.2 h)
 lemma abs_of_neg (h : a < 0) : |a| = -a :=
 abs_of_nonpos h.le
 
+lemma abs_le_abs_of_nonneg (ha : 0 ≤ a) (hab : a ≤ b) : |a| ≤ |b| :=
+by rwa [abs_of_nonneg ha, abs_of_nonneg (ha.trans hab)]
+
 @[simp] lemma abs_zero : |0| = (0:α) :=
 abs_of_nonneg le_rfl
 
@@ -1087,6 +1090,9 @@ decidable.not_iff_not.1 $ ne_comm.trans $ (abs_nonneg a).lt_iff_ne.symm.trans ab
 
 variable [covariant_class α α (swap (+)) (≤)]
 
+lemma abs_le_abs_of_nonpos (ha : a ≤ 0) (hab : b ≤ a) : |a| ≤ |b| :=
+by { rw [abs_of_nonpos ha, abs_of_nonpos (hab.trans ha)], exact neg_le_neg_iff.mpr hab }
+
 lemma abs_lt : |a| < b ↔ - b < a ∧ a < b :=
 max_lt_iff.trans $ and.comm.trans $ by rw [neg_lt]
 

src/data/real/nnreal.lean

@@ -837,6 +837,8 @@ rfl
 @[simp] lemma nnabs_of_nonneg {x : ℝ} (h : 0 ≤ x) : nnabs x = to_nnreal x :=
 by { ext, simp [coe_to_nnreal x h, abs_of_nonneg h] }
 
+lemma nnabs_coe (x : ℝ≥0) : nnabs x = x := by simp
+
 lemma coe_to_nnreal_le (x : ℝ) : (to_nnreal x : ℝ) ≤ |x| :=
 max_le (le_abs_self _) (abs_nonneg _)
 

src/data/set/finite.lean

@@ -564,6 +564,10 @@ theorem finite.of_finite_image {s : set α} {f : α → β} (h : (f '' s).finite
 by { casesI h, exact ⟨fintype.of_injective (λ a, (⟨f a.1, mem_image_of_mem f a.2⟩ : f '' s))
                        (λ a b eq, subtype.eq $ hi a.2 b.2 $ subtype.ext_iff_val.1 eq)⟩ }
 
+lemma finite_of_finite_preimage {f : α → β} {s : set β} (h : (f ⁻¹' s).finite)
+  (hs : s ⊆ range f) : s.finite :=
+by { rw [← image_preimage_eq_of_subset hs], exact finite.image f h }
+
 theorem finite.of_preimage {f : α → β} {s : set β} (h : (f ⁻¹' s).finite) (hf : surjective f) :
   s.finite :=
 hf.image_preimage s ▸ h.image _

src/data/set/function.lean

@@ -476,6 +476,9 @@ theorem inj_on.comp (hg : inj_on g t) (hf: inj_on f s) (h : maps_to f s t) :
   inj_on (g ∘ f) s :=
 λ x hx y hy heq, hf hx hy $ hg (h hx) (h hy) heq
 
+lemma _root_.function.injective.inj_on_range (h : injective (g ∘ f)) : inj_on g (range f) :=
+by { rintros _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ H, exact congr_arg f (h H) }
+
 lemma inj_on_iff_injective : inj_on f s ↔ injective (s.restrict f) :=
 ⟨λ H a b h, subtype.eq $ H a.2 b.2 h,
  λ H a as b bs h, congr_arg subtype.val $ @H ⟨a, as⟩ ⟨b, bs⟩ h⟩
@@ -831,10 +834,9 @@ theorem inv_fun_on_neg (h : ¬ ∃a∈s, f a = b) : inv_fun_on f s b = classical
 by rw [bex_def] at h; rw [inv_fun_on, dif_neg h]
 
 end function
-
-namespace set
 open function
 
+namespace set
 variables {s s₁ s₂ : set α} {t : set β} {f : α → β}
 
 theorem inj_on.left_inv_on_inv_fun_on [nonempty α] (h : inj_on f s) :

src/group_theory/group_action/prod.lean

@@ -41,6 +41,13 @@ variables [has_smul M α] [has_smul M β] [has_smul N α] [has_smul N β] (a : M
 @[to_additive] theorem smul_def (a : M) (x : α × β) : a • x = (a • x.1, a • x.2) := rfl
 @[simp, to_additive] theorem smul_swap : (a • x).swap = a • x.swap := rfl
 
+lemma smul_zero_mk {α : Type*} [monoid M] [add_monoid α] [distrib_mul_action M α] (a : M) (c : β) :
+  a • ((0 : α), c) = (0, a • c) :=
+by rw [prod.smul_mk, smul_zero]
+
+lemma smul_mk_zero {β : Type*} [monoid M] [add_monoid β] [distrib_mul_action M β] (a : M) (b : α) :
+  a • (b, (0 : β)) = (a • b, 0) :=
+by rw [prod.smul_mk, smul_zero]
 
 variables [has_pow α E] [has_pow β E]
 @[to_additive has_smul] instance has_pow : has_pow (α × β) E :=