mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Module.rank_pos_of_free : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [Nontrivial M], 0 < Module.rank R M
-- Batteries.CodeAction.Attr
Batteries.CodeAction.TacticCodeActionEntry.mk : Lean.Name → Array Lean.Name → Batteries.CodeAction.TacticCodeActionEntry
-- Init.GetElem
LawfulGetElem.mk : ∀ {cont : Type u} {idx : Type v} {elem : outParam (Type w)} {dom : outParam (cont → idx → Prop)}
  [ge : GetElem? cont idx elem dom],
  autoParam (∀ (c : cont) (i : idx) [inst : Decidable (dom c i)], c[i]? = if h : dom c i then some c[i] else none)
      LawfulGetElem.getElem?_def._autoParam →
    autoParam
        (∀ [inst : Inhabited elem] (c : cont) (i : idx),
          c[i]! =
            match c[i]? with
            | some e => e
            | none => default)
        LawfulGetElem.getElem!_def._autoParam →
      LawfulGetElem cont idx elem dom
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.eval_multiset_prod_X_sub_C_derivative : ∀ {R : Type u} [inst : CommRing R] [inst_1 : DecidableEq R] {S : Multiset R} {r : R},
  r ∈ S →
    Polynomial.eval r (Polynomial.derivative (Multiset.map (fun a => Polynomial.X - Polynomial.C a) S).prod) =
      (Multiset.map (fun a => r - a) (S.erase r)).prod
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.subtype_comp_inclusion : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} (hH : H ≤ K), K.subtype.comp (Subgroup.inclusion hH) = H.subtype
-- Mathlib.Algebra.Order.Nonneg.Lattice
Nonneg.bot_eq : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, ⊥ = ⟨a, ⋯⟩
-- Mathlib.Algebra.Homology.Functor
CategoryTheory.ShortComplex.quasiIso_iff_evaluation : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {V : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} V] [inst_2 : CategoryTheory.Abelian V]
  {S₁ S₂ : CategoryTheory.ShortComplex (CategoryTheory.Functor T V)} (f : S₁ ⟶ S₂),
  CategoryTheory.ShortComplex.QuasiIso f ↔
    ∀ (j : T), CategoryTheory.ShortComplex.QuasiIso (((CategoryTheory.evaluation T V).obj j).mapShortComplex.map f)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.direction_iInf_of_mem_iInf : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Sort u_4} (s : ι → AffineSubspace k P),
  ∀ p ∈ iInf s, (iInf s).direction = ⨅ i, (s i).direction
-- Mathlib.Analysis.Analytic.CPolynomialDef
CPolynomialAt.exists_mem_nhds_cpolynomialOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E},
  CPolynomialAt 𝕜 f x → ∃ s ∈ nhds x, CPolynomialOn 𝕜 f s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift_denote_mem_prefix : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} {assign : α → Bool} {inv : Bool} (aig : Std.Sat.AIG α)
  (n d q r : aig.RefVec w) (wn wr start : ℕ) (hstart : start < aig.decls.size),
  ⟦assign,
      { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).aig,
        ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧
