mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRight_obj_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (r : R₂ ⟶ R₁) (X : CategoryTheory.Comma L R₂),
  ((CategoryTheory.Comma.mapRight L r).obj X).hom = CategoryTheory.CategoryStruct.comp X.hom (r.app X.right)
-- Mathlib.MeasureTheory.Function.EssSup
essSup_eq_sInf : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder β] {m : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) (f : α → β), essSup f μ = sInf {a | μ {x | a < f x} = 0}
-- Mathlib.Tactic.FunProp.Mor
Mathlib.Meta.FunProp.Mor.App.mk.injEq : ∀ (coe fn arg coe_1 fn_1 arg_1 : Lean.Expr),
  ({ coe := coe, fn := fn, arg := arg } = { coe := coe_1, fn := fn_1, arg := arg_1 }) =
    (coe = coe_1 ∧ fn = fn_1 ∧ arg = arg_1)
-- Mathlib.NumberTheory.Dioph
Poly.sumsq_nonneg : ∀ {α : Type u_1} (x : α → ℕ) (l : List (Poly α)), 0 ≤ (Poly.sumsq l) x
-- Lean.Elab.PreDefinition.Structural.RecArgInfo
/-- position of the argument and its indices we are recursing on, among all parameters  -/
Lean.Elab.Structural.RecArgInfo.indicesAndRecArgPos : Lean.Elab.Structural.RecArgInfo → Array ℕ
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator_hom_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.Arrow C)
  [inst_3 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
      (CategoryTheory.MonoidalCategory.tensorRight X₃.left)]
  [inst_4 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
      (CategoryTheory.MonoidalCategory.tensorRight X₃.right)]
  [inst_5 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₂.hom X₃.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂.left X₃.hom))
      (CategoryTheory.MonoidalCategory.tensorLeft X₁.left)]
  [inst_6 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₂.hom X₃.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂.left X₃.hom))
      (CategoryTheory.MonoidalCategory.tensorLeft X₁.right)],
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator X₁ X₂ X₃).hom.right =
    (CategoryTheory.MonoidalCategoryStruct.associator X₁.right X₂.right X₃.right).hom
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- A path includes the data of `n` 1-simplices in `X`.  -/
SSet.Truncated.Path.arrow : {n : ℕ} →
  {X : SSet.Truncated (n + 1)} → {m : ℕ} → X.Path m → Fin m → X.obj (Opposite.op { obj := { len := 1 }, property := ⋯ })
-- Mathlib.CategoryTheory.Action.Limits
/-- `F : C ⥤ Action V G` preserves limits of some size
if it does after postcomposing with the forgetful functor `Action V G ⥤ V`.  -/
Action.preservesLimitsOfSize_of_preserves : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_2, u_3} C] (F : CategoryTheory.Functor C (Action V G)),
  CategoryTheory.Limits.PreservesLimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F.comp (Action.forget V G)) →
    CategoryTheory.Limits.PreservesLimitsOfSize.{w₂, w₁, v_2, v_1, u_3, max (max u_1 u_2) v_1} F
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_one : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  { toCompletion := ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)).symm 1) } = 1
-- Mathlib.Data.Finsupp.Basic
Finsupp.subtypeDomain_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {p : α → Prop}, Finsupp.subtypeDomain p 0 = 0
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.roth_lower_bound_explicit : ∀ {N : ℕ}, 4096 ≤ N → ↑N * Real.exp (-4 * √(Real.log ↑N)) < ↑(rothNumberNat N)
-- Mathlib.Data.Multiset.ZeroCons
Multiset.empty_or_exists_mem : ∀ {α : Type u_1} (s : Multiset α), s = 0 ∨ ∃ a, a ∈ s
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.mrange_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoidHom.mrange (AddMonoidHom.inr M N) = ⊥.prod ⊤
-- Mathlib.Topology.Sheaves.Functors
/-- Pushforward of sheaves is isomorphic (actually definitionally equal) to pushforward of presheaves.
 -/
TopCat.Sheaf.pushforwardForgetIso : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : TopCat} →
      (f : X ⟶ Y) →
        (TopCat.Sheaf.pushforward C f).comp (TopCat.Sheaf.forget C Y) ≅
          (TopCat.Sheaf.forget C X).comp (TopCat.Presheaf.pushforward C f)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
/-- Integration by parts of Schwartz functions for the Laplacian.

