mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Augment
_private.Mathlib.Algebra.Homology.Augment.0.ChainComplex.augment.match_3.eq_2 : ∀ (motive : ℕ → ℕ → Sort u_1) (i j : ℕ) (h_1 : Unit → motive 1 0) (h_2 : (i j : ℕ) → motive i.succ j.succ)
  (h_3 : (x x_1 : ℕ) → motive x x_1),
  (match i.succ, j.succ with
    | 1, 0 => h_1 ()
    | i.succ, j.succ => h_2 i j
    | x, x_1 => h_3 x x_1) =
    h_2 i j
-- Mathlib.Tactic.CategoryTheory.ToApp
/-- Recursive function which applies `mkLambdaFVars` stepwise
(so that each step can have different binderinfos)  -/
_private.Mathlib.Tactic.CategoryTheory.ToApp.0.Mathlib.Tactic.CategoryTheory.ToApp.toCatExpr.apprec : Array Lean.Expr → Array Lean.BinderInfo → Lean.Expr → Lean.Expr → ℕ → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.SumIntegralComparisons
/-- Bounds the difference between a sum and its partial sums by an integral.  -/
AntitoneOn.abs_tsum_sub_sum_range_le_integral : ∀ {f : ℝ → ℝ} {N : ℕ},
  1 ≤ N →
    AntitoneOn f (Set.Ici (↑N - 1)) →
      MeasureTheory.IntegrableOn f (Set.Ioi (↑N - 1)) MeasureTheory.volume →
        (∀ t ∈ Set.Ioi (↑N - 1), 0 ≤ f t) →
          |∑' (n : ℕ), f ↑n - ∑ n ∈ Finset.range N, f ↑n| ≤ ∫ (x : ℝ) in Set.Ioi (↑N - 1), f x
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.projectionL_eq_id_sub_projectionL : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} [inst_4 : IsTopologicalAddGroup M] (h : Submodule.IsTopCompl p q),
  q.projectionL p ⋯ = ContinuousLinearMap.id R M - p.projectionL q h
-- Mathlib.Analysis.Normed.Lp.lpSpace
PreLp.sub_apply : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {x y : PreLp E} {i : α},
  (x - y) i = x i - y i
-- Mathlib.Tactic.Abel
/-- The `Context` for a call to `abel`.

Stores a few options for this call, and caches some common subexpressions
such as typeclass instances and `0 : α`.
 -/
Mathlib.Tactic.Abel.Context : Type
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.ensureToHomoFieldDefEq : Lean.Expr →
  Lean.Expr →
    Lean.Name → Lean.Name → Lean.Level → Lean.Expr → optParam (Option Lean.Expr) none → Lean.Meta.Grind.GoalM Unit
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- If `R` satisfies the strong rank condition,
then for any linearly independent family `v : ι → M`
and any finite spanning set `w : Set M`,
the cardinality of `ι` is bounded by the cardinality of `w`.
 -/
linearIndependent_le_span : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {ι : Type u_2} (v : ι → M),
  LinearIndependent R v →
    ∀ (w : Set M) [inst_4 : Fintype ↑w], Submodule.span R w = ⊤ → Cardinal.mk ι ≤ ↑(Fintype.card ↑w)
-- Lean.Elab.DefView
Lean.Elab.Command.mkDefView : Lean.Elab.Modifiers → Lean.Syntax → Lean.Elab.Command.CommandElabM Lean.Elab.DefView
-- Mathlib.Util.FormatTable
instInhabitedAlignment : Inhabited Alignment
-- Mathlib.Algebra.Torsor.Basic
vsub_sub_vsub_comm : ∀ {G : Type u_1} {P : Type u_2} [inst : AddCommGroup G] [inst_1 : AddTorsor G P] (p₁ p₂ p₃ p₄ : P),
  p₁ -ᵥ p₂ - (p₃ -ᵥ p₄) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)
