mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.instAdditiveTruncLE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ), (t.truncLE n).Additive
-- Mathlib.Analysis.SpecialFunctions.Integrability.Basic
/-- The real logarithm is interval integrable (with respect to the volume measure) on every interval.
See `intervalIntegrable_log` for a version applying to any locally finite measure, but with an
additional hypothesis on the interval.
 -/
intervalIntegral.intervalIntegrable_log' : ∀ {a b : ℝ}, IntervalIntegrable Real.log MeasureTheory.volume a b
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
cfcₙHom_mem_elemental : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A]
  [inst_3 : Module 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : TopologicalSpace A]
  [inst_7 : ContinuousConstSMul 𝕜 A] [inst_8 : StarModule 𝕜 A] [inst_9 : IsTopologicalRing A]
  [inst_10 : ContinuousStar A] [inst_11 : NonUnitalContinuousFunctionalCalculus 𝕜 A p] {a : A} (ha : p a)
  (f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜), (cfcₙHom ha) f ∈ NonUnitalStarAlgebra.elemental 𝕜 a
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
add_le_mul' : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b : R} [ZeroLEOneClass R] [NeZero 1] [MulPosStrictMono R]
  [PosMulStrictMono R] [AddLeftMono R], 2 ≤ a → 2 ≤ b → a + b ≤ b * a
-- Batteries.Data.String.Lemmas
String.Pos.Raw.valid_endPos : ∀ {s : String}, String.Pos.Raw.Valid s s.rawEndPos
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.dvd_prod : ∀ {M : Type u_5} [inst : CommMonoid M] {s : Multiset M} {a : M}, a ∈ s → a ∣ s.prod
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Fintype.sum_nonneg : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : AddCommMonoid M] [inst_2 : Preorder M] [AddLeftMono M]
  {f : ι → M}, 0 ≤ f → 0 ≤ ∑ i, f i
-- Mathlib.Combinatorics.Quiver.Push
Quiver.instNonemptyPush : ∀ {V : Type u_1} {W : Type u_2} (σ : V → W) [h : Nonempty W], Nonempty (Quiver.Push σ)
-- Mathlib.GroupTheory.Sylow
Sylow.eq_bot_of_one : ∀ {G : Type u_1} [inst : Group G] (H : Sylow 1 G), ↑H = ⊥
-- Aesop.Script.StructureDynamic
Aesop.Script.withUpdatedMVarIds : {α : Type} →
  Lean.Meta.SavedState →
    Lean.Meta.SavedState →
      Array Lean.MVarId →
        Array Lean.MVarId → Aesop.Script.DynStructureM α → Aesop.Script.DynStructureM α → Aesop.Script.DynStructureM α
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.arrowArrowEquivalence_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Square.arrowArrowEquivalence.counitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Square.fromArrowArrowFunctor.comp CategoryTheory.Square.toArrowArrowFunctor)
-- Mathlib.Topology.Order
isOpen_sup : ∀ {α : Type u} {t₁ t₂ : TopologicalSpace α} {s : Set α}, IsOpen s ↔ IsOpen s ∧ IsOpen s
-- Lean.Data.Json.Basic
Lean.Json.brecOn_3.eq : ∀ {motive_1 : Lean.Json → Sort u} {motive_2 : Array Lean.Json → Sort u}
  {motive_3 : Std.TreeMap.Raw String Lean.Json compare → Sort u} {motive_4 : List Lean.Json → Sort u}
  {motive_5 : Std.DTreeMap.Raw String (fun x => Lean.Json) compare → Sort u}
  {motive_6 : (Std.DTreeMap.Internal.Impl String fun x => Lean.Json) → Sort u} (t : List Lean.Json)
  (F_1 : (t : Lean.Json) → t.below → motive_1 t) (F_2 : (t : Array Lean.Json) → Lean.Json.below_1 t → motive_2 t)
  (F_3 : (t : Std.TreeMap.Raw String Lean.Json compare) → Lean.Json.below_2 t → motive_3 t)
  (F_4 : (t : List Lean.Json) → Lean.Json.below_3 t → motive_4 t)
  (F_5 : (t : Std.DTreeMap.Raw String (fun x => Lean.Json) compare) → Lean.Json.below_4 t → motive_5 t)
  (F_6 : (t : Std.DTreeMap.Internal.Impl String fun x => Lean.Json) → Lean.Json.below_5 t → motive_6 t),
  Lean.Json.brecOn_3 t F_1 F_2 F_3 F_4 F_5 F_6 = F_4 t (Lean.Json.brecOn_3.go t F_1 F_2 F_3 F_4 F_5 F_6).2
