mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Compiler.IR.Basic
/-- Set of variable and join point names  -/
Lean.IR.IndexSet : Type
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preAleph_symm_aleph : ∀ (o : Ordinal.{u_1}), Cardinal.preAleph.symm (Cardinal.aleph o) = Ordinal.omega0 + o
-- Mathlib.Topology.Algebra.Valued.WithVal
Valuation.IsEquiv.uniformContinuous_congr : ∀ {R : Type u_4} {Γ₀ : Type u_5} {Γ₀' : Type u_6} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation R Γ₀} {w : Valuation R Γ₀'},
  v.IsEquiv w → UniformContinuous ⇑(WithVal.congr v w (RingEquiv.refl R))
-- Init.Data.Option.Lemmas
Option.get_eq_get! : ∀ {α : Type u_1} [inst : Inhabited α] (o : Option α) {h : o.isSome = true}, o.get h = o.get!
-- Mathlib.Algebra.Lie.Quotient
LieSubmodule.Quotient.lieQuotientHasBracket : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → (I : LieIdeal R L) → Bracket (L ⧸ I) (L ⧸ I)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_injective : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R], Function.Injective AddMonoidAlgebra.coeff
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The isomorphism `S.opcycles ≅ h.Q` induced by a right homology data `h` for a
short complex `S`.  -/
CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso : {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] → S.opcycles ≅ h.Q
-- Lean.Meta.Tactic.Grind.Arith.Linear.Model
/-- Assigns terms that do not have an assignment associated with them because they were used only as markers
for communicating with the `grind` core.
For example, suppose we have `a + b = c`. The `internalize` function marks `a + b`, `a`, and `b`
with theory variables. Let's assume we also have `c = 2*b`. In this case, `internalize` marks `2*b`
with a theory variable, and `b` is already marked. Then, when both equalities are asserted
in the `grind` core, the `linarith` module is notified that `a + b = 2*b` is true, and it is then
normalized as `a + -1*b = 0`. The terms `a` and `b` are assigned rational values by the search
procedure, but `a + b` and `2*b` are not. This procedure assigns them using the model computed by the
search procedure.

**Note**: We should reconsider whether to add the equalities `「a+b」 = a + b` and `「2*b」 = 2*b`
to force the search procedure to assign interpretations to these terms.
 -/
_private.Lean.Meta.Tactic.Grind.Arith.Linear.Model.0.Lean.Meta.Grind.Arith.Linear.assignTerms : Lean.Meta.Grind.Goal → ℕ → Std.HashMap Lean.Expr ℚ → Lean.MetaM (Std.HashMap Lean.Expr ℚ)
-- Lean.Linter.MissingDocs
_private.Lean.Linter.MissingDocs.0.Lean.Linter.MissingDocs.lintDocStatusNamed : Bool → Lean.Syntax → String → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
/-- A variant of `of_isColimit` that is more useful with `apply`.  -/
CategoryTheory.IsPushout.of_isColimit' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P} (w : CategoryTheory.CommSq f g inl inr) (h : CategoryTheory.Limits.IsColimit w.cocone),
  CategoryTheory.IsPushout f g inl inr
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.preEquivalence.inverse_map_left_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e)
  {X Y : CategoryTheory.CostructuredArrow F f.left} (φ : X ⟶ Y),
  ((CategoryTheory.CostructuredArrow.preEquivalence.inverse F f).map φ).left.left = φ.left
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_ofList_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.HashSet.Raw.ofList l).getD k' fallback = k
-- Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
UpperHalfPlane.IsBoundedAtImInfty.eq_1 : ∀ {α : Type u_1} [inst : Norm α] (f : UpperHalfPlane → α),
  UpperHalfPlane.IsBoundedAtImInfty f = UpperHalfPlane.atImInfty.BoundedAtFilter f
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- Variant of `locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const`, using
`ValueDistribution.logCounting` instead of `locallyFinsuppWithin.logCounting`.
 -/
