mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.Deriv.Abs
DifferentiableAt.abs_of_neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  DifferentiableAt ℝ f x → f x < 0 → DifferentiableAt ℝ (fun x => |f x|) x
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.folder.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.folder = 1
-- Lean.Elab.Tactic.RCases
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.RCasesPatt.instInhabited : Inhabited Lean.Elab.Tactic.RCases.RCasesPatt
-- Mathlib.RingTheory.Ideal.Operations
Ideal.IsPrime.multiset_prod_le : ∀ {R : Type u} [inst : CommSemiring R] {s : Multiset (Ideal R)} {P : Ideal R}, P.IsPrime → (s.prod ≤ P ↔ ∃ I ∈ s, I ≤ P)
-- Mathlib.Order.SuccPred.Basic
/-- **Alias** of the forward direction of `Order.succ_lt_succ_iff`. -/
Order.lt_of_succ_lt_succ : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α} [NoMaxOrder α],
  Order.succ a < Order.succ b → a < b
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.posSemidef_submatrix_equiv : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  {M : Matrix n n R} (e : m ≃ n), (M.submatrix ⇑e ⇑e).PosSemidef ↔ M.PosSemidef
-- Mathlib.Algebra.Group.End
Equiv.Perm.one_apply : ∀ {α : Type u_4} (x : α), 1 x = x
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
HomologicalComplex.HomologySequence.mapSnakeInput_f₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂)
  (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i j : ι) (hij : c.Rel i j),
  (HomologicalComplex.HomologySequence.mapSnakeInput φ hS₁ hS₂ i j hij).f₂ =
    (HomologicalComplex.cyclesFunctor C c j).mapShortComplex.map φ
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- Flip arguments in `f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'` to get
`ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')`  -/
ContinuousLinearMap.flipMultilinear : {𝕜 : Type u} →
  {ι : Type v} →
    {E : ι → Type wE} →
      {G : Type wG} →
        {G' : Type wG'} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
              [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
                [inst_3 : SeminormedAddCommGroup G] →
                  [inst_4 : NormedSpace 𝕜 G] →
                    [inst_5 : SeminormedAddCommGroup G'] →
                      [inst_6 : NormedSpace 𝕜 G'] →
                        [Fintype ι] →
                          (G →L[𝕜] ContinuousMultilinearMap 𝕜 E G') → ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')
-- Mathlib.Data.Nat.Factors
Nat.primeFactorsList_zero : Nat.primeFactorsList 0 = []
-- Mathlib.Data.Finset.Lattice.Basic
Finset.mem_inter_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s₁ s₂ : Finset α}, a ∈ s₁ → a ∈ s₂ → a ∈ s₁ ∩ s₂
-- Mathlib.Data.Int.Basic
Int.strongRec_of_ge : ∀ {m n : ℤ} {P : ℤ → Sort u_1} {lt : (n : ℤ) → n < m → P n} {ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n}
  (hn : m ≤ n), Int.strongRec lt ge n = ge n hn fun k x => Int.strongRec lt ge k
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.HalfBraiding.monoidal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X : C}
  (self : CategoryTheory.HalfBraiding X) (U U' : C),
  (self.β (CategoryTheory.MonoidalCategoryStruct.tensorObj U U')).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X U U').inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (self.β U).hom U')
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator U X U').hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U (self.β U').hom)
            (CategoryTheory.MonoidalCategoryStruct.associator U U' X).inv)))
-- Mathlib.LinearAlgebra.RootSystem.Chain
_private.Mathlib.LinearAlgebra.RootSystem.Chain.0.RootPairing.chainCoeff_reflectionPerm_right_aux : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  Set.Icc (-↑(RootPairing.chainTopCoeff i j)) ↑(RootPairing.chainBotCoeff i j) =
    Set.Icc (-↑(RootPairing.chainBotCoeff i (-j))) ↑(RootPairing.chainTopCoeff i (-j))
-- Mathlib.Order.Hom.Basic
/-- Identity order embedding  -/
OrderEmbedding.id : (α : Type u_2) → [inst : LE α] → α ↪o α
-- Lean.Meta.Match.Match
/-- The number of patterns in each AltLHS must be equal to the number of discriminants.  -/
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.checkNumPatterns : ℕ → List Lean.Meta.Match.AltLHS → Lean.MetaM Unit
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.instDistribLattice : DistribLattice Cardinal.{u}
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.AB4OfSize.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C],
  (∀ (α : Type w), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete α) C) →
    CategoryTheory.AB4OfSize.{w, v, u} C
