mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)} →
                {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} →
                  (obj : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })) →
                    (hom :
                        (i j : ι) →
                          (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶
                            (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj j)) →
                      (∀ (i : ι),
                          CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (f i)
                              (CategoryTheory.CategoryStruct.id (X i)) (CategoryTheory.CategoryStruct.id (X i)) ⋯ ⋯ =
                            CategoryTheory.CategoryStruct.id
                              ((F.map (CategoryTheory.CategoryStruct.id (X i)).op.toLoc).toFunctor.obj (obj i))) →
                        (∀ (i₁ i₂ i₃ : ι),
                            CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p
                                  (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯)
                                (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p
                                  (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) =
                              CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁
                                (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) →
                          F.DescentData' sq sq₃
-- Std.Http.Protocol.H1
/-- Maps a reader failure to an HTTP status code.  -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.errorResponseStatus : Std.Http.Protocol.H1.Error → Std.Http.Status
-- Init.Data.Vector.Lemmas
Vector.back?_eq_none_iff : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, xs.back? = none ↔ n = 0
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.forget₂_obj_moduleCat_of : ∀ (R : Type u) [inst : Semiring R] (X : Type v) [inst_1 : AddCommMonoid X] [inst_2 : Module R X],
  (CategoryTheory.forget₂ (SemimoduleCat R) AddCommMonCat).obj (SemimoduleCat.of R X) = AddCommMonCat.of X
-- Init.Data.Option.Lemmas
Option.some_eq_ite_none_left : ∀ {β : Type u_1} {a : β} {p : Prop} {x : Decidable p} {b : Option β}, (some a = if p then none else b) ↔ ¬p ∧ some a = b
-- Mathlib.Topology.UniformSpace.Cauchy
/-- A finite set is totally bounded.  -/
Set.Finite.totallyBounded : ∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α}, s.Finite → TotallyBounded s
-- Mathlib.Data.PFun
/-- Turn a total function into a partial function.  -/
PFun.lift : {α : Type u_1} → {β : Type u_2} → (α → β) → α →. β
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.instIsMultiplicativeSchemeSurjective : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.Surjective
-- Batteries.Data.String.Matcher
/-- Returns all the substrings of `s` that match `pattern`.
 -/
Substring.Raw.findAllSubstr : Substring.Raw → Substring.Raw → Array Substring.Raw
-- Mathlib.Topology.Semicontinuity.Defs
/-- A function `f : α → Set β` has open lower sections on `s` if it has open lower sections within
`s` at every `x ∈ s`.  -/
HasOpenLowerSectionsOn : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → (α → Set β) → Set α → Prop
-- Mathlib.Tactic.NormNum.GCD
Mathlib.Meta.NormNum.nat_gcd_helper_dvd_left : ∀ (x y : ℕ), y % x = 0 → x.gcd y = x
-- Mathlib.CategoryTheory.Filtered.Final
/-- The functor `CostructuredArrow T d ⥤ CostructuredArrow (T ⋙ S) e` that `u : S.obj d ⟶ e`
induces via `CostructuredArrow.map₂` is initial, if `T` and `S` are initial and the domain of `T` is
filtered.  -/
CategoryTheory.CostructuredArrow.initial_map₂_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.IsCofiltered C] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  (T : CategoryTheory.Functor C D) [T.Initial] (S : CategoryTheory.Functor D E) [S.Initial] (d : D) (e : E)
  (u : S.obj d ⟶ e), (CategoryTheory.CostructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (T.comp S)) u).Initial
-- Mathlib.Order.Heyting.Basic
himp_bot : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a : α), a ⇨ ⊥ = aᶜ
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.prod_summand_smul : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [inst_2 : DecidableEq ι]
  [inst_3 : (i : ι) → DecidableEq (G i)] {i : ι} (g : G i) (w : Monoid.PushoutI.NormalWord d),
  (g • w).prod = (Monoid.PushoutI.of i) g * w.prod
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.map_ne_one_iff : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] (h : M ≃* N) {x : M}, h x ≠ 1 ↔ x ≠ 1
-- Mathlib.Algebra.Group.Shrink
Shrink.instAddGroup : {α : Type u_2} → [inst : Small.{v, u_2} α] → [AddGroup α] → AddGroup (Shrink.{v, u_2} α)
-- Mathlib.Data.Multiset.Filter
Multiset.filter_le_filter : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] {s t : Multiset α},
  s ≤ t → Multiset.filter p s ≤ Multiset.filter p t
