mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Matrix.PosDef
Matrix.PosSemidef.trace_eq_zero_iff : ∀ {n : Type u_2} {𝕜 : Type u_3} [inst : Fintype n] [inst_1 : RCLike 𝕜] {A : Matrix n n 𝕜},
  A.PosSemidef → (A.trace = 0 ↔ A = 0)
-- Mathlib.NumberTheory.EulerProduct.Basic
/-- A version of `EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum`
in terms of the value of the series.  -/
EulerProduct.prod_filter_prime_tsum_eq_tsum_factoredNumbers : ∀ {R : Type u_1} [inst : NormedCommRing R] {f : ℕ → R} [CompleteSpace R],
  f 1 = 1 →
    (∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) →
      (Summable fun x => ‖f x‖) →
        ∀ (s : Finset ℕ), ∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n) = ∑' (m : ↑(Nat.factoredNumbers s)), f ↑m
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = true → t.minKey? = none
-- Mathlib.Combinatorics.Matroid.Loop
/-- `Matroid.loops M` is the closure of the empty set.  -/
Matroid.loops : {α : Type u_1} → Matroid α → Set α
-- Std.Http.Data.Status
/-- Converts a Status to a numeric code. This is useful for sending the status code in a response.
 -/
Std.Http.Status.toCode : Std.Http.Status → UInt16
-- Std.Http.Data.Response
/-- Builds and returns the final HTTP Response with the specified body.
 -/
Std.Http.Response.Builder.body : {t : Type} → Std.Http.Response.Builder → t → Std.Http.Response t
-- Mathlib.Topology.UniformSpace.UniformConvergence
TendstoUniformly.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] (F : ι → α → β) (f : α → β) (p : Filter ι),
  TendstoUniformly F f p = ∀ u ∈ uniformity β, ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ u
-- Mathlib.Analysis.Seminorm
Seminorm.instIsScalarTowerOfReal : ∀ {R : Type u_1} {R' : Type u_2} {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E]
  [inst_2 : SMul 𝕜 E] [inst_3 : SMul R ℝ] [inst_4 : SMul R NNReal] [inst_5 : IsScalarTower R NNReal ℝ]
  [inst_6 : SMul R' ℝ] [inst_7 : SMul R' NNReal] [inst_8 : IsScalarTower R' NNReal ℝ] [inst_9 : SMul R R']
  [IsScalarTower R R' ℝ], IsScalarTower R R' (Seminorm 𝕜 E)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.center_prod : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S],
  NonUnitalSubring.center (R × S) = (NonUnitalSubring.center R).prod (NonUnitalSubring.center S)
-- Aesop.Tree.Data
Aesop.RappData.assignedMVars : {Goal MVarCluster : Type} → Aesop.RappData Goal MVarCluster → Aesop.UnorderedArraySet Lean.MVarId
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_le : ∀ {r : ENNReal} {n : ℕ∞}, n ≠ ⊤ → (⌊r⌋ₑ ≤ n ↔ r < ↑n + 1)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.unitHomEquiv_apply_coe : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R) (f : PresheafOfModules.unit R ⟶ M) (X : Cᵒᵖ),
  ↑(M.unitHomEquiv f) X = (CategoryTheory.ConcreteCategory.hom (f.app X)) 1
-- Lean.Meta.Tactic.Cleanup
_private.Lean.Meta.Tactic.Cleanup.0.Lean.Meta.cleanupCore : Lean.MVarId → Array Lean.FVarId → Bool → Lean.MetaM Lean.MVarId
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.leftQuotientEquiv.congr_simp : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {S : Set G} (hS : Subgroup.IsComplement S ↑H),
  hS.leftQuotientEquiv = hS.leftQuotientEquiv
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
/-- The lax functor associated with a pseudofunctor.  -/
CategoryTheory.Pseudofunctor.toLax : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] → CategoryTheory.Pseudofunctor B C → CategoryTheory.LaxFunctor B C
-- Mathlib.NumberTheory.LegendreSymbol.Basic
/-- If `legendreSym p a = -1`, then the only solution of `x^2 - a*y^2 = 0` in `ℤ/pℤ`
is the trivial one.  -/
legendreSym.eq_zero_mod_of_eq_neg_one : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {a : ℤ},
  legendreSym p a = -1 → ∀ {x y : ZMod p}, x ^ 2 - ↑a * y ^ 2 = 0 → x = 0 ∧ y = 0
