mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.toAddHom_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZero M] [inst_1 : AddZero N] (f : M →+ N), (↑f).toFun = ⇑f
-- Mathlib.Order.SymmDiff
himp_bihimp_eq_inf : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b : α), bihimp (b ⇨ a) b = a ⊓ b
-- Mathlib.Algebra.Free
/-- `FreeAddMagma` is traversable.  -/
FreeAddMagma.traverse : {m : Type u → Type u} → [Applicative m] → {α β : Type u} → (α → m β) → FreeAddMagma α → m (FreeAddMagma β)
-- Lean.Server.Utils
/-- Controls when dependencies of the document are built on `textDocument/didOpen` notifications.
 -/
Lean.Server.DocumentMeta.dependencyBuildMode : Lean.Server.DocumentMeta → Lean.Lsp.DependencyBuildMode
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.finrank_add_finrank_orthogonal : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  {B : LinearMap.BilinForm K V},
  B.IsRefl →
    ∀ (W : Submodule K V),
      Module.finrank K ↥W + Module.finrank K ↥(B.orthogonal W) =
        Module.finrank K V + Module.finrank K ↥(W ⊓ B.orthogonal ⊤)
-- Mathlib.Algebra.Ring.Prod
RingEquiv.prodProdProdComm_apply : ∀ (R : Type u_1) (R' : Type u_2) (S : Type u_3) (S' : Type u_4) [inst : NonAssocSemiring R]
  [inst_1 : NonAssocSemiring S] [inst_2 : NonAssocSemiring R'] [inst_3 : NonAssocSemiring S']
  (rrss : (R × R') × S × S'), (RingEquiv.prodProdProdComm R R' S S') rrss = ((rrss.1.1, rrss.2.1), rrss.1.2, rrss.2.2)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.under_iff : ∀ {T : Type u_3} [inst : CategoryTheory.Category.{v_3, u_3} T] {W : CategoryTheory.MorphismProperty T} {X : T}
  {Y Z : CategoryTheory.Under X} (f : Y ⟶ Z), W.under f ↔ W (CategoryTheory.Under.Hom.right f)
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.instCoeOutRingEquiv : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Mul α] →
      [inst_1 : Add α] →
        [inst_2 : LE α] → [inst_3 : Mul β] → [inst_4 : Add β] → [inst_5 : LE β] → CoeOut (α ≃+*o β) (α ≃+* β)
-- Mathlib.Data.Set.Image
Function.Semiconj.set_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β},
  Function.Semiconj f ga gb → Function.Semiconj (Set.image f) (Set.image ga) (Set.image gb)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List α} {k fallback : α}, k ∈ m → (m.insertMany l).getD k fallback = m.getD k fallback
-- Lean.Declaration
Lean.ConstantInfo.isPartial : Lean.ConstantInfo → Bool
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
/-- Hilbert's Theorem 90: given a finite cyclic Galois extension `L/K`, an element `x : L` such
that `N_{L/K}(x) = 1`, and a generator `g` of `Gal(L/K)`, there exists `y : Lˣ`
such that `y/g y = x`.  -/
groupCohomology.exists_div_of_norm_eq_one : ∀ {K L : Type} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [FiniteDimensional K L] [IsGalois K L]
  [IsCyclic Gal(L/K)] {g : Gal(L/K)},
  (∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g) → ∀ {x : L}, (Algebra.norm K) x = 1 → ∃ y, ↑y / g ↑y = x
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.symmetricIoc_filter : ∀ (G : Type u_1) [inst : Neg G] [inst_1 : Preorder G] [inst_2 : LocallyFiniteOrder G],
  (SummationFilter.symmetricIoc G).filter = Filter.map (fun N => Finset.Ioc (-N) N) Filter.atTop
