mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.PowerSeries.Evaluation
/-- Points at which evaluation of power series is well behaved  -/
PowerSeries.HasEval : {S : Type u_2} → [CommRing S] → [TopologicalSpace S] → S → Prop
-- Lean.Data.KVMap
Lean.KVMap.setString : Lean.KVMap → Lean.Name → String → Lean.KVMap
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat : AlgebraicGeometry.HasAffineProperty @AlgebraicGeometry.QuasiCompact fun X x x_1 x_2 => CompactSpace ↥X
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translate_apply : ∀ (x y : ℝ), ↑(CircleDeg1Lift.translate (Multiplicative.ofAdd x)) y = x + y
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.prod_eq_one_iff : ∀ {M : Type u_3} [inst : CommMonoid M] [inst_1 : PartialOrder M] [IsOrderedMonoid M] [CanonicallyOrderedMul M]
  {l : List M}, l.prod = 1 ↔ ∀ x ∈ l, x = 1
-- LeanSearchClient.Syntax
LeanSearchClient.SearchResult.docString? : LeanSearchClient.SearchResult → Option String
-- Mathlib.FieldTheory.RatFunc.Luroth
RatFunc.Luroth.algEquiv_apply : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥) (u : RatFunc K),
  ↑((RatFunc.Luroth.algEquiv h) u) =
    (Polynomial.aeval (RatFunc.Luroth.generator E)) u.num / (Polynomial.aeval (RatFunc.Luroth.generator E)) u.denom
-- Mathlib.Order.BooleanAlgebra.Set
Set.ite_mono : ∀ {α : Type u_1} (t : Set α) {s₁ s₁' s₂ s₂' : Set α}, s₁ ⊆ s₂ → s₁' ⊆ s₂' → t.ite s₁ s₁' ⊆ t.ite s₂ s₂'
-- Mathlib.Data.Multiset.UnionInter
Multiset.union_def : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), s ∪ t = s - t + t
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_eq_getD_getElem? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α}
  {fallback : β}, t.getD a fallback = t[a]?.getD fallback
-- Init.Data.List.TakeDrop
List.dropWhile_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {p : β → Bool} {l : List α},
  List.dropWhile p (List.map f l) = List.map f (List.dropWhile (p ∘ f) l)
-- Std.Data.HashMap.Basic
/-- Groups the elements of a list `xs` according to the function `key`, returning a hash map in which
each group is associated with its key. Groups preserve the relative order of elements in `xs`.

Example:
```lean example
#eval [0, 1, 2, 3, 4, 5, 6].groupByKey (· % 2)
```
```output
Std.HashMap.ofList [(0, [0, 2, 4, 6]), (1, [1, 3, 5])]
```
 -/
List.groupByKey : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (β → α) → List β → Std.HashMap α (List β)
-- Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
CategoryTheory.PreZeroHypercoverFamily.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  {property : ⦃X : C⦄ → CategoryTheory.ObjectProperty (CategoryTheory.PreZeroHypercover X)}
  {iff_shrink : ∀ {X : C} {E : CategoryTheory.PreZeroHypercover X}, property E ↔ property E.shrink}
  {property_1 : ⦃X : C⦄ → CategoryTheory.ObjectProperty (CategoryTheory.PreZeroHypercover X)}
  {iff_shrink_1 : ∀ {X : C} {E : CategoryTheory.PreZeroHypercover X}, property_1 E ↔ property_1 E.shrink},
  { property := property, iff_shrink := iff_shrink } = { property := property_1, iff_shrink := iff_shrink_1 } →
    property = property_1
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.univ_pi_Ioi_ae_eq_Ici : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NullSingletonClass (μ i)] {f : (i : ι) → α i},
  (Set.univ.pi fun i => Set.Ioi (f i)) =ᵐ[MeasureTheory.Measure.pi μ] Set.Ici f
-- Init.Control.Basic
/-- Converts the result of the monadic action `x` to a `Bool`. If it is `true`, returns it and ignores
`y`; otherwise, runs `y` and returns its result.

This is a monadic counterpart to the short-circuiting `||` operator, usually accessed via the `<||>`
operator.


Conventions for notations in identifiers:

 * The recommended spelling of `<||>` in identifiers is `orM`. -/
orM : {m : Type u → Type v} → {β : Type u} → [Monad m] → [ToBool β] → m β → m β → m β
-- Std.Do.SPred.Notation
/-- Unexpander that reconstructs `⌜...⌝` syntax from applications of `SPred.pure`.
 -/
