mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.Associated
Prime.exists_mem_finset_dvd : ∀ {ι : Type u_1} {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] {p : M₀},
  Prime p → ∀ {s : Finset ι} {f : ι → M₀}, p ∣ s.prod f → ∃ i ∈ s, p ∣ f i
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
LieGroup.mk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : Group G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G]
  [toContMDiffMul : ContMDiffMul I n G], (ContMDiff I I n fun a => a⁻¹) → LieGroup I n G
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- Given two bases indexed by `ι` and `ι'` of an `R`-module, where `R` satisfies the invariant
basis number property, an equiv `ι ≃ ι'`.  -/
Module.Basis.indexEquiv : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {ι : Type w} → {ι' : Type w'} → [InvariantBasisNumber R] → Module.Basis ι R M → Module.Basis ι' R M → ι ≃ ι'
-- Mathlib.GroupTheory.Complement
/-- The correct way to unfold `IsComplement` for `SetLike`s such as `Subgroup`s  -/
Subgroup.isComplement_iff_bijective : ∀ {G : Type u_1} [inst : Group G] {S : Type u_2} [inst_1 : SetLike S G] (s t : S),
  Subgroup.IsComplement ↑s ↑t ↔ Function.Bijective fun x => ↑x.1 * ↑x.2
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.forget_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  (A : C) [inst_4 : CategoryTheory.MonObj A] {X Y : CategoryTheory.Mod D A} (f : X ⟶ Y),
  (CategoryTheory.Mod.forget A).map f = f.hom
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.toEmbedding_apply : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f : L.PartialEquiv M N} (m : ↥f.dom), f.toEmbedding m = ↑(f.toEquiv m)
-- Mathlib.Topology.Category.LightProfinite.AsLimit
LightProfinite.surjective_transitionMap : ∀ (S : LightProfinite) (n : ℕ), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (S.transitionMap n))
-- Lean.Meta.Tactic.UnifyEq
_private.Lean.Meta.Tactic.UnifyEq.0.Lean.Meta.toOffset? : Lean.Expr → Lean.MetaM (Option (Lean.Expr × ℕ))
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabWaitIfTypeContainsMVar : Lean.Elab.Term.TermElab
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instCommSemiring : {R : Type u_1} → {a b : R} → [CommSemiring R] → CommSemiring (QuadraticAlgebra R a b)
-- Mathlib.Algebra.Lie.Quotient
LieSubmodule.Quotient.lieModuleHom_ext_iff : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N : LieSubmodule R L M} [inst_5 : LieAlgebra R L]
  [inst_6 : LieModule R L M] {f g : M ⧸ N →ₗ⁅R,L⁆ M},
  f = g ↔ f.comp (LieSubmodule.Quotient.mk' N) = g.comp (LieSubmodule.Quotient.mk' N)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_le_of_brange_subset : ∀ {o : Ordinal.{u}} {o' : Ordinal.{v}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}}
  {g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}}, o.brange f ⊆ o'.brange g → o.bsup f ≤ o'.bsup g
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isSome_minKey?_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {f : β → β},
  (t.modify k f).minKey?.isSome = !t.isEmpty
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintLabelPart.mk.sizeOf_spec : ∀ (value : String) (tooltip? : Option Lean.Lsp.InlayHintTooltip) (location? : Option Lean.Lsp.Location)
  (command? : Option Lean.Lsp.Command),
  sizeOf { value := value, tooltip? := tooltip?, location? := location?, command? := command? } =
    1 + sizeOf value + sizeOf tooltip? + sizeOf location? + sizeOf command?
-- Mathlib.Data.Finset.NAry
Finset.image₂_right : ∀ {α : Type u_1} {β : Type u_3} {s : Finset α} {t : Finset β} [inst : DecidableEq β],
  s.Nonempty → Finset.image₂ (fun x y => y) s t = t