-- Mathlib.CategoryTheory.Bicategory.Coherence
CategoryTheory.FreeBicategory.normalizeAux.eq_2 : ∀ {B : Type u} [inst : Quiver B] {a : B} (x : B) (x_1 : Quiver.Path a x),
  CategoryTheory.FreeBicategory.normalizeAux x_1 (CategoryTheory.FreeBicategory.Hom.id x) = x_1
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.limitsOfShape.mk' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] (X₁ X₂ : CategoryTheory.Functor J C)
  (c₁ : CategoryTheory.Limits.Cone X₁) (c₂ : CategoryTheory.Limits.Cone X₂) (h₁ : CategoryTheory.Limits.IsLimit c₁)
  (h₂ : CategoryTheory.Limits.IsLimit c₂) (f : X₁ ⟶ X₂),
  W.functorCategory J f →
    ∀ (φ : c₁.pt ⟶ c₂.pt),
      (∀ (j : J),
          CategoryTheory.CategoryStruct.comp φ (c₂.π.app j) =
            CategoryTheory.CategoryStruct.comp (c₁.π.app j) (f.app j)) →
        W.limitsOfShape J φ
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.delete_contract_delete : ∀ {α : Type u_1} (M : Matroid α) (D C D' : Set α),
  Disjoint C D → ((M.delete D).contract C).delete D' = (M.contract C).delete (D ∪ D')
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.IsSymmetric.mul : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {φ ψ : MvPolynomial σ R},
  φ.IsSymmetric → ψ.IsSymmetric → (φ * ψ).IsSymmetric
-- Mathlib.Data.Finsupp.Basic
Finsupp.filter.congr_simp : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (p p_1 : α → Prop),
  p = p_1 →
    ∀ {inst_1 : DecidablePred p} [inst_2 : DecidablePred p_1] (f f_1 : α →₀ M),
      f = f_1 → Finsupp.filter p f = Finsupp.filter p_1 f_1
-- Mathlib.Algebra.Star.Module
/-- If `A` is a module over a commutative `R` with compatible actions,
then `star` is a semilinear equivalence.  -/
starLinearEquiv : (R : Type u_1) →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : AddCommMonoid A] → [inst_3 : StarAddMonoid A] → [inst_4 : Module R A] → [StarModule R A] → A ≃ₗ⋆[R] A
-- Mathlib.Analysis.Distribution.Support
Distribution.notMem_dsupport_iff_eventually : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [inst : FunLike F α β] [inst_1 : TopologicalSpace α]
  [inst_2 : Zero β] [inst_3 : Zero V] {f : F → V} {x : α},
  x ∉ Distribution.dsupport f ↔ ∀ᶠ (u : Set α) in (nhds x).smallSets, Distribution.IsVanishingOn f u
-- Std.Time.Format.Modifier
/-- `c`: Stand-alone day of week as number or text (e.g., 2, Tue, Tuesday, T).
Stand-alone means the day is used independently (e.g., a calendar column header) rather than as part of a full date.
Unlike `e`, `cc` (count of 2) is not valid; the minimum is `c` (1 letter) or `ccc` (3 letters).
 -/
