mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.HomotopyEquiv.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : SizeOf C] (hom : S₁ ⟶ S₂) (inv : S₂ ⟶ S₁)
  (homotopyHomInvId :
    CategoryTheory.ShortComplex.Homotopy (CategoryTheory.CategoryStruct.comp hom inv)
      (CategoryTheory.CategoryStruct.id S₁))
  (homotopyInvHomId :
    CategoryTheory.ShortComplex.Homotopy (CategoryTheory.CategoryStruct.comp inv hom)
      (CategoryTheory.CategoryStruct.id S₂)),
  sizeOf { hom := hom, inv := inv, homotopyHomInvId := homotopyHomInvId, homotopyInvHomId := homotopyInvHomId } =
    1 + sizeOf hom + sizeOf inv + sizeOf homotopyHomInvId + sizeOf homotopyInvHomId
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.mk.sizeOf_spec : ∀ {M : Type u_3} [inst : AddZeroClass M] [inst_1 : SizeOf M] (toAddSubsemigroup : AddSubsemigroup M)
  (zero_mem' : 0 ∈ toAddSubsemigroup.carrier),
  sizeOf { toAddSubsemigroup := toAddSubsemigroup, zero_mem' := zero_mem' } =
    1 + sizeOf toAddSubsemigroup + sizeOf zero_mem'
-- Mathlib.Data.NNRat.Lemmas
/-- A recursor for nonnegative rationals in terms of numerators and denominators.  -/
NNRat.rec : {α : ℚ≥0 → Sort u_1} → ((m n : ℕ) → α (↑m / ↑n)) → (q : ℚ≥0) → α q
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
/-- A field `K` is totally real if all of its infinite places are real. In other words,
the image of every ring homomorphism `K → ℂ` is a subset of `ℝ`.  -/
NumberField.IsTotallyReal : (K : Type u_1) → [Field K] → Prop
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.ExplorationStep.gt.injEq : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α → Ordering} (a : List ((a : α) × β a)) (a_1 : α)
  (a_2 : k a_1 = Ordering.gt) (a_3 : β a_1) (a_4 : List ((a : α) × β a)) (a_5 : α) (a_6 : k a_5 = Ordering.gt)
  (a_7 : β a_5),
  (Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_1 a_2 a_3 =
      Std.DTreeMap.Internal.Impl.ExplorationStep.gt a_4 a_5 a_6 a_7) =
    (a = a_4 ∧ a_1 = a_5 ∧ a_3 ≍ a_7)
-- Mathlib.CategoryTheory.Subobject.Limits
/-- A commuting square induces a morphism between the kernel subobjects.  -/
CategoryTheory.Limits.kernelSubobjectMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {f : X ⟶ Y} →
          [inst_2 : CategoryTheory.Limits.HasKernel f] →
            {X' Y' : C} →
              {f' : X' ⟶ Y'} →
                [inst_3 : CategoryTheory.Limits.HasKernel f'] →
                  (CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') →
                    (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f) ⟶
                      CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f'))
-- Mathlib.Topology.Algebra.UniformConvergence
instMonoidUniformOnFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Monoid β],
  instMonoidUniformOnFun =
    { toMul := instMulUniformOnFun, mul_assoc := ⋯, toOne := instOneUniformOnFun, one_mul := ⋯, mul_one := ⋯,
      toNPow := NPow.ofPow, npow_zero := ⋯, npow_succ := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.comp_apply : ∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ}
  (g : B.Copy C) (f : A.Copy B) (a : α), (g.comp f) a = g (f a)
-- Mathlib.Data.Int.Interval
Int.Ioc_eq_finset_map : ∀ (a b : ℤ),
  Finset.Ioc a b = Finset.map (Nat.castEmbedding.trans (addLeftEmbedding (a + 1))) (Finset.range (b - a).toNat)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.epi_L₃_g : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C) [CategoryTheory.Epi S.L₂.g], CategoryTheory.Epi S.L₃.g
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instInvOfContinuousInv : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → [inst_2 : Inv β] → [ContinuousInv β] → Inv C(α, β)
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.instCategoryHom : {J : Type u_1} →
  [inst : LinearOrder J] → (i j : CategoryTheory.SimplicialThickening J) → CategoryTheory.Category.{u_1, u_1} (i ⟶ j)
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
/-- The function `log⁺` commutes with taking powers.  -/
Real.posLog_pow : ∀ (n : ℕ) (x : ℝ), (x ^ n).posLog = ↑n * x.posLog
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.KernelFork.condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} (s : CategoryTheory.Limits.KernelFork f),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι s) f = 0
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
/-- If `H₁ ≃g H₂`, then `extremalNumber n H₁` equals `extremalNumber n H₂`.  -/
SimpleGraph.extremalNumber_congr_right : ∀ {n : ℕ} {W₁ : Type u_4} {W₂ : Type u_5} {H₁ : SimpleGraph W₁} {H₂ : SimpleGraph W₂} (e : H₁ ≃g H₂),
  SimpleGraph.extremalNumber n H₁ = SimpleGraph.extremalNumber n H₂