-- Lean.Meta.FunInfo
_private.Lean.Meta.FunInfo.0.Lean.Meta.instHashableFunInfoEnvCacheKey.hash : Lean.Meta.FunInfoEnvCacheKey✝ → UInt64
-- Lean.Declaration
Lean.DefinitionVal.safety : Lean.DefinitionVal → Lean.DefinitionSafety
-- Init.Tactics
/-- Theorems tagged with the `simp` attribute are used by the simplifier
(i.e., the `simp` tactic, and its variants) to simplify expressions occurring in your goals.
We call theorems tagged with the `simp` attribute "simp theorems" or "simp lemmas".
Lean maintains a database/index containing all active simp theorems.
Here is an example of a simp theorem.
```lean
@[simp] theorem ne_eq (a b : α) : (a ≠ b) = Not (a = b) := rfl
```
This simp theorem instructs the simplifier to replace instances of the term
`a ≠ b` (e.g. `x + 0 ≠ y`) with `Not (a = b)` (e.g., `Not (x + 0 = y)`).
The simplifier applies simp theorems in one direction only:
if `A = B` is a simp theorem, then `simp` replaces `A`s with `B`s,
but it doesn't replace `B`s with `A`s. Hence a simp theorem should have the
property that its right-hand side is "simpler" than its left-hand side.
In particular, `=` and `↔` should not be viewed as symmetric operators in this situation.
The following would be a terrible simp theorem (if it were even allowed):
```lean
@[simp] lemma mul_right_inv_bad (a : G) : 1 = a * a⁻¹ := ...
```
Replacing 1 with a * a⁻¹ is not a sensible default direction to travel.
Even worse would be a theorem that causes expressions to grow without bound,
causing simp to loop forever.

By default the simplifier applies `simp` theorems to an expression `e`
after its sub-expressions have been simplified.
We say it performs a bottom-up simplification.
You can instruct the simplifier to apply a theorem before its sub-expressions
have been simplified by using the modifier `↓`. Here is an example
```lean
@[simp↓] theorem not_and_eq (p q : Prop) : (¬ (p ∧ q)) = (¬p ∨ ¬q) :=
```

You can instruct the simplifier to rewrite the lemma from right-to-left:
```lean
attribute @[simp ←] and_assoc
```

When multiple simp theorems are applicable, the simplifier uses the one with highest priority.
The equational theorems of functions are applied at very low priority (100 and below).
If there are several with the same priority, it is uses the "most recent one". Example:
```lean
@[simp high] theorem cond_true (a b : α) : cond true a b = a := rfl
@[simp low+1] theorem or_true (p : Prop) : (p ∨ True) = True :=
  propext <| Iff.intro (fun _ => trivial) (fun _ => Or.inr trivial)
@[simp 100] theorem ite_self {d : Decidable c} (a : α) : ite c a a = a := by
  cases d <;> rfl
```
 -/
