mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Complex.Order
Complex.lt_def : ∀ {z w : ℂ}, z < w ↔ z.re < w.re ∧ z.im = w.im
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.coe_one : ∀ {α : Type u_2} [inst : NonUnitalNonAssocSemiring α], ⇑1 = id
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.prod_apply : ∀ {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] {P : Type u_4} [inst_5 : AddCommMonoid P] [inst_6 : Module R P]
  {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (g : M [⋀^ι]→ₗ[R] P) (m : (i : ι) → (fun x => M) i), (f.prod g) m = (f m, g m)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinOp.umod.sizeOf_spec : sizeOf Std.Tactic.BVDecide.BVBinOp.umod = 1
-- Mathlib.RingTheory.Polynomial.Subring
Polynomial.support_toSubring : ∀ {R : Type u_1} [inst : Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.coeffs ⊆ ↑T),
  (p.toSubring T hp).support = p.support
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.unop_closure : ∀ {M : Type u_2} [inst : Mul M] (s : Set Mᵐᵒᵖ),
  (Subsemigroup.closure s).unop = Subsemigroup.closure (MulOpposite.op ⁻¹' s)
-- Mathlib.RingTheory.RingHom.Unramified
RingHom.FormallyUnramified.stableUnderComposition : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => RingHom.FormallyUnramified
-- Mathlib.Topology.Connected.Basic
/-- The directed sUnion of a set S of preconnected subsets is preconnected.  -/
IsPreconnected.sUnion_directed : ∀ {α : Type u} [inst : TopologicalSpace α] {S : Set (Set α)},
  DirectedOn (fun x1 x2 => x1 ⊆ x2) S → (∀ s ∈ S, IsPreconnected s) → IsPreconnected (⋃₀ S)
-- Mathlib.LinearAlgebra.Complex.Module
/-- Register as an instance (with low priority) the fact that a complex vector space is also a real
vector space.  -/
Module.complexToReal : (E : Type u_1) → [inst : AddCommGroup E] → [Module ℂ E] → Module ℝ E
-- Mathlib.ModelTheory.Definability
Set.definable_empty : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁}, A.Definable L ∅
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.replaceFTR.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Array α → Sort u_2) (x : α) (xs : List α) (acc : Array α)
  (h_1 : (acc : Array α) → motive [] acc) (h_2 : (x : α) → (xs : List α) → (acc : Array α) → motive (x :: xs) acc),
  (match x :: xs, acc with
    | [], acc => h_1 acc
    | x :: xs, acc => h_2 x xs acc) =
    h_2 x xs acc
-- Mathlib.Topology.Sheaves.Alexandrov
/-- This is an auxiliary definition which is only meant to be used in `isLimit` below.  -/
Alexandrov.lowerCone : {X : Type v} →
  [inst : TopologicalSpace X] →
    [inst_1 : Preorder X] →
      [inst_2 : Topology.IsUpperSet X] →
        {C : Type u} →
          [inst_3 : CategoryTheory.Category.{v, u} C] →
            [inst_4 : CategoryTheory.Limits.HasLimits C] →
              {F : CategoryTheory.Functor X C} →
                {α : Type v} →
                  (Us : α → TopologicalSpace.Opens X) →
                    CategoryTheory.Limits.Cone
                        ((CategoryTheory.ObjectProperty.ι fun V => ∃ i, V ≤ Us i).op.comp
                          (Alexandrov.principalsKanExtension F)) →
                      CategoryTheory.Limits.Cone ((Alexandrov.generator (iSup Us)).comp F)
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- associativity of the tensorator  -/
CategoryTheory.Functor.LaxMonoidal.associativity_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  (F : CategoryTheory.Functor C D) [self : F.LaxMonoidal] (X Y Z : C) {Z_1 : D}
  (h :
    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (F.obj Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
        (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.LaxMonoidal.μ F Y Z))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.LaxMonoidal.μ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) h))
-- Mathlib.Data.Ordmap.Invariants
Ordnode.rotateL.eq_1 : ∀ {α : Type u_1} (x : Ordnode α) (x_1 : α) (size : ℕ) (m : Ordnode α) (y : α) (r : Ordnode α),
  x.rotateL x_1 (Ordnode.node size m y r) =
    if m.size < Ordnode.ratio * r.size then x.node3L x_1 m y r else x.node4L x_1 m y r
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.Presieve.w : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C}
  (R : CategoryTheory.Presieve X) [inst_1 : R.HasPairwisePullbacks],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Equalizer.forkMap P R)
      (CategoryTheory.Equalizer.Presieve.firstMap P R) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Equalizer.forkMap P R)
      (CategoryTheory.Equalizer.Presieve.secondMap P R)
