mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.cmpLT.trans_l : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α},
  RBTree.RBNode.cmpLT cmp x y →
    ∀ {t : RBTree.RBNode α},
      RBTree.RBNode.All (fun x => RBTree.RBNode.cmpLT cmp y x) t →
        RBTree.RBNode.All (fun x_1 => RBTree.RBNode.cmpLT cmp x x_1) t
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.all_takeWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice}, (s.takeWhile pat).all pat = true
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorCompIsoId_add'_inv_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
  [inst_2 : CategoryTheory.HasShift C A] {X : C} (m n p m' n' p' : A) (hm : m' + m = 0) (hn : n' + n = 0)
  (hp : p' + p = 0) (h : m + n = p),
  (CategoryTheory.shiftFunctorCompIsoId C p' p hp).inv.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C n' n hn).inv.app X)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor C n).map
          ((CategoryTheory.shiftFunctorCompIsoId C m' m hm).inv.app ((CategoryTheory.shiftFunctor C n').obj X)))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctorAdd' C m n p h).inv.app
            ((CategoryTheory.shiftFunctor C m').obj ((CategoryTheory.shiftFunctor C n').obj X)))
          ((CategoryTheory.shiftFunctor C p).map ((CategoryTheory.shiftFunctorAdd' C n' m' p' ⋯).inv.app X))))
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.glue!.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) (sz' : ℕ) (k' : α) (v' : β k')
  (l'' r'' : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (r : Std.DTreeMap.Internal.Impl α β) →
      (sz' : ℕ) →
        (k' : α) →
          (v' : β k') →
            (l'' r'' : Std.DTreeMap.Internal.Impl α β) →
              r = Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'' →
                motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'')),
  (match Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'' with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | r@h:(Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'') => h_2 r sz' k' v' l'' r'' h) =
    h_2 (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'') sz' k' v' l'' r'' ⋯
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.mul_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f g : Module.End R M) (x : M), (f * g) x = f (g x)
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.delab : Lean.PrettyPrinter.Delaborator.Delab
-- Lean.Data.PrefixTree
Lean.PrefixTreeNode.brecOn_1.go : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {motive_1 : Lean.PrefixTreeNode α β cmp → Sort u_1} →
        {motive_2 : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp → Sort u_1} →
          {motive_3 : Std.DTreeMap.Raw α (fun x => Lean.PrefixTreeNode α β cmp) cmp → Sort u_1} →
            {motive_4 : (Std.DTreeMap.Internal.Impl α fun x => Lean.PrefixTreeNode α β cmp) → Sort u_1} →
              (t : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp) →
                ((t : Lean.PrefixTreeNode α β cmp) → t.below → motive_1 t) →
                  ((t : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp) →
                      Lean.PrefixTreeNode.below_1 t → motive_2 t) →
                    ((t : Std.DTreeMap.Raw α (fun x => Lean.PrefixTreeNode α β cmp) cmp) →
                        Lean.PrefixTreeNode.below_2 t → motive_3 t) →
                      ((t : Std.DTreeMap.Internal.Impl α fun x => Lean.PrefixTreeNode α β cmp) →
                          Lean.PrefixTreeNode.below_3 t → motive_4 t) →
                        motive_2 t ×' Lean.PrefixTreeNode.below_1 t
-- Mathlib.Algebra.Group.Hom.Instances
/-- `OneHom M N` is a `Monoid` if `N` is.  -/
OneHom.instMonoid : {M : Type uM} → {N : Type uN} → [inst : One M] → [inst_1 : Monoid N] → Monoid (OneHom M N)
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.coords_apply : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) (q : P) (i : ι), b.coords q i = (b.coord i) q
-- Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
/-- If a locally integrable function `f` on a finite-dimensional real manifold has zero integral
when multiplied by any smooth compactly supported function, then `f` vanishes almost everywhere.  -/
ae_eq_zero_of_integral_contMDiff_smul_eq_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2}
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [CompleteSpace F] {H : Type u_3}
  [inst_6 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_4} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [IsManifold I (↑⊤) M] [inst_10 : MeasurableSpace M] [BorelSpace M] [T2Space M] {f : M → F}
  {μ : MeasureTheory.Measure M} [SigmaCompactSpace M],
  MeasureTheory.LocallyIntegrable f μ →
    (∀ (g : M → ℝ), ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0) →
      ∀ᵐ (x : M) ∂μ, f x = 0
