mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ComplexShapeSigns
TotalComplexShape.mk : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₁₂ : Type u_4} →
      {c₁ : ComplexShape I₁} →
        {c₂ : ComplexShape I₂} →
          {c₁₂ : ComplexShape I₁₂} →
            (π : I₁ × I₂ → I₁₂) →
              (ε₁ ε₂ : I₁ × I₂ → ℤˣ) →
                (∀ {i₁ i₁' : I₁}, c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), c₁₂.Rel (π (i₁, i₂)) (π (i₁', i₂))) →
                  (∀ (i₁ : I₁) {i₂ i₂' : I₂}, c₂.Rel i₂ i₂' → c₁₂.Rel (π (i₁, i₂)) (π (i₁, i₂'))) →
                    (∀ {i₁ i₁' : I₁} {i₂ i₂' : I₂},
                        c₁.Rel i₁ i₁' → c₂.Rel i₂ i₂' → ε₂ (i₁, i₂) * ε₁ (i₁, i₂') = -ε₁ (i₁, i₂) * ε₂ (i₁', i₂)) →
                      TotalComplexShape c₁ c₂ c₁₂
-- Mathlib.Topology.Constructions
ContinuousMap.uliftEquiv_apply_apply : ∀ (X : Type u) (Y : Type v) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (f : C(ULift.{v, u} X, ULift.{u, v} Y)) (a : X), ((ContinuousMap.uliftEquiv X Y) f) a = (ULift.down ∘ ⇑f ∘ ULift.up) a
-- Mathlib.CategoryTheory.Sites.Sieves
/-- a morphism in the presieve `S`  -/
CategoryTheory.Presieve.BindStruct.f : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      {S : CategoryTheory.Presieve X} →
        {R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Presieve Y} →
          {Z : C} → {h : Z ⟶ X} → (self : S.BindStruct R h) → self.Y ⟶ X
-- Mathlib.Order.Interval.Set.Basic
Set.Iic_sdiff_right : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α}, Set.Iic a \ {a} = Set.Iio a
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
/-- If `X : Truncated 2` has a unique `0`-simplex and (at most) one `1`-simplex,
this is the isomorphism `Cat.of X.HomotopyCategory ≅ Cat.chosenTerminal` in `Cat`.  -/
SSet.Truncated.HomotopyCategory.isoTerminal : (X : SSet.Truncated 2) →
  [Unique (X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 }))] →
    [Subsingleton
          (X.obj
            (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.HomotopyCategory.isoTerminal._proof_1 }))] →
      CategoryTheory.Cat.of X.HomotopyCategory ≅ CategoryTheory.Cat.chosenTerminal
-- Mathlib.Probability.Independence.Kernel.IndepFun
/-- **Alias** of `ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetSum_of_notMem₀`. -/
ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_sum_of_notMem₀ : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β}
  [inst : AddCommMonoid β] [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ)) →
      ∀ {s : Finset ι} {i : ι}, i ∉ s → ProbabilityTheory.Kernel.IndepFun (∑ j ∈ s, f j) (f i) κ μ