-- Mathlib.Logic.Unique
/-- Given one value over a unique, we get a dependent function.  -/
uniqueElim : {ι : Sort u_2} → {α : ι → Sort u_3} → [inst : Unique ι] → α default → (i : ι) → α i
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : (a : α) → β a → Bool} {k : α} {h' : k ∈ Std.ExtDHashMap.filter f m},
  (Std.ExtDHashMap.filter f m).getKey k h' = m.getKey k ⋯
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instDivisionAddCommMonoidOfAddOpposite : {M : Type u_1} → [SubtractionCommMonoid Mᵃᵒᵖ] → SubtractionCommMonoid Mᵈᵃᵃ
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙHomSuperset_continuous : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {a : A} (ha : p a)
  {s : Set R} (hs : quasispectrum R a ⊆ s), Continuous ⇑(cfcₙHomSuperset ha hs)
-- Mathlib.NumberTheory.FermatPsp
_private.Mathlib.NumberTheory.FermatPsp.0.Nat.AB_id_helper : ∀ (b p : ℕ), 2 ≤ b → Odd p → (b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1)) = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
-- Init.Prelude
Nat.succ_le_succ : ∀ {n m : ℕ}, n ≤ m → n.succ ≤ m.succ
-- Batteries.Data.Array.Basic
_private.Batteries.Data.Array.Basic.0.Array.scanrMFast : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {β : Type u_1} →
      [Monad m] →
        (α → β → m β) → β → (as : Array α) → Array.SizeFitsUSize✝ as → optParam ℕ as.size → optParam ℕ 0 → m (Array β)
-- Mathlib.Combinatorics.Additive.RuzsaCovering
/-- **Ruzsa's covering lemma**  -/
Finset.ruzsa_covering_add : ∀ {G : Type u_1} [inst : AddGroup G] {K : ℝ} [inst_1 : DecidableEq G] {A B : Finset G},
  B.Nonempty → ↑(A + B).card ≤ K * ↑B.card → ∃ F ⊆ A, ↑F.card ≤ K ∧ A ⊆ F + (B - B)
-- Mathlib.Algebra.Order.BigOperators.Expect
/-- If `m` is a subadditive function (`m (x + y) ≤ m x + m y`, `m 0 = 0`) preserved under division
by a natural, then `m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)`.  -/
Finset.le_expect_of_subadditive : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M]
  [inst_2 : AddCommMonoid N] [inst_3 : PartialOrder N] [IsOrderedAddMonoid N] [inst_5 : Module ℚ≥0 N]
  [PosSMulMono ℚ≥0 N] {m : M → N} {f : ι → M} {s : Finset ι},
  m 0 = 0 →
    (∀ (a b : M), m (a + b) ≤ m a + m b) →
      (∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a) → m (s.expect fun i => f i) ≤ s.expect fun i => m (f i)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.zero_add' : ∀ {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.Preadditive C]
  {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : W.HasLeftCalculusOfFractions] {X Y : C} (f : L.obj X ⟶ L.obj Y),
  CategoryTheory.Localization.Preadditive.add' W (L.map 0) f = f
-- Lean.Linter.UnusedVariables
/-- Gets the status of `linter.unusedVariables.patternVars`  -/
Lean.Linter.getLinterUnusedVariablesPatternVars : Lean.Linter.LinterOptions → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- the right type  -/
CategoryTheory.Limits.MulticospanShape.R : CategoryTheory.Limits.MulticospanShape → Type w'
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanRank_restrictScalars_eq : ∀ {R : Type u_1} {S : Type u_2} {M : Type u} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : Algebra R S] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M],
  Function.Surjective ⇑(algebraMap R S) → ∀ (N : Submodule S M), (Submodule.restrictScalars R N).spanRank = N.spanRank
-- Mathlib.FieldTheory.SeparableDegree
/-- If a monic polynomial over a field `F` of exponential characteristic `q` has separable degree
one, then it is of the form `(X ^ (q ^ n) - C y) ^ m` for some non-zero natural number `m`,
some natural number `n`, and some element `y` of `F`, such that either `n = 0` or `y` has no
`q`-th root in `F`.  -/
Polynomial.Monic.eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one : ∀ {F : Type u} [inst : Field F] {f : Polynomial F} (q : ℕ) [inst_1 : ExpChar F q],
  f.Monic →
    f.natSepDegree = 1 →
      ∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (Polynomial.X ^ q ^ n - Polynomial.C y) ^ m
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.hasStrictFDerivAt_smul : ∀ (g : GL (Fin 2) ℝ) (τ : UpperHalfPlane),
  HasStrictFDerivAt (fun z => ↑(g • ↑UpperHalfPlane.ofComplex z)) (UpperHalfPlane.smulFDeriv g ↑τ) ↑τ
