mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.DFinsupp.Multiset
Multiset.toDFinsupp_inj : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, Multiset.toDFinsupp s = Multiset.toDFinsupp t ↔ s = t
-- Mathlib.Algebra.Group.Action.Defs
VAddAssocClass.op_left : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} [inst : VAdd M α] [inst_1 : VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α]
  [inst_3 : VAdd M N] [inst_4 : VAdd Mᵃᵒᵖ N] [IsCentralVAdd M N] [inst_6 : VAdd N α] [VAddAssocClass M N α],
  VAddAssocClass Mᵃᵒᵖ N α
-- Init.Data.Order.PackageFactories
Std.Packages.LinearPreorderOfOrdArgs.beq_iff : ∀ {α : Type u} (self : Std.Packages.LinearPreorderOfOrdArgs α),
  let this := self.ord;
  let this_1 := self.le;
  have this_2 := ⋯;
  let this_3 := self.beq;
  ∀ (a b : α), (a == b) = true ↔ compare a b = Ordering.eq
-- Lean.Data.Lsp.Basic
Lean.Lsp.SnippetString.mk.injEq : ∀ (value value_1 : String), ({ value := value } = { value := value_1 }) = (value = value_1)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.one_mem_nthRootsFinset : ∀ {R : Type u} {n : ℕ} [inst : CommRing R] [inst_1 : IsDomain R], 0 < n → 1 ∈ Polynomial.nthRootsFinset n 1
-- Mathlib.GroupTheory.NoncommPiCoprod
AddSubgroup.noncommPiCoprod_single : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} [inst_1 : Fintype ι]
  [inst_2 : DecidableEq ι] {hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y} (i : ι)
  (y : ↥(H i)), (AddSubgroup.noncommPiCoprod hcomm) (Pi.single i y) = ↑y
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.coe_continuousMap_mk : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] (f : P →ᵃ[R] Q) (h : Continuous f.toFun),
  ↑{ toAffineMap := f, cont := h } = { toFun := ⇑f, continuous_toFun := h }
-- Mathlib.Algebra.Order.Group.Cone
AddGroupCone.mem_nonneg : ∀ {H : Type u_1} [inst : AddCommGroup H] [inst_1 : PartialOrder H] [inst_2 : IsOrderedAddMonoid H] {a : H},
  a ∈ AddGroupCone.nonneg H ↔ 0 ≤ a
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.mkBinOp : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.single_symm_apply : ∀ {α : Type u_1} {β : Type u_2} (a : α) (b a_1 : β), ↑(PartialEquiv.single a b).symm a_1 = Function.const β a a_1
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.isIso_hom_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory}
  (f : X ⟶ Y), CategoryTheory.IsIso f.hom ↔ CategoryTheory.IsIso f
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.eval_charpolyRev : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] {M : Matrix n n R},
  Polynomial.eval 0 M.charpolyRev = 1
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.copy_eq_self : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (f : α →ᵈ β) {f' : α → β}
  (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
AlgebraicGeometry.Scheme.irreducibleComponentOpen_eq_top : ∀ (X : AlgebraicGeometry.Scheme),
  ∀ Z ∈ irreducibleComponents ↥X,
    ∀ [inst : AlgebraicGeometry.IsNoetherian X] [IrreducibleSpace ↥X], X.irreducibleComponentOpen Z = ⊤
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
FundamentalGroupoidFunctor.coneDiscreteComp_obj_mapCone : ∀ {I : Type u} (X : I → TopCat),
  (FundamentalGroupoidFunctor.coneDiscreteComp X).functor.obj
      (FundamentalGroupoid.fundamentalGroupoidFunctor.mapCone (TopCat.piFan X)) =
    CategoryTheory.Limits.Fan.mk (FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of ((i : I) → ↑(X i))))
      (FundamentalGroupoidFunctor.proj X)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.coe_iInf : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {ι : Sort u_1} (p : ι → LieSubmodule R L M),
  ↑(⨅ i, p i) = ⋂ i, ↑(p i)
-- Mathlib.Data.ENNReal.Operations
/-- This lemma has an abbreviated name because it is used frequently.  -/
ENNReal.cancel_of_lt : ∀ {a : ENNReal}, a < ⊤ → AddLECancellable a
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.instIsStrictlyGEObjHomologicalComplexIntUpSingle : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (A : C) (n : ℤ),
  CochainComplex.IsStrictlyGE ((HomologicalComplex.single C (ComplexShape.up ℤ) n).obj A) n
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `le_inv_mul_iff_mul_le`. -/
mul_le_of_le_inv_mul : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] {a b c : α}, b ≤ a⁻¹ * c → a * b ≤ c
-- Lean.Elab.DeclModifiers
Lean.Elab.RecKind.default.sizeOf_spec : sizeOf Lean.Elab.RecKind.default = 1
-- Mathlib.Combinatorics.Additive.CovBySMul
CovByVAdd.of_subset : ∀ {M : Type u_1} {X : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M X] {A B : Set X}, A ⊆ B → CovByVAdd M 1 A B
-- Mathlib.Topology.Algebra.Group.Basic
AddMonoidHom.isOpenQuotientMap_iff_isQuotientMap : ∀ {A : Type u_1} [inst : AddGroup A] [inst_1 : TopologicalSpace A] [ContinuousAdd A] {B : Type u_2}
  [inst_3 : AddGroup B] [inst_4 : TopologicalSpace B] {F : Type u_3} [inst_5 : FunLike F A B] [AddMonoidHomClass F A B]
  {φ : F}, IsOpenQuotientMap ⇑φ ↔ Topology.IsQuotientMap ⇑φ