ValueDistribution.logCounting_zero_sub_logCounting_top_eq_circleAverage_sub_const : ∀ {R : ℝ} {f : ℂ → ℂ},
  Meromorphic f →
    R ≠ 0 →
      (ValueDistribution.logCounting f 0 - ValueDistribution.logCounting f ⊤) R =
        Real.circleAverage (fun x => Real.log ‖f x‖) 0 R - Real.log ‖meromorphicTrailingCoeffAt f 0‖
-- Init.Data.Array.Lemmas
Array.set_push : ∀ {α : Type u_1} {i : ℕ} {xs : Array α} {x y : α} {h : i < (xs.push x).size},
  (xs.push x).set i y h = if x_1 : i < xs.size then (xs.set i y x_1).push x else xs.push y
-- Lean.Elab.InfoTree.Types
Lean.Elab.CommandContextInfo.mk : Lean.Environment →
  Option Lean.Environment →
    Lean.FileMap →
      Lean.MetavarContext →
        Lean.Options → Lean.Name → List Lean.OpenDecl → Lean.NameGenerator → Lean.Elab.CommandContextInfo
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.ModuleColimit.homEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.IsCofiltered C] [inst_3 : CategoryTheory.InitiallySmall C]
  {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R}
  (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf}
  (hcM : CategoryTheory.Limits.IsColimit cM) {N : ModuleCat ↑cR.pt} (β : M ⟶ (PresheafOfModules.constFunctor cR).obj N)
  {X : Cᵒᵖ} (x : ↑(M.obj X)),
  (CategoryTheory.ConcreteCategory.hom ((PresheafOfModules.ModuleColimit.homEquiv hcR hcM).symm β))
      ((CategoryTheory.ConcreteCategory.hom (cM.ι.app X)) x) =
    (CategoryTheory.ConcreteCategory.hom (β.app X)) x
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.toRows₂_apply : ∀ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ ⊕ m₂) n R) (i : m₂) (j : n),
  A.toRows₂ i j = A (Sum.inr i) j
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.any_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {p : α → Bool},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.any p = t₂.any p
-- Init.Data.UInt.Bitwise
UInt64.shiftLeft_add : ∀ {a b c : UInt64}, b < 64 → c < 64 → b + c < 64 → a <<< (b + c) = a <<< b <<< c
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.length_eq_of_isEmpty : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R) [IsEmpty R] (s : Set R),
  f.length s = 0
-- Lean.Parser.Level
Lean.Parser.Level.addLit.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Order.Bounds.Basic
directedOn_or_directedOn_of_union : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) (s ∪ t) → DirectedOn (fun x1 x2 => x1 ≤ x2) s ∨ DirectedOn (fun x1 x2 => x1 ≤ x2) t
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α} (h : t.WF),
  (Std.TreeMap.Raw.filter f t).getKey? k = (t.getKey? k).pfilter fun x h' => f x t[x]
-- Lean.Meta.TryThis
/-- How to represent the suggestion as `MessageData`. This is used only in the text of the
widget diagnostic.
If `none`, we use `suggestion`. Use `toMessageData` to render a `Suggestion` in this manner.  -/
Lean.Meta.Tactic.TryThis.Suggestion.messageData? : Lean.Meta.Tactic.TryThis.Suggestion → Option Lean.MessageData
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.pushforward_toPreZeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C}
  [inst_1 : J.IsStableUnderComposition] [inst_2 : J.HasIsos] {X Y : C} (f : X ⟶ Y)
  (hf : CategoryTheory.Presieve.singleton f ∈ J.coverings Y) (E : J.ZeroHypercover X),
  (CategoryTheory.Precoverage.ZeroHypercover.pushforward f hf E).toPreZeroHypercover =
    CategoryTheory.PreZeroHypercover.pushforward f E.toPreZeroHypercover
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the right whiskering `η ▷ h`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂.whiskerRightM : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadMor₂ m] →
    Mathlib.Tactic.BicategoryLike.Mor₂ → Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.Mor₂
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_map : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (p : Polynomial R) (f : R →+* S) (k : ℕ),
  (⇑Polynomial.derivative)^[k] (Polynomial.map f p) = Polynomial.map f ((⇑Polynomial.derivative)^[k] p)
