chore: get cache

Mathlib.lean

@@ -7451,7 +7451,9 @@ public import Mathlib.Tactic.Linter.Multigoal
 public import Mathlib.Tactic.Linter.OldObtain
 public import Mathlib.Tactic.Linter.OverlappingInstances
 public import Mathlib.Tactic.Linter.PPRoundtrip
+public import Mathlib.Tactic.Linter.PrivateInPublic
 public import Mathlib.Tactic.Linter.PrivateModule
+public import Mathlib.Tactic.Linter.PrivateProof
 public import Mathlib.Tactic.Linter.Style
 public import Mathlib.Tactic.Linter.TacticDocumentation
 public import Mathlib.Tactic.Linter.TextBased
@@ -8316,6 +8318,7 @@ public import Mathlib.Util.Notation3
 public import Mathlib.Util.PPOptions
 public import Mathlib.Util.ParseCommand
 public import Mathlib.Util.PrintSorries
+public import Mathlib.Util.PrivateProof
 public import Mathlib.Util.Qq
 public import Mathlib.Util.Simp
 public import Mathlib.Util.SleepHeartbeats

Mathlib/Algebra/Category/FGModuleCat/Basic.lean

@@ -251,13 +251,11 @@ private theorem evaluation_coevaluation :
   ext : 1
   apply contractLeft_assoc_coevaluation' K V
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 instance exactPairing : ExactPairing V (FGModuleCatDual K V) where
   coevaluation' := FGModuleCatCoevaluation K V
   evaluation' := FGModuleCatEvaluation K V
-  coevaluation_evaluation' := coevaluation_evaluation K V
-  evaluation_coevaluation' := evaluation_coevaluation K V
+  coevaluation_evaluation' := private coevaluation_evaluation K V
+  evaluation_coevaluation' := private evaluation_coevaluation K V
 
 instance rightDual : HasRightDual V :=
   ⟨FGModuleCatDual K V⟩

Mathlib/Algebra/Field/ZMod.lean

@@ -24,11 +24,9 @@ private theorem mul_inv_cancel_aux (a : ZMod p) (h : a ≠ 0) : a * a⁻¹ = 1 :
   apply Nat.Coprime.symm
   rwa [Nat.Prime.coprime_iff_not_dvd Fact.out, ← CharP.cast_eq_zero_iff (ZMod p)]
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- Field structure on `ZMod p` if `p` is prime. -/
 instance : Field (ZMod p) where
-  mul_inv_cancel := mul_inv_cancel_aux p
+  mul_inv_cancel := private mul_inv_cancel_aux p
   inv_zero := inv_zero p
   nnqsmul := _
   nnqsmul_def := fun _ _ => rfl

Mathlib/Algebra/Group/End.lean

@@ -389,19 +389,15 @@ set_option backward.privateInPublic true in
 private theorem inv_aux : (∀ x, p (f x) ↔ p x) ↔ ∀ x, p (f⁻¹ x) ↔ p x :=
   f⁻¹.surjective.forall.trans <| by simp [Iff.comm]
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- See `Equiv.Perm.inv_subtypePerm`. -/
 theorem subtypePerm_inv (f : Perm α) (hf) :
