fix(*): fix typos I made yesterday (#15627)

Fix 4 typos I made yesterday.

Author: urkud

src/data/set/intervals/ord_connected.lean

@@ -169,7 +169,7 @@ lemma ord_connected.interval_subset (hs : ord_connected s) ⦃x⦄ (hx : x ∈ s
   [x, y] ⊆ s :=
 hs.out (min_rec' (∈ s) hx hy) (max_rec' (∈ s) hx hy)
 
-lemma ord_interval.interval_oc_subset (hs : ord_connected s) ⦃x⦄ (hx : x ∈ s) ⦃y⦄ (hy : y ∈ s) :
+lemma ord_connected.interval_oc_subset (hs : ord_connected s) ⦃x⦄ (hx : x ∈ s) ⦃y⦄ (hy : y ∈ s) :
   Ι x y ⊆ s :=
 Ioc_subset_Icc_self.trans $ hs.interval_subset hx hy
 

src/data/set/prod.lean

@@ -327,7 +327,7 @@ subset_compl_comm.trans $ by simp_rw [← range_diag, range_subset_iff,
 
 @[simp] lemma diag_preimage_prod (s t : set α) : (λ x, (x, x)) ⁻¹' (s ×ˢ t) = s ∩ t := rfl
 
-lemma diag_preimage_prod_sellf (s : set α) : (λ x, (x, x)) ⁻¹' (s ×ˢ s) = s := inter_self s
+lemma diag_preimage_prod_self (s : set α) : (λ x, (x, x)) ⁻¹' (s ×ˢ s) = s := inter_self s
 
 end diagonal
 

src/topology/algebra/module/finite_dimension.lean

@@ -313,11 +313,11 @@ def to_continuous_linear_map : (E →ₗ[𝕜] F') ≃ₗ[𝕜] E →L[𝕜] F'
   f.to_continuous_linear_map.det = f.det :=
 rfl
 
-@[simp] lemma ker_to_continuous_linear_map (f : E →ₗ[𝕜] E) :
+@[simp] lemma ker_to_continuous_linear_map (f : E →ₗ[𝕜] F') :
   f.to_continuous_linear_map.ker = f.ker :=
 rfl
 
-@[simp] lemma range_to_continuous_linear_map (f : E →ₗ[𝕜] E) :
+@[simp] lemma range_to_continuous_linear_map (f : E →ₗ[𝕜] F') :
   f.to_continuous_linear_map.range = f.range :=
 rfl