Lean.Parser.Attr.simp : Lean.ParserDescr
-- Init.Data.String.Slice
String.Slice.instDecidableLE : DecidableLE String.Slice
-- Mathlib.Dynamics.Flow
isInvariant_iff_image : ∀ {τ : Type u_1} {α : Type u_2} (ϕ : τ → α → α) (s : Set α), IsInvariant ϕ s ↔ ∀ (t : τ), ϕ t '' s ⊆ s
-- Lean.Expr
Lean.Expr.updateLambda! : Lean.Expr → Lean.BinderInfo → Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.toComp_toAlgHom : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_3} {T : Type u_7} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.Generators S T ι') (P : Algebra.Generators R S ι),
  (Q.toComp P).toAlgHom = MvPolynomial.rename Sum.inr
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- Compatibility with scalar multiplication. Note this assumes `𝕜` is a division ring in order to
ensure that for `c ≠ 0`, `c • f` is integrable iff `f` is. For scalar multiplication by more
general rings assuming integrability, see `IntervalIntegrable.integral_smul`.  -/
intervalIntegral.integral_smul : ∀ {𝕜 : Type u_2} {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ}
  {μ : MeasureTheory.Measure ℝ} [inst_2 : NormedDivisionRing 𝕜] [inst_3 : Module 𝕜 E] [NormSMulClass 𝕜 E]
  [SMulCommClass ℝ 𝕜 E] (r : 𝕜) (f : ℝ → E), ∫ (x : ℝ) in a..b, r • f x ∂μ = r • ∫ (x : ℝ) in a..b, f x ∂μ
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
CategoryTheory.Adjunction.functorCategory_inverseImage_isomorphisms_counit : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  [F.Full] [F.Faithful] (adj : F ⊣ G),
  ((CategoryTheory.MorphismProperty.isomorphisms C₂).inverseImage G).functorCategory C₁ adj.counit
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.instIsSplitEpiBiproductComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁}
  (F : CategoryTheory.Functor C D) (f : J → C) [inst_4 : CategoryTheory.Limits.HasBiproduct f]
  [inst_5 : CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)] [F.PreservesZeroMorphisms],
  CategoryTheory.IsSplitEpi (F.biproductComparison f)
-- Mathlib.Topology.Algebra.LinearTopology
IsLinearTopology.hasBasis_submodule : ∀ (R : Type u_1) {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] [IsLinearTopology R M], (nhds 0).HasBasis (fun N => ↑N ∈ nhds 0) fun N => ↑N
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentPositionParams.mk : Lean.Lsp.TextDocumentIdentifier → Lean.Lsp.Position → Lean.Lsp.TextDocumentPositionParams
-- Mathlib.Order.Filter.Prod
Filter.tendsto_prodAssoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Filter γ},
  Filter.Tendsto (⇑(Equiv.prodAssoc α β γ)) ((f ×ˢ g) ×ˢ h) (f ×ˢ g ×ˢ h)
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.instMulZeroOneClass : {α : Type u_1} → [MulOneClass α] → MulZeroOneClass (WithZero α)
-- Mathlib.Topology.DerivedSet
preperfect_iff_eq_relDerivedSet : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X}, Preperfect U ↔ U = relDerivedSet U
-- Mathlib.Algebra.Free
FreeSemigroup.traverse_pure' : ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β), traverse F ∘ pure = fun x => pure <$> F x
-- Lean.Data.PrefixTree
_private.Lean.Data.PrefixTree.0.Lean.PrefixTreeNode.insert.loop : {α : Type u_1} →
  {β : Type u_2} → (cmp : α → α → Ordering) → β → Lean.PrefixTreeNode α β cmp → List α → Lean.PrefixTreeNode α β cmp
-- Mathlib.CategoryTheory.Monoidal.Linear
/-- A faithful linear monoidal functor to a linear monoidal category
ensures that the domain is linear monoidal.  -/
CategoryTheory.MonoidalLinear.ofFaithful : ∀ (R : Type u_1) [inst : Semiring R] {C : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C]
  [inst_4 : CategoryTheory.MonoidalCategory C] [inst_5 : CategoryTheory.MonoidalPreadditive C]
  [CategoryTheory.MonoidalLinear R C] {D : Type u_3} [inst_7 : CategoryTheory.Category.{v_2, u_3} D]
  [inst_8 : CategoryTheory.Preadditive D] [inst_9 : CategoryTheory.Linear R D]
  [inst_10 : CategoryTheory.MonoidalCategory D] [inst_11 : CategoryTheory.MonoidalPreadditive D]
  (F : CategoryTheory.Functor D C) [F.Monoidal] [F.Faithful] [CategoryTheory.Functor.Linear R F],
  CategoryTheory.MonoidalLinear R D
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
CategoryTheory.Limits.colim.mapShortComplex_X₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} J]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex (CategoryTheory.Functor J C))
  {c₁ : CategoryTheory.Limits.Cocone S.X₁} (hc₁ : CategoryTheory.Limits.IsColimit c₁)
  (c₂ : CategoryTheory.Limits.Cocone S.X₂) (c₃ : CategoryTheory.Limits.Cocone S.X₃) (f : c₁.pt ⟶ c₂.pt)
  (g : c₂.pt ⟶ c₃.pt)
  (hf :
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp (c₁.ι.app j) f = CategoryTheory.CategoryStruct.comp (S.f.app j) (c₂.ι.app j))
  (hg :
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp (c₂.ι.app j) g = CategoryTheory.CategoryStruct.comp (S.g.app j) (c₃.ι.app j)),
  (CategoryTheory.Limits.colim.mapShortComplex S hc₁ c₂ c₃ f g hf hg).X₂ = c₂.pt
