mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.coprodEquivL_apply_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} (S : Type u_5) [inst : NormedField 𝕜]
  [inst_1 : Semiring S] [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E]
  [inst_5 : IsTopologicalAddGroup E] [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F]
  [inst_9 : IsTopologicalAddGroup F] [inst_10 : AddCommGroup G] [inst_11 : Module 𝕜 G] [inst_12 : TopologicalSpace G]
  [inst_13 : IsTopologicalAddGroup G] [inst_14 : ContinuousConstSMul 𝕜 G] [inst_15 : Module S G]
  [inst_16 : SMulCommClass 𝕜 S G] [inst_17 : ContinuousConstSMul S G] (f : (E →L[𝕜] G) × (F →L[𝕜] G)) (a : E × F),
  ((ContinuousLinearMap.coprodEquivL S) f) a = f.1 a.1 + f.2 a.2
-- Std.Data.DTreeMap.Internal.WF.Defs
/-- `erase` preserves well-formedness. Later shown to be subsumed by `.wf`.  -/
Std.DTreeMap.Internal.Impl.WF.erase : ∀ {α : Type u} [inst : Ord α] {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced} {k : α},
  t.WF → (Std.DTreeMap.Internal.Impl.erase k t h).impl.WF
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- Isomorphic monoids have isomorphic additive monoid algebras.  -/
AddMonoidAlgebra.mapDomainRingEquiv : (R : Type u_3) →
  {M : Type u_6} →
    {N : Type u_7} →
      [inst : Semiring R] →
        [inst_1 : AddMonoid M] → [inst_2 : AddMonoid N] → M ≃+ N → AddMonoidAlgebra R M ≃+* AddMonoidAlgebra R N
-- Mathlib.FieldTheory.Relrank
IntermediateField.relrank_mul_rank_top : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E},
  A ≤ B → A.relrank B * Module.rank (↥B) E = Module.rank (↥A) E
-- Mathlib.Algebra.Ring.ULift
/-- The ring equivalence between `ULift R` and `R`.  -/
ULift.ringEquiv : {R : Type u} → [inst : NonUnitalNonAssocSemiring R] → ULift.{u_1, u} R ≃+* R
-- Mathlib.Order.Preorder.Chain
IsChain.directed : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} [Std.Refl r] {f : β → α} {c : Set β},
  IsChain (f ⁻¹'o r) c → Directed r fun x => f ↑x
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.factors_prod : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] (a : Associates α),
  a.factors.prod = a
-- Mathlib.Order.Interval.Finset.Basic
/-- **Alias** of the reverse direction of `Finset.nonempty_Ioi`. -/
Finset.Aesop.nonempty_Ioi_of_not_isMax : ∀ {α : Type u_2} {a : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α], ¬IsMax a → (Finset.Ioi a).Nonempty
-- Mathlib.Algebra.Group.Defs
_private.Mathlib.Algebra.Group.Defs.0.npowRec'.match_1.eq_1 : ∀ {M : Type u_2} (motive : ℕ → M → Sort u_1) (x : M) (h_1 : (x : M) → motive 0 x) (h_2 : (m : M) → motive 1 m)
  (h_3 : (k : ℕ) → (m : M) → motive k.succ.succ m),
  (match 0, x with
    | 0, x => h_1 x
    | 1, m => h_2 m
    | k.succ.succ, m => h_3 k m) =
    h_1 x
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.mk.sizeOf_spec : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] [inst_9 : SizeOf R] [inst_10 : SizeOf V]
  [inst_11 : SizeOf W] [inst_12 : SizeOf P] [inst_13 : SizeOf Q] (toAffineMap : P →ᵃ[R] Q)
  (cont : Continuous toAffineMap.toFun),
  sizeOf { toAffineMap := toAffineMap, cont := cont } = 1 + sizeOf toAffineMap + sizeOf cont
-- Mathlib.RingTheory.Ideal.Operations
Ideal.span_mul_span : ∀ {R : Type u} [inst : Semiring R] (S T : Set R) [(Ideal.span S).IsTwoSided],
  Ideal.span S * Ideal.span T = Ideal.span (S * T)
