mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Linarith.Frontend
/-- Given a list `hyps` of proofs of comparisons, `runLinarith cfg prefType g hyps` preprocesses
`hyps` according to the list of preprocessors in `cfg`. This results in a list of branches
(typically only one), each of which must succeed in order to close the goal.

In each branch, the hypotheses are partitioned by type and `linarith` is run on each class in
turn; one of these must succeed in order for `linarith` to succeed on the branch. If `prefType`
is provided, the corresponding class is tried first.

On success, the metavariable `g` is assigned and the function returns the indices of the
original hypotheses that were used with nonzero coefficient in the final proof.
 -/
Mathlib.Tactic.Linarith.runLinarith : Mathlib.Tactic.Linarith.LinarithConfig → Option Lean.Expr → Lean.MVarId → List Lean.Expr → Lean.MetaM (List ℕ)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.continuousOn : ∀ {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₂) {s : Set E}, ContinuousOn (⇑e) s
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.freeLocus_eq_univ_iff : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.FinitePresentation R M], Module.freeLocus R M = Set.univ ↔ Module.Projective R M
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_insertMany_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m).WF →
    ∀ {l : List (α × β)} {k k' : α},
      (k == k') = true →
        ∀ {v : β},
          List.Pairwise (fun a b => (a.1 == b.1) = false) l →
            (k, v) ∈ l →
              Std.DHashMap.Internal.Raw₀.Const.get! (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)) k' = v
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey?_erase_eq_iff_not_compare_eq_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).maxKey? = t.maxKey? ↔ ∀ {km : α}, t.maxKey? = some km → ¬cmp k km = Ordering.eq
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.Factors.isScalarTower : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : IsDedekindDomain S] (P : ↥(UniqueFactorizationMonoid.factors (Ideal.map (algebraMap R S) p)).toFinset),
  IsScalarTower R (R ⧸ p) (S ⧸ ↑P)
-- Mathlib.CategoryTheory.Monoidal.CommComon_
CategoryTheory.CommComon.id_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommComon C),
  (CategoryTheory.CategoryStruct.id A).hom.hom = CategoryTheory.CategoryStruct.id A.X
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- The number of times an ideal `I` occurs as normalized factor of another ideal `J` is stable
when regarding these ideals as associated elements of the monoid of ideals.  -/
Ideal.count_associates_factors_eq : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {I J : Ideal R},
  I ≠ 0 →
    J.IsPrime →
      J ≠ ⊥ →
        (Associates.mk J).count (Associates.mk I).factors =
          Multiset.count J (UniqueFactorizationMonoid.normalizedFactors I)
-- Mathlib.CategoryTheory.Enriched.Opposite
/-- When composing a tensor product of morphisms with the `V`-composition morphism in `Cᵒᵖ`,
this re-writes the `V`-composition to be in `C` and moves the braiding to the left.  -/
CategoryTheory.tensorHom_eComp_op_eq_assoc : ∀ (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] {x y z : Cᵒᵖ}
  {v w : V} (f : v ⟶ z ⟶[V] y) (g : w ⟶ y ⟶[V] x) {Z : V} (h : (z ⟶[V] x) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V z y x) h) =
    CategoryTheory.CategoryStruct.comp (β_ v w).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g f)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)) h))