-- Mathlib.CategoryTheory.Adjunction.Lifting.Right
CategoryTheory.LiftRightAdjoint.otherMap.eq_1 : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {U : CategoryTheory.Functor A B} {F : CategoryTheory.Functor B A} (L : CategoryTheory.Functor C B)
  (U' : CategoryTheory.Functor A C) (adj₁ : F ⊣ U) (adj₂ : L.comp F ⊣ U') (X : B),
  CategoryTheory.LiftRightAdjoint.otherMap L U' adj₁ adj₂ X =
    CategoryTheory.CategoryStruct.comp (adj₂.unit.app (U'.1 (F.obj X)))
      (U'.map
        (F.map
          (CategoryTheory.CategoryStruct.comp (adj₁.unit.app (L.1 (U'.1 (F.obj X))))
            (U.map (adj₂.counit.app (F.obj X))))))
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedMonoid.instMonoid.eq_1 : ∀ {α : Type u_1} {rels : FreeMonoid α → FreeMonoid α → Prop},
  PresentedMonoid.instMonoid =
    { mul := PresentedMonoid.instMonoid._aux_1, mul_assoc := ⋯, one := PresentedMonoid.instMonoid._aux_4, one_mul := ⋯,
      mul_one := ⋯, npow := PresentedMonoid.instMonoid._aux_8, npow_zero := ⋯, npow_succ := ⋯ }
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instHasPushoutsAgainstOfHasPushouts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.HasPushouts]
  (P' : CategoryTheory.MorphismProperty C), P.HasPushoutsAgainst P'
-- Mathlib.NumberTheory.NumberField.House
NumberField.house_intCast : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : ℤ), NumberField.house ↑x = ↑|x|
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLin'OfInv_symm_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_4} {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1)
  (hM'M : M' * M = 1) (a : n → R) (a_1 : m), (Matrix.toLin'OfInv hMM' hM'M).symm a a_1 = (Matrix.toLin' M) a a_1
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.eval₂_cast_comp : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : σ → τ) (c : ℤ →+* R) (g : τ → R)
  (p : MvPolynomial σ ℤ), MvPolynomial.eval₂ c (g ∘ f) p = MvPolynomial.eval₂ c g ((MvPolynomial.rename f) p)
-- Init.Grind.Ring.Basic
Lean.Grind.Semiring.natCast_mul_comm : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a : ℕ) (b : α), ↑a * b = b * ↑a
-- Std.Data.TreeSet.Raw.Slice
Std.TreeSet.Raw.instSliceableRooSlice : {α : Type u} →
  (cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw.instSliceableRooSlice._auto_1) →
    Std.Roo.Sliceable (Std.TreeSet.Raw α cmp) α (Std.DTreeMap.Internal.Unit.RooSlice α)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
CategoryTheory.Over.sections_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (I : C) [inst_2 : CategoryTheory.Closed I]
  [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.curryRightUnitorHom I)] {X Y : CategoryTheory.Over I}
  (u : X ⟶ Y),
  (CategoryTheory.Over.sections I).map u =
    CategoryTheory.ChosenPullbacksAlong.pullbackMap ((CategoryTheory.ihom I).map Y.hom)
      (CategoryTheory.curryRightUnitorHom I) ((CategoryTheory.ihom I).map X.hom) (CategoryTheory.curryRightUnitorHom I)
      ((CategoryTheory.ihom I).map (CategoryTheory.Over.Hom.left u))
      (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.CategoryStruct.id (I ⟹ I)) ⋯ ⋯
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.lt_translationNumber_of_forall_add_lt : ∀ (f : CircleDeg1Lift), Continuous ⇑f → ∀ {z : ℝ}, (∀ (x : ℝ), x + z < f x) → z < f.translationNumber
-- Std.Time.Time.Unit.Basic
/-- Converts an `Hour.Offset` to a `Second.Offset`.
 -/
Std.Time.Second.Offset.ofHours : Std.Time.Hour.Offset → Std.Time.Second.Offset
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
/-- A concrete category is a category `C` where objects correspond to types and morphisms to
(bundled) functions between those types.

In other words, it has a fixed faithful functor `forget : C ⥤ Type`.

Note that `ConcreteCategory` potentially depends on three independent universe levels,
* the universe level `w` appearing in `forget : C ⥤ Type w`
* the universe level `v` of the morphisms (i.e. we have a `Category.{v} C`)
* the universe level `u` of the objects (i.e `C : Type u`)

They are specified that order, to avoid unnecessary universe annotations.
 -/
CategoryTheory.ConcreteCategory : (C : Type u) →
  [CategoryTheory.Category.{v, u} C] →
    (FC : outParam (C → C → Type u_1)) →
      {CC : outParam (C → Type w)} → [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] → Type (max (max u u_1) v)
-- Mathlib.Analysis.Normed.Module.Bases
/-- Composition of projections: `proj n (proj m x) = proj (min n m) x`.  -/
SchauderBasis.proj_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) (n m : ℕ) (x : X), (b.proj n) ((b.proj m) x) = (b.proj (min n m)) x
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
/-- See `MemLp.prod` for the unapplied version.  -/
MeasureTheory.MemLp.prod' : ∀ {ι : Type u_1} {α : Type u_2} {𝕜 : Type u_3} {x : MeasurableSpace α} [inst : NormedCommRing 𝕜]
  {μ : MeasureTheory.Measure α} {f : ι → α → 𝕜} {p : ι → ENNReal} {s : Finset ι},
  (∀ i ∈ s, MeasureTheory.MemLp (f i) (p i) μ) → MeasureTheory.MemLp (fun ω => ∏ i ∈ s, f i ω) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.mem_edges_toSubgraph : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {e : Sym2 V}, e ∈ p.toSubgraph.edgeSet ↔ e ∈ p.edges
