mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.toExtension_commRing : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι), P.toExtension.commRing = AddMonoidAlgebra.commRing
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.it₁ : {α α₂ β : Type w} → {m : Type w → Type u_1} → Std.Iterators.Types.Flatten α α₂ β m → Std.IterM m (Std.IterM m β)
-- Init.Data.List.TakeDrop
List.length_lt_of_drop_ne_nil : ∀ {α : Type u_1} {l : List α} {i : ℕ}, List.drop i l ≠ [] → i < l.length
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat.equivalenceSingleObjInverse_map : ∀ (R : Type) [inst : Ring R] {X Y : CategoryTheory.Mat_ (CategoryTheory.SingleObj Rᵐᵒᵖ)} (f : X ⟶ Y)
  (i : (FintypeCat.of X.ι).obj) (j : (FintypeCat.of Y.ι).obj),
  (CategoryTheory.Mat.equivalenceSingleObjInverse R).map f i j = MulOpposite.unop (f i j)
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.Precylinder.LeftHomotopy.symm_h : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {P : HomotopicalAlgebra.Precylinder X} {Y : C}
  {f g : X ⟶ Y} (h : P.LeftHomotopy f g), h.symm.h = h.h
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsNonneg.smul : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {I₁ I₂ : R →+* R} [inst_3 : Preorder R] [PosMulMono R] {B : M →ₛₗ[I₁] M →ₛₗ[I₂] R} {c : R},
  B.IsNonneg → 0 ≤ c → (c • B).IsNonneg
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.le_ceil : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] (a : R), a ≤ ↑⌈a⌉₊
-- Mathlib.Data.Fintype.Card
Fintype.card_range_le : ∀ {α : Type u_4} {β : Type u_5} (f : α → β) [inst : Fintype α] [inst_1 : Fintype ↑(Set.range f)],
  Fintype.card ↑(Set.range f) ≤ Fintype.card α
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.tr_respects : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} {enc : Γ → List.Vector Bool n} (dec : List.Vector Bool n → Γ)
  (M : Λ → Turing.TM1.Stmt Γ Λ σ) [inst : Inhabited Γ] {enc0 : enc default = List.Vector.replicate n false},
  (∀ (a : Γ), dec (enc a) = a) →
    StateTransition.Respects (Turing.TM1.step M) (Turing.TM1.step (Turing.TM1to1.tr enc dec M)) fun c₁ c₂ =>
      Turing.TM1to1.trCfg enc enc0 c₁ = c₂
-- Mathlib.Data.Finset.Card
Finset.pred_card_le_card_erase : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α], s.card - 1 ≤ (s.erase a).card
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.RightExactFunctor.ofExact_map_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : C ⥤ₑ D} (α : F ⟶ G), ((CategoryTheory.RightExactFunctor.ofExact C D).map α).hom = α.hom
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.comap_filter : ∀ {β : Type u_2} {γ : Type u_3} (L : SummationFilter β) (f : γ ↪ β),
  (L.comap f).filter = Filter.map (fun s => s.preimage ⇑f ⋯) L.filter
-- Std.Do.PostCond
Std.Do.PostCond.entails_noThrow : ∀ {α : Type u_1} {ps : Std.Do.PostShape} (p : α → Std.Do.Assertion ps) (q : Std.Do.PostCond α ps),
  (Std.Do.PostCond.noThrow p).entails q ↔ ∀ (a : α), p a ⊢ₛ q.1 a
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.mk : {ι : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {s : optParam (Set X) Set.univ} →
        (toFun : ι → C(X, ℝ)) →
          (LocallyFinite fun i => Function.support ⇑(toFun i)) →
            0 ≤ toFun →
              (∀ x ∈ s, ∑ᶠ (i : ι), (toFun i) x = 1) → (∀ (x : X), ∑ᶠ (i : ι), (toFun i) x ≤ 1) → PartitionOfUnity ι X s
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsNonloop.closure_eq_of_mem_closure : ∀ {α : Type u_1} {M : Matroid α} {e f : α}, M.IsNonloop e → e ∈ M.closure {f} → M.closure {e} = M.closure {f}
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.ιMapObjOrZero_eq : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  (X : CategoryTheory.GradedObject I C) (p : I → J) [inst_1 : X.HasMap p]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : DecidableEq J] (i : I) (j : J) (h : p i = j),
  X.ιMapObjOrZero p i j = X.ιMapObj p i j h
