mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Matrix.Order
Matrix.instStarOrderedRing : ∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n], StarOrderedRing (Matrix n n 𝕜)
-- Init.Data.List.Attach
List.unattach_cons : ∀ {α : Type u_1} {p : α → Prop} {a : { x // p x }} {l : List { x // p x }}, (a :: l).unattach = ↑a :: l.unattach
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.sum.unique : ∀ {α : Type u} [inst : AddGroup α] (g : FreeAddGroup α →+ α),
  (∀ (x : α), g (FreeAddGroup.of x) = x) → ∀ {x : FreeAddGroup α}, g x = FreeAddGroup.sum x
-- Init.Data.Slice.List.Lemmas
List.toArray_mkSlice_rii : ∀ {α : Type u_1} {xs : List α}, Std.Slice.toArray (Std.Rii.Sliceable.mkSlice xs *...*) = xs.toArray
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
HasStrictFDerivAt.exp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E},
  HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun x => Real.exp (f x)) (Real.exp (f x) • f') x
-- Mathlib.Data.Sum.Order
Sum.Lex.noMaxOrder_of_nonempty : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] [NoMaxOrder β] [Nonempty β], NoMaxOrder (α ⊕ₗ β)
-- Mathlib.CategoryTheory.Action.Limits
Action.instNegHom : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} → [inst_1 : Monoid G] → [CategoryTheory.Preadditive V] → {X Y : Action V G} → Neg (X ⟶ Y)
-- Mathlib.Analysis.Calculus.Implicit
HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] (f f_1 : E → F) (e_f : f = f_1) (f' : E →L[𝕜] F) {a a_1 : E}
  (e_a : a = a_1) (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) (hker : (↑f').ker.ClosedComplemented),
  HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker =
    HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented f_1 f' ⋯ hf' hker
-- Mathlib.Topology.Algebra.Group.Defs
/-- Eta-expanded form of `Continuous.div'` -/
Continuous.fun_div' : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Div G]
  [ContinuousDiv G] {f g : X → G}, Continuous f → Continuous g → Continuous fun i => f i / g i
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_naturality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (U : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolutionUnit U]
  {F : CategoryTheory.Functor C V}
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F U] {G : CategoryTheory.Functor C V}
  [inst_7 : CategoryTheory.MonoidalCategory.DayConvolution G U] (f : F ⟶ G) {Z : CategoryTheory.Functor C V}
  (h : G ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.DayConvolution.map f (CategoryTheory.CategoryStruct.id U))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor U G).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor U F).hom
      (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.opNorm_mulLeftRight_apply_le : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (R : Type u_3) [inst_1 : NonUnitalSeminormedRing R]
  [inst_2 : NormedSpace 𝕜 R] [inst_3 : IsScalarTower 𝕜 R R] [inst_4 : SMulCommClass 𝕜 R R] (x : R),
  ‖(ContinuousLinearMap.mulLeftRight 𝕜 R) x‖ ≤ ‖x‖
-- Init.Data.Int.Linear
Int.Internal.Linear.norm_le_coeff_tight_cert.eq_1 : ∀ (lhs rhs : Int.Internal.Linear.Expr) (p : Int.Internal.Linear.Poly) (k : ℤ),
  Int.Internal.Linear.norm_le_coeff_tight_cert lhs rhs p k =
    (Int.blt' 0 k).and'
      ((Int.Internal.Linear.Poly.divCoeffs k (lhs.sub rhs).norm).and'
        (p.beq' (Int.Internal.Linear.Poly.div k (lhs.sub rhs).norm)))
-- Mathlib.Order.Antisymmetrization
antisymmRel_iff_eq : ∀ {α : Type u_1} {a b : α} {r : α → α → Prop} [Std.Refl r] [Std.Antisymm r], AntisymmRel r a b ↔ a = b
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- normed group instance on the product of two normed groups, using the `L^p` norm.  -/
WithLp.instProdNormedAddCommGroup : (p : ENNReal) →
  (α : Type u_2) →
    (β : Type u_3) →
      [hp : Fact (1 ≤ p)] → [NormedAddCommGroup α] → [NormedAddCommGroup β] → NormedAddCommGroup (WithLp p (α × β))
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- A splitting of an extension `S` is `N`-conjugate to another iff there exists `n : N` such that
the section homomorphism is a conjugate of the other section homomorphism by `S.inl n`.  -/
GroupExtension.IsConj : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : Group N] →
        [inst_1 : Group E] → [inst_2 : Group G] → (S : GroupExtension N E G) → S.Splitting → S.Splitting → Prop
-- Mathlib.AlgebraicGeometry.GluingOneHypercover
/-- Constructor for sections over `D.glued` of a sheaf of types on the big Zariski site.  -/
AlgebraicGeometry.Scheme.GlueData.sheafValGluedMk : (D : AlgebraicGeometry.Scheme.GlueData) →
  {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type v)} →
    (s : (j : D.J) → F.obj.obj (Opposite.op (D.U j))) →
      (∀ (i j : D.J),
          (CategoryTheory.ConcreteCategory.hom (F.obj.map (D.f i j).op)) (s i) =
            (CategoryTheory.ConcreteCategory.hom
                (F.obj.map (CategoryTheory.CategoryStruct.comp (D.f j i).op (D.t i j).op)))
              (s j)) →
        F.obj.obj (Opposite.op D.glued)
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.Quotient.coe_vadd_out : ∀ {G : Type u} {X : Type v} [inst : AddGroup G] [inst_1 : AddMonoid X] [inst_2 : AddAction X G] (H : AddSubgroup G)
  [inst_3 : AddAction.QuotientAction X H] (b : X) (q : G ⧸ H), ↑(b +ᵥ Quotient.out q) = b +ᵥ q
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.postcomposeEquivalence_counitIso : ∀ {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} (α : F ≅ G),
  (CategoryTheory.Limits.Cone.postcomposeEquivalence α).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun s =>
        CategoryTheory.Limits.Cone.ext
          (CategoryTheory.Iso.refl
            (((CategoryTheory.Limits.Cone.postcompose α.inv).comp (CategoryTheory.Limits.Cone.postcompose α.hom)).obj
                s).pt)
          ⋯)
      ⋯
-- Mathlib.Algebra.Group.Subsemigroup.Basic
AddHom.eq_of_eqOn_dense : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {s : Set M},
  AddSubsemigroup.closure s = ⊤ → ∀ {f g : M →ₙ+ N}, Set.EqOn (⇑f) (⇑g) s → f = g
-- Mathlib.Algebra.Ring.BooleanRing
/-- The "identity" equivalence between `AsBoolAlg α` and `α`.  -/
toBoolAlg : {α : Type u_1} → α ≃ AsBoolAlg α
-- Std.Do.PredTrans
/-- Given a fixed postcondition, the *stronger* predicate transformer will yield a *weaker*
precondition.
 -/
Std.Do.PredTrans.le : {ps : Std.Do.PostShape} → {α : Type u} → Std.Do.PredTrans ps α → Std.Do.PredTrans ps α → Prop
-- Mathlib.RingTheory.DividedPowers.Basic
instInhabitedDividedPowersBotIdeal : {A : Type u_1} → [inst : CommSemiring A] → Inhabited (DividedPowers ⊥)
-- Mathlib.CategoryTheory.Localization.Bifunctor
/-- If `Lifting₂ L₁ L₂ W₁ W₂ F F'` holds, then `Lifting L₂ W₂ (F.obj X₁) (F'.obj (L₁.obj X₁))`
holds for any `X₁ : C₁`.  -/
CategoryTheory.Localization.Lifting₂.fst : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        {E : Type u_5} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} E] →
                    (L₁ : CategoryTheory.Functor C₁ D₁) →
                      (L₂ : CategoryTheory.Functor C₂ D₂) →
                        (W₁ : CategoryTheory.MorphismProperty C₁) →
                          (W₂ : CategoryTheory.MorphismProperty C₂) →
                            (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)) →
                              (F' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) →
                                [CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F F'] →
                                  (X₁ : C₁) → CategoryTheory.Localization.Lifting L₂ W₂ (F.obj X₁) (F'.obj (L₁.obj X₁))
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.instAddCommGroup : (A : Type u_2) →
  (E : Type u_6) →
    [inst : AddMonoid A] →
      [inst_1 : TopologicalSpace A] →
        [inst_2 : AddCommGroup E] → [inst_3 : TopologicalSpace E] → [IsTopologicalAddGroup E] → AddCommGroup (A →ₜ+ E)
-- Init.Data.BitVec.Bitblast
BitVec.shiftLeftRec_succ : ∀ {w₁ w₂ n : ℕ} {x : BitVec w₁} {y : BitVec w₂},
  x.shiftLeftRec y (n + 1) = x.shiftLeftRec y n <<< (y &&& BitVec.twoPow w₂ (n + 1))
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
/-- The (almost) optimal value of `d` in `Behrend.bound_aux`.  -/
Behrend.dValue : ℕ → ℕ
-- Mathlib.Logic.Encodable.Basic
ULower.ext_iff : ∀ {α : Type u_1} [inst : Encodable α] {a b : ULower α}, a = b ↔ a.up = b.up
-- Lean.Elab.Tactic.Config
Lean.Elab.Tactic.ConfigItemView.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (option : Lean.Ident) (value : Lean.Term) (bool : Bool),
  sizeOf { ref := ref, option := option, value := value, bool := bool } =
    1 + sizeOf ref + sizeOf option + sizeOf value + sizeOf bool
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rxc.Iterator.toArray_eq_match : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.Rxc.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  {it : Std.Iter α},
  it.toArray =
    match it.internalState.next with
    | none => #[]
    | some a =>
      if a ≤ it.internalState.upperBound then
        #[a] ++ { internalState := { next := Std.PRange.succ? a, upperBound := it.internalState.upperBound } }.toArray
      else #[]
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_smul' : ∀ {K : Type u_9} {V : Type u_10} {V₂ : Type u_11} [inst : Semifield K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂] (f : V →ₗ[K] V₂) (p : Submodule K V₂) (a : K),
  Submodule.comap (a • f) p = ⨅ (_ : a ≠ 0), Submodule.comap f p
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.StrongCore.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η : F ⟶ G} [inst_2 : SizeOf B] [inst_3 : SizeOf C]
  (naturality :
    {a b : B} →
      (f : a ⟶ b) →
        CategoryTheory.CategoryStruct.comp (F.map f) (η.app b) ≅ CategoryTheory.CategoryStruct.comp (η.app a) (G.map f))
  (naturality_hom :
    autoParam (∀ {a b : B} (f : a ⟶ b), (naturality f).hom = η.naturality f)
      CategoryTheory.Oplax.OplaxTrans.StrongCore.naturality_hom._autoParam),
  sizeOf { naturality := naturality, naturality_hom := naturality_hom } = 1
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homology_π_ι_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} (i : ι) [inst_2 : K.HasHomology i] {Z : C}
  (h : K.opcycles i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.homologyπ i) (CategoryTheory.CategoryStruct.comp (K.homologyι i) h) =
    CategoryTheory.CategoryStruct.comp (K.iCycles i) (CategoryTheory.CategoryStruct.comp (K.pOpcycles i) h)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.self_le_maxKeyD_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β}
  {fallback : α}, (cmp k ((t.insertIfNew k v).maxKeyD fallback)).isLE = true
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.coe_iSup : ∀ {α : Type u_2} [inst : TopologicalSpace α] {ι : Sort u_5} (s : ι → TopologicalSpace.Opens α),
  ↑(⨆ i, s i) = ⋃ i, ↑(s i)
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.lcm_cycleType : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (σ : Equiv.Perm α), σ.cycleType.lcm = orderOf σ
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- The inverse functor of the identity equivalence is compatible with shifts.
 -/
