mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.ColimitPresentation.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (diag : CategoryTheory.Functor J C) (ι : diag ⟶ (CategoryTheory.Functor.const J).obj X)
  (isColimit : CategoryTheory.Limits.IsColimit { pt := X, ι := ι }) (diag_1 : CategoryTheory.Functor J C)
  (ι_1 : diag_1 ⟶ (CategoryTheory.Functor.const J).obj X)
  (isColimit_1 : CategoryTheory.Limits.IsColimit { pt := X, ι := ι_1 }),
  ({ diag := diag, ι := ι, isColimit := isColimit } = { diag := diag_1, ι := ι_1, isColimit := isColimit_1 }) =
    (diag = diag_1 ∧ ι ≍ ι_1 ∧ isColimit ≍ isColimit_1)
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (A : CategoryTheory.Mon (CategoryTheory.Functor C D)),
  CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor.obj A =
    CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj A.X
-- Batteries.Control.Lemmas
StateT.run_orElse : ∀ {m : Type u_1 → Type u_2} {α σ : Type u_1} [inst : Monad m] [inst_1 : Alternative m] (x y : StateT σ m α) (s : σ),
  (x <|> y).run s = (x.run s <|> y.run s)
-- Aesop.Tree.AddRapp
Aesop.makeInitialGoal : Aesop.Subgoal →
  Aesop.UnorderedArraySet Lean.MVarId →
    Aesop.MVarClusterRef →
      Lean.Meta.SavedState →
        Aesop.ForwardState →
          Aesop.ForwardRuleMatches →
            Array Aesop.ForwardRuleMatch → ℕ → Aesop.Percent → Aesop.GoalOrigin → Aesop.TreeM Aesop.Goal
-- Mathlib.Order.Basic
Ne.ge_iff_gt : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, a ≠ b → (b ≤ a ↔ b < a)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedSplitSource : Inhabited Lean.Meta.Grind.SplitSource
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Cont'.cons₂.injEq : ∀ (a a_1 : Turing.PartrecToTM2.Cont'), (a.cons₂ = a_1.cons₂) = (a = a_1)
-- Aesop.Util.EqualUpToIds
Aesop.unassignedMVarsEqualUptoIds : Option Lean.MetavarContext →
  Lean.MetavarContext → Lean.MetavarContext → Lean.MVarId → Lean.MVarId → optParam Bool false → Lean.MetaM Bool
-- Mathlib.NumberTheory.LSeries.SumCoeff
LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_and_nonneg : ∀ (f : ℕ → ℝ) {l : ℝ},
  Filter.Tendsto (fun n => (∑ k ∈ Finset.Icc 1 n, f k) / ↑n) Filter.atTop (nhds l) →
    (∀ (n : ℕ), 0 ≤ f n) →
      Filter.Tendsto (fun s => (↑s - 1) * LSeries (fun n => ↑(f n)) ↑s) (nhdsWithin 1 (Set.Ioi 1)) (nhds ↑l)
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.diagram_map_app : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C) {X Y : Jᵒᵖ} (f : X ⟶ Y)
  (X_1 : J),
  ((CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₂).map f).app X_1 =
    CategoryTheory.eHomWhiskerRight V (F₁.map f.unop) (F₂.obj X_1)
-- Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
/-- **Alias** of `MeasureTheory.projectiveFamilyContent_sdiff_of_subset`. -/
MeasureTheory.projectiveFamilyContent_diff_of_subset : ∀ {ι : Type u_1} {α : ι → Type u_2} {mα : (i : ι) → MeasurableSpace (α i)}
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} {s t : Set ((i : ι) → α i)}
  [∀ (J : Finset ι), MeasureTheory.IsFiniteMeasure (P J)] (hP : MeasureTheory.IsProjectiveMeasureFamily P),
  s ∈ MeasureTheory.measurableCylinders α →
    t ∈ MeasureTheory.measurableCylinders α →
      t ⊆ s →
        (MeasureTheory.projectiveFamilyContent hP) (s \ t) =
          (MeasureTheory.projectiveFamilyContent hP) s - (MeasureTheory.projectiveFamilyContent hP) t