Version for a general bilinear map.  -/
SchwartzMap.integral_bilinear_laplacian_right_eq_left : ∀ {E : Type u_5} {F₁ : Type u_9} {F₂ : Type u_10} {F₃ : Type u_11} [inst : NormedAddCommGroup E]
  [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E] [inst_3 : NormedAddCommGroup F₁]
  [inst_4 : NormedSpace ℝ F₁] [inst_5 : NormedAddCommGroup F₂] [inst_6 : NormedSpace ℝ F₂]
  [inst_7 : NormedAddCommGroup F₃] [inst_8 : NormedSpace ℝ F₃] [inst_9 : MeasurableSpace E]
  {μ : MeasureTheory.Measure E} [BorelSpace E] [μ.IsAddHaarMeasure] (f : SchwartzMap E F₁) (g : SchwartzMap E F₂)
  (L : F₁ →L[ℝ] F₂ →L[ℝ] F₃),
  ∫ (x : E), (L (f x)) ((Laplacian.laplacian g) x) ∂μ = ∫ (x : E), (L ((Laplacian.laplacian f) x)) (g x) ∂μ
-- Mathlib.Analysis.Normed.Group.Uniform
/-- A seminormed group is a uniform additive group, i.e., addition and subtraction are
uniformly continuous.  -/
SeminormedAddCommGroup.to_isUniformAddGroup : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E], IsUniformAddGroup E
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
instPseudoMetricSpaceMultiplicative : {α : Type u} → [PseudoMetricSpace α] → PseudoMetricSpace (Multiplicative α)
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
/-- If `M` is a finite `R`-module, then the canonical map
`AdicCompletion I R ⊗[R] M →ₗ AdicCompletion I M` is surjective.  -/
AdicCompletion.ofTensorProduct_surjective_of_finite : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.Finite R M], Function.Surjective ⇑(AdicCompletion.ofTensorProduct I M)
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.union.inj : ∀ {leanTypeName : Lean.Name} {types : Array Lean.IR.IRType} {leanTypeName_1 : Lean.Name}
  {types_1 : Array Lean.IR.IRType},
  Lean.IR.IRType.union leanTypeName types = Lean.IR.IRType.union leanTypeName_1 types_1 →
    leanTypeName = leanTypeName_1 ∧ types = types_1
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
/-- The Gamma function does not vanish on `ℝ` (except at non-positive integers, where the function
is mathematically undefined and we set it to `0` by convention).  -/
Real.Gamma_ne_zero : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → Real.Gamma s ≠ 0
-- Mathlib.Data.Set.Semiring
SetSemiring.down_zero : ∀ {α : Type u_1}, SetSemiring.down 0 = ∅
-- Mathlib.RingTheory.Flat.Basic
Module.Flat.of_ulift : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Flat R (ULift.{v', v} M)], Module.Flat R M
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.foldWithLeadingToken : {α : Type} → [Inhabited α] → (α → Option Lean.Syntax → Lean.Syntax → α) → α → Lean.Syntax → α
-- Mathlib.Topology.Semicontinuity.Basic
/-- Given a family of upper semicontinuous functions `f : ι → α → β` such that
for each `x : α`, there is a choice `m x : ι` such that the minimum value of
evaluation at `x` is achieved by the function `f (m x)`, then the pointwise
maximum of the family `f` is upper semicontinuous.
In the statement we restrict to subsets `I : Set ι` and `s : Set α` for more generality.  -/
upperSemicontinuousOn_of_forall_isMinOn_and_mem : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {s : Set α} {ι : Type u_4} {f : ι → α → β}
  [inst_1 : Preorder β] {I : Set ι},
  (∀ i ∈ I, UpperSemicontinuousOn (f i) s) →
    ∀ {m : α → ι},
      (∀ x ∈ s, m x ∈ I) → (∀ x ∈ s, IsMinOn (fun i => f i x) I (m x)) → UpperSemicontinuousOn (fun x => f (m x) x) s
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.transpose_empty_cols : ∀ {α : Type u} {m' : Type uₘ} (A : Matrix (Fin 0) m' α), A.transpose = Matrix.of fun x => ![]
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_of_subsingleton : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {f' : α → E'} {g' : α → F'} {l : Filter α} [Subsingleton E'], f' =o[l] g'
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Pos.apply_revSkipWhile_bool_eq_false : ∀ {p : Char → Bool} {s : String} {pos : s.Pos} {h : pos.revSkipWhile p ≠ s.startPos},
  p (((pos.revSkipWhile p).prev h).get ⋯) = false
-- Mathlib.Order.Notation
/-- The top (`⊤`, `\top`) element 

Conventions for notations in identifiers:

 * The recommended spelling of `⊤` in identifiers is `top`. -/
Top.top : {α : Type u_1} → [self : Top α] → α
-- Init.Data.UInt.Lemmas
USize.toUInt8_div : ∀ (a b : USize), a < 256 → b < 256 → (a / b).toUInt8 = a.toUInt8 / b.toUInt8
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.mkEmptyEntries : {α : Type u_1} → {β : Type u_2} → Lean.PersistentHashMap.Node α β
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.mk.injEq : ∀ (wp x y zp ap bp wp_1 x_1 y_1 zp_1 ap_1 bp_1 : ℕ),
  ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp } =
      { wp := wp_1, x := x_1, y := y_1, zp := zp_1, ap := ap_1, bp := bp_1 }) =
    (wp = wp_1 ∧ x = x_1 ∧ y = y_1 ∧ zp = zp_1 ∧ ap = ap_1 ∧ bp = bp_1)
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.representative_toRationalMap_equiv : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y), f.toRationalMap.representative.equiv f
-- Mathlib.Algebra.Notation.Prod
Prod.instNeg.eq_1 : ∀ {G : Type u_8} {H : Type u_9} [inst : Neg G] [inst_1 : Neg H], Prod.instNeg = { neg := fun p => (-p.1, -p.2) }
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdUniformly.congr : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α}
  [inst_1 : UniformSpace α] {f' : ι → β → α},
  HasProdUniformly f g →
    (∀ᶠ (n : Finset ι) in Filter.atTop, ∀ (b : β), ∏ i ∈ n, f i b = ∏ i ∈ n, f' i b) → HasProdUniformly f' g
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
indicator_le_thickenedIndicatorAux : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α), (E.indicator fun x => 1) ≤ thickenedIndicatorAux δ E
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.smul_integral_comp_mul_add : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} (f : ℝ → E) (c d : ℝ),
  c • ∫ (x : ℝ) in a..b, f (c * x + d) = ∫ (x : ℝ) in c * a + d..c * b + d, f x
