mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.hom_id : ∀ {M : MonCat}, MonCat.Hom.hom (CategoryTheory.CategoryStruct.id M) = MonoidHom.id ↑M
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.instAddCommMonoid : {ι : Type u_1} →
  {R : Type u_4} →
    [inst : CommSemiring R] →
      (s : ι → Type u_7) →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] →
          [inst_2 : (i : ι) → Module R (s i)] → AddCommMonoid (PiTensorProduct R fun i => s i)
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.insertMin.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → Sort u_3)
  (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (h_1 : (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) → motive Std.DTreeMap.Internal.Impl.leaf hr)
  (h_2 :
    (sz : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l' r' : Std.DTreeMap.Internal.Impl α β) →
            (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced) →
              motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr),
  (match Std.DTreeMap.Internal.Impl.leaf, hr with
    | Std.DTreeMap.Internal.Impl.leaf, hr => h_1 hr
    | Std.DTreeMap.Internal.Impl.inner sz k' v' l' r', hr => h_2 sz k' v' l' r' hr) =
    h_1 hr
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.meas_countablePartitionSet_le_of_fst_le : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ (n : ℕ) (a : α) (x : γ) (s : Set β),
      (κ a) (MeasurableSpace.countablePartitionSet n x ×ˢ s) ≤ (ν a) (MeasurableSpace.countablePartitionSet n x)
-- Init.Data.Vector.Basic
/-- Count the number of elements of a vector that are equal to `a`.  -/
Vector.count : {α : Type u_1} → {n : ℕ} → [BEq α] → α → Vector α n → ℕ
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
/-- Reinterpret an ordered monoid with zero homomorphism as an order monoid homomorphism.  -/
OrderMonoidWithZeroHom.toOrderMonoidHom : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → [inst_2 : MulZeroOneClass α] → [inst_3 : MulZeroOneClass β] → (α →*₀o β) → α →*o β
-- Mathlib.Order.WithBot
WithBot.coe_mono : ∀ {α : Type u_1} [inst : Preorder α], Monotone fun a => ↑a
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.symm_comp_self : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N), ⇑e.symm ∘ ⇑e = id
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.neg_left : ∀ {R : Type u} [inst : CommRing R] {x y : R}, IsCoprime x y → IsCoprime (-x) y
-- Mathlib.NumberTheory.LSeries.PrimesInAP
/-- As `x` approaches `1` from the right along the real axis, the L-series of
`ArithmeticFunction.vonMangoldt.residueClass` is bounded below by `(q.totient)⁻¹/(x-1) - C`.  -/
ArithmeticFunction.vonMangoldt.LSeries_residueClass_lower_bound : ∀ {q : ℕ} [NeZero q] {a : ZMod q},
  IsUnit a →
    ∃ C,
      ∀ {x : ℝ},
        x ∈ Set.Ioc 1 2 →
          (↑q.totient)⁻¹ / (x - 1) - C ≤ ∑' (n : ℕ), ArithmeticFunction.vonMangoldt.residueClass a n / ↑n ^ x
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.neighborSet_induce : ∀ {V : Type u_1} (G : SimpleGraph V) (s : Set V) (v : ↑s),
  (SimpleGraph.induce s G).neighborSet v = Subtype.val ⁻¹' G.neighborSet ↑v
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.MatcherInfo.arity : Lean.Meta.MatcherInfo → ℕ
-- Mathlib.Data.DFinsupp.Ext
/-- If two additive homomorphisms from `Π₀ i, β i` are equal on each `single a b`, then
they are equal.

See note [partially-applied ext lemmas].  -/
DFinsupp.addHom_ext' : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)] {γ : Type w}
  [inst_2 : AddZeroClass γ] ⦃f g : (Π₀ (i : ι), β i) →+ γ⦄,
  (∀ (x : ι), f.comp (DFinsupp.singleAddHom β x) = g.comp (DFinsupp.singleAddHom β x)) → f = g
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionSemiHomClass.mk : ∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} {φ : outParam (M → N)}
  {A : outParam (Type u_13)} {B : outParam (Type u_14)} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : AddMonoid A]
  [inst_3 : AddMonoid B] [inst_4 : DistribMulAction M A] [inst_5 : DistribMulAction N B] [inst_6 : FunLike F A B]
  [toMulActionSemiHomClass : MulActionSemiHomClass F φ A B] [toAddMonoidHomClass : AddMonoidHomClass F A B],
  DistribMulActionSemiHomClass F φ A B