-- Mathlib.RingTheory.MvPowerSeries.GaussNorm
MvPowerSeries.gaussNorm_mul_le : ∀ {R : Type u_1} {σ : Type u_2} (v : R → ℝ) (c : σ → ℝ) [inst : Semiring R] (f g : MvPowerSeries σ R),
  0 ≤ c →
    (∀ (a : R), v a ≥ 0) →
      (∀ (a b : R), v (a * b) ≤ v a * v b) →
        IsNonarchimedean v →
          v 0 = 0 →
            MvPowerSeries.HasGaussNorm v c f →
              MvPowerSeries.HasGaussNorm v c g →
                MvPowerSeries.gaussNorm v c (f * g) ≤ MvPowerSeries.gaussNorm v c f * MvPowerSeries.gaussNorm v c g
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.toList_toArray_eq_toList : ∀ {α : Type u} {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (Std.DHashMap.Raw.Const.toArray ↑m).toList = Std.DHashMap.Raw.Const.toList ↑m
-- Mathlib.Algebra.Order.Module.Defs
lt_of_smul_lt_smul_right : ∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero β] [SMulPosReflectLT α β], a₁ • b < a₂ • b → 0 ≤ b → a₁ < a₂
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.equiv'_toAlgHom : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (g : Polynomial R)
  (pb : PowerBasis R S) (h₁ : (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0)
  (h₂ : (Polynomial.aeval pb.gen) g = 0),
  ↑(AdjoinRoot.equiv' g pb h₁ h₂) = AdjoinRoot.liftAlgHom g (Algebra.ofId R S) pb.gen h₂
-- Aesop.Util.UnorderedArraySet
Aesop.UnorderedArraySet.instToFormat : {α : Type u_1} → [inst : BEq α] → [Std.ToFormat α] → Std.ToFormat (Aesop.UnorderedArraySet α)
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.BoundedFormula.castLE.match_1.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x x_1 : ℕ) → x ≤ x_1 → L.BoundedFormula α x → Sort u_4)
  (_m _n : ℕ) (_h : _m ≤ _n)
  (h_1 : (_m _n : ℕ) → (_h : _m ≤ _n) → motive _m _n _h FirstOrder.Language.BoundedFormula.falsum)
  (h_2 :
    (_m _n : ℕ) →
      (h : _m ≤ _n) → (t₁ t₂ : L.Term (α ⊕ Fin _m)) → motive _m _n h (FirstOrder.Language.BoundedFormula.equal t₁ t₂))
  (h_3 :
    (_m _n : ℕ) →
      (h : _m ≤ _n) →
        (l : ℕ) →
          (R : L.Relations l) →
            (ts : Fin l → L.Term (α ⊕ Fin _m)) → motive _m _n h (FirstOrder.Language.BoundedFormula.rel R ts))
  (h_4 : (_m _n : ℕ) → (h : _m ≤ _n) → (f₁ f₂ : L.BoundedFormula α _m) → motive _m _n h (f₁.imp f₂))
  (h_5 : (_m _n : ℕ) → (h : _m ≤ _n) → (f : L.BoundedFormula α (_m + 1)) → motive _m _n h f.all),
  (match _m, _n, _h, FirstOrder.Language.BoundedFormula.falsum with
    | _m, _n, _h, FirstOrder.Language.BoundedFormula.falsum => h_1 _m _n _h
    | _m, _n, h, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => h_2 _m _n h t₁ t₂
    | _m, _n, h, FirstOrder.Language.BoundedFormula.rel R ts => h_3 _m _n h l R ts
    | _m, _n, h, f₁.imp f₂ => h_4 _m _n h f₁ f₂
    | _m, _n, h, f.all => h_5 _m _n h f) =
    h_1 _m _n _h
-- Mathlib.Data.Multiset.UnionInter
/-- **Alias** of the forward direction of `Multiset.disjoint_left`. -/
Disjoint.notMem_of_mem_left_multiset : ∀ {α : Type u_1} {s t : Multiset α}, Disjoint s t → ∀ {a : α}, a ∈ s → a ∉ t
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.map_eq_zero_iff : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {p : Polynomial R}, h.map p = 0 ↔ f ∣ p
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_le_iff : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f : MvPolynomial σ R} {d : σ →₀ ℕ},
  m.toSyn (m.degree f) ≤ m.toSyn d ↔ ∀ c ∈ f.support, m.toSyn c ≤ m.toSyn d
