mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Presheaf.isLocallyInjective_comp_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] (J : CategoryTheory.GrothendieckTopology C)
  {F₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ D} (φ : F₁ ⟶ F₂) (ψ : F₂ ⟶ F₃)
  [CategoryTheory.Presheaf.IsLocallyInjective J ψ],
  CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.CategoryStruct.comp φ ψ) ↔
    CategoryTheory.Presheaf.IsLocallyInjective J φ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.μ_pullback_left_fst_fst' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X R Y Z : C} {f : R ⟶ X} (g₁ : Y ⟶ X) (g₂ : Z ⟶ X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left
        (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback f) (CategoryTheory.Over.mk g₁)
          (CategoryTheory.Over.mk g₂)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst g₁ g₂) g₁) f)
        (CategoryTheory.Limits.pullback.fst g₁ g₂)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst ((CategoryTheory.Over.pullback f).obj (CategoryTheory.Over.mk g₁)).hom
        ((CategoryTheory.Over.pullback f).obj (CategoryTheory.Over.mk g₂)).hom)
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Over.mk g₁).hom f)
-- Lean.Parser.Basic
Lean.Parser.unicodeSymbolFn : String → String → Lean.Parser.ParserFn
-- Mathlib.Control.Traversable.Equiv
Equiv.map.eq_1 : ∀ {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [inst : Functor t] {α β : Type u} (f : α → β) (x : t' α),
  Equiv.map eqv f x = (eqv β) (f <$> (eqv α).symm x)
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
_private.Mathlib.Probability.Kernel.IonescuTulcea.Traj.0.iterateInduction.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match 0 with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_1 ()
-- Mathlib.Data.Set.Finite.Lattice
/-- Dependent version of `Finite.biUnion`.  -/
Set.Finite.biUnion' : ∀ {α : Type u} {ι : Type u_1} {s : Set ι},
  s.Finite →
    ∀ {t : (i : ι) → i ∈ s → Set α}, (∀ (i : ι) (hi : i ∈ s), (t i hi).Finite) → (⋃ i, ⋃ (h : i ∈ s), t i h).Finite
-- Mathlib.CategoryTheory.Grothendieck
/-- The object in the fiber of the base object.  -/
CategoryTheory.Grothendieck.fiber : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} → (self : CategoryTheory.Grothendieck F) → ↑(F.obj self.base)
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateSubgroup.card_pow_le : ∀ {G : Type u_1} [inst : Group G] {K : ℝ} [inst_1 : DecidableEq G] {A : Finset G},
  IsApproximateSubgroup K ↑A → ∀ {n : ℕ}, ↑(A ^ n).card ≤ K ^ (n - 1) * ↑A.card
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.coe_id : ∀ {X : MonCat}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  [inst_1 : Inhabited (β k)] {f : Option (β k) → Option (β k)}, (m.alter k f).get! k = (f (m.get? k)).get!
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.isEmptyAlgEquiv_apply : ∀ (R : Type u) (σ : Type u_1) [inst : CommSemiring R] [inst_1 : IsEmpty σ] (a : AddMonoidAlgebra R (σ →₀ ℕ)),
  (MvPolynomial.isEmptyAlgEquiv R σ) a = a.coeff 0
-- Mathlib.Algebra.Order.Group.Cone
GroupCone.instSetLike : (G : Type u_1) → [inst : CommGroup G] → SetLike (GroupCone G) G
-- Mathlib.Algebra.Ring.IsFormallyReal
IsSumNonzeroSq.below.sq_add : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [inst_2 : Zero R] {motive : (a : R) → IsSumNonzeroSq a → Prop}
  {a s : R} (ha : a ≠ 0) (hs : IsSumNonzeroSq s), IsSumNonzeroSq.below hs → motive s hs → IsSumNonzeroSq.below ⋯
-- Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
FiniteField.trace_pow_card : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {K : Type u_2} [inst_2 : Field K] [inst_3 : Fintype K]
  (M : Matrix n n K), (M ^ Fintype.card K).trace = M.trace ^ Fintype.card K
-- Mathlib.Data.Set.NAry
Set.image_uncurry_prod : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α → β → γ) (s : Set α) (t : Set β),
  Function.uncurry f '' s ×ˢ t = Set.image2 f s t
