feat(*): trivial lemmas from #8903 (#8909)

src/algebra/module/pi.lean

@@ -141,6 +141,13 @@ lemma single_smul {α} [monoid α] [Π i, add_monoid $ f i]
   single i (r • x) = r • single i x :=
 single_op (λ i : I, ((•) r : f i → f i)) (λ j, smul_zero _) _ _
 
+/-- A version of `pi.single_smul` for non-dependent functions. It is useful in cases Lean fails
+to apply `pi.single_smul`. -/
+lemma single_smul'' {α β} [monoid α] [add_monoid β]
+  [distrib_mul_action α β] [decidable_eq I] (i : I) (r : α) (x : β) :
+  single i (r • x) = r • single i x :=
+single_smul i r x
+
 lemma single_smul' {g : I → Type*} [Π i, monoid_with_zero (f i)] [Π i, add_monoid (g i)]
   [Π i, distrib_mul_action (f i) (g i)] [decidable_eq I] (i : I) (r : f i) (x : g i) :
   single i (r • x) = single i r • single i x :=

src/analysis/normed_space/operator_norm.lean

@@ -622,6 +622,8 @@ def lsmul : 𝕜' →L[𝕜] E →L[𝕜] E :=
 ((algebra.lsmul 𝕜 E).to_linear_map : 𝕜' →ₗ[𝕜] E →ₗ[𝕜] E).mk_continuous₂ 1 $
   λ c x, by simpa only [one_mul] using (norm_smul c x).le
 
+@[simp] lemma lsmul_apply (c : 𝕜') (x : E) : lsmul 𝕜 𝕜' c x = c • x := rfl
+
 end smul_linear
 
 section restrict_scalars

src/data/part.lean

@@ -74,6 +74,9 @@ theorem mem.left_unique : relator.left_unique ((∈) : α → part α → Prop)
 theorem get_eq_of_mem {o : part α} {a} (h : a ∈ o) (h') : get o h' = a :=
 mem_unique ⟨_, rfl⟩ h
 
+protected theorem subsingleton (o : part α) : set.subsingleton {a | a ∈ o} :=
+λ a ha b hb, mem_unique ha hb
+
 @[simp] theorem get_some {a : α} (ha : (some a).dom) : get (some a) ha = a := rfl
 
 theorem mem_some (a : α) : a ∈ some a := ⟨trivial, rfl⟩

src/data/subtype.lean

@@ -52,6 +52,12 @@ protected theorem forall' {q : ∀ x, p x → Prop} :
   (∃ x, q x) ↔ (∃ a b, q ⟨a, b⟩) :=
 ⟨assume ⟨⟨a, b⟩, h⟩, ⟨a, b, h⟩, assume ⟨a, b, h⟩, ⟨⟨a, b⟩, h⟩⟩
 
+/-- An alternative version of `subtype.exists`. This one is useful if Lean cannot figure out `q`
+  when using `subtype.exists` from right to left. -/
+protected theorem exists' {q : ∀x, p x → Prop} :
+  (∃ x h, q x h) ↔ (∃ x : {a // p a}, q x x.2) :=
+(@subtype.exists _ _ (λ x, q x.1 x.2)).symm
+
 @[ext] protected lemma ext : ∀ {a1 a2 : {x // p x}}, (a1 : α) = (a2 : α) → a1 = a2
 | ⟨x, h1⟩ ⟨.(x), h2⟩ rfl := rfl
 

src/order/bounded_lattice.lean

@@ -1089,6 +1089,8 @@ by rw [disjoint, disjoint, inf_comm]
 @[symm] theorem disjoint.symm ⦃a b : α⦄ : disjoint a b → disjoint b a :=
 disjoint.comm.1
 
+lemma symmetric_disjoint : symmetric (disjoint : α → α → Prop) := disjoint.symm
+
 @[simp] theorem disjoint_bot_left {a : α} : disjoint ⊥ a := inf_le_left
 @[simp] theorem disjoint_bot_right {a : α} : disjoint a ⊥ := inf_le_right
 

src/order/filter/basic.lean

@@ -2254,6 +2254,10 @@ lemma tendsto.sup {f : α → β} {x₁ x₂ : filter α} {y : filter β} :
   tendsto f x₁ y → tendsto f x₂ y → tendsto f (x₁ ⊔ x₂) y :=
 λ h₁ h₂, tendsto_sup.mpr ⟨ h₁, h₂ ⟩
 
+@[simp] lemma tendsto_supr {f : α → β} {x : ι → filter α} {y : filter β} :
+  tendsto f (⨆ i, x i) y ↔ ∀ i, tendsto f (x i) y :=
+by simp only [tendsto, map_supr, supr_le_iff]
+
 @[simp] lemma tendsto_principal {f : α → β} {l : filter α} {s : set β} :
   tendsto f l (𝓟 s) ↔ ∀ᶠ a in l, f a ∈ s :=
 by simp only [tendsto, le_principal_iff, mem_map', filter.eventually]

src/topology/algebra/monoid.lean

@@ -112,6 +112,13 @@ instance pi.has_continuous_mul {C : ι → Type*} [∀ i, topological_space (C i
 { continuous_mul := continuous_pi (λ i, continuous.mul
     ((continuous_apply i).comp continuous_fst) ((continuous_apply i).comp continuous_snd)) }
 
+/-- A version of `pi.has_continuous_mul` for non-dependent functions. It is needed because sometimes
+Lean fails to use `pi.has_continuous_mul` for non-dependent functions. -/
+@[to_additive "A version of `pi.has_continuous_add` for non-dependent functions. It is needed
+because sometimes Lean fails to use `pi.has_continuous_add` for non-dependent functions."]
+instance pi.has_continuous_mul' : has_continuous_mul (ι → M) :=
+pi.has_continuous_mul
+
 @[priority 100, to_additive]
 instance has_continuous_mul_of_discrete_topology [topological_space N]
   [has_mul N] [discrete_topology N] : has_continuous_mul N :=