-- Mathlib.GroupTheory.Coxeter.Inversion
_private.Mathlib.GroupTheory.Coxeter.Inversion.0.CoxeterSystem.leftInvSeq_eq_reverse_rightInvSeq_reverse : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B),
  cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse
-- Mathlib.Algebra.Order.SuccPred
Order.covBy_add_one : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Add α] [inst_2 : One α] [SuccAddOrder α] [NoMaxOrder α] (x : α),
  x ⋖ x + 1
-- Std.Data.ExtTreeSet.Basic
/-- Removes the given key if it exists.  -/
Std.ExtTreeSet.erase : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → α → Std.ExtTreeSet α cmp
-- Mathlib.Analysis.Normed.Lp.WithLp
/-- A type synonym for the given `V`, associated with the L`p` norm. Note that by default this just
forgets the norm structure on `V`; it is up to downstream users to implement the L`p` norm (for
instance, on `Prod` and finite `Pi` types).  -/
WithLp : ENNReal → Type u_1 → Type u_1
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- If `φ : S₁ ⟶ S₂` is a morphism of short complexes such that `φ.τ₁` is epi, `φ.τ₂` is an iso
and `φ.τ₃` is mono, then a left homology data for `S₁` induces a left homology data for `S₂` with
the same `K` and `H` fields. The inverse construction is `ofEpiOfIsIsoOfMono'`.  -/
CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          S₁.LeftHomologyData →
            [CategoryTheory.Epi φ.τ₁] → [CategoryTheory.IsIso φ.τ₂] → [CategoryTheory.Mono φ.τ₃] → S₂.LeftHomologyData
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k a : α}, (t.erase k).getKey! a = if cmp k a = Ordering.eq then default else t.getKey! a
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioi_top : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] [inst_2 : OrderTop α], Finset.Ioi ⊤ = ∅
-- Lean.Compiler.ModPkgExt
_private.Lean.Compiler.ModPkgExt.0.Lean.modPkgExt : Lean.ModuleEnvExtension (Option Lean.PkgId)
-- Mathlib.Analysis.Meromorphic.Order
/-- The order of a quotient is the difference of the orders.
 -/
