mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
/-- `HasSum f a L` means that the (potentially infinite) sum of the `f b` for `b : β`
converges to `a` along the SummationFilter `L`.

By default `L` is the `unconditional` one, corresponding to the limit of all finite sets towards
the entire type. So we take the sum over bigger and bigger finite sets. This sum operation is
invariant under permuting the terms (while sums for more general summation filters usually are not).
This is based on Mario Carneiro's
[infinite sum `df-tsms` in Metamath](http://us.metamath.org/mpeuni/df-tsms.html).

In particular, the function `ℕ → ℝ` sending `n` to `(-1) ^ n / (n + 1)` does not have a
sum for this definition, although it is summable for the `conditional` summation filter that
takes limits of sums over `n ∈ {0, ..., X}` as `X → ∞`. However, a series which is *absolutely*
convergent with respect to the conditional summation filter is in fact unconditionally summable.

For the definition and many statements, `α` does not need to be a topological additive monoid,
only an additive monoid with a topology (i.e. the addition is not assumed to be continuous). We
only add this assumption later, for the lemmas where it is relevant.  -/
HasSum : {α : Type u_1} →
  {β : Type u_2} →
    [AddCommMonoid α] →
      [TopologicalSpace α] → (β → α) → α → optParam (SummationFilter β) (SummationFilter.unconditional β) → Prop
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coe_add : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Add β]
  [inst_3 : ContinuousAdd β] (f g : C(α, β)), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.IsReduced.nil : ∀ {α : Type u}, FreeAddGroup.IsReduced []
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.contains_insertMany_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k : α},
  Std.DTreeMap.Internal.Impl.contains k ↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯) =
    (Std.DTreeMap.Internal.Impl.contains k t || (List.map Prod.fst l).contains k)
-- Std.Tactic.BVDecide.LRAT.Internal.LRATChecker
Std.Tactic.BVDecide.LRAT.Internal.Result.outOfProof : Std.Tactic.BVDecide.LRAT.Internal.Result
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- **Alias** of `Set.mem_finsetSum`.

---

The n-ary version of `Set.mem_add`.  -/
Set.mem_finset_sum : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] (t : Finset ι) (f : ι → Set α) (a : α),
  a ∈ ∑ i ∈ t, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ t → g i ∈ f i), ∑ i ∈ t, g i = a
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.prehaar_sup_eq : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G]
  {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G} {K₁ K₂ : TopologicalSpace.Compacts G},
  (interior U).Nonempty →
    Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹) →
      MeasureTheory.Measure.haar.prehaar (↑K₀) U (K₁ ⊔ K₂) =
        MeasureTheory.Measure.haar.prehaar (↑K₀) U K₁ + MeasureTheory.Measure.haar.prehaar (↑K₀) U K₂
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.mk.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] (a : M) (h : a ≠ 0),
  FiniteArchimedeanClass.mk a h = ⟨ArchimedeanClass.mk a, ⋯⟩
-- Mathlib.Algebra.Group.Finsupp
Finsupp.add_apply : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] (g₁ g₂ : ι →₀ M) (a : ι), (g₁ + g₂) a = g₁ a + g₂ a
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Polynomial.cyclotomic_three : ∀ (R : Type u_1) [inst : Ring R], Polynomial.cyclotomic 3 R = Polynomial.X ^ 2 + Polynomial.X + 1
-- Mathlib.Probability.Moments.SubGaussian
/-- **Hoeffding inequality** for sub-Gaussian random variables.  -/
ProbabilityTheory.HasSubgaussianMGF.measure_sum_ge_le_of_iIndepFun : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ},
  ProbabilityTheory.iIndepFun X μ →
    ∀ {c : ι → NNReal} {s : Finset ι},
      (∀ i ∈ s, ProbabilityTheory.HasSubgaussianMGF (X i) (c i) μ) →
        ∀ {ε : ℝ}, 0 ≤ ε → μ.real {ω | ε ≤ ∑ i ∈ s, X i ω} ≤ Real.exp (-ε ^ 2 / (2 * ↑(∑ i ∈ s, c i)))