-- Mathlib.Logic.Relation
/-- **Alias** of `refl_iff_eq_le`. -/
refl_iff_subrelation_eq : ∀ {α : Type u_1} {r : α → α → Prop}, Std.Refl r ↔ Eq ≤ r
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
_private.Mathlib.Analysis.SpecialFunctions.BinaryEntropy.0.Real.tendsto_log_one_sub_sub_log_nhdsLT_one_atBot : Filter.Tendsto (fun p => Real.log (1 - p) - Real.log p) (nhdsWithin 1 (Set.Iio 1)) Filter.atBot
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- `true` when `norm` is zero, used as a hint to the evaluator.  -/
Mathlib.Tactic.Determinant.Cert.isZero : {u : Lean.Level} → {α : Q(Type u)} → {rα : Q(CommRing «$α»)} → Mathlib.Tactic.Determinant.Cert rα → Bool
-- Init.Data.SInt.Lemmas
Int16.toInt8_add : ∀ (a b : Int16), (a + b).toInt8 = a.toInt8 + b.toInt8
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.eq_comp_symm : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] {α : Type u_3} (e : M ≃ₜ+ N) (f : N → α) (g : M → α), f = g ∘ ⇑e.symm ↔ f ∘ ⇑e = g
-- Mathlib.Order.Directed
/-- A set stable by supremum is `≤`-directed.  -/
directedOn_of_sup_mem : ∀ {α : Type u_1} [inst : SemilatticeSup α] {S : Set α},
  (∀ ⦃i j : α⦄, i ∈ S → j ∈ S → i ⊔ j ∈ S) → DirectedOn (fun x1 x2 => x1 ≤ x2) S
-- Lean.MonadEnv
Lean.evalConstCheck : {m : Type → Type} →
  [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → [Lean.MonadOptions m] → (α : Type) → Lean.Name → Lean.Name → m α
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.map_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (p : PMF α) (g : β → γ),
  PMF.map g (PMF.map f p) = PMF.map (g ∘ f) p
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
/-- The pushout of `biprod.fst` and `biprod.snd` is the zero object.  -/
CategoryTheory.IsPushout.pushoutBiprodFstBiprodSnd : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {X Y : C} →
          [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X Y] →
            CategoryTheory.Limits.pushout CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd ≅ 0
-- Mathlib.Algebra.Lie.Basic
LieHom.zero_apply : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (x : L₁), 0 x = 0
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- The algebra equivalence between `ContinuousLinearMapWOT` and `ContinuousLinearMap`.  -/
ContinuousLinearMapWOT.algEquiv : {𝕜₁ : Type u_1} →
  [inst : NormedField 𝕜₁] →
    {E : Type u_3} →
      [inst_1 : AddCommGroup E] →
        [inst_2 : TopologicalSpace E] →
          [inst_3 : Module 𝕜₁ E] →
            (S : Type u_5) →
              [inst_4 : CommSemiring S] →
                [inst_5 : Module S E] →
                  [inst_6 : SMulCommClass 𝕜₁ S E] →
                    [inst_7 : SMul S 𝕜₁] →
                      [inst_8 : IsScalarTower S 𝕜₁ E] →
                        [inst_9 : ContinuousConstSMul S E] →
                          [inst_10 : IsTopologicalAddGroup E] → (E →WOT[𝕜₁] E) ≃ₐ[S] E →L[𝕜₁] E
-- Mathlib.Data.List.AList
AList.mem_lookup_union : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {s₁ s₂ : AList β},
  b ∈ AList.lookup a (s₁ ∪ s₂) ↔ b ∈ AList.lookup a s₁ ∨ a ∉ s₁ ∧ b ∈ AList.lookup a s₂
-- Mathlib.Data.Semiquot
Semiquot.IsPure.min : ∀ {α : Type u_1} {s t : Semiquot α}, t.IsPure → (s ≤ t ↔ s = t)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedENode : Inhabited Lean.Meta.Grind.ENode
-- Init.Data.Int.DivMod.Lemmas
Int.instNeZeroCastOfNat : ∀ {n : ℕ} [NeZero n], NeZero ↑n
-- Init.Data.List.BasicAux
/-- Drops the first element of a nonempty list, returning the tail. If the list is empty, this function
panics when executed and returns the empty list.

Safer alternatives include
 * `tail`, which returns the empty list without panicking,
 * `tail?`, which returns an `Option`, and
 * `tailD`, which returns a fallback value when passed the empty list.

Examples:
 * `["apple", "banana", "grape"].tail! = ["banana", "grape"]`
 * `["banana", "grape"].tail! = ["grape"]`
 -/
List.tail! : {α : Type u_1} → List α → List α
-- Init.Data.String.TakeDrop
String.dropRight : String → ℕ → String
-- Mathlib.Algebra.Algebra.Operations
Submodule.spanSingleton_apply : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A),
  (Submodule.spanSingleton R) x = R ∙ x
