mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Finiteness
instFGFreeAddGroupOfFinite : ∀ (α : Type u_5) [Finite α], AddGroup.FG (FreeAddGroup α)
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_univ_seven : ∀ {M : Type u_2} [inst : CommMonoid M] (f : Fin 7 → M), ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6
-- Aesop.Search.Queue
Aesop.BestFirstQueue.ActiveGoal.goal : Aesop.BestFirstQueue.ActiveGoal → Aesop.GoalRef
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instAddCommMonoid : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [AddCommMonoid Y] → AddCommMonoid (LocallyConstant X Y)
-- Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Finset.prod_eq_zero_iff : ∀ {ι : Type u_1} {M₀ : Type u_4} [inst : CommMonoidWithZero M₀] {f : ι → M₀} {s : Finset ι} [Nontrivial M₀]
  [NoZeroDivisors M₀], ∏ x ∈ s, f x = 0 ↔ ∃ a ∈ s, f a = 0
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.nth_of_bisim : ∀ {F : PFunctor.{uA, uB}} (R : F.M → F.M → Prop) [inst : Inhabited F.M] [inst_1 : DecidableEq F.A],
  PFunctor.M.IsBisimulation R →
    ∀ (s₁ s₂ : F.M) (ps : PFunctor.Approx.Path F),
      R s₁ s₂ →
        PFunctor.M.IsPath ps s₁ ∨ PFunctor.M.IsPath ps s₂ →
          PFunctor.M.iselect ps s₁ = PFunctor.M.iselect ps s₂ ∧
            ∃ a f f',
              PFunctor.M.isubtree ps s₁ = PFunctor.M.mk ⟨a, f⟩ ∧
                PFunctor.M.isubtree ps s₂ = PFunctor.M.mk ⟨a, f'⟩ ∧ ∀ (i : F.B a), R (f i) (f' i)
-- Mathlib.Algebra.Category.Ring.FinitePresentation
RingHom.liftOfSurjective.congr_simp : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Ring A] [inst_1 : Ring B] [inst_2 : Ring C] (f : A →+* B)
  (hf : Function.Surjective ⇑f), f.liftOfSurjective hf = f.liftOfSurjective hf
-- Mathlib.Analysis.Calculus.Deriv.Add
HasDerivAtFilter.sum : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {L : Filter (𝕜 × 𝕜)} {ι : Type u_1} {u : Finset ι} {A : ι → 𝕜 → F} {A' : ι → F},
  (∀ i ∈ u, HasDerivAtFilter (A i) (A' i) L) → HasDerivAtFilter (∑ i ∈ u, A i) (∑ i ∈ u, A' i) L
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.coe_mul : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R) (x y : ↥s), ↑(x * y) = ↑x * ↑y
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Makes a ring homomorphism from a monoid homomorphism of rings which preserves addition.  -/
RingHom.mk' : {α : Type u_2} →
  {β : Type u_3} →
    [inst : NonAssocSemiring α] →
      [inst_1 : NonAssocRing β] → (f : α →* β) → (∀ (a b : α), f (a + b) = f a + f b) → α →+* β
-- Mathlib.Analysis.Convex.StrictConvexBetween
Isometry.affineIsometryOfStrictConvexSpace_apply : ∀ {E : Type u_3} {F : Type u_4} {PE : Type u_5} {PF : Type u_6} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ E] [inst_3 : NormedSpace ℝ F] [inst_4 : StrictConvexSpace ℝ E]
  [inst_5 : MetricSpace PE] [inst_6 : MetricSpace PF] [inst_7 : NormedAddTorsor E PE] [inst_8 : NormedAddTorsor F PF]
  {f : PF → PE} (hi : Isometry f) (p : PF), hi.affineIsometryOfStrictConvexSpace p = f p
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.instCoeSortType : {X : Type u_2} → [inst : TopologicalSpace X] → CoeSort (DiscreteQuotient X) (Type u_2)
-- Init.Control.ExceptCps
ExceptCpsT.instMonad : {ε : Type u_1} → {m : Type u_1 → Type u_2} → Monad (ExceptCpsT ε m)
-- Mathlib.FieldTheory.IntermediateField.Algebraic
IntermediateField.coe_isIntegral_iff : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {S : IntermediateField K L}
  {R : Type u_3} [inst_3 : CommRing R] [inst_4 : Algebra R K] [inst_5 : Algebra R L] [inst_6 : IsScalarTower R K L]
  {x : ↥S}, IsIntegral R ↑x ↔ IsIntegral R x