-- Mathlib.Algebra.Ring.GeomSum
Odd.add_dvd_pow_add_pow : ∀ {R : Type u_1} [inst : CommRing R] (x y : R) {n : ℕ}, Odd n → x + y ∣ x ^ n + y ^ n
-- Mathlib.Data.Sym.Sym2
Sym2.fromRel_top : ∀ {α : Type u_1}, Sym2.fromRel ⋯ = Set.univ
-- Mathlib.Tactic.Simproc.ExistsAndEq
/-- Finds a `Path` for `findEq`. It leads to a subexpression `a = a'` or `a' = a`, where
`a'` doesn't contain the free variable `a`.
This is a fast version that quickly returns `none` when the simproc
is not applicable.  -/
ExistsAndEq.findEqPath : {u : Lean.Level} → {α : Q(Sort u)} → Q(«$α») → Q(Prop) → Lean.MetaM (Option ExistsAndEq.Path)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {he : t.isEmpty = false} {km : α}, t.minKey he = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Lean.Parser.Do
Lean.Parser.Term.termReturn.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.isUnit_addZ_of_X_ne : ∀ {F : Type u} [inst : Field F] {P Q : Fin 3 → F},
  P 0 * Q 2 ^ 2 ≠ Q 0 * P 2 ^ 2 → IsUnit (WeierstrassCurve.Jacobian.addZ P Q)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFun_asIdeal : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] (f : A)
  (x : ↑↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toPresheafedSpace),
  (AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFun f x).asIdeal =
    AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier x
-- Mathlib.Geometry.Manifold.Algebra.SMul
Diffeomorph.smul_toHomeomorph : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : Group G]
  [inst_12 : MulAction G M] {n : WithTop ℕ∞} [inst_13 : ContMDiffSMul I I' n G M] (g : G),
  (Diffeomorph.smul I I' n g).toHomeomorph = Homeomorph.smul g
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_map_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (adj : F ⊣ G)
  {X Y : CategoryTheory.Endofunctor.Algebra F} (f : X ⟶ Y),
  ((CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf adj).map f).f = f.f
-- Mathlib.Order.Interval.Set.Image
directedOn_ge_Ico : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), DirectedOn (fun x1 x2 => x1 ≥ x2) (Set.Ico a b)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.mk : {M : Type u_3} →
  [inst : Add M] → (carrier : Set M) → (∀ {a b : M}, a ∈ carrier → b ∈ carrier → a + b ∈ carrier) → AddSubsemigroup M
-- Std.Data.HashSet.Raw
/-- Internal implementation detail of the hash map  -/
Std.HashSet.Raw.Equiv.inner : ∀ {α : Type u} {m₁ m₂ : Std.HashSet.Raw α}, m₁.Equiv m₂ → m₁.inner.Equiv m₂.inner
-- Init.Data.Array.InsertIdx
Array.insertIdx_eraseIdx_of_ge : ∀ {α : Type u} {a : α} {i j : ℕ} {as : Array α} (w₁ : i < as.size) (w₂ : j ≤ (as.eraseIdx i w₁).size),
  i ≤ j → (as.eraseIdx i w₁).insertIdx j a w₂ = (as.insertIdx (j + 1) a ⋯).eraseIdx i ⋯
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instSubtractionMonoid : {α : Type u_1} → [SubtractionMonoid α] → SubtractionMonoid (Colex α)
-- Mathlib.Order.Booleanisation
Booleanisation.lift_inf_comp : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] (a b : α),
  Booleanisation.lift a ⊓ Booleanisation.comp b = Booleanisation.lift (a \ b)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.pi_source : ∀ {ι : Type u_5} {αi : ι → Type u_6} {βi : ι → Type u_7} (ei : (i : ι) → PartialEquiv (αi i) (βi i)),
  (PartialEquiv.pi ei).source = Set.univ.pi fun i => (ei i).source
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.extension_map : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {γ : Type u_3}
  [inst_2 : UniformSpace γ] [CompleteSpace γ] [T0Space γ] {f : β → γ} {g : α → β},
  UniformContinuous f →
    UniformContinuous g →
      UniformSpace.Completion.extension f ∘ UniformSpace.Completion.map g = UniformSpace.Completion.extension (f ∘ g)
-- Mathlib.Order.LiminfLimsup
Filter.limsup_nat_add : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] (f : ℕ → α) (k : ℕ),
  Filter.limsup (fun i => f (i + k)) Filter.atTop = Filter.limsup f Filter.atTop