Std.Do.SPred.Notation.unexpandPure : Lean.PrettyPrinter.Unexpander
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_mono : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] {f : F}
  {K L : Ideal S} [inst_3 : RingHomClass F R S], K ≤ L → Ideal.comap f K ≤ Ideal.comap f L
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.Consumer : Type → Type
-- Lean.Level
_private.Lean.Level.0.Lean.Level.geq.go.match_1.eq_2 : ∀ (motive : Lean.Level → Lean.Level → Sort u_1) (u v₁ v₂ : Lean.Level)
  (h_1 : (x : Lean.Level) → motive x Lean.Level.zero) (h_2 : (u v₁ v₂ : Lean.Level) → motive u (v₁.max v₂))
  (h_3 : (u₁ u₂ v : Lean.Level) → motive (u₁.max u₂) v) (h_4 : (a u₂ v : Lean.Level) → motive (a.imax u₂) v)
  (h_5 : (u v : Lean.Level) → motive u.succ v.succ) (h_6 : (x x_1 : Lean.Level) → motive x x_1),
  (match u, v₁.max v₂ with
    | x, Lean.Level.zero => h_1 x
    | u, v₁.max v₂ => h_2 u v₁ v₂
    | u₁.max u₂, v => h_3 u₁ u₂ v
    | a.imax u₂, v => h_4 a u₂ v
    | u.succ, v.succ => h_5 u v
    | x, x_1 => h_6 x x_1) =
    h_2 u v₁ v₂
-- Mathlib.Analysis.Normed.Group.Basic
dist_one_left : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a : E), dist 1 a = ‖a‖
-- Mathlib.Algebra.Order.Ring.Abs
abs_two : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsOrderedRing α], |2| = 2
-- Mathlib.Computability.Primrec.List
/-- A function from vectors to vectors is primitive recursive when all of its projections are.  -/
Nat.Primrec'.Vec : {n m : ℕ} → (List.Vector ℕ n → List.Vector ℕ m) → Prop
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_balanceR : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hlb : l.Balanced}
  {hrb : r.Balanced} {hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond r.size l.size},
  (Std.DTreeMap.Internal.Impl.balanceR k v l r hlb hrb hlr).toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel
-- Mathlib.Algebra.Polynomial.Module.Basic
/-- **Alias** of `PolynomialModule.coeff_single`. -/
PolynomialModule.single_apply : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (n : ℕ) (m : M),
  (PolynomialModule.single R n m).coeff = fun₀ | n => m
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofMkLE_comp_ofLEMk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ A₂ : C} (f : A₁ ⟶ B) [inst_1 : CategoryTheory.Mono f]
  (X : CategoryTheory.Subobject B) (g : A₂ ⟶ B) [inst_2 : CategoryTheory.Mono g]
  (h₁ : CategoryTheory.Subobject.mk f ≤ X) (h₂ : X ≤ CategoryTheory.Subobject.mk g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLE f X h₁) (X.ofLEMk g h₂) =
    CategoryTheory.Subobject.ofMkLEMk f g ⋯
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.pi_apply : ∀ {ι : Type u_7} [inst : Finite ι] {X : ι → Type u_8} {Y : ι → Type u_9} [inst_1 : (i : ι) → TopologicalSpace (X i)]
  [inst_2 : (i : ι) → TopologicalSpace (Y i)] (ei : (i : ι) → OpenPartialHomeomorph (X i) (Y i)) (a : (i : ι) → X i)
  (i : ι), ↑(OpenPartialHomeomorph.pi ei) a i = ↑(ei i) (a i)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.oneToZero_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (f : CategoryTheory.PreOneHypercover S),
  CategoryTheory.PreOneHypercover.oneToZero.obj f = f.toPreZeroHypercover
-- Mathlib.Order.Antisymmetrization
Relation.SymmGen.of_antisymmRel_of_symmGen : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α],
  AntisymmRel (fun x1 x2 => x1 ≤ x2) a b →
    Relation.SymmGen (fun x1 x2 => x1 ≤ x2) b c → Relation.SymmGen (fun x1 x2 => x1 ≤ x2) a c
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.mul_zero : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a : Lean.Grind.Ring.OfSemiring.Q α),
  Lean.Grind.Ring.OfSemiring.mul a (Lean.Grind.Ring.OfSemiring.natCast 0) = Lean.Grind.Ring.OfSemiring.natCast 0
-- Mathlib.LinearAlgebra.Dimension.Basic
LinearIndependent.aleph0_le_rank : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R]
  {ι : Type w} [Infinite ι] {v : ι → M}, LinearIndependent R v → Cardinal.aleph0 ≤ Module.rank R M
