chore: clean up backward.privateInPublic around d₂₃ (leanprover-community#40228)

Inlines a single-use private declaration, which allows us to get rid of a couple `backward.privateInPublic`s.

This reduces instructions in that file by ~29% (but this gets swallowed in the overall noise).

Note: before this PR, `LieModule.Cohomology.d₂₃_aux._proof_17` was the biggest proof in mathlib (counted with sharing). :) This PR changes it to `CategoryTheory.Functor.IsDenseSubsite.isIso_ranCounit_app_of_isDenseSubsite`.

Author: thorimur

Mathlib/Algebra/Lie/Cochain.lean

@@ -117,26 +117,20 @@ lemma d₁₂_apply_apply_ofTrivial [LieModule.IsTrivial L M] (f : oneCochain R
     d₁₂ R L M f x y = - f ⁅x, y⁆ := by
   simp [trivial_lie_zero]
 
-set_option backward.privateInPublic true in
 /-- The coboundary operator taking degree 2 cochains to a space containing degree 3 cochains. -/
-private def d₂₃Aux (a : twoCochain R L M) : L →ₗ[R] L →ₗ[R] L →ₗ[R] M where
-  toFun x :=
-    { toFun y :=
-        { toFun z := ⁅x, a y z⁆ - ⁅y, a x z⁆ + ⁅z, a x y⁆ - a ⁅x, y⁆ z + a ⁅x, z⁆ y - a ⁅y, z⁆ x
-          map_add' _ _ := by simp; abel
-          map_smul' _ _ := by abel_nf; simp }
+def d₂₃ : twoCochain R L M →ₗ[R] L →ₗ[R] L →ₗ[R] L →ₗ[R] M where
+  toFun a := {
+    toFun x := {
+      toFun y := {
+        toFun z := ⁅x, a y z⁆ - ⁅y, a x z⁆ + ⁅z, a x y⁆ - a ⁅x, y⁆ z + a ⁅x, z⁆ y - a ⁅y, z⁆ x
+        map_add' _ _ := by simp; abel
+        map_smul' _ _ := by simp; abel_nf; simp }
       map_add' _ _ := by ext; simp; abel
-      map_smul' _ _ := by ext; abel_nf; simp }
+      map_smul' _ _ := by ext; simp; abel_nf; simp }
+    map_add' _ _ := by ext; simp; abel
+    map_smul' _ _ := by ext; simp; abel_nf; simp }
   map_add' _ _ := by ext; simp; abel
-  map_smul' _ _ := by ext; abel_nf; simp
-
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
-/-- The coboundary operator taking degree 2 cochains to a space containing degree 3 cochains. -/
-def d₂₃ : twoCochain R L M →ₗ[R] L →ₗ[R] L →ₗ[R] L →ₗ[R] M where
-  toFun := d₂₃Aux R L M
-  map_add' _ _ := by ext; simp [d₂₃Aux]; abel
-  map_smul' _ _ := by ext; simp [d₂₃Aux]; abel_nf; simp
+  map_smul' _ _ := by ext; simp; abel_nf; simp
 
 @[simp]
 lemma d₂₃_apply (a : twoCochain R L M) (x y z : L) :