-- Lean.Parser.Do
Lean.Parser.Term.doReassign : Lean.Parser.Parser
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.contractRight_one : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (d : Module.Dual R M), (CliffordAlgebra.contractRight 1) d = 0
-- Mathlib.Data.Int.Fib.Basic
Int.fib_add_one : ∀ (n : ℤ), Int.fib (n + 1) = Int.fib (n + 2) - Int.fib n
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
addRothNumber_le : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] (s : Finset α), addRothNumber s ≤ s.card
-- Mathlib.RingTheory.Congruence.Hom
RingCon.comapQuotientEquivRangeₐ.congr_simp : ∀ {M : Type u_1} {N : Type u_2} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M]
  [inst_3 : Semiring N] [inst_4 : Algebra R N] (c : RingCon M) (f : N →ₐ[R] M) {d : RingCon N} (h : d = c.comap f),
  c.comapQuotientEquivRangeₐ f h = c.comapQuotientEquivRangeₐ f h
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.single_tag : ∀ {ι : Type u_1} (I J : BoxIntegral.Box ι) (hJ : J ≤ I) (x : ι → ℝ) (h : x ∈ BoxIntegral.Box.Icc I),
  (BoxIntegral.TaggedPrepartition.single I J hJ x h).tag = fun x_1 => x
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.biprodComparison_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) (X Y : C) [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)],
  CategoryTheory.CategoryStruct.comp (F.biprodComparison X Y) CategoryTheory.Limits.biprod.snd =
    F.map CategoryTheory.Limits.biprod.snd
-- Mathlib.AlgebraicGeometry.Over
/-- Given `X.Over S` and `Y.Over S` and `f : X ⟶ Y`,
`f.IsOver S` is the typeclass asserting `f` commutes with the structure morphisms.  -/
AlgebraicGeometry.Scheme.Hom.IsOver : {X Y : AlgebraicGeometry.Scheme} → X.Hom Y → (S : AlgebraicGeometry.Scheme) → [X.Over S] → [Y.Over S] → Prop
-- Lean.DocString.Add
/-- Adds an elaborated Verso module docstring to the environment.
 -/
Lean.addVersoModDocStringCore : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [MonadLiftT BaseIO m] → [Lean.MonadError m] → Lean.VersoModuleDocs.Snippet → Array Lean.Doc.DeferredCheck → m Unit
-- Mathlib.Topology.Path
Path.extend_trans_of_le_half : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y z : X} (γ₁ : Path x y) (γ₂ : Path y z) {t : ℝ},
  t ≤ 1 / 2 → (γ₁.trans γ₂).extend t = γ₁.extend (2 * t)
-- Mathlib.Analysis.Calculus.FDeriv.Pow
/-- Eta-expanded form of `fderivWithin_pow'` -/
fderivWithin_fun_pow' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {x : E}
  {s : Set E},
  UniqueDiffWithinAt 𝕜 s x →
    ∀ (n : ℕ),
      DifferentiableWithinAt 𝕜 f s x →
        fderivWithin 𝕜 (fun i => f i ^ n) s x =
          ∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • fderivWithin 𝕜 f s x
-- Mathlib.Algebra.Polynomial.Coeff
/-- `constantCoeff p` returns the constant term of the polynomial `p`,
defined as `coeff p 0`. This is a ring homomorphism.  -/
Polynomial.constantCoeff : {R : Type u} → [inst : Semiring R] → Polynomial R →+* R
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.WeaklyRegular.smul_nnreal : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [μ.WeaklyRegular] (c : NNReal), (c • μ).WeaklyRegular
-- Mathlib.Data.Sum.Lattice
Sum.Lex.inl_sup : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] (a₁ a₂ : α),
  Sum.inlₗ (a₁ ⊔ a₂) = Sum.inlₗ a₁ ⊔ Sum.inlₗ a₂