-- Std.Do.Internal.Ensures.Def
Std.Do.Internal.MayReturn.mk : ∀ {m : Type u → Type v} [inst : Bind m] {α : Type u} {x : m α} {a : α},
  (∀ {P : α → Prop}, Std.Do.Internal.Ensures P x → P a) → Std.Do.Internal.MayReturn x a
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_nonneg : ∀ {x : ℝ}, 0 ≤ x → ∀ (y : ℝ), 0 ≤ x ^ y
-- Mathlib.Analysis.InnerProductSpace.Spectrum
eigenvalue_nonneg_of_nonneg : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {μ : ℝ} {T : E →ₗ[𝕜] E}, Module.End.HasEigenvalue T ↑μ → (∀ (x : E), 0 ≤ RCLike.re (inner 𝕜 x (T x))) → 0 ≤ μ
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.isMatcherAppCore? : Lean.Environment → Lean.Expr → Option Lean.Meta.MatcherInfo
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
CoalgCat.MonoidalCategoryAux.counit_tensorObj : ∀ {R : Type u} [inst : CommRing R] {M N : Type u} [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] [inst_5 : Coalgebra R M] [inst_6 : Coalgebra R N],
  CoalgebraStruct.counit = CoalgebraStruct.counit
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- **Alias** of `Matroid.contract_contract_eq_contract_sdiff`. -/
Matroid.contract_contract_eq_contract_diff : ∀ {α : Type u_1} (M : Matroid α) (C₁ C₂ : Set α), (M.contract C₁).contract C₂ = (M.contract C₁).contract (C₂ \ C₁)
-- Mathlib.Tactic.ClickSuggestions.GRewrite
Mathlib.Tactic.ClickSuggestions.GrwKey.mk.sizeOf_spec : ∀ (numGoals nameLength replacementSize : ℕ) (name : String) (replacement : Lean.Meta.AbstractMVarsResult),
  sizeOf
      { numGoals := numGoals, nameLength := nameLength, replacementSize := replacementSize, name := name,
        replacement := replacement } =
    1 + sizeOf numGoals + sizeOf nameLength + sizeOf replacementSize + sizeOf name + sizeOf replacement
-- Mathlib.Analysis.Normed.Group.Basic
NormedAddGroup.nhds_zero_basis_norm_lt : ∀ {E : Type u_5} [inst : SeminormedAddGroup E], (nhds 0).HasBasis (fun ε => 0 < ε) fun ε => {y | ‖y‖ < ε}
-- Lean.Parser.Module
/-- Whether there is leading whitespace before `pos`.
Used to associate whitespace at the start of the file with the first token of the file.
 -/