-- Mathlib.Algebra.Colimit.Module
AddCommGroup.DirectLimit.map.congr_simp : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (G i)]
  {f : (i j : ι) → i ≤ j → G i →+ G j} [inst_2 : DecidableEq ι] {G' : ι → Type u_5}
  [inst_3 : (i : ι) → AddCommMonoid (G' i)] {f' : (i j : ι) → i ≤ j → G' i →+ G' j} (g g_1 : (i : ι) → G i →+ G' i)
  (e_g : g = g_1) (hg : ∀ (i j : ι) (h : i ≤ j), (g j).comp (f i j h) = (f' i j h).comp (g i)),
  AddCommGroup.DirectLimit.map g hg = AddCommGroup.DirectLimit.map g_1 ⋯
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.mul_log_neg : ∀ {x : ℝ}, 0 < x → x < 1 → x * Real.log x < 0
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Ioc_Ioi_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a : α},
  Filter.TendstoIxxClass Set.Ioc (Filter.principal (Set.Ioi a)) (Filter.principal (Set.Ioi a))
-- Mathlib.CategoryTheory.Category.Preorder
instFullFunctor : ∀ {X : Type u} {Y : Type v} [inst : Preorder X] [inst_1 : Preorder Y] (f : X ↪o Y), ⋯.functor.Full
-- Mathlib.Topology.Algebra.Group.Pointwise
IsDiscrete.exists_nhds_eq_zero_of_image_addLeft_inter_nonempty : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] (S : AddSubgroup G),
  IsDiscrete ↑S → ∃ U ∈ nhds 0, -U = U ∧ ∀ g ∈ S, ((fun x => g + x) '' U ∩ U).Nonempty → g = 0
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.InvariantForm.mk : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {P : RootPairing ι R M N} →
                    (form : LinearMap.BilinForm R M) →
                      LinearMap.IsSymm form →
                        (∀ (i : ι), (form (P.root i)) (P.root i) ≠ 0) →
                          (∀ (i : ι), LinearMap.IsOrthogonal form ⇑(P.reflection i)) → P.InvariantForm
-- Lean.Widget.InteractiveGoal
/-- If true, the goal will be removed on the next tactic state.  -/
Lean.Widget.InteractiveGoal.isRemoved? : Lean.Widget.InteractiveGoal → Option Bool
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.mem_unop_iff : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {I : TwoSidedIdeal Rᵐᵒᵖ} {x : R}, x ∈ I.unop ↔ MulOpposite.op x ∈ I
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.C_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonAssocSemiring R], HahnSeries.C 0 = 0
-- Mathlib.Algebra.Order.CauSeq.Basic
/-- `LimZero f` holds when `f` approaches 0.  -/
CauSeq.LimZero : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [inst_2 : IsStrictOrderedRing α] → [inst_3 : Ring β] → {abv : β → α} → CauSeq β abv → Prop
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.keysArray_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.keysArray = t₂.keysArray
-- Mathlib.Algebra.Homology.Augment
_private.Mathlib.Algebra.Homology.Augment.0.ChainComplex.augment.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((i : ℕ) → motive i.succ) → motive x
-- Mathlib.Order.RelIso.Basic
RelEmbedding.refl_trans : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s), (RelEmbedding.refl r).trans f = f
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.leftUnitor_hom_unit_app : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} (V : Type u₂) {inst_1 : CategoryTheory.Category.{v₂, u₂} V}
  {inst_2 : CategoryTheory.MonoidalCategory C} {inst_3 : CategoryTheory.MonoidalCategory V} {D : Type u₃}
  {inst_4 : CategoryTheory.Category.{v₃, u₃} D} {inst_5 : CategoryTheory.MonoidalCategoryStruct D}
  [self : CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D] (d : D) (y : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.unitUnit C V D)
        (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d).obj y))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionExtensionUnit C V
              (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) d).app
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C, y))
        (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).map
              (CategoryTheory.MonoidalCategoryStruct.leftUnitor d).hom).app
          (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) y))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor
          (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d).obj y)).hom
      (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d).map
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor y).inv)
-- Mathlib.Data.Nat.Fib.Basic
Nat.fib.eq_1 : ∀ (n : ℕ), Nat.fib n = ((fun p => (p.2, p.1 + p.2))^[n] (0, 1)).1
-- Mathlib.Data.SetLike.Basic
SetLike.coe_mono : ∀ {A : Type u_1} {B : Type u_2} [inst : SetLike A B] [inst_1 : Preorder A] [IsConcreteLE A B], Monotone SetLike.coe
-- Mathlib.Order.Category.BddDistLat
BddDistLat.instCoeSortType : CoeSort BddDistLat (Type u_1)
-- Mathlib.Analysis.Normed.Group.Uniform
dist_mul_self_left : ∀ {E : Type u_2} [inst : SeminormedCommGroup E] (a b : E), dist (b * a) a = ‖b‖
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.enorm_tmul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (x : E) (y : F),
  ‖x ⊗ₜ[𝕜] y‖ₑ = ‖x‖ₑ * ‖y‖ₑ
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.id_h₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {i j : E.I₀}
  (x : E.I₁ i j), (CategoryTheory.PreOneHypercover.Hom.id E).h₁ x = CategoryTheory.CategoryStruct.id (E.Y x)
