mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.Frontend.Extension.Init
Aesop.declaredRuleSetsRef : IO.Ref Aesop.DeclaredRuleSets
-- Mathlib.Data.ENat.Lattice
ENat.iSup_add_iSup : ∀ {ι : Sort u_2} {f g : ι → ℕ∞}, (∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k) → iSup f + iSup g = ⨆ i, f i + g i
-- Init.Control.Lawful.MonadLift.Instances
_private.Init.Control.Lawful.MonadLift.Instances.0.ExceptT.bindCont.match_1.splitter : {ε α : Type u_1} →
  (motive : Except ε α → Sort u_2) →
    (x : Except ε α) → ((a : α) → motive (Except.ok a)) → ((e : ε) → motive (Except.error e)) → motive x
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.lie_e_f_ne : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (self : LieAlgebra.Basis ι H) (i j : ι),
  i ≠ j → ⁅self.e i, self.f j⁆ = 0
-- Mathlib.Topology.Compactness.Lindelof
isLindelof_iUnion : ∀ {X : Type u} [inst : TopologicalSpace X] {ι : Sort u_2} {f : ι → Set X} [Countable ι],
  (∀ (i : ι), IsLindelof (f i)) → IsLindelof (⋃ i, f i)
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs
/-- An element `x` of an algebra `A` over a commutative ring `R` is said to be *integral*,
if it is a root of some monic polynomial `p : R[X]`.
Equivalently, the element is integral over `R` with respect to the induced `algebraMap`  -/
IsIntegral : (R : Type u_1) → {A : Type u_3} → [inst : CommRing R] → [inst_1 : Ring A] → [Algebra R A] → A → Prop
-- Mathlib.Topology.MetricSpace.Thickening
/-- An exterior point of a subset `E` (i.e., a point outside the closure of `E`) is not in the
closed `δ`-thickening of `E` for small enough positive `δ`.  -/
Metric.eventually_notMem_cthickening_of_infEDist_pos : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {E : Set α} {x : α},
  x ∉ closure E → ∀ᶠ (δ : ℝ) in nhds 0, x ∉ Metric.cthickening δ E
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.instIsEquivalenceUSwitch : FintypeCat.uSwitch.IsEquivalence
-- Mathlib.Topology.Order
inseparable_top : ∀ {α : Type u} (x y : α), Inseparable x y
-- Mathlib.Topology.Algebra.Star.LinearMap
ContinuousLinearMap.intrinsicStar_toSpanSingleton : ∀ {E : Type u_2} [inst : AddCommMonoid E] [inst_1 : StarAddMonoid E] [inst_2 : TopologicalSpace E]
  [inst_3 : ContinuousStar E] {S : Type u_4} [inst_4 : Semiring S] [inst_5 : StarAddMonoid S] [inst_6 : StarModule S S]
  [inst_7 : Module S E] [inst_8 : StarModule S E] [inst_9 : TopologicalSpace S] [inst_10 : ContinuousStar S]
  [inst_11 : ContinuousSMul S E] (a : E),
  star (WithConv.toConv (ContinuousLinearMap.toSpanSingleton S a)) =
    WithConv.toConv (ContinuousLinearMap.toSpanSingleton S (star a))
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr.eq_12 : Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt) =
  Turing.TM2.Stmt.load (fun x => none) Turing.TM2.Stmt.halt
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.range_eq_bot_iff : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] {f : G →* G'}, f.range = ⊥ ↔ f = 1
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
CategoryTheory.Abelian.LeftResolution.karoubi.F_obj_X : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive A] (P : CategoryTheory.Idempotents.Karoubi A),
  ((CategoryTheory.Abelian.LeftResolution.karoubi.F Λ).obj P).X = Λ.F.obj P.X
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A binary bicone is a bilimit bicone if and only if the corresponding bicone is a bilimit.  -/
CategoryTheory.Limits.BinaryBicone.toBiconeIsBilimit : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} → (b : CategoryTheory.Limits.BinaryBicone X Y) → b.toBicone.IsBilimit ≃ b.IsBilimit
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homology_π_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology] {Z : C} (h : S.opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.homologyπ (CategoryTheory.CategoryStruct.comp S.homologyι h) =
    CategoryTheory.CategoryStruct.comp S.iCycles (CategoryTheory.CategoryStruct.comp S.pOpcycles h)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- Construct a `LinearIsometryEquiv` from a `LinearEquiv` and two inequalities:
`∀ x, ‖e x‖ ≤ ‖x‖` and `∀ y, ‖e.symm y‖ ≤ ‖y‖`.  -/
LinearIsometryEquiv.ofBounds : {R : Type u_1} →
  {R₂ : Type u_2} →
    {E : Type u_5} →
      {E₂ : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            {σ₁₂ : R →+* R₂} →
              {σ₂₁ : R₂ →+* R} →
                [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
                  [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                    [inst_4 : SeminormedAddCommGroup E] →
                      [inst_5 : SeminormedAddCommGroup E₂] →
                        [inst_6 : Module R E] →
                          [inst_7 : Module R₂ E₂] →
                            (e : E ≃ₛₗ[σ₁₂] E₂) →
                              (∀ (x : E), ‖e x‖ ≤ ‖x‖) → (∀ (y : E₂), ‖e.symm y‖ ≤ ‖y‖) → E ≃ₛₗᵢ[σ₁₂] E₂
-- Mathlib.Topology.ShrinkingLemma
/-- Sets that correspond to `i ∉ carrier` are not modified.  -/
ShrinkingLemma.PartialRefinement.apply_eq : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} {p : Set X → Prop}
  (self : ShrinkingLemma.PartialRefinement u s p) {i : ι}, i ∉ self.carrier → self.toFun i = u i
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_inv_app_app_τ₂ : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) (X_1 : J),
  (((CategoryTheory.ShortComplex.FunctorEquivalence.counitIso J C).inv.app X).app X_1).τ₂ =
    CategoryTheory.CategoryStruct.id (X.obj X_1).X₂
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.cokernelOpOp_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y),
  (CategoryTheory.cokernelOpOp f).inv =
    (CategoryTheory.Limits.kernel.lift f (CategoryTheory.Limits.cokernel.π f.op).unop ⋯).op
-- Mathlib.LinearAlgebra.Pi
/-- `diag i j` is the identity map if `i = j`. Otherwise it is the constant 0 map.  -/
LinearMap.diag : {R : Type u} →
  {ι : Type x} →
    [inst : Semiring R] →
      {φ : ι → Type i} →
        [inst_1 : (i : ι) → AddCommMonoid (φ i)] →
          [inst_2 : (i : ι) → Module R (φ i)] → [DecidableEq ι] → (i j : ι) → φ i →ₗ[R] φ j
-- Mathlib.CategoryTheory.Enriched.Opposite
CategoryTheory.forgetEnrichmentOppositeEquivalence_inverse : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  [inst_2 : CategoryTheory.BraidedCategory V] (C : Type u) [inst_3 : CategoryTheory.EnrichedCategory V C],
  (CategoryTheory.forgetEnrichmentOppositeEquivalence V C).inverse =
    CategoryTheory.forgetEnrichmentOppositeEquivalence.inverse V C
-- Mathlib.Data.Matrix.Basis
Matrix.single_neg : ∀ {n : Type u_3} {α : Type u_7} [inst : DecidableEq n] [inst_1 : NegZeroClass α] (i j : n) (b : α),
  -Matrix.single i j b = Matrix.single i j (-b)
-- Mathlib.Topology.UniformSpace.Equiv
/-- A uniform inducing equiv between uniform spaces is a uniform isomorphism.  -/
Equiv.toUniformEquivOfIsUniformInducing : {α : Type u} →
  {β : Type u_1} → [inst : UniformSpace α] → [inst_1 : UniformSpace β] → (f : α ≃ β) → IsUniformInducing ⇑f → α ≃ᵤ β
-- Mathlib.Topology.Algebra.Ring.Basic
instIsSemitopologicalSemiringAddOpposite : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] [inst_1 : TopologicalSpace R] [IsSemitopologicalSemiring R],
  IsSemitopologicalSemiring Rᵃᵒᵖ
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
/-- Assume that `S` is a subset of `ι` with finite complement, that each `R i` is weakly locally
compact, and that `A i` is *compact* for all `i ∈ S`. Then the restricted product
`Πʳ i, [R i, A i]_[𝓟 S]` is locally compact.