-- Mathlib.Algebra.Category.ModuleCat.Topology.Homology
/-- Kernel in `TopModuleCat R` is the kernel of the linear map with the subspace topology.  -/
TopModuleCat.ker : {R : Type u} → [inst : Ring R] → [inst_1 : TopologicalSpace R] → {M N : TopModuleCat R} → (M ⟶ N) → TopModuleCat R
-- Mathlib.Data.ENat.BigOperators
ENat.sum_lt_sum_of_nonempty : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → ∀ {f g : α → ℕ∞}, (∀ i ∈ s, f i < g i) → ∑ i ∈ s, f i < ∑ i ∈ s, g i
-- Init.Data.Nat.Lemmas
Nat.lt_add_right_iff_pos : ∀ {n k : ℕ}, n < n + k ↔ 0 < k
-- Mathlib.Probability.Kernel.WithDensity
ProbabilityTheory.Kernel.lintegral_withDensity : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β → ENNReal}
  (κ : ProbabilityTheory.Kernel α β) [inst : ProbabilityTheory.IsSFiniteKernel κ],
  Measurable (Function.uncurry f) →
    ∀ (a : α) {g : β → ENNReal}, Measurable g → ∫⁻ (b : β), g b ∂(κ.withDensity f) a = ∫⁻ (b : β), f a b * g b ∂κ a
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.mul_apply' : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} {l : Type u_7} [inst : Fintype m] [inst_1 : Mul A]
  [inst_2 : AddCommMonoid A] {M : CStarMatrix l m A} {N : CStarMatrix m n A} {i : l} {k : n},
  (M * N) i k = (fun j => M i j) ⬝ᵥ fun j => N j k
-- Mathlib.Data.ZMod.Basic
ZMod.intCast_eq_one_iff_odd : ∀ {n : ℤ}, ↑n = 1 ↔ Odd n
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- The submodule of homogeneous `MvPolynomial`s of degree `n`.  -/
MvPolynomial.weightedHomogeneousSubmodule : (R : Type u_1) →
  {M : Type u_2} →
    [inst : CommSemiring R] → {σ : Type u_3} → [AddCommMonoid M] → (σ → M) → M → Submodule R (MvPolynomial σ R)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
PresheafOfModules.instPreservesFiniteLimitsSheafOfModulesSheafification : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  [inst_3 : J.WEqualsLocallyBijective AddCommGrpCat] [inst_4 : CategoryTheory.HasSheafify J AddCommGrpCat],
  CategoryTheory.Limits.PreservesFiniteLimits (PresheafOfModules.sheafification α)
-- Mathlib.Topology.Order.LeftRightLim
ContinuousWithinAt.leftLim_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace α]
  [OrderTopology α] [T2Space β] {f : α → β} {a : α}, ContinuousWithinAt f (Set.Iic a) a → Function.leftLim f a = f a