-- Mathlib.Algebra.MonoidAlgebra.Division
AddMonoidAlgebra.add_divOf : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] [inst_2 : IsCancelAdd G]
  (x y : AddMonoidAlgebra k G) (g : G), (x + y).divOf g = x.divOf g + y.divOf g
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- Given any distinguished triangle
```
      f       g       h
  X  ───> Y  ───> Z  ───> X⟦1⟧
```
the composition `g ≫ h = 0`.  -/
CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj T.obj₁ ⟶ Z),
      CategoryTheory.CategoryStruct.comp T.mor₂ (CategoryTheory.CategoryStruct.comp T.mor₃ h) =
        CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.ι_eq_algebraMap_iff : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (x : M) (r : R),
  (ExteriorAlgebra.ι R) x = (algebraMap R (ExteriorAlgebra R M)) r ↔ x = 0 ∧ r = 0
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.hasGenEigenvalue_iff : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {k : ℕ}, f.HasGenEigenvalue μ k ↔ (f.genEigenspace μ) ↑k ≠ ⊥
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.coe_comp : ∀ {X Y Z : MonCat} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Order.BoundedOrder.Monotone
monotone_or : ∀ {α : Type u} [inst : Preorder α] {p q : α → Prop}, Monotone p → Monotone q → Monotone fun x => p x ∨ q x
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.presentation.relationsSolutionEquiv_symm_apply_var : ∀ {R : Type u} [inst : CommRing R] {N : Type u_2} [inst_1 : AddCommGroup N] [inst_2 : Module R N] {ι : Type u_4}
  [inst_3 : DecidableEq ι] {M : Type u_5} [inst_4 : AddCommGroup M] [inst_5 : Module R M] (f : M [⋀^ι]→ₗ[R] N)
  (m : (exteriorPower.presentation.relations R ι M).G),
  (exteriorPower.presentation.relationsSolutionEquiv.symm f).var m = f m
-- Mathlib.Algebra.Torsor.Defs
smul_right_cancel_iff : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] {g₁ g₂ : G} (p : P), g₁ • p = g₂ • p ↔ g₁ = g₂
-- Aesop.Rule
Aesop.UnsafeRuleInfo.mk : Aesop.Percent → Aesop.UnsafeRuleInfo
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.toContinuousMapMonoidHom.eq_1 : ∀ (α : Type u) (R : Type u_2) [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : Monoid R]
  [inst_3 : BoundedMul R] [inst_4 : ContinuousMul R],
  BoundedContinuousFunction.toContinuousMapMonoidHom α R =
    { toFun := BoundedContinuousFunction.toContinuousMap, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.MeasureTheory.Integral.ExpDecay
/-- `exp (-b * x)` is integrable on `(a, ∞)`.  -/
exp_neg_integrableOn_Ioi : ∀ (a : ℝ) {b : ℝ}, 0 < b → MeasureTheory.IntegrableOn (fun x => Real.exp (-b * x)) (Set.Ioi a) MeasureTheory.volume
-- Batteries.Tactic.Lint.Frontend
Batteries.Tactic.Lint.instInhabitedLintVerbosity : Inhabited Batteries.Tactic.Lint.LintVerbosity
-- Mathlib.Data.List.Defs
/-- Greedily create a sublist of `l` such that, for every two adjacent elements `a, b ∈ l`,
`R a b` holds. Mostly used with ≠; for example, `destutter (≠) [1, 2, 2, 1, 1] = [1, 2, 1]`,
`destutter (≠) [1, 2, 3, 3] = [1, 2, 3]`, `destutter (<) [1, 2, 5, 2, 3, 4, 9] = [1, 2, 5, 9]`.  -/
List.destutter : {α : Type u_1} → (R : α → α → Prop) → [DecidableRel R] → List α → List α
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.Reachable.dist_triangle_left : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.Reachable u v → ∀ (w : V), G.dist u w ≤ G.dist u v + G.dist v w
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.minD_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.minD fallback ∈ t
-- Mathlib.RingTheory.Finiteness.Basic
Module.Finite.quotient : ∀ (R : Type u_6) {A : Type u_7} {M : Type u_8} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Ring A]
  [inst_3 : Module A M] [inst_4 : Module R M] [inst_5 : SMul R A] [inst_6 : IsScalarTower R A M] [Module.Finite R M]
  (N : Submodule A M), Module.Finite R (M ⧸ N)
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.coe_inv : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [inst_2 : ContinuousInv G],
  ⇑(Homeomorph.inv G) = Inv.inv
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.integralModel_b₂_eq : ∀ (R : Type u_1) [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] (W : WeierstrassCurve K)
  [hW : WeierstrassCurve.IsIntegral R W], (algebraMap R K) (WeierstrassCurve.integralModel R W).b₂ = W.b₂
-- Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
alternatingGroup.stabilizer.surjective_toPerm : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {s : Set α},
  sᶜ.Nontrivial → Function.Surjective MulAction.toPerm
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denote.eq_2 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Power)
  (m : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.Mon.denote ctx (Lean.Grind.CommRing.Mon.mult p m) =
    Lean.Grind.CommRing.Power.denote ctx p * Lean.Grind.CommRing.Mon.denote ctx m
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.homogeneousIdeal_le_vanishingIdeal_zeroLocus : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (I : HomogeneousIdeal 𝒜),
  I ≤ ProjectiveSpectrum.vanishingIdeal (ProjectiveSpectrum.zeroLocus 𝒜 ↑I)
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.inf : ∀ {P P' : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] => Q]
  [AlgebraicGeometry.HasRingHomProperty P' fun {R S} [CommRing R] [CommRing S] => Q'],
  AlgebraicGeometry.HasRingHomProperty (P ⊓ P') fun {R S} [CommRing R] [CommRing S] f => Q f ∧ Q' f
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.IndepFun.comp₀ : ∀ {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {γ : Type u_6} {γ' : Type u_7} {mα : MeasurableSpace α}
  {mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : Ω → β} {g : Ω → β'}
  {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} {mγ : MeasurableSpace γ} {mγ' : MeasurableSpace γ'} {φ : β → γ}
  {ψ : β' → γ'},
  ProbabilityTheory.Kernel.IndepFun f g κ μ →
    AEMeasurable f (μ.bind ⇑κ) →
      AEMeasurable g (μ.bind ⇑κ) →
        AEMeasurable φ (MeasureTheory.Measure.map f (μ.bind ⇑κ)) →
          AEMeasurable ψ (MeasureTheory.Measure.map g (μ.bind ⇑κ)) →
            ProbabilityTheory.Kernel.IndepFun (φ ∘ f) (ψ ∘ g) κ μ
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.LanLift.CommuteWith.isKan.congr_simp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a)
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g] {x : B} (h : x ⟶ c)
  [inst_2 : CategoryTheory.Bicategory.LanLift.CommuteWith f g h],
  CategoryTheory.Bicategory.LanLift.CommuteWith.isKan f g h = CategoryTheory.Bicategory.LanLift.CommuteWith.isKan f g h
-- Init.Omega.Int
Lean.Omega.Fin.ofNat_val_sub : ∀ {n : ℕ} {x y : Fin n}, ↑↑(x - y) = (↑(n - ↑y) + ↑↑x) % ↑n
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_of_isEmpty : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [IsEmpty α] {f : α → G}, ∫ (x : α), f x ∂μ = 0
-- Mathlib.Data.Sym.Basic
Sym.coe_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α}, ↑(Sym.replicate n a) = Multiset.replicate n a
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkFunctor_map_germ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {F G : TopCat.Presheaf C X} (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U) (f : F ⟶ G) {Z : C}
  (h : (TopCat.Presheaf.stalkFunctor C x).obj G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.germ U x hx)
      (CategoryTheory.CategoryStruct.comp ((TopCat.Presheaf.stalkFunctor C x).map f) h) =
    CategoryTheory.CategoryStruct.comp (f.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (G.germ U x hx) h)
-- Init.Data.List.Sublist
List.Sublist.append_left : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → ∀ (l : List α), (l ++ l₁).Sublist (l ++ l₂)
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Pythagorean theorem, vector inner product form.  -/
norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), inner 𝕜 x y = 0 → ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.card_commonNeighbors_le_degree_left : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] (v w : V),
  Fintype.card ↑(G.commonNeighbors v w) ≤ G.degree v
-- Mathlib.SetTheory.Cardinal.Defs
/-- `Cardinal.{u}` is the type of cardinal numbers in `Type u`,
defined as the quotient of `Type u` by existence of an equivalence
(a bijection with explicit inverse).  -/
Cardinal : Type (u + 1)
-- Mathlib.Topology.Algebra.UniformMulAction
UniformContinuousConstVAdd.mk : ∀ {M : Type v} {X : Type x} [inst : UniformSpace X] [inst_1 : VAdd M X],
  (∀ (c : M), UniformContinuous fun x => c +ᵥ x) → UniformContinuousConstVAdd M X
-- Mathlib.Data.Holor
Holor.instAddCommSemigroup : {α : Type} → {ds : List ℕ} → [AddCommSemigroup α] → AddCommSemigroup (Holor α ds)
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.isOpen_support : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) [inst_5 : FiniteDimensional ℝ E], IsOpen (Function.support ↑f)
-- Init.Data.Array.Find
/-- If `¬ p xs[j]` for all `j < i`, then `i ≤ xs.findIdx p`.  -/
Array.le_findIdx_of_not : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α} {i : ℕ} (h : i < xs.size),
  (∀ (j : ℕ) (hji : j < i), p xs[j] = false) → i ≤ Array.findIdx p xs
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.moment_def : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} (X : Ω → ℝ) (p : ℕ) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.moment X p μ = ∫ (x : Ω), (X ^ p) x ∂μ
-- Mathlib.CategoryTheory.CodiscreteCategory
/-- A wrapper for promoting any type to a category,
with a unique morphism between any two objects of the category.  -/
CategoryTheory.Codiscrete.as : {α : Type u} → CategoryTheory.Codiscrete α → α
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.of_vadd_filter : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f : Filter β} {a : α}, (a +ᵥ f).NeBot → f.NeBot
-- Mathlib.Order.Filter.TendstoCofinite
Filter.TendstoCofinite.finite_preimage : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) [Filter.TendstoCofinite f] {s : Set β}, s.Finite → (f ⁻¹' s).Finite
-- Mathlib.CategoryTheory.Limits.Comma
/-- (Implementation). An auxiliary cocone which is useful in order to construct colimits
in the comma category.  -/
CategoryTheory.Comma.colimitAuxiliaryCocone : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    {A : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} A] →
        {B : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} B] →
            {T : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} T] →
                {L : CategoryTheory.Functor A T} →
                  {R : CategoryTheory.Functor B T} →
                    (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) →
                      CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R)) →
                        CategoryTheory.Limits.Cocone ((F.comp (CategoryTheory.Comma.fst L R)).comp L)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorems.addLetDeclToUnfold : Lean.Meta.SimpTheorems → Lean.FVarId → Lean.Meta.SimpTheorems
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- Type-alias for modifications between oplax transformations of oplax functors. This is the type
used for the 2-homomorphisms in the bicategory of oplax functors equipped with oplax
transformations.  -/
CategoryTheory.Oplax.OplaxTrans.Hom : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} → (F ⟶ G) → (F ⟶ G) → Type (max u₁ w₂)
-- Mathlib.Analysis.Normed.Module.Bases
GeneralSchauderBasis.mk : {β : Type u_3} →
  {𝕜 : Type u_4} →
    {X : Type u_5} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup X] →
          [inst_2 : NormedSpace 𝕜 X] →
            {L : SummationFilter β} →
              (basis : β → X) →
                (coord : β → StrongDual 𝕜 X) →
                  (∀ (i j : β), (coord i) (basis j) = Pi.single j 1 i) →
                    (∀ (x : X), HasSum (fun i => (coord i) x • basis i) x L) → GeneralSchauderBasis β 𝕜 X L
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.AbsolutelyContinuous.add : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M]
  [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N] [inst_4 : ContinuousAdd M]
  {v₁ v₂ : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N},
  v₁.AbsolutelyContinuous w → v₂.AbsolutelyContinuous w → (v₁ + v₂).AbsolutelyContinuous w
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.rlp_coproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C),
  (CategoryTheory.MorphismProperty.coproducts.{w, v, u} T).rlp = T.rlp
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instAddZeroClass : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [AddZeroClass Y] → AddZeroClass (LocallyConstant X Y)
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
/-- An ordered additive monoid is `CanonicallyOrderedAdd`
if the ordering coincides with the subtractibility relation,
which is to say, `a ≤ b` iff there exists `c` with `b = a + c`.
This is satisfied by the natural numbers, for example, but not
the integers or other nontrivial ordered groups.

