feat: supporting lemmas for defining root systems (#8980)

A collection of loosely-related lemmas, split out from other work in the hopes of simplifying review.

Mathlib/Algebra/Module/Basic.lean

@@ -682,6 +682,22 @@ theorem smul_left_injective {x : M} (hx : x ≠ 0) : Function.Injective fun c :
 
 end SMulInjective
 
+instance [NoZeroSMulDivisors ℤ M] : NoZeroSMulDivisors ℕ M :=
+  ⟨fun {c x} hcx ↦ by rwa [nsmul_eq_smul_cast ℤ c x, smul_eq_zero, Nat.cast_eq_zero] at hcx⟩
+
+variable (R M)
+
+theorem NoZeroSMulDivisors.int_of_charZero [CharZero R] : NoZeroSMulDivisors ℤ M :=
+  ⟨fun {z x} h ↦ by simpa [← smul_one_smul R z x] using h⟩
+
+/-- Only a ring of characteristic zero can can have a non-trivial module without additive or
+scalar torsion. -/
+theorem CharZero.of_noZeroSMulDivisors [Nontrivial M] [NoZeroSMulDivisors ℤ M] : CharZero R := by
+  refine ⟨fun {n m h} ↦ ?_⟩
+  obtain ⟨x, hx⟩ := exists_ne (0 : M)
+  replace h : (n : ℤ) • x = (m : ℤ) • x := by simp [zsmul_eq_smul_cast R, h]
+  simpa using smul_left_injective ℤ hx h
+
 end Module
 
 section GroupWithZero

Mathlib/Algebra/Module/Equiv.lean

@@ -659,6 +659,21 @@ instance automorphismGroup : Group (M ≃ₗ[R] M) where
   mul_left_inv f := ext <| f.left_inv
 #align linear_equiv.automorphism_group LinearEquiv.automorphismGroup
 
+@[simp]
+lemma coe_one : ↑(1 : M ≃ₗ[R] M) = id := rfl
+
+@[simp]
+lemma coe_toLinearMap_one : (↑(1 : M ≃ₗ[R] M) : M →ₗ[R] M) = LinearMap.id := rfl
+
+@[simp]
+lemma coe_toLinearMap_mul {e₁ e₂ : M ≃ₗ[R] M} :
+    (↑(e₁ * e₂) : M →ₗ[R] M) = (e₁ : M →ₗ[R] M) * (e₂ : M →ₗ[R] M) := by
+  rfl
+
+theorem coe_pow (e : M ≃ₗ[R] M) (n : ℕ) : ⇑(e ^ n) = e^[n] := hom_coe_pow _ rfl (fun _ _ ↦ rfl) _ _
+
+theorem pow_apply (e : M ≃ₗ[R] M) (n : ℕ) (m : M) : (e ^ n) m = e^[n] m := congr_fun (coe_pow e n) m
+
 /-- Restriction from `R`-linear automorphisms of `M` to `R`-linear endomorphisms of `M`,
 promoted to a monoid hom. -/
 @[simps]

Mathlib/Algebra/Module/LinearMap.lean

@@ -1375,6 +1375,22 @@ theorem smulRight_apply (f : M₁ →ₗ[R] S) (x : M) (c : M₁) : smulRight f
   rfl
 #align linear_map.smul_right_apply LinearMap.smulRight_apply
 
+@[simp]
+lemma smulRight_zero (f : M₁ →ₗ[R] S) : f.smulRight (0 : M) = 0 := by ext; simp
+
+@[simp]
+lemma zero_smulRight (x : M) : (0 : M₁ →ₗ[R] S).smulRight x = 0 := by ext; simp
+
+@[simp]
+lemma smulRight_apply_eq_zero_iff {f : M₁ →ₗ[R] S} {x : M} [NoZeroSMulDivisors S M] :
+    f.smulRight x = 0 ↔ f = 0 ∨ x = 0 := by
+  rcases eq_or_ne x 0 with rfl | hx; simp
+  refine ⟨fun h ↦ Or.inl ?_, fun h ↦ by simp [h.resolve_right hx]⟩
+  ext v
+  replace h : f v • x = 0 := by simpa only [LinearMap.zero_apply] using LinearMap.congr_fun h v
+  rw [smul_eq_zero] at h
+  tauto
+
 end SMulRight
 
 end AddCommMonoid

Mathlib/Data/Finite/Card.lean

@@ -213,4 +213,23 @@ theorem card_union_le (s t : Set α) : Nat.card (↥(s ∪ t)) ≤ Nat.card s +
   · exact Nat.card_eq_zero_of_infinite.trans_le (zero_le _)
 #align set.card_union_le Set.card_union_le
 
+namespace Finite
+
+variable {s t : Set α} (ht : t.Finite)
+
+theorem card_lt_card (hsub : s ⊂ t) : Nat.card s < Nat.card t := by
+  have : Fintype t := Finite.fintype ht
+  have : Fintype s := Finite.fintype (subset ht (subset_of_ssubset hsub))
+  simp only [Nat.card_eq_fintype_card]
+  exact Set.card_lt_card hsub
+
+theorem eq_of_subset_of_card_le (hsub : s ⊆ t) (hcard : Nat.card t ≤ Nat.card s) : s = t :=
+  (eq_or_ssubset_of_subset hsub).elim id fun h ↦ absurd hcard <| not_le_of_lt <| ht.card_lt_card h
+
+theorem equiv_image_eq_iff_subset (e : α ≃ α) (hs : s.Finite) : e '' s = s ↔ e '' s ⊆ s :=
+  ⟨fun h ↦ by rw [h], fun h ↦ hs.eq_of_subset_of_card_le h <|
+    ge_of_eq (Nat.card_congr (e.image s).symm)⟩
+
+end Finite
+
 end Set

Mathlib/Data/Set/Finite.lean

@@ -934,6 +934,22 @@ theorem finite_le_nat (n : ℕ) : Set.Finite { i | i ≤ n } :=
   toFinite _
 #align set.finite_le_nat Set.finite_le_nat
 
+section MapsTo
+
+variable {s : Set α} {f : α → α} (hs : s.Finite) (hm : MapsTo f s s)
+
+theorem Finite.surjOn_iff_bijOn_of_mapsTo : SurjOn f s s ↔ BijOn f s s := by
+  refine ⟨fun h ↦ ⟨hm, ?_, h⟩, BijOn.surjOn⟩
+  have : Finite s := finite_coe_iff.mpr hs
+  exact hm.restrict_inj.mp (Finite.injective_iff_surjective.mpr <| hm.restrict_surjective_iff.mpr h)
+
+theorem Finite.injOn_iff_bijOn_of_mapsTo : InjOn f s ↔ BijOn f s s := by
+  refine ⟨fun h ↦ ⟨hm, h, ?_⟩, BijOn.injOn⟩
+  have : Finite s := finite_coe_iff.mpr hs
+  exact hm.restrict_surjective_iff.mp (Finite.injective_iff_surjective.mp <| hm.restrict_inj.mpr h)
+
+end MapsTo
+
 section Prod
 
 variable {s : Set α} {t : Set β}

Mathlib/Data/Set/Function.lean

@@ -372,6 +372,11 @@ theorem MapsTo.val_restrict_apply (h : MapsTo f s t) (x : s) : (h.restrict f s t
   rfl
 #align set.maps_to.coe_restrict_apply Set.MapsTo.val_restrict_apply
 
+theorem MapsTo.coe_iterate_restrict {f : α → α} (h : MapsTo f s s) (x : s) (k : ℕ) :
+    h.restrict^[k] x = f^[k] x := by
+  induction' k with k ih; · simp
+  simp only [iterate_succ', comp_apply, val_restrict_apply, ih]
+
 /-- Restricting the domain and then the codomain is the same as `MapsTo.restrict`. -/
 @[simp]
 theorem codRestrict_restrict (h : ∀ x : s, f x ∈ t) :
@@ -1004,6 +1009,10 @@ theorem BijOn.image_eq (h : BijOn f s t) : f '' s = t :=
   h.surjOn.image_eq_of_mapsTo h.mapsTo
 #align set.bij_on.image_eq Set.BijOn.image_eq
 
+lemma _root_.Equiv.image_eq_iff_bijOn (e : α ≃ β) : e '' s = t ↔ BijOn e s t :=
+  ⟨fun h ↦ ⟨(mapsTo_image e s).mono_right h.subset, e.injective.injOn _, h ▸ surjOn_image e s⟩,
+  BijOn.image_eq⟩
+
 lemma bijOn_id (s : Set α) : BijOn id s s := ⟨s.mapsTo_id, s.injOn_id, s.surjOn_id⟩
 #align set.bij_on_id Set.bijOn_id
 

Mathlib/Data/Set/Image.lean

@@ -290,11 +290,17 @@ theorem image_congr' {f g : α → β} {s : Set α} (h : ∀ x : α, f x = g x)
   image_congr fun x _ => h x
 #align set.image_congr' Set.image_congr'
 
+@[gcongr]
+lemma image_mono (h : s ⊆ t) : f '' s ⊆ f '' t := by
+  rintro - ⟨a, ha, rfl⟩; exact mem_image_of_mem f (h ha)
+
 theorem image_comp (f : β → γ) (g : α → β) (a : Set α) : f ∘ g '' a = f '' (g '' a) :=
   Subset.antisymm (ball_image_of_ball fun _ ha => mem_image_of_mem _ <| mem_image_of_mem _ ha)
     (ball_image_of_ball <| ball_image_of_ball fun _ ha => mem_image_of_mem _ ha)
 #align set.image_comp Set.image_comp
 
+theorem image_comp_eq {g : β → γ} : image (g ∘ f) = image g ∘ image f := by ext; simp
+
 /-- A variant of `image_comp`, useful for rewriting -/
 theorem image_image (g : β → γ) (f : α → β) (s : Set α) : g '' (f '' s) = (fun x => g (f x)) '' s :=
   (image_comp g f s).symm
@@ -391,6 +397,9 @@ theorem mem_compl_image [BooleanAlgebra α] (t : α) (S : Set α) :
   simp [← preimage_compl_eq_image_compl]
 #align set.mem_compl_image Set.mem_compl_image
 
+@[simp]
+theorem image_id_eq : image (id : α → α) = id := by ext; simp
+
 /-- A variant of `image_id` -/
 @[simp]
 theorem image_id' (s : Set α) : (fun x => x) '' s = s := by
@@ -401,6 +410,10 @@ theorem image_id' (s : Set α) : (fun x => x) '' s = s := by
 theorem image_id (s : Set α) : id '' s = s := by simp
 #align set.image_id Set.image_id
 
+lemma image_iterate_eq {f : α → α} {n : ℕ} : image (f^[n]) = (image f)^[n] := by
+  induction' n with n ih; · simp
+  rw [iterate_succ', iterate_succ',← ih, image_comp_eq]
+
 theorem compl_compl_image [BooleanAlgebra α] (S : Set α) :
     HasCompl.compl '' (HasCompl.compl '' S) = S := by
   rw [← image_comp, compl_comp_compl, image_id]

Mathlib/Dynamics/FixedPoints/Basic.lean

@@ -100,6 +100,10 @@ theorem preimage_iterate {s : Set α} (h : IsFixedPt (Set.preimage f) s) (n : 
   exact h.iterate n
 #align function.is_fixed_pt.preimage_iterate Function.IsFixedPt.preimage_iterate
 
+lemma image_iterate {s : Set α} (h : IsFixedPt (Set.image f) s) (n : ℕ) :
+    IsFixedPt (Set.image f^[n]) s :=
+  Set.image_iterate_eq ▸ h.iterate n
+
 protected theorem equiv_symm (h : IsFixedPt e x) : IsFixedPt e.symm x :=
   h.to_leftInverse e.leftInverse_symm
 #align function.is_fixed_pt.equiv_symm Function.IsFixedPt.equiv_symm

Mathlib/GroupTheory/OrderOfElement.lean

@@ -351,6 +351,11 @@ theorem orderOf_injective {H : Type*} [Monoid H] (f : G →* H) (hf : Function.I
 #align order_of_injective orderOf_injective
 #align add_order_of_injective addOrderOf_injective
 
+@[to_additive]
+theorem Function.Injective.isOfFinOrder_iff [Monoid H] {f : G →* H} (hf : Injective f) :
+    IsOfFinOrder (f x) ↔ IsOfFinOrder x := by
+  rw [← orderOf_pos_iff, orderOf_injective f hf x, ← orderOf_pos_iff]
+
 @[to_additive (attr := norm_cast, simp)]
 theorem orderOf_submonoid {H : Submonoid G} (y : H) : orderOf (y : G) = orderOf y :=
   orderOf_injective H.subtype Subtype.coe_injective y

Mathlib/GroupTheory/Subgroup/ZPowers.lean

@@ -171,6 +171,11 @@ theorem Int.mem_zmultiples_iff {a b : ℤ} : b ∈ AddSubgroup.zmultiples a ↔
   exists_congr fun k => by rw [mul_comm, eq_comm, ← smul_eq_mul]
 #align int.mem_zmultiples_iff Int.mem_zmultiples_iff
 
+@[simp]
+lemma Int.zmultiples_one : AddSubgroup.zmultiples (1 : ℤ) = ⊤ := by
+  ext z
+  simpa only [AddSubgroup.mem_top, iff_true] using ⟨z, zsmul_int_one z⟩
+
 theorem ofMul_image_zpowers_eq_zmultiples_ofMul {x : G} :
     Additive.ofMul '' (Subgroup.zpowers x : Set G) = AddSubgroup.zmultiples (Additive.ofMul x) := by
   ext y

Mathlib/LinearAlgebra/Span.lean

@@ -190,6 +190,11 @@ theorem span_span_coe_preimage : span R (((↑) : span R s → M) ⁻¹' s) = 
     · exact smul_mem _ _
 #align submodule.span_span_coe_preimage Submodule.span_span_coe_preimage
 
+@[simp]
+lemma span_setOf_mem_eq_top :
+    span R {x : span R s | (x : M) ∈ s} = ⊤ :=
+  span_span_coe_preimage
+
 theorem span_nat_eq_addSubmonoid_closure (s : Set M) :
     (span ℕ s).toAddSubmonoid = AddSubmonoid.closure s := by
   refine' Eq.symm (AddSubmonoid.closure_eq_of_le subset_span _)