-- Mathlib.SetTheory.Ordinal.Notation
ONote.fastGrowingε₀.eq_1 : ∀ (i : ℕ), ONote.fastGrowingε₀ i = ((fun a => a.oadd 1 0)^[i] 0).fastGrowing i
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.preservesColimitNatIso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
  [inst_3 : CategoryTheory.Limits.PreservesColimitsOfShape J G] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J D]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfShape J C],
  CategoryTheory.preservesColimitNatIso G = CategoryTheory.preservesColimitNatIso G
-- Mathlib.GroupTheory.Sylow
Sylow.mk.injEq : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] (toSubgroup : Subgroup G) (isPGroup' : IsPGroup p ↥toSubgroup)
  (is_maximal' : ∀ {Q : Subgroup G}, IsPGroup p ↥Q → toSubgroup ≤ Q → Q = toSubgroup) (toSubgroup_1 : Subgroup G)
  (isPGroup'_1 : IsPGroup p ↥toSubgroup_1)
  (is_maximal'_1 : ∀ {Q : Subgroup G}, IsPGroup p ↥Q → toSubgroup_1 ≤ Q → Q = toSubgroup_1),
  ({ toSubgroup := toSubgroup, isPGroup' := isPGroup', is_maximal' := is_maximal' } =
      { toSubgroup := toSubgroup_1, isPGroup' := isPGroup'_1, is_maximal' := is_maximal'_1 }) =
    (toSubgroup = toSubgroup_1)
-- Init.Data.Nat.Basic
Nat.succ_sub_succ : ∀ (n m : ℕ), n.succ - m.succ = n - m
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.symm_bijective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N],
  Function.Bijective FirstOrder.Language.Equiv.symm
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isEmpty_toList : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → m.toList.isEmpty = m.isEmpty
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} CommSemiRingCat
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.isoFinYonedaComponents.congr_simp : ∀ (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [inst : CategoryTheory.Limits.PreservesFiniteProducts F]
  (X : LightProfinite) [inst_1 : Finite ↑X.toTop],
  LightCondensed.isoFinYonedaComponents F X = LightCondensed.isoFinYonedaComponents F X
-- Mathlib.Control.Traversable.Basic
LawfulTraversable.toLawfulFunctor : ∀ {t : Type u → Type u} {inst : Traversable t} [self : LawfulTraversable t], LawfulFunctor t
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_finsupp_sum : ∀ {K : Type u_1} [inst : RCLike K] {α : Type u_3} {M : Type u_4} [inst_1 : Zero M] (f : α →₀ M) (g : α → M → ℝ),
  ↑(f.sum fun a b => g a b) = f.sum fun a b => ↑(g a b)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.Indep.isBase_of_eRk_ge : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → I.Finite → M.eRank ≤ M.eRk I → M.IsBase I
-- Mathlib.Geometry.Convex.Cone.Face.Basic
/-- The comap of a face of a cone under a linear map is a face of the comap of the cone.  -/
PointedCone.IsFaceOf.comap : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C F : PointedCone R M} [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] (f : N →ₗ[R] M), F.IsFaceOf C → (PointedCone.comap f F).IsFaceOf (PointedCone.comap f C)
-- Mathlib.Logic.Basic
/-- **Alias** of `ne_of_ne_of_eq`. -/
Ne.trans_eq : ∀ {α : Sort u_1} {a b c : α}, a ≠ b → b = c → a ≠ c
-- Init.Sym.Lemmas
Lean.Sym.decide_prop_eq_true : ∀ (p : Prop) {inst : Decidable p}, p = True → decide p = true
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.max : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : LinearOrder M] {f g : α → M},
  Function.HasFiniteSupport f → Function.HasFiniteSupport g → Function.HasFiniteSupport fun a => max (f a) (g a)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_refl : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E],
  ⇑(LinearIsometryEquiv.refl R E) = id
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.smul_left : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Zero M] [inst_1 : Zero R] [inst_2 : SMulWithZero R M]
  {f : α → R}, Function.HasFiniteSupport f → ∀ (g : α → M), Function.HasFiniteSupport (f • g)
-- Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
BoundedContinuousFunction.char.eq_1 : ∀ {V : Type u_1} {W : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] [inst_2 : TopologicalSpace V]
  [inst_3 : AddCommGroup W] [inst_4 : Module ℝ W] [inst_5 : TopologicalSpace W] {e : AddChar ℝ Circle}
  {L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ} (he : Continuous ⇑e) (hL : Continuous fun p => (L p.1) p.2) (w : W),
  BoundedContinuousFunction.char he hL w =
    { toFun := fun v => ↑(e ((L v) w)), continuous_toFun := ⋯, map_bounded' := ⋯ }
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : Type w} [inst_1 : CategoryTheory.SmallCategory J]
  {Y : CategoryTheory.Functor J C} {j₀ : J} (y : X ⟶ Y.obj j₀) (t : CategoryTheory.Under j₀),
  (CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g y).app t =
    CategoryTheory.CategoryStruct.comp y (Y.map t.hom)
-- Mathlib.Data.Matrix.Diagonal
Matrix.diag_submatrix : ∀ {l : Type u_1} {m : Type u_2} {α : Type v} (A : Matrix m m α) (e : l → m), (A.submatrix e e).diag = A.diag ∘ e
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Isomorphism of cocones preserves whether or not they are colimiting cocones.  -/
CategoryTheory.Limits.IsColimit.equivIsoColimit : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {r t : CategoryTheory.Limits.Cocone F} →
            (r ≅ t) → CategoryTheory.Limits.IsColimit r ≃ CategoryTheory.Limits.IsColimit t
-- Mathlib.Order.Category.PartOrd
/-- `preordToPartOrd` is left adjoint to the forgetful functor, meaning it is the free
functor from `Preord` to `PartOrd`.  -/
preordToPartOrdForgetAdjunction : preordToPartOrd ⊣ CategoryTheory.forget₂ PartOrd Preord
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `minView` which can be used in the absence of balance information but still
assumes the preconditions of `minView`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.minView! : {α : Type u} →
  {β : α → Type v} →
    (k : α) →
      β k → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl.RawView α β
-- Init.Data.Array.OfFn
Array.ofFnM_pure_comp : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] [LawfulMonad m] {n : ℕ} {f : Fin n → α},
  Array.ofFnM (pure ∘ f) = pure (Array.ofFn f)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceBNe : Lean.Meta.Simp.DSimproc
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.CodeBlock.mk.inj : ∀ {code : Lean.Elab.Term.Do.Code} {uvars : Lean.Elab.Term.Do.VarSet} {code_1 : Lean.Elab.Term.Do.Code}
  {uvars_1 : Lean.Elab.Term.Do.VarSet},
  { code := code, uvars := uvars } = { code := code_1, uvars := uvars_1 } → code = code_1 ∧ uvars = uvars_1
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup.eq_1 : ∀ (o : Ordinal.{u}) (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}), o.bsup f = iSup (o.familyOfBFamily f)
-- Mathlib.Data.Fintype.Pi
Fintype.piFinset.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {δ : α → Type u_4} (t : (a : α) → Finset (δ a)),
  Fintype.piFinset t = Finset.map { toFun := fun f a => f a ⋯, inj' := ⋯ } (Finset.univ.pi t)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
_private.Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.0.CategoryTheory.Limits.WalkingPair.swap.match_1.eq_1 : ∀ (motive : CategoryTheory.Limits.WalkingPair → Sort u_1) (h_1 : Unit → motive CategoryTheory.Limits.WalkingPair.left)
  (h_2 : Unit → motive CategoryTheory.Limits.WalkingPair.right),
  (match CategoryTheory.Limits.WalkingPair.left with
    | CategoryTheory.Limits.WalkingPair.left => h_1 ()
    | CategoryTheory.Limits.WalkingPair.right => h_2 ()) =
    h_1 ()
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.pathObject.lift_π₀_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} {F K : HomologicalComplex C c} [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasPathObject]
  (φ₀ φ₁ : F ⟶ K) (h : Homotopy φ₀ φ₁) {Z : HomologicalComplex C c} (h_1 : K ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.pathObject.lift φ₀ φ₁ h)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.pathObject.π₀ K) h_1) =
    CategoryTheory.CategoryStruct.comp φ₀ h_1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.dropUntil_eq_drop : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk u v) (h : w ∈ p.support),
  p.dropUntil w h = (p.drop (List.idxOf w p.support)).copy ⋯ ⋯