Std.Time.Modifier.c : Std.Time.Number ⊕ Std.Time.Text → Std.Time.Modifier
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.toNonUnitalCommRing : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : NonUnitalCommRing A] →
        [inst_2 : Module R A] → [inst_3 : Star A] → (S : NonUnitalStarSubalgebra R A) → NonUnitalCommRing ↥S
-- Mathlib.Order.RelIso.Basic
RelHom.mk.sizeOf_spec : ∀ {α : Type u_5} {β : Type u_6} {r : α → α → Prop} {s : β → β → Prop} [inst : SizeOf α] [inst_1 : SizeOf β]
  [inst_2 : (a a_1 : α) → SizeOf (r a a_1)] [inst_3 : (a a_1 : β) → SizeOf (s a a_1)] (toFun : α → β)
  (map_rel' : ∀ {a b : α}, r a b → s (toFun a) (toFun b)), sizeOf { toFun := toFun, map_rel' := map_rel' } = 1
-- Std.Data.DHashMap.IteratorLemmas
Std.DHashMap.Raw.toList_iter : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β}, m.iter.toList = m.toList
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.ofCoeff_smul : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {A : Type u_8} [inst_1 : SMulZeroClass A R] (a : A) (x : M →₀ R),
  AddMonoidAlgebra.ofCoeff (a • x) = a • AddMonoidAlgebra.ofCoeff x
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.foldlM.match_1.eq_2 : ∀ {σ : Type u_3} {α : Type u_1} (motive : σ → RBTree.RBNode α → Sort u_2) (b : σ) (c : RBTree.RBColor)
  (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α) (h_1 : (b : σ) → motive b RBTree.RBNode.nil)
  (h_2 :
    (b : σ) →
      (c : RBTree.RBColor) →
        (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive b (RBTree.RBNode.node c l v r)),
  (match b, RBTree.RBNode.node c l v r with
    | b, RBTree.RBNode.nil => h_1 b
    | b, RBTree.RBNode.node c l v r => h_2 b c l v r) =
    h_2 b c l v r
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.lift_lt_aleph_ofNat : ∀ {c : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo],
  Cardinal.lift.{v, u} c < Cardinal.aleph (OfNat.ofNat n) ↔ c < Cardinal.aleph (OfNat.ofNat n)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.map_swap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) f)
      (CategoryTheory.Limits.prod.map g (CategoryTheory.CategoryStruct.id B)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map g (CategoryTheory.CategoryStruct.id A))
      (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id Y) f)