-- Init.Data.Array.Lemmas
Array.anyM_loop_iff_exists : ∀ {α : Type u_1} {p : α → Bool} {as : Array α} {start stop : ℕ} (h : stop ≤ as.size),
  (Array.anyM.loop (fun x => pure (p x)) as stop h start).run = true ↔
    ∃ i, ∃ (x : i < as.size), start ≤ i ∧ i < stop ∧ p as[i] = true
-- Mathlib.GroupTheory.Torsion
/-- The torsion subgroup of an abelian group.  -/
CommGroup.torsion : (G : Type u_1) → [inst : CommGroup G] → Subgroup G
-- Init.Data.Int.Gcd
Int.gcd_self_sub_right : ∀ (m n : ℤ), m.gcd (m - n) = m.gcd n
-- Mathlib.Algebra.Category.Grp.EpiMono
AddCommGrpCat.mono_iff_injective : ∀ {A B : AddCommGrpCat} (f : A ⟶ B), CategoryTheory.Mono f ↔ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.LinearAlgebra.Prod
Submodule.fst.eq_1 : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], Submodule.fst R M M₂ = Submodule.comap (LinearMap.snd R M M₂) ⊥
-- Lean.Linter.UnusedVariables
/-- Collect into a heterogeneous collection of objects with external storage. This uses
pointer identity and does not store the objects, so it is important not to store the last
pointer to an object in the map, or it can be freed and reused, resulting in incorrect behavior.

Returns `true` if the object was not already in the set.  -/
Lean.Linter.UnusedVariables.insertObjImpl : {α : Type} → IO.Ref (Std.HashSet USize) → α → IO Bool
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
nndist_triangle_left : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y z : α), nndist x y ≤ nndist z x + nndist z y
-- Mathlib.Testing.Plausible.Functions
Plausible.Antitone.testable : {α : Type u} →
  {β : Type v} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        (f : α → β) →
          [I :
              Plausible.Testable
                (Plausible.NamedBinder "x"
                  (∀ (x : α), Plausible.NamedBinder "y" (∀ (y : α), Plausible.NamedBinder "H" (x ≤ y → f y ≤ f x))))] →
            Plausible.Testable (Antitone f)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