-- Mathlib.Logic.Embedding.Basic
/-- An embedding as a function. Use coercion instead.  -/
Function.Embedding.toFun : {α : Sort u_1} → {β : Sort u_2} → (α ↪ β) → α → β
-- Mathlib.Order.Cover
Prod.swap_wcovBy_swap : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] {x y : α × β}, x.swap ⩿ y.swap ↔ x ⩿ y
-- Mathlib.Analysis.Matrix.PosDef
/-- The eigenvalues of a positive definite matrix are positive.  -/
Matrix.PosDef.eigenvalues_pos : ∀ {n : Type u_2} {𝕜 : Type u_3} [inst : Fintype n] [inst_1 : RCLike 𝕜] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.PosDef) (i : n), 0 < ⋯.eigenvalues i
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.mapCongr_hom_app_right : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) [inst_1 : Q.IsMultiplicative] [inst_2 : P.IsStableUnderComposition]
  [inst_3 : Q.RespectsIso] {X Y : T} {f g : X ⟶ Y} (hfg : f = g) (hf : P f) (X_1 : P.Under Q Y),
  ((CategoryTheory.MorphismProperty.Under.mapCongr Q hfg hf).hom.app X_1).right =
    CategoryTheory.CategoryStruct.id X_1.right
-- Mathlib.Data.Num.Basic
PosNum.decidableLE : DecidableLE PosNum
-- Std.Do.PredTrans
/-- The type of predicate transformers for a given `ps : PostShape` and return type `α : Type`. A
predicate transformer `x : PredTrans ps α` is a function that takes a postcondition `Q : PostCond α
ps` and returns a precondition `x.apply Q : Assertion ps`.
  -/
Std.Do.PredTrans : Std.Do.PostShape → Type u → Type u
-- Batteries.Recycling.RBTree.Basic
/-- The resulting tree is well formed.  -/
RBTree.RBSet.AlterWF.wf : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : RBTree.RBSet α cmp} {cut : α → Ordering} {f : Option α → Option α}
  [self : t.AlterWF cut f], RBTree.RBNode.WF cmp (RBTree.RBNode.alter cut f ↑t)