-- Lean.ResolveName
Lean.MonadResolveName : (Type → Type) → Type
-- Mathlib.Probability.Independence.Basic
/-- **Alias** of the forward direction of `ProbabilityTheory.iIndepFun_iff_measure_inter_preimage_eq_mul`. -/
ProbabilityTheory.iIndepFun.measure_inter_preimage_eq_mul : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_10} {β : ι → Type u_11}
  {m : (x : ι) → MeasurableSpace (β x)} {f : (i : ι) → Ω → β i},
  ProbabilityTheory.iIndepFun f μ →
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
      (∀ i ∈ S, MeasurableSet (sets i)) → μ (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, μ (f i ⁻¹' sets i)
-- Init.System.IO
/-- An entry in a directory on a filesystem.  -/
IO.FS.DirEntry : Type
-- Std.Data.TreeMap.Basic
/-- Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.
 -/
Std.TreeMap.modify : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → (β → β) → Std.TreeMap α β cmp
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcReleaseParams.uri : Lean.Lsp.RpcReleaseParams → Lean.Lsp.DocumentUri
-- Mathlib.Algebra.Order.Group.Synonym
ofLex_neg : ∀ {α : Type u_1} [inst : Neg α] (a : Lex α), ofLex (-a) = -ofLex a
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- The inner product of a nonzero vector with a positive multiple of
itself, divided by the product of their norms, has value 1.  -/
real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x : F} {r : ℝ},
  x ≠ 0 → 0 < r → inner ℝ x (r • x) / (‖x‖ * ‖r • x‖) = 1
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.VersoModuleDocs.DocContext.priorParts : Lean.VersoModuleDocs.DocContext✝ → Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty)
-- Init.PropLemmas
Bool.dite_then_false_eq_false : ∀ {p : Prop} [inst : Decidable p] {x : ¬p → Bool}, (if h : p then false else x h) = false ↔ ∀ (h : ¬p), x h = false
-- Init.Prelude
/-- A combined state and exception monad in which exceptions do not automatically roll back the state.

Instances of `EStateM.Backtrackable` provide a way to roll back some part of the state if needed.

`EStateM ε σ` is equivalent to `ExceptT ε (StateM σ)`, but it is more efficient.
 -/
EStateM : Type u → Type u → Type u → Type u
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
unitInterval.sigmoid_strictMono : StrictMono unitInterval.sigmoid
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.LeftHomotopy.compRightId_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} {f : u ⟶ u}
  (h : CategoryTheory.Arrow.LeftHomotopy f (CategoryTheory.CategoryStruct.id u)) (g : u ⟶ v),
  (h.compRightId g).hom = CategoryTheory.CategoryStruct.comp h.hom (CategoryTheory.Arrow.Hom.left g)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.LimitCone.mk.injEq : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} (cone : CategoryTheory.Limits.Cone F) (isLimit : CategoryTheory.Limits.IsLimit cone)
  (cone_1 : CategoryTheory.Limits.Cone F) (isLimit_1 : CategoryTheory.Limits.IsLimit cone_1),
  ({ cone := cone, isLimit := isLimit } = { cone := cone_1, isLimit := isLimit_1 }) =
    (cone = cone_1 ∧ isLimit ≍ isLimit_1)