-- Mathlib.Data.Nat.Totient
Even.eq_of_totient_eq_totient : ∀ {a b : ℕ}, a ∣ b → Even a → a.totient = b.totient → a = b
-- Aesop.Nanos
Aesop.instBEqNanos : BEq Aesop.Nanos
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.exists_of_compat : ∀ {X : Type u_2} [inst : TopologicalSpace X] [CompactSpace X] (Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid),
  (∀ (A B : DiscreteQuotient X) (h : A ≤ B), DiscreteQuotient.ofLE h (Qs A) = Qs B) →
    ∃ x, ∀ (Q : DiscreteQuotient X), Q.proj x = Qs Q
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.sat_of_insertRup : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ReadyForRupAdd →
    ∀ (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (p : Std.Tactic.BVDecide.LRAT.Internal.PosFin n → Bool),
      Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p f →
        (f.insertRupUnits c.negate).2 = true → Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.mem_ofList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α}, k ∈ Std.DTreeMap.Const.ofList l cmp ↔ (List.map Prod.fst l).contains k = true
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (hom : X ⟶ Y) (inv : Y ⟶ X)
  (hom_inv_id :
    autoParam (CategoryTheory.CategoryStruct.comp hom inv = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.Iso.hom_inv_id._autoParam)
  (inv_hom_id :
    autoParam (CategoryTheory.CategoryStruct.comp inv hom = CategoryTheory.CategoryStruct.id Y)
      CategoryTheory.Iso.inv_hom_id._autoParam)
  (hom_1 : X ⟶ Y) (inv_1 : Y ⟶ X)
  (hom_inv_id_1 :
    autoParam (CategoryTheory.CategoryStruct.comp hom_1 inv_1 = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.Iso.hom_inv_id._autoParam)
  (inv_hom_id_1 :
    autoParam (CategoryTheory.CategoryStruct.comp inv_1 hom_1 = CategoryTheory.CategoryStruct.id Y)
      CategoryTheory.Iso.inv_hom_id._autoParam),
  ({ hom := hom, inv := inv, hom_inv_id := hom_inv_id, inv_hom_id := inv_hom_id } =
      { hom := hom_1, inv := inv_1, hom_inv_id := hom_inv_id_1, inv_hom_id := inv_hom_id_1 }) =
    (hom = hom_1 ∧ inv = inv_1)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C},
  (∀ {A A' B B' : C} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'},
      CategoryTheory.IsPushout g f f' g' → P f → P f') →
    P.IsStableUnderCobaseChange
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.instInhabited : {α : Type u_1} → Inhabited (FreeMonoid α)
-- Init.Data.Nat.Bitwise.Lemmas
Nat.and_or_distrib_left : ∀ (x y z : ℕ), x &&& (y ||| z) = x &&& y ||| x &&& z
-- Lean.Parser.Term
/-- Defines a possibly non-terminating function as a fixed-point in a suitable partial order.

Such a function is compiled as if it was marked `partial`, but its equations are provided as
theorems, so that it can be verified.

In general it accepts functions whose return type has a `Lean.Order.CCPO` instance and whose
definition is `Lean.Order.monotone` with regard to its recursive calls.

Common special cases are

* Functions whose type is inhabited a-priori (as with `partial`), and where all recursive
  calls are in tail-call position.
* Monadic in certain “monotone chain-complete monads” (in particular, `Option`) composed using
  the bind operator and other supported monadic combinators.

By default, the monotonicity proof is performed by the compositional `monotonicity` tactic. Using
the syntax `partial_fixpoint monotonicity by $tac` the proof can be done manually.
 -/
Lean.Parser.Termination.partialFixpoint : Lean.Parser.Parser
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
instCoeSortProfiniteAddGrpType.eq_1 : instCoeSortProfiniteAddGrpType = { coe := fun G => ↑G.toProfinite.toTop }
-- Mathlib.SetTheory.ZFC.PSet
PSet.Equiv.refl : ∀ (x : PSet.{u_1}), x.Equiv x
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Iso.compInverseIso_hom_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] {F : CategoryTheory.Functor C E}
  {G : CategoryTheory.Functor C D} {H : D ≌ E} (i : F ≅ G.comp H.functor) (X : C),
  i.compInverseIso.hom.app X =
    CategoryTheory.CategoryStruct.comp (H.inverse.map (i.hom.app X)) (H.unitIso.inv.app (G.obj X))
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpToOn.zero_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {f : E → F} {p : E → FormalMultilinearSeries 𝕜 E F} {s : Set E},
  HasFTaylorSeriesUpToOn n f p s → ∀ x ∈ s, (p x 0).curry0 = f x
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.withLetDeclImp : {α : Type} → Lean.Name → Lean.Expr → Lean.Expr → (Lean.Expr → Lean.MetaM α) → Bool → Lean.LocalDeclKind → Lean.MetaM α
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeList_eq_takeListTR.go : ∀ (α : Type u_1) (acc : Array (List α)) (ns : List ℕ) (xs : List α),
  List.takeListTR.go ns xs acc =
    match xs.takeList ns with
    | (l, r) => (acc.toList ++ l, r)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k a : α},
  a ∈ t.erase k ↔ cmp k a ≠ Ordering.eq ∧ a ∈ t