-- Mathlib.Topology.Bornology.BoundedOperation
sub_bounded_of_bounded_of_bounded : ∀ {R : Type u_1} {X : Type u_2} [inst : PseudoMetricSpace R] [inst_1 : Sub R] [BoundedSub R] {f g : X → R},
  (∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C) →
    (∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C) → ∃ C, ∀ (x y : X), dist ((f - g) x) ((f - g) y) ≤ C
-- Init.Data.List.Lemmas
List.getD_cons_succ : ∀ {α : Type u_1} {x : α} {xs : List α} {n : ℕ} {d : α}, (x :: xs).getD (n + 1) d = xs.getD n d
-- Mathlib.Algebra.BigOperators.ModEq
Int.ModEq.listProd_map_one : ∀ {α : Type u_1} {n : ℤ} {l : List α} {f : α → ℤ}, (∀ x ∈ l, f x ≡ 1 [ZMOD n]) → (List.map f l).prod ≡ 1 [ZMOD n]
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- If `f` is multilinear, then `f (Σ_{j₁} g₁ j₁, ..., Σ_{jₙ} gₙ jₙ)` is the sum of
`f (g₁ (r 1), ..., gₙ (r n))` where `r` ranges over all functions `r`. This follows from
multilinearity by expanding successively with respect to each coordinate.  -/
MultilinearMap.map_sum : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) {α : ι → Type u_1} (g : (i : ι) → α i → M₁ i)
  [inst_5 : DecidableEq ι] [inst_6 : Fintype ι] [inst_7 : (i : ι) → Fintype (α i)],
  (f fun i => ∑ j, g i j) = ∑ r, f fun i => g i (r i)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.ArchimedeanStrata.archimedean_stratum : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] (u : HahnEmbedding.ArchimedeanStrata K M)
  {c : FiniteArchimedeanClass M}, Archimedean ↥(u.stratum c)
-- Lean.Elab.Tactic.Grind.Param
_private.Lean.Elab.Tactic.Grind.Param.0.Lean.Meta.Grind.ExtensionStateArray.getKindsFor : Lean.Meta.Grind.ExtensionStateArray → Lean.Meta.Grind.Origin → List Lean.Meta.Grind.EMatchTheoremKind
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.map_swap_add : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (v : ι → M)
  [inst_5 : DecidableEq ι] {i j : ι}, i ≠ j → f (v ∘ ⇑(Equiv.swap i j)) + f v = 0
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.normedGroup : {E : Type u_2} → [NormedGroup E] → NormedGroup (ULift.{u_5, u_2} E)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- Multiplying each column by a fixed `v j` multiplies the determinant by
the product of the `v`s.  -/
Matrix.det_mul_column : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (v : n → R)
  (A : Matrix n n R), (Matrix.of fun i j => v i * A i j).det = (∏ i, v i) * A.det
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.unit_actionHomRight : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {x y : D} (f : x ⟶ y),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f
      (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso x).hom
      (CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso y).inv)
-- Mathlib.Data.Finset.Card
/-- Specialization of `Finset.card_nbij` that automatically fills in most arguments.

See `Fintype.card_bijective` for the version where `s` and `t` are `univ`.  -/
Finset.card_bijective : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (e : α → β),
  Function.Bijective e → (∀ (i : α), i ∈ s ↔ e i ∈ t) → s.card = t.card
-- Mathlib.Topology.Order.UpperLowerSetTopology
/-- The lower set topology is the topology where the open sets are the lower sets. In general the lower
set topology does not coincide with the lower topology.
 -/