Lean.Parser.ModuleParserState.hasLeading : Lean.Parser.ModuleParserState → Bool
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.foldlMAux : {m : Type w → Type w'} →
  [Monad m] →
    {σ : Type w} → {α : Type u_1} → {β : Type u_2} → (σ → α → β → m σ) → Lean.PersistentHashMap.Node α β → σ → m σ
-- Mathlib.GroupTheory.Nilpotent
instIsCyclicOfIsSimpleGroupOfIsNilpotent : ∀ {G : Type u_1} [inst : Group G] [IsSimpleGroup G] [Group.IsNilpotent G], IsCyclic G
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.Coreflective.comp : {C : Type u₁} →
  {D : Type u₂} →
    {E : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (F : CategoryTheory.Functor C D) →
              (G : CategoryTheory.Functor D E) →
                [CategoryTheory.Coreflective F] →
                  [CategoryTheory.Coreflective G] → CategoryTheory.Coreflective (F.comp G)
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.processPostponedStep : Bool → Lean.MetaM Bool
-- Std.Data.ExtTreeMap.Lemmas
/-- Simpler variant of `getD_filterMap` when `LawfulEqCmp` is available.  -/
Std.ExtTreeMap.getD_filterMap' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → Option γ} {k : α} {fallback : γ},
  (Std.ExtTreeMap.filterMap f t).getD k fallback = (t[k]?.bind (f k)).getD fallback
-- Mathlib.Order.Interval.Finset.Basic
Finset.uIcc_of_not_le : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α},
  ¬a ≤ b → Finset.uIcc a b = Finset.Icc b a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
/-- **Alias** of `Complex.logDeriv_exp`. -/
Complex.LogDeriv_exp : logDeriv Complex.exp = 1
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.C_add : ∀ {R : Type u_1} {a b : R} [inst : AddZeroClass R] (x y : R),
  QuadraticAlgebra.C (x + y) = QuadraticAlgebra.C x + QuadraticAlgebra.C y
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.height_one_of_mem_support : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {b : P.Base}
  [inst_5 : CharZero R] {i : ι}, i ∈ b.support → b.height i = 1
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.supDegree_eq_degree : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), AddMonoidAlgebra.supDegree WithBot.some p.toFinsupp = p.degree
-- Mathlib.CategoryTheory.Limits.Over
CategoryTheory.Over.createsColimitsOfSizeMapCompForget : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        CategoryTheory.CreatesColimitsOfSize.{w, w', v, v, max u v, u}
          ((CategoryTheory.Over.map f).comp (CategoryTheory.Over.forget Y))
-- Init.Data.SInt.Bitwise
Int8.toInt32_or : ∀ (a b : Int8), (a ||| b).toInt32 = a.toInt32 ||| b.toInt32
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.ofComponents'.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (app : (X : C) → F.obj X ≅ G.obj X)
  (naturality :
    ∀ {X Y : C} (f : Y ⟶ X),
      CategoryTheory.CategoryStruct.comp (app Y).inv (F.map f) =
        CategoryTheory.CategoryStruct.comp (G.map f) (app X).inv),
  CategoryTheory.NatIso.ofComponents' app naturality =
    { hom := CategoryTheory.NatTrans.mk' (fun X => (app X).hom) ⋯,
      inv := CategoryTheory.NatTrans.mk' (fun X => (app X).inv) ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.Order.CompleteLattice.Basic
Set.BijOn.iInf_congr : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] {s : Set β} {t : Set γ} (f : β → α)
  (g : γ → α) {h : β → γ}, Set.BijOn h s t → (∀ (x : β), g (h x) = f x) → ⨅ x ∈ s, f x = ⨅ y ∈ t, g y
-- Mathlib.GroupTheory.Index
Subgroup.pow_mem_of_index_ne_zero_of_dvd : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G},
  H.index ≠ 0 → ∀ (a : G) {n : ℕ}, (∀ (m : ℕ), 0 < m → m ≤ H.index → m ∣ n) → a ^ n ∈ H
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
/-- If `F` reflects isos and `F.map f` is an iso, then `f` is an iso.  -/
CategoryTheory.isIso_of_reflects_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {A B : C} (f : A ⟶ B) (F : CategoryTheory.Functor C D)
  [CategoryTheory.IsIso (F.map f)] [F.ReflectsIsomorphisms], CategoryTheory.IsIso f
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.r_eq_none : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (i' : ι'),
  (∀ (i : ι), e.f i ≠ i') → e.r i' = none
-- Mathlib.Algebra.Torsor.Basic
Prod.fst_smul : ∀ {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [inst : Group G] [inst_1 : Group G']
  [inst_2 : Torsor G P] [inst_3 : Torsor G' P'] (v : G × G') (p : P × P'), (v • p).1 = v.1 • p.1
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.zero_mem_neg_add_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddGroup α] {s t : Finset α}, 0 ∈ -t + s ↔ ¬Disjoint s t
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.mem_neighborSet : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v w : V), w ∈ G'.neighborSet v ↔ G'.Adj v w
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instInvolutiveInv : {α : Type u_1} → [InvolutiveInv α] → InvolutiveInv (Colex α)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.edges_nil : ∀ {V : Type u} {G : SimpleGraph V} {u : V}, SimpleGraph.Walk.nil.edges = []
-- Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries
PowerSeries.coeff_pentagonalSeries_pentagonal : ∀ (R : Type u_1) [inst : CommRing R] (k : ℤ),
  (PowerSeries.coeff (pentagonal k)) (PowerSeries.pentagonalSeries R) = ↑↑k.negOnePow
-- Mathlib.Analysis.Complex.Asymptotics
Complex.isTheta_ofReal_right : ∀ {α : Type u_1} {E : Type u_2} [inst : Norm E] {l : Filter α} {f : α → E} {g : α → ℝ},
  (f =Θ[l] fun x => ↑(g x)) ↔ f =Θ[l] g
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor_obj : ∀ {V : Type u'} [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {W : Type u''}
  [inst_2 : CategoryTheory.Category.{v'', u''} W] [inst_3 : CategoryTheory.MonoidalCategory W]
  (F : CategoryTheory.Functor V W) [inst_4 : F.LaxMonoidal] (D : Type u) [inst_5 : CategoryTheory.EnrichedCategory V D]
  (e :
    (v : V) →
      (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v))
  (h :
    ∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v),
      (e v) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f))
  (X : CategoryTheory.TransportEnrichment F (CategoryTheory.ForgetEnrichment V D)),
  (CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor F D e h).obj X =
    CategoryTheory.ForgetEnrichment.of W X
