mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Cones
/-- Cones on `F : Jᵒᵖ ⥤ C` are equivalent to cocones on `F.rightOp : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.coconeRightOpOfConeEquiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor Jᵒᵖ C} → (CategoryTheory.Limits.Cone F)ᵒᵖ ≌ CategoryTheory.Limits.Cocone F.rightOp
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
Ideal.inertiaEquiv.congr_simp : ∀ {M : Type u_1} [inst : Group M] {N : Type u_4} [inst_1 : Group N] {R : Type u_5} [inst_2 : Ring R]
  [inst_3 : MulSemiringAction M R] [inst_4 : MulSemiringAction N R] (I : Ideal R) (e e_1 : M ≃* N) (e_e : e = e_1)
  (he : ∀ (m : M) (x : R), e m • x = m • x), I.inertiaEquiv e he = I.inertiaEquiv e_1 ⋯
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.whiskerLeft_ι_colimitCompWhiskeringLeftIsoCompColimit_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂}
  [inst_3 : CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C))
  (G : CategoryTheory.Functor D K) [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J C] (j : J),
  CategoryTheory.CategoryStruct.comp (G.whiskerLeft (CategoryTheory.Limits.colimit.ι F j))
      (CategoryTheory.Limits.colimitCompWhiskeringLeftIsoCompColimit F G).inv =
    CategoryTheory.Limits.colimit.ι (F.comp ((CategoryTheory.Functor.whiskeringLeft D K C).obj G)) j
-- Mathlib.RingTheory.Multiplicity
emultiplicity_eq_zero_iff_multiplicity_eq_zero : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, emultiplicity a b = 0 ↔ multiplicity a b = 0
-- Mathlib.Topology.UniformSpace.Closeds
isSymm_hausdorffEntourage : ∀ {α : Type u_1} (U : SetRel α α) [U.IsSymm], (hausdorffEntourage U).IsSymm
-- Lean.Message
Lean.addMessageContextPartial : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadOptions m] → Lean.MessageData → m Lean.MessageData
-- Mathlib.Analysis.Seminorm
Seminorm.uniformContinuous : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : UniformSpace E] [IsUniformAddGroup E] [ContinuousConstSMul 𝕜 E] {p : Seminorm 𝕜 E} {r : ℝ},
  p.ball 0 r ∈ nhds 0 → UniformContinuous ⇑p
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited α] {f : α → β → γ} {k : α}, (Std.HashMap.map f m).getKey! k = m.getKey! k
-- Init.Data.Float.Model.Format.Valid
Float.Model.Format.Valid.mk : ∀ {spec : Float.Model.Format} {b : BitVec spec.numBits},
  (Float.Model.UnpackedFloat.unpackExponent b = -1#spec.exponentBits →
      Float.Model.UnpackedFloat.unpackMantissa b ≠ 0#spec.mantissaBitsWithoutImplicit →
        b = Float.Model.UnpackedFloat.packedNaN spec) →
    spec.Valid b
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.degreeLT.addLinearEquiv_apply : ∀ {m n : ℕ} {R : Type u_2} [inst : Ring R] (f : ↥(Polynomial.degreeLT R (m + n))),
  (Polynomial.degreeLT.addLinearEquiv R m n) f = (⟨↑f %ₘ Polynomial.X ^ m, ⋯⟩, ⟨↑f /ₘ Polynomial.X ^ m, ⋯⟩)
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- normed group instance on the product of finitely many normed groups, using the `L^p` norm.  -/
PiLp.normedAddCommGroup : (p : ENNReal) →
  {ι : Type u_2} →
    (α : ι → Type u_3) →
      [hp : Fact (1 ≤ p)] → [Fintype ι] → [(i : ι) → NormedAddCommGroup (α i)] → NormedAddCommGroup (PiLp p α)
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.instInhabited.eq_1 : ∀ {G : Type u_1} [inst : Group G], Subgroup.instInhabited = { default := ⊥ }
-- Mathlib.CategoryTheory.Types.Basic
/-- **Alias** of `CategoryTheory.Functor.map_inv_hom_apply`. -/
CategoryTheory.FunctorToTypes.map_hom_map_inv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : Y ⟶ X) [inst_2 : CategoryTheory.IsIso f] {F_1 : D → D → Type uF}
  {carrier : D → Type w} {instFunLike : (X Y : D) → FunLike (F_1 X Y) (carrier X) (carrier Y)}
  [inst_3 : CategoryTheory.ConcreteCategory D F_1] (x : carrier (F.obj X)),
  (CategoryTheory.ConcreteCategory.hom (F.map f))
      ((CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.inv f))) x) =
    x
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Directed.Iic_ciInf : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderInf α] [Nonempty ι] {f : ι → α},
  Directed (fun x1 x2 => x2 ≤ x1) f → BddBelow (Set.range f) → Set.Iic (⨅ i, f i) = ⋂ i, Set.Iic (f i)
-- Mathlib.CategoryTheory.Sites.Subsheaf
CategoryTheory.Subfunctor.to_sheafify_lift_unique : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.Subfunctor F),
  CategoryTheory.Presieve.IsSheaf J F' →
    ∀ (l₁ l₂ : (CategoryTheory.Subfunctor.sheafify J G).toFunctor ⟶ F'),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.homOfLe ⋯) l₁ =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.homOfLe ⋯) l₂ →
        l₁ = l₂
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.balLeft.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α) (z : α)
  (c : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) → (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a y b))
  (h_2 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (b : RBTree.RBNode α) →
          (z : α) →
            (c : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c))
  (h_3 : (r : RBTree.RBNode α) → motive r),
  (match RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c with
    | RBTree.RBNode.node RBTree.RBColor.black a y b => h_1 a y b
    | RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c => h_2 a y b z c
    | r => h_3 r) =
    h_2 a y b z c
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_insertIfNew_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k}, Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl = true
-- Mathlib.Order.Bounds.Image
IsCoinitialFor.image_of_monotone : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s t : Set α} {f : α → β},
  IsCoinitialFor s t → Monotone f → IsCoinitialFor (f '' s) (f '' t)
-- Mathlib.CategoryTheory.Limits.ColimitLimit
/-- Since `colimit_limit_to_limit_colimit` is a morphism from a colimit to a limit,
this lemma characterises it.
 -/
CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π_apply : ∀ {J : Type u₁} {K : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (J × K) C)
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape K C] (j : J)
  (k : K) {F_1 : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F_1 X Y) (carrier X) (carrier Y)} [inst_5 : CategoryTheory.ConcreteCategory C F_1]
  (x :
    carrier
      (((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).comp CategoryTheory.Limits.lim).obj
        k)),
  (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj F).comp CategoryTheory.Limits.colim) j))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimitLimitToLimitColimit F))
        ((CategoryTheory.ConcreteCategory.hom
            (CategoryTheory.Limits.colimit.ι
              ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).comp
                CategoryTheory.Limits.lim)
              k))
          x)) =
    (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj F).obj j) k))
      ((CategoryTheory.ConcreteCategory.hom
          (CategoryTheory.Limits.limit.π
            ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).obj k) j))
        x)
-- Mathlib.Algebra.Opposites
AddOpposite.op_div : ∀ {α : Type u_1} [inst : Div α] (a b : α), AddOpposite.op (a / b) = AddOpposite.op a / AddOpposite.op b
-- Mathlib.Order.Filter.Basic
Filter.skolem : ∀ {ι : Type u_2} {α : ι → Type u_3} [∀ (i : ι), Nonempty (α i)] {P : (i : ι) → α i → Prop} {F : Filter ι},
  (∀ᶠ (i : ι) in F, ∃ b, P i b) ↔ ∃ b, ∀ᶠ (i : ι) in F, P i (b i)
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.comp_assoc : ∀ {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} {𝕜₃ : Type u_7} {𝕜₄ : Type u_8} {E : Type u_9} {F : Type u_10} {G : Type u_11}
  {H : Type u_12} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] [inst_2 : NormedField 𝕜₃] [inst_3 : NormedField 𝕜₄]
  {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₁₃ : 𝕜₁ →+* 𝕜₃} {σ₁₄ : 𝕜₁ →+* 𝕜₄} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₃₄ : 𝕜₃ →+* 𝕜₄}
  [inst_4 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_5 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄]
  [inst_6 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [inst_7 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [inst_8 : AddCommGroup E]
  [inst_9 : TopologicalSpace E] [inst_10 : Module 𝕜₁ E] [inst_11 : AddCommGroup F] [inst_12 : TopologicalSpace F]
  [inst_13 : Module 𝕜₂ F] [inst_14 : AddCommGroup G] [inst_15 : TopologicalSpace G] [inst_16 : Module 𝕜₃ G]
  [inst_17 : AddCommGroup H] [inst_18 : TopologicalSpace H] [inst_19 : Module 𝕜₄ H] (g₃₄ : G →SWOT[σ₃₄] H)
  (g₂₃ : F →SWOT[σ₂₃] G) (g₁₂ : E →SWOT[σ₁₂] F), (g₃₄.comp g₂₃).comp g₁₂ = g₃₄.comp (g₂₃.comp g₁₂)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} [inst_2 : Inhabited (β k)] {f : β k → β k},
  (t.modify k f).get! k = (Option.map f (t.get? k)).get!
-- Mathlib.Tactic.Positivity.Basic
Mathlib.Meta.Positivity.ite_nonneg_of_nonneg_of_pos : ∀ {α : Type u_1} [inst : Zero α] (p : Prop) [inst_1 : Decidable p] {a b : α} [inst_2 : Preorder α],
  0 ≤ a → 0 < b → 0 ≤ if p then a else b
-- Init.Data.Iterators.Producers.Monadic.List
Std.Iterators.Types.ListIterator.instFinite : ∀ {α : Type w} {m : Type w → Type w'} [inst : Pure m], Std.Iterators.Finite (Std.Iterators.Types.ListIterator α) m
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.continuousMapClass : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N], ContinuousMapClass (M [⋀^ι]→L[R] N) (ι → M) N
-- Mathlib.Util.CompileInductive
/-- Returns true if the given declaration has a `@[csimp]` lemma.  -/
Mathlib.Util.hasCSimpLemma : Lean.Environment → Lean.Name → Bool
-- Mathlib.Topology.Algebra.Order.Archimedean
/-- **Alias** of `AddSubgroup.dense_xor_cyclic`.

---

In a nontrivial densely linear ordered archimedean topological additive group,
a subgroup is either dense or is cyclic, but not both.

For a non-exclusive `Or` version with weaker assumptions, see `AddSubgroup.dense_or_cyclic` above.
 -/
AddSubgroup.dense_xor'_addCyclic : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [inst_3 : TopologicalSpace G]
  [OrderTopology G] [Archimedean G] [Nontrivial G] [DenselyOrdered G] (s : AddSubgroup G),
  Xor (Dense ↑s) (∃ a, s = AddSubgroup.zmultiples a)
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.uniq : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} {D : Type uD}
  [inst_1 : CategoryTheory.Category.{uD', uD} D] (G₁ G₂ : CategoryTheory.Functor W.Localization D),
  W.Q.comp G₁ = W.Q.comp G₂ → G₁ = G₂
-- Mathlib.Topology.Compactness.Compact
Ultrafilter.le_nhds_lim : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactSpace X] (F : Ultrafilter X), ↑F ≤ nhds F.lim
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.PolyCnstr.norm : Nat.Internal.Linear.PolyCnstr → Nat.Internal.Linear.PolyCnstr
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- **Alias** of `ValuativeRel.vle_of_veq`. -/
ValuativeRel.veq.vle : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y : R}, x =ᵥ y → x ≤ᵥ y
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.mul_apply : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (χ χ' : MulChar R R') (a : R),
  (χ * χ') a = χ a * χ' a
-- Mathlib.Algebra.GCDMonoid.Nat
Int.eq_of_associated_of_nonneg : ∀ {a b : ℤ}, Associated a b → 0 ≤ a → 0 ≤ b → a = b
-- Aesop.Util.Basic
Aesop.withPPAnalyze : {m : Type → Type} → {α : Type} → [Monad m] → [Lean.MonadWithOptions m] → m α → m α
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- Given a pair of maps out of the summands of a binary biproduct,
we obtain a map out of the binary biproduct.  -/
CategoryTheory.Limits.biprod.desc : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {W X Y : C} → [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] → (X ⟶ W) → (Y ⟶ W) → (X ⊞ Y ⟶ W)
-- Mathlib.Data.Set.Prod
Set.eval_image_pi_subset : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι},
  i ∈ s → Function.eval i '' s.pi t ⊆ t i
-- Init.Data.Nat.Div.Basic
/-- See also `sub_mul_div` for a strictly more general version.  -/
Nat.sub_mul_div_of_le : ∀ (x n p : ℕ), n * p ≤ x → (x - n * p) / n = x / n - p
-- Init.Data.UInt.Bitwise
UInt64.toFin_xor : ∀ (a b : UInt64), (a ^^^ b).toFin = a.toFin ^^^ b.toFin
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.im_add : ∀ {R : Type u_1} {a b : R} [inst : Add R] (z w : QuadraticAlgebra R a b), (z + w).im = z.im + w.im
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
DifferentiableWithinAt.mdifferentiableWithinAt_of_comp_extChartAt_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M} {F : Type u_18}
  [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F] {f : M → F} [IsManifold I 1 M],
  DifferentiableWithinAt 𝕜 (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I)
      (↑(extChartAt I x) x) →
    MDiffAt[s] f x
-- Mathlib.MeasureTheory.Order.UpperLower
/-- If we can fit a small ball inside a set `s` intersected with any neighborhood of `x`, then the
density of `s` near `x` is not `0`.

Along with `aux₁`, this proves that `x` is not a Lebesgue point of `s`. This will be used to prove
that the frontier of an order-connected set is null.  -/
_private.Mathlib.MeasureTheory.Order.UpperLower.0.aux₀ : ∀ {ι : Type u_1} [inst : Fintype ι] {s : Set (ι → ℝ)} {x : ι → ℝ},
  (∀ (δ : ℝ),
      0 < δ → ∃ y, Metric.closedBall y (δ / 4) ⊆ Metric.closedBall x δ ∧ Metric.closedBall y (δ / 4) ⊆ interior s) →
    ¬Filter.Tendsto
        (fun r =>
          MeasureTheory.volume (closure s ∩ Metric.closedBall x r) / MeasureTheory.volume (Metric.closedBall x r))
        (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
-- Init.Data.Slice.Operations
/-- Internal function to obtain an iterator from a slice. Users should import `Std.Data.Iterators`
and use `Std.Slice.iter` instead.
 -/
Std.Slice.Internal.iter : {γ : Type u_1} → {α β : Type u_2} → [Std.ToIterator (Std.Slice γ) Id α β] → Std.Slice γ → Std.Iter β
-- Mathlib.Topology.Constructions
SetLike.isDiscrete_iff_discreteTopology : ∀ {X : Type u_5} [inst : TopologicalSpace X] {S : Type u_6} [inst_1 : SetLike S X] {s : S},
  IsDiscrete ↑s ↔ DiscreteTopology ↥s
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
norm_cfc_lt : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p] {f : 𝕜 → 𝕜}
  {a : A} {c : ℝ}, 0 < c → (∀ x ∈ spectrum 𝕜 a, ‖f x‖ < c) → ‖cfc f a‖ < c
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.instLinearTopModuleCatInvariantsFunctor : ∀ {G : Type v} [inst : Group G] {k : Type u} [inst_1 : CommRing k] [inst_2 : TopologicalSpace k],
  CategoryTheory.Functor.Linear k (TopRep.invariantsFunctor k G)
-- Mathlib.Topology.Sion
/-- From the quasi-concavity of `f (x, ·)`, deduce an inclusion of `sublevelLeft` sets  -/
_private.Mathlib.Topology.Sion.0.Sion.sublevelLeft_subset_union : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} [inst : LinearOrder β] {X : Set E} {Y : Set F} {f : E → F → β}
  [inst_1 : AddCommGroup F] [inst_2 : Module ℝ F],
  (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) →
    ∀ (b : β) (y y' : ↑Y) (z : ↑(segment ℝ ↑y ↑y')),
      Sion.sublevelLeft✝ X f b ↑z ⊆ Sion.sublevelLeft✝ X f b ↑y ∪ Sion.sublevelLeft✝ X f b ↑y'
-- Lean.Elab.PreDefinition.Structural.Preprocess
/-- Preprocesses the expressions to improve the effectiveness of `elimRecursion`.

* Beta reduce terms where the recursive function occurs in the lambda term.
Example:
```
def f : Nat → Nat
  | 0 => 1
  | i+1 => (fun x => f x) i