-- Mathlib.NumberTheory.Cyclotomic.Basic
instInhabitedCyclotomicField : (n : ℕ) → (K : Type u_1) → [inst : Field K] → Inhabited (CyclotomicField n K)
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.group : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {I : ModelWithCorners 𝕜 E H} →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    {G : Type u_10} →
                                      [inst_9 : Group G] →
                                        [inst_10 : TopologicalSpace G] →
                                          [inst_11 : ChartedSpace H' G] →
                                            [LieGroup I' n G] → Group (ContMDiffMap I I' N G n)
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_29 : HAdd Std.Time.Hour.Offset Std.Time.Week.Offset Std.Time.Hour.Offset
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.Term.card_sigma : ∀ {L : FirstOrder.Language} {α : Type u'},
  Cardinal.mk ((n : ℕ) × L.Term (α ⊕ Fin n)) = max Cardinal.aleph0 (Cardinal.mk (α ⊕ (i : ℕ) × L.Functions i))
-- Mathlib.Analysis.InnerProductSpace.Affine
/-- **Pythagorean theorem**: if `p -ᵥ a` is orthogonal to `b -ᵥ a`, then
`dist p b ^ 2 = dist p a ^ 2 + dist a b ^ 2`.  -/
dist_sq_of_inner_eq_zero : ∀ {V : Type u_2} {P : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b p : P}, inner ℝ (p -ᵥ a) (b -ᵥ a) = 0 → dist p b ^ 2 = dist p a ^ 2 + dist a b ^ 2
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The short complex `(G² →₀ A) --d₂₁--> (G →₀ A) --d₁₀--> A` is isomorphic to the 1st
short complex associated to the complex of inhomogeneous chains of `A`.  -/
groupHomology.isoShortComplexH1 : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) →
        HomologicalComplex.sc (groupHomology.inhomogeneousChains A) 1 ≅ groupHomology.shortComplexH1 A
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.isExtrOn_T_real : ∀ {n k : ℕ},
  n ≠ 0 →
    k ≤ n →
      IsExtrOn (fun x => Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n)) (Set.Icc (-1) 1)
        (Real.cos (↑k * Real.pi / ↑n))
-- Init.Data.UInt.Lemmas
UInt8.toUInt32_le : ∀ {a b : UInt8}, a.toUInt32 ≤ b.toUInt32 ↔ a ≤ b
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.XIso.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i : ι) (hi : ¬c.Rel i (c.next i)),
  HomologicalComplex.homotopyCofiber.XIso φ i hi = HomologicalComplex.homotopyCofiber.XIso φ i hi
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_mul_X : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, (p * Polynomial.X).leadingCoeff = p.leadingCoeff
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.rfind'.sizeOf_spec : ∀ (a : Nat.Partrec.Code), sizeOf a.rfind' = 1 + sizeOf a
-- Lean.Parser.Basic
Lean.Parser.ParserCategory.mk.injEq : ∀ (declName : Lean.Name) (kinds : Lean.Parser.SyntaxNodeKindSet) (tables : Lean.Parser.PrattParsingTables)
  (behavior : Lean.Parser.LeadingIdentBehavior) (declName_1 : Lean.Name) (kinds_1 : Lean.Parser.SyntaxNodeKindSet)
  (tables_1 : Lean.Parser.PrattParsingTables) (behavior_1 : Lean.Parser.LeadingIdentBehavior),
  ({ declName := declName, kinds := kinds, tables := tables, behavior := behavior } =
      { declName := declName_1, kinds := kinds_1, tables := tables_1, behavior := behavior_1 }) =
    (declName = declName_1 ∧ kinds = kinds_1 ∧ tables = tables_1 ∧ behavior = behavior_1)
-- Mathlib.Order.Filter.Pointwise
Filter.vadd_le_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f₁ f₂ : Filter α} {g₁ g₂ : Filter β},
  f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ +ᵥ g₁ ≤ f₂ +ᵥ g₂
-- Mathlib.Util.TermReduce
/-- `zeta% t` elaborates to a zeta and zeta-delta reduced version of `t`.  -/
Mathlib.Util.TermReduce.elabZeta : Lean.Elab.Term.TermElab
-- Mathlib.Algebra.Group.Pi.Basic
Pi.divInvOneMonoid : {I : Type u} → {f : I → Type v₁} → [(i : I) → DivInvOneMonoid (f i)] → DivInvOneMonoid ((i : I) → f i)
-- Mathlib.Probability.Process.Adapted
/-- **Alias** of `MeasureTheory.IsStronglyProgressive.inv`. -/
MeasureTheory.ProgMeasurable.inv : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u : ι → Ω → β} [inst_2 : MeasurableSpace ι] [inst_3 : Group β]
  [ContinuousInv β],
  MeasureTheory.IsStronglyProgressive f u → MeasureTheory.IsStronglyProgressive f fun i ω => (u i ω)⁻¹
