mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.dropPrefix?_slice_of_isEmpty : ∀ {pat : String.Slice} {s : String}, pat.isEmpty = true → s.dropPrefix? pat = some s.toSlice
-- Mathlib.RingTheory.Flat.Basic
Module.Flat.instTensorProduct : ∀ {R : Type u} {M : Type v} {N : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {S : Type u_4} [inst_5 : CommSemiring S] [inst_6 : Algebra R S]
  [inst_7 : Module S M] [inst_8 : IsScalarTower R S M] [Module.Flat S M] [Module.Flat R N],
  Module.Flat S (TensorProduct R M N)
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_eq_ofNat_iff : ∀ {a : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo], Cardinal.lift.{v, u} a = OfNat.ofNat n ↔ a = OfNat.ofNat n
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.presheaf_obj_coe : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R) (X : Cᵒᵖ), ↑(M.presheaf.obj X) = ↑(M.obj X)
-- Lean.Meta.Tactic.Symm
/-- Environment extensions for symm lemmas  -/
Lean.Meta.Symm.symmExt : Lean.SimpleScopedEnvExtension (Lean.Name × Array Lean.Meta.DiscrTree.Key) (Lean.Meta.DiscrTree Lean.Name)
-- Lean.Syntax
Lean.Syntax.getRange? : Lean.Syntax → optParam Bool false → Option Lean.Syntax.Range
-- Mathlib.ModelTheory.Types
/-- A complete type over a given theory in a certain type of variables is a maximally
consistent (with the theory) set of formulas in that type.  -/
FirstOrder.Language.Theory.CompleteType : {L : FirstOrder.Language} → L.Theory → Type w → Type (max (max u v) w)
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkSpecializes_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (F : TopCat.Presheaf C X) {x y z : ↑X} (h : x ⤳ y) (h' : y ⤳ z) {Z : C} (h_1 : F.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h')
      (CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h) h_1) =
    CategoryTheory.CategoryStruct.comp (F.stalkSpecializes ⋯) h_1
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.IsFragment.congr_simp : ∀ {G : Type u_1} [inst : Group G] {inst_1 : DecidableEq G} [inst_2 : DecidableEq G] (K K_1 : ℝ),
  K = K_1 →
    ∀ (S S_1 : Finset G),
      S = S_1 → ∀ (A A_1 : Finset G), A = A_1 → Finset.IsFragment✝ K S A = Finset.IsFragment✝ K_1 S_1 A_1
-- Init.Data.Array.Lemmas
Array.foldrM_fold_empty : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {f : α → β → m β} {init : β} {i j : ℕ}
  (h : j ≤ #[].size), Array.foldrM.fold f #[] i j h init = pure init
-- Mathlib.Tactic.NormNum.Ordinal
Mathlib.Meta.NormNum.isNat_ordinalLT_false : ∀ {a b : Ordinal.{u}} {an bn : ℕ},
  Mathlib.Meta.NormNum.IsNat a an → Mathlib.Meta.NormNum.IsNat b bn → decide (an < bn) = false → ¬a < b
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
/-- An alternative formulation of the sheaf condition
(which we prove equivalent to the usual one below as
`isSheaf_iff_isSheafPreservesLimitPairwiseIntersections`).

A presheaf is a sheaf if `F` preserves the limit of `Pairwise.diagram U`.
(Recall `Pairwise.diagram U` is the diagram consisting of the pairwise intersections
`U i ⊓ U j` mapping into the open sets `U i`. This diagram has limit `iSup U`.)
 -/
TopCat.Presheaf.IsSheafPreservesLimitPairwiseIntersections : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {X : TopCat} → TopCat.Presheaf C X → Prop
-- Mathlib.Algebra.Torsor.Defs
Torsor.subsingleton_iff : ∀ (G : Type u_1) (P : Type u_2) [inst : Group G] [Torsor G P], Subsingleton G ↔ Subsingleton P
-- Mathlib.Data.NNReal.Defs
Real.ofNat_lt_toNNReal : ∀ {r : ℝ} {n : ℕ} [inst : n.AtLeastTwo], OfNat.ofNat n < r.toNNReal ↔ ↑n < r
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {h' : a ∈ t.erase k}, (t.erase k).getKey a h' = t.getKey a ⋯
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp]
  (t t_1 : Std.ExtDTreeMap α β cmp) (e_t : t = t_1) (a : α) (h : a ∈ t), t.get a h = t_1.get a ⋯
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], ⌈OfNat.ofNat n⌉ₑ = OfNat.ofNat n
-- Mathlib.Analysis.Normed.Ring.Basic
/-- This inequality is particularly useful when `c = 1` and `‖a‖ = ‖b‖ = 1` as it then shows that
chord length is a metric on the unit complex numbers.  -/
nnnorm_sub_mul_le : ∀ {α : Type u_2} [inst : SeminormedRing α] {a b c : α}, ‖a‖₊ ≤ 1 → ‖c - a * b‖₊ ≤ ‖c - a‖₊ + ‖1 - b‖₊
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
QuadraticMap.Isometry.ofEq_apply : ∀ {R : Type u_1} {M₁ : Type u_3} {N : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M₁] [inst_4 : Module R N] {Q₁ Q₂ : QuadraticMap R M₁ N} (h : Q₁ = Q₂)
  (x : M₁), (QuadraticMap.Isometry.ofEq h) x = x