-- Mathlib.Order.Hom.Order
OrderHom.instMax : {α : Type u_1} → {β : Type u_2} → [inst : Preorder α] → [inst_1 : SemilatticeSup β] → Max (α →o β)
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
_private.Mathlib.CategoryTheory.Limits.Types.Coproducts.0.CategoryTheory.Limits.WalkingPair.swap.match_1.eq_1 : ∀ (motive : CategoryTheory.Limits.WalkingPair → Sort u_1) (h_1 : Unit → motive CategoryTheory.Limits.WalkingPair.left)
  (h_2 : Unit → motive CategoryTheory.Limits.WalkingPair.right),
  (match CategoryTheory.Limits.WalkingPair.left with
    | CategoryTheory.Limits.WalkingPair.left => h_1 ()
    | CategoryTheory.Limits.WalkingPair.right => h_2 ()) =
    h_1 ()
-- Init.Data.Array.Find
Array.find?_eq_findSome?_guard : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, Array.find? p xs = Array.findSome? (Option.guard p) xs
-- Init.SimpLemmas
dite_cond_eq_false : ∀ {α : Sort u} {c : Prop} {x : Decidable c} {t : c → α} {e : ¬c → α} (h : c = False), dite c t e = e ⋯
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.notMem_closure_iff_of_notMem : ∀ {α : Type u_2} {M : Matroid α} {e : α} {I : Set α},
  M.Indep I →
    e ∉ I →
      autoParam (e ∈ M.E) Matroid.Indep.notMem_closure_iff_of_notMem._auto_1 → (e ∉ M.closure I ↔ M.Indep (insert e I))
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instCommMagmaOfMulHomClass.eq_1 : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → CommMagma (G i)] [inst_5 : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)],
  DirectLimit.instCommMagmaOfMulHomClass = { toMul := DirectLimit.instMul, mul_comm := ⋯ }
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.map_add_left_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Add G] (μ : MeasureTheory.Measure G) [μ.IsAddLeftInvariant]
  (g : G), MeasureTheory.Measure.map (fun x => g + x) μ = μ
-- Batteries.Data.Fin.Coding
Fin.encodeSigma.eq_def : ∀ {n : ℕ} (f : Fin n → ℕ) (x : (i : Fin n) × Fin (f i)),
  Fin.encodeSigma f x =
    match n, f, x with
    | a.succ, f, ⟨⟨0, ⋯⟩, j⟩ => ⟨↑j, ⋯⟩
    | n.succ, f, ⟨⟨i.succ, hi⟩, j⟩ =>
      match Fin.encodeSigma (fun x => f x.succ) ⟨⟨i, ⋯⟩, j⟩ with
      | ⟨k, hk⟩ => ⟨f 0 + k, ⋯⟩
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCat_zero_apply : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) (x : ↑S.X₁),
  (CategoryTheory.ConcreteCategory.hom S.g) ((CategoryTheory.ConcreteCategory.hom S.f) x) = 0
-- Lean.Elab.ConfigEval.MetaInstances
Lean.Elab.ConfigEval.instEvalTermOccurrences.evalTerm : Lean.Term → Lean.Elab.TermElabM (Lean.Meta.Occurrences × Lean.Expr)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.C_injective : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonAssocSemiring R], Function.Injective ⇑HahnSeries.C
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKeyD_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [Inhabited α] {k fallback : α} {f : Option β → Option β},
  (Std.ExtDHashMap.Const.alter m k f).getKeyD k fallback =
    if (f (Std.ExtDHashMap.Const.get? m k)).isSome = true then k else fallback
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.append_append : ∀ {α : Type u} {L₁ L₂ L₃ L₄ : List (α × Bool)},
  FreeGroup.Red L₁ L₃ → FreeGroup.Red L₂ L₄ → FreeGroup.Red (L₁ ++ L₂) (L₃ ++ L₄)