-- Mathlib.Algebra.Order.Group.Defs
neg_nonneg_of_nonpos : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a : α}, a ≤ 0 → 0 ≤ -a
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_add_one : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.U R (n + 1) = 2 * Polynomial.X * Polynomial.Chebyshev.U R n - Polynomial.Chebyshev.U R (n - 1)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.u : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Lean.Level
-- Mathlib.FieldTheory.KummerExtension
X_pow_sub_C_eq_prod : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {n : ℕ} {ζ : R},
  IsPrimitiveRoot ζ n →
    ∀ {α a : R},
      0 < n →
        α ^ n = a → Polynomial.X ^ n - Polynomial.C a = ∏ i ∈ Finset.range n, (Polynomial.X - Polynomial.C (ζ ^ i * α))
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.updateSetTag! : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu → Lean.FVarId → ℕ → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Init.Data.Fin.Lemmas
Fin.coeSucc_eq_succ : ∀ {n : ℕ} {a : Fin n}, a.castSucc + 1 = a.succ
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.instRingHomSurjectiveQuotientMk : ∀ {R : Type u} [inst : Ring R] {I : Ideal R} [inst_1 : I.IsTwoSided], RingHomSurjective (Ideal.Quotient.mk I)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₁₂.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃),
  h.p₁₂ = h.chosenPullback.p₁
-- Mathlib.Topology.Compactness.Lindelof
isLindelof_accumulate : ∀ {X : Type u} [inst : TopologicalSpace X] {K : ℕ → Set X},
  (∀ (n : ℕ), IsLindelof (K n)) → ∀ (n : ℕ), IsLindelof (Set.accumulate K n)
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.linearEquivFunOnFinite_symm_apply : ∀ (R : Type u_9) (M : Type u_11) (α : Type u_12) [inst : Finite α] [inst_1 : AddCommMonoid M] [inst_2 : Semiring R]
  [inst_3 : Module R M] (f : α → M), ⇑((Finsupp.linearEquivFunOnFinite R M α).symm f) = f
-- Mathlib.Logic.Nontrivial.Defs
not_nontrivial_iff_subsingleton : ∀ {α : Type u_1}, ¬Nontrivial α ↔ Subsingleton α
-- Std.Data.ExtTreeSet.Basic
/-- Tries to retrieve the smallest element that is less than the given element,
returning `fallback` if no such element exists.
 -/