CategoryTheory.Equivalence.CommShift.instCommShiftInverseRefl : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (A : Type u_3) →
      [inst_1 : AddMonoid A] →
        [inst_2 : CategoryTheory.HasShift C A] → CategoryTheory.Equivalence.refl.inverse.CommShift A
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {E : Type u₂} [inst_4 : CategoryTheory.Category.{v₂, u₂} E]
  [inst_5 : CategoryTheory.CartesianMonoidalCategory E] (G : CategoryTheory.Functor D E) {A : C},
  CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans (F.comp G) A =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.whiskerRight (CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans F A) G)
      (F.whiskerLeft (CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans G (F.obj A)))
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValInt_dvd : ∀ {p : ℕ} (a : ℤ), ↑p ^ padicValInt p a ∣ a
-- Mathlib.Data.Fin.Tuple.Sort
/-- Given `p : α ×ₗ (Fin n) := (f i, i)` with `p ∈ graph f`,
`graph.proj p` is defined to be `f i`.
 -/
Tuple.graph.proj : {n : ℕ} → {α : Type u_1} → [inst : LinearOrder α] → {f : Fin n → α} → ↥(Tuple.graph f) → α
-- Mathlib.Data.WSeq.Defs
/-- Zip a function over two weak sequences  -/
Stream'.WSeq.zipWith : {α : Type u} → {β : Type v} → {γ : Type w} → (α → β → γ) → Stream'.WSeq α → Stream'.WSeq β → Stream'.WSeq γ
-- Mathlib.Order.Bounds.Basic
IsGLB.inter_Iic_of_mem : ∀ {γ : Type u_3} [inst : LinearOrder γ] {s : Set γ} {a b : γ}, IsGLB s a → b ∈ s → IsGLB (s ∩ Set.Iic b) a
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.coe_toLatticeHom : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (f : BoundedLatticeHom α β), ⇑f.toLatticeHom = ⇑f
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.Color.mk.inj : ∀ {red green blue alpha red_1 green_1 blue_1 alpha_1 : Float},
  { red := red, green := green, blue := blue, alpha := alpha } =
      { red := red_1, green := green_1, blue := blue_1, alpha := alpha_1 } →
    red = red_1 ∧ green = green_1 ∧ blue = blue_1 ∧ alpha = alpha_1
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofZeros_f' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg).f' = 0
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instAddMonoid : {R : Type u_3} → {A : Type u_4} → [AddMonoid R] → [AddMonoid A] → AddMonoid (Unitization R A)
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.exists_bifibrant : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (X : HomotopicalAlgebra.CofibrantObject C),
  ∃ Y i,
    HomotopicalAlgebra.Cofibration (HomotopicalAlgebra.CofibrantObject.ι.map i) ∧
      HomotopicalAlgebra.WeakEquivalence (HomotopicalAlgebra.CofibrantObject.ι.map i)