-- Init.MetaTypes
/-- Enable eta only for structures that are not classes.  -/
Lean.Meta.EtaStructMode.notClasses : Lean.Meta.EtaStructMode
-- Std.Http.Data.Method
Std.Http.Method.unlink.sizeOf_spec : sizeOf Std.Http.Method.unlink = 1
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.Spec : (Type u → Type u) → Type (u + 1)
-- Mathlib.Analysis.LocallyConvex.Separation
RCLike.geometric_hahn_banach_closed_compact : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E]
  {s t : Set E} [inst_3 : RCLike 𝕜] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E]
  [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E],
  Convex ℝ s →
    IsClosed s →
      Convex ℝ t →
        IsCompact t → Disjoint s t → ∃ f u v, (∀ a ∈ s, RCLike.re (f a) < u) ∧ u < v ∧ ∀ b ∈ t, v < RCLike.re (f b)
-- Mathlib.Analysis.Normed.Module.DoubleDual
NormedSpace.toLinearMap_inclusionInDoubleDualWeak : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (X : Type u_2) [inst_1 : SeminormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X],
  ↑(NormedSpace.inclusionInDoubleDualWeak 𝕜 X) =
    ((toWeakSpace 𝕜 X).arrowCongr StrongDual.toWeakDual) ↑(NormedSpace.inclusionInDoubleDual 𝕜 X)
-- Mathlib.Data.Bool.Count
List.IsChain.count_true_le_count_false_add_one : ∀ {l : List Bool}, List.IsChain (fun x1 x2 => x1 ≠ x2) l → List.count true l ≤ List.count false l + 1
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.toOrderAddMonoidHom_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β] (f : α →+*o β), f.toOrderAddMonoidHom = ↑f
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.lanPresheafExt.eq_1 : ∀ {F G : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)}
  (i : FintypeCat.toLightProfinite.op.comp F ≅ FintypeCat.toLightProfinite.op.comp G),
  LightCondensed.lanPresheafExt i =
    (FintypeCat.toLightProfinite.op.pointwiseLeftKanExtension
          (FintypeCat.toLightProfinite.op.comp F)).leftKanExtensionUniqueOfIso
      (FintypeCat.toLightProfinite.op.pointwiseLeftKanExtensionUnit (FintypeCat.toLightProfinite.op.comp F)) i
      (LightCondensed.lanPresheaf G)
      (FintypeCat.toLightProfinite.op.pointwiseLeftKanExtensionUnit (FintypeCat.toLightProfinite.op.comp G))
-- Mathlib.CategoryTheory.Pi.Basic
/-- Assemble an `I`-indexed family of natural isomorphisms into a single natural isomorphism.
 -/
CategoryTheory.NatIso.pi' : {I : Type w₀} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {E : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} E] →
          {F G : CategoryTheory.Functor E ((i : I) → C i)} →
            ((i : I) → F.comp (CategoryTheory.Pi.eval C i) ≅ G.comp (CategoryTheory.Pi.eval C i)) → (F ≅ G)
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_pow' : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R},
  p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.rescale_zero : ∀ {σ : Type u_1} {R : Type u_9} [inst : CommSemiring R],
  MvPowerSeries.rescale 0 = MvPowerSeries.C.comp MvPowerSeries.constantCoeff
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_mul_ofNat : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {a k : ℕ} [inst_1 : a.AtLeastTwo],
  (p * OfNat.ofNat a).coeff k = p.coeff k * OfNat.ofNat a
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.currying_unitIso_hom_app_app_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (X : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X_1 : C) (X_2 : D),
  ((CategoryTheory.Functor.currying.unitIso.hom.app X).app X_1).app X_2 =
    CategoryTheory.CategoryStruct.id ((X.obj X_1).obj X_2)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.Const.alterKey_cons_perm.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (v : β) → motive (some v)),
  (match none with
    | none => h_1 ()
    | some v => h_2 v) =
    h_1 ()
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.withTopWithBot'.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder β] (f : LatticeHom α β),
  f.withTopWithBot' = { toLatticeHom := f.withBot'.withTop', map_top' := ⋯, map_bot' := ⋯ }
-- Mathlib.Analysis.Meromorphic.NormalForm
toMeromorphicNFAt.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 → E) (x : 𝕜),
  toMeromorphicNFAt f x =
    if hf : MeromorphicAt f x then
      Function.update f x (if h₁f : meromorphicOrderAt f x = ↑0 then Classical.choose ⋯ x else 0)
    else 0
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.HasFiniteWidePushouts.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (∀ (J : Type) [Finite J], CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Limits.WidePushoutShape J) C) →
    CategoryTheory.Limits.HasFiniteWidePushouts C
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.intervalEdge.congr_simp : ∀ {n : ℕ} (j j_1 : ℕ) (e_j : j = j_1) (l l_1 : ℕ) (e_l : l = l_1) (hjl : j + l ≤ n),
  SimplexCategory.intervalEdge j l hjl = SimplexCategory.intervalEdge j_1 l_1 ⋯