-- Mathlib.Order.Filter.Prod
Filter.prod_mono : ∀ {α : Type u_1} {β : Type u_2} {f₁ f₂ : Filter α} {g₁ g₂ : Filter β}, f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ ×ˢ g₁ ≤ f₂ ×ˢ g₂
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.ConeMorphism.mk.inj : ∀ {J : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} J} {C : Type u₃} {inst_1 : CategoryTheory.Category.{v₃, u₃} C}
  {F : CategoryTheory.Functor J C} {A B : CategoryTheory.Limits.Cone F} {hom : A.pt ⟶ B.pt}
  {w :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp hom (B.π.app j) = A.π.app j)
      CategoryTheory.Limits.ConeMorphism.w._autoParam}
  {hom_1 : A.pt ⟶ B.pt}
  {w_1 :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp hom_1 (B.π.app j) = A.π.app j)
      CategoryTheory.Limits.ConeMorphism.w._autoParam},
  { hom := hom, w := w } = { hom := hom_1, w := w_1 } → hom = hom_1
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.MVarValue.expr.inj : ∀ {e e_1 : Lean.Expr}, Aesop.EqualUpToIds.MVarValue.expr e = Aesop.EqualUpToIds.MVarValue.expr e_1 → e = e_1
-- Std.Data.ExtHashSet.Basic
/-- The number of elements present in the set  -/
Std.ExtHashSet.size : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashSet α → ℕ
-- Mathlib.NumberTheory.LSeries.ZMod
/-- Explicit formula for the L-function of `𝓕 Φ`, where `𝓕` is the discrete Fourier transform.  -/
ZMod.LFunction_dft : ∀ {N : ℕ} [inst : NeZero N] (Φ : ZMod N → ℂ) {s : ℂ},
  Φ 0 = 0 ∨ s ≠ 1 → ZMod.LFunction (ZMod.dft Φ) s = ∑ j, Φ j * HurwitzZeta.expZeta (ZMod.toAddCircle (-j)) s
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.IsPos.add : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {b : P.Base}
  [inst_5 : CharZero R] {i j k : ι}, b.IsPos i → b.IsPos j → P.root k = P.root i + P.root j → b.IsPos k
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.Hom.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {M N : CategoryTheory.Comon C} {hom : M.X ⟶ N.X} {isComonHom_hom : CategoryTheory.IsComonHom hom} {hom_1 : M.X ⟶ N.X}
  {isComonHom_hom_1 : CategoryTheory.IsComonHom hom_1},
  { hom := hom, isComonHom_hom := isComonHom_hom } = { hom := hom_1, isComonHom_hom := isComonHom_hom_1 } → hom = hom_1
-- Mathlib.Algebra.Group.Basic
div_div : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b c : α), a / b / c = a / (b * c)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.alterKey_cons_perm : ∀ {α : Type u} [inst : BEq α] {β : Type v} {k : α} {f : Option β → Option β} {k' : α} {v' : β} {l : List ((_ : α) × β)},
  (Std.Internal.List.Const.alterKey k f (⟨k', v'⟩ :: l)).Perm
    (if (k' == k) = true then
      match f (some v') with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else ⟨k', v'⟩ :: Std.Internal.List.Const.alterKey k f l)
-- Mathlib.Geometry.Manifold.Submersion
/-- A choice of chart on the co-domain `N` of a submersion `f` at `x`:
w.r.t. this chart and the data `h.domChart` and `h.equiv`,
`f` will look like a projection `(u, v) ↦ u` in these extended charts.
The particular chart is arbitrary, but this choice matches the witnesses given by
`h.equiv` and `h.domChart`.  -/
Manifold.IsSubmersionAt.codChart : {𝕜 : Type u_1} →
  {E'' : Type u_3} →
    {H : Type u_7} →
      {G : Type u_9} →
        {E : Type u} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : NormedAddCommGroup E''] →
                  [inst_4 : NormedSpace 𝕜 E''] →
                    [inst_5 : TopologicalSpace H] →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 E'' G} →
                            {M : Type u_11} →
                              {N : Type u_13} →
                                [inst_7 : TopologicalSpace M] →
                                  [inst_8 : ChartedSpace H M] →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} →
                                            {x : M} → Manifold.IsSubmersionAt I J n f x → OpenPartialHomeomorph N G
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph0_lt_aleph_one : Cardinal.aleph0 < Cardinal.aleph 1
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.UnsatProof : Type
-- Mathlib.Analysis.LocallyConvex.SeparatingDual
/-- See also `geometric_hahn_banach_point_point`.  -/
SeparatingDual.eq_iff_forall_dual_eq : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace V]
  [inst_3 : TopologicalSpace R] [inst_4 : Module R V] [SeparatingDual R V] {x y : V},
  x = y ↔ ∀ (g : StrongDual R V), g x = g y
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.det_nonsing_inv_mul_det : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α),
  IsUnit A.det → A⁻¹.det * A.det = 1