-- Mathlib.Analysis.InnerProductSpace.LinearMap
ContinuousLinearMap.toSesqForm_apply_coe : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {E' : Type u_4} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] (f : E →L[𝕜] E') (x : E'),
  (ContinuousLinearMap.toSesqForm f) x = (innerSL 𝕜) x ∘SL f
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.pushforward_map_app' : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (f : X ⟶ Y) {ℱ 𝒢 : TopCat.Presheaf C X}
  (α : ℱ ⟶ 𝒢) {U : (TopologicalSpace.Opens ↑Y)ᵒᵖ},
  ((TopCat.Presheaf.pushforward C f).map α).app U =
    α.app (Opposite.op ((TopologicalSpace.Opens.map f).obj (Opposite.unop U)))
-- Batteries.Data.Char.AsciiCasing
Char.isAlpha_toLower_eq_isAlpha : ∀ (c : Char), c.toLower.isAlpha = c.isAlpha
-- Mathlib.Data.Seq.Basic
Stream'.Seq1.ret_bind : ∀ {α : Type u} {β : Type v} (a : α) (f : α → Stream'.Seq1 β), (Stream'.Seq1.ret a).bind f = f a
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- Formula for `hurwitzZetaOdd` as a Dirichlet series in the convergence range, with sum over `ℕ`
(version without absolute values, assuming `a ∈ Icc 0 1`)  -/
HurwitzZeta.hasSum_nat_hurwitzZetaOdd_of_mem_Icc : ∀ {a : ℝ},
  a ∈ Set.Icc 0 1 →
    ∀ {s : ℂ},
      1 < s.re → HasSum (fun n => (1 / (↑n + ↑a) ^ s - 1 / (↑n + 1 - ↑a) ^ s) / 2) (HurwitzZeta.hurwitzZetaOdd (↑a) s)
-- Mathlib.Logic.Equiv.Prod
Equiv.prodCongrRight_symm : ∀ {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂),
  (Equiv.prodCongrRight e).symm = Equiv.prodCongrRight (Equiv.symm ∘ e)
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_add : ∀ {r p : ℝ}, 0 ≤ r → 0 ≤ p → (r + p).toNNReal = r.toNNReal + p.toNNReal
-- Init.Data.String.Search
/-- Constructs a new string obtained by replacing all occurrences of `pattern` with
`replacement` in `s`.

This function is generic over all currently supported patterns. The replacement may be a
`String` or a `String.Slice`.

Examples:

* `"red green blue".replace 'e' "" = "rd grn blu"`

* `"red green blue".replace (fun c => c == 'u' || c == 'e') "" = "rd grn bl"`

* `"red green blue".replace "e" "" = "rd grn blu"`

* `"red green blue".replace "ee" "E" = "red grEn blue"`

* `"red green blue".replace "e" "E" = "rEd grEEn bluE"`

* `"aaaaa".replace "aa" "b" = "bba"`

* `"abc".replace "" "k" = "kakbkck"`
 -/
String.replace : {ρ : Type} →
  {σ : String.Slice → Type} →
    [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] →
        {α : Type u_1} →
          [String.ToSlice α] → String → (pattern : ρ) → [String.Slice.Pattern.ToForwardSearcher pattern σ] → α → String
-- Mathlib.Algebra.Algebra.Prod
/-- First projection as `AlgHom`.  -/
AlgHom.fst : (R : Type u_1) →
  (A : Type u_2) →
    (B : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] → [inst_2 : Algebra R A] → [inst_3 : Semiring B] → [inst_4 : Algebra R B] → A × B →ₐ[R] A
-- Mathlib.Data.List.GetD
List.getD_append_right : ∀ {α : Type u} (l l' : List α) (d : α) (n : ℕ), l.length ≤ n → (l ++ l').getD n d = l'.getD (n - l.length) d
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_op_zero : ∀ {α : Type u_2} [inst : Zero α], AddOpposite.op '' 0 = 0
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.zeta_apply_ne : ∀ {x : ℕ}, x ≠ 0 → ArithmeticFunction.zeta x = 1
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coe_natCast : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (n : ℕ), ↑↑n = ↑n
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
/-- The function defined by `f : ContDiffBump c`. Use automatic coercion to
function instead.  -/
ContDiffBump.toFun : {E : Type u_1} →
  [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℝ E] → [HasContDiffBump E] → {c : E} → ContDiffBump c → E → ℝ
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_le_inf : ∀ {G : Type u_1} [inst : Group G] (H₁ H₂ : Subgroup G) [H₁.Normal] [H₂.Normal], ⁅H₁, H₂⁆ ≤ H₁ ⊓ H₂
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.zero : {α : Type u_1} → [inst : Zero α] → [inst_1 : Preorder α] → Zero { x // 0 ≤ x }
-- Lean.Elab.Tactic.Omega.OmegaM
/-- Return the `Expr` representing the list of atoms.  -/
Lean.Elab.Tactic.Omega.atomsList : Lean.Elab.Tactic.Omega.OmegaM Lean.Expr
-- Mathlib.CategoryTheory.Galois.Equivalence
CategoryTheory.PreGaloisCategory.instFullContActionFintypeCatFunObjFiniteAutFunctorFunctorToContAction : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F],
  (CategoryTheory.PreGaloisCategory.functorToContAction F).Full
-- Mathlib.Algebra.Group.Graph
AddMonoidHom.mem_mgraph : ∀ {G : Type u_1} {H : Type u_2} [inst : AddMonoid G] [inst_1 : AddMonoid H] {f : G →+ H} {x : G × H},
  x ∈ f.mgraph ↔ f x.1 = x.2
-- Mathlib.Algebra.Order.Module.Defs
SMulPosReflectLE.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero β],
  (∀ ⦃b : β⦄, 0 < b → ∀ ⦃a₁ a₂ : α⦄, a₁ • b ≤ a₂ • b → a₁ ≤ a₂) → SMulPosReflectLE α β
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.continuous_map : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {f : α → β},
  Continuous (UniformSpace.Completion.map f)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.beq'_eq : ∀ (p₁ p₂ : Int.Internal.Linear.Poly), (p₁.beq' p₂ = true) = (p₁ = p₂)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.domExtend_invFun : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  {s : Set B} (e : Bundle.Pretrivialization F fun z => proj ↑z) [inst_2 : Nonempty (Z → F)] (x : B × F),
  e.domExtend.invFun x = ↑(e.invFun x)