_private.Mathlib.Combinatorics.SimpleGraph.Walk.Operations.0.SimpleGraph.Walk.drop.match_1.splitter : {V : Type u_1} →
  {G : SimpleGraph V} →
    {u : V} →
      (motive : (v : V) → G.Walk u v → ℕ → Sort u_2) →
        (v : V) →
          (p : G.Walk u v) →
            (n : ℕ) →
              ((x : ℕ) → motive u SimpleGraph.Walk.nil x) →
                ((v : V) → (p : G.Walk u v) → (v = u → p ≍ SimpleGraph.Walk.nil → False) → motive v p 0) →
                  ((v v_1 : V) →
                      (h : G.Adj u v_1) → (q : G.Walk v_1 v) → (n : ℕ) → motive v (SimpleGraph.Walk.cons h q) n.succ) →
                    motive v p n
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.mk.sizeOf_spec : ∀ {ι : 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} [inst_5 : SizeOf ι]
  [inst_6 : SizeOf R] [inst_7 : SizeOf M] [inst_8 : SizeOf N] (support : Finset ι)
  (linearIndepOn_root : LinearIndepOn R ⇑P.root ↑support) (linearIndepOn_coroot : LinearIndepOn R ⇑P.coroot ↑support)
  (root_mem_or_neg_mem :
    ∀ (i : ι),
      P.root i ∈ AddSubmonoid.closure (⇑P.root '' ↑support) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' ↑support))
  (coroot_mem_or_neg_mem :
    ∀ (i : ι),
      P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' ↑support) ∨
        -P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' ↑support)),
  sizeOf
      { support := support, linearIndepOn_root := linearIndepOn_root, linearIndepOn_coroot := linearIndepOn_coroot,
        root_mem_or_neg_mem := root_mem_or_neg_mem, coroot_mem_or_neg_mem := coroot_mem_or_neg_mem } =
    1 + sizeOf support
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_find?_of_eq : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α → Ordering} [Std.Internal.IsStrictCut compare k]
  {sz : ℕ} {k' : α} {v' : β k'} {l r : Std.DTreeMap.Internal.Impl α β},
  k k' = Ordering.eq →
    (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).Ordered →
      List.find? (fun x => k x.fst == Ordering.eq) (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).toListModel =
        some ⟨k', v'⟩
-- Init.Conv
/-- `done` succeeds iff there are no goals remaining.  -/
Lean.Parser.Tactic.Conv.convDone : Lean.ParserDescr
-- Mathlib.CategoryTheory.Functor.Basic
CategoryTheory.Functor.id_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C), (CategoryTheory.Functor.id C).obj X = X
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.toArray_insert_perm : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : BEq α] [Std.TransCmp cmp]
  [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {k : α} {v : β},
      (t.insert k v).toArray.Perm ((Array.filter (fun x => decide ¬(k == x.1) = true) t.toArray).push (k, v))
-- Mathlib.Analysis.Normed.Ring.Lemmas
Dilation.mulLeft_toFun : ∀ {α : Type u_1} [inst : NonUnitalNormedRing α] [inst_1 : NormMulClass α] (a : α) (ha : a ≠ 0) (b : α),
  (Dilation.mulLeft a ha) b = a * b
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.isClosed_inter_nonempty_of_isClosed : ∀ {α : Type u_1} [inst : TopologicalSpace α] {F : Set α}, IsClosed F → IsClosed {K | (↑K ∩ F).Nonempty}
-- Mathlib.Algebra.PresentedMonoid.Basic
/-- Given a set of relations, `rels`, over a type `α`, `PresentedMonoid` constructs the monoid with
generators `x : α` and relations `rels` as a quotient of a congruence structure over rels.  -/
PresentedMonoid : {α : Type u_1} → (FreeMonoid α → FreeMonoid α → Prop) → Type u_1
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.withPrimedNamesImp : {α : Type} → Array Lean.Expr → Lean.MetaM α → Lean.MetaM α
-- Mathlib.Algebra.Group.Action.Defs
smul_pow : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : MulAction M N] [IsScalarTower M N N]
  [SMulCommClass M N N] (r : M) (x : N) (n : ℕ), (r • x) ^ n = r ^ n • x ^ n
-- Init.Data.SInt.Bitwise
Int32.toInt8_and : ∀ (a b : Int32), (a &&& b).toInt8 = a.toInt8 &&& b.toInt8
-- Mathlib.Order.InitialSeg
/-- **Alias** of the reverse direction of `InitialSeg.isMin_apply_iff`. -/
InitialSeg.map_isMin : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] {a : α} [inst_1 : PartialOrder α] (f : α ≤i β),
  IsMin a → IsMin (f a)
-- Aesop.RuleTac.Forward
_private.Aesop.RuleTac.Forward.0.Aesop.RuleTac.makeForwardHypProofs.loop : Lean.Expr → Array Lean.MVarId → Array Lean.MVarId → ℕ → ℕ → Array Lean.FVarId → Aesop.RuleTac.ForwardM Unit
-- Mathlib.RingTheory.Coalgebra.Basic
Coalgebra.rTensor_counit_comul : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] (a : A), (LinearMap.rTensor A CoalgebraStruct.counit) (CoalgebraStruct.comul a) = 1 ⊗ₜ[R] a
-- Mathlib.CategoryTheory.Limits.Preserves.Lattice
CategoryTheory.Limits.CompleteLattice.instPreservesFiniteLimitsToFunctorToOrderHom : ∀ {α : Type u} {β : Type v} {F : Type u_1} [inst : FunLike F α β] (f : F) [inst_1 : SemilatticeInf α]
  [inst_2 : OrderTop α] [inst_3 : SemilatticeInf β] [inst_4 : OrderTop β] [inst_5 : InfTopHomClass F α β],
  CategoryTheory.Limits.PreservesFiniteLimits (↑f).toFunctor
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.mul_apply : ∀ {R : Type uR} {A₁ : Type uA₁} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Algebra R A₁]
  (e₁ e₂ : A₁ ≃ₐ[R] A₁) (x : A₁), (e₁ * e₂) x = e₁ (e₂ x)
