mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.valMinAbs_inj : ∀ {n : ℕ} {a b : ZMod n}, a.valMinAbs = b.valMinAbs ↔ a = b
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.comp_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z),
  (CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk z₁).comp
      (CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk z₂) =
    z₁.comp z₂
-- Init.Data.Vector.Lemmas
/-- Variant of `any_eq_true` in terms of membership rather than an array index.  -/
Vector.any_eq_true' : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Vector α n}, xs.any p = true ↔ ∃ x ∈ xs, p x = true
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.equiv_iff : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] (G : ι → Type w) [inst_1 : (i : ι) → L.Structure (G i)]
  (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [inst_2 : IsDirectedOrder ι]
  [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] {x y : FirstOrder.Language.Structure.Sigma f} {i : ι}
  (hx : x.fst ≤ i) (hy : y.fst ≤ i), x ≈ y ↔ (f x.fst i hx) x.snd = (f y.fst i hy) y.snd
-- Lean.Meta.SizeOf
/-- Construct proof of auxiliary lemma. See `mkSizeOfAuxLemma`  -/
_private.Lean.Meta.SizeOf.0.Lean.Meta.SizeOfSpecNested.mkSizeOfAuxLemmaProof : Lean.InductiveVal → Lean.Expr → Lean.Meta.SizeOfSpecNested.M Lean.Expr
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
ChartedSpace.LiftProp.eq_1 : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] (P : (H → H') → Set H → H → Prop) (f : M → M'),
  ChartedSpace.LiftProp P f = ∀ (x : M), ChartedSpace.LiftPropAt P f x
-- Init.Data.Slice.List.Lemmas
List.toArray_mkSlice_roo : ∀ {α : Type u_1} {xs : List α} {lo hi : ℕ},
  Std.Slice.toArray (Std.Roo.Sliceable.mkSlice xs lo<...hi) = (List.drop (lo + 1) (List.take hi xs)).toArray
-- Mathlib.Algebra.Group.Defs
/-- Zero is a right neutral element for addition  -/
AddMonoid.add_zero : ∀ {M : Type u} [self : AddMonoid M] (a : M), a + 0 = a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.instIsAddMonHomAddOfIsCommAddMonObj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M : C} [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.BraidedCategory C]
  [CategoryTheory.IsCommAddMonObj M], CategoryTheory.IsAddMonHom CategoryTheory.AddMonObj.add
-- Mathlib.Algebra.Group.Action.Hom
AddMonoidHom.vaddZeroHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : AddMonoid M] [inst_1 : AddZeroClass N] [inst_2 : AddAction M N]
  [inst_3 : VAddAssocClass M N N],
  AddMonoidHom.vaddZeroHom = { toFun := fun x => x +ᵥ 0, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.symm_trans_cancel_right : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [inst_6 : RingHomInvPair σ₁₃ σ₃₁]
  [inst_7 : RingHomInvPair σ₃₁ σ₁₃] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃}
  [inst_8 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_9 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
  [inst_10 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃] [inst_11 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] (e : M₁ ≃ₛₗ[σ₁₂] M₂)
  (f : M₃ ≃ₛₗ[σ₃₂] M₂), (f.trans e.symm).trans e = f
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.hasCompactSupport : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
  (f : ContDiffBump c) [FiniteDimensional ℝ E], HasCompactSupport ↑f
-- Mathlib.Data.Nat.Init
/-- Recursion starting at a non-zero number: given a map `C k → C (k+1)` for each `k ≥ n`,
there is a map from `C n` to each `C m`, `n ≤ m`.

This is a version of `Nat.le.rec` that works for `Sort u`.
Similarly to `Nat.le.rec`, it can be used as
```
induction hle using Nat.leRec with
| refl => sorry
| le_succ_of_le hle ih => sorry
```
 -/
Nat.leRec : {n : ℕ} →
  {motive : (m : ℕ) → n ≤ m → Sort u_1} →
    motive n ⋯ → (⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯) → {m : ℕ} → (h : n ≤ m) → motive m h
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Lex.isStrictOrder : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : LinearOrder ι]
  [inst_2 : (i : ι) → PartialOrder (α i)], IsStrictOrder (Lex (Π₀ (i : ι), α i)) fun x1 x2 => x1 < x2
-- Std.Data.Internal.List.Associative
/-- This is a restatement of `containsKey_insertEntryIfNew` that is written to exactly match the proof
obligation in the statement of `getValueCast_insertEntryIfNew`.
 -/