-- Mathlib.Algebra.Order.Floor.Defs
instFloorRingInt : FloorRing ℤ
-- Init.Data.UInt.Lemmas
UInt8.zero_div : ∀ {a : UInt8}, 0 / a = 0
-- Mathlib.CategoryTheory.Limits.Constructions.Equalizers
/-- Define the equalizing cone  -/
CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.equalizerCone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasBinaryProducts C] →
      [CategoryTheory.Limits.HasPullbacks C] →
        (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) → CategoryTheory.Limits.Cone F
-- Mathlib.CategoryTheory.Bicategory.Coherence
CategoryTheory.FreeBicategory.normalizeIso.eq_def : ∀ {B : Type u} [inst : Quiver B] {a : B} (x x_1 : B) (x_2 : Quiver.Path a x)
  (x_3 : CategoryTheory.FreeBicategory.Hom x x_1),
  CategoryTheory.FreeBicategory.normalizeIso x_2 x_3 =
    match x, x_1, x_2, x_3 with
    | x, x_4, x_5, CategoryTheory.FreeBicategory.Hom.of f =>
      CategoryTheory.Iso.refl
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.FreeBicategory.preinclusion B).map { as := x_5 })
          (CategoryTheory.FreeBicategory.Hom.of f))
    | b, .(b), x, CategoryTheory.FreeBicategory.Hom.id .(b) =>
      CategoryTheory.Bicategory.rightUnitor ((CategoryTheory.FreeBicategory.preinclusion B).map { as := x })
    | x, x_4, p, f.comp g =>
      (CategoryTheory.Bicategory.associator ((CategoryTheory.FreeBicategory.preinclusion B).map { as := p }) f
            g).symm ≪≫
        CategoryTheory.Bicategory.whiskerRightIso (CategoryTheory.FreeBicategory.normalizeIso p f) g ≪≫
          CategoryTheory.FreeBicategory.normalizeIso (CategoryTheory.FreeBicategory.normalizeAux p f) g
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
AlgebraicGeometry.QuasiCompactCover.instUlift : ∀ {S : AlgebraicGeometry.Scheme} (𝒰 : CategoryTheory.PreZeroHypercover S)
  [inst : AlgebraicGeometry.QuasiCompactCover 𝒰],
  AlgebraicGeometry.QuasiCompactCover (AlgebraicGeometry.QuasiCompactCover.ulift 𝒰)
-- Mathlib.Algebra.ContinuedFractions.Basic
SimpContFract.instInhabited : {α : Type u_1} → [inst : One α] → Inhabited (SimpContFract α)
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanRank_eq_of_equiv : ∀ {R : Type u_1} {S : Type u_2} {M N : Type u} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S}
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : Module S N] {σ' : S →+* R}
  [inst_6 : RingHomInvPair σ σ'] [inst_7 : RingHomInvPair σ' σ] (e : M ≃ₛₗ[σ] N), ⊤.spanRank = ⊤.spanRank
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
/-- Infix notation for `OrderMonoidWithZeroHom`.  -/
«term_→*₀o_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.adjoint_one : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E], LinearMap.adjoint 1 = 1
-- Mathlib.Control.Monad.Cont
instMonadContReaderT : {m : Type u → Type v} → {ρ : Type u} → [MonadCont m] → MonadCont (ReaderT ρ m)
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance
/-- **Alias** of `CategoryTheory.SimplicialObject.Homotopy.congr_sSetHomologyMap`.