-- Mathlib.Analysis.Normed.Module.RCLike.Basic
ContinuousLinearEquiv.coord.congr_simp : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  (x : E) (h : x ≠ 0), ContinuousLinearEquiv.coord 𝕜 x h = ContinuousLinearEquiv.coord 𝕜 x h
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.colimitIsoFlipCompColim_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X : K),
  (CategoryTheory.Limits.colimitIsoFlipCompColim F).inv.app X =
    (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F X).inv
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFPresheafedSpaceToPresheafedSpaceGlueDataToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData : ∀ (D : AlgebraicGeometry.Scheme.GlueData) (i j : D.J),
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion
    (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.f i j)
-- Mathlib.CategoryTheory.MorphismProperty.LocalEpi
CategoryTheory.ObjectProperty.instIsStableUnderCobaseChangeLocalEpi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C},
  P.localEpi.IsStableUnderCobaseChange
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.uniqueUnits.eq_1 : ∀ {α : Type u_1}, FreeMonoid.uniqueUnits = { toInhabited := Units.instInhabited, uniq := ⋯ }
-- Init.Data.Iterators.PostconditionMonad
/-- Given a function `f : α → β`, returns a function `PostconditionT m α → PostconditionT m β`,
turning `PostconditionT m` into a functor.

The postcondition of the `x.map f` states that the return value is the image under `f` of some
`a : α` satisfying the `x.Property`.
 -/
Std.Iterators.PostconditionT.map : {m : Type w → Type w'} →
  [Functor m] → {α β : Type w} → (α → β) → Std.Iterators.PostconditionT m α → Std.Iterators.PostconditionT m β
-- Mathlib.Data.Complex.Basic
Complex.coe_imAddGroupHom : ⇑Complex.imAddGroupHom = Complex.im
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.ShiftMkCore.mk.inj : ∀ {C : Type u} {A : Type u_1} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : AddMonoid A}
  {F : A → CategoryTheory.Functor C C} {zero : F 0 ≅ CategoryTheory.Functor.id C}
  {add : (n m : A) → F (n + m) ≅ (F n).comp (F m)}
  {assoc_hom_app :
    autoParam
      (∀ (m₁ m₂ m₃ : A) (X : C),
        CategoryTheory.CategoryStruct.comp ((add (m₁ + m₂) m₃).hom.app X) ((F m₃).map ((add m₁ m₂).hom.app X)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp ((add m₁ (m₂ + m₃)).hom.app X) ((add m₂ m₃).hom.app ((F m₁).obj X))))
      CategoryTheory.ShiftMkCore.assoc_hom_app._autoParam}
  {zero_add_hom_app :
    autoParam
      (∀ (n : A) (X : C),
        (add 0 n).hom.app X =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((F n).map (zero.inv.app X)))
      CategoryTheory.ShiftMkCore.zero_add_hom_app._autoParam}
  {add_zero_hom_app :
    autoParam
      (∀ (n : A) (X : C),
        (add n 0).hom.app X =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (zero.inv.app ((F n).obj X)))
      CategoryTheory.ShiftMkCore.add_zero_hom_app._autoParam}
  {F_1 : A → CategoryTheory.Functor C C} {zero_1 : F_1 0 ≅ CategoryTheory.Functor.id C}
  {add_1 : (n m : A) → F_1 (n + m) ≅ (F_1 n).comp (F_1 m)}
  {assoc_hom_app_1 :
    autoParam
      (∀ (m₁ m₂ m₃ : A) (X : C),
        CategoryTheory.CategoryStruct.comp ((add_1 (m₁ + m₂) m₃).hom.app X) ((F_1 m₃).map ((add_1 m₁ m₂).hom.app X)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp ((add_1 m₁ (m₂ + m₃)).hom.app X)
              ((add_1 m₂ m₃).hom.app ((F_1 m₁).obj X))))
      CategoryTheory.ShiftMkCore.assoc_hom_app._autoParam}
  {zero_add_hom_app_1 :
    autoParam
      (∀ (n : A) (X : C),
        (add_1 0 n).hom.app X =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((F_1 n).map (zero_1.inv.app X)))
      CategoryTheory.ShiftMkCore.zero_add_hom_app._autoParam}
  {add_zero_hom_app_1 :
    autoParam
      (∀ (n : A) (X : C),
        (add_1 n 0).hom.app X =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (zero_1.inv.app ((F_1 n).obj X)))
      CategoryTheory.ShiftMkCore.add_zero_hom_app._autoParam},
  { F := F, zero := zero, add := add, assoc_hom_app := assoc_hom_app, zero_add_hom_app := zero_add_hom_app,
        add_zero_hom_app := add_zero_hom_app } =
      { F := F_1, zero := zero_1, add := add_1, assoc_hom_app := assoc_hom_app_1,
        zero_add_hom_app := zero_add_hom_app_1, add_zero_hom_app := add_zero_hom_app_1 } →
    F = F_1 ∧ zero ≍ zero_1 ∧ add ≍ add_1