-- Lean.Meta.Tactic.NormCast
/-- `addElim decl` adds `decl` as an `elim` lemma to be used by `norm_cast`.  -/
Lean.Meta.NormCast.addElim : Lean.Name → optParam Lean.AttributeKind Lean.AttributeKind.global → optParam ℕ 1000 → Lean.MetaM Unit
-- Mathlib.Topology.Instances.RatLemmas
Rat.not_secondCountableTopology_opc : ¬SecondCountableTopology (OnePoint ℚ)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
div_eq_of_eq_mul : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c : G₀}, b ≠ 0 → a = c * b → a / b = c
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.map_map_equiv : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {γ : α → Type w}
  {δ : α → Type w'} {f : (a : α) → β a → γ a} {g : (a : α) → γ a → δ a},
  (Std.DTreeMap.Raw.map g (Std.DTreeMap.Raw.map f t)).Equiv (Std.DTreeMap.Raw.map (fun k v => g k (f k v)) t)
-- Mathlib.RingTheory.Coalgebra.MonoidAlgebra
AddMonoidAlgebra.comul_def : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] {X : Type u_3} [inst_2 : Module R A]
  [inst_3 : Coalgebra R A],
  CoalgebraStruct.comul =
    TensorProduct.map ↑(AddMonoidAlgebra.coeffLinearEquiv R).symm ↑(AddMonoidAlgebra.coeffLinearEquiv R).symm ∘ₗ
      CoalgebraStruct.comul ∘ₗ ↑(AddMonoidAlgebra.coeffLinearEquiv R)
-- Mathlib.Order.Interval.Set.ProjIcc
Set.IciExtend_of_le : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a x : α} (f : ↑(Set.Ici a) → β),
  x ≤ a → Set.IciExtend f x = f ⟨a, ⋯⟩
-- Aesop.Util.Basic
Aesop.forEachExprInLDeclCore : {ω : Type} →
  {m : Type → Type} →
    [inst : STWorld ω m] →
      [MonadLiftT (ST ω) m] → [Monad m] → Lean.LocalDecl → (Lean.Expr → m Bool) → Lean.MonadCacheT Lean.Expr Unit m Unit
-- Init.Data.UInt.BasicAux
/-- Converts a 32-bit unsigned integer to an 8-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.
 -/
UInt32.toUInt8 : UInt32 → UInt8
-- Init.Data.List.Monadic
List.allM_cons : ∀ {m : Type → Type u_1} {α : Type u_2} [inst : Monad m] {p : α → m Bool} {x : α} {xs : List α},
  List.allM p (x :: xs) = do
    let __do_lift ← p x
    if __do_lift = true then List.allM p xs else pure false
-- Mathlib.Order.Basic
exists_forall_le_and : ∀ {α : Type u_2} [inst : LinearOrder α] {p q : α → Prop},
  (∃ i, ∀ (j : α), i ≥ j → p j) → (∃ i, ∀ (j : α), i ≥ j → q j) → ∃ i, ∀ (j : α), i ≥ j → p j ∧ q j
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.instBEqPoly.beq.match_1.eq_1 : ∀ (motive : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Sort u_1)
  (h_1 : Unit → motive Lean.Grind.Linarith.Poly.nil Lean.Grind.Linarith.Poly.nil)
  (h_2 :
    (a : ℤ) →
      (a_1 : Lean.Grind.Linarith.Var) →
        (a_2 : Lean.Grind.Linarith.Poly) →
          (b : ℤ) →
            (b_1 : Lean.Grind.Linarith.Var) →
              (b_2 : Lean.Grind.Linarith.Poly) →
                motive (Lean.Grind.Linarith.Poly.add a a_1 a_2) (Lean.Grind.Linarith.Poly.add b b_1 b_2))
  (h_3 : (x x_1 : Lean.Grind.Linarith.Poly) → motive x x_1),
  (match Lean.Grind.Linarith.Poly.nil, Lean.Grind.Linarith.Poly.nil with
    | Lean.Grind.Linarith.Poly.nil, Lean.Grind.Linarith.Poly.nil => h_1 ()
    | Lean.Grind.Linarith.Poly.add a a_1 a_2, Lean.Grind.Linarith.Poly.add b b_1 b_2 => h_2 a a_1 a_2 b b_1 b_2
    | x, x_1 => h_3 x x_1) =
    h_1 ()
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_C_le : ∀ {R : Type u} {a : R} [inst : Semiring R], (Polynomial.C a).degree ≤ 0
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.Context.mk.injEq : ∀ (options : Lean.Options) (table : Lean.Parser.TokenTable) (options_1 : Lean.Options)
  (table_1 : Lean.Parser.TokenTable),
  ({ options := options, table := table } = { options := options_1, table := table_1 }) =
    (options = options_1 ∧ table = table_1)