---

Simplicially homotopic maps of simplicial sets induce the same map on
homology of the singular chain complex (with coefficients in `R`).
The assumption is in `SimplicialObject.Homotopy`,
see also `SSet.Homotopy.congr_homologyMap` for the
variant using `SSet.Homotopy` as an assumption.
 -/
CategoryTheory.SimplicialObject.Homotopy.singularChainComplexFunctor_map_homology_eq_of_simplicialHomotopy : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasCoproducts C] {X Y : SSet} {f g : X ⟶ Y}
  [inst_3 : CategoryTheory.CategoryWithHomology C] (H : CategoryTheory.SimplicialObject.Homotopy f g) (R : C) (n : ℕ),
  SSet.homologyMap f R n = SSet.homologyMap g R n
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
IsSimpleRing.isSemisimpleRing_iff_isArtinianRing : ∀ {R : Type u} [inst : Ring R] [IsSimpleRing R], IsSemisimpleRing R ↔ IsArtinianRing R
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure.0.Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go.match_1.eq_1 : ∀ (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (motive : Std.Tactic.BVDecide.Return aig → Sort u_1)
  (aig_1 : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (exprRef : aig_1.Ref)
  (hexpr : aig.decls.size ≤ { aig := aig_1, ref := exprRef }.aig.decls.size)
  (cache : Std.Tactic.BVDecide.BVExpr.Cache (↑⟨{ aig := aig_1, ref := exprRef }, hexpr⟩).aig)
  (h_1 :
    (aig_2 : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) →
      (exprRef : aig_2.Ref) →
        (hexpr : aig.decls.size ≤ { aig := aig_2, ref := exprRef }.aig.decls.size) →
          (cache : Std.Tactic.BVDecide.BVExpr.Cache (↑⟨{ aig := aig_2, ref := exprRef }, hexpr⟩).aig) →
            motive { result := ⟨{ aig := aig_2, ref := exprRef }, hexpr⟩, cache := cache }),
  (match { result := ⟨{ aig := aig_1, ref := exprRef }, hexpr⟩, cache := cache } with
    | { result := ⟨{ aig := aig_2, ref := exprRef }, hexpr⟩, cache := cache } => h_1 aig_2 exprRef hexpr cache) =
    h_1 aig_1 exprRef hexpr cache
-- Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
CategoryTheory.SimplicialObject.isoCoskOfIsCoskeletal_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) (n : ℕ)
  [inst_1 :
    ∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
      (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F]
  [inst_2 : X.IsCoskeletal n], (X.isoCoskOfIsCoskeletal n).hom = (CategoryTheory.SimplicialObject.coskAdj n).unit.app X
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.dual_delete_contract : ∀ {α : Type u_1} (M : Matroid α) (X Y : Set α), ((M.delete X).contract Y)✶ = (M✶.contract X).delete Y
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (tries : Array (Lean.Meta.LazyDiscrTree.Trie α))
  (roots : Std.HashMap Lean.Meta.LazyDiscrTree.Key Lean.Meta.LazyDiscrTree.TrieIndex),
  sizeOf { tries := tries, roots := roots } = 1 + sizeOf tries + sizeOf roots
-- Mathlib.RingTheory.HahnSeries.Basic
/-- **Alias** of `HahnSeries.embDomain_of_notMem_range`. -/
HahnSeries.embDomain_notin_range : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : PartialOrder Γ']
  {f : Γ ↪o Γ'} {x : HahnSeries Γ R} {b : Γ'}, b ∉ Set.range ⇑f → (HahnSeries.embDomain f x).coeff b = 0
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- The basis of N.  -/
Module.Basis.SmithNormalForm.bN : {R : Type u_2} →
  [inst : CommRing R] →
    {M : Type u_3} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {N : Submodule R M} →
            {ι : Type u_4} → {n : ℕ} → Module.Basis.SmithNormalForm N ι n → Module.Basis (Fin n) R ↥N
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.isSemilinearSet_setOfFractNe : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι],
  IsSemilinearSet (IsProperLinearSet.setOfFractNe✝ hs)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.ordCompare_minKey!_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.TreeMap α β compare} [inst_2 : Inhabited α] {k : α}
  {f : β → β}, compare (t.modify k f).minKey! t.minKey! = Ordering.eq
