mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  (k : α) (v : β), m₁.Equiv m₂ → (m₁.insert k v).Equiv (m₂.insert k v)
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
Mathlib.Tactic.Bicategory.instMonadMor₂IsoBicategoryM : Mathlib.Tactic.BicategoryLike.MonadMor₂Iso Mathlib.Tactic.Bicategory.BicategoryM
-- Mathlib.Topology.Instances.ENNReal.Lemmas
Real.diam_Icc : ∀ {a b : ℝ}, a ≤ b → Metric.diam (Set.Icc a b) = b - a
-- Init.Data.String.Lemmas.Basic
String.sliceTo_eq_toSlice_iff : ∀ {s : String} {p : s.Pos}, s.sliceTo p = s.toSlice ↔ p = s.endPos
-- Lean.Meta.Sym.Eta
_private.Lean.Meta.Sym.Eta.0.Lean.Meta.Sym.etaReduce.go : Lean.Expr → Lean.Expr → ℕ → Lean.Expr
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.WSeq.destruct.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 (Option α)) → Sort u_2) (s' : Stream'.Seq (Option α))
  (h_1 : Unit → motive none) (h_2 : (s' : Stream'.Seq (Option α)) → motive (some (none, s')))
  (h_3 : (a : α) → (s' : Stream'.Seq (Option α)) → motive (some (some a, s'))),
  (match some (none, s') with
    | none => h_1 ()
    | some (none, s') => h_2 s'
    | some (some a, s') => h_3 a s') =
    h_2 s'
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_add_ofNat_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ) [inst_4 : m.AtLeastTwo],
  toIcoDiv hp a (b + OfNat.ofNat m * p) = toIcoDiv hp a b + OfNat.ofNat m
-- Mathlib.Data.Set.NAry
Set.Nonempty.of_image2_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β},
  (Set.image2 f s t).Nonempty → t.Nonempty
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_eq_of_eq : ∀ {a b : UInt16}, a = b → a.toBitVec = b.toBitVec
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.killCompl_monomial : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {f : σ → τ} (hf : Function.Injective f)
  {s : τ →₀ ℕ} {c : R} [inst_1 : Decidable (↑s.support ⊆ Set.range f)],
  (MvPolynomial.killCompl hf) ((MvPolynomial.monomial s) c) =
    if ↑s.support ⊆ Set.range f then (MvPolynomial.monomial (Finsupp.comapDomain f s ⋯)) c else 0
-- Mathlib.Topology.Algebra.Group.Basic
IsTopologicalAddGroup.of_comm_of_nhds_zero : ∀ {G : Type u} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G],
  Filter.Tendsto (Function.uncurry fun x1 x2 => x1 + x2) (nhds 0 ×ˢ nhds 0) (nhds 0) →
    Filter.Tendsto (fun x => -x) (nhds 0) (nhds 0) →
      (∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ + x) (nhds 0)) → IsTopologicalAddGroup G
-- Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
UpperHalfPlane.atImInfty_mem : ∀ (S : Set UpperHalfPlane), S ∈ UpperHalfPlane.atImInfty ↔ ∃ A, ∀ (z : UpperHalfPlane), A ≤ z.im → z ∈ S
-- Mathlib.Order.Filter.Pointwise
Filter.mem_div : ∀ {α : Type u_2} [inst : Div α] {f g : Filter α} {s : Set α}, s ∈ f / g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ / t₂ ⊆ s
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_forall_integrable_exp_mul : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ ν →
    ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) (κ ω')
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- Composition of morphisms of monoid objects.  -/
CategoryTheory.Comon.comp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → {M N O : CategoryTheory.Comon C} → M.Hom N → N.Hom O → M.Hom O
-- Mathlib.CategoryTheory.Preadditive.Comma
/-- If a category `T` is preadditive, then so is its category of arrows.
 -/
CategoryTheory.instPreadditiveArrow : {T : Type u₃} →
  [inst : CategoryTheory.Category.{v₃, u₃} T] →
    [CategoryTheory.Preadditive T] → CategoryTheory.Preadditive (CategoryTheory.Arrow T)
-- Mathlib.Algebra.Free
FreeSemigroup.map_pure : ∀ {α β : Type u} (f : α → β) (x : α), f <$> pure x = pure (f x)
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.map_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (P : HomotopicalAlgebra.PrepathObject X) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D), (P.map F).ι = F.map P.ι
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
Std.IterM.map_unattach_toArray_attachWith : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {P : β → Prop} {n : Type u_1 → Type u_2} [inst : Std.Iterator α m β]
  [inst_1 : Monad m] [Monad n] {it : Std.IterM m β} {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out}
  [Std.Iterators.Finite α m] [LawfulMonad m],
  (fun x => Array.map Subtype.val x) <$> (it.attachWith P hP).toArray = it.toArray
-- Lean.Elab.Tactic.Try
/-- Returns tactic kinds that could solve all subgoals.  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.getKindsSolvedAll : Array (Array (Lean.TSyntax `tactic)) → Array Lean.SyntaxNodeKind
-- Mathlib.Analysis.RCLike.Lemmas
/-- A finite-dimensional vector space over an `RCLike` is a proper metric space.

This is not an instance because it would cause a search for `FiniteDimensional ?x E` before
`RCLike ?x`.  -/
FiniteDimensional.proper_rclike : ∀ (K : Type u_1) (E : Type u_2) [inst : RCLike K] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace K E]
  [FiniteDimensional K E], ProperSpace E
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.Batteries.AssocList.forIn.match_1.splitter : {δ : Type u_1} →
  (motive : ForInStep δ → Sort u_2) →
    (__do_lift : ForInStep δ) →
      ((d : δ) → motive (ForInStep.done d)) → ((d : δ) → motive (ForInStep.yield d)) → motive __do_lift
-- Mathlib.Topology.Algebra.Order.Field
Filter.Tendsto.inv_tendsto_nhdsLT_zero : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f : α → 𝕜},
  Filter.Tendsto f l (nhdsWithin 0 (Set.Iio 0)) → Filter.Tendsto f⁻¹ l Filter.atBot
-- Init.Data.Array.Lemmas
Array.push_eq_push : ∀ {α : Type u_1} {a b : α} {xs ys : Array α}, xs.push a = ys.push b ↔ a = b ∧ xs = ys
-- Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
/-- An orthogonal family of subspaces of `E` satisfies `DirectSum.IsInternal` (that is,
they provide an internal direct sum decomposition of `E`) if and only if their span has trivial
orthogonal complement.  -/
OrthogonalFamily.isInternal_iff_of_isComplete : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} [inst_3 : DecidableEq ι] {V : ι → Submodule 𝕜 E},
  (OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) →
    IsComplete ↑(iSup V) → (DirectSum.IsInternal V ↔ (iSup V)ᗮ = ⊥)
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.instIsBoundedSMul : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β]
  {R : Type u_4} [inst_3 : Zero R] [inst_4 : Zero β] [inst_5 : PseudoMetricSpace R] [inst_6 : SMul R β]
  [inst_7 : IsBoundedSMul R β], IsBoundedSMul R C(α, β)
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_comp_right : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : One M] {s : Set α} (f : β → α) {g : α → M} {x : β},
  (f ⁻¹' s).mulIndicator (g ∘ f) x = s.mulIndicator g (f x)
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
CategoryTheory.Bicategory.instIsLocallyDiscreteLocallyDiscrete : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C],
  CategoryTheory.Bicategory.IsLocallyDiscrete (CategoryTheory.LocallyDiscrete C)
-- Mathlib.Topology.Algebra.AsymptoticCone
/-- In a topological affine space `P` over `k`, `AffineSpace.asymptoticNhds k P v` is the filter of
neighborhoods at infinity in directions near `v`. In a topological vector space, this is the filter
`Filter.atTop • 𝓝 v`. To support affine spaces, the actual definition is different and should be
considered an implementation detail. Use `AffineSpace.asymptoticNhds_eq_smul` or
`AffineSpace.asymptoticNhds_eq_smul_vadd` for unfolding.  -/
AffineSpace.asymptoticNhds : (k : Type u_1) →
  {V : Type u_2} →
    (P : Type u_3) →
      [inst : Field k] →
        [LinearOrder k] →
          [inst_2 : AddCommGroup V] → [Module k V] → [AddTorsor V P] → [TopologicalSpace V] → V → Filter P
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- `span f g` is the functor from the walking span hitting `f` and `g`.  -/
CategoryTheory.Limits.span : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} → (X ⟶ Y) → (X ⟶ Z) → CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_pos_of_finite : ∀ {α : Type u_1} [inst : EMetricSpace α] {s : Set α} [Finite ↑s], 0 < s.einfsep
-- Lean.Expr
/-- Given `a b : Nat`, return `a ≤ b`  -/
Lean.mkNatLE : Lean.Expr → Lean.Expr → Lean.Expr
-- Lean.Environment
Lean.Kernel.Exception.excessiveMemory.sizeOf_spec : sizeOf Lean.Kernel.Exception.excessiveMemory = 1
-- Mathlib.GroupTheory.GroupExtension.Basic
GroupExtension.IsConj.setoid.eq_1 : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {E : Type u_3} [inst_2 : Group E]
  (S : GroupExtension N E G), GroupExtension.IsConj.setoid S = { r := S.IsConj, iseqv := ⋯ }
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- For `f : F` where `F` is a class of continuous monoid hom, this yields an element
`ContinuousMonoidHom A B`.  -/
ContinuousMonoidHom.ofClass : (A : Type u_2) →
  (B : Type u_3) →
    [inst : Monoid A] →
      [inst_1 : Monoid B] →
        [inst_2 : TopologicalSpace A] →
          [inst_3 : TopologicalSpace B] →
            (F : Type u_7) →
              [inst_4 : FunLike F A B] → [ContinuousMapClass F A B] → [MonoidHomClass F A B] → F → A →ₜ* B
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Notation for `tensorHom`, the tensor product of morphisms in a monoidal category  -/
CategoryTheory.MonoidalCategory.«term_⊗ₘ_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Group.Pi.Basic
Pi.monoid : {I : Type u} → {f : I → Type v₁} → [(i : I) → Monoid (f i)] → Monoid ((i : I) → f i)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.of_keys_unit_perm : ∀ {α : Type u} {m₁ m₂ : Std.HashMap.Raw α Unit}, m₁.keys.Perm m₂.keys → m₁.Equiv m₂
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.mem_supportAddSubgroup : ∀ {R : Type u_1} [inst : CommRing R] {P : RingPreordering R} {x : R}, x ∈ P.supportAddSubgroup ↔ x ∈ P ∧ -x ∈ P
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {k a : α},
  Std.DTreeMap.Const.get! (t.erase k) a = if cmp k a = Ordering.eq then default else Std.DTreeMap.Const.get! t a
-- Mathlib.Data.Fintype.Order
/-- A nonempty finite linear order is complete. If the linear order is already a `BoundedOrder`,
then use `Fintype.toCompleteLinearOrder` instead, as this gives definitional equality for `⊥` and
`⊤`.  -/
Fintype.toCompleteLinearOrderOfNonempty : (α : Type u_2) → [Fintype α] → [Nonempty α] → [LinearOrder α] → CompleteLinearOrder α
-- Mathlib.Algebra.Lie.Submodule
/-- The range of a morphism of Lie modules `f : M → N` is a Lie submodule of `N`.
See Note [range copy pattern].  -/
LieModuleHom.range : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : Module R M] →
                [inst_4 : LieRingModule L M] →
                  [inst_5 : AddCommGroup N] →
                    [inst_6 : Module R N] → [inst_7 : LieRingModule L N] → (M →ₗ⁅R,L⁆ N) → LieSubmodule R L N
-- Mathlib.Data.Multiset.Antidiagonal
Multiset.card_antidiagonal : ∀ {α : Type u_1} (s : Multiset α), s.antidiagonal.card = 2 ^ s.card
-- Mathlib.Analysis.Calculus.Deriv.Abs
hasStrictDerivAt_abs_pos : ∀ {x : ℝ}, 0 < x → HasStrictDerivAt (fun x => |x|) 1 x
-- Mathlib.Topology.UniformSpace.Closeds
UniformSpace.hausdorff.nhds_closure : ∀ {α : Type u_1} [inst : UniformSpace α] (s : Set α), nhds (closure s) = nhds s
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.uniqueOfSubsingleton : {V : Type u} → [Subsingleton V] → Unique (SimpleGraph V)
-- Mathlib.GroupTheory.NoncommPiCoprod
MonoidHom.independent_range_of_coprime_order : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Type u_3} [inst_1 : (i : ι) → Group (H i)]
  (ϕ : (i : ι) → H i →* G),
  (Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)) →
    ∀ [Finite ι] [inst_3 : (i : ι) → Fintype (H i)],
      (Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))) → iSupIndep fun i => (ϕ i).range
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.eq_zero_or_eq_zero_of_kahler_eq_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) {x y : E}, (o.kahler x) y = 0 → x = 0 ∨ y = 0
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.ofList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)},
  (Std.TreeMap.Raw.ofList l cmp).WF
-- Mathlib.FieldTheory.SeparableClosure
Field.finInsepDegree_self : ∀ (F : Type u) [inst : Field F], Field.finInsepDegree F F = 1
-- Mathlib.Topology.Instances.AddCircle.Real
/-- The product indexed by `d` of copies of the unit circle.  -/
UnitAddTorus : Type u_1 → Type u_1
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
Lean.Meta.Grind.Arith.CommRing.checkInst : Lean.Name → Lean.Expr → Lean.Expr → Lean.MetaM Unit
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.instToStringPenroseVar : ToString Mathlib.Tactic.Widget.StringDiagram.PenroseVar
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ici_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a : α} (b : ↑(Set.Ici a)), Subtype.val '' Set.Ici b = Set.Ici ↑b
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Cofork.op_π_app_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Cofork f g),
  c.op.π.app CategoryTheory.Limits.WalkingParallelPair.one = (c.ι.app CategoryTheory.Limits.WalkingParallelPair.zero).op
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
MeasureTheory.SNormLESNormFDerivOfEqConst_def : ∀ (F : Type u_6) [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {E : Type u_7} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E] [inst_6 : FiniteDimensional ℝ E]
  (μ : MeasureTheory.Measure E) [inst_7 : μ.IsAddHaarMeasure] [inst_8 : FiniteDimensional ℝ F] (p : ℝ),
  MeasureTheory.SNormLESNormFDerivOfEqConst F μ p =
    let F' := EuclideanSpace ℝ (Fin (Module.finrank ℝ F));
    have e := toEuclidean;
    ‖↑e.symm‖₊ * MeasureTheory.eLpNormLESNormFDerivOfEqInnerConst μ p * ‖↑e‖₊
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_le_self : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), ⁅H, H⁆ ≤ H
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedSubgroup.instCoeSubgroup : (G : Type u) → [inst : Group G] → [inst_1 : TopologicalSpace G] → Coe (ClosedSubgroup G) (Subgroup G)
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.UnitaryGroup.map_star_coe : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
  (U : ↥(Matrix.unitaryGroup n α)), ↑(Matrix.UnitaryGroup.map_star U) = (↑U).map star
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.pbool : Std.Internal.Parsec.ByteArray.Parser Bool
-- Mathlib.RingTheory.PowerSeries.PiTopology
/-- A power series is the sum (in the sense of summable families) of its monomials  -/
PowerSeries.hasSum_of_monomials_self : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : TopologicalSpace R] (f : PowerSeries R),
  HasSum (fun d => (PowerSeries.monomial d) ((PowerSeries.coeff d) f)) f
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.leadingCoeff_monomial : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {d : σ →₀ ℕ} (c : R),
  m.leadingCoeff ((MvPolynomial.monomial d) c) = c
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_π_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X)
  (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F))
  (Z : CategoryTheory.Limits.WalkingParallelPair),
  ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U).obj c).π.app Z =
    CategoryTheory.Limits.WalkingParallelPair.rec
      (CategoryTheory.Limits.Pi.lift fun i => c.π.app (Opposite.op (CategoryTheory.Pairwise.single i)))
      (CategoryTheory.Limits.Pi.lift fun b => c.π.app (Opposite.op (CategoryTheory.Pairwise.pair b.1 b.2))) Z
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_Ioc_succ_top : ∀ {M : Type u_3} [inst : AddCommMonoid M] {a b : ℕ},
  a ≤ b → ∀ (f : ℕ → M), ∑ k ∈ Finset.Ioc a (b + 1), f k = ∑ k ∈ Finset.Ioc a b, f k + f (b + 1)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.simp_prefix.injEq : ∀ (lhs : Bool) (s : Lean.Grind.AC.Seq) (c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr) (lhs_1 : Bool) (s_1 : Lean.Grind.AC.Seq)
  (c₁_1 c₂_1 : Lean.Meta.Grind.AC.EqCnstr),
  (Lean.Meta.Grind.AC.EqCnstrProof.simp_prefix lhs s c₁ c₂ =
      Lean.Meta.Grind.AC.EqCnstrProof.simp_prefix lhs_1 s_1 c₁_1 c₂_1) =
    (lhs = lhs_1 ∧ s = s_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.hasLeftResolutions_arrow_of_essSurj_of_full : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {W₁' : CategoryTheory.MorphismProperty D₁}
  {W₂' : CategoryTheory.MorphismProperty D₂} {T : CategoryTheory.LocalizerMorphism W₁ W₂}
  {L : CategoryTheory.LocalizerMorphism W₁ W₁'} {R : CategoryTheory.LocalizerMorphism W₂ W₂'}
  {B : CategoryTheory.LocalizerMorphism W₁' W₂'} [R.functor.EssSurj] [R.functor.Full] [W₂'.RespectsIso]
  (iso : T.functor.comp R.functor ≅ L.functor.comp B.functor) [T.arrow.HasLeftResolutions], B.arrow.HasLeftResolutions
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` preserves colimits of `K.leftOp : Jᵒᵖ ⥤ C`, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves
limits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.preservesLimit_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J Cᵒᵖ)
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimit K.leftOp F],
  CategoryTheory.Limits.PreservesLimit K F.op
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_mono : ∀ {k : Type u_1} {V1 : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : LinearOrder k] [inst_4 : Preorder V1] [AddRightMono V1] [SMulPosMono k V1] {p₀ p₁ : V1},
  p₀ ≤ p₁ → Monotone ⇑(AffineMap.lineMap p₀ p₁)
-- Mathlib.Tactic.Linter.TextBased
/-- Verifies that all modules in `modules` are named in `UpperCamelCase`
(except for explicitly discussed exceptions, which are hard-coded here).
Return the number of modules violating this.  -/
Mathlib.Linter.TextBased.modulesNotUpperCamelCase : Lean.Linter.LinterOptions → Array Lean.Name → IO ℕ
-- Mathlib.Data.Nat.Log
Nat.clog_of_one_lt : ∀ {b n : ℕ}, 1 < b → 1 < n → Nat.clog b n = Nat.clog b ((n + b - 1) / b) + 1
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- Proper group action in the sense of Bourbaki:
the map `G × X → X × X` is a proper map (see `IsProperMap`).  -/
ProperVAdd : (G : Type u_1) →
  (X : Type u_2) → [TopologicalSpace G] → [TopologicalSpace X] → [inst : AddGroup G] → [AddAction G X] → Prop
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- The groupoid of all open partial homeomorphisms on a topological space `H`.  -/
continuousGroupoid : (H : Type u_2) → [inst : TopologicalSpace H] → StructureGroupoid H
-- Init.Data.Array.MapIdx
_private.Init.Data.Array.MapIdx.0.List.mapFinIdx.go.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (as : List α)
  (motive : (x : List α) → (x_1 : Array β) → x.length + x_1.size = as.length → Sort u_3) (a : α) (as_1 : List α)
  (acc : Array β) (h : (a :: as_1).length + acc.size = as.length)
  (h_1 : (acc : Array β) → (h : [].length + acc.size = as.length) → motive [] acc h)
  (h_2 :
    (a : α) →
      (as_2 : List α) → (acc : Array β) → (h : (a :: as_2).length + acc.size = as.length) → motive (a :: as_2) acc h),
  (match a :: as_1, acc, h with
    | [], acc, h => h_1 acc h
    | a :: as_2, acc, h => h_2 a as_2 acc h) =
    h_2 a as_1 acc h
-- Mathlib.Data.Finsupp.SMul
Finsupp.comapDomain_smul : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} {R : Type u_6} [inst : Zero M] [inst_1 : SMulZeroClass R M] {f : α → β}
  (r : R) (v : β →₀ M) (hfv : Set.InjOn f (f ⁻¹' ↑v.support))
  (hfrv : optParam (Set.InjOn f (f ⁻¹' ↑(r • v).support)) ⋯),
  Finsupp.comapDomain f (r • v) hfrv = r • Finsupp.comapDomain f v hfv
-- Mathlib.Algebra.Homology.LeftResolution.Basic
/-- Given `Λ : LeftResolution ι`, the chain complex `Λ.chainComplex X`
identifies in degree `0` to `Λ.F.obj X`.  -/
CategoryTheory.Abelian.LeftResolution.chainComplexXZeroIso : {A : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_1} A] →
        {ι : CategoryTheory.Functor C A} →
          (Λ : CategoryTheory.Abelian.LeftResolution ι) →
            (X : A) →
              [inst_2 : ι.Full] →
                [inst_3 : ι.Faithful] →
                  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] →
                    [inst_5 : CategoryTheory.Abelian A] → (Λ.chainComplex X).X 0 ≅ Λ.F.obj X
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.boundariesOfIsBoundary₂_coe : ∀ {k G A : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup A] [inst_3 : Module k A]
  [inst_4 : DistribMulAction G A] [inst_5 : SMulCommClass G k A] (x : G × G →₀ A) (hx : groupHomology.IsBoundary₂ x),
  ↑(groupHomology.boundariesOfIsBoundary₂ x hx) = x
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.instMonoFKernelSequenceCycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁),
  CategoryTheory.Mono (X.kernelSequenceCycles f g n₀ n₁ hn₁).f
-- Mathlib.Data.Fin.Tuple.Reflection
/-- Rewrites `∑ i : Fin n, f i` as `f 0 + f 1 + ... + f (n - 1)` when `n` is a numeral.  -/
Fin.sum_univ_ofNat : Lean.Meta.Simp.Simproc
-- Mathlib.Order.Defs.PartialOrder
lt_of_ne_of_le : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ≠ b → a ≤ b → a < b
-- Init.Data.Vector.OfFn
Vector.ofFn_getElem : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, (Vector.ofFn fun i => xs[↑i]) = xs
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α}, a ∈ t.erase k ↔ cmp k a ≠ Ordering.eq ∧ a ∈ t
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_bot : ∀ {X : AlgebraicGeometry.Scheme}, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal ⊥ = ⊤