-- Mathlib.CategoryTheory.DinatTrans
CategoryTheory.DinatTrans.compNatTrans_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C D)} (δ : CategoryTheory.DinatTrans F G) (α : G ⟶ H)
  (X : C), (δ.compNatTrans α).app X = CategoryTheory.CategoryStruct.comp (δ.app X) ((α.app (Opposite.op X)).app X)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- The product comparison morphism from `F(- ⊗ -)` to `F- ⊗ F-`, whose components are given by
`prodComparison`.  -/
CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans : {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) →
              (CategoryTheory.MonoidalCategory.curriedTensor C).comp
                  ((CategoryTheory.Functor.whiskeringRight C C D).obj F) ⟶
                F.comp
                  ((CategoryTheory.MonoidalCategory.curriedTensor D).comp
                    ((CategoryTheory.Functor.whiskeringLeft C D D).obj F))
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.norm_le_natCast_iff_of_nonneg : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] (a : A) (n : ℕ),
  autoParam (0 ≤ a) CStarAlgebra.norm_le_natCast_iff_of_nonneg._auto_1 → (‖a‖ ≤ ↑n ↔ a ≤ ↑n)
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Polynomial.Monic.leadingCoeff_notMem : ∀ {R : Type u} [inst : CommSemiring R] {𝓟 : Ideal R} {f : Polynomial R}, f.Monic → 𝓟 ≠ ⊤ → f.leadingCoeff ∉ 𝓟
-- Mathlib.Algebra.Algebra.TransferInstance
/-- An equivalence `e : α ≃ β` gives an algebra equivalence `α ≃ₐ[R] β`
where the `R`-algebra structure on `α` is
the one obtained by transporting an `R`-algebra structure on `β` back along `e`.  -/
Equiv.algEquiv : (R : Type u_1) →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : CommSemiring R] →
        (e : α ≃ β) →
          [inst_1 : Semiring β] →
            [inst_2 : Algebra R β] →
              let semiring := e.semiring;
              have algebra := Equiv.algebra R e;
              α ≃ₐ[R] β
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Cofork.op.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Cofork f g),
  c.op =
    (CategoryTheory.Limits.Cone.postcompose (CategoryTheory.Limits.parallelPairOpIso f g).symm.hom).obj
      (CategoryTheory.Limits.Cone.whisker CategoryTheory.Limits.walkingParallelPairOpEquiv.functor
        (CategoryTheory.Limits.Cocone.op c))
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.tr.match_1.eq_5 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (q : Turing.PartrecToTM2.Λ')
  (h_1 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k₁ k₂ : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (k : Turing.PartrecToTM2.K') →
      (f : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
        (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.push k f q))
  (h_3 : (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (q : Turing.PartrecToTM2.Λ') → motive q.copy) (h_6 : (q : Turing.PartrecToTM2.Λ') → motive q.succ)
  (h_7 : (q₁ q₂ : Turing.PartrecToTM2.Λ') → motive (q₁.pred q₂))
  (h_8 :
    (fs : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k)))
  (h_9 : (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret k.cons₂))
  (h_10 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k)))
  (h_11 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k)))
  (h_12 : Unit → motive (Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt)),
  (match q.copy with
    | Turing.PartrecToTM2.Λ'.move p k₁ k₂ q => h_1 p k₁ k₂ q
    | Turing.PartrecToTM2.Λ'.push k f q => h_2 k f q
    | Turing.PartrecToTM2.Λ'.read q => h_3 q
    | Turing.PartrecToTM2.Λ'.clear p k q => h_4 p k q
    | q.copy => h_5 q
    | q.succ => h_6 q
    | q₁.pred q₂ => h_7 q₁ q₂
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k) => h_8 fs k
    | Turing.PartrecToTM2.Λ'.ret k.cons₂ => h_9 k
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k) => h_10 f k
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k) => h_11 f k
    | Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt => h_12 ()) =
    h_5 q