-- Std.Http.Transport
Std.Http.Internal.instTransportClient : Std.Http.Transport Std.Http.Internal.Mock.Client
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.tr.eq_3 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ)
  (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2to1.tr M (Turing.TM2to1.Λ'.ret q) =
    Turing.TM1.Stmt.branch (fun a x => a.1) (Turing.TM2to1.trNormal q)
      (Turing.TM1.Stmt.move Turing.Dir.left (Turing.TM1.Stmt.goto fun x x_1 => Turing.TM2to1.Λ'.ret q))
-- Mathlib.GroupTheory.ArchimedeanDensely
/-- Any linearly ordered mul-archimedean group is either isomorphic (and order-isomorphic)
to the multiplicative integers, or is densely ordered.  -/
LinearOrderedCommGroup.discrete_or_denselyOrdered : ∀ (G : Type u_1) [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G],
  Nonempty (G ≃*o Multiplicative ℤ) ∨ DenselyOrdered G
-- Aesop.Rule
Aesop.LocalNormSimpRule.mk : Lean.Name → Lean.Term → Aesop.LocalNormSimpRule
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.instSetLike : {R : Type u} → [inst : NonAssocRing R] → SetLike (Subring R) R
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- The difference of two completed even Hurwitz zeta functions is differentiable at `s = 1`.  -/
HurwitzZeta.differentiableAt_one_completedHurwitzZetaEven_sub_completedHurwitzZetaEven : ∀ (a b : UnitAddCircle),
  DifferentiableAt ℂ (fun s => HurwitzZeta.completedHurwitzZetaEven a s - HurwitzZeta.completedHurwitzZetaEven b s) 1
-- Init.Data.SInt.Lemmas
ISize.toInt16_ofIntClamp : ∀ {n : ℤ},
  -2 ^ (System.Platform.numBits - 1) ≤ n →
    n < 2 ^ (System.Platform.numBits - 1) → (ISize.ofIntClamp n).toInt16 = Int16.ofInt n
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Function.Injective.multipliable_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {g : γ → β}, Function.Injective g → (∀ x ∉ Set.range g, f x = 1) → (Multipliable (f ∘ g) ↔ Multipliable f)
-- Mathlib.Order.Monotone.Monovary
antivaryOn_univ : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
  AntivaryOn f g Set.univ ↔ Antivary f g
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_insertMany_list_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {l : List (α × β)},
  (t.insertMany l).size ≤ t.size + l.length
-- Mathlib.Algebra.Category.MonCat.Limits
/-- If `J` is `u`-small, the forgetful functor from `MonCat.{u}` preserves limits of shape `J`.  -/
MonCat.forget_preservesLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget MonCat)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMapClass.toContinuousMapClass : ∀ {F : Type u_5} {α : outParam (Type u_6)} {β : outParam (Type u_7)} {inst : TopologicalSpace α} {inst_1 : Zero β}
  {inst_2 : TopologicalSpace β} {inst_3 : FunLike F α β} [self : CompactlySupportedContinuousMapClass F α β],
  ContinuousMapClass F α β
-- Mathlib.Topology.Separation.DisjointCover
/-- If `S` is any neighbourhood of the diagonal in a profinite topological space `X`, then there
exists a finite cover of `X` by disjoint nonempty clopens `U i` with `U i ×ˢ U i ⊆ S` for all `i`.
 -/
_private.Mathlib.Topology.Separation.DisjointCover.0.TopologicalSpace.exists_finite_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal_of_profinite : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set (X × X)} [CompactSpace X] [TotallyDisconnectedSpace X]
  [T2Space X],
  S ∈ nhdsSet (Set.diagonal X) →
    ∃ n D,
      (∀ (i : Fin n), D i ≠ ⊥) ∧
        (∀ (i : Fin n), ∀ y ∈ D i, ∀ z ∈ D i, (y, z) ∈ S) ∧
          Set.univ ⊆ ⋃ i, ↑(D i) ∧ Pairwise (Function.onFun Disjoint D)
-- Mathlib.Order.Hom.Lattice
LatticeHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : Lattice α] [inst_1 : Lattice β]
  [inst_2 : Lattice γ] [inst_3 : Lattice δ] (f : LatticeHom γ δ) (g : LatticeHom β γ) (h : LatticeHom α β),
  (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.Analysis.Convex.Combination
convex_iff_sum_mem : ∀ {R : Type u_1} {E : Type u_3} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E] {s : Set E}
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R],
  Convex R s ↔
    ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.takeWhile_append_dropWhile : ∀ {ρ : Type} {pat : ρ} [String.Slice.Pattern.Model.PatternModel pat] [inst : String.Slice.Pattern.ForwardPattern pat]
  [String.Slice.Pattern.LawfulForwardPattern pat] {s : String.Slice},
  (s.takeWhile pat).copy ++ (s.dropWhile pat).copy = s.copy
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
/-- If the measure `μ.trim hm` is sigma-finite, then the conditional expectation of a measurable set
with finite measure is integrable.  -/
MeasureTheory.integrable_condExpIndSMul : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] (hm : m ≤ m0) [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : MeasurableSet s)
  (hμs : μ s ≠ ⊤) (x : G), MeasureTheory.Integrable (↑↑(MeasureTheory.condExpIndSMul hm hs hμs x)) μ