Std.Internal.List.containsKey_of_containsKey_insertEntryIfNew' : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  Std.Internal.List.containsKey a (Std.Internal.List.insertEntryIfNew k v l) = true →
    ¬((k == a) = true ∧ Std.Internal.List.containsKey k l = false) → Std.Internal.List.containsKey a l = true
-- Batteries.Recycling.RBTree.Lemmas
/-- The value `x` returned by `upperBound?` is greater or equal to the `cut`.  -/
RBTree.RBNode.upperBound?_ge' : ∀ {α : Type u_1} {ub : Option α} {cut : α → Ordering} {x : α} {t : RBTree.RBNode α},
  (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → RBTree.RBNode.upperBound? cut t ub = some x → cut x ≠ Ordering.gt
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.mk.inj : ∀ {α : Type u_1} {inst : Fintype α} {inst_1 : Nonempty α} {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} {n₀ : ℕ}
  {n₀_gt_zero : 0 < n₀} {a_pos : ∀ (i : α), 0 < a i} {b_pos : ∀ (i : α), 0 < b i} {b_lt_one : ∀ (i : α), b i < 1}
  {g_nonneg : ∀ x ≥ 0, 0 ≤ g x} {g_grows_poly : AkraBazziRecurrence.GrowsPolynomially g}
  {h_rec : ∀ (n : ℕ), n₀ ≤ n → T n = ∑ i, a i * T (r i n) + g ↑n} {T_gt_zero' : ∀ n < n₀, 0 < T n}
  {r_lt_n : ∀ (i : α) (n : ℕ), n₀ ≤ n → r i n < n}
  {dist_r_b : ∀ (i : α), (fun n => ↑(r i n) - b i * ↑n) =o[Filter.atTop] fun n => ↑n / Real.log ↑n ^ 2} {n₀_1 : ℕ}
  {n₀_gt_zero_1 : 0 < n₀_1} {a_pos_1 : ∀ (i : α), 0 < a i} {b_pos_1 : ∀ (i : α), 0 < b i}
  {b_lt_one_1 : ∀ (i : α), b i < 1} {g_nonneg_1 : ∀ x ≥ 0, 0 ≤ g x}
  {g_grows_poly_1 : AkraBazziRecurrence.GrowsPolynomially g}
  {h_rec_1 : ∀ (n : ℕ), n₀_1 ≤ n → T n = ∑ i, a i * T (r i n) + g ↑n} {T_gt_zero'_1 : ∀ n < n₀_1, 0 < T n}
  {r_lt_n_1 : ∀ (i : α) (n : ℕ), n₀_1 ≤ n → r i n < n}
  {dist_r_b_1 : ∀ (i : α), (fun n => ↑(r i n) - b i * ↑n) =o[Filter.atTop] fun n => ↑n / Real.log ↑n ^ 2},
  { n₀ := n₀, n₀_gt_zero := n₀_gt_zero, a_pos := a_pos, b_pos := b_pos, b_lt_one := b_lt_one, g_nonneg := g_nonneg,
        g_grows_poly := g_grows_poly, h_rec := h_rec, T_gt_zero' := T_gt_zero', r_lt_n := r_lt_n,
        dist_r_b := dist_r_b } =
      { n₀ := n₀_1, n₀_gt_zero := n₀_gt_zero_1, a_pos := a_pos_1, b_pos := b_pos_1, b_lt_one := b_lt_one_1,
        g_nonneg := g_nonneg_1, g_grows_poly := g_grows_poly_1, h_rec := h_rec_1, T_gt_zero' := T_gt_zero'_1,
        r_lt_n := r_lt_n_1, dist_r_b := dist_r_b_1 } →
    n₀ = n₀_1
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a colimit for `F.leftOp : Jᵒᵖ ⥤ C` into a limit for `F : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.isLimitOfCoconeLeftOpOfCone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor J Cᵒᵖ) →
          {c : CategoryTheory.Limits.Cone F} →
            CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeLeftOpOfCone c) →
              CategoryTheory.Limits.IsLimit c
-- Init.Data.String.Lemmas.Order
String.Pos.ofSliceTo_lt_iff : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos},
  String.Pos.ofSliceTo p < q ↔ ∀ (h : q ≤ p₀), p < p₀.sliceTo q h
-- Mathlib.Analysis.Normed.Group.Continuity
SeminormedGroup.toContinuousENorm : {E : Type u_4} → [inst : SeminormedGroup E] → ContinuousENorm E
-- Mathlib.Analysis.Convex.Strict
IsOpen.strictConvex_iff : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCommMonoid E] [inst_4 : Module 𝕜 E] {s : Set E}, IsOpen s → (StrictConvex 𝕜 s ↔ Convex 𝕜 s)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- The isomorphism `X ×[Z] Y ≅ Y ×[Z] X`.  -/
CategoryTheory.Limits.pullbackSymmetry : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          [inst_1 : CategoryTheory.Limits.HasPullback f g] →
            CategoryTheory.Limits.pullback f g ≅ CategoryTheory.Limits.pullback g f
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.instBooleanAlgebra : {α : Type u_2} → [inst : TopologicalSpace α] → BooleanAlgebra (TopologicalSpace.Clopens α)
-- Mathlib.Algebra.Ring.Defs
NonAssocSemiring.toAddCommMonoidWithOne : {α : Type u} → [self : NonAssocSemiring α] → AddCommMonoidWithOne α
-- Mathlib.Tactic.NormNum.LegendreSymbol
Mathlib.Meta.NormNum.jacobiSymNat.zero_left : ∀ (b : ℕ), (b / 2).beq 0 = false → Mathlib.Meta.NormNum.jacobiSymNat 0 b = 0
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.mk : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {r : HomRel C} → C → CategoryTheory.Quotient r
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.norm_nonarchimedean : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (f g : PadicSeq p), (f + g).norm ≤ max f.norm g.norm
-- Aesop.Rule
Aesop.instOrdNormRuleInfo : Ord Aesop.NormRuleInfo
-- Mathlib.Analysis.Real.Sqrt
Real.isSquare_iff : ∀ {x : ℝ}, IsSquare x ↔ 0 ≤ x
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.up'_mk : ∀ {α : Type u_2} [inst : Add α] [inst_1 : IsRightCancelAdd α] (a i j : α), i + a = j → (ComplexShape.up' a).Rel i j
-- Mathlib.Algebra.Order.Group.Indicator
Set.one_le_mulIndicator : ∀ {α : Type u_2} {M : Type u_3} [inst : Preorder M] [inst_1 : One M] {s : Set α} {f : α → M},
  (∀ a ∈ s, 1 ≤ f a) → ∀ (a : α), 1 ≤ s.mulIndicator f a
-- Mathlib.Topology.MetricSpace.Closeds
TopologicalSpace.NonemptyCompacts.lipschitz_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : EMetricSpace α] [inst_1 : EMetricSpace β], LipschitzWith 1 fun p => p.1 ×ˢ p.2
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.liftOfLE.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M₁ : Type u_6}
  {M₂ : Type u_7} [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R M₁] [inst_6 : Module R M₂]
  (S₁ S₂ : Submonoid R) (h : S₁ ≤ S₂) (f₁ : M →ₗ[R] M₁) (f₂ : M →ₗ[R] M₂) [inst_7 : IsLocalizedModule S₁ f₁]
  [inst_8 : IsLocalizedModule S₂ f₂], IsLocalizedModule.liftOfLE S₁ S₂ h f₁ f₂ = IsLocalizedModule.lift S₁ f₁ f₂ ⋯
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- The image of a non-unital subsemiring along a ring homomorphism is a non-unital subsemiring.  -/
NonUnitalSubsemiring.map : {R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring S] →
        {F : Type u_1} →
          [inst_2 : FunLike F R S] → [NonUnitalRingHomClass F R S] → F → NonUnitalSubsemiring R → NonUnitalSubsemiring S
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.FriendlyOperationClass.friend : ∀ {α : Type u_1} {γ : Type u_3} {F : γ → Stream'.Seq α → Stream'.Seq α}
  [self : Tactic.ComputeAsymptotics.Seq.FriendlyOperationClass F] (c : γ),
  Tactic.ComputeAsymptotics.Seq.FriendlyOperation (F c)
-- Mathlib.Topology.Maps.Basic
Topology.IsClosedEmbedding.id : ∀ {X : Type u_1} [inst : TopologicalSpace X], Topology.IsClosedEmbedding id
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.fromCostructuredArrow_ι_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor C D) {X : D}
  (G : CategoryTheory.Functor J (CategoryTheory.CostructuredArrow F X)) (j : J),
  (CategoryTheory.Limits.Cocone.fromCostructuredArrow F G).ι.app j = (G.obj j).hom
-- Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
/-- The ring `ℤ` has finite quotients.  -/
Ring.HasFiniteQuotients.instInt : Ring.HasFiniteQuotients ℤ
-- Mathlib.Analysis.Analytic.Composition
/-- Auxiliary lemma to prove that the composition of formal multilinear series is associative.

Consider a composition `a` of `n` and a composition `b` of `a.length`. Grouping together some
blocks of `a` according to `b` as in `a.gather b`, one can compute the total size of the blocks
of `a` up to an index `sizeUpTo b i + j` (where the `j` corresponds to a set of blocks of `a`
that do not fill a whole block of `a.gather b`). The first part corresponds to a sum of blocks
in `a.gather b`, and the second one to a sum of blocks in the next block of
`sigmaCompositionAux a b`. This is the content of this lemma.  -/
Composition.sizeUpTo_sizeUpTo_add : ∀ {n : ℕ} (a : Composition n) (b : Composition a.length) {i j : ℕ} (hi : i < b.length),
  j < b.blocksFun ⟨i, hi⟩ →
    a.sizeUpTo (b.sizeUpTo i + j) = (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo j
-- Std.Net.Addr
Std.Net.instInhabitedSocketAddressV4 : Inhabited Std.Net.SocketAddressV4
-- Mathlib.Data.Set.Card
Set.encard_congr : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (e : ↑s ≃ ↑t), s.encard = t.encard
-- Mathlib.Topology.Separation.CompletelyRegular
separatesPoints_continuous_of_t35Space : ∀ {X : Type u} [inst : TopologicalSpace X] [T35Space X], {f | Continuous f}.SeparatesPoints
-- Mathlib.Combinatorics.Matroid.Map
Matroid.restrictSubtype_inter_indep_iff : ∀ {α : Type u_1} {X I : Set α} {M : Matroid α}, (M.restrictSubtype X).Indep (Subtype.val ⁻¹' I) ↔ M.Indep (X ∩ I)
-- Aesop.Stats.Basic
Aesop.Stats.scriptGenerated : Aesop.Stats → Option Aesop.ScriptGenerated
-- Mathlib.Data.Fin.Tuple.Curry
/-- Uncurry all the arguments of `Function.OfArity α n` to get a function from a tuple.

Note this can be used on raw functions if used.  -/
Function.OfArity.uncurry : {α β : Type u} → {n : ℕ} → Function.OfArity α β n → (Fin n → α) → β
-- Mathlib.Data.Sym.Sym2
Sym2.instSetLike : {α : Type u_1} → SetLike (Sym2 α) α
-- Mathlib.Order.Preorder.Finsupp
Finsupp.semilatticeSup : {ι : Type u_1} → {M : Type u_2} → [inst : Zero M] → [SemilatticeSup M] → SemilatticeSup (ι →₀ M)
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- For an `R`-algebra homomorphism `f : S →ₐ[R] P` and prime ideals `I = f⁻¹(J)`, the induced
`R`-algebra homomorphism from the localization of `S` at `I` to the localization of `P` at `J`.

See `localAlgHom'` for a variant where the base ring `R` is also localized.  -/
Localization.localAlgHom : {R : Type u_1} →
  [inst : CommSemiring R] →
    {S : Type u_2} →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          {P : Type u_3} →
            [inst_3 : CommSemiring P] →
              [inst_4 : Algebra R P] →
                (I : Ideal S) →
                  [inst_5 : I.IsPrime] →
                    (J : Ideal P) →
                      [inst_6 : J.IsPrime] →
                        (f : S →ₐ[R] P) → I = Ideal.comap f J → Localization.AtPrime I →ₐ[R] Localization.AtPrime J
-- Mathlib.RingTheory.Coprime.Lemmas
IsRelPrime.pow_left : ∀ {α : Type u_1} [inst : CommMonoid α] [DecompositionMonoid α] {x y : α} {m : ℕ}, IsRelPrime x y → IsRelPrime (x ^ m) y
-- Mathlib.CategoryTheory.Localization.Triangulated
CategoryTheory.Triangulated.Localization.instIsTriangulatedLocalization' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (W : CategoryTheory.MorphismProperty C) [inst_6 : W.HasLeftCalculusOfFractions]
  [inst_7 : W.IsCompatibleWithTriangulation] [inst_8 : W.HasLocalization] [CategoryTheory.IsTriangulated C],
  CategoryTheory.IsTriangulated W.Localization'
-- Mathlib.Algebra.Category.Grp.Zero
GrpCat.isZero_iff_subsingleton : ∀ {G : GrpCat}, CategoryTheory.Limits.IsZero G ↔ Subsingleton ↑G
-- Init.Data.UInt.Bitwise
UInt64.and_zero : ∀ {a : UInt64}, a &&& 0 = 0
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- In the characteristic zero case, the weights in the centroid
indexed by a `Fintype` sum to 1 if the number of points is `n + 1`.  -/
Finset.sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one : ∀ (k : Type u_1) [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι) [CharZero k] [inst_2 : Fintype ι] {n : ℕ},
  s.card = n + 1 → ∑ i, Finset.centroidWeightsIndicator k s i = 1
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mk'_mul_mk' : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_6} {M' : Type u_7} [inst_1 : Semiring M]
  [inst_2 : Semiring M'] [inst_3 : Algebra R M] [inst_4 : Algebra R M'] (f : M →ₐ[R] M')
  [inst_5 : IsLocalizedModule S f.toLinearMap] (m₁ m₂ : M) (s₁ s₂ : ↥S),
  IsLocalizedModule.mk' f.toLinearMap m₁ s₁ * IsLocalizedModule.mk' f.toLinearMap m₂ s₂ =
    IsLocalizedModule.mk' f.toLinearMap (m₁ * m₂) (s₁ * s₂)
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.coe_genWeightSpaceOf_zero : ∀ {R : Type u_2} {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (x : L),
  ↑(LieModule.genWeightSpaceOf M 0 x) = ⨆ k, ((LieModule.toEnd R L M) x ^ k).ker
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.mk : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_5} →
      {P : Type u_10} →
        {P₂ : Type u_11} →
          [inst : NormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup V] →
              [inst_2 : NormedSpace 𝕜 V] →
                [inst_3 : PseudoMetricSpace P] →
                  [inst_4 : NormedAddTorsor V P] →
                    [inst_5 : SeminormedAddCommGroup V₂] →
                      [inst_6 : NormedSpace 𝕜 V₂] →
                        [inst_7 : PseudoMetricSpace P₂] →
                          [inst_8 : NormedAddTorsor V₂ P₂] →
                            (toAffineEquiv : P ≃ᵃ[𝕜] P₂) → (∀ (x : V), ‖toAffineEquiv.linear x‖ = ‖x‖) → P ≃ᵃⁱ[𝕜] P₂
-- Mathlib.Probability.Moments.CovarianceBilinDual
StrongDual.toLp_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} {p : ENNReal}
  {𝕜 : Type u_2} [inst_1 : RCLike 𝕜] [inst_2 : NormedSpace 𝕜 E] [inst_3 : OpensMeasurableSpace E]
  [inst_4 : Fact (1 ≤ p)] (h_Lp : MeasureTheory.MemLp id p μ) (L : StrongDual 𝕜 E),
  (StrongDual.toLp μ p) L = MeasureTheory.MemLp.toLp ⇑L ⋯
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.coe_toContinuousMap : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  (f : ZeroAtInftyContinuousMap α β), ⇑f.toContinuousMap = ⇑f
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.DelayedTheoremInstance.mk.injEq : ∀ (thm : Lean.Meta.Grind.EMatchTheorem) (proof prop : Lean.Expr) (generation : ℕ)
  (guards : List Lean.Meta.Grind.TheoremGuard) (sources : List Lean.Meta.Grind.EMatchDiagNode)
  (thm_1 : Lean.Meta.Grind.EMatchTheorem) (proof_1 prop_1 : Lean.Expr) (generation_1 : ℕ)
  (guards_1 : List Lean.Meta.Grind.TheoremGuard) (sources_1 : List Lean.Meta.Grind.EMatchDiagNode),
  ({ thm := thm, proof := proof, prop := prop, generation := generation, guards := guards, sources := sources } =
      { thm := thm_1, proof := proof_1, prop := prop_1, generation := generation_1, guards := guards_1,
        sources := sources_1 }) =
    (thm = thm_1 ∧
      proof = proof_1 ∧ prop = prop_1 ∧ generation = generation_1 ∧ guards = guards_1 ∧ sources = sources_1)
-- Lean.Expr
Lean.Expr.quickComp : Lean.Expr → Lean.Expr → Ordering
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.instSemilatticeInf : {α : Type u} → [inst : AddGroup α] → SemilatticeInf (AddGroupTopology α)
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.smul_hadamard : ∀ {α : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_4} (A B : Matrix m n α) [inst : Mul α] [inst_1 : SMul R α]
  [IsScalarTower R α α] (k : R), (k • A).hadamard B = k • A.hadamard B
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.tobject.sizeOf_spec : sizeOf Lean.IR.IRType.tobject = 1