-- Lean.Meta.Tactic.Grind.CasesMatch
/-- Given a splitter alternative, annotate the terms that are `match`-expression
conditions corresponding to overlapping patterns.
 -/
_private.Lean.Meta.Tactic.Grind.CasesMatch.0.Lean.Meta.Grind.addMatchCondsToAlt : Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.BindStruct.bind : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Presieve X}
  {R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Presieve Y} {Z : C} {h : Z ⟶ X} (b : S.BindStruct R h), S.bind R h
-- Mathlib.Order.Filter.Pi
Filter.pi_inf_principal_pi_neBot : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {s : (i : ι) → Set (α i)} [∀ (i : ι), (f i).NeBot]
  {I : Set ι}, (Filter.pi f ⊓ Filter.principal (I.pi s)).NeBot ↔ ∀ i ∈ I, (f i ⊓ Filter.principal (s i)).NeBot
-- Mathlib.GroupTheory.Coset.Basic
AddMonoidHom.fiberEquiv_symm_apply : ∀ {α : Type u_1} [inst : AddGroup α] {H : Type u_2} [inst_1 : AddGroup H] (f : α →+ H) (a b : α) (g : ↑(⇑f ⁻¹' {f b})),
  ↑((f.fiberEquiv a b).symm g) = a + (-b + ↑g)
-- Batteries.CodeAction.Attr
/-- Read a tactic code action from a declaration of the right type.  -/
Batteries.CodeAction.mkTacticCodeAction : Lean.Name → Lean.ImportM Batteries.CodeAction.TacticCodeAction
-- Mathlib.Computability.Primrec.Basic
Primcodable.option : {α : Type u_1} → [h : Primcodable α] → Primcodable (Option α)
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_singleton_neg : ∀ {α : Type u} [inst : Ring α] (x : α), Ideal.span {-x} = Ideal.span {x}
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.deleteVerts_verts : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s : Set V}, (G'.deleteVerts s).verts = G'.verts \ s
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.coe_skeletonLT : ∀ {X : Type u_1} [t : TopologicalSpace X] [inst : T2Space X] (C : Set X) {D : Set X}
  [inst_1 : Topology.RelCWComplex C D] (n : ℕ∞),
  ↑(Topology.RelCWComplex.skeletonLT C n) = D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, Topology.RelCWComplex.closedCell m j
-- Init.Data.List.Range
List.zipIdx_map_fst : ∀ {α : Type u_1} (i : ℕ) (l : List α), List.map Prod.fst (l.zipIdx i) = l
-- Mathlib.Order.Disjoint
disjoint_iff : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b ↔ a ⊓ b = ⊥
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Fact.mk : (coeffs : Lean.Omega.Coeffs) →
  (constraint : Lean.Omega.Constraint) →
    Lean.Elab.Tactic.Omega.Justification constraint coeffs → Lean.Elab.Tactic.Omega.Fact
-- Mathlib.GroupTheory.CoprodI
/-- Given a family of free groups with distinguished bases, then their free product is free, with
a basis given by the union of the bases of the components.  -/
Monoid.CoprodI.FreeGroupBasis.coprodI : {ι : Type u_4} →
  {X : ι → Type u_5} →
    {G : ι → Type u_6} →
      [inst : (i : ι) → Group (G i)] →
        ((i : ι) → FreeGroupBasis (X i) (G i)) → FreeGroupBasis ((i : ι) × X i) (Monoid.CoprodI G)
-- Mathlib.Analysis.Calculus.Gradient.Basic
hasGradientWithinAt_iff_hasFDerivWithinAt : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F} {s : Set F},
  HasGradientWithinAt f f' s x ↔ HasFDerivWithinAt f ((InnerProductSpace.toDual 𝕜 F) f') s x
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonInlayHint : Lean.FromJson Lean.Lsp.InlayHint
-- Init.Data.Range.Polymorphic.IntLemmas
Int.map_add_toArray_rco : ∀ {m n k : ℤ}, Array.map (fun x => x + k) (m...n).toArray = ((m + k)...n + k).toArray
-- Mathlib.Order.Basic
/-- **Alias** of `lt_of_eq_of_lt''`. -/
Eq.trans_gt : ∀ {α : Type u_1} {a b c : α} [inst : LT α], a = b → c < b → c < a
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- When `S₁.g` and `S₂.g` are zero and we have chosen colimit cokernel coforks `c₁` and `c₂`
for `S₁.f` and `S₂.f` respectively, the action on left homology of a morphism `φ : S₁ ⟶ S₂` of
short complexes is given by the unique morphism `f : c₁.pt ⟶ c₂.pt` such that
`φ.τ₂ ≫ c₂.π = c₁.π ≫ f`.  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsColimitCokernelCofork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (hg₁ : S₁.g = 0) →
            (c₁ : CategoryTheory.Limits.CokernelCofork S₁.f) →
              (hc₁ : CategoryTheory.Limits.IsColimit c₁) →
                (hg₂ : S₂.g = 0) →
                  (c₂ : CategoryTheory.Limits.CokernelCofork S₂.f) →
                    (hc₂ : CategoryTheory.Limits.IsColimit c₂) →
                      (f : c₁.pt ⟶ c₂.pt) →
                        CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) =
                            CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f →
                          CategoryTheory.ShortComplex.LeftHomologyMapData φ
                            (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S₁ hg₁ c₁ hc₁)
                            (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S₂ hg₂ c₂ hc₂)
