mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Quaternion
Quaternion.star_eq_neg : ∀ {R : Type u_3} [inst : CommRing R] [NoZeroDivisors R] [CharZero R] {a : Quaternion R}, star a = -a ↔ a.re = 0
-- Mathlib.Data.SetLike.Basic
SetLike.instCoeSortType : {A : Type u_1} → {B : Type u_2} → [i : SetLike A B] → CoeSort A (Type u_2)
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.InjectiveResolution.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroObject C}
  {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {Z : C} {cocomplex : CochainComplex C ℕ}
  {injective :
    autoParam (∀ (n : ℕ), CategoryTheory.Injective (cocomplex.X n))
      CategoryTheory.InjectiveResolution.injective._autoParam}
  {hasHomology : ∀ (i : ℕ), HomologicalComplex.HasHomology cocomplex i}
  {ι : (CochainComplex.single₀ C).obj Z ⟶ cocomplex}
  {quasiIso : autoParam (QuasiIso ι) CategoryTheory.InjectiveResolution.quasiIso._autoParam}
  {cocomplex_1 : CochainComplex C ℕ}
  {injective_1 :
    autoParam (∀ (n : ℕ), CategoryTheory.Injective (cocomplex_1.X n))
      CategoryTheory.InjectiveResolution.injective._autoParam}
  {hasHomology_1 : ∀ (i : ℕ), HomologicalComplex.HasHomology cocomplex_1 i}
  {ι_1 : (CochainComplex.single₀ C).obj Z ⟶ cocomplex_1}
  {quasiIso_1 : autoParam (QuasiIso ι_1) CategoryTheory.InjectiveResolution.quasiIso._autoParam},
  { cocomplex := cocomplex, injective := injective, hasHomology := hasHomology, ι := ι, quasiIso := quasiIso } =
      { cocomplex := cocomplex_1, injective := injective_1, hasHomology := hasHomology_1, ι := ι_1,
        quasiIso := quasiIso_1 } →
    cocomplex = cocomplex_1 ∧ ι ≍ ι_1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.mapArrowRight_id : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {f₁ : CategoryTheory.Arrow C₁}
  {f₃ : CategoryTheory.Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom),
  sq₁₃.mapArrowRight sq₁₃ (CategoryTheory.CategoryStruct.id f₃) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk sq₁₃.π)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.ext : ∀ {M N : SemiNormedGrp₁} {f₁ f₂ : M ⟶ N},
  (∀ (x : M.carrier), ↑(SemiNormedGrp₁.Hom.hom f₁) x = ↑(SemiNormedGrp₁.Hom.hom f₂) x) → f₁ = f₂
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.dualBasis_repr_apply : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_9}
  [inst_3 : DecidableEq ι] [inst_4 : Finite ι] {B : LinearMap.BilinForm K V} (hB : B.Nondegenerate)
  (b : Module.Basis ι K V) (x : V) (i : ι), ((B.dualBasis hB b).repr x) i = (B x) (b i)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.iteratedSliceEquiv_unitIso : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X),
  f.iteratedSliceEquiv.unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun g =>
        CategoryTheory.Over.isoMk
          (CategoryTheory.Over.isoMk
            (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Over f)).obj g).left.left) ⋯)
          ⋯)
      ⋯
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isLittleO_neg_left`. -/
Asymptotics.IsLittleO.of_neg_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {f' : α → E'} {l : Filter α}, (fun x => -f' x) =o[l] g → f' =o[l] g
-- Mathlib.Geometry.Polygon.Basic
/-- The `edgeSet` is equivalent to the image of the `edgePath`.  -/
Polygon.edgeSet_eq_image_edgePath : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_3} {n : ℕ} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder R] (poly : Polygon P n) (i : Fin n),
  Polygon.edgeSet R poly i = ⇑(Polygon.edgePath R poly i) '' Set.Icc 0 1
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- Multiplicativity of leading coefficients  -/
MonomialOrder.leadingCoeff_mul : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
  {f g : MvPolynomial σ R}, m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
/-- The components of the colimit of a diagram of `PresheafedSpace C` is obtained
via taking componentwise limits.
 -/
AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit : {J : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [CategoryTheory.Limits.HasColimitsOfShape J TopCat] →
          [∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)] →
            [inst_4 : CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C] →
              (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) →
                [inst_5 : CategoryTheory.Limits.HasColimit F] →
                  (U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.colimit F)) →
                    (CategoryTheory.Limits.colimit F).presheaf.obj (Opposite.op U) ≅
                      CategoryTheory.Limits.limit (AlgebraicGeometry.PresheafedSpace.componentwiseDiagram F U)
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Split a set at the `i`th element, getting the first `i` and everything else.

```
splitAt 2 {a, b, c, d} = ({a, b}, {c, d})
splitAt 5 {a, b, c, d} = ({a, b, c, d}, ∅)
```  -/
Ordnode.splitAt : {α : Type u_1} → ℕ → Ordnode α → Ordnode α × Ordnode α
-- Batteries.Data.BinomialHeap.Basic
/-- `O(n log n)`. Construct a heap from a list by inserting all the elements.  -/
Batteries.BinomialHeap.ofArray : {α : Type u} → (le : α → α → Bool) → Array α → Batteries.BinomialHeap α le
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getEntryGT_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {h' : ∃ a ∈ t₁, cmp a k = Ordering.gt} (h : t₁.Equiv t₂), t₁.getEntryGT k h' = t₂.getEntryGT k ⋯
-- Init.Prelude
MonadEval.mk : {m : semiOutParam (Type u → Type v)} → {n : Type u → Type w} → ({α : Type u} → m α → n α) → MonadEval m n
-- Std.Data.HashMap.IteratorLemmas
_private.Std.Data.HashMap.IteratorLemmas.0.Std.HashMap.Raw.toList_inner : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β}, m.inner.toList = List.map (fun e => ⟨e.1, e.2⟩) m.toList
-- Std.Time.Zoned.TimeZone
Std.Time.instDecidableEqTimeZone.decEq : (x x_1 : Std.Time.TimeZone) → Decidable (x = x_1)
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.IsRkFinite.inter_right : ∀ {α : Type u_1} {M : Matroid α} {X Y : Set α}, M.IsRkFinite X → M.IsRkFinite (X ∩ Y)
-- Mathlib.Data.Finset.Powerset
Finset.powerset_nonempty : ∀ {α : Type u_1} (s : Finset α), s.powerset.Nonempty
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- The pointwise difference of two bounded continuous functions is again bounded continuous.  -/
BoundedContinuousFunction.instSub : {α : Type u} →
  [inst : TopologicalSpace α] →
    {R : Type u_2} →
      [inst_1 : PseudoMetricSpace R] →
        [inst_2 : Sub R] → [BoundedSub R] → [ContinuousSub R] → Sub (BoundedContinuousFunction α R)
-- Mathlib.RingTheory.Nilpotent.Basic
/-- **Alias** of `IsIdempotentElem.eq_zero_of_isNilpotent`. -/
IsNilpotent.eq_zero_of_isIdempotentElem : ∀ {R : Type u_1} [inst : MonoidWithZero R] {e : R}, IsIdempotentElem e → IsNilpotent e → e = 0
-- Mathlib.CategoryTheory.ObjectProperty.SiteLocal
CategoryTheory.ObjectProperty.IsLocal.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C}
  {K : CategoryTheory.Precoverage C} [toIsClosedUnderIsomorphisms : P.IsClosedUnderIsomorphisms],
  (∀ {X : C} {R : CategoryTheory.Presieve X}, R ∈ K.coverings X → ∀ {Y : C} (f : Y ⟶ X), R f → P X → P Y) →
    (∀ {X : C} {R : CategoryTheory.Presieve X}, R ∈ K.coverings X → (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → P Y) → P X) →
      P.IsLocal K
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- (Implementation) The underlying space of `Spec(𝒪ₓ/I)` is homeomorphic to the support of `I`.  -/
AlgebraicGeometry.Scheme.IdealSheafData.gluedHomeo : {X : AlgebraicGeometry.Scheme} → (I : X.IdealSheafData) → ↥I.glueData.glued ≃ₜ ↥I.support
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- `G.killCopies H` is a subgraph of `G` where an *arbitrary* edge was removed from each copy of
`H` in `G`. By construction, it doesn't contain `H` (unless `H` had no edges) and has at most the
number of copies of `H` edges less than `G`. See `free_killCopies` and
`le_card_edgeFinset_killCopies` for these two properties.  -/
SimpleGraph.killCopies : {V : Type u_7} → {W : Type u_8} → SimpleGraph V → SimpleGraph W → SimpleGraph V
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
Std.Tactic.BVDecide.LRAT.Internal.Formula.readyForRupAdd_delete : ∀ {α : 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 ℕ),
  Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd f →
    Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd (Std.Tactic.BVDecide.LRAT.Internal.Formula.delete f arr)
-- Init.Data.UInt.Basic
/-- Converts 8-bit unsigned integers to word-sized unsigned integers.

This function is overridden at runtime with an efficient implementation.
 -/
UInt8.toUSize : UInt8 → USize
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.inter_smul_union_subset_union : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s₁ s₂ : Finset α} {t₁ t₂ : Finset β}
  [inst_2 : DecidableEq α], (s₁ ∩ s₂) • (t₁ ∪ t₂) ⊆ s₁ • t₁ ∪ s₂ • t₂
-- Mathlib.Order.Filter.AtTopBot.Finite
Filter.Tendsto.eventually_forall_ge_atTop : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] {l : Filter α} {p : β → Prop} {f : α → β},
  Filter.Tendsto f l Filter.atTop → (∀ᶠ (x : β) in Filter.atTop, p x) → ∀ᶠ (x : α) in l, ∀ (y : β), f x ≤ y → p y
-- Mathlib.Order.Bounds.Basic
IsGLB.dual : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α},
  IsGLB s a → IsLUB (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)
-- Mathlib.Analysis.CStarAlgebra.Exponential
selfAdjoint.expUnitary_coe : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : StarRing A] [inst_3 : ContinuousStar A]
  [inst_4 : CompleteSpace A] [inst_5 : StarModule ℂ A] (a : ↥(selfAdjoint A)),
  ↑(selfAdjoint.expUnitary a) = NormedSpace.exp (Complex.I • ↑a)
-- Mathlib.Analysis.Analytic.Polynomial
AnalyticOnNhd.eval_continuousLinearMap' : ∀ {𝕜 : Type u_1} {E : Type u_2} {B : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedCommRing B] [inst_4 : NormedAlgebra 𝕜 B] {σ : Type u_5} (f : σ → E →L[𝕜] B)
  (p : MvPolynomial σ B), AnalyticOnNhd 𝕜 (fun x => (MvPolynomial.eval fun x_1 => (f x_1) x) p) Set.univ
-- Mathlib.Geometry.Manifold.ContMDiffMap
/-- Bundled `n` times continuously differentiable maps,
denoted as `C^n(I, M; I', M')` and `C^n(I, M; k)` (when the target is a normed space `k` with
the trivial model) in the `Manifold` namespace.  -/
Manifold.«termC^_⟮_,_;_,_⟯» : Lean.ParserDescr
-- Mathlib.Combinatorics.Graph.Basic
Graph.vertexSet_noEdge : ∀ {α : Type u_1} (vertexSet : Set α) (β : Type u_3), (Graph.noEdge vertexSet β).vertexSet = vertexSet
-- Mathlib.Tactic.ReduceModChar
Tactic.ReduceModChar.TypeToCharPResult.failure.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)}, sizeOf Tactic.ReduceModChar.TypeToCharPResult.failure = 1
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.diam_range : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂),
  Metric.diam (Set.range ⇑f) = Metric.diam Set.univ
-- Init.Prelude
/-- Equality with `List.nil` is decidable even if the underlying type does not have decidable equality.
 -/
List.instDecidableNilEq : {α : Type u_1} → (a : List α) → Decidable ([] = a)
-- Mathlib.Logic.Equiv.Set
Equiv.Set.image_apply : ∀ {α : Type u_3} {β : Type u_4} (f : α → β) (s : Set α) (H : Function.Injective f) (p : ↑s),
  (Equiv.Set.image f s H) p = ⟨f ↑p, ⋯⟩
-- Mathlib.Algebra.Free
/-- The unique additive semigroup homomorphism that sends `of x` to `of (f x)`.  -/
FreeAddSemigroup.map : {α : Type u} → {β : Type v} → (α → β) → FreeAddSemigroup α →ₙ+ FreeAddSemigroup β
-- Mathlib.Algebra.Lie.Basis.Basic
/-- Lemma 4.4 from [Geck](Geck2017).  -/
LieAlgebra.Basis.borelUpper_le_biSup : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H) [inst_4 : Fintype ι] [IsDomain R]
  [CharZero R], b.borelUpper ≤ ⨆ n, ⨆ (_ : n ≠ 0), LieAlgebra.rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedGroup.toPseudoMetricSpace : {E : Type u_8} → [self : SeminormedGroup E] → PseudoMetricSpace E
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.mk_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOne N] (f : M →* N)
  (hmul : ∀ (x y : M), (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y), { toOneHom := ↑f, map_mul' := hmul } = f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_lt_pi_div_two : ∀ {x : ℝ}, Real.arccos x < Real.pi / 2 ↔ 0 < x
-- Mathlib.Order.Atoms
OrderDual.instIsSimpleOrder : ∀ {α : Type u_4} [inst : LE α] [inst_1 : BoundedOrder α] [IsSimpleOrder α], IsSimpleOrder αᵒᵈ
-- Mathlib.CategoryTheory.MorphismProperty.Quotient
CategoryTheory.MorphismProperty.HasQuotient.iff : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} (W : CategoryTheory.MorphismProperty C)
  {homRel : HomRel C} {inst_1 : CategoryTheory.HomRel.IsStableUnderPrecomp homRel}
  {inst_2 : CategoryTheory.HomRel.IsStableUnderPostcomp homRel} [self : W.HasQuotient homRel] ⦃X Y : C⦄ ⦃f g : X ⟶ Y⦄,
  homRel f g → (W f ↔ W g)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.insert k).min ⋯ = t.min?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Lean.Meta.Tactic.Induction
Lean.Meta.InductionSubgoal.mk.sizeOf_spec : ∀ (mvarId : Lean.MVarId) (fields : Array Lean.Expr) (subst : Lean.Meta.FVarSubst),
  sizeOf { mvarId := mvarId, fields := fields, subst := subst } = 1 + sizeOf mvarId + sizeOf fields + sizeOf subst
-- Mathlib.MeasureTheory.Group.Pointwise
MeasurableSet.const_vadd : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  [MeasurableConstVAdd G α] {s : Set α}, MeasurableSet s → ∀ (a : G), MeasurableSet (a +ᵥ s)
-- Mathlib.Topology.Separation.DisjointCover
/-- For any continuous function `f : X → V`, with `X` profinite, and `S` a neighbourhood of the
diagonal in `V × V`, the function `f` can be `S`-approximated by a function factoring through
`Fin n`, for some `n`.  -/
ContinuousMap.exists_finite_approximation_of_mem_nhds_diagonal : ∀ {X : Type u_1} {V : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace V] [TotallyDisconnectedSpace X]
  [T2Space X] [CompactSpace X] {S : Set (V × V)} (f : C(X, V)),
  S ∈ nhdsSet (Set.diagonal V) → ∃ n g h, Continuous g ∧ ∀ (x : X), (f x, h (g x)) ∈ S
-- Mathlib.Data.List.Forall2
List.Sublist.sublistForall₂ : ∀ {α : Type u_1} {Rₐ : α → α → Prop} {l₁ l₂ : List α}, l₁.Sublist l₂ → ∀ [Std.Refl Rₐ], List.SublistForall₂ Rₐ l₁ l₂
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- The measurable equivalence between the pi type over a sum type and a product of pi-types.
This is similar to `MeasurableEquiv.piEquivPiSubtypeProd`.  -/
MeasurableEquiv.sumPiEquivProdPi : {δ : Type u_4} →
  {δ' : Type u_5} →
    (α : δ ⊕ δ' → Type u_8) →
      [inst : (i : δ ⊕ δ') → MeasurableSpace (α i)] →
        ((i : δ ⊕ δ') → α i) ≃ᵐ ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i'))
-- Mathlib.Analysis.Convex.Combination
Finset.centerMass_smul_left : ∀ {R : Type u_1} {R' : Type u_2} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : Field R']
  [inst_2 : AddCommGroup E] [inst_3 : Module R E] (t : Finset ι) {w : ι → R} (z : ι → E) {c : R'} [inst_4 : Module R' R]
  [inst_5 : Module R' E] [SMulCommClass R' R R] [IsScalarTower R' R R] [SMulCommClass R R' E] [IsScalarTower R' R E],
  c ≠ 0 → t.centerMass (c • w) z = t.centerMass w z
-- Batteries.Data.List.Basic
List.tailsTR.go.eq_2 : ∀ {α : Type u_1} (acc : Array (List α)) (a : α) (l_1 : List α),
  List.tailsTR.go (a :: l_1) acc = List.tailsTR.go l_1 (acc.push (a :: l_1))
-- Mathlib.Order.Fin.Basic
Fin.instMin_mathlib : {n : ℕ} → Min (Fin n)
-- Std.Data.DHashMap.RawDef
/-- Monadically computes a value by folding the given function over the mappings in the hash
map in some order.
 -/
Std.DHashMap.Raw.foldM : {α : Type u} →
  {β : α → Type v} →
    {δ : Type w} → {m : Type w → Type w'} → [Monad m] → (δ → (a : α) → β a → m δ) → δ → Std.DHashMap.Raw α β → m δ
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.one_apply_of_ne_zero : ∀ {M₀ : Type u_7} {N₀ : Type u_8} [inst : MulZeroOneClass M₀] [inst_1 : MulZeroOneClass N₀]
  [inst_2 : DecidablePred fun x => x = 0] [inst_3 : Nontrivial M₀] [inst_4 : NoZeroDivisors M₀] {x : M₀},
  x ≠ 0 → 1 x = 1
-- Init.Data.BitVec.Lemmas
BitVec.toFin_cast : ∀ {w v : ℕ} (h : w = v) (x : BitVec w), (BitVec.cast h x).toFin = Fin.cast ⋯ x.toFin
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.IsColimitCore.isColimit : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} (c : F.CoconeTypes)
  (hc : c.IsColimitCore), c.IsColimit
-- Mathlib.Data.Complex.Basic
Complex.normSq_eq_conj_mul_self : ∀ {z : ℂ}, ↑(Complex.normSq z) = (starRingEnd ℂ) z * z
-- Batteries.Data.UnionFind.Basic
/-- Rank of a union-find node, defaults to 0 when the node is a root  -/
Batteries.UnionFind.rankD : Array Batteries.UFNode → ℕ → ℕ
-- Mathlib.Lean.Meta.CongrTheorems
/-- Generates a congruence lemma for a function `f` for `numArgs` of its arguments.
The only `Lean.Meta.CongrArgKind` kinds that appear in such a lemma
are `.eq`, `.heq`, and `.subsingletonInst`.
The resulting lemma proves either an `Eq` or a `HEq` depending on whether the types
of the LHS and RHS are equal or not.

This function is a wrapper around `Lean.Meta.mkHCongrWithArity`.
It transforms the resulting congruence lemma by trying to automatically prove hypotheses
using subsingleton lemmas, and if they are so provable they are recorded with `.subsingletonInst`.
Note that this is slightly abusing `.subsingletonInst` since
(1) the argument might not be for a `Decidable` instance and
(2) the argument might not even be an instance.  -/
Lean.Meta.mkHCongrWithArity' : Lean.Expr → ℕ → Lean.MetaM Lean.Meta.CongrTheorem
-- Init.Grind.Attr
/-- The `inj` modifier marks injectivity theorems for use by `grind`.
The conclusion of the theorem must be of the form `Function.Injective f`
where the term `f` contains at least one constant symbol.
 -/
Lean.Parser.Attr.grindInj : Lean.ParserDescr
-- Mathlib.LinearAlgebra.FixedSubmodule
LinearMap.fixedSubmodule_inf_fixedSubmodule_le_comp : ∀ {R : Type u_1} [inst : Semiring R] {V : Type u_3} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] (f g : V →ₗ[R] V),
  f.fixedSubmodule ⊓ g.fixedSubmodule ≤ (f ∘ₗ g).fixedSubmodule
-- Mathlib.Algebra.Homology.Embedding.TruncGE
/-- Given an embedding `e : Embedding c c'` of complex shapes which satisfy `e.IsTruncGE`,
this is the (canonical) truncation functor
`HomologicalComplex C c' ⥤ HomologicalComplex C c`.  -/
ComplexShape.Embedding.truncGE'Functor : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        (e : c.Embedding c') →
          [e.IsTruncGE] →
            (C : Type u_4) →
              [inst : CategoryTheory.Category.{v_2, u_4} C] →
                [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
                  [CategoryTheory.CategoryWithHomology C] →
                    CategoryTheory.Functor (HomologicalComplex C c') (HomologicalComplex C c)
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
HasLineDerivWithinAt.lineDifferentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {f' : F}
  {s : Set E} {x v : E}, HasLineDerivWithinAt 𝕜 f f' s x v → LineDifferentiableWithinAt 𝕜 f s x v
-- Mathlib.Logic.Equiv.Fin.Rotate
lt_finRotate_iff_ne_last : ∀ {n : ℕ} (i : Fin (n + 1)), i < (finRotate (n + 1)) i ↔ i ≠ Fin.last n
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
/-- Given a Cartesian morphism `φ : a ⟶ b` lying over `f : R ⟶ S` in `𝒳`, and two morphisms
`ψ ψ' : a' ⟶ a` such that `ψ ≫ φ = ψ' ≫ φ`. Then we must have `ψ = ψ'`.  -/
CategoryTheory.Functor.IsCartesian.ext : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : 𝒳}
  (ψ ψ' : a' ⟶ a) [p.IsHomLift (CategoryTheory.CategoryStruct.id R) ψ]
  [p.IsHomLift (CategoryTheory.CategoryStruct.id R) ψ'],
  CategoryTheory.CategoryStruct.comp ψ φ = CategoryTheory.CategoryStruct.comp ψ' φ → ψ = ψ'
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Extension.State : Type
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.cos_neg_iff_pi_div_two_lt_abs_toReal : ∀ {θ : Real.Angle}, θ.cos < 0 ↔ Real.pi / 2 < |θ.toReal|
-- Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
AlgebraicGeometry.IsPreimmersion.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.IsPreimmersion
-- Mathlib.Data.List.DropRight
List.dropWhile_idempotent : ∀ {α : Type u_1} (p : α → Bool) (l : List α), List.dropWhile p (List.dropWhile p l) = List.dropWhile p l
-- Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
BoundedContinuousFunction.isBounded_range_integral : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [OpensMeasurableSpace X] [SecondCountableTopology E] [inst_5 : MeasurableSpace E] [BorelSpace E]
  [inst_7 : NormedSpace ℝ E] {ι : Type u_3} (μs : ι → MeasureTheory.Measure X)
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] (f : BoundedContinuousFunction X E),
  Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)
-- Init.Data.BitVec.Lemmas
BitVec.sdiv_one : ∀ {w : ℕ} {x : BitVec w}, x.sdiv 1#w = x
-- Mathlib.AlgebraicGeometry.Restrict
/-- The restriction of an open cover to an open subset.  -/
AlgebraicGeometry.Scheme.OpenCover.restrict : {X : AlgebraicGeometry.Scheme} → X.OpenCover → (U : X.Opens) → (↑U).OpenCover
-- Mathlib.RingTheory.PowerBasis
PowerBasis.exists_gen_dvd_sub : ∀ {A : Type u_4} {B : Type u_5} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (pb : PowerBasis A B)
  (b : B), ∃ a, pb.gen ∣ b - (algebraMap A B) a
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.smul_ofGroup : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g₁ g₂ : G),
  g₁ • HNNExtension.NormalWord.ofGroup g₂ = HNNExtension.NormalWord.ofGroup (g₁ * g₂)
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_neg : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : HasDistribNeg α] [inst_2 : NormalizedGCDMonoid α] {a b : α},
  gcd a (-b) = gcd a b
-- Mathlib.Data.Set.Finite.Basic
Finset.exists_card_eq : ∀ {α : Type u} [Infinite α] (n : ℕ), ∃ s, s.card = n
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.combineC : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → ℕ → Lean.Grind.CommRing.Poly