mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
/-- The homotopy category of cofibrant objects.  -/
HomotopicalAlgebra.CofibrantObject.HoCat : (C : Type u_1) → [inst : CategoryTheory.Category.{v_1, u_1} C] → [HomotopicalAlgebra.ModelCategory C] → Type u_1
-- Mathlib.Control.ULift
PLift.instLawfulFunctor_mathlib : LawfulFunctor PLift
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.pushMsg : Lean.MessageData → Lean.Meta.Grind.M✝ Unit
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.nontrivial : ∀ (R : Type u_8) (S : Type u_9) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [h : IsFractionRing R S] [hR : Nontrivial R], Nontrivial S
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.X.eq_1 : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K],
  RatFunc.X = (algebraMap (Polynomial K) (RatFunc K)) Polynomial.X
-- Mathlib.Algebra.Order.Ring.Cone
RingCone.mem_mk : ∀ {R : Type u_1} [inst : Ring R] {toSubsemiring : Subsemiring R}
  (eq_zero_of_mem_of_neg_mem : ∀ {a : R}, a ∈ toSubsemiring.carrier → -a ∈ toSubsemiring.carrier → a = 0) {x : R},
  x ∈ { toSubsemiring := toSubsemiring, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem } ↔ x ∈ toSubsemiring
-- Batteries.Data.List.Basic
/-- `lookmap` is a combination of `lookup` and `filterMap`.
`lookmap f l` will apply `f : α → Option α` to each element of the list,
replacing `a → b` at the first value `a` in the list such that `f a = some b`.
 -/
List.lookmap : {α : Type u_1} → (α → Option α) → List α → List α
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) {Z : ↑(F.obj d)}
  (h_1 : (F.map h).toFunctor.obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).hom.toNatTrans.app X)) h_1) =
    CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).hom.toNatTrans.app X)
        (CategoryTheory.CategoryStruct.comp ((F.mapComp g h).hom.toNatTrans.app ((F.map f).toFunctor.obj X)) h_1))
-- Mathlib.Analysis.Normed.Group.Pointwise
inv_ball : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x : E), (Metric.ball x δ)⁻¹ = Metric.ball x⁻¹ δ
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.valuation_zero : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], Padic.valuation 0 = 0
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.prime_mk : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p : M}, Prime (Associates.mk p) ↔ Prime p
-- Mathlib.Logic.Embedding.Basic
Equiv.trans_toEmbedding : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (f : β ≃ γ),
  (e.trans f).toEmbedding = e.toEmbedding.trans f.toEmbedding
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatIso.removeOp_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F.op ≅ G.op),
  (CategoryTheory.NatIso.removeOp α).hom = CategoryTheory.NatTrans.removeOp α.hom
-- Mathlib.LinearAlgebra.Finsupp.LSum
Submodule.mulRightMap.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_4} [inst_1 : Semiring S] [inst_2 : Module R S]
  [inst_3 : SMulCommClass R R S] [inst_4 : IsScalarTower R S S] (M : Submodule R S) {N : Submodule R S} {ι : Type u_5}
  (n : ι → ↥N), M.mulRightMap n = (Finsupp.lsum R) fun i => MulOpposite.op ↑(n i) • M.subtype
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.ext_of_isThin : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [Quiver.IsThin C] {n : SimplexCategoryᵒᵖ}
  {x y : (CategoryTheory.nerve C).obj n}, x.obj = y.obj → x = y
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjCyclesSelfIso_hom : ∀ {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),
  (HomologicalComplex.singleObjCyclesSelfIso c j A).hom =
    CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single C c j).obj A).iCycles j)
      (HomologicalComplex.singleObjXSelf c j A).hom