-- Mathlib.RingTheory.Kaehler.Basic
Derivation.tensorProductTo_mul : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M : Type u_1}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (D : Derivation R S M) (x y : TensorProduct R S S),
  D.tensorProductTo (x * y) =
    (Algebra.TensorProduct.lmul' R) x • D.tensorProductTo y + (Algebra.TensorProduct.lmul' R) y • D.tensorProductTo x
-- Mathlib.Order.SuccPred.Limit
Order.isSuccLimitRecOn_of_isMin : ∀ {α : Type u_1} {b : α} {motive : α → Sort u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α]
  (isMin : (a : α) → IsMin a → motive a) (succ : (a : α) → ¬IsMax a → motive (Order.succ a))
  (isSuccLimit : (a : α) → Order.IsSuccLimit a → motive a) (hb : IsMin b),
  Order.isSuccLimitRecOn b isMin succ isSuccLimit = isMin b hb
-- Mathlib.Analysis.Complex.UpperHalfPlane.Measure
UpperHalfPlane.instSigmaFiniteComapComplexCoeVolume : MeasureTheory.SigmaFinite (MeasureTheory.Measure.comap UpperHalfPlane.coe MeasureTheory.volume)
-- Mathlib.Order.Fin.Tuple
StrictAnti.vecCons : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α},
  StrictAnti f → f 0 < a → StrictAnti (Matrix.vecCons a f)
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.comap_map_eq_self : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {H : Subgroup G},
  f.ker ≤ H → Subgroup.comap f (Subgroup.map f H) = H
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
CategoryTheory.ShrinkHoms.isGrothendieckAbelian : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C],
  CategoryTheory.IsGrothendieckAbelian.{w, w, u} (CategoryTheory.ShrinkHoms.{u} C)
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
/-- the morphism to the single chain complex with `Z` in degree `0`  -/
CategoryTheory.ProjectiveResolution.π : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {Z : C} → (self : CategoryTheory.ProjectiveResolution Z) → self.complex ⟶ (ChainComplex.single₀ C).obj Z
-- Init.Grind.ToInt
_private.Init.Grind.ToInt.0.Lean.Grind.instBEqIntInterval.beq_spec_1 : ∀ (a a_1 b b_1 : ℤ), (Lean.Grind.IntInterval.co a a_1 == Lean.Grind.IntInterval.co b b_1) = (a == b && a_1 == b_1)
-- Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
contDiff_clm_apply_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {D : Type uD} [inst_1 : NormedAddCommGroup D]
  [inst_2 : NormedSpace 𝕜 D] {E : Type uE} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {F : Type uF}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} [CompleteSpace 𝕜] {f : D → E →L[𝕜] F}
  [FiniteDimensional 𝕜 E], ContDiff 𝕜 n f ↔ ∀ (y : E), ContDiff 𝕜 n fun x => (f x) y
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.mk.sizeOf_spec : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Zero Y] [inst_2 : SizeOf X]
  [inst_3 : (a : X) → SizeOf (U a)] [inst_4 : SizeOf Y] (toFun : X → Y)
  (supportWithinDomain' : Function.support toFun ⊆ U)
  (supportLocallyFiniteWithinDomain' : ∀ z ∈ U, ∃ t ∈ nhds z, (t ∩ Function.support toFun).Finite),
  sizeOf
      { toFun := toFun, supportWithinDomain' := supportWithinDomain',
        supportLocallyFiniteWithinDomain' := supportLocallyFiniteWithinDomain' } =
    1
-- Init.Data.List.MinMaxOn
List.apply_maxOn_lt_iff : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [inst_2 : LT β] [Std.IsLinearPreorder β]
  [Std.LawfulOrderLT β] {xs : List α} {f : α → β} (h : xs ≠ []) {b : β}, f (List.maxOn f xs h) < b ↔ ∀ x ∈ xs, f x < b
-- Batteries.Data.UnionFind.Basic
/-- Link two union-find nodes, uniting their respective classes.  -/
Batteries.UnionFind.unionN : {n : ℕ} → (self : Batteries.UnionFind) → Fin n → Fin n → n = self.size → Batteries.UnionFind
-- Mathlib.Data.Nat.Factors
Nat.primeFactorsList_subset_right : ∀ {n k : ℕ}, k ≠ 0 → n.primeFactorsList ⊆ (n * k).primeFactorsList
-- Init.Data.Array.Lemmas
Array.extract_empty_of_size_le_start : ∀ {α : Type u_1} {xs : Array α} {start stop : ℕ}, xs.size ≤ start → xs.extract start stop = #[]
-- Mathlib.CategoryTheory.Functor.Trifunctor
CategoryTheory.bifunctorComp₁₂_map_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {X₁ Y₁ : C₁} (φ : X₁ ⟶ Y₁) (X₂ : C₂) (X₃ : C₃),
  (((CategoryTheory.bifunctorComp₁₂ F₁₂ G).map φ).app X₂).app X₃ = (G.map ((F₁₂.map φ).app X₂)).app X₃
-- Init.Data.BitVec.Bitblast
BitVec.getMsbD_smod : ∀ {w i : ℕ} {x y : BitVec w},
  (x.smod y).getMsbD i =
    match x.msb, y.msb with
    | false, false => (x % y).getMsbD i
    | false, true => (if x % -y = 0#w then x % -y else x % -y + y).getMsbD i
    | true, false => (if -x % y = 0#w then -x % y else y - -x % y).getMsbD i
    | true, true => (-(-x % -y)).getMsbD i
-- Mathlib.Algebra.Group.Basic
add_neg_eq_of_eq_add : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, a = c + b → a + -b = c
-- Init.Core
Function.comp_apply : ∀ {β : Sort u_1} {δ : Sort u_2} {α : Sort u_3} {f : β → δ} {g : α → β} {x : α}, (f ∘ g) x = f (g x)
-- Mathlib.Analysis.Seminorm
/-- A seminorm is continuous at `0` if `p.ball 0 r ∈ 𝓝 0` for *all* `r > 0`.
Over a `NontriviallyNormedField` it is actually enough to check that this is true
for *some* `r`, see `Seminorm.continuousAt_zero'`.  -/
Seminorm.continuousAt_zero_of_forall : ∀ {𝕝 : Type u_6} {E : Type u_7} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕝 E]
  [inst_3 : TopologicalSpace E] {p : Seminorm 𝕝 E}, (∀ r > 0, p.ball 0 r ∈ nhds 0) → ContinuousAt (⇑p) 0
-- Mathlib.Order.DirectedInverseSystem
Equiv.piCongrSet.congr_simp : ∀ {α : Type u_11} {W : α → Sort w} {s t : Set α} (h : s = t), Equiv.piCongrSet h = Equiv.piCongrSet h
-- Init.Data.String.Search
/-- Creates an iterator over all lines in `s` with the line ending characters `\r\n` or `\n` being
stripped.

Examples:

* `"foo\r\nbar\n\nbaz\n".lines.toList  == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]`

* `"foo\r\nbar\n\nbaz".lines.toList  == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]`

* `"foo\r\nbar\n\nbaz\r".lines.toList  == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz\r".toSlice]`
 -/
String.lines : (s : String) → Std.Iter String.Slice
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- If a function applied at a point is 1, a product is unchanged by
removing that point, if present, from a `Finset`.  -/
Finset.prod_erase : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) {f : ι → M} {a : ι},
  f a = 1 → ∏ x ∈ s.erase a, f x = ∏ x ∈ s, f x
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.instAlgebraRatFuncAdicCompl : (K : Type u_2) → [inst : Field K] → Algebra K (LaurentSeries.RatFuncAdicCompl K)
-- Std.Time.Time.Unit.Basic
/-- Converts an `Hour.Offset` to a `Millisecond.Offset`.
 -/
Std.Time.Hour.Offset.toMilliseconds : Std.Time.Hour.Offset → Std.Time.Millisecond.Offset
-- Lean.Data.Lsp.Workspace
Lean.Lsp.WorkspaceFolder.mk.injEq : ∀ (uri : Lean.Lsp.DocumentUri) (name : String) (uri_1 : Lean.Lsp.DocumentUri) (name_1 : String),
  ({ uri := uri, name := name } = { uri := uri_1, name := name_1 }) = (uri = uri_1 ∧ name = name_1)
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.instInhabited : {α ι : Type} → Inhabited (Std.Internal.Parsec ι α)
-- Mathlib.Data.Nat.Choose.Basic
Nat.multichoose.eq_2 : ∀ (n : ℕ), Nat.multichoose 0 n.succ = 0