-- Std.Http.Protocol.H1.Parser
/-- Parses a line terminator.
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.crlf : Std.Internal.Parsec.ByteArray.Parser Unit
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
AlgebraicGeometry.Scheme.zariskiTopology_le_fpqcTopology : AlgebraicGeometry.Scheme.zariskiTopology ≤ AlgebraicGeometry.Scheme.fpqcTopology
-- Mathlib.Data.Nat.Cast.Order.Field
Nat.one_div_le_one_div : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {n m : ℕ},
  n ≤ m → 1 / (↑m + 1) ≤ 1 / (↑n + 1)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- the first component of `f : Hom x y` is a morphism `x.fst ⟶ y.fst`  -/
CategoryTheory.Limits.CategoricalPullback.Hom.fst : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                {x y : CategoryTheory.Limits.CategoricalPullback F G} → x.Hom y → (x.fst ⟶ y.fst)
-- Mathlib.Algebra.Polynomial.Basic
/-- **Alias** of `Polynomial.coeff_C_of_ne_zero`. -/
Polynomial.coeff_C_ne_zero : ∀ {R : Type u} {a : R} {n : ℕ} [inst : Semiring R], n ≠ 0 → (Polynomial.C a).coeff n = 0
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.instDecidableOfExistsUnitsEqVal.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] (x : M) [h : Decidable (∃ u, ↑u = x)], IsUnit.instDecidableOfExistsUnitsEqVal x = h
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Cotrident.ofπ_pt : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [inst_1 : Nonempty J]
  {P : C} (π : Y ⟶ P)
  (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) π = CategoryTheory.CategoryStruct.comp (f j₂) π),
  (CategoryTheory.Limits.Cotrident.ofπ π w).pt = P
-- Mathlib.Tactic.Widget.LibraryRewrite
Mathlib.Tactic.LibraryRewrite.instInhabitedRewriteLemma.default : Mathlib.Tactic.LibraryRewrite.RewriteLemma
-- Mathlib.Topology.Order
continuous_iSup_rng : ∀ {α : Type u} {β : Type v} {f : α → β} {ι : Sort u_2} {t₁ : TopologicalSpace α} {t₂ : ι → TopologicalSpace β} {i : ι},
  Continuous f → Continuous f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey!_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α} {v : β}, (t.insert k v).minKey! = t.minKey?.elim k fun k' => if (cmp k k').isLE = true then k else k'
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousWithinAt_biInf : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {ι : Sort u_4} {δ : Type u_5}
  [inst_1 : CompleteLinearOrder δ] {p : ι → Prop} {f : (i : ι) → p i → α → δ},
  (∀ (i : ι) (hi : p i), UpperSemicontinuousWithinAt (f i hi) s x) →
    UpperSemicontinuousWithinAt (fun x' => ⨅ i, ⨅ (hi : p i), f i hi x') s x