-- Mathlib.Probability.CondVar
ProbabilityTheory.condVar_of_not_integrable : ∀ {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  ¬MeasureTheory.Integrable (fun ω => (X ω - μ[X | m] ω) ^ 2) μ → ProbabilityTheory.condVar m X μ = 0
-- Init.Data.SInt.IntToBitVec
ISize.ne_iff_toBitVec64_ne : ∀ {a b : ISize} (h : System.Platform.numBits = 64), a ≠ b ↔ a.toBitVec64 h ≠ b.toBitVec64 h
-- Mathlib.Order.PartialSups
ciSup_partialSups_eq : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : LocallyFiniteOrderBot ι]
  [inst_2 : ConditionallyCompleteLattice α] {f : ι → α}, BddAbove (Set.range f) → ⨆ i, (partialSups f) i = ⨆ i, f i
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.mapEquiv_trans : ∀ {S₁ : Type v} {S₂ : Type w} {S₃ : Type x} (σ : Type u_1) [inst : CommSemiring S₁] [inst_1 : CommSemiring S₂]
  [inst_2 : CommSemiring S₃] (e : S₁ ≃+* S₂) (f : S₂ ≃+* S₃),
  (MvPolynomial.mapEquiv σ e).trans (MvPolynomial.mapEquiv σ f) = MvPolynomial.mapEquiv σ (e.trans f)
-- Lean.Parser.Term
Lean.Parser.Term.letMVar.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst : ∀ {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.pullbackIsoPullback f g).inv
      (CategoryTheory.Limits.pullback.fst f g) =
    TypeCat.ofHom fun p => (↑p).1
-- Mathlib.Tactic.CancelDenoms.Core
_private.Mathlib.Tactic.CancelDenoms.Core.0.Mathlib.Tactic.cancelDenominatorsAt : Lean.FVarId → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- To construct a morphism between left extensions, we need a 2-morphism between the extensions,
and to check that it is compatible with the units.  -/
CategoryTheory.Bicategory.LeftExtension.homMk : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} →
        {g : a ⟶ c} →
          {s t : CategoryTheory.Bicategory.LeftExtension f g} →
            (η : s.extension ⟶ t.extension) →
              autoParam (CategoryTheory.CategoryStruct.comp s.unit (CategoryTheory.Bicategory.whiskerLeft f η) = t.unit)
                  CategoryTheory.Bicategory.LeftExtension.homMk._auto_1 →
                (s ⟶ t)
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
CochainComplex.mappingConeCompTriangle_mor₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃),
  (CochainComplex.mappingConeCompTriangle f g).mor₃ =
    CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.triangle g).mor₃
      ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (CochainComplex.mappingCone.inr f))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_ofList_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    ∀ {v : β} [inst_4 : Inhabited β],
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l → Std.DHashMap.Raw.Const.get! (Std.DHashMap.Raw.Const.ofList l) k' = v
-- Init.Data.Vector.Lemmas
Vector.pop_empty : ∀ {α : Type u_1}, #v[].pop = #v[]
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_image : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] [inst_1 : OrderBot α] [inst_2 : DecidableEq β]
  (s : Finset γ) (f : γ → β) (g : β → α), (Finset.image f s).sup g = s.sup (g ∘ f)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshotInner.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (toSnapshot : Lean.Language.Snapshot) (stx : Lean.Syntax)
  (inner? : Option (Lean.Language.SnapshotTask α))
  (finished : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticFinishedSnapshot),
  sizeOf { toSnapshot := toSnapshot, stx := stx, inner? := inner?, finished := finished } =
    1 + sizeOf toSnapshot + sizeOf stx + sizeOf inner? + sizeOf finished
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.step_flattenAfter : ∀ {α α₂ β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m (Std.IterM m β)]
  [inst_2 : Std.Iterator α₂ m β] {it₁ : Std.IterM m (Std.IterM m β)} {it₂ : Option (Std.IterM m β)},
  (Std.IterM.flattenAfter✝ it₁ it₂).step =
    match it₂ with
    | none => do
      let __do_lift ← it₁.step
      match __do_lift.inflate with
        | ⟨Std.IterStep.yield it₁' it₂', h⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.flattenAfter✝ it₁' (some it₂')) ⋯))
        | ⟨Std.IterStep.skip it₁', h⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.flattenAfter✝ it₁' none) ⋯))
        | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
    | some it₂ => do
      let __do_lift ← it₂.step
      match __do_lift.inflate with
        | ⟨Std.IterStep.yield it₂' out, h⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.flattenAfter✝ it₁ (some it₂')) out ⋯))
        | ⟨Std.IterStep.skip it₂', h⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.flattenAfter✝ it₁ (some it₂')) ⋯))
        | ⟨Std.IterStep.done, h⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.flattenAfter✝ it₁ none) ⋯))