-- Aesop.Forward.State
/-- Returns the set of matches and hypotheses associated with a slot `slot`
with instantiation `inst`, or `(∅, ∅)` if `slot` and `inst` do not have any
associated matches.  -/
Aesop.InstMap.findD : Aesop.InstMap → Aesop.SlotIndex → Lean.Expr → Lean.MetaM (Lean.PHashSet Aesop.Match × Lean.PHashSet Aesop.Hyp)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.NatStruct.toQFn : Lean.Meta.Grind.Arith.Linear.NatStruct → Lean.Expr
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.coe_toNonUnitalSubsemiring : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R), ↑s.toNonUnitalSubsemiring = ↑s
-- Init.Data.List.TakeDrop
List.take_cons : ∀ {α : Type u_1} {i : ℕ} {a : α} {l : List α}, 0 < i → List.take i (a :: l) = a :: List.take (i - 1) l
-- Init.Data.UInt.Lemmas
UInt64.toUInt16_sub : ∀ (a b : UInt64), (a - b).toUInt16 = a.toUInt16 - b.toUInt16
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_of_isEmpty : ∀ {α : Type u_1} {β : Type u_2} [IsEmpty α] {f : α → β} {la : Filter α} {lb : Filter β}, Filter.Tendsto f la lb
-- Init.Data.Range.Lemmas
Std.Legacy.Range.forIn'_eq_forIn'_range' : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] (r : Std.Legacy.Range) (init : β)
  (f : (a : ℕ) → a ∈ r → β → m (ForInStep β)),
  forIn' r init f = forIn' (List.range' r.start r.size r.step) init fun a h => f a ⋯
-- Mathlib.Data.Set.Prod
Set.prod_univ : ∀ {α : Type u_1} {β : Type u_2} {s : Set α}, s ×ˢ Set.univ = Prod.fst ⁻¹' s
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_finsetSum_cbm : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] {f : X → E} {μ : MeasureTheory.VectorMeasure X F}
  {B : ι → E →L[ℝ] F →L[ℝ] G} {s : Finset ι},
  μ.Integrable f → ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B i; μ] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ]
-- Mathlib.Order.Interval.Set.Final
Set.Ici.subtype_functor_final : ∀ {J : Type u} [inst : LinearOrder J] (j : J), ⋯.functor.Final
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- Uniqueness of lift.  -/
Hausdorffification.lift_eq : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] [h : IsHausdorff I N] (f : M →ₗ[R] N)
  (g : Hausdorffification I M →ₗ[R] N), g ∘ₗ Hausdorffification.of I M = f → g = Hausdorffification.lift I f
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.toCompletion_one : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K),
  NumberField.InfinitePlace.Completion.toCompletion 1 = 1
-- Mathlib.LinearAlgebra.Matrix.Echelon.Pivot
Matrix.IsPivotedBy.strictMonoOn : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Zero R] {A : Matrix m n R} {l : m → WithTop n}
  [inst_1 : LinearOrder n] [inst_2 : Preorder m], A.IsPivotedBy l → StrictMonoOn l {i | l i ≠ ⊤}