-- Mathlib.Topology.Inseparable
specializes_iff_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ⤳ y ↔ nhds x ≤ nhds y
-- Mathlib.Algebra.Category.CommHopfAlgCat
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
CommHopfAlgCat.Hom.Simps.hom : {R : Type u} → [inst : CommRing R] → (A B : CommHopfAlgCat R) → A.Hom B → ↑A →ₐc[R] ↑B
-- Mathlib.CategoryTheory.CofilteredSystem
CategoryTheory.Functor.IsMittagLeffler.subset_image_eventualRange : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i j : J},
  F.IsMittagLeffler →
    ∀ (f : j ⟶ i), F.eventualRange i ⊆ ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) '' F.eventualRange j
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.instantiateMVars : Lean.Option Bool
-- Lean.Data.PersistentArray
Lean.PersistentArray.Stats.mk.sizeOf_spec : ∀ (numNodes depth tailSize : ℕ),
  sizeOf { numNodes := numNodes, depth := depth, tailSize := tailSize } =
    1 + sizeOf numNodes + sizeOf depth + sizeOf tailSize
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.nontrivial_iff_ne_bot : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), Nontrivial ↥H ↔ H ≠ ⊥
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.forIn_eq_forIn_toList : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {δ : Type w}
  {m' : Type w → Type w'} [inst : Monad m'] [LawfulMonad m'] {f : (a : α) × β a → δ → m' (ForInStep δ)} {init : δ},
  forIn m init f = forIn m.toList init f
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Composition of semiring homomorphisms is associative.  -/
RingHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β}
  {x_2 : NonAssocSemiring γ} {δ : Type u_5} {x_3 : NonAssocSemiring δ} (f : α →+* β) (g : β →+* γ) (h : γ →+* δ),
  (h.comp g).comp f = h.comp (g.comp f)
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_addSubmonoid : ∀ {G : Type u_1} [inst : AddMonoid G] {H : AddSubmonoid G} (y : ↥H), addOrderOf ↑y = addOrderOf y
-- Init.Data.String.Lemmas.Basic
String.Slice.sliceTo_sliceTo : ∀ {s : String.Slice} {pos : s.Pos} {pos' : (s.sliceTo pos).Pos},
  (s.sliceTo pos).sliceTo pos' = s.sliceTo (String.Slice.Pos.ofSliceTo pos')
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.comm₂_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) {Z : C}
  (h : (CategoryTheory.shiftFunctor C 1).obj X₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.m₁ (CategoryTheory.CategoryStruct.comp w₁₃ h) =
    CategoryTheory.CategoryStruct.comp w₁₂ h
-- Aesop.Tree.Data
Aesop.GoalOrigin.originalGoalId? : Aesop.GoalOrigin → Option Aesop.GoalId
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.lsmul_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (R : Type u_3) [inst_3 : SeminormedRing R] [inst_4 : NormedAlgebra 𝕜 R]
  [inst_5 : Module R E] [inst_6 : IsBoundedSMul R E] [inst_7 : IsScalarTower 𝕜 R E] (c : R) (x : E),
  ((ContinuousLinearMap.lsmul 𝕜 R) c) x = c • x
-- Mathlib.Order.PrimeIdeal
Order.Ideal.IsPrime.isMaximal : ∀ {P : Type u_1} [inst : BooleanAlgebra P] {I : Order.Ideal P} [I.IsPrime], I.IsMaximal
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.invVeblen₂_lt_iff : ∀ {a x : Ordinal.{u}}, x.invVeblen₂ < a ↔ Ordinal.omega0 ^ x < Ordinal.veblen x.invVeblen₁ a
-- Init.Data.List.Sublist
List.infix_map_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : List α} {l₂ : List β},
  l₂ <:+: List.map f l₁ ↔ ∃ l, l <:+: l₁ ∧ l₂ = List.map f l