-- Mathlib.Algebra.Lie.Matrix
/-- For square matrices, the natural map that reindexes a matrix's rows and columns with equivalent
types, `Matrix.reindex`, is an equivalence of Lie algebras.  -/
Matrix.reindexLieEquiv : {R : Type u} →
  [inst : CommRing R] →
    {n : Type w} →
      [inst_1 : DecidableEq n] →
        [inst_2 : Fintype n] →
          {m : Type w₁} → [inst_3 : DecidableEq m] → [inst_4 : Fintype m] → n ≃ m → Matrix n n R ≃ₗ⁅R⁆ Matrix m m R
-- Mathlib.CategoryTheory.IsoCat
/-- The equivalence of categories underlying an `IsoCat`, with the unit and counit
isomorphisms induced by the defining equalities.  -/
CategoryTheory.IsoCat.toEquivalence : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] → CategoryTheory.IsoCat C D → (C ≌ D)
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.Slice.foldr.eq_1 : ∀ {α : Type u} (f : Char → α → α) (init : α) (s : String.Slice),
  String.Slice.foldr f init s = Std.Iter.fold (flip f) init s.revChars
-- Mathlib.GroupTheory.OrderOfElement
card_nsmul_eq_zero' : ∀ {G : Type u_6} [inst : AddGroup G] {x : G}, Nat.card G • x = 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.find?_eq_some_iff_getValueCast?_eq_some : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.DistinctKeys l →
    (List.find? (fun x => x.fst == k) l = some ⟨k, v⟩ ↔ Std.Internal.List.getValueCast? k l = some v)
-- Mathlib.Data.Set.NAry
/-- A common special case of `image2_congr`  -/
Set.image2_congr' : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f f' : α → β → γ} {s : Set α} {t : Set β},
  (∀ (a : α) (b : β), f a b = f' a b) → Set.image2 f s t = Set.image2 f' s t
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- If a measure `μ` is left-invariant and satisfies the right scaling condition, then it
satisfies `QuotientMeasureEqMeasurePreimage`.  -/
MeasureTheory.leftInvariantIsQuotientMeasureEqMeasurePreimage : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G] [IsTopologicalGroup G]
  [BorelSpace G] [PolishSpace G] {Γ : Subgroup G} [inst_6 : Γ.Normal] [T2Space (G ⧸ Γ)]
  [SecondCountableTopology (G ⧸ Γ)] {μ : MeasureTheory.Measure (G ⧸ Γ)} (ν : MeasureTheory.Measure G)
  [ν.IsMulLeftInvariant] [Countable ↥Γ] [ν.IsMulRightInvariant] [MeasureTheory.SigmaFinite ν] [μ.IsMulLeftInvariant]
  [MeasureTheory.SigmaFinite μ] [MeasureTheory.IsFiniteMeasure μ]
  [hasFun : MeasureTheory.HasFundamentalDomain (↥Γ.op) G ν],
  MeasureTheory.covolume (↥Γ.op) G ν = μ Set.univ → MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ
-- Mathlib.Algebra.Ring.Equiv
/-- Reinterpret a ring equivalence as a ring homomorphism.  -/
RingEquiv.toRingHom : {R : Type u_4} → {S : Type u_5} → [inst : NonAssocSemiring R] → [inst_1 : NonAssocSemiring S] → R ≃+* S → R →+* S
-- Init.PropLemmas
Bool.ite_then_true : ∀ {p : Prop} [inst : Decidable p] {x : Bool}, (if p then true else x) = true ↔ p ∨ x = true
-- Mathlib.Algebra.Ring.Subring.Order
/-- A subring of a strict ordered ring is a strict ordered ring.  -/
Subring.toIsStrictOrderedRing : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : SetLike S R]
  [inst_3 : SubringClass S R] [IsStrictOrderedRing R] (s : S), IsStrictOrderedRing ↥s
-- Init.Grind.Lemmas
Lean.Grind.eq_false_of_or_eq_false_left : ∀ {a b : Prop}, (a ∨ b) = False → a = False
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- A subring is a `ℤ`-subalgebra.  -/
subalgebraOfSubring : {R : Type u_1} → [inst : Ring R] → Subring R → Subalgebra ℤ R
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Lift a function `{a : M // a ≠ 1} → α` that's monotone along archimedean classes to a
monotone function `FiniteMulArchimedeanClass M →o α`.  -/
FiniteMulArchimedeanClass.liftOrderHom : {M : Type u_1} →
  [inst : CommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedMonoid M] →
        {α : Type u_2} →
          [inst_3 : PartialOrder α] →
            (f : { a // a ≠ 1 } → α) →
              (∀ (a b : { a // a ≠ 1 }),
                  FiniteMulArchimedeanClass.mk ↑a ⋯ ≤ FiniteMulArchimedeanClass.mk ↑b ⋯ → f a ≤ f b) →
                FiniteMulArchimedeanClass M →o α
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- The measurable equivalence between `UnitAddTorus` and a product of `Ioc` intervals.  -/
UnitAddTorus.measurableEquivPiIoc : {ι : Type u_2} → (b : ι → ℝ) → UnitAddTorus ι ≃ᵐ { x // ∀ (i : ι), x i ∈ Set.Ioc (b i) (b i + 1) }
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- The right whiskering of a 2-isomorphism is a 2-isomorphism.  -/
CategoryTheory.Bicategory.«term_▷ᵢ_» : Lean.TrailingParserDescr
-- Init.Data.List.Impl
List.takeWhile_eq_takeWhileTR : @List.takeWhile = @List.takeWhileTR
-- Mathlib.Analysis.Complex.Angle
Complex.angle_div_left_eq_angle_mul_right : ∀ (a x y : ℂ), InnerProductGeometry.angle (x / a) y = InnerProductGeometry.angle x (y * a)
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.instFullInclusion : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C),
  (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.inclusion F).Full
-- Mathlib.Combinatorics.Enumerative.Composition
/-- The blocks of a composition, seen as a function on `Fin c.length`. When composing analytic
functions using compositions, this is the main player.  -/
Composition.blocksFun : {n : ℕ} → (c : Composition n) → Fin c.length → ℕ
-- Mathlib.LinearAlgebra.Contraction
/-- The natural map associating a linear map to the tensor product of two modules.  -/
dualTensorHom : (R : Type u_2) →
  (M : Type u_3) →
    (N : Type u_4) →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] → [inst_4 : Module R N] → TensorProduct R (Module.Dual R M) N →ₗ[R] M →ₗ[R] N
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.basicOpen_zero : ∀ {R : Type u} [inst : CommSemiring R], PrimeSpectrum.basicOpen 0 = ⊥
-- Mathlib.Topology.Compactness.SigmaCompact
CompactExhaustion.isCompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] (K : CompactExhaustion X) (n : ℕ), IsCompact (K n)