-- Mathlib.MeasureTheory.Group.Prod
/-- A *right*-invariant measure is quasi-preserved by *left*-addition.
This should not be confused with `(measurePreserving_add_left μ g).quasiMeasurePreserving`.  -/
MeasureTheory.quasiMeasurePreserving_add_left : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddRightInvariant] (g : G),
  MeasureTheory.Measure.QuasiMeasurePreserving (fun h => g + h) μ μ
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Given a natural transformation `α : F ⟶ G`, we give a morphism from the cocone point
of a colimit cocone over `F` to the cocone point of any cocone over `G`.  -/
CategoryTheory.Limits.IsColimit.map : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F G : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cocone G} →
            CategoryTheory.Limits.IsColimit t → (s : CategoryTheory.Limits.Cocone F) → (G ⟶ F) → (t.pt ⟶ s.pt)
-- Mathlib.Data.Setoid.Partition
Setoid.quotientEquivClasses_mk_eq : ∀ {α : Type u_1} (r : Setoid α) (a : α), ↑(r.quotientEquivClasses ⟦a⟧) = {x | r x a}
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.ite : ∀ {α : Type u_1} {m : MeasurableSpace α} {t s₁ s₂ : Set α},
  MeasurableSet t → MeasurableSet s₁ → MeasurableSet s₂ → MeasurableSet (t.ite s₁ s₂)
-- Mathlib.Algebra.QuadraticDiscriminant
/-- A quadratic has roots if its discriminant has square roots  -/
exists_quadratic_eq_zero : ∀ {K : Type u_1} [inst : Field K] [NeZero 2] {a b c : K},
  a ≠ 0 → (∃ s, discrim a b c = s * s) → ∃ x, a * (x * x) + b * x + c = 0
-- Mathlib.CategoryTheory.Adjunction.Whiskering
CategoryTheory.Adjunction.whiskerRight_counit_app_app : ∀ (C : Type u_1) {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} (adj : F ⊣ G) (X : CategoryTheory.Functor C E)
  (X_1 : C), ((CategoryTheory.Adjunction.whiskerRight C adj).counit.app X).app X_1 = adj.counit.app (X.obj X_1)
-- Init.Data.UInt.Basic
/-- Bitwise complement, also known as bitwise negation, for 8-bit unsigned integers. Usually accessed
via the `~~~` prefix operator.

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.

This function is overridden at runtime with an efficient implementation.
 -/
UInt8.complement : UInt8 → UInt8
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.isCircuit_antichain : ∀ {α : Type u_1} {M : Matroid α}, IsAntichain (fun x1 x2 => x1 ⊆ x2) (Set.ofPred M.IsCircuit)
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.IsTerminal.strict_hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] {I : C}
  (hI : CategoryTheory.Limits.IsTerminal I) {A : C} (f g : I ⟶ A), f = g