-    f⁻¹.subtypePerm hf = (f.subtypePerm <| inv_aux.2 hf : Perm { x // p x })⁻¹ :=
+    f⁻¹.subtypePerm hf = (f.subtypePerm <| private inv_aux.2 hf : Perm { x // p x })⁻¹ :=
   rfl
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- See `Equiv.Perm.subtypePerm_inv`. -/
 @[simp]
 theorem inv_subtypePerm (f : Perm α) (hf) :
-    (f.subtypePerm hf : Perm { x // p x })⁻¹ = f⁻¹.subtypePerm (inv_aux.1 hf) :=
+    (f.subtypePerm hf : Perm { x // p x })⁻¹ = f⁻¹.subtypePerm (private inv_aux.1 hf) :=
   rfl
 
 set_option backward.privateInPublic true in
@@ -410,11 +406,9 @@ private theorem pow_aux (hf : ∀ x, p (f x) ↔ p x) : ∀ {n : ℕ} (x), p ((f
   | _ + 1, _ => (pow_aux hf (f _)).trans (hf _)
 
 set_option backward.isDefEq.respectTransparency false in
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 @[simp]
 theorem subtypePerm_pow (f : Perm α) (n : ℕ) (hf) :
-    (f.subtypePerm hf : Perm { x // p x }) ^ n = (f ^ n).subtypePerm (pow_aux hf) := by
+    (f.subtypePerm hf : Perm { x // p x }) ^ n = (f ^ n).subtypePerm (private pow_aux hf) := by
   induction n with
   | zero => simp
   | succ n ih => simp_rw [pow_succ', ih, subtypePerm_mul]
@@ -426,11 +420,9 @@ private theorem zpow_aux (hf : ∀ x, p (f x) ↔ p x) : ∀ {n : ℤ} (x), p ((
     rw [zpow_negSucc]
     exact pow_aux (inv_aux.1 hf)
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 @[simp]
 theorem subtypePerm_zpow (f : Perm α) (n : ℤ) (hf) :
-    (f.subtypePerm hf ^ n : Perm { x // p x }) = (f ^ n).subtypePerm (zpow_aux hf) := by
+    (f.subtypePerm hf ^ n : Perm { x // p x }) = (f ^ n).subtypePerm (private zpow_aux hf) := by
   cases n with
   | ofNat n => exact subtypePerm_pow _ _ _
   | negSucc n => simp only [zpow_negSucc, subtypePerm_pow, subtypePerm_inv]

Mathlib/Algebra/Lie/BaseChange.lean

@@ -101,24 +101,20 @@ private theorem bracket_leibniz_lie (x y : A ⊗[R] L) (z : A ⊗[R] M) :
     · grind [LinearMap.add_apply]
   · grind [LinearMap.add_apply]
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 instance instLieRing : LieRing (A ⊗[R] L) where
   add_lie x y z := by simp only [bracket_def, LinearMap.add_apply, map_add]
   lie_add x y z := by simp only [bracket_def, map_add]
-  lie_self := bracket_lie_self R A L
-  leibniz_lie := bracket_leibniz_lie R A L L
+  lie_self := private bracket_lie_self R A L
+  leibniz_lie := private bracket_leibniz_lie R A L L
 
 instance instBaseLieAlgebra : LieAlgebra R (A ⊗[R] L) where lie_smul := by simp [bracket_def]
 
 instance instLieAlgebra : LieAlgebra A (A ⊗[R] L) where lie_smul _a _x _y := map_smul _ _ _
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 instance instLieRingModule : LieRingModule (A ⊗[R] L) (A ⊗[R] M) where
   add_lie x y z := by simp only [bracket_def, LinearMap.add_apply, map_add]
   lie_add x y z := by simp only [bracket_def, map_add]
-  leibniz_lie := bracket_leibniz_lie R A L M
+  leibniz_lie := private bracket_leibniz_lie R A L M
 
 instance instLieModule : LieModule A (A ⊗[R] L) (A ⊗[R] M) where
   smul_lie t x m := by simp only [bracket_def, map_smul, LinearMap.smul_apply]

Mathlib/Algebra/Lie/LieTheorem.lean

@@ -146,14 +146,12 @@ private lemma weightSpaceOfIsLieTower_aux (z : L) (v : V) (hv : v ∈ weightSpac
     rw [pow_zero, Module.End.one_apply]
   exact nontrivial_of_ne ⟨v, hvU⟩ 0 <| by simp [hv']
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 variable (R V) in
 /-- The weight space of `V` with respect to `χ : A → R`, a priori a Lie submodule for `A`, is also a
 Lie submodule for `L`. -/
 def weightSpaceOfIsLieTower (χ : A → R) : LieSubmodule R L V :=
   { toSubmodule := weightSpace V χ
-    lie_mem {z v} hv := weightSpaceOfIsLieTower_aux χ z v hv }
+    lie_mem {z v} hv := private weightSpaceOfIsLieTower_aux χ z v hv }
 
 end
 

Mathlib/Algebra/Lie/Weights/RootSystem.lean

@@ -64,13 +64,11 @@ private lemma chainLength_aux (hα : α.IsNonZero) {x} (hx : x ∈ rootSpace H (
   obtain ⟨μ, hμ⟩ := this.exists_nat
   exact ⟨μ, by rw [← Nat.cast_smul_eq_nsmul K, ← hμ, lie_eq_smul_of_mem_rootSpace hx]⟩
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- The length of the `α`-chain through `β`. See `chainBotCoeff_add_chainTopCoeff`. -/
 def chainLength (α β : Weight K H L) : ℕ :=
   letI := Classical.propDecidable
   if hα : α.IsZero then 0 else
-    (chainLength_aux α β hα (chainTop α β).exists_ne_zero.choose_spec.1).choose
+    (private chainLength_aux α β hα (chainTop α β).exists_ne_zero.choose_spec.1 :).choose
 
 lemma chainLength_of_isZero (hα : α.IsZero) : chainLength α β = 0 := dite_eq_left hα
 

Mathlib/Algebra/Module/Injective.lean

@@ -232,18 +232,14 @@ private theorem extensionOfMax_adjoin.aux1 {y : N} (x : supExtensionOfMaxSinglet
   rcases b_mem with ⟨z, eq2⟩
   exact ⟨⟨a, a_mem⟩, z, by rw [← eq1, ← eq2]⟩
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- If `x ∈ M ⊔ ⟨y⟩`, then `x = m + r • y`, `fst` pick an arbitrary such `m`. -/
 def ExtensionOfMaxAdjoin.fst {y : N} (x : supExtensionOfMaxSingleton i f y) :
     (extensionOfMax i f).domain :=
-  (extensionOfMax_adjoin.aux1 i x).choose
+  (private extensionOfMax_adjoin.aux1 i x :).choose
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- If `x ∈ M ⊔ ⟨y⟩`, then `x = m + r • y`, `snd` pick an arbitrary such `r`. -/
 def ExtensionOfMaxAdjoin.snd {y : N} (x : supExtensionOfMaxSingleton i f y) : R :=
-  (extensionOfMax_adjoin.aux1 i x).choose_spec.choose
+  (private extensionOfMax_adjoin.aux1 i x :).choose_spec.choose
 
 theorem ExtensionOfMaxAdjoin.eqn {y : N} (x : supExtensionOfMaxSingleton i f y) :
     ↑x = ↑(ExtensionOfMaxAdjoin.fst i x) + ExtensionOfMaxAdjoin.snd i x • y :=

Mathlib/Algebra/Module/LocalizedModule/Basic.lean

@@ -367,17 +367,15 @@ private theorem zero_smul_aux (p : LocalizedModule S M) : (0 : T) • p = 0 := b
   rw [show (0 : T) = IsLocalization.mk' T (0 : R) (1 : S) by rw [IsLocalization.mk'_zero],
     mk'_smul_mk, zero_smul, zero_mk]
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- If `IsLocalization S T`, then `M[S⁻¹]` is a `T`-module.
 This should eventually be replaced with `IsLocalizedModule f N` and `Module T N`. -/
 noncomputable abbrev moduleOfIsLocalization : Module T (LocalizedModule S M) where
-  one_smul := one_smul_aux
-  mul_smul := mul_smul_aux
-  smul_add := smul_add_aux
-  smul_zero := smul_zero_aux
-  add_smul := add_smul_aux
-  zero_smul := zero_smul_aux
+  one_smul := private one_smul_aux
+  mul_smul := private mul_smul_aux
+  smul_add := private smul_add_aux
+  smul_zero := private smul_zero_aux
+  add_smul := private add_smul_aux
+  zero_smul := private zero_smul_aux
 
 @[simp]
 theorem mk_cancel_common_left (s' s : S) (m : M) : mk (s' • m) (s' * s) = mk m s :=

Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean

@@ -159,11 +159,10 @@ set_option backward.privateInPublic true in
 private theorem end_path : f x₁ = g x₃ := by convert! hfg 1 <;> simp only [Path.target]
 
 set_option backward.isDefEq.respectTransparency false in
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 theorem eq_path_of_eq_image :
     (πₘ (TopCat.ofHom f)).map ⟦p⟧ =
-        hcast (start_path hfg) ≫ (πₘ (TopCat.ofHom g)).map ⟦q⟧ ≫ hcast (end_path hfg).symm := by
+        hcast (private start_path hfg) ≫ (πₘ (TopCat.ofHom g)).map ⟦q⟧ ≫
+          hcast (private (end_path hfg).symm) := by
   rw [conj_eqToHom_iff_heq
     ((πₘ (TopCat.ofHom f)).map ⟦p⟧) ((πₘ (TopCat.ofHom g)).map ⟦q⟧)
     (FundamentalGroupoid.ext <| start_path hfg)

Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean

@@ -187,31 +187,25 @@ def δ1₂ : ⦋1⦌₂ ⟶ ⦋2⦌₂ := δ₂ (n := 1) 1
 /-- The 2nd face of a 2-simplex, as a morphism in the 2-truncated simplex category. -/
 def δ2₂ : ⦋1⦌₂ ⟶ ⦋2⦌₂ := δ₂ (n := 1) 2
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- The arrow in the ReflQuiver `OneTruncation₂ V` of a 2-truncated simplicial set arising from the
 0th face of a 2-simplex. -/
 def ev12₂ {V : SSet.Truncated 2} (φ : V _⦋2⦌₂) : ev1₂ φ ⟶ ev2₂ φ :=
   ⟨V.map δ0₂.op φ,
-    map_map_of_eq V (InducedCategory.hom_ext
+    private map_map_of_eq V (InducedCategory.hom_ext
       (SimplexCategory.δ_comp_δ (i := 0) (j := 1) (by decide)).symm),
-    map_map_of_eq V rfl⟩
+    private map_map_of_eq V rfl⟩
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- The arrow in the ReflQuiver `OneTruncation₂ V` of a 2-truncated simplicial set arising from the
 1st face of a 2-simplex. -/
 def ev02₂ {V : SSet.Truncated 2} (φ : V _⦋2⦌₂) : ev0₂ φ ⟶ ev2₂ φ :=
-  ⟨V.map δ1₂.op φ, map_map_of_eq V rfl, map_map_of_eq V rfl⟩
+  ⟨V.map δ1₂.op φ, private map_map_of_eq V rfl, private map_map_of_eq V rfl⟩
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- The arrow in the ReflQuiver `OneTruncation₂ V` of a 2-truncated simplicial set arising from the
 2nd face of a 2-simplex. -/
 def ev01₂ {V : SSet.Truncated 2} (φ : V _⦋2⦌₂) : ev0₂ φ ⟶ ev1₂ φ :=
   ⟨V.map δ2₂.op φ,
-    map_map_of_eq V (InducedCategory.hom_ext (SimplexCategory.δ_comp_δ (j := 1) le_rfl)),
-    map_map_of_eq V rfl⟩
+    private map_map_of_eq V (InducedCategory.hom_ext (SimplexCategory.δ_comp_δ (j := 1) le_rfl)),
+    private map_map_of_eq V rfl⟩
 
 end Truncated
 

Mathlib/Analysis/InnerProductSpace/TensorProduct.lean

@@ -128,17 +128,15 @@ private protected theorem re_inner_self_nonneg (x : E ⊗[𝕜] F) :
   rw [inner_mapIncl_mapIncl, inner_self y e f, RCLike.ofReal_re]
   exact Finset.sum_nonneg fun _ _ ↦ sq_nonneg _
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 noncomputable instance instNormedAddCommGroup : NormedAddCommGroup (E ⊗[𝕜] F) :=
   letI : InnerProductSpace.Core 𝕜 (E ⊗[𝕜] F) :=
   { conj_inner_symm x y :=
       x.induction_on (by simp [inner]) (y.induction_on (by simp [inner]) (by simp)
         (by simp_all [inner])) (by simp_all [inner])
     add_left _ _ _ := LinearMap.map_add₂ _ _ _ _
     smul_left _ _ _ := LinearMap.map_smulₛₗ₂ _ _ _ _
-    definite := TensorProduct.inner_definite
-    re_inner_nonneg := TensorProduct.re_inner_self_nonneg }
+    definite := private TensorProduct.inner_definite
+    re_inner_nonneg := private TensorProduct.re_inner_self_nonneg }
   this.toNormedAddCommGroup
 
 instance instInnerProductSpace : InnerProductSpace 𝕜 (E ⊗[𝕜] F) := .ofCore _

Mathlib/Analysis/Normed/Lp/PiLp.lean

@@ -599,25 +599,21 @@ section Fintype
 variable [hp : Fact (1 ≤ p)]
 variable [Fintype ι]
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- pseudoemetric space instance on the product of finitely many pseudoemetric spaces, using the
 `L^p` pseudoedistance, and having as uniformity the product uniformity. -/
 instance [∀ i, PseudoEMetricSpace (β i)] : PseudoEMetricSpace (PiLp p β) :=
-  (pseudoEmetricAux p β).replaceUniformity (uniformity_aux p β).symm
+  (pseudoEmetricAux p β).replaceUniformity <| private (uniformity_aux p β).symm
 
 /-- emetric space instance on the product of finitely many emetric spaces, using the `L^p`
 edistance, and having as uniformity the product uniformity. -/
 instance [∀ i, EMetricSpace (α i)] : EMetricSpace (PiLp p α) :=
   EMetricSpace.ofT0PseudoEMetricSpace (PiLp p α)
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- pseudometric space instance on the product of finitely many pseudometric spaces, using the
 `L^p` distance, and having as uniformity the product uniformity. -/
 instance [∀ i, PseudoMetricSpace (β i)] : PseudoMetricSpace (PiLp p β) :=
-  ((pseudoMetricAux p β).replaceUniformity (uniformity_aux p β).symm).replaceBornology fun s =>
-    Filter.ext_iff.1 (cobounded_aux p β).symm sᶜ
+  ((pseudoMetricAux p β).replaceUniformity <| private (uniformity_aux p β).symm).replaceBornology
+  fun s => Filter.ext_iff.1 (private (cobounded_aux p β).symm) sᶜ
 
 /-- metric space instance on the product of finitely many metric spaces, using the `L^p` distance,
 and having as uniformity the product uniformity. -/

Mathlib/Analysis/Normed/Lp/ProdLp.lean

@@ -575,28 +575,24 @@ end ContinuousLinearEquiv
 /-! Throughout the rest of the file, we assume `1 ≤ p`. -/
 variable [hp : Fact (1 ≤ p)]
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- `PseudoEMetricSpace` instance on the product of two pseudoemetric spaces, using the
 `L^p` pseudoedistance, and having as uniformity the product uniformity. -/
 instance instProdPseudoEMetricSpace [PseudoEMetricSpace α] [PseudoEMetricSpace β] :
     PseudoEMetricSpace (WithLp p (α × β)) :=
-  (prodPseudoEMetricAux p α β).replaceUniformity (prod_uniformity_aux p α β).symm
+  (prodPseudoEMetricAux p α β).replaceUniformity <| private (prod_uniformity_aux p α β).symm
 
 /-- `EMetricSpace` instance on the product of two emetric spaces, using the `L^p`
 edistance, and having as uniformity the product uniformity. -/
 instance instProdEMetricSpace [EMetricSpace α] [EMetricSpace β] : EMetricSpace (WithLp p (α × β)) :=
   EMetricSpace.ofT0PseudoEMetricSpace (WithLp p (α × β))
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- `PseudoMetricSpace` instance on the product of two pseudometric spaces, using the
 `L^p` distance, and having as uniformity the product uniformity. -/
 instance instProdPseudoMetricSpace [PseudoMetricSpace α] [PseudoMetricSpace β] :
     PseudoMetricSpace (WithLp p (α × β)) :=
   ((prodPseudoMetricAux p α β).replaceUniformity
-    (prod_uniformity_aux p α β).symm).replaceBornology
-    fun s => Filter.ext_iff.1 (prod_cobounded_aux p α β).symm sᶜ
+    (private (prod_uniformity_aux p α β).symm)).replaceBornology
+    fun s => Filter.ext_iff.1 (private (prod_cobounded_aux p α β).symm) sᶜ
 
 /-- `MetricSpace` instance on the product of two metric spaces, using the `L^p` distance,
 and having as uniformity the product uniformity. -/

Mathlib/Analysis/Normed/Operator/Basic.lean

@@ -372,10 +372,9 @@ private lemma uniformity_eq_seminorm :
     rw [mul_comm] at hδ
     exact le_trans (le_of_opNorm_le_of_le _ hf.le (hε _ hx)) hδ.le
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 instance toPseudoMetricSpace : PseudoMetricSpace (E →SL[σ₁₂] F) := .replaceUniformity
-  ContinuousLinearMap.seminorm.toSeminormedAddCommGroup.toPseudoMetricSpace uniformity_eq_seminorm
+  ContinuousLinearMap.seminorm.toSeminormedAddCommGroup.toPseudoMetricSpace
+    (private uniformity_eq_seminorm)
 
 /-- Continuous linear maps themselves form a seminormed space with respect to the operator norm. -/
 instance toSeminormedAddCommGroup : SeminormedAddCommGroup (E →SL[σ₁₂] F) where

Mathlib/Analysis/Seminorm.lean

@@ -571,8 +571,6 @@ private theorem isLUB_sSup (s : Set (Seminorm 𝕜 E)) (hs₁ : BddAbove s) (hs
     exact le_ciSup ⟨q x, forall_mem_range.mpr fun i : s => hq i.2 x⟩ ⟨p, hp⟩
   · exact ciSup_le fun q => hp q.2 x
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- `Seminorm 𝕜 E` is a conditionally complete lattice.
 
 Note that, while `inf`, `sup` and `sSup` have good definitional properties (corresponding to
@@ -582,7 +580,7 @@ need to use `sInf` on seminorms, then you should probably provide a more workabl
 but this is unlikely to happen so we keep the "bad" definition for now. -/
 noncomputable instance instConditionallyCompleteLattice :
     ConditionallyCompleteLattice (Seminorm 𝕜 E) :=
-  conditionallyCompleteLatticeOfLatticeOfsSup (Seminorm 𝕜 E) Seminorm.isLUB_sSup
+  conditionallyCompleteLatticeOfLatticeOfsSup (Seminorm 𝕜 E) (private Seminorm.isLUB_sSup)
 
 end Classical
 

Mathlib/CategoryTheory/Monoidal/Closed/FunctorCategory/Complete.lean

@@ -65,14 +65,12 @@ set_option backward.privateInPublic.warn false in
 instance (F : I ⥤ C) : IsLeftAdjoint (tensorLeft (incl I ⋙ F)) :=
   (ihom.adjunction (incl I ⋙ F)).isLeftAdjoint
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- Auxiliary definition for `functorCategoryMonoidalClosed` -/
 @[instance_reducible]
 def functorCategoryClosed (F : I ⥤ C) : Closed F :=
-  have := (ihom.adjunction (incl I ⋙ F)).isLeftAdjoint
-  have := isLeftAdjoint_square_lift_comonadic (tensorLeft F) ((whiskeringLeft _ _ C).obj (incl I))
-    ((whiskeringLeft _ _ C).obj (incl I)) (tensorLeft (incl I ⋙ F)) (Iso.refl _)
+  have : (tensorLeft F).IsLeftAdjoint := private isLeftAdjoint_square_lift_comonadic
+    (tensorLeft F) ((whiskeringLeft _ _ C).obj (incl I)) ((whiskeringLeft _ _ C).obj (incl I))
+    (tensorLeft (incl I ⋙ F)) (Iso.refl _)
   { rightAdj := (tensorLeft F).rightAdjoint
     adj := Adjunction.ofIsLeftAdjoint (tensorLeft F) }