-- Mathlib.Logic.Equiv.Prod
/-- A family of equivalences `∀ (a : α₁), β₁ ≃ β₂` generates an equivalence
between `α₁ × β₁` and `α₁ × β₂`.  -/
Equiv.prodCongrRight : {α₁ : Type u_9} → {β₁ : Type u_11} → {β₂ : Type u_12} → (α₁ → β₁ ≃ β₂) → α₁ × β₁ ≃ α₁ × β₂
-- Mathlib.Algebra.Group.Subgroup.Actions
AddSubgroup.vaddCommClass_right : ∀ {G : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddGroup G] [inst_1 : VAdd α β] [inst_2 : AddAction G β]
  [VAddCommClass α G β] (S : AddSubgroup G), VAddCommClass α (↥S) β
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_zero_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E), inner 𝕜 0 x = 0
-- Lean.Parser.Term.Basic
Lean.Parser.Term.binderTactic : Lean.Parser.Parser
-- Mathlib.Analysis.SpecificLimits.Normed
/-- **Dirichlet's test** for monotone sequences.  -/
Monotone.cauchySeq_series_mul_of_tendsto_zero_of_bounded : ∀ {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {b : ℝ} {f : ℕ → ℝ} {z : ℕ → E},
  Monotone f →
    Filter.Tendsto f Filter.atTop (nhds 0) →
      (∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b) → CauchySeq fun n => ∑ i ∈ Finset.range n, f i • z i
-- Mathlib.Algebra.Order.UpperLower
add_upperClosure : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α] (s t : Set α),
  s + ↑(upperClosure t) = ↑(upperClosure (s + t))
-- Mathlib.Computability.Partrec
Partrec.nat_rec : ∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α → ℕ} {g : α →. σ}
  {h : α → ℕ × σ →. σ},
  Computable f → Partrec g → Partrec₂ h → Partrec fun a => Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) (f a)
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.renameEquiv_apply : ∀ {σ : Type u_1} {τ : Type u_2} (R : Type u_4) [inst : CommSemiring R] (e : σ ≃ τ) (a : MvPowerSeries σ R),
  (MvPowerSeries.renameEquiv R e) a = (↑↑(MvPowerSeries.rename ⇑e).toRingHom).toFun a
-- Mathlib.AlgebraicTopology.ModelCategory.Basic
HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemCofibrationsTrivialFibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)
-- Init.Data.UInt.Bitwise
UInt8.ofNatLT_shiftLeft : ∀ {a b : ℕ} (ha : a <<< b < UInt8.size) (hb : b < 8),
  UInt8.ofNatLT (a <<< b) ha = UInt8.ofNatLT a ⋯ <<< UInt8.ofNatLT b ⋯