-- Init.Data.List.TakeDrop
List.drop_cons : ∀ {α : Type u_1} {i : ℕ} {a : α} {l : List α}, 0 < i → List.drop i (a :: l) = List.drop (i - 1) l
-- Mathlib.Analysis.Normed.Lp.PiLp
instInhabitedPiLp : (p : ENNReal) → {ι : Type u_1} → (α : ι → Type u_2) → [(i : ι) → Inhabited (α i)] → Inhabited (PiLp p α)
-- Init.Data.List.Lemmas
List.foldr_assoc : ∀ {α : Type u_1} {op : α → α → α} [ha : Std.Associative op] {l : List α} {a₁ a₂ : α},
  List.foldr op (op a₁ a₂) l = op (List.foldr op a₁ l) a₂
-- Lean.Linter.Deprecated
Lean.Linter.DeprecationEntry.mk.injEq : ∀ (newName? : Option Lean.Name) (text? since? : Option String) (newName?_1 : Option Lean.Name)
  (text?_1 since?_1 : Option String),
  ({ newName? := newName?, text? := text?, since? := since? } =
      { newName? := newName?_1, text? := text?_1, since? := since?_1 }) =
    (newName? = newName?_1 ∧ text? = text?_1 ∧ since? = since?_1)
-- Mathlib.Order.Lattice
Prod.snd_sup : ∀ (α : Type u) (β : Type v) [inst : Max α] [inst_1 : Max β] (p q : α × β), (p ⊔ q).2 = p.2 ⊔ q.2
-- Mathlib.Analysis.ODE.Gronwall
gronwallBound_ε0 : ∀ (δ K x : ℝ), gronwallBound δ K 0 x = δ * Real.exp (K * x)
-- Mathlib.Algebra.Order.Group.Synonym
ofLex_div : ∀ {α : Type u_1} [inst : Div α] (a b : Lex α), ofLex (a / b) = ofLex a / ofLex b
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.unit_app_commShiftIso_hom_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) (A : Type u_3) [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] [inst_6 : G.CommShift A] [adj.CommShift A] (a : A)
  (X : C),
  CategoryTheory.CategoryStruct.comp (adj.unit.app ((CategoryTheory.shiftFunctor C a).obj X))
      ((CategoryTheory.Functor.commShiftIso (F.comp G) a).hom.app X) =
    (CategoryTheory.shiftFunctor C a).map (adj.unit.app X)
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.hom_hom_id : ∀ {X : FinPartOrd}, PartOrd.Hom.hom (CategoryTheory.CategoryStruct.id X).hom = OrderHom.id
-- Mathlib.Data.Finsupp.MonomialOrder
/-- the additive equivalence from `σ →₀ ℕ` to `syn`  -/
MonomialOrder.toSyn : {σ : Type u_1} → (self : MonomialOrder σ) → (σ →₀ ℕ) ≃+ self.syn
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.RecCallCache.rcc : Lean.Elab.WF.GuessLex.RecCallCache → Lean.Elab.WF.GuessLex.RecCallWithContext
-- Mathlib.Topology.Algebra.Group.Basic
Subgroup.le_topologicalClosure : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G] (s : Subgroup G),
  s ≤ s.topologicalClosure
-- Mathlib.Algebra.Category.ModuleCat.LeftResolution
/-- An `R`-module `M` can be functorially written as a quotient of a
projective `R`-module.  -/
ModuleCat.projectiveResolution : (R : Type u) → [inst : Ring R] → CategoryTheory.Abelian.LeftResolution (CategoryTheory.isProjective (ModuleCat R)).ι
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.instInhabited.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R],
  AddMonoidAlgebra.instInhabited = { default := AddMonoidAlgebra.coeffEquiv.symm.1 default }
