From e0ccbbe6213c4c7c56e6f664ce0c818d44451037 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgami@math.hu-berlin.de>
Date: Mon, 22 Jul 2024 19:12:47 +0200
Subject: [PATCH] Fix a few lean3 names.

---
 SphereEversion/ToMathlib/Analysis/ContDiff.lean                 | 2 +-
 SphereEversion/ToMathlib/Analysis/Convex/Basic.lean             | 2 +-
 .../ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean      | 2 +-
 SphereEversion/ToMathlib/LinearAlgebra/Basic.lean               | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/SphereEversion/ToMathlib/Analysis/ContDiff.lean b/SphereEversion/ToMathlib/Analysis/ContDiff.lean
index d8330fef..3f59b92f 100644
--- a/SphereEversion/ToMathlib/Analysis/ContDiff.lean
+++ b/SphereEversion/ToMathlib/Analysis/ContDiff.lean
@@ -230,7 +230,7 @@ variable {𝕜 : Type*} [RCLike 𝕜]
 
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E]
 
--- variant of `orthogonal_projection_singleton`
+-- variant of `orthogonalProjection_singleton`
 theorem orthogonalProjection_singleton' {v : E} :
     (𝕜 ∙ v).subtypeL.comp (orthogonalProjection (𝕜 ∙ v)) =
       (1 / (‖v‖ : 𝕜) ^ 2) • .toSpanSingleton 𝕜 v ∘L InnerProductSpace.toDual 𝕜 E v := by
diff --git a/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean
index f6a0564b..bb00c91d 100644
--- a/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean
+++ b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean
@@ -103,7 +103,7 @@ theorem reallyConvexHull_mono : Monotone (reallyConvexHull 𝕜 : Set E → Set
   rintro s t h _ ⟨w, w_pos, supp_w, sum_w, rfl⟩
   exact ⟨w, w_pos, supp_w.trans h, sum_w, rfl⟩
 
-/-- Generalization of `convex` to semirings. We only add the `s = ∅` clause if `𝕜` is trivial. -/
+/-- Generalization of `Convex` to semirings. We only add the `s = ∅` clause if `𝕜` is trivial. -/
 def ReallyConvex (𝕜 : Type*) {E : Type*} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E]
     (s : Set E) : Prop :=
   s = ∅ ∨ ∀ w : E → 𝕜, 0 ≤ w → support w ⊆ s → ∑ᶠ x, w x = 1 → ∑ᶠ x, w x • x ∈ s
diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean
index 662092f6..fe0bd9c2 100644
--- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean
+++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean
@@ -71,7 +71,7 @@ theorem inner_crossProduct_apply_apply_self (u : E) (v : (ℝ ∙ u)ᗮ) : ⟪u
   rw [ω.inner_crossProduct_apply u v v]
   exact ω.volumeForm.map_eq_zero_of_eq ![u, v, v] (by simp) (by norm_num; decide : (1 : Fin 3) ≠ 2)
 
-/-- The map `cross_product`, upgraded from linear to continuous-linear; useful for calculus. -/
+/-- The map `crossProduct`, upgraded from linear to continuous-linear; useful for calculus. -/
 def crossProduct' : E →L[ℝ] E →L[ℝ] E :=
   LinearMap.toContinuousLinearMap
     (↑(LinearMap.toContinuousLinearMap : (E →ₗ[ℝ] E) ≃ₗ[ℝ] E →L[ℝ] E) ∘ₗ ω.crossProduct)
diff --git a/SphereEversion/ToMathlib/LinearAlgebra/Basic.lean b/SphereEversion/ToMathlib/LinearAlgebra/Basic.lean
index 0a901e26..28080f7b 100644
--- a/SphereEversion/ToMathlib/LinearAlgebra/Basic.lean
+++ b/SphereEversion/ToMathlib/LinearAlgebra/Basic.lean
@@ -1,6 +1,6 @@
 import Mathlib.LinearAlgebra.Span
 
-/-! Note: some results should go to `linear_algebra.span`. -/
+/-! Note: some results should go to `LinearAlgebra.Span`. -/
 
 
 open Submodule Function