-- Batteries.Data.List.Basic
List.instDecidableForall₂ : {α : Type u_1} →
  {β : Type u_2} →
    {R : α → β → Prop} →
      [(a : α) → (b : β) → Decidable (R a b)] → (l₁ : List α) → (l₂ : List β) → Decidable (List.Forall₂ R l₁ l₂)
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- Eta-expanded form of `derivWithin.neg` -/
derivWithin.fun_neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜}, derivWithin (fun i => -f i) s x = -derivWithin f s x
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_deg : ∀ (pq : ℕ × ℕ), CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat.deg pq = ↑pq.1 + ↑pq.2
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (lhs lhs_1 : aig.RefVec w),
  lhs = lhs_1 →
    ∀ (rhs rhs_1 : aig.RefVec w),
      rhs = rhs_1 →
        ∀ (curr : ℕ) (hcurr : curr ≤ w) (cin cin_1 : aig.Ref),
          cin = cin_1 →
            ∀ (s s_1 : aig.RefVec curr),
              s = s_1 →
                Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go aig lhs rhs curr hcurr cin s =
                  Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go aig lhs_1 rhs_1 curr hcurr cin_1 s_1
-- Mathlib.Data.Multiset.UnionInter
Multiset.add_eq_union_right_of_le : ∀ {α : Type u_1} [inst : DecidableEq α] {x y z : Multiset α}, z ≤ y → (x + y = x ∪ z ↔ y = z ∧ Disjoint x y)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.isCycleOn : ∀ {α : Type u_2} {f : Equiv.Perm α}, f.IsCycle → f.IsCycleOn {x | f x ≠ x}
-- Aesop.Builder.Basic
Aesop.RuleBuilderInput.term : Aesop.RuleBuilderInput → Lean.Term
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.void.sizeOf_spec : sizeOf Lean.IR.IRType.void = 1
-- Mathlib.Analysis.Convex.Gauge
/-- **Alias** of `setOfPred_gauge_lt_one_eq_interior`. -/
gauge_lt_one_eq_interior : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : TopologicalSpace E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E], Convex ℝ s → s ∈ nhds 0 → {x | gauge s x < 1} = interior s
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : LawfulBEq α] {f : α → β → γ} {k : α} {h' : k ∈ Std.ExtDHashMap.map f m},
  Std.ExtDHashMap.Const.get (Std.ExtDHashMap.map f m) k h' = f k (Std.ExtDHashMap.Const.get m k ⋯)
-- Mathlib.Data.List.MinMax
List.minimum_le_of_mem : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} {a m : α}, a ∈ l → l.minimum = ↑m → m ≤ a
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IteratorLoop.wellFounded_of_productive.match_1.eq_1 : ∀ {γ : Type u_1} (motive : ForInStep γ → Sort u_2) (a : γ) (h_1 : (a : γ) → motive (ForInStep.done a))
  (h_2 : (x : ForInStep γ) → motive x),
  (match ForInStep.done a with
    | ForInStep.done a => h_1 a
    | x => h_2 x) =
    h_1 a
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.PosNum.cmp.match_1.eq_1 : ∀ (motive : PosNum → PosNum → Sort u_1) (h_1 : Unit → motive PosNum.one PosNum.one)
  (h_2 : (x : PosNum) → motive x PosNum.one) (h_3 : (x : PosNum) → motive PosNum.one x)
  (h_4 : (a b : PosNum) → motive a.bit0 b.bit0) (h_5 : (a b : PosNum) → motive a.bit0 b.bit1)
  (h_6 : (a b : PosNum) → motive a.bit1 b.bit0) (h_7 : (a b : PosNum) → motive a.bit1 b.bit1),
  (match PosNum.one, PosNum.one with
    | PosNum.one, PosNum.one => h_1 ()
    | x, PosNum.one => h_2 x
    | PosNum.one, x => h_3 x
    | a.bit0, b.bit0 => h_4 a b
    | a.bit0, b.bit1 => h_5 a b
    | a.bit1, b.bit0 => h_6 a b
    | a.bit1, b.bit1 => h_7 a b) =
    h_1 ()
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.embedding_obj_X : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] (X : C)
  (x : PUnit.{1}), ((CategoryTheory.Mat_.embedding C).obj X).X x = X