-- Mathlib.Data.Rat.Lemmas
Rat.mul_self_den : ∀ (q : ℚ), (q * q).den = q.den * q.den
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.qExpansion_mul : ∀ {h : ℝ} {f g : UpperHalfPlane → ℂ},
  AnalyticAt ℂ (UpperHalfPlane.cuspFunction h f) 0 →
    AnalyticAt ℂ (UpperHalfPlane.cuspFunction h g) 0 →
      UpperHalfPlane.qExpansion h (f * g) = UpperHalfPlane.qExpansion h f * UpperHalfPlane.qExpansion h g
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.monomial_sub : ∀ {R : Type u_1} [inst : Ring R] {a b : R} (n : ℕ),
  (SkewPolynomial.monomial n) (a - b) = (SkewPolynomial.monomial n) a - (SkewPolynomial.monomial n) b
-- Batteries.Recycling.RBTree.Lemmas
/-- A stronger version of `lowerBound?_greatest` that holds when the cut is strict.  -/
RBTree.RBNode.Ordered.lowerBound?_lt : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBTree.RBNode α} {x y : α} [Std.TransCmp cmp]
  [RBTree.RBNode.IsStrictCut cmp cut],
  RBTree.RBNode.Ordered cmp t →
    RBTree.RBNode.lowerBound? cut t = some x → y ∈ t → (cmp x y = Ordering.lt ↔ cut y = Ordering.lt)