-- Mathlib.Topology.Algebra.Monoid
/-- Construct a bundled monoid homomorphism `M₁ →* M₂` from a function `f` and a proof that it
belongs to the closure of the range of the coercion from `M₁ →* M₂` (or another type of bundled
homomorphisms that has a `MonoidHomClass` instance) to `M₁ → M₂`.  -/
monoidHomOfMemClosureRangeCoe : {M₁ : Type u_6} →
  {M₂ : Type u_7} →
    [inst : TopologicalSpace M₂] →
      [T2Space M₂] →
        [inst_2 : MulOneClass M₁] →
          [inst_3 : MulOneClass M₂] →
            [ContinuousMul M₂] →
              {F : Type u_8} →
                [inst_5 : FunLike F M₁ M₂] →
                  [MonoidHomClass F M₁ M₂] → (f : M₁ → M₂) → f ∈ closure (Set.range fun f x => f x) → M₁ →* M₂
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.ofArrows.fac : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : C} {Y : I → C} {f : (i : I) → Y i ⟶ X}
  {W : C} {g : W ⟶ X} (hg : (CategoryTheory.Sieve.ofArrows Y f).arrows g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Sieve.ofArrows.h hg) (f (CategoryTheory.Sieve.ofArrows.i hg)) = g
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₁.id.sizeOf_spec : ∀ (e : Lean.Expr) (a : Mathlib.Tactic.BicategoryLike.Obj),
  sizeOf (Mathlib.Tactic.BicategoryLike.Mor₁.id e a) = 1 + sizeOf e + sizeOf a
-- Aesop.RuleTac.Basic
/-- The set of mvars that `goal` depends on.  -/
Aesop.RuleTacInput.mvars : Aesop.RuleTacInput → Aesop.UnorderedArraySet Lean.MVarId
-- Mathlib.Order.Bounds.Basic
bddAbove_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, BddAbove (Set.Iio a)
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.NatTrans.mapHomologicalComplex_app_f : ∀ {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] {F G : CategoryTheory.Functor W₁ W₂}
  [inst_4 : F.PreservesZeroMorphisms] [inst_5 : G.PreservesZeroMorphisms] (α : F ⟶ G) (c : ComplexShape ι)
  (C : HomologicalComplex W₁ c) (x : ι), ((CategoryTheory.NatTrans.mapHomologicalComplex α c).app C).f x = α.app (C.X x)
-- Mathlib.Data.Part
Part.instLawfulMonad : LawfulMonad Part
-- Mathlib.Data.Nat.Log
Nat.log_pos : ∀ {b n : ℕ}, 1 < b → b ≤ n → 0 < Nat.log b n
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.adjMatrix_add_compl_adjMatrix_eq_adjMatrix_completeGraph : ∀ (α : Type u_1) {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : DecidableEq V]
  [inst_2 : DecidableEq α] [inst_3 : AddZeroClass α] [inst_4 : One α],
  SimpleGraph.adjMatrix α G + (SimpleGraph.adjMatrix α G).compl = SimpleGraph.adjMatrix α (SimpleGraph.completeGraph V)
-- Std.Do.Triple.SpecLemmas
Std.Do.Invariant.eq_1 : ∀ {α : Type u₁} (xs : List α) (β : Type u₂) (ps : Std.Do.PostShape),
  Std.Do.Invariant xs β ps = Std.Do.PostCond (xs.Cursor × β) ps
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_le_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k km : α} (hc : t.contains k = true), t.minKey?.get ⋯ = km → (cmp km k).isLE = true
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.projectiveDimension_le_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C) (n : ℕ),
  CategoryTheory.projectiveDimension X ≤ ↑n ↔ CategoryTheory.HasProjectiveDimensionLE X n
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.leftUnitor_inv_iso_hom : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Pith B} (x : a ⟶ b),
  (CategoryTheory.Bicategory.leftUnitor x).inv.iso.hom = (CategoryTheory.Bicategory.leftUnitor x.of).inv