-- Mathlib.Algebra.Ring.Subring.Basic
/-- A ring isomorphism `e : R ≃+* S` descends to subrings `s' ≃+* s` provided
`x ∈ s' ↔ e x ∈ s`.  -/
RingEquiv.restrict : {R : Type u} →
  {S : Type v} →
    [inst : NonAssocSemiring R] →
      [inst_1 : NonAssocSemiring S] →
        {σR : Type u_1} →
          {σS : Type u_2} →
            [inst_2 : SetLike σR R] →
              [inst_3 : SetLike σS S] →
                [inst_4 : SubsemiringClass σR R] →
                  [inst_5 : SubsemiringClass σS S] →
                    (e : R ≃+* S) → (s' : σR) → (s : σS) → (∀ (x : R), x ∈ s' ↔ e x ∈ s) → ↥s' ≃+* ↥s
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.exchange_isBase_of_indep' : ∀ {α : Type u_1} {M : Matroid α} {B : Set α} {e f : α},
  M.IsBase B → e ∈ B → f ∉ B → M.Indep (insert f B \ {e}) → M.IsBase (insert f B \ {e})
-- Init.Data.Array.InsertIdx
Array.getElem?_insertIdx : ∀ {α : Type u} {xs : Array α} {x : α} {i k : ℕ} (h : i ≤ xs.size),
  (xs.insertIdx i x h)[k]? =
    if k < i then xs[k]? else if k = i then if k ≤ xs.size then some x else none else xs[k - 1]?
-- Mathlib.RingTheory.LocalRing.Module
/-- If `M` is a finitely presented module over a local ring `(R, 𝔪)` such that `m ⊗ M → M` is
injective, then every generating family contains a basis.
 -/
Module.exists_basis_of_span_of_maximalIdeal_rTensor_injective : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsLocalRing R] [Module.FinitePresentation R M],
  Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype (IsLocalRing.maximalIdeal R))) →
    ∀ {ι : Type u} (v : ι → M), Submodule.span R (Set.range v) = ⊤ → ∃ κ a b, ∀ (i : κ), b i = v (a i)
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
LeftPreLieAlgebra.toIsScalarTower : ∀ {R : Type u_1} {inst : CommRing R} {L : Type u_2} {inst_1 : LeftPreLieRing L} [self : LeftPreLieAlgebra R L],
  IsScalarTower R L L
-- Mathlib.Computability.Reduce
_private.Mathlib.Computability.Reduce.0.ManyOneDegree.le_trans : ∀ {d₁ d₂ d₃ : ManyOneDegree}, d₁ ≤ d₂ → d₂ ≤ d₃ → d₁ ≤ d₃
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.le_def : ∀ {E : Type u_3} [inst : AddGroup E] {p q : NonarchAddGroupSeminorm E}, p ≤ q ↔ ⇑p ≤ ⇑q
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.comap_mk_nhds : ∀ {M : Type u_1} [inst : TopologicalSpace M] (x : Mᵈᵐᵃ),
  Filter.comap (⇑DomMulAct.mk) (nhds x) = nhds (DomMulAct.mk.symm x)
-- Init.Data.Array.Erase
_private.Init.Data.Array.Erase.0.Array.eraseP_filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (y : β) (h_1 : (y : β) → motive (some y)) (h_2 : Unit → motive none),
  (match some y with
    | some y => h_1 y
    | none => h_2 ()) =
    h_1 y
-- Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
mem_adjoin_of_dvd_coeff_of_dvd_aeval : ∀ {A : Type u_1} {B : Type u_2} [inst : CommSemiring A] [inst_1 : Ring B] [inst_2 : Algebra A B] [IsDomain A]
  [Module.IsTorsionFree A B] {Q : Polynomial A} {p : A} {x z : B},
  p ≠ 0 → (∀ i ∈ Finset.range (Q.natDegree + 1), p ∣ Q.coeff i) → (Polynomial.aeval x) Q = p • z → z ∈ A[x]
