mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.foldM_filterMapWithPostcondition : ∀ {α β γ δ : Type w} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : Monad o] [LawfulMonad n]
  [inst_5 : Std.Internal.Do.Assertion Pred] [inst_6 : Std.Internal.Do.Assertion EPred]
  [inst_7 : Std.Internal.Do.WPMonad o Pred EPred] [inst_8 : Std.IteratorLoop α Id n] [inst_9 : Std.IteratorLoop α Id o]
  [Std.LawfulIteratorLoop α Id n] [Std.LawfulIteratorLoop α Id o] [inst_12 : MonadLiftT n o] [LawfulMonadLiftT n o]
  {f : β → Std.Iterators.PostconditionT n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : Std.Iter β} {P : Pred}
  {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.Iter.foldM
        (fun d b => do
          let __x ← liftM (f b).run
          match __x with
            | some c => g d c
            | x => pure d)
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.foldM g init (Std.Iter.filterMapWithPostcondition f it) ⦃ Q; eQ ⦄
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkYonedaObjObjEquiv_obj_map_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X : C}
  {Y Y' : Cᵒᵖ} (g : Y ⟶ Y') (f : (CategoryTheory.shrinkYoneda.{w, v, u}.obj X).obj Y) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.shrinkYonedaObjObjEquiv
        ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkYoneda.{w, v, u}.obj X).map g)) f))
      h =
    CategoryTheory.CategoryStruct.comp g.unop
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkYonedaObjObjEquiv f) h)
-- Mathlib.Algebra.Order.Floor.Defs
Nat.ceil_le : ∀ {α : Type u_2} [inst : Semiring α] [inst_1 : PartialOrder α] [inst_2 : FloorSemiring α] {a : α} {n : ℕ},
  ⌈a⌉₊ ≤ n ↔ a ≤ ↑n
-- Mathlib.NumberTheory.ModularForms.Cusps
/-- Surjection from `SL(2, ℤ) / (𝒢 ⊓ SL(2, ℤ))` to cusp orbits of `𝒢`. Mostly useful for showing
that `CuspOrbits 𝒢` is finite for arithmetic subgroups.  -/
cosetToCuspOrbit : (𝒢 : Subgroup (GL (Fin 2) ℝ)) →
  [𝒢.IsArithmetic] →
    Matrix.SpecialLinearGroup (Fin 2) ℤ ⧸ Subgroup.comap (Matrix.SpecialLinearGroup.mapGL ℝ) 𝒢 → CuspOrbits 𝒢
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.widePushout.congr_simp : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C) (objs : J → C)
  (arrows arrows_1 : (j : J) → B ⟶ objs j) (e_arrows : arrows = arrows_1)
  [inst_1 : CategoryTheory.Limits.HasWidePushout B objs arrows],
  CategoryTheory.Limits.widePushout B objs arrows = CategoryTheory.Limits.widePushout B objs arrows_1
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_filter_containsKey_of_containsKey_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α}
  {fallback : β k},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = false →
      Std.Internal.List.getValueCastD k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) fallback =
        fallback
-- Mathlib.Logic.Function.Basic
Function.instTrichotomousSwapProp : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Trichotomous r], Std.Trichotomous (Function.swap r)
-- Std.Async.Process
/-- Number of signals received
 -/