-- Mathlib.Algebra.Order.Pi
Function.const_neg' : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : Preorder α] {a : α} [Nonempty β],
  Function.const β a < 0 ↔ a < 0
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv
HasStrictDerivAt.eventually_right_inverse : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] {f : 𝕜 → 𝕜} {f' a : 𝕜}
  (hf : HasStrictDerivAt f f' a) (hf' : f' ≠ 0),
  ∀ᶠ (x : 𝕜) in nhds (f a), f (HasStrictDerivAt.localInverse f f' a hf hf' x) = x
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- The two types of composition are associative.  -/
LinearMap.compMultilinearMap_compLinearMap : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₁' : ι → Type v₁'} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : (i : ι) → AddCommMonoid (M₁' i)] [inst_3 : AddCommMonoid M₂]
  [inst_4 : AddCommMonoid M₃] [inst_5 : (i : ι) → Module R (M₁ i)] [inst_6 : (i : ι) → Module R (M₁' i)]
  [inst_7 : Module R M₂] [inst_8 : Module R M₃] (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂)
  (f' : (i : ι) → M₁' i →ₗ[R] M₁ i),
  g.compMultilinearMap (f.compLinearMap f') = (g.compMultilinearMap f).compLinearMap f'
-- Init.Data.Option.Instances
Option.instMembership : {α : Type u_1} → Membership α (Option α)
-- Mathlib.Computability.Primrec.List
Primrec.vector_get' : ∀ {α : Type u_1} [inst : Primcodable α] {n : ℕ}, Primrec List.Vector.get
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.ext_iff : ∀ {ι : 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} {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  {inst_5 : AddCommGroup M₂} {inst_6 : Module R M₂} {inst_7 : AddCommGroup N₂} {inst_8 : Module R N₂}
  {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} {x y : P.Equiv Q},
  x = y ↔ (↑x).weightMap = (↑y).weightMap ∧ (↑x).coweightMap = (↑y).coweightMap ∧ (↑x).indexEquiv = (↑y).indexEquiv
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
/-- Let `ι : A ⥤ C` be a fully faithful additive functor where `A` is
an additive category and `C` is a triangulated category. The category `A`
is abelian if the following conditions are satisfied:
* For any object `X` and `Y` in `A`, there is no nonzero morphism
  `ι.obj X ⟶ (ι.obj Y)⟦n⟧` when `n < 0`.
* Any morphism `f₁ : X₁ ⟶ X₂` in `A` is admissible, i.e. when
  we complete `ι.obj f₁` in a distinguished triangle
  `ι.obj X₁ ⟶ ι.obj X₂ ⟶ X₃ ⟶ (ι.obj X₁)⟦1⟧`, there exists objects `K`
  and `Q`, and a distinguished triangle `(ι.obj K)⟦1⟧ ⟶ X₃ ⟶ (ι.obj Q) ⟶ ...`.  -/
CategoryTheory.Triangulated.AbelianSubcategory.abelian : {C : Type u_1} →
  {A : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.HasShift C ℤ] →
            [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
              [inst_5 : CategoryTheory.Pretriangulated C] →
                [inst_6 : CategoryTheory.Category.{v_2, u_2} A] →
                  (ι : CategoryTheory.Functor A C) →
                    (∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (CategoryTheory.shiftFunctor C n).obj (ι.obj Y)),
                        n < 0 → f = 0) →
                      [inst_7 : CategoryTheory.Preadditive A] →
                        [ι.Full] →
                          [ι.Faithful] →
                            [CategoryTheory.Limits.HasFiniteProducts A] →
                              [ι.Additive] →
                                CategoryTheory.Triangulated.AbelianSubcategory.admissibleMorphism ι = ⊤ →
                                  [CategoryTheory.IsTriangulated C] → CategoryTheory.Abelian A
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.not_neg' : ∀ {w : ℕ} (x : BitVec w), ~~~(x + 1#w) = ~~~x + -1#w
-- Mathlib.Data.List.Sublists
List.length_of_sublistsLen : ∀ {α : Type u} {n : ℕ} {l l' : List α}, l' ∈ List.sublistsLen n l → l'.length = n
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.norm_const_eq : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] [h : Nonempty α] (b : β),
  ‖BoundedContinuousFunction.const α b‖ = ‖b‖
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIci_of_mem : ∀ {α : Type u_1} [inst : LinearOrder α] {a x : α} (hx : x ∈ Set.Ici a), Set.projIci a x = ⟨x, hx⟩
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_insertIfNew : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k a : α} {v : β},
      Std.DHashMap.Raw.Const.get? (m.insertIfNew k v) a =
        if (k == a) = true ∧ k ∉ m then some v else Std.DHashMap.Raw.Const.get? m a
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.exists_cell_of_updateCell : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Ord α] [Std.TransOrd α] [Std.LawfulBEqOrd α]
  (l : Std.DTreeMap.Internal.Impl α β) (hlb : l.Balanced),
  l.Ordered →
    ∀ (k : α) (f : Std.DTreeMap.Internal.Cell α β (compare k) → Std.DTreeMap.Internal.Cell α β (compare k)),
      ∃ l',
        l.toListModel.Perm ((List.find? (fun x => compare k x.fst == Ordering.eq) l.toListModel).toList ++ l') ∧
          (Std.DTreeMap.Internal.Impl.updateCell k f l hlb).impl.toListModel.Perm
              ((f (Std.DTreeMap.Internal.List.findCell l.toListModel (compare k))).inner.toList ++ l') ∧
            Std.Internal.List.containsKey k l' = false
-- Mathlib.Order.Filter.Pi
Filter.HasBasis.pi_self : ∀ {ι : Type u_1} {α : Type u_3} {κ : Type u_4} {f : Filter α} {p : κ → Prop} {s : κ → Set α},
  f.HasBasis p s → (Filter.pi fun x => f).HasBasis (fun Ik => Ik.1.Finite ∧ p Ik.2) fun Ik => Ik.1.pi fun x => s Ik.2
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1to0.tr.match_1.eq_2 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (M : Λ → Turing.TM1.Stmt Γ Λ σ)
  (motive : Turing.TM1to0.Λ' M → Γ → Sort u_4) (q : Turing.TM1.Stmt Γ Λ σ) (v : σ) (s : Γ)
  (h_1 : (snd : σ) → (x : Γ) → motive (none, snd) x)
  (h_2 : (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (s : Γ) → motive (some q, v) s),
  (match (some q, v), s with
    | (none, snd), x => h_1 snd x
    | (some q, v), s => h_2 q v s) =
    h_2 q v s
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.replicateRow_empty : ∀ {α : Type u} {ι : Type u_1}, Matrix.replicateRow ι ![] = Matrix.of fun x => ![]
-- Mathlib.CategoryTheory.Limits.Preorder
/-- The infimum of two elements in a preordered type is a binary product in
the category associated to this preorder.  -/
Preorder.isLimitBinaryFan : {C : Type u} →
  [inst : SemilatticeInf C] →
    (X Y : C) →
      CategoryTheory.Limits.IsLimit
        (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯))
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isLongestRevMatch_iff : ∀ {c : Char} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatch c pos ↔
    ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ (s.endPos.prev h).get ⋯ = c
-- Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
TopCat.Sheaf.eq_of_locally_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.HasLimitsOfSize.{x, x, v_1, u_1} C] [(CategoryTheory.forget C).ReflectsIsomorphisms]
  [CategoryTheory.Limits.PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)] {X : TopCat}
  (F : TopCat.Sheaf C X) {ι : Type u_4} (U : ι → TopologicalSpace.Opens ↑X)
  (s t : CategoryTheory.ToType (F.obj.obj (Opposite.op (iSup U)))),
  (∀ (i : ι),
      (CategoryTheory.ConcreteCategory.hom (F.obj.map (TopologicalSpace.Opens.leSupr U i).op)) s =
        (CategoryTheory.ConcreteCategory.hom (F.obj.map (TopologicalSpace.Opens.leSupr U i).op)) t) →
    s = t
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.instReprExprCnstr_lean.repr : Nat.Internal.Linear.ExprCnstr → ℕ → Std.Format
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.trans_apply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [inst_3 : RingHomInvPair σ₁₂ σ₂₁] [inst_4 : RingHomInvPair σ₂₁ σ₁₂]
  {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [inst_5 : RingHomInvPair σ₂₃ σ₃₂] [inst_6 : RingHomInvPair σ₃₂ σ₂₃]
  {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [inst_7 : RingHomInvPair σ₁₃ σ₃₁] [inst_8 : RingHomInvPair σ₃₁ σ₁₃]
  [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {M₁ : Type u_4}
  [inst_11 : TopologicalSpace M₁] [inst_12 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_13 : TopologicalSpace M₂]
  [inst_14 : AddCommMonoid M₂] {M₃ : Type u_6} [inst_15 : TopologicalSpace M₃] [inst_16 : AddCommMonoid M₃]
  [inst_17 : Module R₁ M₁] [inst_18 : Module R₂ M₂] [inst_19 : Module R₃ M₃] (e₁ : M₁ ≃SL[σ₁₂] M₂) (e₂ : M₂ ≃SL[σ₂₃] M₃)
  (c : M₁), (e₁.trans e₂) c = e₂ (e₁ c)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.length_map : ∀ {α : Type u} {β : Type v} {s : Stream'.Seq α} {f : α → β} (h : (Stream'.Seq.map f s).Terminates),
  (Stream'.Seq.map f s).length h = s.length ⋯
-- Mathlib.Algebra.Algebra.Equiv
/-- An equivalence of algebras (denoted as `A ≃ₐ[R] B`)
is an equivalence of rings commuting with the actions of scalars.  -/
AlgEquiv : (R : Type u) →
  (A : Type v) →
    (B : Type w) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] → [inst_2 : Semiring B] → [Algebra R A] → [Algebra R B] → Type (max v w)
-- Mathlib.GroupTheory.EckmannHilton
EckmannHilton.addCommGroup.eq_1 : ∀ {X : Type u} {m₁ : X → X → X} {e₁ : X} (h₁ : EckmannHilton.IsUnital m₁ e₁) [G : AddGroup X]
  (distrib : ∀ (a b c d : X), m₁ (a + b) (c + d) = m₁ a c + m₁ b d),
  EckmannHilton.addCommGroup h₁ distrib = { toAddGroup := G, add_comm := ⋯ }
-- Aesop.Tracing
Aesop.TraceOption.mk.inj : ∀ {traceClass : Lean.Name} {option : Lean.Option Bool} {traceClass_1 : Lean.Name} {option_1 : Lean.Option Bool},
  { traceClass := traceClass, option := option } = { traceClass := traceClass_1, option := option_1 } →
    traceClass = traceClass_1 ∧ option = option_1
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.coeff_truncTotal_pow : ∀ {σ : Type u_1} {R : Type u_2} {n m : ℕ} [inst : Finite σ] [inst_1 : CommSemiring R] (p : MvPowerSeries σ R)
  {x : σ →₀ ℕ},
  Finsupp.degree x < n → MvPolynomial.coeff x ((MvPowerSeries.truncTotal n) p ^ m) = (MvPowerSeries.coeff x) (p ^ m)
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.ext : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] {f g : A →ₛₙₐ[φ] B}, (∀ (x : A), f x = g x) → f = g
-- Init.Data.Array.Lemmas
Array.foldr_append : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → β} {b : β} {xs ys : Array α},
  Array.foldr f b (xs ++ ys) = Array.foldr f (Array.foldr f b ys) xs
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.preimage : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set β}, Set.InjOn f (f ⁻¹' s) → s.Finite → (f ⁻¹' s).Finite
-- Std.Data.DTreeMap.Internal.Operations
/-- A tree map obtained by inserting elements into `t` if they are new, bundled with an inductive principle.  -/
Std.DTreeMap.Internal.Impl.IteratedNewInsertionInto : {α : Type u} → {β : α → Type v} → [Ord α] → Std.DTreeMap.Internal.Impl α β → Type (max 0 u v)
-- Mathlib.CategoryTheory.Limits.Preserves.Presheaf
CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux_hom_app : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] [inst_1 : CategoryTheory.Limits.HasFiniteColimits C]
  (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type} [inst_2 : CategoryTheory.SmallCategory J]
  [inst_3 : CategoryTheory.FinCategory J] (K : CategoryTheory.Functor J Cᵒᵖ),
  (CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux A K).hom.app = fun X =>
    CategoryTheory.CategoryStruct.id (Opposite.unop (CategoryTheory.Limits.limit K) ⟶ X.left)
-- Mathlib.Analysis.Normed.Algebra.Exponential
/-- `expSeries 𝕂 𝔸` is the `FormalMultilinearSeries` whose `n`-th term is the map
`(xᵢ) : 𝔸ⁿ ↦ (1/n! : 𝕂) • ∏ xᵢ`. Its sum is the exponential map `NormedSpace.exp : 𝔸 → 𝔸`.  -/
NormedSpace.expSeries : (𝕂 : Type u_1) →
  (𝔸 : Type u_2) →
    [inst : Field 𝕂] →
      [inst_1 : Ring 𝔸] →
        [inst_2 : Algebra 𝕂 𝔸] →
          [inst_3 : TopologicalSpace 𝔸] → [inst_4 : IsTopologicalRing 𝔸] → FormalMultilinearSeries 𝕂 𝔸 𝔸
-- Init.Data.String.Lemmas.FindPos
String.Slice.posGE.congr_simp : ∀ (s : String.Slice) (offset offset_1 : String.Pos.Raw) (e_offset : offset = offset_1) (h : offset ≤ s.rawEndPos),
  s.posGE offset h = s.posGE offset_1 ⋯
-- Mathlib.Data.Bundle
Bundle.TotalSpace.toProd_apply : ∀ (B : Type u_4) (F : Type u_5) (x : Bundle.TotalSpace F fun x => F), (Bundle.TotalSpace.toProd B F) x = (x.proj, x.snd)
-- Mathlib.Topology.Algebra.Valued.ValuedField
/-- An abbreviation for `IsLocalRing.ResidueField 𝒪[K]` of a `Valued` instance, enabling the
notation `𝓀[K]` for the residue field of a valued field `K`.  -/
Valued.«term𝓀[_]» : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RooSliceData.range : {α : Type u} → {β : α → Type v} → [inst : Ord α] → Std.DTreeMap.Internal.RooSliceData α β → Std.Roo α
-- Init.Grind.Interactive
/-- `apply t` applies theorem `t` as a backward rule.
Only available in `sym =>` mode.
When used with `repeat`, the backward rule is cached for efficiency.  -/
Lean.Parser.Tactic.Grind.symApply : Lean.ParserDescr
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, returning `fallback` if no such pair exists.
 -/
Std.DTreeMap.getEntryGED : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → Sigma β → (a : α) × β a
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If we have a product of `X` and `Y`, we can access it using `prod X Y` or `X ⨯ Y`.  -/
CategoryTheory.Limits.prod : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (X Y : C) → [CategoryTheory.Limits.HasBinaryProduct X Y] → C
-- Mathlib.Data.Fintype.Card
/-- Given that `α ⊕ β` is a fintype, `β` is also a fintype. This is non-computable as it uses
that `Sum.inr` is an injection, but there's no clear inverse if `β` is empty.  -/
Fintype.sumRight : {α : Type u_4} → {β : Type u_5} → [Fintype (α ⊕ β)] → Fintype β
-- Lean.Parser.Command
Lean.Parser.Command.universe.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Category.CompHausLike.EffectiveEpi
/-- If `π` is a surjective morphism in `CompHausLike P`, then it is an effective epi.
 -/
CompHausLike.effectiveEpiStruct : {P : TopCat → Prop} →
  {B X : CompHausLike P} →
    (π : X ⟶ B) → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π) → CategoryTheory.EffectiveEpiStruct π
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.whiskerRight_unit_iso_of_R_fully_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [R.Full] [R.Faithful],
  CategoryTheory.IsIso (CategoryTheory.Functor.whiskerRight h.unit L)
-- Lean.DocString.Extension
Lean.doc.verso : Lean.Option Bool
-- Mathlib.Data.Matrix.Mul
Matrix.smul_mulVec : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n]
  [inst_2 : DistribSMul R α] [IsScalarTower R α α] (b : R) (M : Matrix m n α) (v : n → α),
  (b • M).mulVec v = b • M.mulVec v
-- Mathlib.Data.Finset.NatAntidiagonal
Finset.Nat.antidiagonal_filter_fst_le_of_le : ∀ {n k : ℕ},
  k ≤ n →
    {a ∈ Finset.HasAntidiagonal.antidiagonal n | a.1 ≤ k} =
      Finset.map ((Function.Embedding.refl ℕ).prodMap { toFun := fun x => x + (n - k), inj' := ⋯ })
        (Finset.HasAntidiagonal.antidiagonal k)