-- Mathlib.Data.Set.Enumerate
_private.Mathlib.Data.Set.Enumerate.0.Set.enumerate.match_1.eq_2 : ∀ {α : Type u_1} (motive : Set α → ℕ → Sort u_2) (s : Set α) (n : ℕ) (h_1 : (s : Set α) → motive s 0)
  (h_2 : (s : Set α) → (n : ℕ) → motive s n.succ),
  (match s, n.succ with
    | s, 0 => h_1 s
    | s, n.succ => h_2 s n) =
    h_2 s n
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.isoMk_inv_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S}
  (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j))
  (h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k))
  (w₀ :
    autoParam (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i)
      CategoryTheory.PreOneHypercover.isoMk._auto_1)
  (w₁₁ :
    autoParam
      (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k).hom (F.p₁ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₁ k) (h₀ i).hom)
      CategoryTheory.PreOneHypercover.isoMk._auto_3)
  (w₁₂ :
    autoParam
      (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k).hom (F.p₂ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₂ k) (h₀ j).hom)
      CategoryTheory.PreOneHypercover.isoMk._auto_5)
  (i : F.I₀),
  (CategoryTheory.PreOneHypercover.isoMk s₀ h₀ s₁ h₁ w₀ w₁₁ w₁₂).inv.h₀ i =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (h₀ (s₀.symm i)).inv
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiableWithinAt_one : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {x : E} {s : Set E} [inst_7 : One F], DifferentiableWithinAt 𝕜 1 s x
-- Mathlib.Order.SuccPred.Basic
Order.pred_eq_iff_isMin : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] {a : α}, Order.pred a = a ↔ IsMin a
-- Init.Prelude
decide_eq_false : ∀ {p : Prop} [inst : Decidable p], ¬p → decide p = false
-- Mathlib.Order.Filter.Basic
Filter.instTransSetMem_1 : {α : Type u} → Trans Membership.mem (fun x1 x2 => x1 ⊆ x2) Membership.mem
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.instEpiFRestrictionToTruncGE' : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  (i : ι), CategoryTheory.Epi ((K.restrictionToTruncGE' e).f i)
-- Mathlib.Topology.EMetricSpace.Basic
/-- A variation around the emetric characterization of Cauchy sequences  -/
EMetric.cauchySeq_iff' : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [Nonempty β] [inst_2 : SemilatticeSup β] {u : β → α},
  CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (u n) (u N) < ε
-- Mathlib.Algebra.Homology.FullSubcategory
HomologicalComplex.liftObjectProperty_d : ∀ {ι : Type u_1} {c : ComplexShape ι} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V]
  [inst_1 : CategoryTheory.Preadditive V] (P : CategoryTheory.ObjectProperty V) (K : HomologicalComplex V c)
  (hK : ∀ (n : ι), P (K.X n)) (i j : ι),
  (HomologicalComplex.liftObjectProperty P K hK).d i j = CategoryTheory.ObjectProperty.homMk (K.d i j)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.commTensorRight_inv_app : ∀ {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) [inst_4 : F.Monoidal] (X X_1 : C),
  (CategoryTheory.Functor.Monoidal.commTensorRight F X).inv.app X_1 = CategoryTheory.Functor.OplaxMonoidal.δ F X_1 X
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  (t : CategoryTheory.Limits.PushoutCocone f g) {Z_1 : C} (h : t.pt ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp t.inl h) =
    CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp t.inr h)