Std.IO.Process.ResourceUsageStats.signalsReceived : Std.IO.Process.ResourceUsageStats → UInt64
-- Batteries.Data.List.Lemmas
List.chain_succ_range' : ∀ (s n step : ℕ), List.IsChain (fun a b => b = a + step) (s :: List.range' (s + step) n step)
-- Mathlib.Order.Filter.IsBounded
Filter.IsBoundedUnder.le_of_finite : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [Nonempty α] [IsDirectedOrder α] [Finite β] {f : Filter β}
  {u : β → α}, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minView.match_3.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (r : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (l : Std.DTreeMap.Internal.Impl α β) →
      l.Balanced → Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size → Sort u_3)
  (size : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
  (hl : (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').Balanced)
  (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').size r.size)
  (h_1 :
    (hl : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot Std.DTreeMap.Internal.Impl.leaf.size r.size) →
        motive Std.DTreeMap.Internal.Impl.leaf hl hlr)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l' r' : Std.DTreeMap.Internal.Impl α β) →
            (hl : (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').size
                    r.size) →
                motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') hl hlr),
  (match Std.DTreeMap.Internal.Impl.inner size k' v' l' r', hl, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hl, hlr => h_1 hl hlr
    | Std.DTreeMap.Internal.Impl.inner size k' v' l' r', hl, hlr => h_2 size k' v' l' r' hl hlr) =
    h_2 size k' v' l' r' hl hlr
-- Mathlib.GroupTheory.Complement
AddSubgroup.exists_isComplement_right : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) (g : G), ∃ T, AddSubgroup.IsComplement (↑H) T ∧ g ∈ T
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- Laplacian expansion of the determinant of an `n+1 × n+1` matrix along column 0.  -/
Matrix.det_succ_column_zero : ∀ {R : Type v} [inst : CommRing R] {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R),
  A.det = ∑ i, (-1) ^ ↑i * A i 0 * (A.submatrix i.succAbove Fin.succ).det
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.mk.sizeOf_spec : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} [inst_2 : SizeOf J] [inst_3 : SizeOf C] (pt : C)
  (π : (j : J) → pt ⟶ F j) (ι : (j : J) → F j ⟶ pt)
  (ι_π :
    autoParam
      (∀ (j j' : J),
        CategoryTheory.CategoryStruct.comp (ι j) (π j') = if h : j = j' then CategoryTheory.eqToHom ⋯ else 0)
      CategoryTheory.Limits.Bicone.ι_π._autoParam),
  sizeOf { pt := pt, π := π, ι := ι, ι_π := ι_π } = 1 + sizeOf pt
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t t_1 : Std.TreeMap α β cmp) (e_t : t = t_1) (a a_1 : α)
  (e_a : a = a_1) (h : a ∈ t), t.get a h = t_1.get a_1 ⋯
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.IsHermitian.smul : ∀ {α : Type u_1} {n : Type u_4} {R : Type u_5} [inst : Star R] [inst_1 : Star α] [inst_2 : SMul R α] [StarModule R α]
  {A : Matrix n n α}, A.IsHermitian → ∀ {k : R}, IsSelfAdjoint k → (k • A).IsHermitian
-- Mathlib.Algebra.Lie.Basic
/-- A Lie ring is an additive group with compatible product, known as the bracket, satisfying the
Jacobi identity.  -/
LieRing : Type v → Type v
-- Std.Data.DTreeMap.Basic
/-- Returns the `n`-th smallest key.  -/
Std.DTreeMap.keyAtIdx : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → (t : Std.DTreeMap α β cmp) → (n : ℕ) → n < t.size → α
-- Mathlib.Tactic.Linarith.Datatypes
/-- `c.coeffOf a` projects the coefficient of variable `a` out of `c`.  -/
Mathlib.Tactic.Linarith.Comp.coeffOf : Mathlib.Tactic.Linarith.Comp → ℕ → ℤ
-- Mathlib.Order.WithBot
WithTop.untopD_coe : ∀ {α : Type u_5} (d x : α), WithTop.untopD d ↑x = x
-- Init.Data.Array.Monadic
_private.Init.Data.Array.Monadic.0.Array.forIn'_eq_foldlM.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (b : ForInStep β) → ((b : β) → motive (ForInStep.yield b)) → ((b : β) → motive (ForInStep.done b)) → motive b
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.mk.injEq : ∀ {α : Type u_6} [inst : NonUnitalNonAssocSemiring α] (toAddMonoidHom : α →+ α)
  (map_mul_left' : ∀ (a b : α), (↑toAddMonoidHom).toFun (a * b) = a * (↑toAddMonoidHom).toFun b)
  (map_mul_right' : ∀ (a b : α), (↑toAddMonoidHom).toFun (a * b) = (↑toAddMonoidHom).toFun a * b)
  (toAddMonoidHom_1 : α →+ α)
  (map_mul_left'_1 : ∀ (a b : α), (↑toAddMonoidHom_1).toFun (a * b) = a * (↑toAddMonoidHom_1).toFun b)
  (map_mul_right'_1 : ∀ (a b : α), (↑toAddMonoidHom_1).toFun (a * b) = (↑toAddMonoidHom_1).toFun a * b),
  ({ toAddMonoidHom := toAddMonoidHom, map_mul_left' := map_mul_left', map_mul_right' := map_mul_right' } =
      { toAddMonoidHom := toAddMonoidHom_1, map_mul_left' := map_mul_left'_1, map_mul_right' := map_mul_right'_1 }) =
    (toAddMonoidHom = toAddMonoidHom_1)
-- Init.Data.Array.Monadic
List.filterMapM_toArray : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {l : List α}
  {f : α → m (Option β)}, Array.filterMapM f l.toArray = List.toArray <$> List.filterMapM f l
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- A `SignedMeasure` is an `ℝ`-vector measure.  -/
MeasureTheory.SignedMeasure : (α : Type u_3) → [MeasurableSpace α] → Type (max u_3 0)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.min.congr_simp : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x x_1 : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N)
  (e_x : x = x_1) {d : ℕ} (hd : x.dim = d),
  SSet.prodStdSimplex.pairingCore.min x hd = SSet.prodStdSimplex.pairingCore.min x_1 ⋯
-- Std.Data.TreeSet.Basic
/-- Tries to retrieve the smallest element that is greater than the given element,
panicking if no such element exists.
 -/
Std.TreeSet.getGT! : {α : Type u} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeSet α cmp → α → α
-- Mathlib.Data.Finset.NAry
Finset.image₂_singleton_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {b : β},
  Finset.image₂ f s {b} = Finset.image (fun a => f a b) s
-- Init.Grind.Module.Basic
/-- We say a module has no natural number zero divisors if
`k ≠ 0` and `k * a = k * b` implies `a = b` (here `k` is a natural number and `a` and `b` are element of the module).

For a module over the integers this is equivalent to
`k ≠ 0` and `k * a = 0` implies `a = 0`.
(See the alternative constructor `NoNatZeroDivisors.mk'`,
and the theorem `eq_zero_of_mul_eq_zero`.)
 -/
Lean.Grind.NoNatZeroDivisors : (α : Type u) → [Lean.Grind.NatModule α] → Prop
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.stieltjesOfMeasurableRat_le_one : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : Measurable f) (a : α) (x : ℝ),
  ↑(ProbabilityTheory.stieltjesOfMeasurableRat f hf a) x ≤ 1
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_obj₂ : ∀ {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]
  (t : CategoryTheory.Triangulated.TStructure C) (i : EInt) (j : C), ((t.eTriangleLTGE.obj i).obj j).obj₂ = j
-- Init.Data.List.Lemmas
List.leftpad_prefix : ∀ {α : Type u_1} {n : ℕ} {a : α} {l : List α}, List.replicate (n - l.length) a <+: List.leftpad n a l
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₂₃_p₂_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C}
  (h_1 : X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.p₂₃ (CategoryTheory.CategoryStruct.comp h₂₃.p₁ h_1) =
    CategoryTheory.CategoryStruct.comp h.p₂ h_1
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instCreatesColimitsOfShapeSchemeLocallyRingedSpaceDiscreteForgetToLocallyRingedSpaceOfSmall : {σ : Type v} →
  [Small.{u, v} σ] →
    CategoryTheory.CreatesColimitsOfShape (CategoryTheory.Discrete σ)
      AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace
-- Lean.Util.LeanOptions
Lean.LeanOptions.mk.injEq : ∀ (values values_1 : Lean.NameMap Lean.LeanOptionValue),
  ({ values := values } = { values := values_1 }) = (values = values_1)
-- Aesop.Tree.Data
Aesop.Goal.setFailedRapps : Array Aesop.RegularRule → Aesop.Goal → Aesop.Goal
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
/-- The natural map from a nonsingular Jacobian point representative on a Weierstrass curve to its
corresponding nonsingular point in affine coordinates.  -/
WeierstrassCurve.Jacobian.Point.toAffine : {F : Type u} → [inst : Field F] → (W : WeierstrassCurve.Jacobian F) → (Fin 3 → F) → W.toAffine.Point
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_lt_inv_mul₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b : G₀},
  0 < a → (1 < a⁻¹ * b ↔ a < b)
-- Lean.Data.JsonRpc
/-- A JSON-RPC message.

Uses separate constructors for notifications and errors because client and server
behavior is expected to be wildly different for both.
 -/
Lean.JsonRpc.Message : Type
-- Mathlib.Data.Finset.Sym
Finset.eq_empty_of_sym_eq_empty : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α] {n : ℕ}, s.sym n = ∅ → s = ∅
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
CategoryTheory.Limits.Concrete.colimit_exists_of_rep_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type s}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {J : Type w}
  [inst_3 : CategoryTheory.Category.{r, w} J] (F : CategoryTheory.Functor J C)
  [CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)] [CategoryTheory.IsFiltered J]
  [inst_6 : CategoryTheory.Limits.HasColimit F] {i j : J} (x : CategoryTheory.ToType (F.obj i))
  (y : CategoryTheory.ToType (F.obj j)),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F i)) x =
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) y →
    ∃ k f g, (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map g)) y