-- Mathlib.LinearAlgebra.Basis.VectorSpace
/-- If `V` and `V'` are nontrivial vector spaces over a field `K`, the space of `K`-linear maps
between them is nontrivial.  -/
instNontrivialLinearMapId : ∀ {K : Type u_3} {V : Type u_4} {V' : Type u_5} [inst : DivisionRing K] [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup V'] [inst_3 : Module K V] [inst_4 : Module K V'] [Nontrivial V] [Nontrivial V'],
  Nontrivial (V →ₗ[K] V')
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.isOpen_resolventSet : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] (a : A), IsOpen (resolventSet 𝕜 a)
-- Mathlib.CategoryTheory.Limits.FinallySmall
/-- Constructor for `FinallySmall C` from an explicit small category witness.  -/
CategoryTheory.FinallySmall.mk' : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {S : Type w} [inst_1 : CategoryTheory.SmallCategory S]
  (F : CategoryTheory.Functor S J) [F.Final], CategoryTheory.FinallySmall J
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.tr_respects_aux : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ)
  {q : Turing.TM2.Stmt Γ Λ σ} {v : σ} {T : Turing.ListBlank ((i : K) → Option (Γ i))} {k : K}
  {S : (k : K) → List (Γ k)},
  (∀ (k : K), Turing.ListBlank.map (Turing.proj k) T = Turing.ListBlank.mk (List.map some (S k)).reverse) →
    ∀ (o : Turing.TM2to1.StAct K Γ σ k),
      (∀ {v : σ} {S : (k : K) → List (Γ k)} {T : Turing.ListBlank ((k : K) → Option (Γ k))},
          (∀ (k : K), Turing.ListBlank.map (Turing.proj k) T = Turing.ListBlank.mk (List.map some (S k)).reverse) →
            ∃ b,
              Turing.TM2to1.TrCfg (Turing.TM2.stepAux q v S) b ∧
                StateTransition.Reaches (Turing.TM1.step (Turing.TM2to1.tr M))
                  (Turing.TM1.stepAux (Turing.TM2to1.trNormal q) v (Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom T))) b) →
        ∃ b,
          Turing.TM2to1.TrCfg (Turing.TM2.stepAux (Turing.TM2to1.stRun o q) v S) b ∧
            StateTransition.Reaches (Turing.TM1.step (Turing.TM2to1.tr M))
              (Turing.TM1.stepAux (Turing.TM2to1.trNormal (Turing.TM2to1.stRun o q)) v
                (Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom T)))
              b
-- Mathlib.Analysis.Calculus.FDeriv.Defs
/-- **Alias** of the forward direction of `hasFDerivAt_iff_isLittleO`. -/
HasFDerivAt.isLittleO : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E}, HasFDerivAt f f' x → (fun x' => f x' - f x - f' (x' - x)) =o[nhds x] fun x' => x' - x
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.mk.injEq : ∀ {P : TopCat → Prop} (toTop : TopCat) [is_compact : CompactSpace ↑toTop] [is_hausdorff : T2Space ↑toTop]
  (prop : P toTop) (toTop_1 : TopCat) (is_compact_1 : CompactSpace ↑toTop_1) (is_hausdorff_1 : T2Space ↑toTop_1)
  (prop_1 : P toTop_1),
  ({ toTop := toTop, is_compact := is_compact, is_hausdorff := is_hausdorff, prop := prop } =
      { toTop := toTop_1, is_compact := is_compact_1, is_hausdorff := is_hausdorff_1, prop := prop_1 }) =
    (toTop = toTop_1)
-- Mathlib.GroupTheory.NoncommCoprod
AddMonoidHom.noncommCoprod_inl_inr : ∀ {M : Type u_4} {N : Type u_5} [inst : AddMonoid M] [inst_1 : AddMonoid N],
  (AddMonoidHom.inl M N).noncommCoprod (AddMonoidHom.inr M N) ⋯ = AddMonoidHom.id (M × N)
-- Mathlib.Data.FinEnum
/-- No non-empty enumeration has 0 elements.  -/
FinEnum.card_ne_zero : ∀ {α : Type u_1} [inst : FinEnum α] [Nonempty α], FinEnum.card α ≠ 0
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.inv_eq_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G : C}
  [inst_2 : CategoryTheory.GrpObj G], CategoryTheory.GrpObj.inv = (CategoryTheory.CategoryStruct.id G)⁻¹
-- Init.Data.Option.Lemmas
Option.get_inj : ∀ {α : Type u_1} {o1 o2 : Option α} {h1 : o1.isSome = true} {h2 : o2.isSome = true}, o1.get h1 = o2.get h2 ↔ o1 = o2
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
/-- The coproduct of all the morphisms `f` indexed by all diagrams
consisting of a morphism `f : X ⟶ Y` satisfying `W` and of a morphism `d : X ⟶ Z`.  -/
CategoryTheory.OrthogonalReflection.D₁.t : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (Z : C) →
        [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] →
          [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] →
            ∐ CategoryTheory.OrthogonalReflection.D₁.obj₁ ⟶ ∐ CategoryTheory.OrthogonalReflection.D₁.obj₂