-- Init.Data.UInt.Lemmas
UInt32.div_one : ∀ {a : UInt32}, a / 1 = a
-- Init.Data.Int.Basic
instNatCastInt : NatCast ℤ
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.p_comp_opcyclesIso_inv_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) [inst_2 : S.HasRightHomology] {Z : C}
  (h_1 : S.opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.p (CategoryTheory.CategoryStruct.comp h.opcyclesIso.inv h_1) =
    CategoryTheory.CategoryStruct.comp S.pOpcycles h_1
-- Mathlib.Topology.Algebra.ProperConstSMul
instProperConstVAddOfContinuousConstVAddOfT2SpaceOfCompactSpace : ∀ {M : Type u_1} {X : Type u_2} [inst : VAdd M X] [inst_1 : TopologicalSpace X] [ContinuousConstVAdd M X] [T2Space X]
  [CompactSpace X], ProperConstVAdd M X
-- Init.Prelude
/-- The implementation of the `<*>` operator.

In a monad, `mf <*> mx` is the same as `do let f ← mf; x ← mx; pure (f x)`: it evaluates the
function first, then the argument, and applies one to the other.

To avoid surprising evaluation semantics, `mx` is taken "lazily", using a `Unit → f α` function.


Conventions for notations in identifiers:

 * The recommended spelling of `<*>` in identifiers is `seq`. -/
Seq.seq : {f : Type u → Type v} → [self : Seq f] → {α β : Type u} → f (α → β) → (Unit → f α) → f β
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- The inf of two subgroups is their intersection.  -/
Subgroup.instMin : {G : Type u_1} → [inst : Group G] → Min (Subgroup G)
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The Monge point of a simplex (in 2 or more dimensions) is a
generalization of the orthocenter of a triangle.  It is defined to be
the intersection of the Monge planes, where a Monge plane is the
(n-1)-dimensional affine subspace of the subspace spanned by the
simplex that passes through the centroid of an (n-2)-dimensional face
and is orthogonal to the opposite edge (in 2 dimensions, this is the
same as an altitude).  The circumcenter O, centroid G and Monge point
M are collinear in that order on the Euler line, with OG : GM = (n-1): 2.
Here, we use that ratio to define the Monge point (so resulting
in a point that equals the centroid in 0 or 1 dimensions), and then
show in subsequent lemmas that the point so defined lies in the Monge
planes and is their unique point of intersection.  -/
Affine.Simplex.mongePoint : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] → [inst_3 : NormedAddTorsor V P] → {n : ℕ} → Affine.Simplex ℝ P n → P
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.le_op_iff : ∀ {G : Type u_2} [inst : Group G] {S₁ : Subgroup Gᵐᵒᵖ} {S₂ : Subgroup G}, S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.fintypeWalkingPair : Fintype CategoryTheory.Limits.WalkingPair
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTreeTarget : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → ℕ → Type
-- Mathlib.CategoryTheory.Bicategory.SingleObj
CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence_inverse_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C),
  (CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence C).inverse.obj X = X
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_eq_top_iff : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a : M},
  ArchimedeanClass.mk a = ⊤ ↔ a = 0
-- Mathlib.Algebra.Order.Ring.Archimedean
Rat.castHom.congr_simp : ∀ (α : Type u_3) [inst : DivisionRing α] [inst_1 : CharZero α], Rat.castHom α = Rat.castHom α
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.add_eq_eq : ∀ {α : Type u_1} {a₁ a₂ b₁ b₂ : α} [inst : Add α], a₁ = b₁ → a₂ = b₂ → a₁ + a₂ = b₁ + b₂
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.invertible_mk'_one_invOf : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (s : ↥M), ⅟(IsLocalization.mk' S 1 s) = (algebraMap R S) ↑s
-- Mathlib.Geometry.Euclidean.Sphere.SecondInter
/-- The point given by `secondInter` equals the original point if and only if the line is
orthogonal to the radius vector.  -/
EuclideanGeometry.Sphere.secondInter_eq_self_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p : P} {v : V},
  s.secondInter p v = p ↔ inner ℝ v (p -ᵥ s.center) = 0
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.contains.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashSet α), m = m_1 → ∀ (a a_1 : α), a = a_1 → m.contains a = m_1.contains a_1
-- Mathlib.Data.Fin.Tuple.Take
/-- Take the first `m` elements of an `n`-tuple where `m ≤ n`, returning an `m`-tuple.  -/
Fin.take : {n : ℕ} → {α : Fin n → Sort u_1} → (m : ℕ) → (h : m ≤ n) → ((i : Fin n) → α i) → (i : Fin m) → α (Fin.castLE h i)
-- Init.Data.SInt.Lemmas
Int8.ofInt_int32ToInt : ∀ (x : Int32), Int8.ofInt x.toInt = x.toInt8
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.ExplorationStep.lt.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α → Ordering} [inst_1 : SizeOf α] [inst_2 : (a : α) → SizeOf (β a)]
  (a : α) (a_1 : k a = Ordering.lt) (a_2 : β a) (a_3 : List ((a : α) × β a)),
  sizeOf (Std.DTreeMap.Internal.Impl.ExplorationStep.lt a a_1 a_2 a_3) =
    1 + sizeOf a + sizeOf a_1 + sizeOf a_2 + sizeOf a_3
-- Mathlib.Order.Minimal
OrderIso.image_setOfPred_minimal : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) (P : α → Prop),
  ⇑f '' {x | Minimal P x} = {x | Minimal (fun x => P (f.symm x)) x}
-- Mathlib.Topology.LocallyConstant.Algebra
/-- The constant-function embedding, as a multiplicative monoid hom.  -/
LocallyConstant.constMonoidHom : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : MulOneClass Y] → Y →* LocallyConstant X Y
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netEntropyEntourage_nonneg : ∀ {X : Type u_1} {F : Set X} (T : X → X), F.Nonempty → ∀ (U : SetRel X X), 0 ≤ Dynamics.netEntropyEntourage T F U