-- Mathlib.Topology.ContinuousMap.Defs
/-- Deprecated. Use `DFunLike.congr_arg` instead.  -/
ContinuousMap.congr_arg : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y)) {x y : X},
  x = y → f x = f y
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.coe_prod : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {H : Type u_2} [inst_2 : AddGroup H]
  [inst_3 : TopologicalSpace H] (U : OpenAddSubgroup G) (V : OpenAddSubgroup H), ↑(U.prod V) = ↑U ×ˢ ↑V
-- Mathlib.Data.Seq.Computation
Computation.thinkN_terminates : ∀ {α : Type u} (s : Computation α) [s.Terminates] (n : ℕ), (s.thinkN n).Terminates
-- Lean.ExtraModUses
/-- Copies additional recorded import dependencies from one environment to another.  -/
Lean.copyExtraModUses : Lean.Environment → Lean.Environment → Lean.Environment
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_hom_actionHomLeft : ∀ {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.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {x y : D} (f : x ≅ y) (z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f.inv z)
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f.hom z) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj y z)
-- Init.Data.UInt.Bitwise
UInt64.ofBitVec_shiftRight_mod : ∀ (a : BitVec 64) (b : ℕ), { toBitVec := a >>> (b % 64) } = { toBitVec := a } >>> UInt64.ofNat b
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.top_prod_top : ∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M], ⊤.prod ⊤ = ⊤
-- Mathlib.Tactic.Bound.Attribute
/-- Insist that our conclusion is an inequality  -/
_private.Mathlib.Tactic.Bound.Attribute.0.Mathlib.Tactic.Bound.typePriority.checkResult : Lean.Name → Lean.Expr → Q(Prop) → Lean.MetaM Unit
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.coe_top : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜], ↑⊤ = Set.univ
-- Lean.Elab.Tactic.Try
/-- Returns `true` if `fvarId` has an accessible name.  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.isAccessible : Lean.FVarId → Lean.MetaM Bool
-- Mathlib.SetTheory.Ordinal.Notation
/-- Calculate division and remainder of `o` mod `ω`:

`split' o = (a, n)` means `o = ω * a + n`.  -/
ONote.split' : ONote → ONote × ℕ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonReferenceContext : Lean.FromJson Lean.Lsp.ReferenceContext
-- Std.Time.Format.Modifier
Std.Time.instReprText : Repr Std.Time.Text
-- Mathlib.GroupTheory.IsSubnormal
Subgroup.IsSubnormal.below.step : ∀ {G : Type u_1} [inst : Group G] {motive : (a : Subgroup G) → a.IsSubnormal → Prop} (H K : Subgroup G) (h_le : H ≤ K)
  (hSubn : K.IsSubnormal) (hN : (H.subgroupOf K).Normal),
  Subgroup.IsSubnormal.below hSubn → motive K hSubn → Subgroup.IsSubnormal.below ⋯
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.pow_nc_NonnegCoeffs : ∀ {p : Lean.Grind.CommRing.Poly} (k : ℕ), p.NonnegCoeffs → (p.pow_nc k).NonnegCoeffs
-- Mathlib.Algebra.Homology.Augment
CochainComplex.augment_d_succ_succ : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : CochainComplex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0) (i j : ℕ),
  (C.augment f w).d (i + 1) (j + 1) = C.d i j
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.nonempty_coeSort : ∀ {α : Type u_2} [inst : TopologicalSpace α] {U : TopologicalSpace.Opens α}, Nonempty ↥U ↔ (↑U).Nonempty
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inl_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ],
  (CochainComplex.mappingCone.inl φ).comp ↑(CochainComplex.mappingCone.fst φ) ⋯ =
    CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id F)