-- Mathlib.RingTheory.PowerSeries.PiTopology
/-- The pointwise topology on `PowerSeries`  -/
PowerSeries.WithPiTopology.instTopologicalSpace : (R : Type u_1) → [TopologicalSpace R] → TopologicalSpace (PowerSeries R)
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_inf : ∀ {R : Type u} [inst : CommSemiring R] (I J : Ideal R),
  PrimeSpectrum.zeroLocus ↑(I ⊓ J) = PrimeSpectrum.zeroLocus ↑I ∪ PrimeSpectrum.zeroLocus ↑J
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- If `F` has a colimit, so does any naturally isomorphic functor.  -/
CategoryTheory.Limits.hasColimit_of_iso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [CategoryTheory.Limits.HasColimit F] (α : G ≅ F),
  CategoryTheory.Limits.HasColimit G
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- This definition allows to endow `Π i, α i` with the Lp norm with the uniformity and bornology
being defeq to the product ones. It is useful to endow a type synonym of `Π i, α i` with the
Lp norm.  -/
PiLp.normedAddCommGroupToPi : (p : ENNReal) →
  {ι : Type u_2} →
    (α : ι → Type u_3) →
      [Fact (1 ≤ p)] → [Fintype ι] → [(i : ι) → NormedAddCommGroup (α i)] → NormedAddCommGroup ((i : ι) → α i)
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isBigOWith_norm_right`. -/
Asymptotics.IsBigOWith.of_norm_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {c : ℝ} {f : α → E}
  {g' : α → F'} {l : Filter α}, (Asymptotics.IsBigOWith c l f fun x => ‖g' x‖) → Asymptotics.IsBigOWith c l f g'
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.instInhabitedFunIndParamKind.default : Lean.Meta.FunIndParamKind
-- Mathlib.Topology.Category.TopCat.Limits.Products
/-- The explicit cofan of a family of topological spaces given by the sigma type.  -/
TopCat.sigmaCofan : {ι : Type v} → (α : ι → TopCat) → CategoryTheory.Limits.Cofan α
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneUnopOfCoconeEquiv_functor_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : (CategoryTheory.Limits.Cocone F)ᵒᵖ),
  CategoryTheory.Limits.coneUnopOfCoconeEquiv.functor.obj c = CategoryTheory.Limits.coneUnopOfCocone (Opposite.unop c)
-- Mathlib.Order.Interval.Set.UnorderedInterval
/-- The open-closed uIcc with unordered bounds.  -/
Set.uIoc : {α : Type u_1} → [LinearOrder α] → α → α → Set α
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_eq_isSome_get? : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α}, m.contains a = (m.get? a).isSome
-- Mathlib.Order.Sublattice
Sublattice.supClosed' : ∀ {α : Type u_2} [inst : Lattice α] (self : Sublattice α), SupClosed self.carrier
-- Mathlib.LinearAlgebra.Finsupp.Span
Finsupp.ker_lsingle : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (a : α), (Finsupp.lsingle a).ker = ⊥
-- Init.Data.Vector.Lemmas
Vector.exists_mem_empty : ∀ {α : Type u_1} (p : α → Prop), ¬∃ x, ∃ (_ : x ∈ #v[]), p x
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
/-- Composition as a non-unital algebra homomorphism.  -/
ZeroAtInftyContinuousMap.compNonUnitalAlgHom : {β : Type v} →
  {γ : Type w} →
    {δ : Type u_2} →
      [inst : TopologicalSpace β] →
        [inst_1 : TopologicalSpace γ] →
          [inst_2 : TopologicalSpace δ] →
            {R : Type u_3} →
              [inst_3 : Semiring R] →
                [inst_4 : NonUnitalNonAssocSemiring δ] →
                  [inst_5 : IsTopologicalSemiring δ] →
                    [inst_6 : Module R δ] →
                      [inst_7 : ContinuousConstSMul R δ] →
                        CocompactMap β γ → ZeroAtInftyContinuousMap γ δ →ₙₐ[R] ZeroAtInftyContinuousMap β δ
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- Restrict the codomain of an alternating map to a submodule.  -/
AlternatingMap.codRestrict : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_3} →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                {ι : Type u_7} → (f : M [⋀^ι]→ₗ[R] N) → (p : Submodule R N) → (∀ (v : ι → M), f v ∈ p) → M [⋀^ι]→ₗ[R] ↥p
-- Mathlib.Order.BoundedOrder.Basic
isTop_top : ∀ {α : Type u} [inst : LE α] [inst_1 : OrderTop α], IsTop ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The triangle consisting of the two natural transformations and `hom` commutes  -/
CategoryTheory.Limits.BinaryBiconeMorphism.winr_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} (self : CategoryTheory.Limits.BinaryBiconeMorphism A B)
  {Z : C} (h : B.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp A.inr (CategoryTheory.CategoryStruct.comp self.hom h) =
    CategoryTheory.CategoryStruct.comp B.inr h
-- Mathlib.FieldTheory.LinearDisjoint
IntermediateField.LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic_right : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type v} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L →
    ∀ [Algebra.IsAlgebraic F L], Module.rank F L * Module.rank (↥(IntermediateField.adjoin L ↑A)) E = Module.rank (↥A) E
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
IsOpen.balancedHull : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousConstSMul 𝕜 E] {s : Set E}, IsOpen s → 0 ∈ s → IsOpen (balancedHull 𝕜 s)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftIso_inverse_obj_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₂ R),
  ((CategoryTheory.Comma.mapLeftIso R i).inverse.obj X).right = X.right
-- Mathlib.Data.Seq.Basic
_private.Mathlib.Data.Seq.Basic.0.Stream'.Seq.join.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 α) → Sort u_2) (s' : Stream'.Seq1 α) (h_1 : Unit → motive none)
  (h_2 : (s' : Stream'.Seq1 α) → motive (some s')),
  (match some s' with
    | none => h_1 ()
    | some s' => h_2 s') =
    h_2 s'
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `LawfulOrderLT` instance if available  -/
Lean.Meta.Grind.Arith.Linear.Struct.lawfulOrderLTInst? : Lean.Meta.Grind.Arith.Linear.Struct → Option Lean.Expr
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The canonical isomorphism `K.cycles i ≅ K.X i` when the differential from `i` is zero.  -/
HomologicalComplex.iCyclesIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            (i j : ι) → c.next i = j → K.d i j = 0 → [inst_2 : K.HasHomology i] → K.cycles i ≅ K.X i
-- Aesop.Tree.Data
Aesop.GoalId : Type
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- Let `R` satisfy the strong rank condition. If `m` elements of a free rank `n` `R`-module are
linearly independent, then `m ≤ n`.  -/
Basis.card_le_card_of_linearIndependent_aux : ∀ {R : Type u_2} [inst : Semiring R] [StrongRankCondition R] (n : ℕ) {m : ℕ} (v : Fin m → Fin n → R),
  LinearIndependent R v → m ≤ n
-- Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
CategoryTheory.Limits.SequentialProduct.cone_π_app : ∀ {C : Type u_1} {M N : ℕ → C} [inst : CategoryTheory.Category.{v_1, u_1} C] (f : (n : ℕ) → M n ⟶ N n)
  [inst_1 : CategoryTheory.Limits.HasCountableProducts C] (n : ℕ),
  (CategoryTheory.Limits.SequentialProduct.cone f).π.app (Opposite.op n) =
    CategoryTheory.Limits.Pi.map fun m =>
      if h : m < n then CategoryTheory.eqToHom ⋯
      else CategoryTheory.CategoryStruct.comp (f m) (CategoryTheory.eqToHom ⋯)
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.Functor.instHasPointwiseLeftKanExtensionOfIsDense : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.IsDense], F.HasPointwiseLeftKanExtension F
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
CategoryTheory.Functor.closedIhom_obj_obj : ∀ {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 Y : CategoryTheory.Functor D C) (X : D), (F.closedIhom.obj Y).obj X = (F.obj X ⟹ Y.obj X)
-- Init.Prelude
/-- Interpret a bitvector as a number less than `2^w`.
O(1), because we use `Fin` as the internal representation of a bitvector.  -/
BitVec.toFin : {w : ℕ} → BitVec w → Fin (2 ^ w)
-- Mathlib.Analysis.Convex.BetweenList
/-- The points in a list are weakly in that order on a line.  -/
List.Wbtw : (R : Type u_1) →
  {V : Type u_2} →
    {P : Type u_4} →
      [inst : Ring R] → [PartialOrder R] → [inst_2 : AddCommGroup V] → [Module R V] → [AddTorsor V P] → List P → Prop
-- Init.Meta
/-- `simp!` is shorthand for `simp` with `autoUnfold := true`.
This will unfold applications of functions defined by pattern matching, when one of the patterns applies.
This can be used to partially evaluate many definitions.  -/
Lean.Parser.Tactic.simpAutoUnfold : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.IsCofiltered.IsEventuallyConstant.exists_isEventuallyConstantTo : ∀ {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}
  [self : CategoryTheory.IsCofiltered.IsEventuallyConstant F], ∃ j, F.IsEventuallyConstantTo j
-- Mathlib.RingTheory.Perfection
/-- **Alias** of `Perfection.subsemiring`.

---

`Perfection R p` as a subsemiring of `ℕ → R`.  -/
Ring.perfectionSubsemiring : (R : Type u_1) → [inst : CommSemiring R] → (p : ℕ) → [hp : Fact (Nat.Prime p)] → [CharP R p] → Subsemiring (ℕ → R)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.instInhabited.eq_1 : ∀ (A : Type u_2) (B : Type u_3) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B], ContinuousAddMonoidHom.instInhabited A B = { default := 0 }
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
/-- Eventually all functions from a well-formed basis are positive.  -/
Tactic.ComputeAsymptotics.WellFormedBasis.eventually_pos : ∀ {basis : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis basis → ∀ᶠ (x : ℝ) in Filter.atTop, ∀ f ∈ basis, 0 < f x
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.mk.inj : ∀ {carrier : Type u} {str : AddMonoid carrier} {carrier_1 : Type u} {str_1 : AddMonoid carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
/-- If `X` is an integral scheme that is universally closed over `Spec K`,
then `Γ(X, ⊤)` is a field.  -/
AlgebraicGeometry.isField_of_universallyClosed : ∀ {X : AlgebraicGeometry.Scheme} (K : Type u) [inst : Field K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K))
  [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.UniversallyClosed f], IsField ↑(X.presheaf.obj (Opposite.op ⊤))
-- Batteries.Data.BitVec.Lemmas
BitVec.getElem_ofFnBE : ∀ {n : ℕ} (f : Fin n → Bool) (i : ℕ) (h : i < n), (BitVec.ofFnBE f)[i] = f ⟨i, h⟩.rev
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SOppSide.not_sSameSide : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.SOppSide x y → ¬s.SSameSide x y
-- Lean.Server.Completion.EligibleHeaderDecls
/-- Cached header declarations for which `allowCompletion headerEnv decl` is true.  -/
Lean.Server.Completion.eligibleHeaderDeclsMutex : Std.Mutex (Option Lean.Server.Completion.EligibleHeaderDecls)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- If a sheaf of `R`-modules `M` has a presentation, then `M` is quasi-coherent.  -/
SheafOfModules.Presentation.isQuasicoherent : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasBinaryProducts C]
  {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat}
  [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat] [inst_3 : J.WEqualsLocallyBijective AddCommGrpCat]
  [inst_4 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_5 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (P : M.Presentation),
  M.IsQuasicoherent
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.piCongrLeft_apply : ∀ {ι : Type u_7} {ι' : Type u_8} {Y : ι' → Type u_9} [inst : (j : ι') → TopologicalSpace (Y j)] (e : ι ≃ ι')
  (a : (b : ι) → Y (e.symm.symm b)) (a_1 : ι'),
  (Homeomorph.piCongrLeft e) a a_1 = (Equiv.piCongrLeft' Y e.symm).symm a a_1