-- Mathlib.Order.Hom.Lattice
InfHom.instBoundedOrder.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : SemilatticeInf β] [inst_2 : BoundedOrder β],
  InfHom.instBoundedOrder = BoundedOrder.lift DFunLike.coe ⋯ ⋯ ⋯
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
lintegral_comp_pi_polarCoord_symm : ∀ {ι : Type u_1} [inst : Fintype ι] (f : (ι → ℝ × ℝ) → ENNReal),
  (∫⁻ (p : ι → ℝ × ℝ) in Set.univ.pi fun x => polarCoord.target,
      (∏ i, ENNReal.ofReal (p i).1) * f fun i => ↑polarCoord.symm (p i)) =
    ∫⁻ (p : ι → ℝ × ℝ), f p
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.D₁_D₁_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁₂ i₁₂' i₁₂'' : I₁₂) {Z : C} (h : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂' i₁₂'') h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Data.Nat.GCD.Basic
/-- **Alias** of `Nat.Coprime.stdSymm`. -/
Nat.Coprime.symmetric : Std.Symm Nat.Coprime
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerLeft_hom_inv_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) {Z : a ⟶ c}
  (h_1 : CategoryTheory.CategoryStruct.comp f g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η.inv) h_1) =
    h_1
-- Init.Data.List.Count
List.count_reverse : ∀ {α : Type u_1} [inst : BEq α] {a : α} {l : List α}, List.count a l.reverse = List.count a l
-- Qq.MetaM
Qq.instReprMaybeLevelDefEq : {u v : Lean.Level} → Repr (Qq.MaybeLevelDefEq u v)
-- Std.Http.Internal.Char
_private.Std.Http.Internal.Char.0.Std.Http.Internal.Char.quotedPairChar.match_1.eq_1 : ∀ (motive : Char → Sort u_1) (h_1 : Unit → motive '\t') (h_2 : Unit → motive ' ') (h_3 : (x : Char) → motive x),
  (match '\t' with
    | '\t' => h_1 ()
    | ' ' => h_2 ()
    | x => h_3 x) =
    h_1 ()
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentFilter.mk : Option String → Option String → Option String → Lean.Lsp.DocumentFilter
-- Mathlib.Analysis.Convex.Exposed
/-- If `B` is a nonempty exposed subset of `A`, then `B` is the intersection of `A` with some closed
half-space. The converse is *not* true. It would require that the corresponding open half-space
doesn't intersect `A`.  -/
IsExposed.eq_inter_halfSpace' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [inst_2 : PartialOrder 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module 𝕜 E] {A B : Set E},
  IsExposed 𝕜 A B → B.Nonempty → ∃ l a, B = {x | x ∈ A ∧ a ≤ l x}
-- Init.Data.List.Sublist
List.cons_prefix_iff : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, a :: l₁ <+: l₂ ↔ ∃ l', l₂ = a :: l' ∧ l₁ <+: l'
-- Std.Data.HashMap.IteratorLemmas
Std.HashMap.toList_keysIter : ∀ {α β : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m.keysIter.toList = m.keys
-- Mathlib.Algebra.Homology.SpectralObject.Homology
/-- The exact sequence expressing `E^n(f₂ ≫ f₃, f₄, f₅)` as the kernel
of the differential `E^n(f₃, f₄, f₅) ⟶ E^{n+1}(f₁, f₂, f₃)`  -/
CategoryTheory.Abelian.SpectralObject.dKernelSequence : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Abelian C] →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] →
          CategoryTheory.Abelian.SpectralObject C ι →
            {i₀ i₁ i₂ i₃ i₄ i₅ : ι} →
              (i₀ ⟶ i₁) →
                (f₂ : i₁ ⟶ i₂) →
                  (f₃ : i₂ ⟶ i₃) →
                    (i₃ ⟶ i₄) →
                      (i₄ ⟶ i₅) →
                        (f₂₃ : i₁ ⟶ i₃) →
                          CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃ →
                            (n₀ n₁ n₂ n₃ : ℤ) →
                              autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dKernelSequence._auto_1 →
                                autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dKernelSequence._auto_3 →
                                  autoParam (n₂ + 1 = n₃)
                                      CategoryTheory.Abelian.SpectralObject.dKernelSequence._auto_5 →
                                    CategoryTheory.ShortComplex C
-- Lean.Parser.Command
Lean.Parser.Command.public.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticForm.isSymm_toMatrix' : ∀ {R : Type u_3} {n : Type w} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] [inst_3 : Invertible 2]
  (Q : QuadraticForm R (n → R)), Q.toMatrix'.IsSymm
-- Mathlib.Topology.Algebra.Order.Floor
ContinuousOn.comp_fract : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α]
  [inst_3 : TopologicalSpace α] [IsStrictOrderedRing α] [OrderTopology α] [inst_6 : TopologicalSpace β]
  [inst_7 : TopologicalSpace γ] {s : β → α} {f : β → α → γ},
  ContinuousOn (Function.uncurry f) (Set.univ ×ˢ Set.Icc 0 1) →
    Continuous s → (∀ (s : β), f s 0 = f s 1) → Continuous fun x => f x (Int.fract (s x))