-- Mathlib.RingTheory.WittVector.Isocrystal
WittVector.IsocrystalEquiv.mk : {p : ℕ} →
  [inst : Fact (Nat.Prime p)] →
    {k : Type u_1} →
      [inst_1 : CommRing k] →
        [inst_2 : CharP k p] →
          [inst_3 : PerfectRing k p] →
            {V : Type u_2} →
              [inst_4 : AddCommGroup V] →
                [inst_5 : WittVector.Isocrystal p k V] →
                  {V₂ : Type u_3} →
                    [inst_6 : AddCommGroup V₂] →
                      [inst_7 : WittVector.Isocrystal p k V₂] →
                        (toLinearEquiv : V ≃ₗ[FractionRing (WittVector p k)] V₂) →
                          (∀ (x : V),
                              (WittVector.Isocrystal.frobenius p k) (toLinearEquiv x) =
                                toLinearEquiv ((WittVector.Isocrystal.frobenius p k) x)) →
                            WittVector.IsocrystalEquiv p k V V₂
-- Qq.Macro
Qq.Impl.floatExprAntiquot' : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadQuotation m] → ℕ → Lean.Syntax → StateT (Array (Lean.Syntax × Lean.Syntax × Lean.Syntax)) m Lean.Syntax
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffWithinAt_congr_of_mem : ∀ {𝕜 : 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 f₁ : M → M'} {s : Set M} {x : M}
  {n : WithTop ℕ∞}, (∀ y ∈ s, f₁ y = f y) → x ∈ s → (ContMDiffWithinAt I I' n f₁ s x ↔ ContMDiffWithinAt I I' n f s x)
-- Init.Data.Array.Lemmas
Array.filterMap_congr : ∀ {α : Type u_1} {β : Type u_2} {as bs : Array α},
  as = bs →
    ∀ {f g : α → Option β},
      f = g →
        ∀ {start stop start' stop' : ℕ},
          start = start' → stop = stop' → Array.filterMap f as start stop = Array.filterMap g bs start' stop'
-- Mathlib.Data.Nat.Cast.Order.Basic
Nat.not_ofNat_lt_one : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α]
  {n : ℕ} [inst_5 : n.AtLeastTwo], ¬OfNat.ofNat n < 1
-- Mathlib.Data.Complex.Basic
Complex.normSq_intCast : ∀ (z : ℤ), Complex.normSq ↑z = ↑z * ↑z
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.FG.eq_1 : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : IntermediateField F E),
  S.FG = ∃ t, IntermediateField.adjoin F ↑t = S
-- Init.Data.SInt.Lemmas
Int8.toNatClampNeg_ofBitVec : ∀ (b : BitVec 8), (Int8.ofBitVec b).toNatClampNeg = b.toInt.toNat
-- Mathlib.ModelTheory.Ultraproducts
/-- **Łoś's Theorem**: A sentence is true in an ultraproduct if and only if the set of structures
it is true in is in the ultrafilter.  -/
FirstOrder.Language.Ultraproduct.sentence_realize : ∀ {α : Type u_1} {M : α → Type u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [inst : (a : α) → L.Structure (M a)]
  [∀ (a : α), Nonempty (M a)] (φ : L.Sentence), (↑u).Product M ⊨ φ ↔ ∀ᶠ (a : α) in ↑u, M a ⊨ φ
-- Mathlib.Combinatorics.SimpleGraph.Partition
/-- Like `SimpleGraph.Partition.toColoring` but uses `Set V` as the coloring type.  -/
SimpleGraph.Partition.toColoring' : {V : Type u} → {G : SimpleGraph V} → G.Partition → G.Coloring (Set V)
-- Mathlib.Order.Sublattice
Sublattice.mem_map_of_mem : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] {L : Sublattice α} (f : LatticeHom α β) {a : α},
  a ∈ L → f a ∈ Sublattice.map f L