-- Std.Http.Protocol.H1
/-- Stores the machine-level error field used by external callers for diagnostics.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.setError : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Error → Std.Http.Protocol.H1.Machine dir
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_eq_some_get : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α} (h' : a ∈ t), t.get? a = some (t.get a h')
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
SSet.innerAnodyneExtensions.of_isIso : ∀ {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.IsIso f], SSet.innerAnodyneExtensions f
-- Lean.Server.InfoUtils
Lean.Elab.Info.pos? : Lean.Elab.Info → Option String.Pos.Raw
-- Init.Data.List.Monadic
List.zipWithM.match_1.congr_eq_2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (motive : List α → List β → Array γ → Sort u_4) (x : List α)
  (x_1 : List β) (x_2 : Array γ)
  (h_1 : (a : α) → (as : List α) → (b : β) → (bs : List β) → (acc : Array γ) → motive (a :: as) (b :: bs) acc)
  (h_2 : (x : List α) → (x_3 : List β) → (acc : Array γ) → motive x x_3 acc) (x_3 : List α) (x_4 : List β)
  (acc : Array γ),
  x = x_3 →
    x_1 = x_4 →
      x_2 = acc →
        (∀ (a : α) (as : List α) (b : β) (bs : List β), x_3 = a :: as → x_4 = b :: bs → False) →
          (match x, x_1, x_2 with
            | a :: as, b :: bs, acc => h_1 a as b bs acc
            | x, x_6, acc => h_2 x x_6 acc) ≍
            h_2 x_3 x_4 acc
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.map_sup : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H K : Subgroup G) (f : G →* N),
  Subgroup.map f (H ⊔ K) = Subgroup.map f H ⊔ Subgroup.map f K
-- Lean.Meta.Tactic.LibrarySearch
/-- Interleave x y interleaves the elements of x and y until one is empty and then returns
final elements in other list.
 -/
Lean.Meta.LibrarySearch.interleaveWith : {α : Type u_1} → {β : Type u_2} → {γ : Type} → (α → γ) → Array α → (β → γ) → Array β → Array γ
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.fst.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ],
  CochainComplex.mappingCocone.fst φ =
    -((CochainComplex.mappingCone.fst φ).leftShift (-1) 0 CochainComplex.mappingCocone.fst._proof_1).homOf
-- Init.Data.Vector.Basic
/-- Swaps an element of a vector with a given value using a `Fin` index. The original value is returned
along with the updated vector.

This will perform the update destructively provided that the vector has a reference count of 1.
 -/
Vector.swapAt : {α : Type u_1} → {n : ℕ} → Vector α n → (i : ℕ) → α → autoParam (i < n) Vector.swapAt._auto_1 → α × Vector α n
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.PrepathObject.RightHomotopy.precomp_h : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Y : C} {P : HomotopicalAlgebra.PrepathObject Y} {X : C}
  {f g : X ⟶ Y} (h : P.RightHomotopy f g) {Z : C} (i : Z ⟶ X),
  (h.precomp i).h = CategoryTheory.CategoryStruct.comp i h.h
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapAddEquiv_trans : ∀ {R : Type u_3} {S : Type u_4} {T : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Semiring T] [inst_3 : Add M] (e₁ : R ≃+ S) (e₂ : S ≃+ T),
  AddMonoidAlgebra.mapAddEquiv M (e₁.trans e₂) =
    (AddMonoidAlgebra.mapAddEquiv M e₁).trans (AddMonoidAlgebra.mapAddEquiv M e₂)
-- Init.Data.List.Sublist
List.isInfixOf_internal.eq_1 : ∀ {α : Type u} [inst : BEq α] (l₁ : List α), l₁.isInfixOf_internal [] = (l₁.isPrefixOf [] || false)
-- Mathlib.Topology.PartitionOfUnity
/-- A `BumpCovering` that consists of a single function, uniformly equal to one, defined as an
example for `Inhabited` instance.  -/
BumpCovering.single : {ι : Type u} → {X : Type v} → [inst : TopologicalSpace X] → ι → (s : Set X) → BumpCovering ι X s
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- If a fundamental domain has volume 0, then `QuotientMeasureEqMeasurePreimage` holds.  -/
MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_of_zero : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  {ν : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α ν] [Countable G] [MeasurableConstSMul G α]
  {s : Set α}, MeasureTheory.IsFundamentalDomain G s ν → ν s = 0 → MeasureTheory.QuotientMeasureEqMeasurePreimage ν 0