-- Mathlib.Algebra.Star.Center
Set.star_mem_centralizer : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : StarMul R] {a : R} {s : Set R},
  a ∈ (s ∪ star s).centralizer → star a ∈ (s ∪ star s).centralizer
-- Mathlib.Combinatorics.Matroid.Basic
/-- **Alias** of `Matroid.setOfPred_indep_eq`. -/
Matroid.setOf_indep_eq : ∀ {α : Type u_1} (M : Matroid α), {I | M.Indep I} = ↑(lowerClosure {B | M.IsBase B})
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_mul_coe_angle : ∀ {x y : ℂ}, x ≠ 0 → y ≠ 0 → ↑(x * y).arg = ↑x.arg + ↑y.arg
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {he : t ≠ ∅}
  {fallback : α}, t.getKeyD (t.minKey he) fallback = t.minKey he
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
det_fderivPolarCoordSymm : ∀ (p : ℝ × ℝ), (fderivPolarCoordSymm p).det = p.1
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.unop_top : ∀ {M : Type u_2} [inst : Add M], ⊤.unop = ⊤
-- Init.Data.Fin.Lemmas
/-- For rewriting in the reverse direction, see `Fin.cast_addNat_left`.  -/
Fin.addNat_cast : ∀ {n n' m : ℕ} (i : Fin n') (h : n' = n), (Fin.cast h i).addNat m = Fin.cast ⋯ (i.addNat m)
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_39 : HSub Std.Time.Week.Offset Std.Time.Minute.Offset Std.Time.Minute.Offset
-- Mathlib.Algebra.Group.Basic
eq_neg_add_iff_add_eq : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, a = -b + c ↔ b + a = c
-- Lean.Elab.InfoTree.Types
Lean.Elab.CommandContextInfo.mctx : Lean.Elab.CommandContextInfo → Lean.MetavarContext
-- Init.System.IOError
IO.Error.mkResourceExhausted : UInt32 → String → IO.Error
-- Mathlib.NumberTheory.FLT.Three
/-- Given `S' : Solution'`, `S'.multiplicity` is the multiplicity of `λ` in `S'.c`, as a natural
number.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution'.multiplicity : {K : Type u_1} →
  [inst : Field K] → {ζ : K} → {hζ : IsPrimitiveRoot ζ 3} → FermatLastTheoremForThreeGen.Solution'✝ hζ → ℕ
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.WideSubcategory.isoMk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.MorphismProperty C}
  [inst_1 : P.IsMultiplicative] {X Y : CategoryTheory.WideSubcategory P} (e e_1 : X.obj ≅ Y.obj) (e_e : e = e_1)
  (h₁ : P e.hom) (h₂ : P e.inv),
  CategoryTheory.WideSubcategory.isoMk e h₁ h₂ = CategoryTheory.WideSubcategory.isoMk e_1 ⋯ ⋯