-- Mathlib.RingTheory.Etale.StandardEtale
Ideal.quotientEquivAlg.congr_simp : ∀ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A]
  [inst_3 : Ring B] [inst_4 : Algebra R₁ B] (I : Ideal A) (J : Ideal B) [inst_5 : I.IsTwoSided] [inst_6 : J.IsTwoSided]
  (f f_1 : A ≃ₐ[R₁] B) (e_f : f = f_1) (hIJ : J = Ideal.map (↑f) I),
  I.quotientEquivAlg J f hIJ = I.quotientEquivAlg J f_1 ⋯
-- Init.Data.List.Attach
_private.Init.Data.List.Attach.0.List.filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.symmCompOfNondegenerate.eq_1 : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : FiniteDimensional K V] (B₁ B₂ : LinearMap.BilinForm K V) (b₂ : B₂.Nondegenerate),
  B₁.symmCompOfNondegenerate B₂ b₂ = ↑(B₂.toDual b₂).symm ∘ₗ B₁
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
/-- The full subcategory where `F.partialRightAdjoint` shall be defined.  -/
CategoryTheory.Functor.PartialRightAdjointSource : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Type u₂
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.toPartialMap_hom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialIso Y),
  f.toPartialMap.hom = CategoryTheory.CategoryStruct.comp f.iso.hom f.target.ι
-- Mathlib.Order.Hom.WithTopBot
/-- Adjoins a `⊥` to the domain and codomain of a `SupHom`.  -/
SupHom.withBot : {α : Type u_1} →
  {β : Type u_2} →
    [inst : SemilatticeSup α] → [inst_1 : SemilatticeSup β] → SupHom α β → SupBotHom (WithBot α) (WithBot β)
-- Mathlib.Algebra.Category.ModuleCat.Colimits
ModuleCat.hasColimitsOfSize : ∀ (R : Type w) [inst : Ring R] [CategoryTheory.Limits.HasColimitsOfSize.{v, u, w', w' + 1} AddCommGrpCat],
  CategoryTheory.Limits.HasColimitsOfSize.{v, u, w', max (w' + 1) w} (ModuleCat R)
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_reindex : ∀ {m : Type um} {m₀ : Type um₀} {n : Type un} {n₀ : Type un₀} {R : Type uR} [inst : Fintype n] [inst_1 : Fintype n₀]
  [inst_2 : CommSemiring R] (em : m ≃ m₀) (en : n ≃ n₀) (A : Matrix m n R), ((Matrix.reindex em en) A).rank = A.rank
-- Mathlib.Analysis.Normed.Group.HomCompletion
NormedAddCommGroup.denseRange_toCompl : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G], DenseRange ⇑NormedAddCommGroup.toCompl
-- Init.Data.Array.Zip
Array.lt_size_right_of_zip : ∀ {α : Type u_1} {β : Type u_2} {i : ℕ} {as : Array α} {bs : Array β}, i < (as.zip bs).size → i < bs.size
-- Mathlib.Tactic.Linter.PPRoundtrip
/-- The "ppRoundtrip" linter emits a warning when the syntax of a command differs substantially
from the pretty-printed version of itself.

The linter makes an effort to start the highlighting at the first difference.
However, it may not always be successful.
It also prints both the source code and the "expected code" in a 5-character radius from
the first difference.
 -/
Mathlib.Linter.linter.ppRoundtrip : Lean.Option Bool
-- Mathlib.Data.Real.ConjExponents
Real.HolderConjugate.symm : ∀ {p q : ℝ}, p.HolderConjugate q → q.HolderConjugate p
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- For `f : ℕ → G`, the product `∏' k, f (k + i)` tends to one. This does not require a
multipliability assumption on `f`, as otherwise all such products are one.  -/
tendsto_prod_nat_add : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] (f : ℕ → G),
  Filter.Tendsto (fun i => ∏' (k : ℕ), f (k + i)) Filter.atTop (nhds 1)