Topology.IsLowerSet : (α : Type u_4) → [t : TopologicalSpace α] → [Preorder α] → Prop
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.toEquiv_reindexAddEquiv : ∀ {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} (R : Type u_11) [inst : Add R] (eₘ : m ≃ m')
  (eₙ : n ≃ n'), ↑(Matrix.reindexAddEquiv R eₘ eₙ) = Matrix.reindex eₘ eₙ
-- Mathlib.Analysis.Normed.Group.Quotient
/-- `IsQuotient f`, for `f : M ⟶ N` means that `N` is isomorphic to the quotient of `M`
by the kernel of `f`.  -/
NormedAddGroupHom.IsQuotient : {M : Type u_1} →
  {N : Type u_2} →
    [inst : SeminormedAddCommGroup M] → [inst_1 : SeminormedAddCommGroup N] → NormedAddGroupHom M N → Prop
-- Mathlib.Data.List.Palindrome
List.Palindrome.below.cons_concat : ∀ {α : Type u_1} {motive : (a : List α) → a.Palindrome → Prop} (x : α) {l : List α} (a : l.Palindrome),
  List.Palindrome.below a → motive l a → List.Palindrome.below ⋯
-- Mathlib.Algebra.Group.Ideal
SemigroupIdeal.FG.eq_1 : ∀ {M : Type u_1} [inst : Mul M] (I : SemigroupIdeal M), I.FG = ∃ s, s.Finite ∧ I = SemigroupIdeal.closure s
-- Init.Data.List.Basic
/-- Returns a pair of lists that together contain all the elements of `as`. The first list contains
those elements for which `p` returns `true`, and the second contains those for which `p` returns
`false`.

`O(|l|)`. `as.partition p` is equivalent to `(as.filter p, as.filter (not ∘ p))`, but it is slightly
more efficient since it only has to do one pass over the list.

Examples:
 * `[1, 2, 5, 2, 7, 7].partition (· > 2) = ([5, 7, 7], [1, 2, 2])`
 * `[1, 2, 5, 2, 7, 7].partition (fun _ => false) = ([], [1, 2, 5, 2, 7, 7])`
 * `[1, 2, 5, 2, 7, 7].partition (fun _ => true) = ([1, 2, 5, 2, 7, 7], [])`
 -/
List.partition : {α : Type u} → (α → Bool) → List α → List α × List α
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.id_toHom : ∀ (X : AlgebraicGeometry.LocallyRingedSpace),
  (CategoryTheory.CategoryStruct.id X).toHom = CategoryTheory.CategoryStruct.id X.toPresheafedSpace
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.instInhabitedDelabM : {α : Type} → Inhabited (Lean.PrettyPrinter.Delaborator.DelabM α)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instDivisionSemiring : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → DivisionSemiring (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] → DivisionSemiring (DirectLimit G f)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- **Alias** of the reverse direction of `measurableSet_inl_image`. -/
MeasurableSet.inl_image : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α},
  MeasurableSet s → MeasurableSet (Sum.inl '' s)
-- Mathlib.Topology.UniformSpace.Separation
SeparationQuotient.comap_map_mk_uniformity : ∀ {α : Type u} [inst : UniformSpace α],
  Filter.comap (Prod.map SeparationQuotient.mk SeparationQuotient.mk)
      (Filter.map (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (uniformity α)) =
    uniformity α
-- Mathlib.Order.Interval.Set.SuccPred
Set.Ici_succ_eq_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a : α),
  Set.Ici (Order.succ a) = Set.Ioi a
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.measurePreserving_prod_mul_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [ν.IsMulRightInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.1, z.2 * z.1)) (μ.prod ν) (μ.prod ν)
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.inducingFn_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul 𝕜₂ F] {f : E →SWOT[σ] F} {x : E} {y : StrongDual 𝕜₂ F},
  (ContinuousLinearMapWOT.inducingFn σ E F) f (x, y) = y (f x)
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C}
  {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.ProjectiveResolution Z}
  (f f_1 : P.complex ⟶ Q.complex) (e_f : f = f_1) (comm : CategoryTheory.CategoryStruct.comp f Q.π = 0),
  CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero f comm =
    CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero f_1 ⋯