-- Mathlib.Topology.Semicontinuity.Defs
lowerHemicontinuousOn_iff_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {s : Set α},
  LowerHemicontinuousOn f s ↔ ∀ x ∈ s, ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ t) → f x ⊆ t
-- Init.Data.Range.Polymorphic.PRange
/-- `*...*` is the range that is unbounded in both directions. See also `Std.Rii`.  -/
Std.«term*...*» : Lean.ParserDescr
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {S : CategoryTheory.ShortComplex C} {K H : C} {i : K ⟶ S.X₂} {π : K ⟶ H}
  {wi : CategoryTheory.CategoryStruct.comp i S.g = 0}
  {hi : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι i wi)}
  {wπ : CategoryTheory.CategoryStruct.comp (hi.lift (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)) π = 0}
  {hπ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π wπ)} {K_1 H_1 : C}
  {i_1 : K_1 ⟶ S.X₂} {π_1 : K_1 ⟶ H_1} {wi_1 : CategoryTheory.CategoryStruct.comp i_1 S.g = 0}
  {hi_1 : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι i_1 wi_1)}
  {wπ_1 : CategoryTheory.CategoryStruct.comp (hi_1.lift (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)) π_1 = 0}
  {hπ_1 : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π_1 wπ_1)},
  { K := K, H := H, i := i, π := π, wi := wi, hi := hi, wπ := wπ, hπ := hπ } =
      { K := K_1, H := H_1, i := i_1, π := π_1, wi := wi_1, hi := hi_1, wπ := wπ_1, hπ := hπ_1 } →
    K = K_1 ∧ H = H_1 ∧ i ≍ i_1 ∧ π ≍ π_1 ∧ hi ≍ hi_1 ∧ hπ ≍ hπ_1
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.precomposeComp.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G H : CategoryTheory.Functor J C} (β : H ⟶ G) (α : G ⟶ F),
  CategoryTheory.Limits.Cocone.precomposeComp β α =
    CategoryTheory.NatIso.ofComponents'
      (fun s =>
        CategoryTheory.Limits.Cocone.extInv
          (CategoryTheory.Iso.refl
            ((CategoryTheory.Limits.Cocone.precompose (CategoryTheory.CategoryStruct.comp β α)).obj s).pt)
          ⋯)
      ⋯
-- Mathlib.Data.Int.Bitwise
/-- `land` takes two integers and returns their bitwise `and`  -/
Int.land : ℤ → ℤ → ℤ
-- Batteries.Data.Array.Pairwise
/-- `Pairwise R as` means that all the elements of the array `as` are `R`-related to all elements with
larger indices.

`Pairwise R #[1, 2, 3] ↔ R 1 2 ∧ R 1 3 ∧ R 2 3`

For example `as.Pairwise (· ≠ ·)` asserts that `as` has no duplicates, `as.Pairwise (· < ·)` asserts
that `as` is strictly sorted and `as.Pairwise (· ≤ ·)` asserts that `as` is weakly sorted.
 -/