-- Mathlib.Data.Multiset.Sum
Multiset.card_disjSum : ∀ {α : Type u_1} {β : Type u_2} (s : Multiset α) (t : Multiset β), (s.disjSum t).card = s.card + t.card
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Embedding.preimage_neighborSet : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (v : V) (f : G ↪g G'),
  ⇑f ⁻¹' G'.neighborSet (f v) = G.neighborSet v
-- Mathlib.Data.Finsupp.MonomialOrder
/-- Monomial orders : equivalence of `σ →₀ ℕ` with a well-ordered type  -/
MonomialOrder : Type u_1 → Type (max u_1 (u_2 + 1))
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_const_add : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (α : ℝ),
  ProbabilityTheory.mgf (fun ω => α + X ω) μ t = Real.exp (t * α) * ProbabilityTheory.mgf X μ t
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
/-- The bottom map in a valuative commutative map.  -/
AlgebraicGeometry.ValuativeCommSq.i₂ : {X Y : AlgebraicGeometry.Scheme} →
  {f : X ⟶ Y} → (self : AlgebraicGeometry.ValuativeCommSq f) → AlgebraicGeometry.Spec (CommRingCat.of self.R) ⟶ Y
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.rename.eq_1 : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : σ → τ),
  MvPolynomial.rename f = AddMonoidAlgebra.mapDomainAlgHom R R (Finsupp.mapDomain.addMonoidHom f)
-- Mathlib.Order.WithBot
WithBot.ofDual_lt_iff : ∀ {α : Type u_1} [inst : LT α] {x : WithBot αᵒᵈ} {y : WithTop α}, WithBot.ofDual x < y ↔ WithTop.toDual y < x
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- "Precomposition" of `F : ComposableArrows C n` by a morphism `f : X ⟶ F.left`.  -/
CategoryTheory.ComposableArrows.precomp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {n : ℕ} →
      (F : CategoryTheory.ComposableArrows C n) → {X : C} → (X ⟶ F.left) → CategoryTheory.ComposableArrows C (n + 1)
-- Init.Data.List.OfFn
List.idRun_ofFnM : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → Id α}, (List.ofFnM f).run = List.ofFn fun i => (f i).run
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.WF.brecOn : ∀ {α : Type u_1} {cmp : α → α → Ordering} {motive : (a : RBTree.RBNode α) → RBTree.RBNode.WF cmp a → Prop}
  {a : RBTree.RBNode α} (t : RBTree.RBNode.WF cmp a),
  (∀ (a : RBTree.RBNode α) (t : RBTree.RBNode.WF cmp a), RBTree.RBNode.WF.below t → motive a t) → motive a t
-- Std.Data.HashSet.Basic
Std.HashSet.mk.injEq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (inner inner_1 : Std.HashMap α Unit),
  ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (KaehlerDifferential.derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ
      Finsupp.linearCombination S ⇑(KaehlerDifferential.D R S) =
    (KaehlerDifferential.kerTotal R S).mkQ
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- We construct the pullback along an open immersion via restricting along the pullback of the
maps of underlying spaces (which is also an open embedding).
 -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : AlgebraicGeometry.PresheafedSpace C} →
      (f : X ⟶ Z) →
        [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] →
          (g : Y ⟶ Z) → CategoryTheory.Limits.PullbackCone f g
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.hasForgetToAddMagmaCat : CategoryTheory.HasForget₂ AddSemigrp AddMagmaCat
-- Batteries.Data.NameSet
Lean.NameSet.instSingletonName_batteries : Singleton Lean.Name Lean.NameSet
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.associator_obj_inl_inl : ∀ (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] (X : C),
  (CategoryTheory.sum.associator C D E).obj (Sum.inl (Sum.inl X)) = Sum.inl X
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.uliftFunctor_obj_coe : ∀ (X : AddMonCat), ↑(AddMonCat.uliftFunctor.obj X) = ULift.{u, v} ↑X
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.smul_bot : ∀ {α : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : Monoid α] [inst_2 : MulDistribMulAction α M] (a : α),
  a • ⊥ = ⊥