meromorphicOrderAt_div : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_4} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {x : 𝕜} {f g : 𝕜 → 𝕜'},
  MeromorphicAt f x → MeromorphicAt g x → meromorphicOrderAt (f / g) x = meromorphicOrderAt f x - meromorphicOrderAt g x
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoTree.brecOn_6.eq : ∀ {motive_1 : Lean.Elab.InfoTree → Sort u} {motive_2 : Lean.PersistentArray Lean.Elab.InfoTree → Sort u}
  {motive_3 : Lean.PersistentArrayNode Lean.Elab.InfoTree → Sort u} {motive_4 : Array Lean.Elab.InfoTree → Sort u}
  {motive_5 : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u}
  {motive_6 : List Lean.Elab.InfoTree → Sort u} {motive_7 : List (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u}
  (t : List (Lean.PersistentArrayNode Lean.Elab.InfoTree)) (F_1 : (t : Lean.Elab.InfoTree) → t.below → motive_1 t)
  (F_2 : (t : Lean.PersistentArray Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_1 t → motive_2 t)
  (F_3 : (t : Lean.PersistentArrayNode Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_2 t → motive_3 t)
  (F_4 : (t : Array Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_3 t → motive_4 t)
  (F_5 : (t : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree)) → Lean.Elab.InfoTree.below_4 t → motive_5 t)
  (F_6 : (t : List Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_5 t → motive_6 t)
  (F_7 : (t : List (Lean.PersistentArrayNode Lean.Elab.InfoTree)) → Lean.Elab.InfoTree.below_6 t → motive_7 t),
  Lean.Elab.InfoTree.brecOn_6 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 =
    F_7 t (Lean.Elab.InfoTree.brecOn_6.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7).2
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, (t₁ \ t₂).getKeyD k fallback = if k ∈ t₂ then fallback else t₁.getKeyD k fallback
-- Init.Data.SInt.Bitwise
ISize.and_assoc : ∀ (a b c : ISize), a &&& b &&& c = a &&& (b &&& c)
-- Mathlib.Algebra.Group.Support
Function.mulSupport_div : ∀ {α : Type u_1} {G : Type u_3} [inst : DivisionMonoid G] (f g : α → G),
  (Function.mulSupport fun x => f x / g x) ⊆ Function.mulSupport f ∪ Function.mulSupport g
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- The domain of definition of a partial map.  -/
AlgebraicGeometry.Scheme.PartialMap.domain : {X Y : AlgebraicGeometry.Scheme} → X.PartialMap Y → X.Opens
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.comp_assoc_of_third_is_zero_cochain : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K L : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁)
  (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (z₃ : CochainComplex.HomComplex.Cochain K L 0) (h₁₂ : n₁ + n₂ = n₁₂),
  (z₁.comp z₂ h₁₂).comp z₃ ⋯ = z₁.comp (z₂.comp z₃ ⋯) h₁₂
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey!_eq_minKeyD_default : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t.minKey! = t.minKeyD default
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceL!.match_3.congr_eq_1 : ∀ {α : Type u_1} {β : α → Type u_2}
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (ll lr : Std.DTreeMap.Internal.Impl α β)
  (h_1 :
    (lls : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (lrs : ℕ) →
              (lrk : α) →
                (lrv : β lrk) →
                  (lrl lrr : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner lls k v l r)
                      (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr))
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l r) Std.DTreeMap.Internal.Impl.leaf)
  (h_3 : (x : Std.DTreeMap.Internal.Impl α β) → motive Std.DTreeMap.Internal.Impl.leaf x) (lls : ℕ) (k : α) (v : β k)
  (l r : Std.DTreeMap.Internal.Impl α β) (lrs : ℕ) (lrk : α) (lrv : β lrk) (lrl lrr : Std.DTreeMap.Internal.Impl α β),
  ll = Std.DTreeMap.Internal.Impl.inner lls k v l r →
    lr = Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr →
      (match ll, lr with
        | Std.DTreeMap.Internal.Impl.inner lls k v l r, Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr =>
          h_1 lls k v l r lrs lrk lrv lrl lrr
        | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l r
        | Std.DTreeMap.Internal.Impl.leaf, x => h_3 x) ≍
        h_1 lls k v l r lrs lrk lrv lrl lrr
-- Mathlib.Probability.Kernel.Disintegration.Basic
/-- A kernel `κCond` is a conditional kernel for a kernel `κ` if it disintegrates it in the sense
that `κ.fst ⊗ₖ κCond = κ`.  -/
ProbabilityTheory.Kernel.IsCondKernel : {α : Type u_1} →
  {β : Type u_2} →
    {Ω : Type u_3} →
      {mα : MeasurableSpace α} →
        {mβ : MeasurableSpace β} →
          {mΩ : MeasurableSpace Ω} → ProbabilityTheory.Kernel α (β × Ω) → ProbabilityTheory.Kernel (α × β) Ω → Prop
-- Mathlib.CategoryTheory.SmallRepresentatives
/-- Given `h : CoreSmallCategoryOfSet Ω C`,
the obvious functor `h.smallCategoryOfSet.obj ⥤ C` is an equivalence.  -/
CategoryTheory.CoreSmallCategoryOfSet.equivalence : {Ω : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (h : CategoryTheory.CoreSmallCategoryOfSet Ω C) → ↑h.smallCategoryOfSet.obj ≌ C
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.inr_inr_pushoutAssoc_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂)
  (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [inst_1 : CategoryTheory.Limits.HasPushout g₁ g₂]
  [inst_2 : CategoryTheory.Limits.HasPushout g₃ g₄]
  [inst_3 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂))
      g₄]
  [inst_4 :
    CategoryTheory.Limits.HasPushout g₁
      (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))]
  {Z : C}
  (h :
    CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄ ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₃ g₄)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pushout.inr g₁
          (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pushout.inr
        (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄)
      h
-- Mathlib.Analysis.Matrix.Normed
Matrix.norm_replicateCol : ∀ {m : Type u_3} {α : Type u_5} {ι : Type u_7} [inst : Fintype m] [inst_1 : Unique ι]
  [inst_2 : SeminormedAddCommGroup α] (v : m → α), ‖Matrix.replicateCol ι v‖ = ‖v‖
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.FunctionData.mk.sizeOf_spec : ∀ (lctx : Lean.LocalContext) (insts : Lean.LocalInstances) (fn : Lean.Expr) (args : Array Mathlib.Meta.FunProp.Mor.Arg)
  (mainVar : Lean.Expr) (mainArgs : Array ℕ),
  sizeOf { lctx := lctx, insts := insts, fn := fn, args := args, mainVar := mainVar, mainArgs := mainArgs } =
    1 + sizeOf lctx + sizeOf insts + sizeOf fn + sizeOf args + sizeOf mainVar + sizeOf mainArgs
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Embedding.domRestrict_apply : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Embedding M N) (p : L.Substructure M) (x : ↥p), (f.domRestrict p) x = f ↑x
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.GeneralLinearGroup.isParabolic_iff_of_upperTriangular : ∀ {K : Type u_2} [inst : Field K] {g : GL (Fin 2) K}, ↑g 1 0 = 0 → (g.IsParabolic ↔ ↑g 0 0 = ↑g 1 1 ∧ ↑g 0 1 ≠ 0)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.lt_aleph0 : ∀ {c : Cardinal.{u_1}}, c < Cardinal.aleph0 ↔ ∃ n, c = ↑n
-- Init.Data.Array.DecidableEq
Array.instReflBEq : ∀ {α : Type u_1} [inst : BEq α] [ReflBEq α], ReflBEq (Array α)
-- Mathlib.Algebra.BigOperators.Ring.Nat
Finset.even_sum_iff_even_card_odd : ∀ {ι : Type u_1} {s : Finset ι} (f : ι → ℕ), Even (∑ i ∈ s, f i) ↔ Even {x ∈ s | Odd (f x)}.card
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.instNonempty : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps : DiscreteTiling.Protoset G X ιₚ} [Nonempty ιₚ], Nonempty (DiscreteTiling.PlacedTile ps)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getKey_getValue_mem : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {β : Type v} {l : List ((_ : α) × β)} {k : α}
  {h : Std.Internal.List.containsKey k l = true}, ⟨Std.Internal.List.getKey k l h, Std.Internal.List.getValue k l h⟩ ∈ l
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.postEquiv_counitIso : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : T ≌ D),
  (CategoryTheory.Over.postEquiv X F).counitIso =
    CategoryTheory.NatIso.ofComponents (fun A => CategoryTheory.Over.isoMk (F.counitIso.app A.left) ⋯) ⋯