Array.Pairwise : {α : Type u_1} → (α → α → Prop) → Array α → Prop
-- Init.WFExtrinsicFix
_private.Init.WFExtrinsicFix.0.WellFounded.extrinsicFix.eq_1 : ∀ {α : Sort u_1} {C : α → Sort u_2} [inst : ∀ (a : α), Nonempty (C a)] (R : α → α → Prop)
  (F : (a : α) → ((a' : α) → R a' a → C a') → C a) (a : α),
  WellFounded.extrinsicFix R F a = if h : WellFounded R then h.fix F a else WellFounded.opaqueFix✝ R F a
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.induction_of_closure_eq_top_left : ∀ {M : Type u_1} [inst : AddMonoid M] {s : Set M} {motive : M → Prop},
  AddSubmonoid.closure s = ⊤ → ∀ (x : M), motive 0 → (∀ x ∈ s, ∀ (y : M), motive y → motive (x + y)) → motive x
-- Mathlib.LinearAlgebra.Matrix.Swap
/-- `Matrix.swap` as an element of `GL n R`.  -/
Matrix.GeneralLinearGroup.swap : (R : Type u_1) → {n : Type u_2} → [inst : CommRing R] → [inst_1 : DecidableEq n] → [inst_2 : Fintype n] → n → n → GL n R
-- Mathlib.Topology.Sheaves.Stalks
/-- Let `F` be a sheaf valued in a concrete category, whose forgetful functor reflects isomorphisms,
preserves limits and filtered colimits. Then two sections who agree on every stalk must be equal.
 -/
TopCat.Presheaf.section_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type v} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [instCC : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms]
  (F : TopCat.Sheaf C X) (U : TopologicalSpace.Opens ↑X) (s t : CategoryTheory.ToType (F.obj.obj (Opposite.op U))),
  (∀ (x : ↑X) (hx : x ∈ U),
      (CategoryTheory.ConcreteCategory.hom (F.presheaf.germ U x hx)) s =
        (CategoryTheory.ConcreteCategory.hom (F.presheaf.germ U x hx)) t) →
    s = t
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt16.reduceGT : Lean.Meta.Simp.Simproc
-- Mathlib.Data.ENNReal.Basic
ENNReal.toReal_le_coe_of_le_coe : ∀ {a : ENNReal} {b : NNReal}, a ≤ ↑b → a.toReal ≤ ↑b
-- Mathlib.Algebra.Group.Basic
add_right_iterate : ∀ {M : Type u_4} [inst : AddMonoid M] (a : M) (n : ℕ), (fun x => x + a)^[n] = fun x => x + n • a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_union!_of_contains_eq_false_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k m₂ = false →
          Std.DTreeMap.Internal.Impl.Const.get? (m₁.union! m₂) k = Std.DTreeMap.Internal.Impl.Const.get? m₁ k
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.instIsLeftCancelMulZeroOfIsCancelAdd : ∀ {R : Type u} [inst : Semiring R] [IsCancelAdd R] [IsLeftCancelMulZero R], IsLeftCancelMulZero (Polynomial R)
-- Mathlib.Combinatorics.SetFamily.Shadow
Finset.sized_shadow_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {r : ℕ},
  ∅ ∉ 𝒜 → (Set.Sized r ↑𝒜.shadow ↔ Set.Sized (r + 1) ↑𝒜)
-- Mathlib.Algebra.DirectSum.Internal
SetLike.algebraMap_mem_graded : ∀ {ι : Type u_1} {S : Type u_3} {R : Type u_4} [inst : Zero ι] [inst_1 : CommSemiring S] [inst_2 : Semiring R]
  [inst_3 : Algebra S R] (A : ι → Submodule S R) [SetLike.GradedOne A] (s : S), (algebraMap S R) s ∈ A 0
-- Mathlib.Computability.Language
/-- A language is a set of strings over an alphabet.  -/
Language : Type u_4 → Type u_4
-- Mathlib.Algebra.Ring.Defs
neg_mul_neg : ∀ {α : Type u} [inst : Mul α] [inst_1 : HasDistribNeg α] (a b : α), -a * -b = a * b
-- Mathlib.Control.Functor.Multivariate
TypeVec.RelLast.eq_2 : ∀ {n : ℕ} (α : TypeVec.{u} n) {β γ : Type u} (r : β → γ → Prop), α.RelLast r = r
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.Context.paramDecls : Lean.Elab.Term.CollectPatternVars.Context → Array (Lean.Name × Lean.BinderInfo)
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.intNorm_mem_spanNorm : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] {I : Ideal S} {x : S}, x ∈ I → (Algebra.intNorm R S) x ∈ Ideal.spanNorm R I
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_zero : ENNReal.log 0 = ⊥
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.range_π : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (solution : relations.Solution M), solution.π.range = Submodule.span A (Set.range solution.var)
-- Mathlib.RingTheory.MvPowerSeries.Equiv
PowerSeries.toMvPowerSeries_coeff_eq_zero : ∀ {σ : Type u_2} {R : Type u_4} [inst : CommRing R] {f : PowerSeries R} {i : σ} {d : σ →₀ ℕ},
  d i = 0 → PowerSeries.constantCoeff f = 0 → (MvPowerSeries.coeff d) ((PowerSeries.toMvPowerSeries i) f) = 0
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.coe_toMulEquiv : ∀ {A : Type u_2} {B : Type u_3} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Star A] [inst_3 : Star B] (f : A ≃⋆* B),
  ⇑f.toMulEquiv = ⇑f
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.List.forIn'_cons.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.done b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_1 b
-- Lean.DocString.DeferredCheck
/-- The index of this reference into the deferred checks of its docstring, in source order.  -/
Lean.Doc.DeferredCheck.index : Lean.Doc.DeferredCheck → ℕ
-- Mathlib.NumberTheory.LSeries.Convolution
LSeriesHasSum.eq_1 : ∀ (f : ℕ → ℂ) (s a : ℂ), LSeriesHasSum f s a = HasSum (LSeries.term f s) a
-- Init.ShareCommon
ShareCommon.StateFactoryImpl.mk.sizeOf_spec : ∀ (Map Set : Type) (mkState : Unit → Map × Set) (mapFind? : Map → ShareCommon.Object → Option ShareCommon.Object)
  (mapInsert : Map → ShareCommon.Object → ShareCommon.Object → Map)
  (setFind? : Set → ShareCommon.Object → Option ShareCommon.Object) (setInsert : Set → ShareCommon.Object → Set),
  sizeOf
      { Map := Map, Set := Set, mkState := mkState, mapFind? := mapFind?, mapInsert := mapInsert, setFind? := setFind?,
        setInsert := setInsert } =
    1 + sizeOf Map + sizeOf Set + sizeOf mkState
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
IsSimplyConnected.nonempty : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsSimplyConnected s → s.Nonempty
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (state : Std.Mutex (Std.Bounded.State✝ α)), sizeOf { state := state } = 1 + sizeOf state
-- Lean.Hygiene
Lean.Unhygienic.Context.ref : Lean.Unhygienic.Context → Lean.Syntax
-- Init.Data.UInt.Lemmas
UInt8.left_eq_add : ∀ {a b : UInt8}, a = a + b ↔ b = 0
-- Mathlib.Data.Int.Order.Basic
Int.mul_neg_iff : ∀ {a b : ℤ}, a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
-- Init.Data.List.Zip
List.unzip_zip_left : ∀ {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β}, l₁.length ≤ l₂.length → (l₁.zip l₂).unzip.1 = l₁
-- Mathlib.Topology.UniformSpace.Ascoli
/-- Let `X` be a topological space, `𝔖` a family of compact subsets of `X` and
`α` a uniform space. An equicontinuous subset of `X → α` is closed in the topology of uniform
convergence on all `K ∈ 𝔖` iff it is closed in the topology of pointwise convergence on `⋃₀ 𝔖`.  -/
EquicontinuousOn.isClosed_range_pi_of_uniformOnFun' : ∀ {ι : Type u_1} {X : Type u_2} {α : Type u_3} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α}
  {𝔖 : Set (Set X)},
  (∀ K ∈ 𝔖, IsCompact K) →
    (∀ K ∈ 𝔖, EquicontinuousOn F K) →
      IsClosed (Set.range (⇑(UniformOnFun.ofFun 𝔖) ∘ F)) → IsClosed (Set.range ((⋃₀ 𝔖).domRestrict ∘ F))