-- Plausible.Functions
/-- Create a `Finmap` from a list of pairs.  -/
Plausible.TotalFunction.List.toFinmap' : {α : Type u} → {β : Type v} → List (α × β) → List ((_ : α) × β)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_modify_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ [inst_1 : Inhabited α] {k : α} {f : β k → β k},
      (Std.DTreeMap.Internal.Impl.modify k f t).getKey! k = if k ∈ t then k else default
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Ioc : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a b : ι → α},
  Filter.Tendsto a l Filter.atBot →
    Filter.Tendsto b l Filter.atTop → ∀ [NoMinOrder α], MeasureTheory.AECover μ l fun i => Set.Ioc (a i) (b i)
-- Std.Async.Process
/-- Gets the current process id.
 -/
Std.IO.Process.getId : IO Std.IO.Process.PId
-- Mathlib.LinearAlgebra.Projection
Submodule.coe_isComplEquivProj_symm_apply : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (p : Submodule R E)
  (f : { f // ∀ (x : ↥p), f ↑x = x }), ↑(p.isComplEquivProj.symm f) = (↑f).ker
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndep.of_precomp : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m : ι → MeasurableSpace Ω}
  {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {ι' : Type u_5}
  {g : ι' → ι},
  Function.Surjective g → ProbabilityTheory.Kernel.iIndep (m ∘ g) κ μ → ProbabilityTheory.Kernel.iIndep m κ μ
-- Init.Data.String.Decode
ByteArray.isSome_utf8DecodeChar?_append : ∀ {b : ByteArray} {i : ℕ},
  (b.utf8DecodeChar? i).isSome = true → ∀ (b' : ByteArray), ((b ++ b').utf8DecodeChar? i).isSome = true
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- Building a `C^n` manifold from a `HasGroupoid` assumption.  -/
IsManifold.mk' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞)
  (M : Type u_4) [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [gr : HasGroupoid M (contDiffGroupoid n I)],
  IsManifold I n M
-- Mathlib.AlgebraicGeometry.Sites.ElladicCohomology
/-- `ℓ`-adic cohomology is trivial for the empty scheme.  -/
AlgebraicGeometry.Scheme.instSubsingletonEllAdicCohomologyOfIsEmptyCarrierCarrierCommRingCat : ∀ (X : AlgebraicGeometry.Scheme) (ℓ : ℕ) [inst : Fact (Nat.Prime ℓ)] [IsEmpty ↥X] (n : ℕ),
  Subsingleton (X.EllAdicCohomology ℓ n)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Grind.Linarith.Poly.gcdCoeffs : Lean.Grind.Linarith.Poly → ℕ
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.nextCoeff_X_add_C : ∀ {S : Type v} [inst : Semiring S] (c : S), (Polynomial.X + Polynomial.C c).nextCoeff = c
-- Init.Data.String.Lemmas.Iter
Std.Iter.joinString_eq : ∀ {α β : Type} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : ToString β] {it : Std.Iter β},
  it.joinString = String.join (List.map toString it.toList)
-- Mathlib.Tactic.NormNum.RealSqrt
Mathlib.Meta.NormNum.isNat_realSqrt_neg : ∀ {x : ℝ} {nx : ℕ}, Mathlib.Meta.NormNum.IsInt x (Int.negOfNat nx) → Mathlib.Meta.NormNum.IsNat (√x) 0
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aevalTower_algebraMap : ∀ {R : Type u} {S : Type v} {A' : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring A'] [inst_2 : CommSemiring S]
  [inst_3 : Algebra S R] [inst_4 : Algebra S A'] (g : R →ₐ[S] A') (y : A') (x : R),
  (Polynomial.aevalTower g y) ((algebraMap R (Polynomial R)) x) = g x
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- Given an abelian group `M` with a `MulDistribMulAction` of `G`, and a function
`f : G × G → M` satisfying the multiplicative 2-coboundary condition, produces a
2-coboundary for the representation on `M` induced by the `MulDistribMulAction`.  -/
groupCohomology.coboundariesOfIsMulCoboundary₂ : {G M : Type} →
  [inst : Group G] →
    [inst_1 : CommGroup M] →
      [inst_2 : MulDistribMulAction G M] →
        {f : G × G → M} →
          groupCohomology.IsMulCoboundary₂ f → ↥(groupCohomology.coboundaries₂ (Rep.ofMulDistribMulAction G M))
-- Std.Time.Format
/-- The time12Hour format, which follows the pattern `hh:mm:ss aa` for representing time
in a 12-hour clock format with an upper case AM/PM marker.
 -/
Std.Time.Formats.time12Hour : Std.Time.GenericFormat Std.Time.Awareness.any
-- Mathlib.Algebra.Homology.Monoidal
/-- The inclusion `K₁.X i₁ ⊗ K₂.X i₂ ⟶ (tensorObj K₁ K₂).X j` of a summand in
the tensor product of the homological complexes.  -/
HomologicalComplex.ιTensorObj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        [inst_3 : (CategoryTheory.MonoidalCategory.curriedTensor C).Additive] →
          [inst_4 : ∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] →
            {I : Type u_2} →
              [inst_5 : AddMonoid I] →
                {c : ComplexShape I} →
                  [inst_6 : c.TensorSigns] →
                    [inst_7 : DecidableEq I] →
                      (K₁ K₂ : HomologicalComplex C c) →
                        [inst_8 : K₁.HasTensor K₂] →
                          (i₁ i₂ j : I) →
                            i₁ + i₂ = j →
                              (CategoryTheory.MonoidalCategoryStruct.tensorObj (K₁.X i₁) (K₂.X i₂) ⟶
                                (K₁.tensorObj K₂).X j)
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
_private.Mathlib.GroupTheory.SpecificGroups.Dihedral.0.instDecidableEqDihedralGroup.decEq.match_1.splitter : {n : ℕ} →
  (motive : DihedralGroup n → DihedralGroup n → Sort u_1) →
    (x x_1 : DihedralGroup n) →
      ((a b : ZMod n) → motive (DihedralGroup.r a) (DihedralGroup.r b)) →
        ((a a_1 : ZMod n) → motive (DihedralGroup.r a) (DihedralGroup.sr a_1)) →
          ((a a_1 : ZMod n) → motive (DihedralGroup.sr a) (DihedralGroup.r a_1)) →
            ((a b : ZMod n) → motive (DihedralGroup.sr a) (DihedralGroup.sr b)) → motive x x_1
-- Mathlib.Algebra.Order.Sub.Basic
tsub_eq_zero_iff_le : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b : α}, a - b = 0 ↔ a ≤ b
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.instInhabited : {E : Type u_1} → (c : E) → Inhabited (ContDiffBump c)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_ric_succ : ∀ {n : ℕ}, (*...=n + 1).toArray = (*...=n).toArray.push (n + 1)
-- Init.Data.Int.Order
Int.eq_succ_of_zero_lt : ∀ {a : ℤ}, 0 < a → ∃ n, a = ↑n + 1
-- Mathlib.Order.Interval.Set.Image
Monotone.image_Ici_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a : α},
  Monotone f → f '' Set.Ici a ⊆ Set.Ici (f a)
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.fromRows_inj : ∀ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5}, Function.Injective2 Matrix.fromRows
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.instIsConnectedCostructuredArrowStructuredArrowObjStructuredArrowDownwardsOfGuitartExact : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  [hw : w.GuitartExact] {X₂ : C₂} (g : CategoryTheory.StructuredArrow (R.obj X₂) B),
  CategoryTheory.IsConnected (CategoryTheory.CostructuredArrow (w.structuredArrowDownwards X₂) g)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.exists_prod_multiset_X_sub_C_mul : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (p : Polynomial R),
  ∃ q,
    (Multiset.map (fun a => Polynomial.X - Polynomial.C a) p.roots).prod * q = p ∧
      p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
/-- Eta-expanded form of `InnerProductSpace.HarmonicContOnCl.add` -/
InnerProductSpace.HarmonicContOnCl.fun_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f₁ f₂ : E → F} {s : Set E},
  InnerProductSpace.HarmonicContOnCl f₁ s →
    InnerProductSpace.HarmonicContOnCl f₂ s → InnerProductSpace.HarmonicContOnCl (fun i => f₁ i + f₂ i) s
-- Lean.Elab.Do.InferControlInfo
/-- The `ControlInfo` of a sequence `a; b`: effect flags are unioned, the regular exits are those of
`b`, and the sequence falls through iff both parts fall through.
 -/
Lean.Elab.Do.ControlInfo.sequence : Lean.Elab.Do.ControlInfo → Lean.Elab.Do.ControlInfo → Lean.Elab.Do.ControlInfo