-- Mathlib.Order.Bounds.Defs
IsLeast.eq_1 : ∀ {α : Type u_1} [inst : LE α] (s : Set α) (a : α), IsLeast s a = (a ∈ s ∧ a ∈ lowerBounds s)
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.le_meet_left : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q : l},
  Lean.Order.PartialOrder.rel P Q → Lean.Order.PartialOrder.rel P (Lean.Order.meet Q P)
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.SeparatingRight.toBilin' : ∀ {R₂ : Type u_3} [inst : CommRing R₂] {ι : Type u_6} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {M : Matrix ι ι R₂},
  M.SeparatingRight → LinearMap.SeparatingRight (Matrix.toBilin' M)
-- Lean.Parser.Basic
Lean.Parser.charLitNoAntiquot : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- `desc` is the unique such map  -/
CategoryTheory.Limits.IsColimit.uniq : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (self : CategoryTheory.Limits.IsColimit t)
  (s : CategoryTheory.Limits.Cocone F) (m : t.pt ⟶ s.pt),
  (∀ (j : J), CategoryTheory.CategoryStruct.comp (t.ι.app j) m = s.ι.app j) → m = self.desc s
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.HeadInfo.mk : Lean.Elab.Term.Quotation.HeadCheck →
  (Lean.Elab.Term.Quotation.HeadCheck → Lean.Elab.Term.Quotation.MatchResult) →
    ((List Lean.Term → Lean.Elab.TermElabM Lean.Term) → Lean.Elab.TermElabM Lean.Term → Lean.Elab.TermElabM Lean.Term) →
      Lean.Elab.Term.Quotation.HeadInfo
-- Std.Http.Data.Method
Std.Http.Method.put.sizeOf_spec : sizeOf Std.Http.Method.put = 1
-- Mathlib.Data.EReal.Operations
EReal.coe_ennreal_mul_top : ∀ {x : ENNReal}, x ≠ 0 → ↑x * ⊤ = ⊤
-- Lean.Meta.Basic
/-- Mark declaration `declName` with the attribute `[inline]`.
This method does not check whether the given declaration is a definition.

Recall that this attribute can only be set in the same module where `declName` has been declared.
 -/
Lean.Meta.setInlineAttribute : Lean.Name → optParam Lean.Compiler.InlineAttributeKind Lean.Compiler.InlineAttributeKind.inline → Lean.MetaM Unit
-- Init.Data.List.Lemmas
List.reverse_eq_cons_iff : ∀ {α : Type u_1} {xs : List α} {a : α} {ys : List α}, xs.reverse = a :: ys ↔ xs = ys.reverse ++ [a]
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat.instFaithfulMat_SingleObjMulOppositeEquivalenceSingleObjInverse : ∀ (R : Type) [inst : Ring R], (CategoryTheory.Mat.equivalenceSingleObjInverse R).Faithful
-- Mathlib.Analysis.Complex.Harmonic.MeanValue
/-- Compositions of continuous ℝ-linear maps with functions that are harmonic on a set and continuous
on its closure are again harmonic on the set and continuous on its closure.
 -/
InnerProductSpace.HarmonicContOnCl.comp_CLM : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {G : Type u_3}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace ℝ G] {f : E → F} {s : Set E},
  InnerProductSpace.HarmonicContOnCl f s → ∀ (l : F →L[ℝ] G), InnerProductSpace.HarmonicContOnCl (⇑l ∘ f) s