-- Init.Data.Iterators.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Consumers.Monadic.Loop.0.Std.IterM.DefaultConsumers.forIn'.match_1.eq_2 : ∀ {β : Type u_3} (γ : Type u_1) (PlausibleForInStep : β → γ → ForInStep γ → Prop) (acc : γ) (out : β)
  (motive : Subtype (PlausibleForInStep out acc) → Sort u_2) (c : γ) (h : PlausibleForInStep out acc (ForInStep.done c))
  (h_1 : (c : γ) → (h' : PlausibleForInStep out acc (ForInStep.yield c)) → motive ⟨ForInStep.yield c, h'⟩)
  (h_2 : (c : γ) → (h : PlausibleForInStep out acc (ForInStep.done c)) → motive ⟨ForInStep.done c, h⟩),
  (match ⟨ForInStep.done c, h⟩ with
    | ⟨ForInStep.yield c, h'⟩ => h_1 c h'
    | ⟨ForInStep.done c, h⟩ => h_2 c h) =
    h_2 c h
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.left_inv_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  (X : C) [self : CategoryTheory.GrpObj X] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.GrpObj.inv (CategoryTheory.CategoryStruct.id X))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h)
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.instFullProdCurry₃ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E], CategoryTheory.Functor.curry₃.Full
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.factors_right_of_factors_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {P : CategoryTheory.Subobject Y} (f g : X ⟶ Y), P.Factors (f + g) → P.Factors f → P.Factors g
-- Mathlib.CategoryTheory.Limits.Filtered
/-- `C` is filtered if and only if for every functor `F : J ⥤ C` from a finite category there is
some `X : C` such that `lim Hom(F·, X)` is nonempty.