-- Mathlib.CategoryTheory.Yoneda
/-- The morphism `X ⟶ Y` corresponding to a natural transformation
`coyoneda.obj X ⟶ coyoneda.obj Y`.  -/
CategoryTheory.Coyoneda.preimage : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : Cᵒᵖ} → (CategoryTheory.coyoneda.obj X ⟶ CategoryTheory.coyoneda.obj Y) → (X ⟶ Y)
-- Lean.HeadIndex
/-- Convert the given expression into a `HeadIndex`.
 -/
Lean.Expr.toHeadIndex : Lean.Expr → Lean.HeadIndex
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.ranCompIsoOfPreserves_inv_app : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (L : CategoryTheory.Functor A C)
  [inst_4 : G.PreservesRightKanExtensions L] [inst_5 : ∀ (F : CategoryTheory.Functor A B), L.HasRightKanExtension F]
  [inst_6 : ∀ (F : CategoryTheory.Functor A D), L.HasRightKanExtension F] (X : CategoryTheory.Functor A B),
  (G.ranCompIsoOfPreserves L).inv.app X = (G.rightKanExtensionCompIsoOfPreserves X L).inv
-- Mathlib.MeasureTheory.Measure.OpenPos
/-- If two functions are a.e. equal on an open set and are continuous on this set, then they are
equal on this set.  -/
MeasureTheory.Measure.eqOn_open_of_ae_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {m : MeasurableSpace X} [inst_1 : TopologicalSpace Y]
  [T2Space Y] {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] {U : Set X} {f g : X → Y},
  f =ᵐ[μ.restrict U] g → IsOpen U → ContinuousOn f U → ContinuousOn g U → Set.EqOn f g U
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α} {fallback : β},
  (List.map Prod.fst l).contains k = false →
    Std.DTreeMap.Raw.Const.getD (Std.DTreeMap.Raw.Const.ofList l cmp) k fallback = fallback
-- Mathlib.CategoryTheory.Join.Basic
_private.Mathlib.CategoryTheory.Join.Basic.0.CategoryTheory.Join.id.match_1.eq_1 : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D] (motive : CategoryTheory.Join C D → Sort u_5) (x : C)
  (h_1 : (x : C) → motive (CategoryTheory.Join.left x)) (h_2 : (x : D) → motive (CategoryTheory.Join.right x)),
  (match CategoryTheory.Join.left x with
    | CategoryTheory.Join.left x => h_1 x
    | CategoryTheory.Join.right x => h_2 x) =
    h_1 x
-- Mathlib.CategoryTheory.Filtered.Small
/-- Implementation detail for the instance
`EssentiallySmall.{max v w} (FullSubcategory (cofilteredClosure f))`.  -/
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] →
      {α : Type w} → (f : α → C) → CategoryTheory.IsCofiltered.CofilteredClosureSmall.AbstractCofilteredClosure✝ f → C
-- Init.Data.Vector.Lemmas
Vector.map_pop : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n}, Vector.map f xs.pop = (Vector.map f xs).pop
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
/-- Functoriality of `PiLocalization` but restricted to bijective ring homs.
If R and S are commutative rings, surjectivity would be enough.  -/
MaximalSpectrum.mapPiLocalization : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        (f : R →+* S) → Function.Bijective ⇑f → MaximalSpectrum.PiLocalization R →+* MaximalSpectrum.PiLocalization S
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsRestriction.isLoop_iff : ∀ {α : Type u_1} {M N : Matroid α} {e : α}, N.IsRestriction M → (N.IsLoop e ↔ e ∈ N.E ∧ M.IsLoop e)
-- Mathlib.CategoryTheory.ShrinkYoneda
/-- The functor `shrinkYoneda.{w}` followed by the evaluation
at `Y : Cᵒᵖ` and `uliftFunctor.{v}` identifies to `coyoneda.obj Y` followed
by `uliftFunctor.{w}`.  -/
CategoryTheory.shrinkYonedaCompEvaluationCompUliftFunctorIsoUliftFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
      (Y : Cᵒᵖ) →
        CategoryTheory.shrinkYoneda.{w, v, u}.comp
            (((CategoryTheory.evaluation Cᵒᵖ (Type w)).obj Y).comp CategoryTheory.uliftFunctor.{v, w}) ≅
          (CategoryTheory.coyoneda.obj Y).comp CategoryTheory.uliftFunctor.{w, v}
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.Skeleton.instFullIncl : FintypeCat.Skeleton.incl.Full
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- When `C` and `D` have chosen finite products and `F : C ⥤ D` is any functor,
`prodComparison F A B` is the canonical comparison morphism from `F (A ⊗ B)` to `F(A) ⊗ F(B)`.  -/
CategoryTheory.CartesianMonoidalCategory.prodComparison : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₁} →
        [inst_2 : CategoryTheory.Category.{v₁, u₁} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              (A B : C) →
                F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj A B) ⟶
                  CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj A) (F.obj B)