Std.ExtTreeSet.getLTD : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → α → α → α
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.le_measure_symmDiff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α}, μ s₁ - μ s₂ ≤ μ (symmDiff s₁ s₂)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.restrictPreimage'_target : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) (s : Set B)
  [inst_3 : Nonempty (↑s → F → ↑(proj ⁻¹' s))],
  (e.restrictPreimage' s).target = Prod.map Subtype.val id ⁻¹' e.toPretrivialization.target
-- Mathlib.Tactic.Abel
/-- A synonym for `•`, used internally in `abel`.  -/
Mathlib.Tactic.Abel.smulg : {α : Type u_1} → [AddCommGroup α] → ℤ → α → α
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.IsInner.ne_last : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {inst : P.IsProper} [self : P.IsInner] (x : ↑P.II) {d : ℕ}
  (hd : (↑x).dim = d), ⋯.index hd ≠ Fin.last (d + 1)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddMemClass.mk_add_mk : ∀ {M : Type u_1} {A : Type u_3} [inst : Add M] [inst_1 : SetLike A M] [hA : AddMemClass A M] (S' : A) (x y : M)
  (hx : x ∈ S') (hy : y ∈ S'), ⟨x, hx⟩ + ⟨y, hy⟩ = ⟨x + y, ⋯⟩
-- Mathlib.Combinatorics.SetFamily.Shatter
/-- **Alias** of the reverse direction of `Finset.shatters_shatterer`. -/
Finset.Shatters.shatterer : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α}, 𝒜.Shatters s → 𝒜.shatterer.Shatters s
-- Mathlib.Algebra.Polynomial.CoeffList
/-- Only the zero polynomial has no coefficients.  -/
Polynomial.coeffList_eq_nil : ∀ {R : Type u_1} [inst : Semiring R] {P : Polynomial R}, P.coeffList = [] ↔ P = 0
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.map_symm_map : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {P' : Type u_3} [inst_3 : CommRing P'] [inst_4 : Algebra R P'] (I : FractionalIdeal S P') (g : P ≃ₐ[R] P'),
  FractionalIdeal.map (↑g) (FractionalIdeal.map (↑g.symm) I) = I
-- Mathlib.Order.Bounded
Set.bounded_lt_Ioc : ∀ {α : Type u_1} [inst : Preorder α] [NoMaxOrder α] (a b : α), Set.Bounded (fun x1 x2 => x1 < x2) (Set.Ioc a b)
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.injOn_pow_mul : ∀ {M₀ : Type u_7} [inst : CommMonoidWithZero M₀] [IsCancelMulZero M₀] {n : ℕ} {ζ : M₀},
  IsPrimitiveRoot ζ n → ∀ {α : M₀}, α ≠ 0 → Set.InjOn (fun x => ζ ^ x * α) ↑(Finset.range n)
-- Mathlib.Data.Seq.Computation
Computation.liftRel_def : ∀ {α : Type u} {β : Type v} {R : α → β → Prop} {ca : Computation α} {cb : Computation β},
  Computation.LiftRel R ca cb ↔ (ca.Terminates ↔ cb.Terminates) ∧ ∀ {a : α} {b : β}, a ∈ ca → b ∈ cb → R a b
-- Mathlib.Data.Ordmap.Ordnode
_private.Mathlib.Data.Ordmap.Ordnode.0.BinaryTree.toOrdNode.match_1.splitter : {α : Type u_1} →
  (motive : BinaryTree α → Sort u_2) →
    (x : BinaryTree α) →
      (Unit → motive BinaryTree.nil) → ((x : α) → (l r : BinaryTree α) → motive (BinaryTree.node x l r)) → motive x
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsRestriction.base_iff : ∀ {α : Type u_1} {M N : Matroid α}, N.IsRestriction M → ∀ {B : Set α}, N.IsBase B ↔ M.IsBasis B N.E
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.lt_rankMax : ∀ (self : Batteries.UnionFind) (i : ℕ), self.rank i < self.rankMax
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.functor_additive_iff : ∀ {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.Preadditive C]
  (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W]
  [W.HasLeftCalculusOfFractions] {E : Type u_3} [inst_5 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_6 : CategoryTheory.Preadditive E] [inst_7 : CategoryTheory.Preadditive D] [L.Additive]
  (G : CategoryTheory.Functor D E), G.Additive ↔ (L.comp G).Additive
-- Lean.Meta.Tactic.Grind.CheckResult
Lean.Meta.Grind.instReprCheckResult.repr : Lean.Meta.Grind.CheckResult → ℕ → Std.Format
-- Mathlib.Analysis.SpecificLimits.Basic
Filter.EventuallyEq.div_mul_cancel : ∀ {α : Type u_4} {G : Type u_5} [inst : GroupWithZero G] {f g : α → G} {l : Filter α},
  Filter.Tendsto g l (Filter.principal {0}ᶜ) → (fun x => f x / g x * g x) =ᶠ[l] fun x => f x
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.of.inj : ∀ {carrier : Type u_1} {str : PartialOrder carrier} {carrier_1 : Type u_1} {str_1 : PartialOrder carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Mathlib.CategoryTheory.Limits.Elements
CategoryTheory.Functor.Elements.isRepresentable_of_hasInitial : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type w))
  [CategoryTheory.Limits.HasInitial F.Elements], F.IsRepresentable
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
_private.Mathlib.Combinatorics.Extremal.RuzsaSzemeredi.0.mem_triangleIndices : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : CommRing α] {s : Finset α} {x : α × α × α},
  x ∈ triangleIndices✝ s ↔ ∃ y, ∃ a ∈ s, (y, y + a, y + 2 * a) = x
-- Mathlib.GroupTheory.Congruence.BigOperators
Con.coe_listProd : ∀ {ι : Type u_1} {M : Type u_2} [inst : MulOneClass M] (c : Con M) (l : List ι) (f : ι → M),
  ↑(List.map f l).prod = (List.map (fun i => ↑(f i)) l).prod
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.negPart_zero : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint], 0⁻ = 0
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
/-- Uniqueness part of **Sylvester's law of inertia** (positive part):
for any weighted sum of squares equivalent to `Q`,
the number of strictly positive weights is equal to `sigPos Q`.  -/
QuadraticForm.sigPos_of_equiv_weightedSumSquares : ∀ {M : Type u_2} [inst : AddCommGroup M] {𝕜 : Type u_4} [inst_1 : Field 𝕜] [inst_2 : LinearOrder 𝕜]
  [inst_3 : Module 𝕜 M] {Q : QuadraticForm 𝕜 M} {ι : Type u_5} [inst_4 : Fintype ι] {w : ι → 𝕜} [IsStrictOrderedRing 𝕜],
  QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares 𝕜 w) → sigPos Q = {i | 0 < w i}.ncard
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.isOrtho_span : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {s t : Set E}, Submodule.span 𝕜 s ⟂ Submodule.span 𝕜 t ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → inner 𝕜 u v = 0
-- Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
HomotopicalAlgebra.map_surjective_of_isLocalization : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {H : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} H] (L : CategoryTheory.Functor C H)
  [L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)] (X Y : C) [HomotopicalAlgebra.IsCofibrant X]
  [HomotopicalAlgebra.IsFibrant Y], Function.Surjective L.map
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderTriple.inv_eq : ∀ {p q r : NNReal}, p.HolderTriple q r → r⁻¹ = p⁻¹ + q⁻¹
-- Mathlib.CategoryTheory.Monoidal.Action.End
/-- If the action of `C` on `D` comes from a monoidal functor `C ⥤ (D ⥤ D)`,
then `curriedActionMop C D` is naturally isomorphic to that functor.  -/
CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionActionOfMonoidalFunctorToEndofunctorIso : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.MonoidalCategory C] →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) →
            [inst_3 : F.Monoidal] → CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction C D ≅ F