Note: we spell "`S` has finite complement" as `cofinite ≤ 𝓟 S`.  -/
RestrictedProduct.weaklyLocallyCompactSpace_of_principal : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)] {S : Set ι}
  [∀ (i : ι), WeaklyLocallyCompactSpace (R i)],
  Filter.cofinite ≤ Filter.principal S →
    (∀ i ∈ S, IsCompact (A i)) →
      WeaklyLocallyCompactSpace (RestrictedProduct (fun i => R i) (fun i => A i) (Filter.principal S))
-- Mathlib.GroupTheory.GroupAction.Period
/-- If for some `n`, `m ^ n • a = a`, then `period m a ≤ n`.  -/
MulAction.period_le_of_fixed : ∀ {α : Type v} {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α] {m : M} {a : α} {n : ℕ},
  0 < n → m ^ n • a = a → MulAction.period m a ≤ n
-- Mathlib.LinearAlgebra.QuadraticForm.AlgClosed
/-- The isometry between a weighted sum of squares on an algebraically closed field and the
sum of squares, i.e. `weightedSumSquares` with weights 1 or 0.  -/
QuadraticForm.isometryEquivSumSquares : {ι : Type u_1} →
  [inst : Fintype ι] →
    {K : Type u_2} →
      [inst_1 : Field K] →
        [IsAlgClosed K] →
          [inst_3 : DecidableEq K] →
            (w : ι → K) →
              (QuadraticMap.weightedSumSquares K w).IsometryEquiv
                (QuadraticMap.weightedSumSquares K fun i => if w i = 0 then 0 else 1)