-- Mathlib.Algebra.Homology.Embedding.TruncLE
/-- The morphism `K.truncLE' e ⟶ L.truncLE' e` induced by a morphism `K ⟶ L`.  -/
HomologicalComplex.truncLE'Map : {ι : 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 L : HomologicalComplex C c'} →
                (K ⟶ L) →
                  (e : c.Embedding c') →
                    [inst_2 : e.IsTruncLE] →
                      [inst_3 : ∀ (i' : ι'), K.HasHomology i'] →
                        [inst_4 : ∀ (i' : ι'), L.HasHomology i'] → K.truncLE' e ⟶ L.truncLE' e
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.equiv_fst : ∀ {A : Type u_2} {E : Type u_3} {F : Type u_4} (x : WithCStarModule A (E × F)),
  ((WithCStarModule.equiv A (E × F)) x).1 = x.1
-- Mathlib.Algebra.Category.MonCat.Adjunctions
AddMonCat.adjoinZero_obj_coe : ∀ (S : AddSemigrp), ↑(AddMonCat.adjoinZero.obj S) = WithZero ↑S
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α} {h' : k ∈ Std.ExtDTreeMap.filter f t},
  (Std.ExtDTreeMap.filter f t).get k h' = t.get k ⋯
-- Init.Data.List.Sort.Impl
/-- Faster version of `mergeSortTR`, which avoids unnecessary list reversals.
 -/
List.MergeSort.Internal.mergeSortTR₂ : {α : Type u_1} → List α → autoParam (α → α → Bool) List.MergeSort.Internal.mergeSortTR₂._auto_1 → List α
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.colorable_sum : ∀ {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} {n : ℕ},
  (G ⊕g H).Colorable n ↔ G.Colorable n ∧ H.Colorable n
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Constructor for natural isomorphisms between parallel pairs.  -/
CategoryTheory.Limits.parallelPairIsoMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C} →
      (p :
          F.obj CategoryTheory.Limits.WalkingParallelPair.zero ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.zero) →
        (q :
            F.obj CategoryTheory.Limits.WalkingParallelPair.one ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.one) →
          autoParam
              (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) q.hom =
                CategoryTheory.CategoryStruct.comp p.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.left))
              CategoryTheory.Limits.parallelPairIsoMk._auto_1 →
            autoParam
                (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.right) q.hom =
                  CategoryTheory.CategoryStruct.comp p.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.right))
                CategoryTheory.Limits.parallelPairIsoMk._auto_3 →
              (F ≅ G)
-- Mathlib.Algebra.Algebra.Operations
Submodule.mem_one : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] {x : A},
  x ∈ 1 ↔ ∃ y, (algebraMap R A) y = x
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.isBasis'_iff_isBasis_inter_ground : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis' I X ↔ M.IsBasis I (X ∩ M.E)
-- Init.Data.Nat.Dvd
Nat.dvd_antisymm : ∀ {m n : ℕ}, m ∣ n → n ∣ m → m = n
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.abs_tendsto_atBot : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜)
  [OrderTopology 𝕜], 0 < P.degree → Filter.Tendsto (fun x => |Polynomial.eval x P|) Filter.atBot Filter.atTop
-- Init.Data.List.Scan.Lemmas
List.getLast_scanr : ∀ {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : α → β → β} (h : List.scanr f b l ≠ []),
  (List.scanr f b l).getLast h = b
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.precomp_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} (I : S.Arrow) {Z : C} (g : Z ⟶ I.Y), (I.precomp g).f = CategoryTheory.CategoryStruct.comp g I.f
-- Mathlib.Algebra.Category.Grp.Colimits
/-- (internal implementation) The fact that the candidate colimit cocone constructed in
`colimitCocone` is the colimit.
 -/
AddCommGrpCat.Colimits.colimitCoconeIsColimit : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor J AddCommGrpCat) →
      [inst_1 : DecidableEq J] →
        [inst_2 : Small.{w, max u w} (AddCommGrpCat.Colimits.Quot F)] →
          CategoryTheory.Limits.IsColimit (AddCommGrpCat.Colimits.colimitCocone F)
-- Mathlib.Topology.Order.OrderClosed
lt_subset_interior_le : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {f g : β → α}
  [inst_3 : TopologicalSpace β], Continuous f → Continuous g → {b | f b < g b} ⊆ interior {b | f b ≤ g b}
-- Mathlib.RingTheory.ReesAlgebra
reesAlgebra.fg : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R}, I.FG → (reesAlgebra I).FG
-- Mathlib.Algebra.Polynomial.Basic
/-- The coefficients `ℕ →₀ R` of a polynomial in `R[X]`.  -/
Polynomial.toFinsupp : {R : Type u_1} → [inst : Semiring R] → Polynomial R → AddMonoidAlgebra R ℕ