-- Mathlib.Data.EReal.Operations
EReal.neg_le_zero : ∀ {a : EReal}, -a ≤ 0 ↔ 0 ≤ a
-- Mathlib.AlgebraicGeometry.Birational.Composition
AlgebraicGeometry.Scheme.RationalMap.comp_assoc : ∀ {X₁ X₂ X₃ Y : AlgebraicGeometry.Scheme} [inst : PreirreducibleSpace ↥X₁] [inst_1 : IrreducibleSpace ↥X₂]
  [inst_2 : Nonempty ↥X₃] (f₁ : X₁.RationalMap X₂) [inst_3 : f₁.IsDominant] (f₂ : X₂.RationalMap X₃)
  [inst_4 : f₂.IsDominant] (f₃ : X₃.RationalMap Y), (f₁.comp f₂).comp f₃ = f₁.comp (f₂.comp f₃)
-- Std.Time.Format
/-- Parses a time string in the lean 24-hour format (`HH:mm:ss.SSSSSSSSS` or `HH:mm:ss`) and returns a `PlainTime`.
 -/
Std.Time.PlainTime.fromLeanTime24Hour : String → Except String Std.Time.PlainTime
-- Mathlib.Algebra.Group.Finsupp
Finsupp.eraseAddHom_apply : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] (a : ι) (f : ι →₀ M),
  (Finsupp.eraseAddHom a) f = Finsupp.erase a f
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.iteratedLineDerivOp_sum : ∀ {ι : Type u_1} {V : Type u_5} {E : Type u_6} [inst : LineDeriv V E E] {n : ℕ} (m : Fin n → V)
  [inst_1 : AddCommGroup V] [inst_2 : AddCommGroup E] [LineDerivAdd V E E] (f : ι → E) (s : Finset ι),
  LineDeriv.iteratedLineDerivOp m (∑ i ∈ s, f i) = ∑ i ∈ s, LineDeriv.iteratedLineDerivOp m (f i)
-- Init.Data.UInt.Lemmas
USize.ofBitVec_sub : ∀ (a b : BitVec System.Platform.numBits), { toBitVec := a - b } = { toBitVec := a } - { toBitVec := b }
-- Mathlib.LinearAlgebra.Matrix.Diagonal
LinearMap.rank_diagonal : ∀ {m : Type u_1} [inst : Fintype m] {K : Type u} [inst_1 : Field K] [inst_2 : DecidableEq m] [inst_3 : DecidableEq K]
  (w : m → K), (Matrix.toLin' (Matrix.diagonal w)).rank = ↑(Fintype.card { i // w i ≠ 0 })
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_wf : WellFounded fun x1 x2 => x1 ∈ x2
-- Mathlib.Combinatorics.Quiver.SingleObj
Quiver.SingleObj.pathToList_listToPath : ∀ {α : Type u_1} (l : List α), Quiver.SingleObj.pathToList (Quiver.SingleObj.listToPath l) = l
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.tensor_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M N : CategoryTheory.AddMon C),
  CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M.X N.X M.X N.X)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- If `h : is_zero X`, then `h.from_ Y` is a choice of unique morphism `Y → X`.

`from` is a reserved word, it was replaced by `from_`
 -/
CategoryTheory.Limits.IsZero.from_ : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X : C} → CategoryTheory.Limits.IsZero X → (Y : C) → Y ⟶ X
-- Init.Data.List.Basic
List.set.eq_1 : ∀ {α : Type u_1} (x head : α) (as : List α), (head :: as).set 0 x = x :: as
-- Mathlib.RingTheory.GradedAlgebra.Radical
Ideal.IsHomogeneous.radical : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : CommRing A] [inst_1 : AddCommMonoid ι] [inst_2 : LinearOrder ι]
  [IsOrderedCancelAddMonoid ι] [inst_4 : SetLike σ A] [inst_5 : AddSubmonoidClass σ A] {𝒜 : ι → σ}
  [inst_6 : GradedRing 𝒜] {I : Ideal A}, Ideal.IsHomogeneous 𝒜 I → Ideal.IsHomogeneous 𝒜 I.radical
