mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ D` creates finite coproducts, then `F.rightOp : C ⥤ Dᵒᵖ` creates finite
products.  -/
CategoryTheory.Limits.createsFiniteProductsRightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor Cᵒᵖ D) →
          [CategoryTheory.Limits.CreatesFiniteCoproducts F] → CategoryTheory.Limits.CreatesFiniteProducts F.rightOp
-- Mathlib.AlgebraicTopology.DoldKan.FunctorN
AlgebraicTopology.DoldKan.N₂_obj_X_d : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)) (i j : ℕ),
  (AlgebraicTopology.DoldKan.N₂.obj P).X.d i j =
    ChainComplex.of.d (fun n => P.X.obj (Opposite.op { len := n }))
      (AlgebraicTopology.AlternatingFaceMapComplex.objD P.X) i j
-- Mathlib.Topology.LocallyFinsupp
/-- Function with locally finite support have a zero.
 -/
instZeroLocallyFinsuppWithin : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} → {Y : Type u_2} → [inst_1 : Zero Y] → Zero (Function.locallyFinsuppWithin U Y)
-- Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
/-- Generalization of `circleAverage_log_norm_sub_const_eq_posLog`: The
`circleAverage (log ‖· - a‖) c R` equals `log R + log⁺ (|R|⁻¹ * ‖c - a‖)`.
 -/
circleAverage_log_norm_sub_const_eq_log_radius_add_posLog : ∀ {a c : ℂ} {R : ℝ}, R ≠ 0 → Real.circleAverage (fun x => Real.log ‖x - a‖) c R = Real.log R + (R⁻¹ * ‖c - a‖).posLog
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- The iterated derivative commutes with shifting the function by a constant on the left.  -/
iteratedFDeriv_comp_add_left' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  (n : ℕ) (a : E), (iteratedFDeriv 𝕜 n fun z => f (a + z)) = fun x => iteratedFDeriv 𝕜 n f (a + x)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey?_eq_some_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.maxKey? = some (t.maxKeyD fallback)
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.modifyTR.go.eq_3 : ∀ {α : Type u_1} (f : α → α) (a : Array α) (x_3 : α) (xs : List α) (n : ℕ),
  List.modifyTR.go✝ f (x_3 :: xs) n.succ a = List.modifyTR.go✝ f xs n (a.push x_3)
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
/-- The canonical isomorphism `Triangle.shiftFunctor C 0 ≅ 𝟭 (Triangle C)`.  -/
CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        CategoryTheory.Pretriangulated.Triangle.shiftFunctor C 0 ≅
          CategoryTheory.Functor.id (CategoryTheory.Pretriangulated.Triangle C)
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.opEquiv_apply : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (S : Subsemiring R), Subsemiring.opEquiv S = S.op
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.listDecode.eq_6 : ∀ {L : FirstOrder.Language} {α : Type u'} (x : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
  (∀ (n : ℕ) (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
      x = Sum.inr (Sum.inr n.succ.succ) :: l → False) →
    (∀ (n₁ : ℕ) (t₁ : L.Term (α ⊕ Fin n₁)) (n₂ : ℕ) (t₂ : L.Term (α ⊕ Fin n₂))
        (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
        x = Sum.inl ⟨n₁, t₁⟩ :: Sum.inl ⟨n₂, t₂⟩ :: l → False) →
      (∀ (n : ℕ) (R : L.Relations n) (k : ℕ) (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
          x = Sum.inr (Sum.inl ⟨n, R⟩) :: Sum.inr (Sum.inr k) :: l → False) →
        (∀ (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
            x = Sum.inr (Sum.inr 0) :: l → False) →
          (∀ (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
              x = Sum.inr (Sum.inr 1) :: l → False) →
            FirstOrder.Language.BoundedFormula.listDecode x = []
-- Mathlib.Order.Defs.LinearOrder
LinOrd.of.sizeOf_spec : ∀ (carrier : Type u_2) [str : LinearOrder carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- For the versions of this lemma where `μ.singularPart ν` or `ν.withDensity (μ.rnDeriv ν)` are
isolated, see `MeasureTheory.Measure.measure_sub_singularPart` and
`MeasureTheory.Measure.measure_sub_rnDeriv`.  -/
MeasureTheory.Measure.rnDeriv_add_singularPart : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [μ.HaveLebesgueDecomposition ν],
  ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν = μ
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instIsCentralScalar : ∀ {R : Type u_1} {S : Type u_2} {a b : R} [inst : SMul S R] [inst_1 : SMul Sᵐᵒᵖ R] [IsCentralScalar S R],
  IsCentralScalar S (QuadraticAlgebra R a b)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ofHom_zero : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {X Y : Type w} [inst_2 : AddCommGroup X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module k X] [inst_5 : Module k Y] {ρ : Representation k G X}
  {σ : Representation k G Y}, Rep.ofHom 0 = 0
-- Std.Data.ExtDTreeMap.Basic
/-- Returns a list of all values present in the tree map in ascending  order.  -/
Std.ExtDTreeMap.values : {α : Type u} →
  {cmp : α → α → Ordering} → [Std.TransCmp cmp] → {β : Type v} → Std.ExtDTreeMap α (fun x => β) cmp → List β
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
/-- Associating to an element `x` of a vector space `E₂` the continuous multilinear map in `0`
variables taking the (unique) value `x`  -/
ContinuousMultilinearMap.uncurry0 : (𝕜 : Type u) →
  (G : Type wG) →
    {G' : Type wG'} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup G] →
          [inst_2 : NormedSpace 𝕜 G] →
            [inst_3 : NormedAddCommGroup G'] → [inst_4 : NormedSpace 𝕜 G'] → G' → G [×0]→L[𝕜] G'
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Construct the expression for a right-whiskered 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.WhiskerLeft.of : Mathlib.Tactic.BicategoryLike.HorizontalComp → Mathlib.Tactic.BicategoryLike.WhiskerLeft
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.isoWhiskerLeft_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G H : CategoryTheory.Functor D E} (α : G ≅ H), (F.isoWhiskerLeft α).inv = F.whiskerLeft α.inv
-- Mathlib.Analysis.Convex.Deriv
ConvexOn.hasDerivWithinAt_leftDeriv_of_mem_interior : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ},
  ConvexOn ℝ S f → x ∈ interior S → HasDerivWithinAt f (derivWithin f (Set.Iio x) x) (Set.Iio x) x
-- Mathlib.GroupTheory.GroupAction.Hom
/-- If Y/X/M forms a scalar tower, any map X → Y preserving X-action also preserves M-action.  -/
IsScalarTower.smulHomClass : ∀ (M' : Type u_1) (X : Type u_5) [inst : SMul M' X] (Y : Type u_6) [inst_1 : SMul M' Y] (F : Type u_8)
  [inst_2 : FunLike F X Y] [inst_3 : MulOneClass X] [inst_4 : SMul X Y] [IsScalarTower M' X Y]
  [MulActionHomClass F X X Y], MulActionHomClass F M' X Y
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vsub_subset_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s₁ s₂ t₁ t₂ : Set β}, s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ -ᵥ t₁ ⊆ s₂ -ᵥ t₂
-- Batteries.CodeAction.Misc
/-- Returns true if this field is an autoParam or optParam, or if it is given an optional value
in a child struct.  -/
_private.Batteries.CodeAction.Misc.0.Batteries.CodeAction.instanceStub.isAutofillable : Lean.Environment → Lean.StructureFieldInfo → List Lean.Name → Bool
-- Mathlib.RepresentationTheory.Basic
/-- Given a `k`-linear `G`-representation `(V, ρ)`, this is the representation defined by
restricting `ρ` to a `G`-invariant `k`-submodule of `V`.  -/
Representation.subrepresentation : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : Semiring k] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] →
            [inst_3 : Module k V] →
              (ρ : Representation k G V) →
                (W : Submodule k V) → (∀ (g : G), W ≤ Submodule.comap (ρ g) W) → Representation k G ↥W
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.ofMagma_apply : ∀ (R : Type u_8) (M : Type u_9) [inst : Semiring R] [inst_1 : Mul M] (a : M),
  (MonoidAlgebra.ofMagma R M) a = MonoidAlgebra.single a 1
-- Std.Time.Date.Unit.Year
/-- The Common Era (CE), represents dates from year 0 onwards.  -/
Std.Time.Year.Era.ce : Std.Time.Year.Era
-- Mathlib.Data.Set.Basic
/-- **Alias** of the forward direction of `Set.le_iff_subset`. -/
LE.le.subset : ∀ {α : Type u} {s t : Set α}, s ⊆ t → s ⊆ t
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.ne_zero_of_eq_add_single : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddMonoid R] [inst_2 : Zero Γ] {x y : HahnSeries Γ R},
  x = y + (HahnSeries.single x.order) x.leadingCoeff → y ≠ 0 → x ≠ 0
-- Mathlib.Algebra.Group.Action.Faithful
/-- Typeclass for faithful actions.  -/
FaithfulVAdd : (G : Type u_4) → (P : Type u_5) → [VAdd G P] → Prop
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.restrictFreeVar.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : DecidableEq α] (x l : ℕ) (R : L.Relations l)
  (ts : Fin l → L.Term (α ⊕ Fin x)) (f : ↥(FirstOrder.Language.BoundedFormula.rel R ts).freeVarFinset → β),
  (FirstOrder.Language.BoundedFormula.rel R ts).restrictFreeVar f =
    FirstOrder.Language.BoundedFormula.rel R fun i => (ts i).restrictVarLeft (f ∘ Set.inclusion ⋯)
-- Mathlib.Analysis.Normed.Algebra.GelfandFormula
/-- The **spectral mapping theorem** for polynomials in a Banach algebra over `ℂ`.  -/
spectrum.map_polynomial_aeval : ∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [CompleteSpace A] [Nontrivial A] (a : A)
  (p : Polynomial ℂ), spectrum ℂ ((Polynomial.aeval a) p) = (fun k => Polynomial.eval k p) '' spectrum ℂ a
-- Mathlib.LinearAlgebra.Eigenspace.Pi
/-- Given a family of endomorphisms `i ↦ f i`, a family of candidate eigenvalues `i ↦ μ i`, and a
distinguished index `i` whose maximal generalised `μ i`-eigenspace is invariant w.r.t. every `f j`,
taking simultaneous maximal generalised eigenspaces is unaffected by first restricting to the
distinguished generalised `μ i`-eigenspace.  -/
Module.End.iInf_maxGenEigenspace_restrict_map_subtype_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (f : ι → Module.End R M) {μ : ι → R} (i : ι)
  (h : ∀ (j : ι), Set.MapsTo ⇑(f j) ↑((f i).maxGenEigenspace (μ i)) ↑((f i).maxGenEigenspace (μ i))),
  Submodule.map ((f i).maxGenEigenspace (μ i)).subtype
      (⨅ j, (fun j => Module.End.maxGenEigenspace (LinearMap.restrict (f j) ⋯) (μ j)) j) =
    ⨅ j, (f j).maxGenEigenspace (μ j)
-- Mathlib.Probability.BrownianMotion.Basic
ProbabilityTheory.IsPreBrownianReal.neg : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.IsPreBrownianReal B P → ProbabilityTheory.IsPreBrownianReal (-B) P
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.mem_preimage : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {x : ↥X} {U : Y.Opens},
  x ∈ (TopologicalSpace.Opens.map f.base).obj U ↔ f x ∈ U
-- Mathlib.RingTheory.Etale.Basic
Algebra.FormallyEtale.iff_restrictScalars : ∀ {R : Type u} {A : Type v} {B : Type u_1} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B] [Algebra.FormallyEtale R A],
  Algebra.FormallyEtale R B ↔ Algebra.FormallyEtale A B
-- Mathlib.Tactic.DefEqAbuse
/-- > **WARNING:** `#defeq_abuse` is an experimental tool intended to assist with breaking
changes to transparency handling. Its syntax may change at any time, and it may not behave as
expected. Please report unexpected behavior [on Zulip](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/backward.2EisDefEq.2ErespectTransparency/with/575685551).