-- Mathlib.Algebra.Group.End
instMonoidEnd : {α : Type u_4} → Monoid (Function.End α)
-- Init.Data.UInt.Lemmas
USize.ofNatClamp.eq_1 : ∀ (n : ℕ),
  USize.ofNatClamp n =
    if h : n < USize.size then USize.ofNatLT n h else USize.ofNatLT (USize.size - 1) USize.ofNatClamp._proof_1
-- Std.Time.Format.Basic
/-- Parses an input string using a builder function, panicking on errors.
 -/
Std.Time.GenericFormat.parseBuilder! : {α : Type} →
  {aw : Std.Time.Awareness} →
    [Inhabited α] → (format : Std.Time.GenericFormat aw) → Std.Time.FormatType (Option α) format.string → String → α
-- Mathlib.Topology.Order.IntermediateValue
ContinuousOn.image_Ico_of_strictAntiOn : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α} {f : α → δ},
  a ≤ b → ContinuousOn f (Set.Icc a b) → StrictAntiOn f (Set.Icc a b) → f '' Set.Ico a b = Set.Ioc (f b) (f a)
-- Init.Data.String.Defs
String.Pos.Raw.isValid_of_eq_rawEndPos : ∀ {s : String} {p : String.Pos.Raw}, p = s.rawEndPos → String.Pos.Raw.IsValid s p
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
AEMeasurable.ae_eq_mk : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α} (h : AEMeasurable f μ), f =ᵐ[μ] AEMeasurable.mk f h
-- Batteries.Data.List.Lemmas
List.diff_cons_right : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (l₁ l₂ : List α) (a : α), l₁.diff (a :: l₂) = (l₁.diff l₂).erase a
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateMulAct.instCountable : ∀ {α : Type u_1} {f : α → α}, Countable (IterateMulAct f)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.map_map_equiv : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  {δ : α → Type w'} {f : (a : α) → β a → γ a} {g : (a : α) → γ a → δ a},
  (Std.DTreeMap.Internal.Impl.map g (Std.DTreeMap.Internal.Impl.map f t)).Equiv
    (Std.DTreeMap.Internal.Impl.map (fun k v => g k (f k v)) t)
-- Mathlib.Algebra.Order.Module.Defs
Pi.instPosSMulStrictMono : ∀ {α : Type u_1} {ι : Type u_3} {β : ι → Type u_4} [inst : Zero α] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : PartialOrder α] [inst_3 : (i : ι) → PartialOrder (β i)] [inst_4 : (i : ι) → SMulWithZero α (β i)]
  [∀ (i : ι), PosSMulStrictMono α (β i)], PosSMulStrictMono α ((i : ι) → β i)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.add'_eq : ∀ {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] [inst_2 : CategoryTheory.Preadditive C]
  {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : W.HasLeftCalculusOfFractions] {X Y : C} (f₁ f₂ : L.obj X ⟶ L.obj Y) (φ : W.LeftFraction₂ X Y),
  f₁ = φ.fst.map L ⋯ → f₂ = φ.snd.map L ⋯ → CategoryTheory.Localization.Preadditive.add' W f₁ f₂ = φ.add.map L ⋯
-- Mathlib.Algebra.Order.Interval.Finset.Basic
Finset.map_add_right_Ioo : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α]
  [ExistsAddOfLE α] [inst_4 : LocallyFiniteOrder α] (a b c : α),
  Finset.map (addRightEmbedding c) (Finset.Ioo a b) = Finset.Ioo (a + c) (b + c)