-- Mathlib.Data.List.Triplewise
List.triplewise_reverse : ∀ {α : Type u_1} {l : List α} {p : α → α → α → Prop},
  List.Triplewise p l.reverse ↔ List.Triplewise (fun a b c => p c b a) l
-- Mathlib.Data.Finset.Card
/-- Analogue of `strongInduction` with order of arguments swapped.  -/
Finset.strongInductionOn : {α : Type u_1} →
  {p : Finset α → Sort u_4} → (s : Finset α) → ((s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s) → p s
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
max_add_min : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : AddCommSemigroup α] (a b : α), max a b + min a b = a + b
-- Mathlib.Analysis.Normed.Ring.InfiniteSum
summable_sum_mul_antidiagonal_of_summable_norm' : ∀ {R : Type u_1} [inst : NormedRing R] {f g : ℕ → R},
  (Summable fun x => ‖f x‖) →
    Summable f →
      (Summable fun x => ‖g x‖) →
        Summable g → Summable fun n => ∑ kl ∈ Finset.HasAntidiagonal.antidiagonal n, f kl.1 * g kl.2
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.Batteries.AssocList.find?.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Lean.Parser.Do
Lean.Parser.Term.doLet : Lean.Parser.Parser
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.singleton_injective : ∀ {α : Type u_1} [inst : TopologicalSpace α], Function.Injective fun x => {x}
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_union!_of_contains_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (h : Std.DTreeMap.Internal.Impl.contains k m₂ = true),
  Std.DTreeMap.Internal.Impl.Const.get (m₁.union! m₂) k ⋯ = Std.DTreeMap.Internal.Impl.Const.get m₂ k h
-- Batteries.Util.ProofWanted
/-- Wrapper recording that a `proof_wanted` of statement `α` has been declared.  -/
ProofWanted : Sort u → Type
-- Lean.Data.Options
Lean.MonadWithOptions.withOptions : {m : Type → Type} → [self : Lean.MonadWithOptions m] → {α : Type} → (Lean.Options → Lean.Options) → m α → m α
-- Init.Data.UInt.Lemmas
UInt32.add_neg_eq_sub : ∀ {a b : UInt32}, a + -b = a - b
-- Init.Data.UInt.Bitwise
UInt8.not_xor : ∀ {a b : UInt8}, ~~~a ^^^ b = ~~~(a ^^^ b)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.WalkingParallelFamily.hom_id : ∀ {J : Type w} (X : CategoryTheory.Limits.WalkingParallelFamily J),
  CategoryTheory.Limits.WalkingParallelFamily.Hom.id X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Topology.Algebra.UniformConvergence
/-- Let `𝔖 : Set (Set α)`. If `G` is a uniform group, then `α →ᵤ[𝔖] G` is a uniform group as
well.  -/
instIsUniformGroupUniformOnFun : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] {𝔖 : Set (Set α)} [inst_1 : UniformSpace G] [IsUniformGroup G],
  IsUniformGroup (UniformOnFun α G 𝔖)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.algebraMap_leftInverse : ∀ {R : Type u1} [inst : CommRing R] (M : Type u2) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Function.LeftInverse ⇑ExteriorAlgebra.algebraMapInv ⇑(algebraMap R (ExteriorAlgebra R M))
-- Mathlib.Order.Preorder.Finite
OrderEmbedding.range_eq_iff : ∀ {α : Type u_4} {β : Type u_5} [inst : LinearOrder α] [inst_1 : PartialOrder β] [Finite α] {f g : α ↪o β},
  Set.range ⇑f = Set.range ⇑g ↔ f = g