-- Mathlib.Data.NNReal.Defs
NNReal.coe_mono : Monotone NNReal.toReal
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
Filter.Tendsto.uniformity_div : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3} {f g : ι → α × α}
  {l : Filter ι},
  Filter.Tendsto f l (uniformity α) → Filter.Tendsto g l (uniformity α) → Filter.Tendsto (f / g) l (uniformity α)
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wOppSide_comm : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.WOppSide x y ↔ s.WOppSide y x
-- Init.Data.List.Lemmas
List.foldl_assoc : ∀ {α : Type u_1} {op : α → α → α} [ha : Std.Associative op] {l : List α} {a₁ a₂ : α},
  List.foldl op (op a₁ a₂) l = op a₁ (List.foldl op a₂ l)
-- Init.Data.UInt.BasicAux
UInt32.instOfNat : {n : ℕ} → OfNat UInt32 n
-- Mathlib.Algebra.Order.Group.Indicator
Set.mulIndicator_le_mulIndicator' : ∀ {α : Type u_2} {M : Type u_3} [inst : Preorder M] [inst_1 : One M] {s : Set α} {f g : α → M} {a : α},
  (a ∈ s → f a ≤ g a) → s.mulIndicator f a ≤ s.mulIndicator g a
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.toTriangle_surjOn : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [inst : DecidableEq α] [inst_1 : DecidableEq β]
  [inst_2 : DecidableEq γ] [SimpleGraph.TripartiteFromTriangles.NoAccidental t],
  Set.SurjOn (⇑SimpleGraph.TripartiteFromTriangles.toTriangle) (↑t)
    ((SimpleGraph.TripartiteFromTriangles.graph t).cliqueSet 3)
-- Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic
/-- The embedding itself (position of vertices)  -/
SimpleGraph.UnitDistEmbedding.p : {V : Type u_1} → {G : SimpleGraph V} → {E : Type u_3} → [inst : MetricSpace E] → G.UnitDistEmbedding E → V ↪ E
-- Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.exists_colimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {κ : Cardinal.{w}}
  [inst_1 : Fact κ.IsRegular],
  P.IsCardinalFilteredGenerator κ →
    ∀ (X : C), ∃ J x, ∃ (_ : CategoryTheory.IsCardinalFiltered J κ), P.colimitsOfShape J X
-- Mathlib.Algebra.Module.Submodule.Lattice
AddSubmonoid.toNatSubmodule_toAddSubmonoid : ∀ {M : Type u_3} [inst : AddCommMonoid M] (S : AddSubmonoid M), (AddSubmonoid.toNatSubmodule S).toAddSubmonoid = S
-- Mathlib.Algebra.Homology.HomotopyCategory.KInjective
CochainComplex.IsKInjective.eq_δ_of_cocycle' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} {n : ℤ} (z : CochainComplex.HomComplex.Cocycle K L n) [L.IsKInjective],
  HomologicalComplex.Acyclic L → ∀ (m : ℤ), m + 1 = n → ∃ α, CochainComplex.HomComplex.δ m n α = ↑z
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.elabAppLVals : Lean.Expr →
  List Lean.Elab.Term.LVal →
    Array Lean.Elab.Term.NamedArg →
      Array Lean.Elab.Term.Arg → Option Lean.Expr → Bool → Bool → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.mk_add_mk : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Add R] (a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R),
  { re := a₁, imI := a₂, imJ := a₃, imK := a₄ } + { re := b₁, imI := b₂, imJ := b₃, imK := b₄ } =
    { re := a₁ + b₁, imI := a₂ + b₂, imJ := a₃ + b₃, imK := a₄ + b₄ }
-- Mathlib.Condensed.TopCatAdjunction
CondensedSet.toTopCatMap_hom_apply : ∀ {X Y : CondensedSet} (f : X ⟶ Y) (a : X.obj.obj (Opposite.op (CompHaus.of PUnit.{u + 1}))),
  (TopCat.Hom.hom (CondensedSet.toTopCatMap f)) a =
    (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op (CompHaus.of PUnit.{u + 1})))) a
-- Mathlib.SetTheory.ZFC.PSet
PSet.instInhabitedTypeInsert : (x y : PSet.{u_1}) → Inhabited (insert x y).Type