-- Mathlib.Algebra.GradedMulAction
/-- Associativity of `•` and `*`  -/
GradedMonoid.GMulAction.mul_smul : ∀ {ιA : Type u_1} {ιM : Type u_3} {A : ιA → Type u_4} {M : ιM → Type u_5} {inst : AddMonoid ιA} {inst_1 : VAdd ιA ιM}
  {inst_2 : GradedMonoid.GMonoid A} [self : GradedMonoid.GMulAction A M] (a a' : GradedMonoid A) (b : GradedMonoid M),
  (a * a') • b = a • a' • b
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_eq_some_get : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a : α}
  (h : a ∈ m), m.get? a = some (m.get a h)
-- Lean.Data.Lsp.Extra
Lean.Lsp.instInhabitedDependencyBuildMode : Inhabited Lean.Lsp.DependencyBuildMode
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.mkUnary : Lean.Name → Lean.Expr → ℚ × Lean.Expr → (ℚ → ℚ) → Lean.Meta.Grind.Arith.FieldNormNum.M✝ (ℚ × Lean.Expr)
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
LinearIsometryEquiv.hasFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {s : Set E} (iso : E ≃ₗᵢ[𝕜] F), HasFDerivWithinAt (⇑iso) (↑↑iso) s x
-- Lean.Structure
Lean.StructureResolutionOrderConflict.badParent : Lean.StructureResolutionOrderConflict → Lean.Name
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a : α} {v : β k}, (t.insert k v).contains a = (cmp k a == Ordering.eq || t.contains a)
-- Mathlib.Order.Fin.InsertNth
Fin.insertNth_zero_monotone : ∀ {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : Fin (n + 1) → α},
  Monotone f → ∀ x ≤ f 0, Monotone (Fin.insertNth 0 x f)
-- Mathlib.Algebra.Polynomial.Module.Basic
/-- This is required to have the `IsScalarTower S R M` instance to avoid diamonds.  -/
PolynomialModule.instModule : {R : Type u_2} →
  {M : Type u_3} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {S : Type u_5} → [inst_3 : CommSemiring S] → [Module S M] → Module S (PolynomialModule R M)