-- Lean.LoadDynlib
_private.Lean.LoadDynlib.0.Lean.loadPlugin.unsafe_impl_8 : (dynlib : Lean.Dynlib) → dynlib.Symbol → IO Unit
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given Localization maps `f : M →* N, k : P →* Q` for Submonoids `S, T` respectively, if a
`CommMonoid` homomorphism `g : M →* P` induces a `f.map hy k : N →* Q`, then for all `z : N`,
we have `k (g y) * f.map hy k z = k (g x)` where `x : M, y ∈ S` are such that
`z * f y = f x`.  -/
Submonoid.LocalizationMap.map_mul_left : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
  {Q : Type u_4} [inst_3 : CommMonoid Q] {k : T.LocalizationMap Q} (z : N),
  k (g ↑(f.sec z).2) * (f.map hy k) z = k (g (f.sec z).1)
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Quiver.FreeGroupoid.of_eq : ∀ {V : Type u} [inst : Quiver V],
  Quiver.FreeGroupoid.of V =
    Quiver.Symmetrify.of ⋙q CategoryTheory.Paths.of (Quiver.Symmetrify V) ⋙q
      (CategoryTheory.Quotient.functor Quiver.FreeGroupoid.redStep).toPrefunctor
-- Mathlib.Data.List.Rotate
List.isRotated_concat : ∀ {α : Type u} (hd : α) (tl : List α), tl ++ [hd] ~r hd :: tl
-- Mathlib.Algebra.Lie.TraceForm
LieSubmodule.traceForm_eq_of_le_idealizer : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [Module.Free R M] [Module.Finite R M] [IsDomain R] [IsPrincipalIdealRing R] (N : LieSubmodule R L M),
  ∀ I ≤ N.idealizer,
    LieModule.traceForm R ↥I ↥N = (LieModule.traceForm R L M).restrict (LieIdeal.toLieSubalgebra R L I).toSubmodule
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.diff!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t₁ t₂ : Std.DTreeMap.Internal.Impl α β),
  t₁.diff! t₂ =
    if t₁.size ≤ t₂.size then
      Std.DTreeMap.Internal.Impl.filter! (fun p x => !Std.DTreeMap.Internal.Impl.contains p t₂) t₁
    else ↑(t₁.eraseManyEntries! t₂)
-- Mathlib.CategoryTheory.Core
CategoryTheory.Core.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : CategoryTheory.Core C} {f g : X ⟶ Y},
  f = g ↔ f.iso.hom = g.iso.hom
-- Mathlib.CategoryTheory.Preadditive.Projective.Preserves
CategoryTheory.Functor.PreservesProjectiveObjects.projective_obj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : F.PreservesProjectiveObjects] {X : C},
  CategoryTheory.Projective X → CategoryTheory.Projective (F.obj X)
-- Mathlib.CategoryTheory.EssentialImage
/-- Extract the isomorphism between `F.obj h.witness` and `Y` itself.  -/
CategoryTheory.Functor.essImage.getIso : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} → {Y : D} → (h : F.essImage Y) → F.obj h.witness ≅ Y
-- Init.Data.Fin.Lemmas
Fin.is_lt : ∀ {n : ℕ} (a : Fin n), ↑a < n
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.SeparatingLeft.congr_simp : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : NonUnitalNonAssocSemiring R] [inst_1 : Finite m]
  [inst_2 : Finite n] (M M_1 : Matrix m n R), M = M_1 → M.SeparatingLeft = M_1.SeparatingLeft
-- Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
/-- If `Y ⟶ S` is surjective on stalks, then for every `X ⟶ S`, `X ×ₛ Y` is a subset of
`X × Y` (Cartesian product as topological spaces) with the induced topology.  -/
AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullback : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.SurjectiveOnStalks g],
  Topology.IsEmbedding fun x => ((CategoryTheory.Limits.pullback.fst f g) x, (CategoryTheory.Limits.pullback.snd f g) x)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.isPrime : ∀ {R : Type u_1} [inst : CommRing R] (self : IsDedekindDomain.HeightOneSpectrum R), self.asIdeal.IsPrime
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.mem_vadd_set : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {t : Set β} {a : α} {x : β}, x ∈ a +ᵥ t ↔ ∃ y ∈ t, a +ᵥ y = x
-- Init.Data.String.Lemmas.Pattern.Basic
/-- Inductive predicate stating that a list of search steps represents a valid backwards search from a
given position in a slice.