Lemma 3.1.2 of [Kashiwara2006]  -/
CategoryTheory.IsFiltered.iff_nonempty_limit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.IsFiltered C ↔
    ∀ {J : Type v} [inst_1 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J]
      (F : CategoryTheory.Functor J C),
      ∃ X, Nonempty (CategoryTheory.Limits.limit (F.op.comp (CategoryTheory.yoneda.obj X)))
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toArray_roc_eq_fallback : ∀ {m n i fallback : ℕ}, n ≤ i + m → (m<...=n).toArray.getD i fallback = fallback
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {l : List α} {k : α}, (Std.HashMap.unitOfList l)[k]! = ()
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.coe_subtype : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R), ⇑s.subtype = Subtype.val
-- Mathlib.Probability.ProbabilityMassFunction.Basic
/-- The support of a `PMF` is the set where it is nonzero.  -/
PMF.support : {α : Type u_1} → PMF α → Set α
-- Mathlib.Data.Finsupp.PointwiseSMul
/-- **Alias** of `Finset.mem_vaddAntidiagonal`. -/
Finsupp.mem_vaddAntidiagonal_iff : ∀ {G : Type u_1} {P : Type u_2} [inst : VAdd G P] {s : Set G} {t : Set P} (a : P) (h : (s.vaddAntidiagonal t a).Finite)
  {x : G × P}, x ∈ Finset.VAddAntidiagonal a h ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 +ᵥ x.2 = a
-- Mathlib.NumberTheory.Ostrowski
Rat.AbsoluteValue.padic.congr_simp : ∀ (p p_1 : ℕ) (e_p : p = p_1) [inst : Fact (Nat.Prime p)], Rat.AbsoluteValue.padic p = Rat.AbsoluteValue.padic p_1
-- Lean.Setup
Lean.ModuleArtifacts.mk : Option System.FilePath →
  Option System.FilePath →
    Option System.FilePath →
      Option System.FilePath →
        Option System.FilePath →
          Option System.FilePath →
            Option System.FilePath → Option System.FilePath → Option System.FilePath → Lean.ModuleArtifacts
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Multipliable.comp_nat_add : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M] {f : ℕ → M} {k : ℕ},
  (Multipliable fun n => f (n + k)) → Multipliable f
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.sub_mem_Ioo_zero_iff_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b : α},
  b - a ∈ Set.Ioo 0 b ↔ a ∈ Set.Ioo 0 b
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toList_rcc_eq_zero_iff : ∀ {m n : ℤ} {i : ℕ}, (m...=n).toList[i]! = 0 ↔ (n + 1 - m).toNat ≤ i ∨ m + ↑i = 0
-- Mathlib.Order.Minimal
Maximal.not_ssuperset : ∀ {α : Type u_2} {P : Set α → Prop} {s t : Set α}, Maximal P s → P t → ¬s ⊂ t
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.inv_Ioi₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀]
  {a : G₀}, 0 < a → (Set.Ioi a)⁻¹ = Set.Ioo 0 a⁻¹