-- Init.Data.List.Lemmas
List.replicate_append_replicate : ∀ {n : ℕ} {α : Type u_1} {a : α} {m : ℕ}, List.replicate n a ++ List.replicate m a = List.replicate (n + m) a
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- Collects the binderIdents into a `⟨...⟩` expression.  -/
BigOperators.bigOpBindersPattern : Array (Lean.Term × Lean.Term) → Lean.MacroM Lean.Term
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.inv_left_hom_right : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g)
  [inst_1 : CategoryTheory.IsIso sq],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Arrow.Hom.left sq))
      (CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.Arrow.Hom.right sq)) =
    g.hom
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_filter_key : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → Bool} {k fallback : α},
  (Std.ExtDTreeMap.filter (fun k x => f k) t).getKeyD k fallback = (Option.filter f (t.getKey? k)).getD fallback
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.Faithful.mapAddGrp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] [F.Faithful], F.mapAddGrp.Faithful
-- Mathlib.Topology.Order.Hom.Basic
/-- Turn an element of a type `F` satisfying `ContinuousOrderHomClass F α β` into an actual
`ContinuousOrderHom`. This is declared as the default coercion from `F` to `α →Co β`.  -/
ContinuousOrderHomClass.toContinuousOrderHom : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : Preorder α] →
        [inst_1 : Preorder β] →
          [inst_2 : TopologicalSpace α] →
            [inst_3 : TopologicalSpace β] → [inst_4 : FunLike F α β] → [ContinuousOrderHomClass F α β] → F → α →Co β
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.length_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.keys.length = t.size
-- Mathlib.RingTheory.DedekindDomain.Basic
Ring.DimensionLEOne.mk : ∀ {R : Type u_1} [inst : CommRing R], (∀ {p : Ideal R}, p ≠ ⊥ → p.IsPrime → p.IsMaximal) → Ring.DimensionLEOne R
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Iic_sub_one_eq_Iio_of_not_isMin : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrderBot α] [inst_3 : Sub α]
  [PredSubOrder α] {b : α}, ¬IsMin b → Finset.Iic (b - 1) = Finset.Iio b
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_stoppedProcess_of_le_left : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} {τ σ : Ω → WithTop ι}
  [inst_1 : LinearOrder ι],
  τ ≤ σ → MeasureTheory.stoppedProcess (MeasureTheory.stoppedProcess u τ) σ = MeasureTheory.stoppedProcess u τ
-- Mathlib.Data.Prod.Basic
Function.RightInverse.prodMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α} {g₂ : δ → γ},
  Function.RightInverse f₁ f₂ → Function.RightInverse g₁ g₂ → Function.RightInverse (Prod.map f₁ g₁) (Prod.map f₂ g₂)
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Composition by continuous linear equivs on the right respects higher differentiability at a
point in a domain.  -/
ContinuousLinearEquiv.contDiffWithinAt_comp_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {f : E → F} {x : E} {n : WithTop ℕ∞}
  (e : G ≃L[𝕜] E), ContDiffWithinAt 𝕜 n (f ∘ ⇑e) (⇑e ⁻¹' s) (e.symm x) ↔ ContDiffWithinAt 𝕜 n f s x
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
/-- Types are counted less towards the total matching score.
The reason is that types are usually implicit arguments. For example

- If the goal is `(1 : ℕ) = 1`, we could find
  - `rfl (a : α) : a = a`.
    This gets extra points for matching `1`
  - `Nat.succ.inj (n m : ℕ) (h : n.succ = m.succ) : n = m`.
    This gets extra points for matching `ℕ`

  Clearly, `rfl` is better.

- If we rewrite `|(0 : ℝ)|`, we could find
  - `abs_zero : |(0 : α)| = 0`
    This gets extra points for matching `0`
  - `Real.norm_eq_abs : ∀ (r : ℝ), ‖r‖ = |r|`
    This gets extra points for matching `ℝ`

  Clearly, `abs_zero` is better

In both examples, matching the type (`ℕ` or `ℝ`) was not very important for how good
the match actually was.
 -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.Key.score : Lean.Meta.RefinedDiscrTree.Key → Lean.MetaM ℕ
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsInducedSubgraph.instIsPartialOrder : ∀ {α : Type u_1} {β : Type u_2}, IsPartialOrder (Graph α β) fun x1 x2 => x1.IsInducedSubgraph x2
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.toList_succ_eq_map : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [Std.PRange.LinearlyUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.PRange.InfinitelyUpwardEnumerable α]
  [inst_7 : Std.Rxo.IsAlwaysFinite α] [inst_8 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_9 : Std.PRange.LawfulUpwardEnumerableLeast? α] {hi : α},
  (*...Std.PRange.succ hi).toList = Std.PRange.UpwardEnumerable.least :: List.map Std.PRange.succ (*...hi).toList
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.toFun_eq_coe : ∀ {E : Type u_3} [inst : Group E] {p : GroupSeminorm E}, p.toFun = ⇑p
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.germToPullbackStalk_stalkPullbackHom : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U),
  CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.germToPullbackStalk C f F U x hx)
      (TopCat.Presheaf.stalkPullbackHom C f F x) =
    ((TopCat.Presheaf.pullback C f).obj F).germ U x hx