-- Mathlib.Algebra.Order.Module.Equiv
coe_ofLexLinearEquiv : ∀ (α : Type u_1) (β : Type u_2) [inst : Semiring α] [inst_1 : AddCommMonoid β] [inst_2 : Module α β],
  ⇑(ofLexLinearEquiv α β) = ⇑ofLex
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The natural isomorphism `K.homology j ≅ (K.sc' i j k).homology`
for all homological complexes `K` when `c.prev j = i` and `c.next j = k`.  -/
HomologicalComplex.homologyFunctorIso' : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        (c : ComplexShape ι) →
          (i j k : ι) →
            [inst_2 : CategoryTheory.CategoryWithHomology C] →
              c.prev j = i →
                c.next j = k →
                  (HomologicalComplex.homologyFunctor C c j ≅
                    (HomologicalComplex.shortComplexFunctor' C c i j k).comp
                      (CategoryTheory.ShortComplex.homologyFunctor C))
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.comp_whisker_right : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b c : B} {f g h : CategoryTheory.FreeBicategory.Hom a b} (i : CategoryTheory.FreeBicategory.Hom b c)
  (η : CategoryTheory.FreeBicategory.Hom₂ f g) (θ : CategoryTheory.FreeBicategory.Hom₂ g h),
  CategoryTheory.FreeBicategory.Rel.below ⋯
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- When a short complex has homology, this is the canonical isomorphism
`S.leftHomology ≅ S.homology`.  -/
CategoryTheory.ShortComplex.leftHomologyIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [inst_2 : S.HasHomology] → S.leftHomology ≅ S.homology
-- Aesop.Search.Expansion.Norm
Aesop.normUnfoldCore : Lean.MVarId → Aesop.NormM (Option Aesop.NormRuleResult)
-- Mathlib.Tactic.FunProp.Mor
_private.Mathlib.Tactic.FunProp.Mor.0.Mathlib.Meta.FunProp.Mor.withApp.go : {α : Type} →
  (Lean.Expr → Array Mathlib.Meta.FunProp.Mor.Arg → Lean.MetaM α) →
    Lean.Expr → Array Mathlib.Meta.FunProp.Mor.Arg → Lean.MetaM α
-- Mathlib.Algebra.Order.Module.Defs
PosSMulMono.lift : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : SMul α β] [inst_4 : SMul α γ] (f : β → γ) [inst_5 : Zero α] [PosSMulMono α γ],
  (∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂) → (∀ (a : α) (b : β), f (a • b) = a • f b) → PosSMulMono α β