-- Mathlib.Order.ConditionallyCompleteLattice.Group
le_ciInf_add_ciInf : ∀ {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [Nonempty ι] [Nonempty ι'] [inst : ConditionallyCompleteLattice α]
  [inst_1 : AddGroup α] [AddLeftMono α] [AddRightMono α] {a : α} {g : ι → α} {h : ι' → α},
  (∀ (i : ι) (j : ι'), a ≤ g i + h j) → a ≤ iInf g + iInf h
-- Lean.Elab.Parallel
/-- Runs a list of CoreM computations in parallel and returns:
* a combined cancellation hook for all tasks, and
* an iterator that yields results in completion order (greedily).

The iterator runs in CoreM, and as it yields each result, it updates the CoreM state
to reflect the state when that particular task completed. This means the state is
threaded through the iteration in task completion order.

Results are wrapped in `Except Exception α` so that errors in individual tasks don't stop
the iteration - you can observe all results including which tasks failed.

The iterator will terminate after all jobs complete (assuming they all do complete).
 -/
Lean.Core.CoreM.parIterGreedyWithCancel : {α : Type} → List (Lean.CoreM α) → Lean.CoreM (BaseIO PUnit.{1} × Std.IterM Lean.CoreM (Except Lean.Exception α))
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
jacobiTheta_eq_tsum_nat : ∀ {τ : ℂ}, 0 < τ.im → jacobiTheta τ = 1 + 2 * ∑' (n : ℕ), Complex.exp (↑Real.pi * Complex.I * (↑n + 1) ^ 2 * τ)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_erase : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (x : AddMonoidAlgebra R M),
  (AddMonoidAlgebra.erase m x).coeff = Finsupp.erase m x.coeff
-- Mathlib.MeasureTheory.Function.AEEqFun.DomAct
DomMulAct.mk_smul_mk_aeeqFun : ∀ {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : SMul M α] [inst_3 : MeasurableConstSMul M α]
  [inst_4 : MeasureTheory.SMulInvariantMeasure M α μ] (c : M) (f : α → β) (hf : MeasureTheory.AEStronglyMeasurable f μ),
  DomMulAct.mk c • MeasureTheory.AEEqFun.mk f hf = MeasureTheory.AEEqFun.mk (fun x => f (c • x)) ⋯
-- Mathlib.Data.Set.Basic
/-- See also `Subtype.prop`  -/
Subtype.mem : ∀ {α : Type u_1} {s : Set α} (p : ↑s), ↑p ∈ s
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_inv_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (X : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ),
  (CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso C).inv.app X =
    ((Opposite.unop X).homMk
        (CategoryTheory.Pretriangulated.Triangle.mk (Opposite.unop X).mor₁ (Opposite.unop X).mor₂
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).unitIso.inv.app
                (Opposite.op (Opposite.unop X).obj₃)).unop
            ((CategoryTheory.shiftFunctor C 1).map
              (CategoryTheory.CategoryStruct.comp
                ((CategoryTheory.shiftFunctor Cᵒᵖ 1).map (Opposite.unop X).mor₃.op).unop
                ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).counitIso.inv.app
                    (Opposite.op (Opposite.unop X).obj₁)).unop))))
        (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₁)
        (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₂)
        (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₃) ⋯ ⋯ ⋯).op
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.iterOfTree.eq_1 : ∀ {α : Type u} {β : α → Type v} (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Zipper.iterOfTree t =
    (Std.DTreeMap.Internal.Zipper.prependMap t Std.DTreeMap.Internal.Zipper.done).iter
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
CategoryTheory.Mono.inr_of_binaryCoproductDisjoint : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.BinaryCoproductDisjoint X Y]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y], CategoryTheory.Mono CategoryTheory.Limits.coprod.inr
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.boundary.hom_ext : ∀ {n : ℕ} {X : SSet} {f g : (SSet.boundary (n + 1)).toSSet ⟶ X},
  (∀ (i : Fin (n + 2)),
      CategoryTheory.CategoryStruct.comp (SSet.boundary.ι i) f =
        CategoryTheory.CategoryStruct.comp (SSet.boundary.ι i) g) →
    f = g