mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.WithOne.Basic
WithZero.lift_zero : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : AddZeroClass β] (f : α →ₙ+ β), (WithZero.lift f) 0 = 0
-- Lean.Compiler.IR.Basic
Lean.IR.instBEqLitVal : BEq Lean.IR.LitVal
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.eq_nil_of_length_zero : ∀ {V : Type u} [inst : Quiver V] {a : V} (p : Quiver.Path a a), p.length = 0 → p = Quiver.Path.nil
-- Mathlib.Algebra.Order.BigOperators.Expect
Finset.exists_le_of_expect_le_expect : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [IsOrderedCancelAddMonoid α]
  [inst_3 : Module ℚ≥0 α] [PosSMulStrictMono ℚ≥0 α] {s : Finset ι} {f g : ι → α},
  s.Nonempty → ((s.expect fun i => g i) ≤ s.expect fun i => f i) → ∃ x ∈ s, g x ≤ f x
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.instEpiδ₀Iter : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (i : ℕ) {n m : ℕ}
  (hi : n + i = m), CategoryTheory.Epi (X.δ₀Iter i hi)
-- Init.Data.Rat.Basic
/-- Negation of rational numbers.  -/
Rat.neg : ℚ → ℚ
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- The left dual of the object `X`.  -/
CategoryTheory.HasLeftDual.leftDual : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} → (Y : C) → [self : CategoryTheory.HasLeftDual Y] → C
-- Mathlib.Topology.Semicontinuity.Basic
IsOpen.upperSemicontinuous_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {s : Set α} {y : β} [inst_1 : Zero β] [inst_2 : Preorder β],
  IsOpen s → y ≤ 0 → UpperSemicontinuous (s.indicator fun _x => y)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atomRel_neg₂ : ∀ {R : Type u_1} [inst : CommRing R] {W : ℤ → R},
  Function.Odd W → ∀ (a b c d : ℤ), IsEllipticNet.atomRel W a (-b) c d = IsEllipticNet.atomRel W a b c d
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.norm_eq_one : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (i : ι), ‖b i‖ = 1
-- Mathlib.RingTheory.Polynomial.Hermite.Basic
/-- the probabilists' Hermite polynomials.  -/
Polynomial.hermite : ℕ → Polynomial ℤ
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A binary bicone for a pair of objects `P Q : C` consists of the cone point `X`,
maps from `X` to both `P` and `Q`, and maps from both `P` and `Q` to `X`,
so that `inl ≫ fst = 𝟙 P`, `inl ≫ snd = 0`, `inr ≫ fst = 0`, and `inr ≫ snd = 𝟙 Q`  -/
CategoryTheory.Limits.BinaryBicone.pt : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → {P Q : C} → CategoryTheory.Limits.BinaryBicone P Q → C
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.nhds_bot' : nhds ⊥ = ⨅ a, Filter.principal (Set.Iio ↑a)
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingNorm.ringNormClass : ∀ {R : Type u_1} [inst : NonUnitalRing R], RingNormClass (RingNorm R) R ℝ
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.toArrow_map_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.CosimplicialObject.Augmented C}
  (η : X ⟶ Y), (CategoryTheory.CosimplicialObject.Augmented.toArrow.map η).left = η.left
-- Aesop.Forward.State
/-- Extract stats from a `RuleState`.  -/
Aesop.RuleState.stats : Aesop.RuleState → Aesop.ForwardRuleStateStats
-- Mathlib.Order.Heyting.Basic
disjoint_compl_right : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a : α}, Disjoint a aᶜ
-- Mathlib.Algebra.Group.Finsupp
AddEquiv.finsuppUnique_apply : ∀ {M : Type u_3} [inst : AddZeroClass M] {ι : Type u_8} [inst_1 : Unique ι] (a : ι →₀ M),
  AddEquiv.finsuppUnique a = a default
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
Finsupp.DegLex.wellFoundedLT : ∀ {α : Type u_1} [inst : LinearOrder α] [WellFoundedGT α], WellFoundedLT (DegLex (α →₀ ℕ))
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.mem_subgroup_orbit_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {H : Subgroup G} {x : α}
  {a b : ↑(MulAction.orbit G x)}, a ∈ MulAction.orbit (↥H) b ↔ ↑a ∈ MulAction.orbit ↥H ↑b