-- Lean.Parser.Basic
Lean.Parser.fieldIdxFn : Lean.Parser.ParserFn
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.SpecToEquivOfLocalRing_apply_snd_coe : ∀ (X : AlgebraicGeometry.Scheme) (R : CommRingCat) [inst : IsLocalRing ↑R] (f : AlgebraicGeometry.Spec R ⟶ X),
  ↑((AlgebraicGeometry.SpecToEquivOfLocalRing X R) f).snd = AlgebraicGeometry.Scheme.stalkClosedPointTo f
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.MonicDegreeEq.mk_coe : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] (p : Polynomial R) (hp : p.Monic) (hp' : p.natDegree = n),
  ↑(Polynomial.MonicDegreeEq.mk p hp hp') = p
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.ediam_eq_top_of_not_preconnected : ∀ {α : Type u_1} {G : SimpleGraph α}, ¬G.Preconnected → G.ediam = ⊤
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getEntryGTD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : α × β}, t₁.Equiv t₂ → t₁.getEntryGTD k fallback = t₂.getEntryGTD k fallback
-- Std.Time.Time.PlainTime
Std.Time.PlainTime.ext : ∀ {x y : Std.Time.PlainTime},
  x.hour = y.hour → x.minute = y.minute → x.second = y.second → x.nanosecond = y.nanosecond → x = y
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_inv_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] (K : CochainComplex C ℤ) (n i : ℤ),
  ((CategoryTheory.Functor.commShiftIso (F.mapHomologicalComplex (ComplexShape.up ℤ)) n).inv.app K).f i =
    CategoryTheory.CategoryStruct.id
      ((((F.mapHomologicalComplex (ComplexShape.up ℤ)).comp
                (CategoryTheory.shiftFunctor (HomologicalComplex D (ComplexShape.up ℤ)) n)).obj
            K).X
        i)
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.below.mul_compat_right : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R]
  {motive : (a a_1 : FreeAlgebra.Pre R X) → FreeAlgebra.Rel R X a a_1 → Prop} {a b c : FreeAlgebra.Pre R X}
  (a_1 : FreeAlgebra.Rel R X a b), FreeAlgebra.Rel.below a_1 → motive a b a_1 → FreeAlgebra.Rel.below ⋯
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.homInhabited : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (M : CategoryTheory.Mon C) → Inhabited (M.Hom M)
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderivWithin_comp_of_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M' → M} {g : M → 𝕜} {x : M'}
  {y : M} {u : Set M} {s : Set M'},
  MDiffAt[u] g y →
    MDiffAt[s] f x → s ⊆ f ⁻¹' u → UniqueMDiffAt[s] x → f x = y → d[s] (g ∘ f) x = d[u] g y ∘SL mfderiv[s] f x
-- Mathlib.CategoryTheory.Limits.Sifted
/-- Through the isomorphisms `PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂` and
`externalProductCompDiagIso`, the comparison map `colimit.pre (X ⊠ Y) (diag C)` identifies with the
product comparison map for the colimit functor.  -/
CategoryTheory.IsSifted.factorization_prodComparison_colim : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] (X Y : CategoryTheory.Functor C (Type u)),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.HasColimit.isoOfNatIso
          ((CategoryTheory.MonoidalCategory.externalProductCompDiagIso C (Type u)).app (X, Y)).symm).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.colimit.pre (CategoryTheory.MonoidalCategory.externalProduct X Y)
          (CategoryTheory.Functor.diag C))
        (CategoryTheory.Limits.PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ X Y
            (CategoryTheory.MonoidalCategory.curriedTensor (Type u))).hom) =
    CategoryTheory.CartesianMonoidalCategory.prodComparison CategoryTheory.Limits.colim X Y
-- Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
/-- Module of functions that are zero at infinity.  -/
UpperHalfPlane.zeroAtImInftySubmodule : (α : Type u_1) → [inst : NormedField α] → Submodule α (UpperHalfPlane → α)
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- On a set with unique differentiability, any choice of iterated differential has to coincide
with the one we have chosen in `iteratedFDerivWithin 𝕜 m f s`.  -/
HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpToOn n f p s → ∀ {m : ℕ}, ↑m ≤ n → UniqueDiffOn 𝕜 s → x ∈ s → p x m = iteratedFDerivWithin 𝕜 m f s x
-- Mathlib.NumberTheory.ModularForms.NormTrace
ModularForm.coe_trace : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f : F) [inst : FunLike F UpperHalfPlane ℂ]
  {k : ℤ} [inst_1 : 𝒢.IsFiniteRelIndex ℋ] [inst_2 : ModularFormClass F 𝒢 k],
  ⇑(ModularForm.trace ℋ f) = ∑ q, SlashInvariantForm.quotientFunc f q
-- Mathlib.Order.OrderIsoNat
not_strictAnti_of_wellFoundedLT : ∀ {α : Type u_1} [inst : Preorder α] [WellFoundedLT α] (f : ℕ → α), ¬StrictAnti f
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.vadd_mem_inter_orthRadius_iff_norm_sq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p : P} {v : V},
  0 ≤ s.radius →
    v ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ →
      (v +ᵥ p ∈ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) ↔ ‖v‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.ball_infDist_compl_subset : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α}, Metric.ball x (Metric.infDist x sᶜ) ⊆ s
-- Mathlib.Algebra.GradedMonoid
/-- A graded version of `Mul`. Multiplication combines grades additively, like
`AddMonoidAlgebra`.  -/
GradedMonoid.GMul : {ι : Type u_1} → (ι → Type u_2) → [Add ι] → Type (max u_1 u_2)
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.indiscreteTopology_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  IndiscreteTopology X ↔ IndiscreteTopology Y
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.unop_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y) [inst_1 : CategoryTheory.IsIso f],
  (CategoryTheory.inv f).unop = CategoryTheory.inv f.unop
-- Mathlib.Algebra.DirectSum.Internal
SetLike.GradeZero.coe_algebraMap : ∀ {ι : Type u_1} {S : Type u_3} {R : Type u_4} [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : Algebra S R]
  [inst_3 : AddMonoid ι] (A : ι → Submodule S R) [inst_4 : SetLike.GradedMonoid A] (s : S),
  ↑((algebraMap S ↥(A 0)) s) = (algebraMap S R) s
-- Mathlib.Order.Concept
Concept.extent_iInf : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (f : ι → Concept α β r),
  (⨅ i, f i).extent = ⋂ i, (f i).extent
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.HeapNode.rankTR.go.eq_2 : ∀ {α : Type u_1} (a : ℕ) (a_1 : α) (child s : Batteries.BinomialHeap.Imp.HeapNode α),
  Batteries.BinomialHeap.Imp.HeapNode.rankTR.go (Batteries.BinomialHeap.Imp.HeapNode.node a_1 child s) a =
    Batteries.BinomialHeap.Imp.HeapNode.rankTR.go s (a + 1)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_erase_le : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m.erase k).size ≤ m.size
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.hom_ext : ∀ {R : Type u} [inst : CommRing R] {A B : CommHopfAlgCat R} {f g : A ⟶ B},
  CommHopfAlgCat.Hom.hom f = CommHopfAlgCat.Hom.hom g → f = g
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.AEval.X_pow_smul_of : ∀ {R : Type u_2} {A : Type u_3} {M : Type u_1} [inst : CommSemiring R] [inst_1 : Semiring A] (a : A)
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R A M] (m : M) (n : ℕ),
  Polynomial.X ^ n • (Module.AEval.of R M a) m = (Module.AEval.of R M a) (a ^ n • m)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.instUniqueLOfLinearOrderBool : Unique (CategoryTheory.Limits.MultispanShape.ofLinearOrder Bool).L