-- Mathlib.Algebra.Order.Group.Basic
zsmul_lt_zsmul_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {n : ℤ} {a b : α},
  0 < n → a < b → n • a < n • b
-- Mathlib.CategoryTheory.Filtered.Basic
/-- Given a "crown" of morphisms
```
  j₁   j₂   j₃
 /  \  /\  /  \
|    \/  \/    |
|    /\  /\    |
|   |  \/  |   |
 \  |  /\  |  /
  \ | /  \ | /
   vvv    vvv
    k₁    k₂
```
in a filtered category, we can construct an object `s` and two morphisms from `k₁` and `k₂` to `s`,
making the resulting squares commute.
 -/
CategoryTheory.IsFiltered.crown₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j₁ j₂ j₃ k₁ k₂ : C}
  (f₁ : j₁ ⟶ k₁) (g₁ : j₁ ⟶ k₂) (f₂ : j₂ ⟶ k₁) (g₂ : j₂ ⟶ k₂) (f₃ : j₃ ⟶ k₁) (g₃ : j₃ ⟶ k₂),
  ∃ s α β,
    CategoryTheory.CategoryStruct.comp f₁ α = CategoryTheory.CategoryStruct.comp g₁ β ∧
      CategoryTheory.CategoryStruct.comp f₂ α = CategoryTheory.CategoryStruct.comp g₂ β ∧
        CategoryTheory.CategoryStruct.comp f₃ α = CategoryTheory.CategoryStruct.comp g₃ β
-- Mathlib.Data.Finset.Sups
Finset.Nonempty.of_infs_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {s t : Finset α}, (s ⊼ t).Nonempty → s.Nonempty
-- Mathlib.RingTheory.FractionalIdeal.Basic
_private.Mathlib.RingTheory.FractionalIdeal.Basic.0.Nat.unaryCast.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
/-- A presheaf of sets on a category which is `FinitaryExtensive` is a sheaf iff it preserves finite
products.
 -/
CategoryTheory.Presieve.isSheaf_iff_preservesFiniteProducts : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.FinitaryPreExtensive C]
  [CategoryTheory.FinitaryExtensive C] (F : CategoryTheory.Functor Cᵒᵖ (Type w)),
  CategoryTheory.Presieve.IsSheaf (CategoryTheory.extensiveTopology C) F ↔
    CategoryTheory.Limits.PreservesFiniteProducts F
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.instRepr : {α : Type u} → [Repr α] → Repr (Std.HashSet.Raw α)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.closedCell_nonempty : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (j : Topology.RelCWComplex.cell C n), (Topology.RelCWComplex.closedCell n j).Nonempty
-- Mathlib.LinearAlgebra.Matrix.Circulant
Matrix.circulant_apply : ∀ {α : Type u_1} {n : Type u_3} [inst : Sub n] (v : n → α) (i j : n), Matrix.circulant v i j = v (i - j)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.forM_eq_forM_toList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {cmp : α → α → Ordering} {f : α → β → m PUnit.{u_1 + 1}}
  [inst : Monad m] [LawfulMonad m] {t : RBTree.RBMap α β cmp}, RBTree.RBMap.forM f t = t.toList.forM fun p => f p.1 p.2
-- Lean.Meta.Match.CaseArraySizes
/-- Split goal `... |- C a` into sizes.size + 1 subgoals
1) `..., x_1 ... x_{sizes[0]} |- C #[x_1, ... x_{sizes[0]}]`
...
n) `..., x_1 ... x_{sizes[n-1]}  |- C #[x_1, ..., x_{sizes[n-1]}]`
n+1) `..., (h_1 : a.size != sizes[0]), ..., (h_n : a.size != sizes[n-1]) |- C a`
where `n = sizes.size`  -/
Lean.Meta.caseArraySizes : Lean.MVarId →
  Lean.FVarId →
    Array ℕ → optParam Lean.Name `x → optParam Lean.Name `h → Lean.MetaM (Array Lean.Meta.CaseArraySizesSubgoal)
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
_private.Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol.0.fastJacobiSym.eq : jacobiSym = fastJacobiSym✝
-- Init.Control.State
/-- Runs an action from the underlying monad in the monad with state. The state is not modified.