-- Mathlib.Algebra.Homology.Augment
CochainComplex.truncate_map_f : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  {X Y : CochainComplex V ℕ} (f : X ⟶ Y) (i : ℕ), (CochainComplex.truncate.map f).f i = f.f (i + 1)
-- Mathlib.Data.DFinsupp.Notation
/-- Unexpander for the `fun₀ | i => x` notation.  -/
DFinsupp.singleUnexpander : Lean.PrettyPrinter.Unexpander
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.oreEqv.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] (S : AddSubmonoid R) [inst_1 : AddOreLocalization.AddOreSet S] (X : Type u_2)
  [inst_2 : AddAction R X],
  AddOreLocalization.oreEqv S X =
    { r := fun rs rs' => ∃ u v, u +ᵥ rs'.1 = v +ᵥ rs.1 ∧ ↑u + ↑rs'.2 = v + ↑rs.2, iseqv := ⋯ }
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- `[(exp, coef)]` is `Sorted` when `coef` is `Sorted`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.cons_nil : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl},
  coef.Sorted →
    (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef
        Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil).Sorted
-- Mathlib.Topology.Order.ScottTopology
Topology.WithScott.ofScott_toScott : ∀ {α : Type u_1} (a : α), Topology.WithScott.ofScott (Topology.WithScott.toScott a) = a
-- Mathlib.CategoryTheory.Comma.Basic
/-- The isomorphism between `map α β ⋙ fst L' R'` and `fst L R ⋙ F₁`,
where `α : F₁ ⋙ L' ⟶ L ⋙ F`.  -/
CategoryTheory.Comma.mapFst : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {A' : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] →
                {B' : Type u₅} →
                  [inst_4 : CategoryTheory.Category.{v₅, u₅} B'] →
                    {T' : Type u₆} →
                      [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] →
                        {L : CategoryTheory.Functor A T} →
                          {R : CategoryTheory.Functor B T} →
                            {L' : CategoryTheory.Functor A' T'} →
                              {R' : CategoryTheory.Functor B' T'} →
                                {F₁ : CategoryTheory.Functor A A'} →
                                  {F₂ : CategoryTheory.Functor B B'} →
                                    {F : CategoryTheory.Functor T T'} →
                                      (α : F₁.comp L' ⟶ L.comp F) →
                                        (β : R.comp F ⟶ F₂.comp R') →
                                          (CategoryTheory.Comma.map α β).comp (CategoryTheory.Comma.fst L' R') ≅
                                            (CategoryTheory.Comma.fst L R).comp F₁