-- Init.Core
Iff.trans : ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
-- Mathlib.CategoryTheory.Category.RelCat
/-- The other direction of `opFunctor`.  -/
CategoryTheory.RelCat.unopFunctor : CategoryTheory.Functor CategoryTheory.RelCatᵒᵖ CategoryTheory.RelCat
-- Init.Data.Array.Lemmas
Array.forall_mem_empty : ∀ {α : Type u_1} (p : α → Prop), ∀ x ∈ #[], p x
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.instCompleteSpace : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], CompleteSpace ℚ_[p]
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.divLeft_symm_apply : ∀ {G : Type u_5} [inst : Group G] (a b : G), (Equiv.divLeft a).symm b = b⁻¹ * a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.self_le_maxKey?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {kmi : α}, (t.insert k v).maxKey?.get ⋯ = kmi → (cmp k kmi).isLE = true
-- Mathlib.Topology.Order
instIndiscreteTopologyPEmpty : IndiscreteTopology PEmpty.{u_1 + 1}
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.evaln_map : ∀ (k : ℕ) (c : Nat.Partrec.Code) (n : ℕ),
  ((List.range k)[n]?.bind fun a => Nat.Partrec.Code.evaln k c a) = Nat.Partrec.Code.evaln k c n
-- Mathlib.Data.List.Map2
List.zipLeft_nil_left : ∀ {α : Type u} {β : Type v} (bs : List β), [].zipLeft bs = []
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.edist_def : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : EDist X] (x y : Metric.Snowflaking X α hα₀ hα₁),
  edist x y = edist (Metric.Snowflaking.ofSnowflaking x) (Metric.Snowflaking.ofSnowflaking y) ^ α
-- Mathlib.CategoryTheory.ShrinkYoneda
/-- `uliftYoneda` identifies to `shrinkYoneda`.  -/
CategoryTheory.uliftYonedaIsoShrinkYoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.uliftYoneda.{w', v, u} ≅ CategoryTheory.shrinkYoneda.{max w' v, v, u}
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.run_ExceptT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε α : Type u}
  (x : ExceptT ε m α) (post : α → Pred) (epost : EPost.Cons✝ (ε → Pred) EPred),
  ⦃ Std.Internal.Do.wp x post epost ⦄ x.run ⦃ Std.Internal.Do.EPost.Cons.pushExcept post epost; epost.tail ⦄
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.refl_symm : ∀ {X : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G X],
  (Equidecomp.refl X G).symm = Equidecomp.refl X G
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
/-- `ContinuousLinearMap.compContinuousMultilinearMap` as a bundled continuous bilinear map.

Given a continuous linear map `f : F →L[𝕜] G`
and a continuous multilinear map `g` from `Π i, E i` to `F`,
this function returns `f ∘ g` as a continuous multilinear map.

With this order of arguments, the function is continuous in `g` (for each fixed `f`)
and is continuous in `f` (as a function to the space of continuous linear maps).
Note that for general topological vector spaces, it is not guaranteed to be continuous in `(g, f)`.
 -/