"Searching" here means always taking the longest match at the first position where the pattern
matches.

Hence, this predicate determines the list of search steps up to grouping of rejections.
 -/
String.Slice.Pattern.Model.IsValidRevSearchFrom : {ρ : Type} →
  (pat : ρ) →
    [String.Slice.Pattern.Model.PatternModel pat] →
      {s : String.Slice} → s.Pos → List (String.Slice.Pattern.SearchStep s) → Prop
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- **Alias** of `Set.mem_finsetProd`.

---

The n-ary version of `Set.mem_mul`.  -/
Set.mem_finset_prod : ∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] (t : Finset ι) (f : ι → Set α) (a : α),
  a ∈ ∏ i ∈ t, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ t → g i ∈ f i), ∏ i ∈ t, g i = a
-- Mathlib.Algebra.Algebra.Defs
/-- This is just a special case of the global `smul_mul_assoc` lemma that requires less typeclass
search (and was here first).  -/
Algebra.smul_mul_assoc : ∀ {R : Type u} {A : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R) (x y : A),
  r • x * y = r • (x * y)
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.isIso_factorThruImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q)
  [CategoryTheory.Mono f], CategoryTheory.IsIso (CategoryTheory.Abelian.factorThruImage f)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.ne_bot_iff_nonempty_verts : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph), G' ≠ ⊥ ↔ G'.verts.Nonempty
-- Init.Data.List.Lemmas
List.forall_none_of_filterMap_eq_nil : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {xs : List α}, List.filterMap f xs = [] → ∀ x ∈ xs, f x = none
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
/-- The number of connected components in `G` is the dimension of the nullspace of its Laplacian.  -/
SimpleGraph.card_connectedComponent_eq_finrank_ker_toLin'_lapMatrix : ∀ {V : Type u_1} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj] [inst_2 : DecidableEq V],
  Fintype.card G.ConnectedComponent = Module.finrank ℝ ↥(Matrix.toLin' (SimpleGraph.lapMatrix ℝ G)).ker
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
Mathlib.Tactic.Linarith.SimplexAlgorithm.SparseMatrix.mk.inj : ∀ {n m : ℕ} {data data_1 : Array (Std.HashMap ℕ ℚ)}, { data := data } = { data := data_1 } → data = data_1
-- Mathlib.Topology.Algebra.Ring.Real
EReal.instContinuousNeg : ContinuousNeg EReal
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The 0th differential in the complex of inhomogeneous cochains of `A : Rep k G`, as a
`k`-linear map `A → Fun(G, A)`. It sends `(a, g) ↦ ρ_A(g)(a) - a.`  -/
groupCohomology.d₀₁ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{max u u_1, u, u} k G) → ModuleCat.of k ↑A ⟶ ModuleCat.of k (G → ↑A)
-- Mathlib.Algebra.Lie.Derivation.Killing
/-- A local notation for the range of `ad`.  -/
_private.Mathlib.Algebra.Lie.Derivation.Killing.0.LieDerivation.IsKilling.term𝕀 : Lean.ParserDescr
-- Mathlib.Topology.EMetricSpace.Defs
instEDistMultiplicative : {X : Type u_1} → [EDist X] → EDist (Multiplicative X)
-- Mathlib.Algebra.Homology.DerivedCategory.Fractions
/-- Any morphism `f : Q.obj X ⟶ Q.obj Y` in the derived category with `X` strictly `≤ n`
can be written as `f = inv (Q.map s) ≫ Q.map g` with `s : X' ⟶ X` a quasi-isomorphism with
`X'` strictly `≤ n` and `g : X' ⟶ Y`.  -/
DerivedCategory.right_fac_of_isStrictlyLE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {X Y : CochainComplex C ℤ} (f : DerivedCategory.Q.obj X ⟶ DerivedCategory.Q.obj Y)
  (n : ℤ) [X.IsStrictlyLE n],
  ∃ X',
    ∃ (_ : X'.IsStrictlyLE n),
      ∃ s,
        ∃ (x : CategoryTheory.IsIso (DerivedCategory.Q.map s)),
          ∃ g,
            f =
              CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (DerivedCategory.Q.map s))
                (DerivedCategory.Q.map g)