-- Init.Data.Range.Polymorphic.PRange
/-- The intersection operator.  -/
Std.Roo.HasRcoIntersection.intersection : {α : Type w} → [self : Std.Roo.HasRcoIntersection α] → Std.Roo α → Std.Rco α → Std.Rco α
-- Std.Data.ExtTreeSet.Basic
Std.ExtTreeSet.instLawfulSingleton : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp], LawfulSingleton α (Std.ExtTreeSet α cmp)
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff_of_eventuallyEq : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {P : (H → H') → Set H → H → Prop} {g g' : M → M'} {s : Set M} {x : M},
  G.LocalInvariantProp G' P →
    g' =ᶠ[nhdsWithin x s] g →
      g' x = g x → (ChartedSpace.LiftPropWithinAt P g' s x ↔ ChartedSpace.LiftPropWithinAt P g s x)
-- Mathlib.Data.Multiset.AddSub
Multiset.count_erase_self : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Multiset α), Multiset.count a (s.erase a) = Multiset.count a s - 1
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
/-- Constructor for pseudofunctors from a locally discrete bicategory. In that
case, we do not need to provide the `map₂` field of pseudofunctors.  -/
CategoryTheory.pseudofunctorOfIsLocallyDiscrete : {B : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Bicategory B] →
      [inst_1 : CategoryTheory.Bicategory.IsLocallyDiscrete B] →
        [inst_2 : CategoryTheory.Bicategory C] →
          (obj : B → C) →
            (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) →
              (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) →
                (mapComp :
                    {b₀ b₁ b₂ : B} →
                      (f : b₀ ⟶ b₁) →
                        (g : b₁ ⟶ b₂) →
                          map (CategoryTheory.CategoryStruct.comp f g) ≅
                            CategoryTheory.CategoryStruct.comp (map f) (map g)) →
                  autoParam
                      (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
                        CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom
                            (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h))
                              (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv)
                                  (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) =
                          CategoryTheory.eqToHom ⋯)
                      CategoryTheory.pseudofunctorOfIsLocallyDiscrete._auto_1 →
                    autoParam
                        (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁),
                          CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom
                              (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f))
                                (CategoryTheory.Bicategory.leftUnitor (map f)).hom) =
                            CategoryTheory.eqToHom ⋯)
                        CategoryTheory.pseudofunctorOfIsLocallyDiscrete._auto_3 →
                      autoParam
                          (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁),
                            CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom)
                                  (CategoryTheory.Bicategory.rightUnitor (map f)).hom) =
                              CategoryTheory.eqToHom ⋯)
                          CategoryTheory.pseudofunctorOfIsLocallyDiscrete._auto_5 →
                        CategoryTheory.Pseudofunctor B C
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsType₂.simplex_mem_nonDegenerate : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N}
  (hx : SSet.prodStdSimplex.pairingCore.IsType₂ x) {d : ℕ} (hd : x.dim = d),
  hx.simplex hd ∈
    (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := m + 1 })
          (SSet.stdSimplex.obj { len := n })).nonDegenerate
      (d + 1)
-- Init.Data.Float.Model.Float
/-- The logical model for the `Float` type.

This is defined as the type of `UInt64` with the additional restriction that bit patterns encoding
a `NaN` must be exactly a chosen canonical `NaN`.

Most functions on `Float.Model` work by unpacking the `Float.Model` into the inductive type
`UnpackedFloat`, performing the operation there, and then repacking the result into a `Float.Model`.

It is not a goal of this development to serve as the basis for a general-purpose floating-point
library or to have any direct lemmas written about it at all. Rather, users interested in a library
about floating-point numbers should develop such a library completely separately, and users
interested in proving properties of their programs involving `Float` should prove that the
operations defined here are equivalent to the operations defined in the separate library and then
transfer lemmas from the library to the `Float` and `Float32` types.
 -/
Float.Model : Type
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cocycle.fromSingleMk_mem_coboundaries_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ}
  (h : p + n = q) (q' : ℤ) (hq' : q + 1 = q') (hf : CategoryTheory.CategoryStruct.comp f (K.d q q') = 0) (q'' : ℤ),
  q'' + 1 = q →
    (CochainComplex.HomComplex.Cocycle.fromSingleMk f h q' hq' hf ∈
        CochainComplex.HomComplex.coboundaries ((CochainComplex.singleFunctor C p).obj X) K n ↔
      ∃ g, CategoryTheory.CategoryStruct.comp g (K.d q'' q) = f)
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.MatchEqns.mk : Array Lean.Name → Lean.Name → Lean.Meta.MatcherInfo → Lean.Meta.Match.MatchEqns
-- Mathlib.Data.Nat.Factorial.DoubleFactorial
_private.Mathlib.Data.Nat.Factorial.DoubleFactorial.0.Nat.doubleFactorial.match_1.eq_3 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (k : ℕ) → motive k.succ.succ),
  (match k.succ.succ with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | k.succ.succ => h_3 k) =
    h_3 k