-- Mathlib.CategoryTheory.Monoidal.Hopf_
CategoryTheory.Hopf.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {X : C} {hopf : CategoryTheory.HopfObj X} {X_1 : C}
  {hopf_1 : CategoryTheory.HopfObj X_1},
  { X := X, hopf := hopf } = { X := X_1, hopf := hopf_1 } → X = X_1 ∧ hopf ≍ hopf_1
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.homEquiv_symm_apply_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I J : C} {f : I ⟶ J}
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ExponentiableMorphism f]
  {X : CategoryTheory.Over I} {A : CategoryTheory.Over J}
  (v : A ⟶ (CategoryTheory.ExponentiableMorphism.pushforward f).obj X),
  ((CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj f).homEquiv A X).symm v =
    CategoryTheory.ExponentiableMorphism.pushforwardUncurry v
-- Mathlib.RingTheory.Invariant.Galois
Ideal.IsFractionRing.normal : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (G : Type u_3)
  [Finite G] [inst_4 : Group G] [inst_5 : MulSemiringAction G B] [Algebra.IsInvariant A B G] (P : Ideal A) (Q : Ideal B)
  [inst_7 : Q.LiesOver P] [P.IsPrime] [Q.IsPrime] (K : Type u_4) (L : Type u_5) [inst_10 : Field K] [inst_11 : Field L]
  [inst_12 : Algebra K L] [inst_13 : Algebra (A ⧸ P) K] [IsFractionRing (A ⧸ P) K] [inst_15 : Algebra (B ⧸ Q) L]
  [IsFractionRing (B ⧸ Q) L] [inst_17 : Algebra (A ⧸ P) L] [IsScalarTower (A ⧸ P) (B ⧸ Q) L]
  [IsScalarTower (A ⧸ P) K L], Normal K L
-- Lean.Meta.Offset
_private.Lean.Meta.Offset.0.Lean.Meta.evalNat.visit : Lean.Expr → OptionT Lean.MetaM ℕ
-- Mathlib.Algebra.Homology.Single
HomologicalComplex.single_map_f_self : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  {A B : V} (f : A ⟶ B),
  ((HomologicalComplex.single V c j).map f).f j =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c j A).hom
      (CategoryTheory.CategoryStruct.comp f (HomologicalComplex.singleObjXSelf c j B).inv)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.differentiable_hurwitzZetaEven_sub_hurwitzZetaEven : ∀ (a b : UnitAddCircle), Differentiable ℂ fun s => HurwitzZeta.hurwitzZetaEven a s - HurwitzZeta.hurwitzZetaEven b s
-- Init.Data.BitVec.Basic
BitVec.cast_cast : ∀ {n m k : ℕ} (h₁ : n = m) (h₂ : m = k) (x : BitVec n), BitVec.cast h₂ (BitVec.cast h₁ x) = BitVec.cast ⋯ x
-- Lean.Parser.Term.Basic
/-- `sepByIndentSemicolon(p)` parses a sequence of `p` optionally followed by `;`,
similar to `manyIndent(p ";"?)`, except that if two occurrences of `p` occur on the same line,
the `;` is mandatory. This is used by tactic parsing, so that
```
example := by
  skip
  skip
```
is legal, but `by skip skip` is not - it must be written as `by skip; skip`.  -/
Lean.Parser.Tactic.sepByIndentSemicolon : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Order.Hom.Lattice
SupHom.instInhabited : (α : Type u_2) → [inst : Max α] → Inhabited (SupHom α α)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.isBasis_iff_indep_closure : ∀ {α : Type u_2} {M : Matroid α} {X I : Set α}, M.IsBasis I X ↔ M.Indep I ∧ X ⊆ M.closure I ∧ I ⊆ X
-- Mathlib.Algebra.DirectSum.Module
DirectSum.lmap_apply : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {N : ι → Type u_1} [inst_3 : (i : ι) → AddCommMonoid (N i)]
  [inst_4 : (i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i) (x : DirectSum ι fun i => M i) (i : ι),
  ((DirectSum.lmap f) x) i = (f i) (x i)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
/-- Canonical embedding of the upper half-plane into `ℂ`.  -/
UpperHalfPlane.coe : UpperHalfPlane → ℂ
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.hom_ext : ∀ {X Y : SSet} {f g : X ⟶ Y}, (∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n) → f = g
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.sin_sq_arctan : ∀ (x : ℝ), Real.sin (Real.arctan x) ^ 2 = x ^ 2 / (1 + x ^ 2)
-- Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
/-- A nonzero prime ideal of a ring with finite quotients is maximal.  -/
Ring.HasFiniteQuotients.maximalOfPrime : ∀ {R : Type u_1} [inst : CommRing R] [Ring.HasFiniteQuotients R] {P : Ideal R} [P.IsPrime], P ≠ ⊥ → P.IsMaximal
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.ge_lower' : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] (lo : ℤ),
  i.lo? = some lo → ∀ (a : α), lo ≤ ↑a
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
ContinuousLinearMap.isBoundedBilinearMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {G : Type u_4} [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G),
  IsBoundedBilinearMap 𝕜 fun x => (f x.1) x.2
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instOneCoeOfOneMemClass.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → One (R i)] [inst_2 : ∀ (i : ι), OneMemClass (S i) (R i)],
  RestrictedProduct.instOneCoeOfOneMemClass R = { one := ⟨fun x => 1, ⋯⟩ }