-- Std.Data.TreeMap.Basic
/-- Transforms an array of keys into a tree map.  -/
Std.TreeMap.unitOfArray : {α : Type u} → Array α → (cmp : autoParam (α → α → Ordering) Std.TreeMap.unitOfArray._auto_1) → Std.TreeMap α Unit cmp
-- Mathlib.Data.Set.SMulAntidiagonal
Set.smulAntidiagonal.eq_1 : ∀ {G : Type u_1} {P : Type u_2} [inst : SMul G P] (s : Set G) (t : Set P) (a : P),
  s.smulAntidiagonal t a = {x | x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a}
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
HomogeneousIdeal.coe_comap : ∀ {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} {ι : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] [inst_4 : AddSubmonoidClass σ A] [inst_5 : AddSubmonoidClass τ B]
  [inst_6 : DecidableEq ι] [inst_7 : AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} [inst_8 : GradedRing 𝒜]
  [inst_9 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) {J : HomogeneousIdeal ℬ}, ↑(HomogeneousIdeal.comap f J) = ⇑f ⁻¹' ↑J
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rcc_eq_singleton_append : ∀ {m n : ℤ}, m ≤ n → (m...=n).toArray = #[m] ++ ((m + 1)...=n).toArray
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.equiv_of_beq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α] [inst_3 : (k : α) → BEq (β k)] [∀ (k : α), LawfulBEq (β k)],
  (↑m₁).WF → (↑m₂).WF → m₁.beq m₂ = true → (↑m₁).Equiv ↑m₂
-- Mathlib.CategoryTheory.Preadditive.HomOrthogonal
/-- `HomOrthogonal.matrixDecomposition` as an additive equivalence.  -/
CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_1} →
      {s : ι → C} →
        [inst_1 : CategoryTheory.Preadditive C] →
          [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C] →
            CategoryTheory.HomOrthogonal s →
              {α β : Type} →
                [inst_3 : Finite α] →
                  [inst_4 : Finite β] →
                    {f : α → ι} →
                      {g : β → ι} →
                        ((⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) ≃+
                          ((i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (CategoryTheory.End (s i)))
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.inf_comap_le_comap_add : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (q : Submodule R₂ M₂) (f₁ f₂ : M →ₛₗ[τ₁₂] M₂),
  Submodule.comap f₁ q ⊓ Submodule.comap f₂ q ≤ Submodule.comap (f₁ + f₂) q
-- Lean.Meta.Tactic.Grind.Util
/-- Unfolds all `reducible` declarations occurring in the goal's target.
 -/
Lean.MVarId.unfoldReducible : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.Order.Monotone.Defs
Antitone.strictAnti_of_injective : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : PartialOrder β] {f : α → β},
  Antitone f → Function.Injective f → StrictAnti f
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k : α} [inst_2 : Inhabited β],
  (List.map Prod.fst l).contains k = false → Std.ExtDHashMap.Const.get! (Std.ExtDHashMap.Const.ofList l) k = default
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.pow_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (e : C ≌ C), e ^ 0 = CategoryTheory.Equivalence.refl
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
/-- The cokernel cofork of `(K.extend e).d i' j'` that is deduced from a cokernel
cofork of `K.d i j`.  -/
HomologicalComplex.extend.rightHomologyData.cokernelCofork : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                (K : HomologicalComplex C c) →
                  (e : c.Embedding c') →
                    {i j : ι} →
                      {i' j' : ι'} →
                        e.f j = j' →
                          c.prev j = i →
                            c'.prev j' = i' →
                              CategoryTheory.Limits.CokernelCofork (K.d i j) →
                                CategoryTheory.Limits.CokernelCofork ((K.extend e).d i' j')
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.opcyclesFunctor_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i : ι) [inst_2 : CategoryTheory.CategoryWithHomology C]
  {X Y : HomologicalComplex C c} (f : X ⟶ Y),
  (HomologicalComplex.opcyclesFunctor C c i).map f = HomologicalComplex.opcyclesMap f i
-- Lean.Elab.Tactic.Omega.MinNatAbs
Lean.Elab.Tactic.Omega.List.nonzeroMinimum_map_le_nonzeroMinimum : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (p : α → ℕ) (q : β → ℕ) (xs : List α),
  (∀ a ∈ xs, p a = 0 ↔ q (f a) = 0) →
    (∀ a ∈ xs, p a ≠ 0 → q (f a) ≤ p a) →
      Lean.Elab.Tactic.Omega.List.nonzeroMinimum (List.map q (List.map f xs)) ≤
        Lean.Elab.Tactic.Omega.List.nonzeroMinimum (List.map p xs)
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.Q_idem_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (q : ℕ) {Z : ChainComplex C ℕ}
  (h : AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Q q)
      (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Q q) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Q q) h
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.State.generatorStack : Lean.Meta.SynthInstance.State → Array Lean.Meta.SynthInstance.GeneratorNode
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.locallySmall_max : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], CategoryTheory.LocallySmall.{max v w, v, u} C
-- Lean.Data.PersistentArray
Lean.PersistentArray.empty : {α : Type u} → Lean.PersistentArray α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.eraseMany_list : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : t₁.WF)
  (h₂ : t₂.WF), t₁.Equiv t₂ → ∀ {l : List α}, (↑(t₁.eraseMany l ⋯)).Equiv ↑(t₂.eraseMany l ⋯)