-- Mathlib.MeasureTheory.Integral.Asymptotics
/-- Variant of `MeasureTheory.Integrable.mono` taking `f =O[⊤] (g)` instead of `‖f(x)‖ ≤ ‖g(x)‖`  -/
Asymptotics.IsBigO.integrable : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] {f : α → E} {g : α → F}
  [inst_1 : MeasurableSpace α] [inst_2 : NormedAddCommGroup F] {μ : MeasureTheory.Measure α},
  MeasureTheory.AEStronglyMeasurable f μ → f =O[⊤] g → MeasureTheory.Integrable g μ → MeasureTheory.Integrable f μ
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.col_transpose : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α), A.transpose.col = A.row
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_nonpos_ae : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → ℝ} {s : Set X},
  MeasurableSet s → (∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ 0) → ∫ (x : X) in s, f x ∂μ ≤ 0
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
CategoryTheory.Preadditive.commGrpEquivalence_counitIso_inv_app_hom_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C]
  (X : CategoryTheory.CommGrp C),
  (CategoryTheory.Preadditive.commGrpEquivalence.counitIso.inv.app X).hom.hom.hom = CategoryTheory.CategoryStruct.id X.X
-- Mathlib.LinearAlgebra.Pi
/-- `Fin.consEquiv` as a continuous linear equivalence.  -/
Fin.consLinearEquiv : (R : Type u) →
  {n : ℕ} →
    (M : Fin n.succ → Type u_1) →
      [inst : Semiring R] →
        [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] →
          [inst_2 : (i : Fin n.succ) → Module R (M i)] → (M 0 × ((i : Fin n) → M i.succ)) ≃ₗ[R] (i : Fin n.succ) → M i
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.reflectsColimitsOfCreatesColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_ofNat : ∀ {K : Type u_1} [inst : RCLike K] (n : ℕ) [inst_1 : n.AtLeastTwo], ↑(OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.ShortComplex.ShortExact.hasInjectiveDimensionLT_X₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C},
  S.ShortExact →
    ∀ (n : ℕ),
      CategoryTheory.HasInjectiveDimensionLT S.X₁ n →
        CategoryTheory.HasInjectiveDimensionLT S.X₃ n → CategoryTheory.HasInjectiveDimensionLT S.X₂ n