-- Mathlib.Condensed.Light.TopCatAdjunction
/-- The functor from topological spaces to light condensed sets restricted to sequential spaces
is fully faithful.

Note: for now, we only have `ℕ∪{∞}` as a light profinite set at universe level 0, which is why we
can only prove this for the functor `Sequential.{0} ⥤ LightCondSet.{0}`.
 -/
LightCondSet.fullyFaithfulSequentialToLightCondSet : LightCondSet.sequentialToLightCondSet.FullyFaithful
-- Init.Data.List.Sublist
List.IsPrefix.eq_of_length : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → l₁.length = l₂.length → l₁ = l₂
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentation.desc_var : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'}
  [inst_3 : AddCommGroup N] [inst_4 : Module A N] (s : relations.Solution N) (g : relations.G),
  (h.desc s) (solution.var g) = s.var g
-- Mathlib.Algebra.Notation
/-- The *negative part* of an element `a`.  -/
NegPart.negPart : {α : Type u_1} → [self : NegPart α] → α → α
-- Mathlib.Data.Multiset.Defs
Multiset.card_lt_card : ∀ {α : Type u_1} {s t : Multiset α}, s < t → s.card < t.card
-- Mathlib.Data.Nat.Factorial.Basic
Nat.pow_sub_lt_descFactorial : ∀ {n k : ℕ}, 2 ≤ k → k ≤ n → (n + 1 - k) ^ k < n.descFactorial k
-- Init.Data.Range.Basic
Std.Legacy.Range.«term[_:_]» : Lean.ParserDescr
-- Mathlib.RingTheory.Algebraic.Basic
Subalgebra.inv_mem_of_root_of_coeff_zero_ne_zero : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (A : Subalgebra K L) {x : ↥A}
  {p : Polynomial K}, (Polynomial.aeval x) p = 0 → p.coeff 0 ≠ 0 → (↑x)⁻¹ ∈ A
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.map_inf_eq : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H K : Subgroup G) (f : G →* N),
  Function.Injective ⇑f → Subgroup.map f (H ⊓ K) = Subgroup.map f H ⊓ Subgroup.map f K
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.isBoundedSMulSeminormedAddCommGroupToProd : ∀ (p : ENNReal) [hp : Fact (1 ≤ p)] (α : Type u_4) (β : Type u_5) [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β] {R : Type u_6} [inst_2 : SeminormedRing R] [inst_3 : Module R α]
  [inst_4 : Module R β] [IsBoundedSMul R α] [IsBoundedSMul R β], IsBoundedSMul R (α × β)
-- Mathlib.CategoryTheory.Limits.Cones
/-- Whiskering on the left by `E : K ⥤ J` gives a functor from `Cocone F` to `Cocone (E ⋙ F)`.
 -/
CategoryTheory.Limits.Cocone.whiskering : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              (E : CategoryTheory.Functor K J) →
                CategoryTheory.Functor (CategoryTheory.Limits.Cocone F) (CategoryTheory.Limits.Cocone (E.comp F))
-- Mathlib.RingTheory.Derivation.ToSquareZero
/-- Given a tower of algebras `R → A → B`, and a square-zero `I : Ideal B`, each `R`-derivation
from `A` to `I` corresponds to a lift `A →ₐ[R] B` of the canonical map `A →ₐ[R] B ⧸ I`.  -/
liftOfDerivationToSquareZero : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : CommRing B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                (I : Ideal B) →
                  [inst_5 : Algebra A B] → [IsScalarTower R A B] → I ^ 2 = ⊥ → Derivation R A ↥I → A →ₐ[R] B