-- Mathlib.LinearAlgebra.SymplecticGroup
Matrix.isUnit_det_J : ∀ (l : Type u_1) (R : Type u_2) [inst : DecidableEq l] [inst_1 : CommRing R] [inst_2 : Fintype l],
  IsUnit (Matrix.J l R).det
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
PresheafOfModules.instIsLeftAdjointSheafOfModulesSheafification : ∀ {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.HasWeakSheafify J AddCommGrpCat],
  (PresheafOfModules.sheafification α).IsLeftAdjoint
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_inter_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → (t₁ ∩ t₂).get? k = t₁.get? k
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.skip : Lean.ParseImports.Parser
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.postcomp₂_app_toFunctor_obj : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b) (x : Bᵒᵖ) (x_1 : Opposite.unop x ⟶ a),
  ((CategoryTheory.Bicategory.postcomp₂ f).app x).toFunctor.obj x_1 = CategoryTheory.CategoryStruct.comp x_1 f
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.notation : Lean.Option Bool
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.instHasBinaryBiproductOppositeOp : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} [CategoryTheory.Limits.HasBinaryBiproduct P Q],
  CategoryTheory.Limits.HasBinaryBiproduct (Opposite.op P) (Opposite.op Q)
-- Mathlib.Algebra.Ring.Pi
/-- **Alias** of `NonUnitalRingHom.pi_injective`. -/
Pi.nonUnitalRingHom_injective : ∀ {I : Type u} {f : I → Type u_1} {γ : Type u_2} [Nonempty I] [inst : (i : I) → NonUnitalNonAssocSemiring (f i)]
  [inst_1 : NonUnitalNonAssocSemiring γ] (g : (i : I) → γ →ₙ+* f i),
  (∀ (i : I), Function.Injective ⇑(g i)) → Function.Injective ⇑(NonUnitalRingHom.pi g)