-- Mathlib.Tactic.Lift
Subtype.canLift : ∀ {α : Sort u_1} (p : α → Prop), CanLift α { x // p x } Subtype.val p
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.IsHermitian.sort_roots_charpoly_eq_eigenvalues₀ : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian),
  ((Multiset.map (⇑RCLike.re) A.charpoly.roots).sort fun x1 x2 => x1 ≥ x2) = List.ofFn hA.eigenvalues₀
-- Init.Data.Nat.Internal.SOM
_private.Init.Data.Nat.Internal.SOM.0.Nat.Internal.SOM.Poly.mulMon.eq_1 : ∀ (p : Nat.Internal.SOM.Poly) (k : ℕ) (m : Nat.Internal.SOM.Mon),
  p.mulMon k m = Nat.Internal.SOM.Poly.mulMon.go✝ k m p []
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousLinearMap.uncurryLeft_norm : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : Ei 0 →L[𝕜] Ei i.succ [×n]→L[𝕜] G),
  ‖f.uncurryLeft‖ = ‖f‖
-- Std.Async.System
/-- The numeric user ID.
 -/
Std.Async.System.UserId.toNat : Std.Async.System.UserId → ℕ
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.exactAt_single_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C) (i : ι), i ≠ j → ((HomologicalComplex.single C c j).obj A).ExactAt i
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.sdiff_adj : ∀ {V : Type u} (x y : SimpleGraph V) (v w : V), (x \ y).Adj v w ↔ x.Adj v w ∧ ¬y.Adj v w
-- Mathlib.Topology.MetricSpace.Equicontinuity
/-- Characterization of uniform equicontinuity for families of functions between
(pseudo) metric spaces.  -/
Metric.uniformEquicontinuous_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] {ι : Type u_4} [inst_1 : PseudoMetricSpace β]
  {F : ι → β → α},
  UniformEquicontinuous F ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε
-- Mathlib.Algebra.BigOperators.Group.List.Basic
Commute.list_prod_left : ∀ {M : Type u_4} [inst : Monoid M] (l : List M) (y : M), (∀ x ∈ l, Commute x y) → Commute l.prod y
-- Mathlib.Tactic.Simps.Basic
/-- Make generated lemmas simp lemmas  -/
Simps.Config.isSimp : Simps.Config → Bool
-- Mathlib.GroupTheory.Torsion
IsAddTorsion.torsionAddEquiv.eq_1 : ∀ {G : Type u_1} [inst : AddCommMonoid G] (tG : IsAddTorsion G),
  tG.torsionAddEquiv = (AddEquiv.addSubmonoidCongr ⋯).trans AddSubmonoid.topEquiv
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.multispanIndexCoend_right : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) (j : (CategoryTheory.Limits.multispanShapeCoend J).R),
  (CategoryTheory.Limits.multispanIndexCoend F).right j = (F.obj (Opposite.op j)).obj j
-- Init.Data.List.Pairwise
List.rel_of_pairwise_cons : ∀ {α : Type u_1} {a : α} {l : List α} {R : α → α → Prop}, List.Pairwise R (a :: l) → ∀ {a' : α}, a' ∈ l → R a a'
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.copy.congr_simp : ∀ {V : Type u} {G : SimpleGraph V} {u v u' v' : V} (p p_1 : G.Walk u v),
  p = p_1 → ∀ (hu : u = u') (hv : v = v'), p.copy hu hv = p_1.copy hu hv
-- Mathlib.Analysis.Normed.Group.Continuity
NormedAddGroup.toENormedAddMonoid.eq_1 : ∀ {F : Type u_7} [inst : NormedAddGroup F],
  NormedAddGroup.toENormedAddMonoid =
    { toContinuousENorm := SeminormedAddGroup.toContinuousENorm, toAddMonoid := inst.toAddMonoid, enorm_zero := ⋯,
      enorm_add_le := ⋯, enorm_eq_zero := ⋯ }
-- Std.Time.Duration
Std.Time.Duration.instHAddOffset : HAdd Std.Time.Duration Std.Time.Day.Offset Std.Time.Duration
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.minDegree.eq_1 : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj],
  G.minDegree = WithTop.untopD 0 (Finset.image (fun v => G.degree v) Finset.univ).min