We have `a ≤ b + a` and `a ≤ a + b` as separate fields. In the commutative case the second field
is redundant, but in the noncommutative case (satisfied most relevantly by the ordinals), this
extra field allows us to prove more things without the extra commutativity assumption.  -/
CanonicallyOrderedAdd : (α : Type u_1) → [Add α] → [LE α] → Prop
-- Mathlib.Algebra.Group.Equiv.Opposite
AddEquiv.op_symm_apply_symm_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : Add α] [inst_1 : Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) (a : β),
  (AddEquiv.op.symm f).symm a = (AddOpposite.unop ∘ ⇑f.symm ∘ AddOpposite.op) a
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.sSup_unitClosedBall_eq_norm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : DenselyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F),
  sSup ((fun x => ‖f x‖) '' Metric.closedBall 0 1) = ‖f‖
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
/-- Given any function `m` assigning measures to sets satisfying `m ∅ = 0`, there is
a unique maximal outer measure `μ` satisfying `μ s ≤ m s` for all `s : Set α`.  -/
MeasureTheory.OuterMeasure.ofFunction : {α : Type u_1} → (m : Set α → ENNReal) → m ∅ = 0 → MeasureTheory.OuterMeasure α
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `r` is a positive constant, `fun x ↦ f x * r` tends to infinity along a filter
if and only if `f` tends to infinity along the same filter.  -/
Filter.tendsto_mul_const_atTop_of_pos : ∀ {α : Type u_1} {β : Type u_2} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, 0 < r → (Filter.Tendsto (fun x => f x * r) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.erase_same : ∀ {R : Type u_1} [inst : Semiring R] (p : SkewPolynomial R) (n : ℕ), (SkewPolynomial.erase n p).coeff n = 0
-- Init.Data.Array.Basic
Array.modifyMUnsafe : {α : Type u} → {m : Type u → Type u_1} → [Monad m] → Array α → ℕ → (α → m α) → m (Array α)
-- Mathlib.Algebra.Notation.Support
Function.ext_iff_support : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] {f g : ι → M},
  f = g ↔ Function.support f = Function.support g ∧ ∀ x ∈ Function.support f, f x = g x