-- Std.Time.Format.Modifier
Std.Time.instInhabitedYear : Inhabited Std.Time.Year
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.mapDomainBialgHom_add : ∀ {R : Type u_1} {M : Type u_8} {N : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] (f g : M →+ N),
  AddMonoidAlgebra.mapDomainBialgHom R (f + g) =
    (WithConv.toConv (AddMonoidAlgebra.mapDomainBialgHom R f) *
        WithConv.toConv (AddMonoidAlgebra.mapDomainBialgHom R g)).ofConv
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.coe_injective : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L],
  Function.Injective SetLike.coe
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.Fix.dest.eq_1 : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n},
  MvQPF.Fix.dest = MvQPF.Fix.rec (MvFunctor.map (TypeVec.id ::: MvQPF.Fix.mk))
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.IsMinor.trans : ∀ {α : Type u_1} {M₁ M₂ M₃ : Matroid α}, M₁ ≤m M₂ → M₂ ≤m M₃ → M₁ ≤m M₃
-- Mathlib.Data.Finset.Sups
Finset.card_sups_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] (s t : Finset α),
  (s ⊻ t).card = s.card * t.card ↔ Set.InjOn (fun x => x.1 ⊔ x.2) (↑s ×ˢ ↑t)
-- Lean.Meta.Tactic.Util
Lean.Meta.ensureAtMostOne : List Lean.MVarId →
  optParam Lean.MessageData ((Lean.MessageData.ofFormat ∘ Std.format) "unexpected number of goals") →
    Lean.MetaM (Option Lean.MVarId)
-- Mathlib.Algebra.Notation.Prod
Prod.vadd_def : ∀ {E : Type u_8} {α : Type u_9} {β : Type u_10} [inst : VAdd E α] [inst_1 : VAdd E β] (c : E) (p : α × β),
  c +ᵥ p = (c +ᵥ p.1, c +ᵥ p.2)
-- Mathlib.Topology.Compactness.LocallyCompact
IsOpenQuotientMap.weaklyLocallyCompactSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [WeaklyLocallyCompactSpace X]
  {f : X → Y}, IsOpenQuotientMap f → WeaklyLocallyCompactSpace Y
-- Mathlib.Analysis.ODE.Transform
/-- If the vector field `v` vanishes at `x₀` for all times, then the constant curve at `x₀`
is a global integral curve of `v`.  -/
isIntegralCurve_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {x : E},
  (∀ (t : ℝ), v t x = 0) → IsIntegralCurve (fun x_1 => x) v
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
polarCoord_target : polarCoord.target = Set.Ioi 0 ×ˢ Set.Ioo (-Real.pi) Real.pi
-- Mathlib.Topology.Order.LawsonTopology
/-- The complements of the upper closures of finite sets intersected with Scott open sets form
a basis for the lawson topology.  -/
Topology.IsLawson.lawsonBasis : (α : Type u_1) → [Preorder α] → Set (Set α)
-- Mathlib.MeasureTheory.Function.LpSpace.Complete
_private.Mathlib.MeasureTheory.Function.LpSpace.Complete.0.MeasureTheory.Lp.lintegral_rpow_sum_enorm_sub_le_rpow_tsum : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_3} [inst : NormedAddCommGroup E]
  {f : ℕ → α → E} {p : ℝ},
  1 ≤ p →
    ∀ {B : ℕ → ENNReal} (n : ℕ),
      MeasureTheory.eLpNorm' (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i →
        ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
-- Lean.Meta.Transform
/-- Unfolds theorems that are applied to `f x₁ .. xₙ` where `f` is in `fnNames` and
`n ≤ numSectionVars` (i.e., an unsaturated application of `f`).

This is used to undo proof abstraction for termination checking, as otherwise the bare
occurrence of the recursive function prevents termination checking from succeeding.

Usually, the argument is just `f` (the constant), arising from `mkAuxTheorem` abstracting over the
aux decl representing `f`. If the mutual function is defined within the scope of `variable` commands,
it is `f x y` where `x y` are the variables in scope, so we use the `numSectionVars` to recognize that
while avoiding to unfold theorems applied to saturated applications of `f`.

This unfolds from the private environment. The resulting definitions are (usually) not
exposed anyways.
 -/
Lean.Meta.unfoldIfArgIsAppOf : Array Lean.Name → ℕ → Lean.Expr → Lean.CoreM Lean.Expr
-- Init.Data.BitVec.Lemmas
BitVec.toInt_concat : ∀ {w : ℕ} (x : BitVec w) (b : Bool), (x.concat b).toInt = if w = 0 then -b.toInt else x.toInt * 2 + b.toInt