-- Mathlib.Topology.EMetricSpace.Lipschitz
LocallyLipschitz.prodMk_right : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (b : β),
  LocallyLipschitz fun a => (a, b)
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
/-- Coerce continuous linear equivs to continuous linear maps.  -/
ContinuousAffineEquiv.ContinuousAffineMap.coe : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {V₁ : Type u_6} →
        {V₂ : Type u_7} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : Module k V₁] →
                [inst_3 : AddTorsor V₁ P₁] →
                  [inst_4 : TopologicalSpace P₁] →
                    [inst_5 : AddCommGroup V₂] →
                      [inst_6 : Module k V₂] →
                        [inst_7 : AddTorsor V₂ P₂] → [inst_8 : TopologicalSpace P₂] → Coe (P₁ ≃ᴬ[k] P₂) (P₁ →ᴬ[k] P₂)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.addEquivOfLocalizations.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) (k : S.LocalizationMap P),
  f.addEquivOfLocalizations k =
    { toFun := ⇑(f.lift ⋯), invFun := ⇑(k.lift ⋯), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Ring.BooleanRing
Bool.one_eq_true : 1 = true
-- Mathlib.Topology.ClusterPt
ContinuousAt.mapClusterPt : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} [inst_1 : TopologicalSpace α]
  {a : α}, ContinuousAt u a → ClusterPt a F → MapClusterPt (u a) F u
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {l : List ((a : α) × β a)} {k : α}
  [inst_1 : Inhabited (β k)], (List.map Sigma.fst l).contains k = false → (Std.DHashMap.ofList l).get! k = default
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.comp_factorThruImage_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  {f : X ⟶ Y} {g : Y ⟶ Z} [inst_2 : CategoryTheory.Limits.HasImage g],
  CategoryTheory.CategoryStruct.comp f g = 0 →
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.factorThruImage g) = 0
-- Mathlib.Data.QPF.Univariate.Basic
QPF.has_good_supp_iff : ∀ {F : Type u → Type u} [q : QPF F] {α : Type u} (x : F α),
  (∀ (p : α → Prop), Functor.Liftp p x ↔ ∀ u ∈ Functor.supp x, p u) ↔
    ∃ a f,
      QPF.abs ⟨a, f⟩ = x ∧
        ∀ (a' : (QPF.P F).A) (f' : (QPF.P F).B a' → α), QPF.abs ⟨a', f'⟩ = x → f '' Set.univ ⊆ f' '' Set.univ
-- Std.Data.DTreeMap.Slice
Std.DTreeMap.instSliceableRciSlice : {α : Type u} →
  {β : α → Type v} →
    (cmp : autoParam (α → α → Ordering) Std.DTreeMap.instSliceableRciSlice._auto_1) →
      Std.Rci.Sliceable (Std.DTreeMap α β cmp) α (Std.DTreeMap.Internal.RciSlice α β)
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.typeMatchesBaseName : Lean.Expr → Lean.Name → Lean.MetaM Bool
-- Mathlib.Geometry.Manifold.Instances.Real
instTopologicalSpaceEuclideanQuadrant : (n : ℕ) → TopologicalSpace (EuclideanQuadrant n)
-- Lean.Elab.Tactic.Conv.Basic
/-- Evaluate `sepByIndent conv "; "  -/
Lean.Elab.Tactic.Conv.evalSepByIndentConv : Lean.Syntax → Lean.Elab.Tactic.TacticM Unit
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.symm : ∀ {α : Type u} {β : α → Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β}, t₁.Equiv t₂ → t₂.Equiv t₁
-- Mathlib.Probability.Kernel.Proper
ProbabilityTheory.Kernel.IsProper.mk : ∀ {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : ProbabilityTheory.Kernel X X},
  (∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), (π.restrict ⋯) x = B.indicator (fun x => 1) x • π x) → π.IsProper
-- Mathlib.Analysis.SpecificLimits.Normed
/-- A geometric series in a normed field is summable iff the norm of the common ratio is less than
one.  -/
summable_geometric_iff_norm_lt_one : ∀ {K : Type u_4} [inst : NormedDivisionRing K] {ξ : K}, (Summable fun n => ξ ^ n) ↔ ‖ξ‖ < 1
-- Init.Data.List.Erase
List.eraseP_append_right : ∀ {α : Type u_1} {p : α → Bool} {l₁ : List α} (l₂ : List α),
  (∀ b ∈ l₁, ¬p b = true) → List.eraseP p (l₁ ++ l₂) = l₁ ++ List.eraseP p l₂