-- Aesop.Script.SpecificTactics
Aesop.Script.Tactic.skip : Aesop.Script.Tactic
-- Lean.Meta.Basic
Lean.Meta.withIncRecDepth : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → n α → n α
-- Mathlib.Algebra.Order.Interval.Basic
instMulNonemptyInterval.eq_1 : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Mul α] [inst_2 : MulLeftMono α] [inst_3 : MulRightMono α],
  instMulNonemptyInterval = { mul := fun s t => { toProd := s.toProd * t.toProd, fst_le_snd := ⋯ } }
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isSeparator_of_isColimit_cofan : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w}
  {f : β → C},
  (CategoryTheory.ObjectProperty.ofObj f).IsSeparating →
    ∀ {c : CategoryTheory.Limits.Cofan f} (hc : CategoryTheory.Limits.IsColimit c), CategoryTheory.IsSeparator c.pt
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C (CategoryTheory.Comon D)),
  (CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj F).X = F.comp (CategoryTheory.Comon.forget D)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue!_insertEntry : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] [inst_2 : Inhabited β] {l : List ((_ : α) × β)} {k a : α}
  {v : β},
  Std.Internal.List.getValue! a (Std.Internal.List.insertEntry k v l) =
    if (k == a) = true then v else Std.Internal.List.getValue! a l
-- Init.Data.Char.Basic
/-- Converts an uppercase ASCII letter to the corresponding lowercase letter. Letters outside the ASCII
alphabet are returned unchanged.

The uppercase ASCII letters are the following: `ABCDEFGHIJKLMNOPQRSTUVWXYZ`.
 -/
Char.toLower : Char → Char
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- **Alias** of `contMDiffAt_finsetSum`. -/
contMDiffAt_finset_sum : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {x : M} {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiffAt I' I n (f i) x) → ContMDiffAt I' I n (fun x => ∑ i ∈ t, f i x) x
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.add_def : ∀ {d : ℤ} (x y x' y' : ℤ), { re := x, im := y } + { re := x', im := y' } = { re := x + x', im := y + y' }
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_le_one_of_nonpos₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {n : ℤ}, 1 ≤ a → n ≤ 0 → a ^ n ≤ 1
-- Init.Control.Lawful.Instances
OptionT.run_seq : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] [LawfulMonad m] (f : OptionT m (α → β)) (x : OptionT m α),
  (f <*> x).run = Option.elimM f.run (pure none) fun f => Option.map f <$> x.run
-- Mathlib.Topology.Order.WithTop
TopologicalSpace.instWithBotOfOrderTopology : {ι : Type u_1} → [inst : Preorder ι] → [inst_1 : TopologicalSpace ι] → [OrderTopology ι] → TopologicalSpace (WithBot ι)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- `ContinuousLinearMap.compContinuousAlternatingMap` as a bundled bilinear map.  -/
ContinuousLinearMap.compContinuousAlternatingMapₗ : (R : Type u_1) →
  (M : Type u_2) →
    (N : Type u_4) →
      (N' : Type u_5) →
        {ι : Type u_6} →
          [inst : CommSemiring R] →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : Module R M] →
                [inst_3 : TopologicalSpace M] →
                  [inst_4 : AddCommMonoid N] →
                    [inst_5 : Module R N] →
                      [inst_6 : TopologicalSpace N] →
                        [inst_7 : ContinuousAdd N] →
                          [inst_8 : ContinuousConstSMul R N] →
                            [inst_9 : AddCommMonoid N'] →
                              [inst_10 : Module R N'] →
                                [inst_11 : TopologicalSpace N'] →
                                  [inst_12 : ContinuousAdd N'] →
                                    [inst_13 : ContinuousConstSMul R N'] →
                                      (N →L[R] N') →ₗ[R] M [⋀^ι]→L[R] N →ₗ[R] M [⋀^ι]→L[R] N'