-- Mathlib.Analysis.ODE.DiscreteGronwall
/-- Discrete Grönwall inequality, product form: if `u (n+1) ≤ c n * u n + b n` and `0 ≤ c n`
then `u n ≤ u n₀ * ∏ c i + ∑ b k * ∏ c i` over the appropriate ranges.  -/
discrete_gronwall_prod_general : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] {u b c : ℕ → R} {n₀ : ℕ},
  (∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n) →
    (∀ n ≥ n₀, 0 ≤ c n) →
      ∀ ⦃n : ℕ⦄,
        n₀ ≤ n → u n ≤ u n₀ * ∏ i ∈ Finset.Ico n₀ n, c i + ∑ k ∈ Finset.Ico n₀ n, b k * ∏ i ∈ Finset.Ico (k + 1) n, c i
-- Std.Data.HashMap.Lemmas
Std.HashMap.get!_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited β] {k a : α}, (m.erase k).get! a = if (k == a) = true then default else m.get! a
-- Mathlib.Analysis.CStarAlgebra.ContinuousMap
ZeroAtInftyContinuousMap.instNonUnitalCommCStarAlgebra : {α : Type u_1} →
  {A : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : NonUnitalCommCStarAlgebra A] → NonUnitalCommCStarAlgebra (ZeroAtInftyContinuousMap α A)
-- Init.Data.String.Basic
String.data_push : ∀ {s : String} (c : Char), (s.push c).toList = s.toList ++ [c]
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A kernel fork for the kernel of `BinaryBicone.snd`. It consists of the morphism
`BinaryBicone.inl`.  -/
CategoryTheory.Limits.BinaryBicone.sndKernelFork : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} → (c : CategoryTheory.Limits.BinaryBicone X Y) → CategoryTheory.Limits.KernelFork c.snd
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- A bounded variation function has a limit at `-∞`.  -/
BoundedVariationOn.exists_tendsto_atBot : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [CompleteSpace E]
  [hE : Nonempty E] {f : α → E} {s : Set α},
  BoundedVariationOn f s → ∃ l, Filter.Tendsto f (Filter.principal s ⊓ Filter.atBot) (nhds l)