`#defeq_abuse in tac` runs `tac` with `backward.isDefEq.respectTransparency` both `true` and
`false`. If the tactic succeeds with `false` but fails with `true`, it identifies the specific
`isDefEq` checks that fail with the stricter setting.

The tactic still executes (using the permissive setting if needed), so proofs remain valid
during debugging.
 -/
Mathlib.Tactic.DefEqAbuse.defeqAbuse : Lean.ParserDescr
-- Mathlib.Data.Set.Lattice
Set.mem_sUnion_of_mem : ∀ {α : Type u_1} {x : α} {t : Set α} {S : Set (Set α)}, x ∈ t → t ∈ S → x ∈ ⋃₀ S
-- Mathlib.Topology.ContinuousMap.StarOrdered
ContinuousSqrt.sqrt_mul_sqrt : ∀ {R : Type u_1} {inst : LE R} {inst_1 : NonUnitalSemiring R} {inst_2 : TopologicalSpace R} [self : ContinuousSqrt R]
  (x : R × R), x.1 ≤ x.2 → x.2 = x.1 + ContinuousSqrt.sqrt x * ContinuousSqrt.sqrt x
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castSucc_Ici : ∀ {n : ℕ} (i : Fin n), Finset.image Fin.castSucc (Finset.Ici i) = Finset.Ico i.castSucc (Fin.last n)
-- Mathlib.Tactic.Order.Preprocessing
/-- Preprocesses facts for order of `orderType` using either `preprocessFactsPreorder` or
`preprocessFactsPartial` or `preprocessFactsLinear`.  -/
Mathlib.Tactic.Order.preprocessFacts : Array Mathlib.Tactic.Order.AtomicFact →
  Mathlib.Tactic.Order.OrderType → Mathlib.Tactic.AtomM (Array Mathlib.Tactic.Order.AtomicFact)
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.instInhabited : {α : Type u_1} → {β : Type u_2} → [inst : BEq α] → [inst_1 : Hashable α] → Inhabited (Lean.PersistentHashMap α β)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.condExpL2_indicator_ae_eq_smul : ∀ {α : Type u_1} {E' : Type u_3} (𝕜 : Type u_7) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E']
  [inst_2 : InnerProductSpace 𝕜 E'] [inst_3 : CompleteSpace E'] [inst_4 : NormedSpace ℝ E'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : E'),
  ↑↑↑((MeasureTheory.condExpL2 E' 𝕜 hm) (MeasureTheory.indicatorConstLp 2 hs hμs x)) =ᵐ[μ] fun a =>
    ↑↑↑((MeasureTheory.condExpL2 ℝ ℝ hm) (MeasureTheory.indicatorConstLp 2 hs hμs 1)) a • x
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Subspace.mk.sizeOf_spec : ∀ {η : Type u_5} {α : Type u_6} {ι : Type u_7} [inst : SizeOf η] [inst_1 : SizeOf α] [inst_2 : SizeOf ι]
  (idxFun : ι → α ⊕ η) (proper : ∀ (e : η), ∃ i, idxFun i = Sum.inr e),
  sizeOf { idxFun := idxFun, proper := proper } = 1
-- Mathlib.Topology.MetricSpace.Closeds
TopologicalSpace.Closeds.lipschitz_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : EMetricSpace α] [inst_1 : EMetricSpace β], LipschitzWith 1 fun p => p.1 ×ˢ p.2
-- Mathlib.Data.Nat.Choose.Factorization
Nat.factorization_factorial_le_div_pred : ∀ {p : ℕ}, Nat.Prime p → ∀ (n : ℕ), n.factorial.factorization p ≤ n / (p - 1)
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.instRpcEncodableVersionedHtml : Lean.Server.RpcEncodable ProofWidgets.RefreshComponent.VersionedHtml
-- Mathlib.RingTheory.Spectrum.Prime.Noetherian
IsArtinianRing.exists_not_mem_forall_mem_of_ne : ∀ {R : Type u_1} [inst : CommRing R] [IsArtinianRing R] (p : Ideal R) [p.IsPrime],
  ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
-- Init.Data.List.Basic
/-- Returns the largest element of the list if it is not empty, or `none` if it is empty.

Examples:
* `[].max? = none`
* `[4].max? = some 4`
* `[1, 4, 2, 10, 6].max? = some 10`
 -/
List.max? : {α : Type u} → [Max α] → List α → Option α
-- Mathlib.Topology.Path
Path.mk.injEq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (toContinuousMap : C(↑unitInterval, X))
  (source' : toContinuousMap.toFun 0 = x) (target' : toContinuousMap.toFun 1 = y)
  (toContinuousMap_1 : C(↑unitInterval, X)) (source'_1 : toContinuousMap_1.toFun 0 = x)
  (target'_1 : toContinuousMap_1.toFun 1 = y),
  ({ toContinuousMap := toContinuousMap, source' := source', target' := target' } =
      { toContinuousMap := toContinuousMap_1, source' := source'_1, target' := target'_1 }) =
    (toContinuousMap = toContinuousMap_1)
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.domRestrict_piecewise_compl`. -/
Set.restrict_piecewise_compl : ∀ {α : Type u_1} {β : Type u_2} (f g : α → β) (s : Set α) [inst : (x : α) → Decidable (x ∈ s)],
  sᶜ.domRestrict (s.piecewise f g) = sᶜ.domRestrict g
-- Mathlib.Analysis.Convex.Slope
/-- If `f : 𝕜 → 𝕜` is convex, then for any point `a` the slope of the secant line of `f` through `a`
and `b ≠ a` is monotone with respect to `b`.  -/
ConvexOn.secant_mono : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  ConvexOn 𝕜 s f →
    ∀ {a x y : 𝕜}, a ∈ s → x ∈ s → y ∈ s → x ≠ a → y ≠ a → x ≤ y → (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
-- Init.Data.UInt.Lemmas
UInt32.toUInt64_eq_mod_4294967296_iff : ∀ (a : UInt32) (b : UInt64), a.toUInt64 = b % 4294967296 ↔ a = b.toUInt32
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.prodEquiv.eq_1 : ∀ {G : Type u} [inst : AddGroup G] {H : Type v} [inst_1 : AddGroup H] (A : AddSubgroup G) (B : AddSubgroup H),
  QuotientAddGroup.prodEquiv A B =
    {
      toFun := fun q =>
        Quotient.liftOn' q
          (fun x =>
            match x with
            | (g, h) => (↑g, ↑h))
          ⋯,
      invFun := fun q => Quotient.liftOn₂' q.1 q.2 (fun g h => ↑(g, h)) ⋯, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.monic_X_add_C : ∀ {R : Type u_2} [inst : CommRing R] {ι : Type u_3} (m : MonomialOrder ι) (i : ι) (r : R),
  m.Monic (MvPolynomial.X i + MvPolynomial.C r)
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.mulMapLeftOfSupEqTop.congr_simp : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {A B : Subalgebra R S} (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤),
  H.mulMapLeftOfSupEqTop H' = H.mulMapLeftOfSupEqTop H'
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] (h : t.WF)
  {l : List α} {k : α}, k ∈ t → (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯)).getKey? k = t.getKey? k
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.map_algebraMap_eq_subst_X : ∀ {R : Type u_2} [inst : CommRing R] {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S] (f : PowerSeries R),
  (PowerSeries.map (algebraMap R S)) f = PowerSeries.subst PowerSeries.X f
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- If two left extensions `E` and `E'` are isomorphic, `E` is a pointwise
left Kan extension iff `E'` is.  -/
CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionEquivOfIso : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} →
                {E E' : L.LeftExtension F} → (E ≅ E') → E.IsPointwiseLeftKanExtension ≃ E'.IsPointwiseLeftKanExtension
-- Mathlib.RingTheory.PowerSeries.PiTopology
/-- Formula for geometric series.  -/
PowerSeries.WithPiTopology.tsum_pow_mul_one_sub_of_constantCoeff_eq_zero : ∀ {R : Type u_3} [inst : TopologicalSpace R] [inst_1 : Ring R] [IsTopologicalRing R] [T2Space R] {f : PowerSeries R},
  PowerSeries.constantCoeff f = 0 → (∑' (i : ℕ), f ^ i) * (1 - f) = 1
-- Mathlib.GroupTheory.Finiteness
Submonoid.FG.biSup : ∀ {M : Type u_1} [inst : Monoid M] {ι : Type u_3} {s : Set ι},
  s.Finite → ∀ (P : ι → Submonoid M), (∀ i ∈ s, (P i).FG) → (⨆ i ∈ s, P i).FG
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instContinuousEval : ∀ {X : Type u_1} {R : Type u_3} [inst : Zero X] [inst_1 : Zero R] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace R] [LocallyCompactPair X R], ContinuousEval (ContinuousMapZero X R) X R
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_insert_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {a fallback : α} {b : β a}, (Std.DTreeMap.Internal.Impl.insert a b t ⋯).impl.getKeyD a fallback = a
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.castLE.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u'} (x x_1 : ℕ) (x_2 : x ≤ x_1) (l : ℕ) (R : L.Relations l)
  (ts : Fin l → L.Term (α ⊕ Fin x)),
  FirstOrder.Language.BoundedFormula.castLE x_2 (FirstOrder.Language.BoundedFormula.rel R ts) =
    FirstOrder.Language.BoundedFormula.rel R (FirstOrder.Language.Term.relabel (Sum.map id (Fin.castLE x_2)) ∘ ts)
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement'_of_disjoint_and_mul_eq_univ : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, Disjoint H K → ↑H * ↑K = Set.univ → H.IsComplement' K
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- If `n₁ ≥ n₂` and `K₁ ⊆ K₂`, `monoCLM 𝕜` is the continuous `𝕜`-linear inclusion of
`𝓓^{n₁}_{K₁}(E, F)` inside `𝓓^{n₂}_{K₂}(E, F)`. Otherwise, this is the zero map.

Furthermore:
* it is a topological embedding when `n₁ = n₂` and `K₁ ⊆ K₂` (not in Mathlib as of March 2026).
* it maps bounded sets to compact sets when `n₁ ≥ n₂ + 1` and `K₁ ⊆ K₂` (not in Mathlib as of
March 2026).

The parameters `n₁, n₂, K₁, K₂` are implicit as they can often be inferred from context, or
specified by a type ascription.
 -/
ContDiffMapSupportedIn.monoCLM : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace ℝ E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace ℝ F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : SMulCommClass ℝ 𝕜 F] →
                    {n₁ n₂ : ℕ∞} →
                      {K₁ K₂ : TopologicalSpace.Compacts E} →
                        ContDiffMapSupportedIn E F n₁ K₁ →L[𝕜] ContDiffMapSupportedIn E F n₂ K₂
-- Mathlib.Topology.Bases
TopologicalSpace.separableSpace_sum_iff : ∀ {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [inst : TopologicalSpace β],
  TopologicalSpace.SeparableSpace (α ⊕ β) ↔ TopologicalSpace.SeparableSpace α ∧ TopologicalSpace.SeparableSpace β
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.hom_inv_leftUnitor : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {X : Rep.{u, u, v} k G},
  Rep.Hom.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv = ↑(Representation.TensorProduct.lid k X.ρ).symm
-- Mathlib.Topology.Irreducible
preimage_mem_irreducibleComponents : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {t : Set X},
  t ∈ irreducibleComponents X →
    ∀ {f : Y → X}, Topology.IsOpenEmbedding f → (t ∩ Set.range f).Nonempty → f ⁻¹' t ∈ irreducibleComponents Y
-- Mathlib.Order.Booleanisation
Booleanisation.instBoundedOrder : {α : Type u_1} → [inst : GeneralizedBooleanAlgebra α] → BoundedOrder (Booleanisation α)