-- Mathlib.Data.Int.Cast.Lemmas
/-- Two additive monoid homomorphisms `f`, `g` from `ℤ` to an additive monoid are equal
if `f 1 = g 1`.  -/
AddMonoidHom.ext_int : ∀ {A : Type u_5} [inst : AddMonoid A] {f g : ℤ →+ A}, f 1 = g 1 → f = g
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.below.mul_assoc : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R]
  {motive : (a a_1 : FreeAlgebra.Pre R X) → FreeAlgebra.Rel R X a a_1 → Prop} {a b c : FreeAlgebra.Pre R X},
  FreeAlgebra.Rel.below ⋯
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- The structural isomorphism between `d ⊙ᵣ 𝟙_ C` and `d`.  -/
CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso : {C : Type u_1} →
  {D : Type u_2} →
    {inst : CategoryTheory.Category.{v_1, u_1} C} →
      {inst_1 : CategoryTheory.Category.{v_2, u_2} D} →
        {inst_2 : CategoryTheory.MonoidalCategoryStruct C} →
          [self : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct C D] →
            (d : D) →
              CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d
                  (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅
                d
-- Mathlib.Control.Functor.Multivariate
LawfulMvFunctor.mk : ∀ {n : ℕ} {F : TypeVec.{u_2} n → Type u_1} [inst : MvFunctor F],
  (∀ {α : TypeVec.{u_2} n} (x : F α), MvFunctor.map TypeVec.id x = x) →
    (∀ {α β γ : TypeVec.{u_2} n} (g : α.Arrow β) (h : β.Arrow γ) (x : F α),
        MvFunctor.map (TypeVec.comp h g) x = MvFunctor.map h (MvFunctor.map g x)) →
      LawfulMvFunctor F
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.Equivalence.induced_inverse_map : ∀ {D : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} D] {T : Type u_2} (e : T ≃ D) {X Y : D} (f : X ⟶ Y),
  (CategoryTheory.Equivalence.induced e).inverse.map f =
    CategoryTheory.InducedCategory.homMk
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
        (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯)))
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.usize.inj : ∀ {val val_1 : UInt64}, Lean.Compiler.LCNF.LitValue.usize val = Lean.Compiler.LCNF.LitValue.usize val_1 → val = val_1
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.Hom.comm_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  {X X' : CategoryTheory.Abelian.SpectralObject C ι} (self : X.Hom X') (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i j k : ι}
  (f : i ⟶ j) (g : j ⟶ k) {Z : C} (h : (X'.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁)
      (CategoryTheory.CategoryStruct.comp ((self.hom n₁).app (CategoryTheory.ComposableArrows.mk₁ f)) h) =
    CategoryTheory.CategoryStruct.comp ((self.hom n₀).app (CategoryTheory.ComposableArrows.mk₁ g))
      (CategoryTheory.CategoryStruct.comp (X'.δ f g n₀ n₁ hn₁) h)
-- Mathlib.Analysis.Normed.Group.Basic
edist_eq_enorm_inv_mul : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a b : E), edist a b = ‖a⁻¹ * b‖ₑ
-- Mathlib.Analysis.Convex.Jensen
/-- Canonical form of the **strict Jensen's inequality**.  -/
StrictConcaveOn.lt_map_sum_iff_of_pos' : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  StrictConcaveOn 𝕜 s f →
    (∀ i ∈ t, 0 < w i) →
      ∑ i ∈ t, w i = 1 →
        (∀ i ∈ t, p i ∈ s) → (∑ i ∈ t, w i • f (p i) < f (∑ i ∈ t, w i • p i) ↔ ∃ j ∈ t, p j ≠ ∑ i ∈ t, w i • p i)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.card_le_of : ∀ {α : Type u} {n : ℕ}, (∀ (s : Finset α), s.card ≤ n) → Cardinal.mk α ≤ ↑n
-- Mathlib.AlgebraicGeometry.RelativeGluing
AlgebraicGeometry.Scheme.Cover.RelativeGluingData.mk.injEq : ∀ {S : AlgebraicGeometry.Scheme} {𝒰 : S.OpenCover} [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀]
  [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (functor : CategoryTheory.Functor 𝒰.I₀ AlgebraicGeometry.Scheme)
  (natTrans : functor ⟶ AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected 𝒰)
  (equifibered : CategoryTheory.NatTrans.Equifibered natTrans)
  (functor_1 : CategoryTheory.Functor 𝒰.I₀ AlgebraicGeometry.Scheme)
  (natTrans_1 : functor_1 ⟶ AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected 𝒰)
  (equifibered_1 : CategoryTheory.NatTrans.Equifibered natTrans_1),
  ({ functor := functor, natTrans := natTrans, equifibered := equifibered } =
      { functor := functor_1, natTrans := natTrans_1, equifibered := equifibered_1 }) =
    (functor = functor_1 ∧ natTrans ≍ natTrans_1)
-- Mathlib.MeasureTheory.PiSystem
subset_piiUnionInter : ∀ {α : Type u_3} {ι : Type u_4} {π : ι → Set (Set α)} {S : Set ι} {i : ι}, i ∈ S → π i ⊆ piiUnionInter π S
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.single_apply_ne : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : DecidableEq α] (p : ENNReal)
  (i : α) (a : E i) {j : α}, j ≠ i → ↑(lp.single p i a) j = 0
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- An `AddSubsemigroup` is closed under addition.  -/
AddSubsemigroup.add_mem : ∀ {M : Type u_1} [inst : Add M] (S : AddSubsemigroup M) {x y : M}, x ∈ S → y ∈ S → x + y ∈ S
-- Mathlib.Algebra.Order.Module.Defs
smul_le_smul_of_nonpos_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β] [PosSMulMono α β],
  b₁ ≤ b₂ → a ≤ 0 → a • b₂ ≤ a • b₁
-- Mathlib.Algebra.Algebra.Subalgebra.Pointwise
Subalgebra.instCovariantClassHSMulLe : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {R' : Type u_3}
  [inst_3 : Semiring R'] [inst_4 : MulSemiringAction R' A] [inst_5 : SMulCommClass R' R A],
  CovariantClass R' (Subalgebra R A) HSMul.hSMul LE.le
-- Mathlib.Logic.Equiv.PartialEquiv
Set.BijOn.toPartialEquiv_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Nonempty α] (f : α → β) (s : Set α) (t : Set β) (hf : Set.BijOn f s t),
  ↑(Set.BijOn.toPartialEquiv f s t hf) = f
-- Init.Data.Nat.Div.Basic
/-- Divisibility of natural numbers. `a ∣ b` (typed as `\|`) says that
there is some `c` such that `b = a * c`.
 -/
Nat.instDvd : Dvd ℕ
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.ofList_eq_empty_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)},
  Std.ExtHashMap.ofList l = ∅ ↔ l = []
-- Mathlib.Order.Filter.Pointwise
Filter.inv_mem_inv : ∀ {α : Type u_2} [inst : InvolutiveInv α] {f : Filter α} {s : Set α}, s ∈ f → s⁻¹ ∈ f⁻¹
-- Mathlib.NumberTheory.Modular
ModularGroup.g_eq_of_c_eq_one : ∀ {g : Matrix.SpecialLinearGroup (Fin 2) ℤ},
  ↑g 1 0 = 1 → g = ModularGroup.T ^ ↑g 0 0 * ModularGroup.S * ModularGroup.T ^ ↑g 1 1
-- Mathlib.Topology.Algebra.Group.Basic
Specializes.zsmul : ∀ {G : Type u_1} [inst : SubNegMonoid G] [inst_1 : TopologicalSpace G] [ContinuousAdd G] [ContinuousNeg G] {x y : G},
  x ⤳ y → ∀ (m : ℤ), (m • x) ⤳ (m • y)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_neg_add_right_singleton : ∀ {α : Type u_2} [inst : AddGroup α] {a b : α}, (fun x => -x + a) ⁻¹' {b} = {a - b}
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.colon_ι_app_π_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ Ψ : CategoryTheory.Abelian.Preradical C) (X : C),
  CategoryTheory.CategoryStruct.comp ((Φ.colon Ψ).ι.app X) (Φ.π.app X) =
    CategoryTheory.CategoryStruct.comp ((Φ.colonπ Ψ).app X) (Ψ.ι.app (Φ.quotient.obj X))
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.toFun_sub : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Sub β] (f g : UniformOnFun α β 𝔖),
  (UniformOnFun.toFun 𝔖) (f - g) = (UniformOnFun.toFun 𝔖) f - (UniformOnFun.toFun 𝔖) g