ContinuousLinearMap.compContinuousMultilinearMapL : (𝕜 : Type u_1) →
  {ι : Type u_2} →
    (E : ι → Type u_3) →
      (F : Type u_4) →
        (G : Type u_5) →
          [inst : NormedField 𝕜] →
            [inst_1 : (i : ι) → TopologicalSpace (E i)] →
              [inst_2 : (i : ι) → AddCommGroup (E i)] →
                [inst_3 : (i : ι) → Module 𝕜 (E i)] →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : Module 𝕜 F] →
                      [inst_6 : TopologicalSpace F] →
                        [inst_7 : IsTopologicalAddGroup F] →
                          [inst_8 : ContinuousConstSMul 𝕜 F] →
                            [inst_9 : AddCommGroup G] →
                              [inst_10 : Module 𝕜 G] →
                                [inst_11 : TopologicalSpace G] →
                                  [inst_12 : IsTopologicalAddGroup G] →
                                    [inst_13 : ContinuousConstSMul 𝕜 G] →
                                      (F →L[𝕜] G) →L[𝕜]
                                        ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G
-- Aesop.Stats.Basic
Aesop.instToStringMethod : ToString Aesop.ScriptGenerated.Method
-- Lean.Data.RArray
Lean.RArray.ofArray : {α : Type u_1} → (xs : Array α) → 0 < xs.size → Lean.RArray α
-- Mathlib.Algebra.Ring.Int.Parity
/-- **Alias** of `Int.even_xor_odd`. -/
Int.even_xor'_odd : ∀ (n : ℤ), Xor (Even n) (Odd n)
-- Init.Prelude
HSMul.mk : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → (α → β → γ) → HSMul α β γ
-- Mathlib.Order.Lattice
inf_le_of_left_le : ∀ {α : Type u} [inst : SemilatticeInf α] {a b c : α}, a ≤ c → a ⊓ b ≤ c
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred.c₁ : Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred → Lean.Meta.Grind.Arith.Cutsat.LeCnstr
-- Mathlib.Data.Nat.Cast.Order.Basic
Nat.one_le_cast_iff_ne_zero : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α]
  {n : ℕ}, 1 ≤ ↑n ↔ n ≠ 0
-- Mathlib.Algebra.Order.Hom.Monoid
strictAnti_iff_map_pos : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F)
  [iamhc : AddMonoidHomClass F α β], StrictAnti ⇑f ↔ ∀ a < 0, 0 < f a
-- Mathlib.Algebra.Group.Int.Defs
Int.instSemigroup : Semigroup ℤ
-- Init.Data.List.Lemmas
List.ne_of_not_mem_cons : ∀ {α : Type u_1} {a b : α} {l : List α}, a ∉ b :: l → a ≠ b
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasLaw.lintegral_comp : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure 𝓧}
  {P : MeasureTheory.Measure Ω} {X : Ω → 𝓧},
  ProbabilityTheory.HasLaw X μ P → ∀ {f : 𝓧 → ENNReal}, AEMeasurable f μ → ∫⁻ (ω : Ω), f (X ω) ∂P = ∫⁻ (x : 𝓧), f x ∂μ
-- Mathlib.Algebra.BigOperators.Associated
Associates.finsetProd_mk : ∀ {ι : Type u_1} {M : Type u_2} [inst : CommMonoid M] {p : Finset ι} {f : ι → M},
  ∏ i ∈ p, Associates.mk (f i) = Associates.mk (∏ i ∈ p, f i)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.OplaxMonoidal.instIsIsoδ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] [CategoryTheory.Limits.PreservesFiniteProducts F]
  (X Y : C), CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.elabInductiveViewsFinalize : Array Lean.Elab.Command.InductiveView → Lean.Elab.Command.FinalizeContext✝ → Lean.Elab.Command.CommandElabM Unit
-- Lean.Meta.Tactic.Grind.Internalize
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.isCongruentCheck.go : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.Hom.w : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor C D} {T : D} {X Y : CategoryTheory.CostructuredArrow S T} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (S.map f.left) Y.hom = X.hom
-- Mathlib.Algebra.Order.Group.Basic
/-- A nontrivial densely linear ordered commutative group can't be a cyclic group.  -/
not_isCyclic_of_denselyOrdered : ∀ (α : Type u_1) [inst : CommGroup α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] [DenselyOrdered α] [Nontrivial α],
  ¬IsCyclic α