-- Mathlib.Analysis.Complex.Exponential
Real.expNear_sub : ∀ (n : ℕ) (x r₁ r₂ : ℝ), Real.expNear n x r₁ - Real.expNear n x r₂ = x ^ n / ↑n.factorial * (r₁ - r₂)
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Triangle inequality** for the norm.  -/
norm_mul₄_le' : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a b c d : E}, ‖a * b * c * d‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentContentChangeEvent.rangeChange.injEq : ∀ (range : Lean.Lsp.Range) (text : String) (range_1 : Lean.Lsp.Range) (text_1 : String),
  (Lean.Lsp.TextDocumentContentChangeEvent.rangeChange range text =
      Lean.Lsp.TextDocumentContentChangeEvent.rangeChange range_1 text_1) =
    (range = range_1 ∧ text = text_1)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instHashableResolvableCompletionItemData : Hashable Lean.Lsp.ResolvableCompletionItemData
-- Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
/-- The subgroup of `alternatingGroup α` generated by permutations of cycle type (2, 2).

When `Nat.card α = 4`, it will effectively be of Klein Four type.  -/
alternatingGroup.kleinFour : (α : Type u_1) → [inst : DecidableEq α] → [inst_1 : Fintype α] → Subgroup ↥(alternatingGroup α)
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.homologyπ_restrictionHomologyIso_hom : ∀ {ι : 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]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (i j k : ι) (hi : c.prev j = i)
  (hk : c.next j = k) {i' j' k' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hk' : e.f k = k') (hi'' : c'.prev j' = i')
  (hk'' : c'.next j' = k') [inst_3 : K.HasHomology j'] [inst_4 : (K.restriction e).HasHomology j],
  CategoryTheory.CategoryStruct.comp ((K.restriction e).homologyπ j)
      (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom =
    CategoryTheory.CategoryStruct.comp (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom (K.homologyπ j')
-- Init.Data.List.MinMaxOn
_private.Init.Data.List.MinMaxOn.0.List.foldl.match_1.eq_2 : ∀ {α : Type u_3} {β : Type u_1} (motive : α → List β → Sort u_2) (a : α) (b : β) (l : List β)
  (h_1 : (a : α) → motive a []) (h_2 : (a : α) → (b : β) → (l : List β) → motive a (b :: l)),
  (match a, b :: l with
    | a, [] => h_1 a
    | a, b :: l => h_2 a b l) =
    h_2 a b l
-- Batteries.CodeAction.Attr
Batteries.CodeAction.TacticCodeActions.mk : Array Batteries.CodeAction.TacticCodeAction →
  Lean.NameMap (Array Batteries.CodeAction.TacticCodeAction) → Batteries.CodeAction.TacticCodeActions
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.instInitialElementsFiberFunctorOfIsCofiltered : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  {N : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C)
  [inst_3 : CategoryTheory.InitiallySmall N] [CategoryTheory.IsCofiltered N],
  (CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.functor p).Initial
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_diff_eq_size_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  (∀ a ∈ m₁, a ∉ m₂) → (m₁ \ m₂).size = m₁.size
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_set_insert : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] (a : α) (b : β) (s : Set β),
  a +ᵥ insert b s = insert (a +ᵥ b) (a +ᵥ s)
-- Mathlib.Algebra.Group.Action.Defs
/-- Auxiliary definition for `VAdd.comp`, `AddAction.compHom`, etc.  -/
VAdd.comp.vadd : {M : Type u_1} → {N : Type u_2} → {α : Type u_5} → [VAdd M α] → (N → M) → N → α → α
-- Mathlib.Algebra.Ring.Defs
/-- The canonical homomorphism `ℤ → R` agrees with the one from `ℕ → R` on `ℕ`.  -/
NonAssocRing.intCast_ofNat : ∀ {α : Type u_1} [self : NonAssocRing α] (n : ℕ), IntCast.intCast ↑n = ↑n
-- Mathlib.AlgebraicGeometry.Noetherian
AlgebraicGeometry.IsLocallyNoetherian.mk : ∀ {X : AlgebraicGeometry.Scheme},
  autoParam (∀ (U : ↑X.affineOpens), IsNoetherianRing ↑(X.presheaf.obj (Opposite.op ↑U)))
      AlgebraicGeometry.IsLocallyNoetherian.component_noetherian._autoParam →
    AlgebraicGeometry.IsLocallyNoetherian X
-- Mathlib.Order.Filter.AtTopBot.Defs
Filter.atTop.eq_1 : ∀ {α : Type u_3} [inst : Preorder α], Filter.atTop = ⨅ a, Filter.principal (Set.Ici a)
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Break.runK.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive x
-- Mathlib.Geometry.Manifold.ChartedSpace
nonempty_of_chartedSpace : ∀ {H : Type u_5} {M : Type u_6} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [ChartedSpace H M] (x : M),
  Nonempty H
-- Mathlib.Algebra.Homology.HomotopyCategory
/-- Homotopy equivalent complexes become isomorphic in the homotopy category.  -/
HomotopyCategory.isoOfHomotopyEquiv : {ι : Type u_2} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C D : HomologicalComplex V c} →
            HomotopyEquiv C D → ((HomotopyCategory.quotient V c).obj C ≅ (HomotopyCategory.quotient V c).obj D)
-- Init.Data.String.Basic
String.Slice.Pos.cast_le_iff : ∀ {s t : String.Slice} {pos : s.Pos} {pos' : t.Pos} {h : s.copy = t.copy}, pos.cast h ≤ pos' ↔ pos ≤ pos'.cast ⋯
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveElabStep1.mk.sizeOf_spec : ∀ (view : Lean.Elab.Command.InductiveView)
  (elabCtors :
    Array Lean.Elab.Command.ElabHeaderResult →
      Lean.Elab.Command.ElabHeaderResult → Array Lean.Expr → Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep2),
  sizeOf { view := view, elabCtors := elabCtors } = 1 + sizeOf view
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.StrictOrLazy.strict.injEq : ∀ {α β : Type} (a a_1 : α), (Lean.Widget.StrictOrLazy.strict a = Lean.Widget.StrictOrLazy.strict a_1) = (a = a_1)
-- Mathlib.Tactic.Simps.Basic
/-- Output debug messages. Not used much, use `set_option simps.debug true` instead.  -/
Simps.Config.debug : Simps.Config → Bool
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.nextCoeffUp_C_eq_zero : ∀ {R : Type u} [inst : Semiring R] (c : R), (Polynomial.C c).nextCoeffUp = 0
-- Mathlib.Data.Finset.Sym
Finset.sym2_val : ∀ {α : Type u_1} (s : Finset α), s.sym2.val = s.val.sym2
-- Std.Internal.UV.Timer
/-- This function has different behavior depending on the state and configuration of the `Timer`:
- if `repeating` is `false` and:
  - it is initial, run it and return a new `IO.Promise` that is set to resolve once `timeout`
    milliseconds have elapsed. After this `IO.Promise` is resolved the `Timer` is finished.
  - it is running or finished, return the same `IO.Promise` that the first call to `next` returned.
- if `repeating` is `true` and:
  - it is initial, run it and return a new `IO.Promise` that resolves right away
    (as it is the 0th multiple of `timeout`).
  - it is running, check whether the last returned `IO.Promise` is already resolved:
     - If it is, return a new `IO.Promise` that resolves upon finishing the next cycle
     - If it is not, return the last `IO.Promise`
     This ensures that the returned `IO.Promise` resolves at the next repetition of the timer.
  - if it is finished, return the last `IO.Promise` created by `next`. Notably this could be one
    that never resolves if the timer was stopped before fulfilling the last one.
 -/
Std.Internal.UV.Timer.next : Std.Internal.UV.Timer → IO (IO.Promise Unit)
-- Mathlib.MeasureTheory.Function.LpSpace.Complete
_private.Mathlib.MeasureTheory.Function.LpSpace.Complete.0.MeasureTheory.Lp.eLpNorm'_sum_norm_sub_le_tsum_of_cauchy_eLpNorm' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_3} [inst : NormedAddCommGroup E]
  {f : ℕ → α → E},
  (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
    ∀ {p : ℝ},
      1 ≤ p →
        ∀ {B : ℕ → ENNReal},
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → MeasureTheory.eLpNorm' (f n - f m_1) p μ < B N) →
            ∀ (n : ℕ),
              MeasureTheory.eLpNorm' (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypeEquivCodomain_apply : ∀ {X : Sort u_9} {Y : Sort u_10} [inst : DecidableEq X] {x : X} (f : { x' // x' ≠ x } → Y)
  (g : { g // g ∘ Subtype.val = f }), (Equiv.subtypeEquivCodomain f) g = ↑g x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getEntryGT_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α} {h' : ∃ a ∈ t₁, cmp a k = Ordering.gt} (h : t₁.Equiv t₂), t₁.getEntryGT k h' = t₂.getEntryGT k ⋯
-- Init.Data.String.Lemmas.FindPos
String.le_posLE_iff : ∀ {s : String} {p : s.Pos} {q : String.Pos.Raw}, p ≤ s.posLE q ↔ p.offset ≤ q
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.IsCofiltered.IsEventuallyConstant.mk : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C},
  (∃ j, F.IsEventuallyConstantTo j) → CategoryTheory.IsCofiltered.IsEventuallyConstant F
-- Mathlib.Data.Analysis.Topology
Ctop.toTopsp_isTopologicalBasis : ∀ {α : Type u_1} {σ : Type u_3} (F : Ctop α σ), TopologicalSpace.IsTopologicalBasis (Set.range F.f)
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- The function that sends an element of the additive free group to its maximal
reduction.  -/
FreeAddGroup.toWord : {α : Type u_1} → [DecidableEq α] → FreeAddGroup α → List (α × Bool)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.instQuiverArrow : {T : Type u} → [inst : CategoryTheory.Category.{v, u} T] → Quiver (CategoryTheory.Arrow T)
-- Mathlib.GroupTheory.Divisible
ULift.instRootableBy : (A : Type u_1) →
  (α : Type u_2) →
    [inst : Monoid A] → [inst_1 : Pow A α] → [inst_2 : Zero α] → [RootableBy A α] → RootableBy (ULift.{u_3, u_1} A) α
-- Mathlib.Algebra.Category.ModuleCat.Free
ModuleCat.free_shortExact_rank_add : ∀ {R : Type u_3} [inst : Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)},
  S.ShortExact →
    ∀ [Module.Free R ↑S.X₁] [Module.Free R ↑S.X₃] [StrongRankCondition R],
      Module.rank R ↑S.X₂ = Module.rank R ↑S.X₁ + Module.rank R ↑S.X₃
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph_degree_three_le : ∀ {n : ℕ} {v : Fin (n + 3)}, (SimpleGraph.cycleGraph (n + 3)).degree v = 2
-- Mathlib.Data.ENNReal.Basic
ENNReal.iUnion_Ioo_coe_nat : ∀ {a : ENNReal}, ⋃ n, Set.Ioo a ↑n = Set.Ioi a \ {⊤}
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoTree.brecOn_4.go : {motive_1 : Lean.Elab.InfoTree → Sort u} →
  {motive_2 : Lean.PersistentArray Lean.Elab.InfoTree → Sort u} →
    {motive_3 : Lean.PersistentArrayNode Lean.Elab.InfoTree → Sort u} →
      {motive_4 : Array Lean.Elab.InfoTree → Sort u} →
        {motive_5 : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u} →
          {motive_6 : List Lean.Elab.InfoTree → Sort u} →
            {motive_7 : List (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u} →
              (t : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree)) →
                ((t : Lean.Elab.InfoTree) → t.below → motive_1 t) →
                  ((t : Lean.PersistentArray Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_1 t → motive_2 t) →
                    ((t : Lean.PersistentArrayNode Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_2 t → motive_3 t) →
                      ((t : Array Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_3 t → motive_4 t) →
                        ((t : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree)) →
                            Lean.Elab.InfoTree.below_4 t → motive_5 t) →
                          ((t : List Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_5 t → motive_6 t) →
                            ((t : List (Lean.PersistentArrayNode Lean.Elab.InfoTree)) →
                                Lean.Elab.InfoTree.below_6 t → motive_7 t) →
                              motive_5 t ×' Lean.Elab.InfoTree.below_4 t
-- Mathlib.Order.ModularLattice
inf_lt_inf_of_lt_of_sup_le_sup : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {x y z : α}, x < y → y ⊔ z ≤ x ⊔ z → x ⊓ z < y ⊓ z
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.isChain_adj_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), List.IsChain G.Adj p.support
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.instHasProductOppositeOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C}
  [CategoryTheory.Limits.HasCoproduct Z], CategoryTheory.Limits.HasProduct fun x => Opposite.op (Z x)
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.State.mk.inj : ∀ {count : ℕ} {results : Std.HashMap Lean.ExprStructEq Lean.Meta.LetToHave.Result✝} {count_1 : ℕ}
  {results_1 : Std.HashMap Lean.ExprStructEq Lean.Meta.LetToHave.Result✝},
  { count := count, results := results } = { count := count_1, results := results_1 } →
    count = count_1 ∧ results = results_1
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.blockTriangular_blockDiagonal : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} [inst : Preorder α] [inst_1 : Zero R] [inst_2 : DecidableEq α]
  (d : α → Matrix m m R), (Matrix.blockDiagonal d).BlockTriangular Prod.snd
-- Mathlib.Order.Heyting.Basic
/-- A generalized co-Heyting algebra is a lattice with an additional binary
difference operation `\` such that `(· \ a)` is left adjoint to `(· ⊔ a)`.

This generalizes `CoheytingAlgebra` by not requiring a top element.  -/
GeneralizedCoheytingAlgebra : Type u_4 → Type u_4
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.normalizationPullback.eq_1 : ∀ {X S Y : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f],
  AlgebraicGeometry.Scheme.Hom.normalizationPullback f g =
    AlgebraicGeometry.Scheme.Hom.normalizationDesc (CategoryTheory.Limits.pullback.snd f g)
      (CategoryTheory.Limits.pullback.map f g (AlgebraicGeometry.Scheme.Hom.fromNormalization f) g
        (AlgebraicGeometry.Scheme.Hom.toNormalization f) (CategoryTheory.CategoryStruct.id Y)
        (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
      (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Hom.fromNormalization f) g) ⋯
-- Init.Data.BitVec.Basic
/-- Returns the most significant bit in a bitvector.  -/
BitVec.msb : {n : ℕ} → BitVec n → Bool
-- Lean.Elab.Command
Lean.Elab.Command.instMonadTraceCommandElabM : Lean.MonadTrace Lean.Elab.Command.CommandElabM
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The 2-cocycles `Z²(G, A)` of `A : Rep k G`, defined as the kernel of the map
`Fun(G × G, A) → Fun(G × G × G, A)` sending
`(f, (g₁, g₂, g₃)) ↦ ρ_A(g₁)(f(g₂, g₃)) - f(g₁g₂, g₃) + f(g₁, g₂g₃) - f(g₁, g₂).`  -/
groupCohomology.cocycles₂ : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → (A : Rep.{u_1, u, u} k G) → Submodule k (G × G → ↑A)
-- Mathlib.Topology.Order.LeftRight
nhdsWithinLT_sup_nhdsWithinGE : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] {s : Set α} (a : α),
  nhdsWithin a (s ∩ Set.Iio a) ⊔ nhdsWithin a (s ∩ Set.Ici a) = nhdsWithin a s
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.bot_toSubalgebra : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E], ⊥.toSubalgebra = ⊥
-- Batteries.Data.BitVec.Lemmas
/-- **Alias** of `BitVec.getMsb_ofFnBE`. -/
BitVec.getMsb'_ofFnBE : ∀ {n : ℕ} (f : Fin n → Bool) (i : Fin n), (BitVec.ofFnBE f).getMsb i = f i
-- Mathlib.InformationTheory.Hamming
Hamming.norm_eq_hammingNorm : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
  [inst_2 : (i : ι) → Zero (β i)] (x : Hamming β), ‖x‖ = ↑(hammingNorm (Hamming.ofHamming x))
-- Mathlib.Combinatorics.SimpleGraph.Prod
/-- Turn a walk on `G` into a walk on `G □ H`.  -/
SimpleGraph.Walk.boxProdLeft : {α : Type u_1} →
  {β : Type u_2} →
    {G : SimpleGraph α} → (H : SimpleGraph β) → {a₁ a₂ : α} → (b : β) → G.Walk a₁ a₂ → (G □ H).Walk (a₁, b) (a₂, b)
-- Init.Data.List.Sublist
List.isPrefixOf_cons_cons_self : ∀ {α : Type u_1} [inst : BEq α] {as bs : List α} [LawfulBEq α] {a : α},
  (a :: as).isPrefixOf (a :: bs) = as.isPrefixOf bs
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Fork.op_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Fork f g), c.op.π = c.ι.op
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.preimage_ae_eq : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β} {s t : Set β},
  MeasureTheory.Measure.QuasiMeasurePreserving f μa μb → s =ᵐ[μb] t → f ⁻¹' s =ᵐ[μa] f ⁻¹' t
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.IsMarkovKernel.compProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel κ]
  (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsMarkovKernel η],
  ProbabilityTheory.IsMarkovKernel (κ.compProd η)
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_one_add : ∀ (a b : Ordinal.{u_1}), a ^ (1 + b) = a * a ^ b
-- Mathlib.Algebra.Group.Units.Basic
instUniqueUnitsOfSubsingleton.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : Subsingleton M],
  instUniqueUnitsOfSubsingleton = { toInhabited := Units.instInhabited, uniq := ⋯ }
-- Batteries.Data.List.Basic
/-- `product l₁ l₂` is the list of pairs `(a, b)` where `a ∈ l₁` and `b ∈ l₂`.
```
product [1, 2] [5, 6] = [(1, 5), (1, 6), (2, 5), (2, 6)]
```
 -/
List.product : {α : Type u_1} → {β : Type u_2} → List α → List β → List (α × β)
-- Mathlib.Data.Part
Part.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (Dom : Prop) (get : Dom → α), sizeOf { Dom := Dom, get := get } = 1 + sizeOf Dom
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.HasInjectiveResolutions.out : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroObject C}
  {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} [self : CategoryTheory.HasInjectiveResolutions C] (Z : C),
  CategoryTheory.HasInjectiveResolution Z
-- Mathlib.AlgebraicGeometry.Birational.Composition
AlgebraicGeometry.Scheme.RationalMap.instIsDominantComp : ∀ {X Y Z : AlgebraicGeometry.Scheme} [inst : PreirreducibleSpace ↥X] [inst_1 : Nonempty ↥Y] (f : X.RationalMap Y)
  [inst_2 : f.IsDominant] (g : Y.RationalMap Z) [g.IsDominant], (f.comp g).IsDominant
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.coe_smul : ∀ {M : Type u_2} {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Monoid M] [inst_2 : DistribMulAction M α]
  [inst_3 : SMulCommClass M α α] [inst_4 : IsScalarTower M α α] (n : M) (f : CentroidHom α), ⇑(n • f) = n • ⇑f
-- Mathlib.Algebra.Group.Action.Defs
smul_eq_mul : ∀ {α : Type u_9} [inst : Mul α] (a b : α), a • b = a * b
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- The identity partial isomorphism on `X`, defined on all of `X`.  -/
AlgebraicGeometry.Scheme.PartialIso.refl : (X : AlgebraicGeometry.Scheme) → X.PartialIso X
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.instHasLimitWalkingCospanCospan : ∀ {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g],
  CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Syntax.decodeOctalLitAux : String → String.Pos.Raw → ℕ → Option ℕ