-- Mathlib.Algebra.Group.Basic
add_one_zsmul : ∀ {G : Type u_3} [inst : AddGroup G] (a : G) (n : ℤ), (n + 1) • a = n • a + a
-- Lean.Data.KVMap
Lean.KVMap.setInt : Lean.KVMap → Lean.Name → ℤ → Lean.KVMap
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.toArray_map : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp} {f : α → β → γ},
  Std.DTreeMap.Const.toArray (Std.DTreeMap.map f t) =
    Array.map (fun p => (p.1, f p.1 p.2)) (Std.DTreeMap.Const.toArray t)
-- Init.Data.String.FindPos
/-- Returns the previous valid position before the given position, given a proof that the position
is not the start position, which guarantees that such a position exists.
 -/
String.Slice.Pos.prev : {s : String.Slice} → (pos : s.Pos) → pos ≠ s.startPos → s.Pos
-- Mathlib.Algebra.Lie.Classical
/-- A matrix transforming the bilinear form defined by the matrix `JD` into a split-signature
diagonal matrix.

It looks like this as a `2l x 2l` matrix of `l x l` blocks:

```
[ 1 -1 ]
[ 1  1 ]
```  -/
LieAlgebra.Orthogonal.PD : (l : Type u_4) → (R : Type u₂) → [DecidableEq l] → [CommRing R] → Matrix (l ⊕ l) (l ⊕ l) R
-- Mathlib.Order.Interval.Basic
Interval.forall : ∀ {α : Type u_1} [inst : LE α] {p : Interval α → Prop},
  (∀ (s : Interval α), p s) ↔ p ⊥ ∧ ∀ (s : NonemptyInterval α), p ↑s
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.comapDomainAddMonoidHom.eq_1 : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f : M → N) (hf : Function.Injective f),
  MonoidAlgebra.comapDomainAddMonoidHom f hf =
    { toFun := MonoidAlgebra.comapDomain f hf, map_zero' := ⋯, map_add' := ⋯ }
-- Lean.Elab.InfoTree.Types
Lean.Elab.instInhabitedInfoTree : Inhabited Lean.Elab.InfoTree
-- Lean.Data.KVMap
Lean.DataValue.ofBool.injEq : ∀ (v v_1 : Bool), (Lean.DataValue.ofBool v = Lean.DataValue.ofBool v_1) = (v = v_1)
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.dNatTrans_app : ∀ {ι : Type u_1} (V : Type u) [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (i j : ι) (X : HomologicalComplex V c),
  (HomologicalComplex.dNatTrans V c i j).app X = X.d i j
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_toInt32 : ∀ (n : ISize) (h : System.Platform.numBits = 32), n.toInt32.toBitVec = BitVec.signExtend 32 (n.toBitVec32 h)
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.prod_mono_left : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (t : Subring S),
  Monotone fun s => s.prod t
-- Mathlib.RingTheory.Ideal.Height
Ideal.height_lt_top : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R}, I ≠ ⊤ → ∀ [I.FiniteHeight], I.height < ⊤
-- Mathlib.Data.Semiquot
/-- Apply a function returning a `Semiquot` to a `Semiquot`.  -/
Semiquot.bind : {α : Type u_1} → {β : Type u_2} → Semiquot α → (α → Semiquot β) → Semiquot β
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag'_neg : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [inst : AddGroup α]
  (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α), (-M).blockDiag' = -M.blockDiag'