-- Init.Data.Array.Lemmas
Array.append_eq_push_iff : ∀ {α : Type u_1} {xs ys zs : Array α} {x : α},
  xs ++ ys = zs.push x ↔ ys = #[] ∧ xs = zs.push x ∨ ∃ ys', ys = ys'.push x ∧ zs = xs ++ ys'
-- Mathlib.RingTheory.Flat.Basic
Submodule.toBaseChange_injective : ∀ {R : Type u_1} (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [Module.Flat R A]
  {M : Type u_5} [inst_4 : AddCommMonoid M] [inst_5 : Module R M] (p : Submodule R M),
  Function.Injective ⇑(Submodule.toBaseChange A p)
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.cgf_zero_measure : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ}, ProbabilityTheory.cgf X 0 = 0
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.instInhabitedAlgebraId : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [Inhabited C] → Inhabited (CategoryTheory.Endofunctor.Algebra (CategoryTheory.Functor.id C))
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.IsZariskiLocalAtTarget.restrict : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtTarget P]
  {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y}, P f → ∀ (U : Y.Opens), P (f ∣_ U)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_5.go : {motive_1 : Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
  {motive_2 :
      Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
        Sort u} →
    {motive_3 : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
      {motive_4 : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
        {motive_5 : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
          {motive_6 : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
            {motive_7 : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
              {motive_8 : Task Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
                (t : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                  ((t : Lean.Elab.Tactic.TacticParsedSnapshot) → t.below → motive_1 t) →
                    ((t :
                          Lean.Language.TransformedSnap
                            (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot)) →
                        Lean.Elab.Tactic.TacticParsedSnapshot.below_1 t → motive_2 t) →
                      ((t : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                          Lean.Elab.Tactic.TacticParsedSnapshot.below_2 t → motive_3 t) →
                        ((t : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
                            Lean.Elab.Tactic.TacticParsedSnapshot.below_3 t → motive_4 t) →
                          ((t : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                              Lean.Elab.Tactic.TacticParsedSnapshot.below_4 t → motive_5 t) →
                            ((t : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                                Lean.Elab.Tactic.TacticParsedSnapshot.below_5 t → motive_6 t) →
                              ((t : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) →
                                  Lean.Elab.Tactic.TacticParsedSnapshot.below_6 t → motive_7 t) →
                                ((t : Task Lean.Elab.Tactic.TacticParsedSnapshot) →
                                    Lean.Elab.Tactic.TacticParsedSnapshot.below_7 t → motive_8 t) →
                                  motive_6 t ×' Lean.Elab.Tactic.TacticParsedSnapshot.below_5 t
-- Mathlib.LinearAlgebra.Dimension.Constructions
Module.Basis.sumQuot.eq_1 : ∀ {R : Type u_2} {V : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {W : Submodule R V}
  {m : Type u_4} {n : Type u_5} (bW : Module.Basis m R ↥W) (bQ : Module.Basis n R (V ⧸ W)),
  bW.sumQuot bQ = Module.Basis.mk ⋯ ⋯
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
HopfAlgCat.Hom.toBialgHom_injective : ∀ {R : Type u} [inst : CommRing R] (V W : HopfAlgCat R), Function.Injective HopfAlgCat.Hom.toBialgHom
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- Version of `LinearIndepOn.id_insert` that works when the scalars are not a field.  -/
LinearIndepOn.id_insert' : ∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {s : Set M} {x : M},
  LinearIndepOn R id s → (∀ (r : R), r • x ∈ Submodule.span R s → r = 0) → LinearIndepOn R id (insert x s)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_maxKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.contains (t.maxKeyD fallback) = true
-- Std.Internal.Do.PredTrans
Std.Internal.Do.PredTrans.mk : {Pred : Type u} → {EPred : Type v} → {α : Type w} → ((α → Pred) → EPred → Pred) → Std.Internal.Do.PredTrans Pred EPred α
-- Mathlib.Algebra.Order.Pi
Function.one_le_extend : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : One γ] [inst_1 : LE γ] {f : α → β} {g : α → γ} {e : β → γ},
  1 ≤ g → 1 ≤ e → 1 ≤ Function.extend f g e
-- Init.Prelude
/-- The typeclass behind the notation `a ∈ s : Prop` where `a : α`, `s : γ`.
Because `α` is an `outParam`, the "container type" `γ` determines the type
of the elements of the container.
 -/
Membership : outParam (Type u) → Type v → Type (max u v)
-- Mathlib.Algebra.Group.Basic
eq_inv_mul_of_mul_eq : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, b * a = c → a = b⁻¹ * c
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.VersoModuleDocs.DocContext.mk.inj : ∀ {content : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock)}
  {priorParts : Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty)}
  {context : Array Lean.VersoModuleDocs.DocFrame✝} {content_1 : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock)}
  {priorParts_1 : Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty)}
  {context_1 : Array Lean.VersoModuleDocs.DocFrame✝},
  { content := content, priorParts := priorParts, context := context } =
      { content := content_1, priorParts := priorParts_1, context := context_1 } →
    content = content_1 ∧ priorParts = priorParts_1 ∧ context = context_1
-- Mathlib.Geometry.Euclidean.Simplex
Affine.Simplex.acuteAngled_reindex_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {m n : ℕ} {s : Affine.Simplex ℝ P m} (e : Fin (m + 1) ≃ Fin (n + 1)),
  (s.reindex e).AcuteAngled ↔ s.AcuteAngled
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffOn.fst : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : E → F × G} {s : Set E},
  ContDiffOn 𝕜 n f s → ContDiffOn 𝕜 n (fun x => (f x).1) s
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme},
  AlgebraicGeometry.Scheme.JointlySurjective (AlgebraicGeometry.Scheme.precoverage P)
-- Mathlib.Data.Tree.Basic
/-- Induction principle for `BinaryTree Unit`s  -/
BinaryTree.unitRecOn : {motive : BinaryTree Unit → Sort u_1} →
  (t : BinaryTree Unit) →
    motive BinaryTree.nil → ((x y : BinaryTree Unit) → motive x → motive y → motive (BinaryTree.node () x y)) → motive t
-- Mathlib.Computability.DFA
DFA.reindex_apply_start : ∀ {α : Type u} {σ : Type v} {σ' : Type u_2} (g : σ ≃ σ') (M : DFA α σ), ((DFA.reindex g) M).start = g M.start
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContinuousLinearMap.contMDiff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_6} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  (L : E →L[𝕜] F), ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) n ⇑L
-- Mathlib.MeasureTheory.Measure.Content
/-- Extending a content on compact sets to an outer measure on all sets.  -/
MeasureTheory.Content.outerMeasure : {G : Type w} → [inst : TopologicalSpace G] → MeasureTheory.Content G → MeasureTheory.OuterMeasure G
-- Mathlib.Algebra.Group.Hom.Defs
/-- Composition of additive monoid morphisms as an additive monoid morphism.  -/
AddMonoidHom.comp : {M : Type u_4} →
  {N : Type u_5} →
    {P : Type u_6} → [inst : AddZero M] → [inst_1 : AddZero N] → [inst_2 : AddZero P] → (N →+ P) → (M →+ N) → M →+ P
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.pi_eq_zero : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : AddTorsor V1 P1]
  [inst_3 : Module k V1] {ι : Type u_9} {φv : ι → Type u_10} [inst_4 : (i : ι) → AddCommGroup (φv i)]
  [inst_5 : (i : ι) → Module k (φv i)] (fv : (i : ι) → P1 →ᵃ[k] φv i), AffineMap.pi fv = 0 ↔ ∀ (i : ι), fv i = 0
-- Mathlib.Algebra.Group.Basic
mul_zpow_mul : ∀ {G : Type u_3} [inst : Group G] (a b : G) (n : ℤ), (a * b) ^ n * a = a * (b * a) ^ n
-- Lean.Util.LeanOptions
Lean.LeanOptionValue.ofString.sizeOf_spec : ∀ (s : String), sizeOf (Lean.LeanOptionValue.ofString s) = 1 + sizeOf s
-- Mathlib.Analysis.LocallyConvex.AbsConvexOpen
AbsConvexOpenSets.instNonempty : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : TopologicalSpace E] [inst_1 : AddCommMonoid E] [inst_2 : SeminormedRing 𝕜]
  [inst_3 : SMul 𝕜 E] [inst_4 : PartialOrder 𝕜], Nonempty (AbsConvexOpenSets 𝕜 E)
-- Init.Data.SInt.Lemmas
Int8.add_sub_cancel : ∀ (a b : Int8), a + b - b = a
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- The support of the empty graph is empty.  -/
SimpleGraph.support_bot : ∀ {V : Type u}, ⊥.support = ∅
-- Init.Data.String.PosRaw
String.Pos.Raw.addChar_byteIdx : ∀ (p : String.Pos.Raw) (c : Char), (p + c).byteIdx = p.byteIdx + c.utf8Size
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv_restriction_assoc : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) (X₀ : C₀) {Y₀ : C₀}
  (f : F.obj Y₀ ⟶ F.obj X₀) {Z : A} (h : G₀.obj.obj (Opposite.op Y₀) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv data G₀ X₀)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction data G₀ f)
        h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsDenseSubsite.mapPreimage J F G₀ f) h
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.chromaticNumber_ne_top_iff_exists : ∀ {V : Type u} {G : SimpleGraph V}, G.chromaticNumber ≠ ⊤ ↔ ∃ n, G.Colorable n
-- Mathlib.Algebra.Group.Subgroup.Map
AddEquiv.addSubgroupMap_symm_apply : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (e : G ≃+ G') (H : AddSubgroup G)
  (g : ↥(AddSubgroup.map (↑e) H)), (e.addSubgroupMap H).symm g = ⟨e.symm ↑g, ⋯⟩
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Mathlib.Meta.Positivity.log_pos_of_isNat : ∀ {e : ℝ} {n : ℕ}, Mathlib.Meta.NormNum.IsNat e n → Nat.blt 1 n = true → 0 < Real.log e
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.Hom.ext : ∀ {A B : AddCommMonCat} {x y : A.Hom B}, x.hom' = y.hom' → x = y
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcConnectParams.mk : Lean.Lsp.DocumentUri → Lean.Lsp.RpcConnectParams