-- Mathlib.CategoryTheory.Galois.Topology
CategoryTheory.PreGaloisCategory.instT2SpaceAutFunctorFintypeCat : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat),
  T2Space (CategoryTheory.Aut F)
-- Mathlib.Order.LiminfLimsup
Filter.limsup_le_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {x : β},
  autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) Filter.limsup_le_iff._auto_1 →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) Filter.limsup_le_iff._auto_3 →
      (Filter.limsup u f ≤ x ↔ ∀ y > x, ∀ᶠ (a : α) in f, u a < y)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
CategoryTheory.Limits.FormalCoproduct.instHasWidePullbackFinHAddNatOfNatRightMkFromIsTerminalInclLeftHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C]
  (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (n : ℕ),
  CategoryTheory.Limits.HasWidePullback
    (CategoryTheory.Arrow.mk ((CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT).from U)).right
    (fun x => (CategoryTheory.Arrow.mk ((CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT).from U)).left)
    fun x => (CategoryTheory.Arrow.mk ((CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT).from U)).hom
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.coe_comp : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Zero M] [inst_1 : Zero N] [inst_2 : Zero P] (g : ZeroHom N P)
  (f : ZeroHom M N), ⇑(g.comp f) = ⇑g ∘ ⇑f
-- Mathlib.Topology.ContinuousOn
continuous_of_cover_nhds : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {ι : Sort u_5}
  {s : ι → Set α}, (∀ (x : α), ∃ i, s i ∈ nhds x) → (∀ (i : ι), ContinuousOn f (s i)) → Continuous f
-- Std.Data.HashMap.IteratorLemmas
Std.HashMap.Raw.toArray_iter : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → m.iter.toArray = m.toArray
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.op_inj : ∀ {G : Type u_2} [inst : Group G] {S T : Subgroup G}, S.op = T.op ↔ S = T
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k k' : α},
  (k == k') = true →
    ∀ {v : β}, List.Pairwise (fun a b => (a.1 == b.1) = false) l → (k, v) ∈ l → (m.insertMany l)[k']? = some v
-- Lean.Meta.Sym.Simp.SimpM
/-- Cache for context-dependent results. Cleared when entering binders
(where new hypotheses may change the result).
 -/
Lean.Meta.Sym.Simp.State.transientCache : Lean.Meta.Sym.Simp.State → Lean.Meta.Sym.Simp.Cache
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
/-- The functor which maps an object of `D` to the constant sheaf at that object, i.e. the
sheafification of the constant presheaf.
 -/
CategoryTheory.constantSheaf : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (D : Type u_2) →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [CategoryTheory.HasWeakSheafify J D] → CategoryTheory.Functor D (CategoryTheory.Sheaf J D)
-- Batteries.Data.Fin.Lemmas
Fin.findSome?_rev : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → Option α}, (Fin.findSome? fun x => f x.rev) = Fin.findSomeRev? f