-- Mathlib.Algebra.Order.GroupWithZero.Basic
lt_self_pow₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a : M₀} {m : ℕ} [PosMulStrictMono M₀]
  [ZeroLEOneClass M₀], 1 < a → 1 < m → a < a ^ m
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.colimit.toCostructuredArrow_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F] {X Y : J} (f : X ⟶ Y),
  (CategoryTheory.Limits.colimit.toCostructuredArrow F).map f = CategoryTheory.CostructuredArrow.homMk f ⋯
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsBigO.smul : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {R : Type u_13} {𝕜' : Type u_16} [inst : SeminormedAddCommGroup E']
  [inst_1 : SeminormedAddCommGroup F'] [inst_2 : SeminormedRing R] [inst_3 : NormedDivisionRing 𝕜'] {f' : α → E'}
  {g' : α → F'} {l : Filter α} [inst_4 : Module R E'] [IsBoundedSMul R E'] [inst_6 : Module 𝕜' F'] [NormSMulClass 𝕜' F']
  {k₁ : α → R} {k₂ : α → 𝕜'}, k₁ =O[l] k₂ → f' =O[l] g' → (fun x => k₁ x • f' x) =O[l] fun x => k₂ x • g' x
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.snd_inl : ∀ {R : Type u} (M : Type v) [inst : Zero M] (r : R), (TrivSqZeroExt.inl r).snd = 0
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.smul_finset_subset_mul : ∀ {α : Type u_2} [inst : Mul α] [inst_1 : DecidableEq α] {s t : Finset α} {a : α}, a ∈ s → a • t ⊆ s * t
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.eq_mk'_iff_mul_eq : ∀ {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] {x : R} {y : ↥M} {z : S},
  z = IsLocalization.mk' S x y ↔ z * (algebraMap R S) ↑y = (algebraMap R S) x
-- Mathlib.Algebra.Category.MonCat.Limits
/-- The forgetful functor from commutative monoids to types preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of types.  -/
CommMonCat.forget_preservesLimitsOfSize : ∀ [UnivLE.{v, u}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, u, u, u + 1, u + 1} (CategoryTheory.forget CommMonCat)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
Std.Tactic.BVDecide.LRAT.Internal.Formula.delete_subset : ∀ {α : outParam (Type u)} {β : outParam (Type v)} {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w}
  {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ]
  (f : σ) (arr : Array ℕ),
  ∀ c ∈ Std.Tactic.BVDecide.LRAT.Internal.Formula.toList (Std.Tactic.BVDecide.LRAT.Internal.Formula.delete f arr),
    c ∈ Std.Tactic.BVDecide.LRAT.Internal.Formula.toList f
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.add_eq_empty : ∀ {α : Type u_2} [inst : Add α] {s t : Set α}, s + t = ∅ ↔ s = ∅ ∨ t = ∅
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.mk.sizeOf_spec : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} [inst_2 : SizeOf G] [inst_3 : SizeOf H]
  (toFun : G → H) (map_add_const' : ∀ (x : G), toFun (x + a) = toFun x + b),
  sizeOf { toFun := toFun, map_add_const' := map_add_const' } = 1
-- Mathlib.Algebra.Homology.Homotopy
dNext_comp_right : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D E : HomologicalComplex V c} (f : (i j : ι) → C.X i ⟶ D.X j) (g : D ⟶ E) (i : ι),
  ((dNext i) fun i j => CategoryTheory.CategoryStruct.comp (f i j) (g.f j)) =
    CategoryTheory.CategoryStruct.comp ((dNext i) f) (g.f i)
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.spectralRadius_zero : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A], spectralRadius 𝕜 0 = 0
-- Mathlib.Geometry.Polygon.Basic
/-- A polygon has nondegenerate vertices if any three consecutive vertices
are affinely independent.  -/
Polygon.HasNondegenerateVertices : (R : Type u_1) →
  {V : Type u_2} →
    {P : Type u_3} →
      {n : ℕ} →
        [inst : Ring R] → [inst_1 : AddCommGroup V] → [Module R V] → [AddTorsor V P] → [NeZero n] → Polygon P n → Prop