-- Mathlib.Order.Hom.Basic
OrderHom.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : Preorder α} {inst_1 : Preorder β} {toFun : α → β} {monotone' : Monotone toFun}
  {toFun_1 : α → β} {monotone'_1 : Monotone toFun_1},
  { toFun := toFun, monotone' := monotone' } = { toFun := toFun_1, monotone' := monotone'_1 } → toFun = toFun_1
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.right_inv : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {x : β}, x ∈ e.target → ↑e (↑e.symm x) = x
-- Mathlib.CategoryTheory.Monad.Kleisli
/-- For (T : Monad C), morphisms `c ⟶ c'` in the Kleisli category of `T` are
morphisms ` c ⟶ T.obj c'` in `C`.  -/
CategoryTheory.Kleisli.Hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {T : CategoryTheory.Monad C} → CategoryTheory.Kleisli T → CategoryTheory.Kleisli T → Type v
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instInhabited : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} → [inst_1 : TopologicalSpace β] → [Inhabited β] → Inhabited (α →ₘ[μ] β)
-- Mathlib.Tactic.MkIffOfInductiveProp
/-- Drops the final element of a list.  -/
Mathlib.Tactic.MkIff.List.init : {α : Type u_1} → List α → List α
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
jacobiTheta₂'_neg_left : ∀ (z τ : ℂ), jacobiTheta₂' (-z) τ = -jacobiTheta₂' z τ
-- Mathlib.Algebra.Order.Group.Defs
neg_lt_neg : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b : α}, a < b → -b < -a
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- The underlying partial map of a partial isomorphism.  -/
AlgebraicGeometry.Scheme.PartialIso.toPartialMap : {X Y : AlgebraicGeometry.Scheme} → X.PartialIso Y → X.PartialMap Y
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.aeval_val : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [inst_3 : CommRing R']
  [inst_4 : CommRing S'] [inst_5 : Algebra R' S'] {P' : Algebra.Generators R' S' ι'} [inst_6 : Algebra S S']
  (self : P.Hom P') (i : ι), (MvPolynomial.aeval P'.val) (self.val i) = (algebraMap S S') (P.val i)
-- Lean.Parser.Command
Lean.Parser.Command.where.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.LinearAlgebra.Eigenspace.Minpoly
Matrix.instFiniteSpectrum : ∀ {n : Type u_1} {R : Type u_2} [inst : Field R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (A : Matrix n n R),
  Finite ↑(spectrum R A)
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.truncLT.eq_1 : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero R] [inst_1 : PartialOrder Γ] [inst_2 : DecidableLT Γ] (c : Γ),
  HahnSeries.truncLT c =
    { toFun := fun x => { coeff := fun i => if i < c then x.coeff i else 0, isPWO_support' := ⋯ }, map_zero' := ⋯ }
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.isCycleOn_of_subsingleton : ∀ {α : Type u_2} [Subsingleton α] (f : Equiv.Perm α) (s : Set α), f.IsCycleOn s
-- Mathlib.Algebra.Category.BialgCat.Basic
CategoryTheory.Iso.toBialgEquiv_refl : ∀ {R : Type u} [inst : CommRing R] {X : BialgCat R},
  (CategoryTheory.Iso.refl X).toBialgEquiv = BialgEquiv.refl R X.carrier
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
WeakSpace.instModule : {𝕜 : Type u_2} →
  {E : Type u_4} →
    [inst : CommSemiring 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [inst_2 : ContinuousAdd 𝕜] →
          [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
            [inst_4 : AddCommMonoid E] →
              [inst_5 : Module 𝕜 E] → [inst_6 : TopologicalSpace E] → Module 𝕜 (WeakSpace 𝕜 E)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.extendIso.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) {X : C} (f : s.pt ≅ X),
  s.extendIso f = { hom := { hom := f.hom, w := ⋯ }, inv := { hom := f.inv, w := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_subset_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s₁ s₂ : Finset α}, s₁ ∩ s₂ ⊆ s₂
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, k ∉ t₁ → (t₁ \ t₂).getKey! k = default