```

* Floats out the RecApp markers.
Example:
```
def f : Nat → Nat
  | 0 => 1
  | i+1 => (f x) i
```

* Unfold auxiliary definitions abstracting over the function call
(typically abstracted) proofs.

 -/
Lean.Elab.Structural.preprocess : Lean.Expr → Array Lean.Name → ℕ → Lean.CoreM Lean.Expr
-- Mathlib.Analysis.InnerProductSpace.Laplacian
bilinearIteratedFDerivWithinTwo.eq_1 : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F)
  (s : Set E) (x : E),
  bilinearIteratedFDerivWithinTwo 𝕜 f s x = ContinuousLinearMap.toLinearMap₁₂ (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.PushoutCocone.unop_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z}
  (c : CategoryTheory.Limits.PushoutCocone f g), c.unop.snd = c.inr.unop
-- Lean.Meta.Tactic.Grind.MarkNestedSubsingletons
/-- Wrap nested proofs and decidable instances in `e` with `Lean.Grind.nestedProof` and `Lean.Grind.nestedDecidable`-applications.
Recall that the congruence closure module has special support for them.
 -/
Lean.Meta.Grind.markNestedSubsingletons : Lean.Expr → Lean.Meta.Grind.GrindM Lean.Expr
-- Mathlib.RingTheory.MvPolynomial.Ideal
MvPolynomial.restrictSupportIdeal.eq_1 : ∀ {σ : Type u} (R : Type v) [inst : CommSemiring R] (s : Set (σ →₀ ℕ)) (hs : IsUpperSet s),
  MvPolynomial.restrictSupportIdeal R s hs =
    { toAddSubmonoid := (MvPolynomial.restrictSupport R s).toAddSubmonoid, smul_mem' := ⋯ }
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- Twice the circumradius of a triangle may be expressed explicitly as the length of a side
divided by the sine of the angle at the third point (a version of the law of sines or sine rule).  -/
Affine.Triangle.dist_div_sin_angle_eq_two_mul_circumradius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        dist (t.points i₁) (t.points i₃) /
            Real.sin (EuclideanGeometry.angle (t.points i₁) (t.points i₂) (t.points i₃)) =
          2 * Affine.Simplex.circumradius t
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rcc_eq_cons_iff : ∀ {xs : List ℤ} {m n a : ℤ}, (m...=n).toList = a :: xs ↔ m = a ∧ m ≤ n ∧ ((m + 1)...=n).toList = xs
-- Mathlib.Order.Hom.CompleteLattice
/-- `id` as a `CompleteLatticeHom`.  -/
CompleteLatticeHom.id : (α : Type u_2) → [inst : CompleteLattice α] → CompleteLatticeHom α α
-- Mathlib.Algebra.Star.Basic
Units.instStarModule : ∀ {R : Type u} [inst : Monoid R] [inst_1 : StarMul R] {A : Type u_1} [inst_2 : Star A] [inst_3 : SMul R A]
  [StarModule R A], StarModule Rˣ A
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.eq' : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) {a₁ b₁ : M} {a₂ b₂ : ↥S}, f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ (Localization.r S) (a₁, a₂) (b₁, b₂)
-- Lean.Parser.Term.Basic
Lean.Parser.Term.implicitBinder.parenthesizer : optParam Bool false → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.shiftFunctor_obj_obj : ∀ {S : Type u_1} [inst : AddCommGroupWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (n : S)
  (X : CategoryTheory.DifferentialObject S C),
  ((CategoryTheory.DifferentialObject.shiftFunctor C n).obj X).obj = (CategoryTheory.shiftFunctor C n).obj X.obj
-- Mathlib.CategoryTheory.Functor.TwoSquare
/-- The vertical composition of 2-squares.  -/
CategoryTheory.TwoSquare.vComp : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B : CategoryTheory.Functor C₃ C₄} →
                        {C₇ : Type u₇} →
                          {C₈ : Type u₈} →
                            [inst_4 : CategoryTheory.Category.{v₇, u₇} C₇] →
                              [inst_5 : CategoryTheory.Category.{v₈, u₈} C₈] →
                                {L' : CategoryTheory.Functor C₃ C₇} →
                                  {R'' : CategoryTheory.Functor C₄ C₈} →
                                    {B'' : CategoryTheory.Functor C₇ C₈} →
                                      CategoryTheory.TwoSquare T L R B →
                                        CategoryTheory.TwoSquare B L' R'' B'' →
                                          CategoryTheory.TwoSquare T (L.comp L') (R.comp R'') B''
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.exists_basicOpen_le_affine_inter : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {V : X.Opens},
      AlgebraicGeometry.IsAffineOpen V → ∀ x ∈ U ⊓ V, ∃ f g, X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.insertManyIfNewUnit_nil : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit},
  Std.DHashMap.Const.insertManyIfNewUnit m [] = m
-- Mathlib.LinearAlgebra.AffineSpace.Slope
LinearMap.slope_comp : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E] {F : Type u_4}
  [inst_3 : AddCommGroup F] [inst_4 : Module k F] (f : E →ₗ[k] F) (g : k → E) (a b : k),
  slope (⇑f ∘ g) a b = f (slope g a b)
-- Mathlib.Data.Set.Lattice
Set.sdiff_iUnion : ∀ {β : Type u_2} {ι : Sort u_5} [Nonempty ι] (s : Set β) (t : ι → Set β), s \ ⋃ i, t i = ⋂ i, s \ t i
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
AlgebraicIndependent.algebraMap_aevalEquiv : ∀ {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] (hx : AlgebraicIndependent R x) (p : MvPolynomial ι R),
  (algebraMap (↥(Algebra.adjoin R (Set.range x))) A) (hx.aevalEquiv p) = (MvPolynomial.aeval x) p