-- Mathlib.Data.FunLike.Equiv
EquivLike.bijective : ∀ {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [inst : EquivLike E α β] (e : E), Function.Bijective ⇑e
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
/-- every singleton is a face  -/
AbstractSimplicialComplex.singleton_mem : ∀ {ι : Type u_1} (self : AbstractSimplicialComplex ι) (v : ι), {v} ∈ self.faces
-- Lean.Elab.InfoTree.Types
Lean.Elab.FVarAliasInfo.mk.inj : ∀ {userName : Lean.Name} {id baseId : Lean.FVarId} {userName_1 : Lean.Name} {id_1 baseId_1 : Lean.FVarId},
  { userName := userName, id := id, baseId := baseId } = { userName := userName_1, id := id_1, baseId := baseId_1 } →
    userName = userName_1 ∧ id = id_1 ∧ baseId = baseId_1
-- Mathlib.Algebra.Regular.Defs
isRegular_iff : ∀ {R : Type u_1} [inst : Mul R] {c : R}, IsRegular c ↔ IsLeftRegular c ∧ IsRightRegular c
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.hasCountableLimits_of_hasLimits : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasLimits C],
  CategoryTheory.Limits.HasCountableLimits C
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.SavedLocalContext.mk.sizeOf_spec : ∀ (savedLocalContext : Lean.LocalContext) (savedLocalInstances : Lean.LocalInstances)
  (savedState : Lean.Meta.SavedState),
  sizeOf
      { savedLocalContext := savedLocalContext, savedLocalInstances := savedLocalInstances, savedState := savedState } =
    1 + sizeOf savedLocalContext + sizeOf savedLocalInstances + sizeOf savedState
-- Mathlib.Order.CompleteLattice.Basic
sInf_eq_top : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α}, sInf s = ⊤ ↔ ∀ a ∈ s, a = ⊤
-- Init.Data.String.FindPos
/-- Returns the previous valid position before the given position, or panics if the position is
the start position.  -/
String.Slice.Pos.prev! : {s : String.Slice} → s.Pos → s.Pos
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.hom_ext : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂}
  (sq : F.PushoutObjObj f₁ f₂) {X₃ : C₃} {f g : sq.pt ⟶ X₃},
  CategoryTheory.CategoryStruct.comp sq.inl f = CategoryTheory.CategoryStruct.comp sq.inl g →
    CategoryTheory.CategoryStruct.comp sq.inr f = CategoryTheory.CategoryStruct.comp sq.inr g → f = g
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.preimage_obj : ∀ {X Y : SSet} (A : X.Subcomplex) (p : Y ⟶ X) (n : SimplexCategoryᵒᵖ),
  (A.preimage p).obj n = ⇑(CategoryTheory.ConcreteCategory.hom (p.app n)) ⁻¹' A.obj n
-- Mathlib.RingTheory.Nullstellensatz
MvPolynomial.instIsMaximalVanishingIdealSingletonForallSet : ∀ {K : Type u_2} [inst : Field K] {σ : Type u_3} {x : σ → K}, (MvPolynomial.vanishingIdeal K {x}).IsMaximal
-- Mathlib.Algebra.Order.Group.Abs
apply_abs_le_add_of_nonneg' : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {H : Type u_2}
  [inst_3 : AddZeroClass H] [inst_4 : LE H] [AddLeftMono H] [AddRightMono H] {f : G → H} {a : G},
  0 ≤ f a → 0 ≤ f (-a) → f |a| ≤ f a + f (-a)
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.IsBasis'.cardinalMk_eq : ∀ {α : Type u} {M : Matroid α} {I J X : Set α} [M.InvariantCardinalRank],
  M.IsBasis' I X → M.IsBasis' J X → Cardinal.mk ↑I = Cardinal.mk ↑J
-- Mathlib.RingTheory.RingHom.Flat
/-- The morphism property of flat ring maps.  -/
CommRingCat.flat : CategoryTheory.MorphismProperty CommRingCat
-- Lean.Widget.Diff
_private.Lean.Widget.Diff.0.Lean.Widget.showTacticDiff : Lean.Option Bool
-- Mathlib.Topology.ContinuousOn
continuousOn_prod_of_discrete_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [DiscreteTopology α] {f : α × β → γ} {s : Set (α × β)},
  ContinuousOn f s ↔ ∀ (a : α), ContinuousOn (fun x => f (a, x)) {b | (a, b) ∈ s}
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
_private.Mathlib.Combinatorics.Extremal.RuzsaSzemeredi.0.card_triangleIndices : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : CommRing α] {s : Finset α},
  (triangleIndices✝ s).card = Fintype.card α * s.card
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.trivial_toPreOneHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (S : C),
  (CategoryTheory.GrothendieckTopology.OneHypercover.trivial J S).toPreOneHypercover =
    CategoryTheory.PreOneHypercover.trivial S
-- Mathlib.Control.Monad.Writer
WriterT.ext : ∀ {M : Type u → Type v} {α ω : Type u} (x x' : WriterT ω M α), x.run = x'.run → x = x'