This function is typically implicitly accessed via a `MonadLiftT` instance as part of [automatic
lifting](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=monad-lifting).
 -/
StateT.lift : {σ : Type u} → {m : Type u → Type v} → [Monad m] → {α : Type u} → m α → StateT σ m α
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- A cotrident on `f` and `g` is just a `Cocone (parallelFamily f)`.  -/
CategoryTheory.Limits.Cotrident : {J : Type w} →
  {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (J → (X ⟶ Y)) → Type (max (max w u) v)
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
/-- The sigmoid function from `ℝ` to `I`.  -/
unitInterval.sigmoid : ℝ → ↑unitInterval
-- Mathlib.Data.Nat.Find
Nat.find_spec : ∀ {p : ℕ → Prop} [inst : DecidablePred p] (H : ∃ n, p n), p (Nat.find H)
-- Mathlib.Data.PEquiv
PEquiv.single_trans_of_eq_none : ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : DecidableEq α] [inst_1 : DecidableEq β] (a : α) {b : β} {f : β ≃. δ},
  f b = none → (PEquiv.single a b).trans f = ⊥
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.monotone_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F}, Monotone (AddSubmonoid.comap f)
-- Mathlib.Analysis.Normed.Module.Basic
/-- Produces a `PseudoMetricSpace E` instance from a `SeminormedSpace.Core` on a type that
already has a preexisting uniform space structure and a preexisting bornology. This requires proofs
that the uniformity induced by the norm is equal to the preexisting uniformity, and likewise for
the bornology. See note [reducible non-instances].  -/
PseudoMetricSpace.ofSeminormedSpaceCoreReplaceAll : {𝕜 : Type u_6} →
  {E : Type u_7} →
    [inst : NormedField 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Norm E] →
          [inst_3 : Module 𝕜 E] →
            [U : UniformSpace E] →
              [B : Bornology E] →
                (core : SeminormedSpace.Core 𝕜 E) →
                  uniformity E = uniformity E →
                    (∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s) → PseudoMetricSpace E
-- Mathlib.Logic.IsEmpty.Basic
rightTotal_empty : ∀ {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty β], Relator.RightTotal R
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.map.eq_1 : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁),
  MvPolynomial.map f = AddMonoidAlgebra.mapRingHom (σ →₀ ℕ) f
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.domDomCongr_refl : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N),
  AlternatingMap.domDomCongr (Equiv.refl ι) f = f
-- Mathlib.Topology.Order.LawsonTopology
/-- Type synonym for a preorder equipped with the Lawson topology.
 -/
Topology.WithLawson : Type u_2 → Type u_2
-- Mathlib.Data.FunLike.Group
FunLike.coe_coeAddMonoidHom' : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : AddZero F] [inst_2 : AddZeroClass β]
  [inst_3 : IsZeroApply F α β] [inst_4 : IsAddApply F α β], ↑(FunLike.coeAddMonoidHom F α β) = FunLike.coeAddHom F α β
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.iInf_ker_proj : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_4} {φ : ι → Type u_5} [inst_1 : (i : ι) → TopologicalSpace (φ i)]
  [inst_2 : (i : ι) → AddCommMonoid (φ i)] [inst_3 : (i : ι) → Module R (φ i)],
  ⨅ i, (↑(ContinuousLinearMap.proj i)).ker = ⊥
-- Mathlib.Tactic.Linter.MinImports
/-- `#reset_min_imports` sets to empty the current list of cumulative imports.  -/
Mathlib.Linter.«command#reset_min_imports» : Lean.ParserDescr