-- Mathlib.Order.PFilter
Order.PFilter.antitone_principal : ∀ {P : Type u_1} [inst : Preorder P], Antitone Order.PFilter.principal
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.ofList_nil : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α], Std.HashMap.Raw.ofList [] = ∅
-- Init.Data.Vector.Lemmas
Vector.length_toList : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, xs.toList.length = n
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
_private.Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass.0.PeriodPair.analyticAt_relation : ∀ (L : PeriodPair) (x : ℂ), AnalyticAt ℂ (PeriodPair.relation✝ L) x
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.equivToUnitHom_symm_coe : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (f : Rˣ →* R'ˣ) (a : Rˣ),
  (MulChar.equivToUnitHom.symm f) ↑a = ↑(f a)
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Pretty print a tactic with its docstring as hover info.

I would love to print `tac` with another colour, e.g. the keyword highlighting used by the editor,
but I have no idea how to do this.
 -/
Mathlib.Tactic.ClickSuggestions.tacticToHtml : Lean.TSyntax `tactic → Lean.MetaM ProofWidgets.Html
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.nondegenerate_iff_forall_vecMul_and_mulVec_eq_zero : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : CommSemiring R] {M : Matrix m n R} [inst_1 : Fintype m]
  [inst_2 : Fintype n],
  M.Nondegenerate ↔ (∀ (v : m → R), Matrix.vecMul v M = 0 → v = 0) ∧ ∀ (v : n → R), M.mulVec v = 0 → v = 0
-- Mathlib.Algebra.Star.Basic
StarMul.mk : {R : Type u} →
  [inst : Mul R] → [toInvolutiveStar : InvolutiveStar R] → (∀ (r s : R), star (r * s) = star s * star r) → StarMul R
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.CG.of_map_embedding : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {N : Type u_2} [inst_1 : L.Structure N]
  (f : L.Embedding M N) {s : L.Substructure M}, (FirstOrder.Language.Substructure.map f.toHom s).CG → s.CG
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inter_mul_subset : ∀ {α : Type u_2} [inst : Mul α] {s₁ s₂ t : Set α}, s₁ ∩ s₂ * t ⊆ s₁ * t ∩ (s₂ * t)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_braiding_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f g) (β_ X Y).hom =
    CategoryTheory.CartesianMonoidalCategory.lift g f
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- An inner product with a sum on the left, `Finsupp` version.  -/
Finsupp.sum_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {M : Type u_5} [inst_3 : Zero M] (l : ι →₀ M) (v : ι → M → E) (x : E),
  inner 𝕜 (l.sum v) x = l.sum fun i a => inner 𝕜 (v i a) x
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.addAux.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.lt) → (Unit → motive Ordering.eq) → (Unit → motive Ordering.gt) → motive x
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
/-- A morphism between presheafed spaces `X` and `Y` consists of a continuous map
`f` between the underlying topological spaces, and a (note: contravariant!) map
from the presheaf on `Y` to the pushforward of the presheaf on `X` via `f`.  -/
AlgebraicGeometry.PresheafedSpace.Hom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    AlgebraicGeometry.PresheafedSpace C → AlgebraicGeometry.PresheafedSpace C → Type (max u_2 v_1)
-- Init.System.IO
/-- Creates a new task that waits for all the tasks in the list `tasks` to complete, and then runs the
`IO` action `f` on their results. This new task has priority `prio`.

Running the resulting `BaseIO` action causes the task to be started eagerly. Unlike pure tasks
created by `Task.spawn`, tasks created by this function will run even if the last reference to the
task is dropped. The `act` should explicitly check for cancellation via `IO.checkCanceled` if it
should be terminated or otherwise react to the last reference being dropped.
 -/
BaseIO.mapTasks : {α : Type u_1} →
  {β : Type} →
    (List α → BaseIO β) →
      List (Task α) → optParam Task.Priority Task.Priority.default → optParam Bool false → BaseIO (Task β)
-- Mathlib.FieldTheory.AbelRuffini
IsSolvableByRad.below.rad : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  {motive : (a : E) → IsSolvableByRad F a → Prop} (α : E) (n : ℕ) (hn : n ≠ 0) (a : IsSolvableByRad F (α ^ n)),
  IsSolvableByRad.below a → motive (α ^ n) a → IsSolvableByRad.below ⋯
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.toSubring.eq_1 : ∀ {R : Type u_1} [inst : Ring R] (p : PowerSeries R) (T : Subring R) (hp : ∀ (n : ℕ), (PowerSeries.coeff n) p ∈ T),
  p.toSubring T hp = PowerSeries.mk fun n => ⟨(PowerSeries.coeff n) p, ⋯⟩
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
/-- Any continuous linear map to a locally compact space is a compact operator.  -/
isCompactOperator_of_locallyCompactSpace_dom : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  {M₂ : Type u_5} [inst_2 : TopologicalSpace M₁] [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M₁]
  [inst_5 : Module R₁ M₁] [inst_6 : AddCommGroup M₂] [inst_7 : Module R₂ M₂] [IsTopologicalAddGroup M₂]
  [LocallyCompactSpace M₂] (T : M₁ →SL[σ₁₂] M₂), IsCompactOperator ⇑T
-- Init.Data.Array.Basic
Array.foldlM.loop : {α : Type u} →
  {β : Type v} →
    {m : Type v → Type w} → [Monad m] → (β → α → m β) → (as : Array α) → (stop : ℕ) → stop ≤ as.size → ℕ → ℕ → β → m β
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.comp_right_injective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {P : Type u_1}
  [inst_2 : L.Structure P] (h : L.Equiv M N), Function.Injective fun f => f.comp h
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.UseImplicitLambdaResult.postpone.sizeOf_spec : sizeOf Lean.Elab.Term.UseImplicitLambdaResult.postpone = 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.comp_equiv_comp : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {K : Type v} [inst_1 : Field K] (f : F →+* K)
  {P Q : Fin 3 → F}, W.Nonsingular P → W.Nonsingular Q → (⇑f ∘ P ≈ ⇑f ∘ Q ↔ P ≈ Q)