mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.RightExtension.postcompose₂_obj_right : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor H D')
  (X : CategoryTheory.Comma ((CategoryTheory.Functor.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F)),
  ((CategoryTheory.Functor.RightExtension.postcompose₂ L F G).obj X).right = X.right
-- Mathlib.Data.List.Count
List.count_lt_length_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l : List α} {a : α}, List.count a l < l.length ↔ ∃ b ∈ l, b ≠ a
-- Mathlib.Algebra.Tropical.Basic
Tropical.trop_zero : ∀ {R : Type u} [inst : Zero R], Tropical.trop 0 = 1
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
/-- the bottom morphism of the pushout square  -/
HomotopicalAlgebra.AttachCells.g₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type t} →
      {A B : α → C} →
        {g : (a : α) → A a ⟶ B a} →
          {X₁ X₂ : C} → {f : X₁ ⟶ X₂} → (self : HomotopicalAlgebra.AttachCells g f) → self.cofan₂.pt ⟶ X₂
-- Std.Tactic.Do.Syntax
/-- `mclear` is like `clear`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (P Q : SPred σs) : P ⊢ₛ Q → Q := by
  mintro HP
  mintro HQ
  mclear HP
  mexact HQ
```
 -/
Lean.Parser.Tactic.mclearError : Lean.ParserDescr
-- Init.Data.Array.Lemmas
Array.getElem_extract_loop_lt_aux : ∀ {α : Type u_1} {i : ℕ} {xs ys : Array α} {size start : ℕ},
  i < ys.size → i < (Array.extract.loop xs size start ys).size
-- Lean.Elab.Do.Basic
/-- The subset of `mutVars` that were reassigned in any of the `childCtxs` relative to the given
`rootCtx`.
 -/
Lean.Elab.Do.getReassignedMutVars : Lean.LocalContext → Std.HashSet Lean.Name → Array Lean.LocalContext → Std.HashSet Lean.Name
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
/-- The limit cone for the product with a zero object is limiting.  -/
CategoryTheory.Limits.binaryFanZeroRightIsLimit : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (X : C) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.binaryFanZeroRight X)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instSMulCommClass : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : (i : ι) → Mul (G i)]
  [inst_5 : (i : ι) → SMul R (G i)] [∀ (i : ι), SMulCommClass R (G i) (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)]
  [inst_8 : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)],
  SMulCommClass R (DirectLimit G f) (DirectLimit G f)
-- Mathlib.RingTheory.Invariant.Basic
/-- For any domain `k` containing `B ⧸ Q`,
any endomorphism of `k` can be restricted to an endomorphism of `B ⧸ Q`.

This is basically the fact that `L/K` normal implies `κ(Q)/κ(P)` normal in the Galois setting.
 -/
Ideal.Quotient.exists_algHom_fixedPoint_quotient_under : ∀ {A : Type u_1} {B : Type u_2} {k : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  (G : Type u_4) [Finite G] [inst_4 : Group G] [inst_5 : MulSemiringAction G B] [Algebra.IsInvariant A B G]
  (P : Ideal A) (Q : Ideal B) [inst_7 : Q.LiesOver P] [inst_8 : CommRing k] [inst_9 : Algebra (A ⧸ P) k]
  [inst_10 : Algebra (B ⧸ Q) k] [IsScalarTower (A ⧸ P) (B ⧸ Q) k] [IsDomain k] [FaithfulSMul (B ⧸ Q) k]
  (σ : k →ₐ[A ⧸ P] k), ∃ τ, ∀ (x : B ⧸ Q), (algebraMap (B ⧸ Q) k) (τ x) = σ ((algebraMap (B ⧸ Q) k) x)
-- ProofWidgets.Component.PenroseDiagram
ProofWidgets.Penrose.DiagramProps.dsl : ProofWidgets.Penrose.DiagramProps → String
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.maxUnifEigenspaceIndex_le_finrank : ∀ {K : Type v} {V : Type w} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  (f : Module.End K V) (μ : K), f.maxUnifEigenspaceIndex μ ≤ Module.finrank K V
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.forallProp.inj : ∀ {e e_1 : Lean.Expr}, Lean.Meta.Grind.SplitSource.forallProp e = Lean.Meta.Grind.SplitSource.forallProp e_1 → e = e_1
-- Mathlib.Order.GaloisConnection.Defs
/-- A Galois coinsertion is a Galois connection where `u ∘ l = id`. It also contains a constructive
choice function, to give better definitional equalities when lifting order structures. Dual to
`GaloisInsertion`  -/
GaloisCoinsertion : {α : Type u} → {β : Type v} → [Preorder α] → [Preorder β] → (α → β) → (β → α) → Type (max u v)
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
CategoryTheory.Functor.closedUnit_app_app : ∀ {D : Type u} {C : Type u_1} [inst : CategoryTheory.Groupoid D] [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  (F G : CategoryTheory.Functor D C) (X : D),
  (F.closedUnit.app G).app X = (CategoryTheory.ihom.coev (F.obj X)).app (G.obj X)
-- Qq.SortLocalDecls
Qq.SortLocalDecls.State : Type
-- Std.Do.Triple.Basic
Std.Do.Triple.iff : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Std.Do.WP m ps] {α : Type u} {x : m α} {P : Std.Do.Assertion ps}
  {Q : Std.Do.PostCond α ps}, ⦃P⦄ x ⦃Q⦄ ↔ P ⊢ₛ (Std.Do.wp x).apply Q
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.comp_familyOfBFamily : ∀ {α : Type u_1} {β : Type u_2} {o : Ordinal.{u_3}} (f : (a : Ordinal.{u_3}) → a < o → α) (g : α → β),
  g ∘ o.familyOfBFamily f = o.familyOfBFamily fun i hi => g (f i hi)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesMap'_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData),
  CategoryTheory.ShortComplex.cyclesMap' (CategoryTheory.CategoryStruct.id S) h h = CategoryTheory.CategoryStruct.id h.K
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.mapRange.linearEquiv_symm : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : Module R₂ N] {σ₁₂ : R →+* R₂}
  {σ₂₁ : R₂ →+* R} [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] N),
  (Finsupp.mapRange.linearEquiv f).symm = Finsupp.mapRange.linearEquiv f.symm
-- Mathlib.Analysis.Convex.Continuous
ConcaveOn.isBoundedUnder_abs : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {C : Set E} {f : E → ℝ},
  ConcaveOn ℝ C f →
    ∀ {x₀ : E},
      C ∈ nhds x₀ →
        (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhds x₀) |f| ↔
          Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (nhds x₀) f)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
/-- A version of δ_comp_δ with indices in ℕ satisfying relevant inequalities.  -/
SimplexCategoryGenRel.δ_comp_δ_nat : ∀ {n : ℕ} (i j : ℕ) (hi : i < n + 2) (hj : j < n + 2),
  i ≤ j →
    CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ ⟨i, hi⟩) (SimplexCategoryGenRel.δ ⟨j + 1, ⋯⟩) =
      CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ ⟨j, hj⟩) (SimplexCategoryGenRel.δ ⟨i, ⋯⟩)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearMap.BilinMap.toQuadraticMap_comp_same : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {N' : Type u_8} [inst_5 : AddCommMonoid N'] [inst_6 : Module R N']
  (B : LinearMap.BilinMap R M N) (f : N' →ₗ[R] M),
  LinearMap.BilinMap.toQuadraticMap (LinearMap.compl₁₂ B f f) = B.toQuadraticMap.comp f
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- `MonoidAlgebra.map` of an injective function is injective.  -/
MonoidAlgebra.map_injective : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+ S),
  Function.Injective ⇑f → Function.Injective (MonoidAlgebra.map f)
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical.congr_simp : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  (a a_1 : M), a = a_1 → UniqueFactorizationMonoid.radical a = UniqueFactorizationMonoid.radical a_1
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
/-- Make an `n`-cocycle out of an element of the kernel of the `n`th differential.  -/
groupCohomology.cocyclesMk : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      {A : Rep.{u, u, u} k G} →
        {n : ℕ} →
          (f : (Fin n → G) → ↑A) →
            (CategoryTheory.ConcreteCategory.hom (inhomogeneousCochains.d A n)) f = 0 → ↑(groupCohomology.cocycles A n)
-- Mathlib.Data.List.Infix
List.getElem_inits : ∀ {α : Type u_1} (l : List α) (n : ℕ) (h : n < l.inits.length), l.inits[n] = List.take n l
-- Mathlib.Topology.LocallyConstant.Algebra
/-- Evaluation as an `AddMonoidHom`  -/
LocallyConstant.evalAddMonoidHom : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : AddZeroClass Y] → X → LocallyConstant X Y →+ Y
-- Mathlib.Data.Num.Bitwise
/-- Bitwise "or" for `Num`.  -/
Num.lor : Num → Num → Num
-- Mathlib.Data.ENNReal.Operations
ENNReal.le_toReal_sub : ∀ {a b : ENNReal}, b ≠ ⊤ → a.toReal - b.toReal ≤ (a - b).toReal
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
extDerivWithin_congr' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E} {x : E},
  Set.EqOn ω₁ ω₂ s → x ∈ s → extDerivWithin ω₁ s x = extDerivWithin ω₂ s x
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
AlgebraicIndependent.instFinitaryMatroid : ∀ (R : Type u_1) (A : Type w) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A] [inst_4 : NoZeroDivisors A], (AlgebraicIndependent.matroid R A).Finitary
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.safeRule.inj : ∀ {r r_1 : Aesop.SafeRule}, Aesop.BaseRuleSetMember.safeRule r = Aesop.BaseRuleSetMember.safeRule r_1 → r = r_1
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multiequalizer.ιPi_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasMultiequalizer I]
  [inst_2 : CategoryTheory.Limits.HasProduct I.left] [inst_3 : CategoryTheory.Limits.HasProduct I.right] (a : J.L)
  {Z : C} (h : I.left a ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ιPi I)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left a) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I a) h
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.exact_f_d : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughInjectives C] {X Y : C} (f : X ⟶ Y),
  { X₁ := X, X₂ := Y, X₃ := CategoryTheory.Injective.syzygies f, f := f, g := CategoryTheory.Injective.d f,
      zero := ⋯ }.Exact
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
/-- Element of the initial family.  -/
CategoryTheory.Precoverage.SubsheafClosure.base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))} {Z : C}
  {a : F.obj (Opposite.op Z)}, a ∈ 𝒮 Z → K.SubsheafClosure 𝒮 Z a
-- Mathlib.LinearAlgebra.Dimension.LinearMap
LinearMap.lift_rank_comp_le_right : ∀ {K : Type u} {V : Type v} {V' : Type v'} {V'' : Type v''} [inst : Semiring K] [inst_1 : AddCommMonoid V]
  [inst_2 : Module K V] [inst_3 : AddCommMonoid V'] [inst_4 : Module K V'] [inst_5 : AddCommMonoid V'']
  [inst_6 : Module K V''] (g : V →ₗ[K] V') (f : V' →ₗ[K] V''),
  Cardinal.lift.{v', v''} (f ∘ₗ g).rank ≤ Cardinal.lift.{v'', v'} g.rank
-- Mathlib.Order.Interval.Set.SurjOn
surjOn_Iio_of_monotone_surjective : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PartialOrder β] {f : α → β},
  Monotone f → Function.Surjective f → ∀ (a : α), Set.SurjOn f (Set.Iio a) (Set.Iio (f a))
-- Mathlib.CategoryTheory.Sites.Subsheaf
/-- The mono factorization given by `image_sheaf` for a morphism is an image.  -/
CategoryTheory.imageFactorization : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {F F' : CategoryTheory.Sheaf J (Type (max v u))} → (f : F ⟶ F') → CategoryTheory.Limits.ImageFactorisation f
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.BinaryInput.cast.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig1 aig2 : Std.Sat.AIG α}
  (input input_1 : aig1.BinaryInput),
  input = input_1 → ∀ (h : aig1.decls.size ≤ aig2.decls.size), input.cast h = input_1.cast h
-- Lean.CoreM
Lean.Core.withCurrHeartbeats : {m : Type → Type u_1} → {α : Type} → [Monad m] → [MonadControlT Lean.CoreM m] → m α → m α
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.instDecidableEqDyadic.decEq.match_1.splitter : (motive : Dyadic → Dyadic → Sort u_1) →
  (x x_1 : Dyadic) →
    (Unit → motive Dyadic.zero Dyadic.zero) →
      ((n k : ℤ) → (hn : n % 2 = 1) → motive Dyadic.zero (Dyadic.ofOdd n k hn)) →
        ((n k : ℤ) → (hn : n % 2 = 1) → motive (Dyadic.ofOdd n k hn) Dyadic.zero) →
          ((a a_1 : ℤ) →
              (a_2 : a % 2 = 1) →
                (b b_1 : ℤ) → (b_2 : b % 2 = 1) → motive (Dyadic.ofOdd a a_1 a_2) (Dyadic.ofOdd b b_1 b_2)) →
            motive x x_1
-- Mathlib.Data.Multiset.MapFold
Multiset.map_congr : ∀ {α : Type u_1} {β : Type v} {f g : α → β} {s t : Multiset α},
  s = t → (∀ x ∈ t, f x = g x) → Multiset.map f s = Multiset.map g t
-- Mathlib.Data.Set.Card
Set.ncard.eq_1 : ∀ {α : Type u_1} (s : Set α), s.ncard = s.encard.toNat
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smulCommClass_set' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SMul α γ] [inst_1 : SMul β γ] [SMulCommClass α β γ],
  SMulCommClass α (Set β) (Set γ)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.negMap_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  P 2 ≠ 0 → W.negMap ⟦P⟧ = ⟦![P 0 / P 2, W.toAffine.negY (P 0 / P 2) (P 1 / P 2), 1]⟧
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- The pointwise intersection of an upper hemicontinuous function with a fixed closed set is
upper hemicontinuous.  -/
UpperHemicontinuous.inter : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β},
  UpperHemicontinuous f → ∀ {u : Set β}, IsClosed u → UpperHemicontinuous fun x => f x ∩ u
-- Init.Data.SInt.Lemmas
Int64.ofBitVec_ofNat : ∀ (n : ℕ), Int64.ofBitVec (BitVec.ofNat 64 n) = Int64.ofNat n
-- Lean.Meta.Tactic.Cases
Lean.Meta.withNewEqs : {α : Type} → Array Lean.Expr → Array Lean.Expr → (Array Lean.Expr → Array Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.lintDeclHead : Lean.SyntaxNodeKind → Lean.Syntax → optParam Bool false → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.AbelianStruct.ι_imageπ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {f : X ⟶ Y} (self : CategoryTheory.Abelian.AbelianStruct f),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι self.kernelFork) self.imageπ = 0
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α} (h : t.WF),
  Std.DTreeMap.Raw.Const.get? (Std.DTreeMap.Raw.filter f t) k =
    (Std.DTreeMap.Raw.Const.get? t k).pfilter fun x h' => f (t.getKey k ⋯) x
-- Mathlib.Data.TypeVec
TypeVec.casesCons_append1 : ∀ (n : ℕ) {β : TypeVec.{u_2} (n + 1) → Sort u_1} (f : (t : Type u_2) → (v : TypeVec.{u_2} n) → β (v ::: t))
  (v : TypeVec.{u_2} n) (α : Type u_2), TypeVec.casesCons n f (v ::: α) = f α v
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.zero_lt_apply_root_root_iff : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (B : RootPairing.RootPositiveForm S P) (i j : ι) [inst_9 : FaithfulSMul S R] [inst_10 : Module S M]
  [inst_11 : IsScalarTower S R M] [IsStrictOrderedRing S]
  (hi : optParam (P.root i ∈ Submodule.span S (Set.range ⇑P.root)) ⋯)
  (hj : optParam (P.root j ∈ Submodule.span S (Set.range ⇑P.root)) ⋯),
  0 < (B.posForm ⟨P.root i, hi⟩) ⟨P.root j, hj⟩ ↔ 0 < P.pairingIn S i j
-- Init.System.IO
/-- Rewinds the read/write cursor to the beginning of the handle's file.
 -/
IO.FS.Handle.rewind : IO.FS.Handle → IO Unit
-- Mathlib.Order.Filter.IndicatorFunction
Monotone.indicator_eventuallyEq_iUnion : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_5} [inst : Preorder ι] [inst_1 : Zero β] (s : ι → Set α),
  Monotone s → ∀ (f : α → β) (a : α), (fun i => (s i).indicator f a) =ᶠ[Filter.atTop] fun x => (⋃ i, s i).indicator f a
-- Mathlib.Analysis.Convex.Independent
/-- If a set is convex independent, a point in the set is not in the convex hull of the other
points. See `convexIndependent_iff_notMem_convexHull_sdiff` for the indexed family version.  -/
convexIndependent_set_iff_notMem_convexHull_sdiff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {s : Set E}, ConvexIndependent 𝕜 Subtype.val ↔ ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
-- Mathlib.Data.Stream.Init
Stream'.map_iterate : ∀ {α : Type u} (f : α → α) (a : α), Stream'.iterate f (f a) = Stream'.map f (Stream'.iterate f a)
-- Mathlib.Order.Lattice.Nat
Nat.iInf_le_succ : ∀ {α : Type u_1} [inst : CompleteLattice α] (u : ℕ → α) (n : ℕ),
  ⨅ k, ⨅ (_ : k ≤ n + 1), u k = (⨅ k, ⨅ (_ : k ≤ n), u k) ⊓ u (n + 1)
-- Mathlib.Topology.Algebra.Module.Cardinality
/-- In a nontrivial topological vector space over a complete nontrivially normed field, any nonempty
open set has cardinality at least continuum.  -/
continuum_le_cardinal_of_isOpen : ∀ {E : Type u_1} (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [Nontrivial E] [inst_5 : TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {s : Set E},
  IsOpen s → s.Nonempty → Cardinal.continuum ≤ Cardinal.mk ↑s
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.ColimitType.instNeg : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J RingCat) → Neg (RingCat.Colimits.ColimitType F)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RcoSliceData.treeMap : {α : Type u} →
  {β : α → Type v} → [inst : Ord α] → Std.DTreeMap.Internal.RcoSliceData α β → Std.DTreeMap.Internal.Impl α β
-- Lean.ResolveName
Lean.throwReservedNameNotAvailable : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → Lean.Name → Lean.Name → m Unit
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- A product monoid algebra is a nested monoid algebra.  -/
MonoidAlgebra.curryAlgEquiv : (R : Type u_1) →
  {A : Type u_4} →
    {M : Type u_7} →
      {N : Type u_8} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : Monoid M] →
                [inst_4 : Monoid N] → MonoidAlgebra A (M × N) ≃ₐ[R] MonoidAlgebra (MonoidAlgebra A N) M
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_add_le : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b : E), ‖a + b‖₊ ≤ ‖a‖₊ + ‖b‖₊
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
/-- Every Yoneda-presheaf is a sheaf for the regular topology.  -/
CategoryTheory.regularTopology.isSheaf_yoneda_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preregular C] (W : C),
  CategoryTheory.Presieve.IsSheaf (CategoryTheory.regularTopology C) (CategoryTheory.yoneda.obj W)
-- Mathlib.AlgebraicTopology.DoldKan.GammaCompN
/-- Compatibility isomorphism between `toKaroubi _ ⋙ Γ₂ ⋙ N₂` and `Γ₀ ⋙ N₁` which
are functors `ChainComplex C ℕ ⥤ Karoubi (ChainComplex C ℕ)`.  -/
AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] →
        (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).comp
            (AlgebraicTopology.DoldKan.Γ₂.comp AlgebraicTopology.DoldKan.N₂) ≅
          AlgebraicTopology.DoldKan.Γ₀.comp AlgebraicTopology.DoldKan.N₁
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.coeff_natTrailingDegree_eq_zero_of_trailingDegree_lt : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R},
  p.trailingDegree < q.trailingDegree → q.coeff p.natTrailingDegree = 0
-- Mathlib.Data.Quot
Quot.eq : ∀ {α : Type u_3} {r : α → α → Prop} {x y : α}, Quot.mk r x = Quot.mk r y ↔ Relation.EqvGen r x y
-- Mathlib.CategoryTheory.MorphismProperty.Ind
CategoryTheory.MorphismProperty.instRespectsIsoInd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.RespectsIso],
  P.ind.RespectsIso
-- Mathlib.RingTheory.Extension.Presentation.Core
/-- A ring `R₀` has the coefficients of the presentation `P` if the coefficients of the relations of `P`
lie in the image of `R₀` in `R`.
The smallest subring of `R` satisfying this is given by `Algebra.Presentation.Core P`.
 -/
Algebra.Presentation.HasCoeffs : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              Algebra.Presentation R S ι σ →
                (R₀ : Type u_5) →
                  [inst_3 : CommRing R₀] →
                    [inst_4 : Algebra R₀ R] → [inst_5 : Algebra R₀ S] → [IsScalarTower R₀ R S] → Prop
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
/-- Determinant of the derivative of `g : ℍ → ℍ` considered as an `ℝ`-linear map. This is used in
the proof that the action is measure-preserving. Note this formula applies for both orientation-
preserving and orientation-reserving isometries.  -/
UpperHalfPlane.det_smulFDeriv : ∀ (g : GL (Fin 2) ℝ) (z : ℂ),
  (UpperHalfPlane.smulFDeriv g z).det =
    ↑(SignType.sign ↑(Matrix.GeneralLinearGroup.det g)) * ↑(Matrix.GeneralLinearGroup.det g) ^ 2 /
      ‖UpperHalfPlane.denom g z‖ ^ 4
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.rfl : ∀ {α : Type u} {m : Std.HashSet.Raw α}, m.Equiv m
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
NumberField.rootDiscr_rat : NumberField.rootDiscr ℚ = 1
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.comp_continuousWithinAt_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (h : X ≃ₜ Y) (f : Z → X) (s : Set Z) (z : Z),
  ContinuousWithinAt f s z ↔ ContinuousWithinAt (⇑h ∘ f) s z
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.singleton.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T),
  CategoryTheory.PreZeroHypercover.singleton f = { I₀ := PUnit.{w + 1}, X := fun x => S, f := fun x => f }