mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_filter_not_contains_map_fst_of_containsKey_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = false →
      Std.Internal.List.getKey? k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) =
        Std.Internal.List.getKey? k l₁
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.one_mem_iff : ∀ {R : Type u_2} [inst : NonAssocRing R] (I : TwoSidedIdeal R), 1 ∈ I ↔ I = ⊤
-- Mathlib.Combinatorics.SetFamily.Compression.UV
/-- Compressing a family is idempotent.  -/
UV.compression_idem : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  [inst_3 : DecidableEq α] (u v : α) (s : Finset α), UV.compression u v (UV.compression u v s) = UV.compression u v s
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableSMul₂.mk : ∀ {M : Type u_2} {α : Type u_3} [inst : SMul M α] [inst_1 : MeasurableSpace M] [inst_2 : MeasurableSpace α],
  Measurable (Function.uncurry fun x1 x2 => x1 • x2) → MeasurableSMul₂ M α
-- Mathlib.RepresentationTheory.Induced
/-- Given a group hom `φ : G →* H`, `A : Rep k G` and `B : Rep k H`, this is the `k`-linear
isomorphism `(Ind(φ)(A) ⊗ B))_H ⟶ (A ⊗ Res(φ)(B))_G` sending `⟦h ⊗ₜ a⟧ ⊗ₜ b` to `⟦a ⊗ ρ(h)(b)⟧`
for all `h : H`, `a : A`, and `b : B`.  -/
Rep.coinvariantsTensorIndIso : {k : Type u} →
  [inst : CommRing k] →
    {G H : Type u} →
      [inst_1 : Group G] →
        [inst_2 : Group H] →
          (φ : G →* H) →
            (A : Rep.{u, u, u} k G) →
              (B : Rep.{u, u, u} k H) →
                ((Rep.coinvariantsTensor k H).obj (Rep.ind φ A)).obj B ≅
                  ((Rep.coinvariantsTensor k G).obj A).obj (Rep.res φ B)
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_eq_iSup_sum : ∀ {α : Type u_1} {f : α → ENNReal}, ∑' (a : α), f a = ⨆ s, ∑ a ∈ s, f a
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.ofBdd.congr_simp : ∀ {α : Type u_1} (E E_1 : Set α) (e_E : E = E_1) (Indep Indep_1 : Set α → Prop) (e_Indep : Indep = Indep_1)
  (indep_empty : Indep ∅) (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I))
  (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E) (indep_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n),
  IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground indep_bdd =
    IndepMatroid.ofBdd E_1 Indep_1 ⋯ ⋯ ⋯ ⋯ ⋯
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.appendSeq : Array (Lean.TSyntax `tactic) → Lean.TSyntax `tactic → Array (Lean.TSyntax `tactic)
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- See also `Semiring.toModule`  -/
MonoidWithZero.toMulActionWithZero : (M₀ : Type u_2) → [inst : MonoidWithZero M₀] → MulActionWithZero M₀ M₀
-- Mathlib.CategoryTheory.Topos.Sheaf
/-- A construction of a subobject classifier for sheaf categories. `Ω` is the sheaf of closed sieves,
and `truth` maps for each object `X : C`, an element of `PUnit` to the maximal `Sieve X`, which is
always closed.
 -/
CategoryTheory.Sheaf.classifier : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      CategoryTheory.Subobject.Classifier (CategoryTheory.Sheaf J (Type (max u v)))
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.map_snd : ∀ {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] {J : CategoryTheory.Limits.MulticospanShape}
  (d : CategoryTheory.Limits.MulticospanIndex J C) (F : CategoryTheory.Functor C D) (i : J.R),
  (d.map F).snd i = F.map (d.snd i)
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.getLast?.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Mathlib.LinearAlgebra.Reflection
Submodule.mem_invtSubmodule_reflection_of_mem : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x : M}
  {f : Module.Dual R M} (h : f x = 2) (p : Submodule R M), x ∈ p → p ∈ Module.End.invtSubmodule ↑(Module.reflection h)
-- Std.Http.Data.Headers
/-- Filters header key-value pairs, keeping only those that satisfy the predicate.
 -/
Std.Http.Headers.filter : Std.Http.Headers → (Std.Http.Header.Name → Std.Http.Header.Value → Bool) → Std.Http.Headers
-- Mathlib.Algebra.Module.LinearMap.Index
LinearMap.index_zero : ∀ {M : Type u_1} {N : Type u_2} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {R : Type u_3} [inst_2 : Ring R]
  [inst_3 : Module R M] [inst_4 : Module R N], LinearMap.index 0 = ↑(Module.finrank R M) - ↑(Module.finrank R N)
-- Mathlib.Combinatorics.Hindman
/-- Multiplication of ultrafilters given by `∀ᶠ m in U*V, p m ↔ ∀ᶠ m in U, ∀ᶠ m' in V, p (m*m')`.  -/
Ultrafilter.mul : {M : Type u_1} → [Mul M] → Mul (Ultrafilter M)
-- Mathlib.Algebra.Group.End
/-- A stronger version of `mul_right_injective`  -/
Equiv.swap_mul_involutive : ∀ {α : Type u_4} [inst : DecidableEq α] (i j : α), Function.Involutive fun x => Equiv.swap i j * x
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.isStrictMinor_iff_isMinor_ssubset : ∀ {α : Type u_1} {M N : Matroid α}, N <m M ↔ N ≤m M ∧ N.E ⊂ M.E
-- Mathlib.MeasureTheory.Measure.Complex
MeasureTheory.SignedMeasure.toComplexMeasure_apply_re : ∀ {α : Type u_1} {m : MeasurableSpace α} (s t : MeasureTheory.SignedMeasure α) (i : Set α),
  ((s.toComplexMeasure t).measureOf' i).re = s i
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- If a family is affinely independent, so is any subfamily indexed
by a subtype of the index type.  -/
AffineIndependent.subtype : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} {p : ι → P},
  AffineIndependent k p → ∀ (s : Set ι), AffineIndependent k fun i => p ↑i
-- Mathlib.ModelTheory.Algebra.Ring.FreeCommRing
FirstOrder.Ring.realize_termOfFreeCommRing : ∀ {α : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : FirstOrder.Ring.CompatibleRing R] (p : FreeCommRing α)
  (v : α → R), FirstOrder.Language.Term.realize v (FirstOrder.Ring.termOfFreeCommRing p) = (FreeCommRing.lift v) p
-- Init.Data.SInt.Lemmas
Int8.lt_of_lt_of_le : ∀ {a b c : Int8}, a < b → b ≤ c → a < c
-- Mathlib.Analysis.Convex.StdSimplex
convex_stdSimplex : ∀ (𝕜 : Type u_2) (ι : Type u_1) [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : Fintype ι] [IsOrderedRing 𝕜],
  Convex 𝕜 (stdSimplex 𝕜 ι)
-- Mathlib.Data.Fin.Basic
Fin.le_iff_val_le_val : ∀ {n : ℕ} {a b : Fin n}, a ≤ b ↔ ↑a ≤ ↑b
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Finset.sum_product_right : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddCommMonoid β] (s : Finset γ) (t : Finset α) (f : γ × α → β),
  ∑ x ∈ s ×ˢ t, f x = ∑ y ∈ t, ∑ x ∈ s, f (x, y)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullback.lift.congr_simp : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  {arrows : (j : J) → objs j ⟶ B} [inst_1 : CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} (f f_1 : X ⟶ B)
  (e_f : f = f_1) (fs fs_1 : (j : J) → X ⟶ objs j) (e_fs : fs = fs_1)
  (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f),
  CategoryTheory.Limits.WidePullback.lift f fs w = CategoryTheory.Limits.WidePullback.lift f_1 fs_1 ⋯
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.vadd_def : ∀ {α : Type u_1} {β : Type u_2} (f : α → β → β) (l : FreeAddMonoid α) (b : β),
  l +ᵥ b = List.foldr f b (FreeAddMonoid.toList l)
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.GrothendieckTopology C}
  {inst_1 : CategoryTheory.HasWeakSheafify J (Type v)} {toSquare : CategoryTheory.Square C}
  {mono_f₁₃ :
    autoParam (CategoryTheory.Mono toSquare.f₁₃)
      CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mono_f₁₃._autoParam}
  {isPushout : (toSquare.map (CategoryTheory.yoneda.comp (CategoryTheory.presheafToSheaf J (Type v)))).IsPushout}
  {toSquare_1 : CategoryTheory.Square C}
  {mono_f₁₃_1 :
    autoParam (CategoryTheory.Mono toSquare_1.f₁₃)
      CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mono_f₁₃._autoParam}
  {isPushout_1 : (toSquare_1.map (CategoryTheory.yoneda.comp (CategoryTheory.presheafToSheaf J (Type v)))).IsPushout},
  { toSquare := toSquare, mono_f₁₃ := mono_f₁₃, isPushout := isPushout } =
      { toSquare := toSquare_1, mono_f₁₃ := mono_f₁₃_1, isPushout := isPushout_1 } →
    toSquare = toSquare_1
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.mkOrderedRingInst? : Lean.Level →
  Lean.Expr →
    Option Lean.Expr → Option Lean.Expr → Option Lean.Expr → Option Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.eq_div_iff : ∀ {α : Type u} [inst : DivisionMonoid α] {a b c : α}, IsUnit c → (a = b / c ↔ a * c = b)
-- Mathlib.Data.Matrix.Basis
Matrix.single_mul_mul_single : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_7} [inst : DecidableEq l]
  [inst_1 : DecidableEq m] [inst_2 : DecidableEq n] [inst_3 : DecidableEq o] [inst_4 : Fintype m]
  [inst_5 : NonUnitalNonAssocSemiring α] [inst_6 : Fintype n] (i : l) (i' : m) (j' : n) (j : o) (a : α)
  (x : Matrix m n α) (b : α), Matrix.single i i' a * x * Matrix.single j' j b = Matrix.single i j (a * x i' j' * b)
-- Mathlib.RingTheory.Valuation.Basic
/-- The restriction of a valuation so that it takes values in its `valueGroup₀`.  -/
Valuation.restrict : {R : Type u_3} →
  {Γ₀ : Type u_4} →
    [inst : Ring R] →
      [inst_1 : LinearOrderedCommGroupWithZero Γ₀] →
        (v : Valuation R Γ₀) → Valuation R (MonoidWithZeroHom.ofClass v).ValueGroup₀
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.degree_weierstrassMod_lt : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] (f g : PowerSeries A)
  [inst_2 : IsPrecomplete (IsLocalRing.maximalIdeal A) A],
  (f %ʷ g).degree < ↑((PowerSeries.map (IsLocalRing.residue A)) g).order.toNat
-- Mathlib.Data.ENat.Basic
ENat.natCast_ne_top : ∀ (a : ℕ), ↑a ≠ ⊤
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.isBasis_ground_iff : ∀ {α : Type u_1} {M : Matroid α} {B : Set α}, M.IsBasis B M.E ↔ M.IsBase B
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.min_const : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι},
  MeasureTheory.IsStoppingTime f τ → ∀ (i : ι), MeasureTheory.IsStoppingTime f fun ω => min (τ ω) ↑i
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.mem_glpos : ∀ {n : Type u} {R : Type v} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing R] [inst_3 : LinearOrder R]
  [inst_4 : IsStrictOrderedRing R] (A : GL n R), A ∈ Matrix.GLPos n R ↔ 0 < ↑(Matrix.GeneralLinearGroup.det A)
-- Init.Data.String.Basic
String.Slice.Pos.ofSliceTo_inj : ∀ {s : String.Slice} {p₀ : s.Pos} {pos pos' : (s.sliceTo p₀).Pos},
  String.Slice.Pos.ofSliceTo pos = String.Slice.Pos.ofSliceTo pos' ↔ pos = pos'
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `L` are linearly disjoint, then any `F`-linearly independent family on `A` remains
linearly independent over `L`.  -/
IntermediateField.LinearDisjoint.linearIndependent_left : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L → ∀ {ι : Type u_1} {a : ι → ↥A}, LinearIndependent F a → LinearIndependent L (⇑A.val ∘ a)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- The cochain of degree `-1` given by a homotopy between two morphisms of complexes.  -/
CochainComplex.HomComplex.Cochain.ofHomotopy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} → {φ₁ φ₂ : F ⟶ G} → Homotopy φ₁ φ₂ → CochainComplex.HomComplex.Cochain F G (-1)
-- Mathlib.Algebra.Module.FinitePresentation
Module.FinitePresentation.isBaseChange_map : ∀ (R : Type u_4) (M : Type u_5) (N : Type u_6) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (S : Type u_3) [inst_5 : CommRing S] [inst_6 : Algebra R S]
  [Module.Flat R S] [Module.FinitePresentation R M], IsBaseChange S (LinearMap.baseChangeHom R S M N)
-- Mathlib.Algebra.Order.Field.Basic
inv_antitoneOn_Icc_left : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  b < 0 → AntitoneOn (fun x => x⁻¹) (Set.Icc a b)
-- Mathlib.Algebra.Order.Positive.Ring
Positive.coe_add : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : Preorder M] [inst_2 : AddLeftStrictMono M] (x y : { x // 0 < x }),
  ↑(x + y) = ↑x + ↑y
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- If the restriction to a set `s` of a σ-algebra `m` is included in the restriction to `s` of
another σ-algebra `m₂` (hypothesis `hs`), the set `s` is `m` measurable and a function `f` supported
on `s` is `m`-strongly-measurable, then `f` is also `m₂`-strongly-measurable.  -/
MeasureTheory.StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_on : ∀ {α : Type u_5} {E : Type u_6} {m m₂ : MeasurableSpace α} [inst : TopologicalSpace E] [inst_1 : Zero E] {s : Set α}
  {f : α → E},
  MeasurableSet s →
    (∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)) →
      MeasureTheory.StronglyMeasurable f → (∀ x ∉ s, f x = 0) → MeasureTheory.StronglyMeasurable f
-- Mathlib.NumberTheory.Primorial
primorial_zero : primorial 0 = 1
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofMkLEMk_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ A₂ : C} {f : A₁ ⟶ B} {g : A₂ ⟶ B}
  [inst_1 : CategoryTheory.Mono f] [inst_2 : CategoryTheory.Mono g]
  (h : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLEMk f g h) g = f
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegal.spineToSimplex_spine_apply : ∀ {X : SSet} (sx : X.StrictSegal) {n : ℕ} (Δ : X.obj (Opposite.op { len := n })), sx.spineToSimplex (X.spine n Δ) = Δ
-- Mathlib.Data.Vector3
Vector3.consElim_cons : ∀ {α : Type u_1} {n : ℕ} {C : Vector3 α (n + 1) → Sort u_2} {H : (a : α) → (t : Vector3 α n) → C (Vector3.cons a t)}
  {a : α} {t : Vector3 α n}, Vector3.consElim H (Vector3.cons a t) = H a t
-- Mathlib.Algebra.Order.GroupWithZero.Defs
MulRightMono.toMulPosReflectLT : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [MulRightReflectLT α], MulPosReflectLT α
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.op_apply_symm_apply : ∀ {α : Type u_7} {β : Type u_8} [inst : Add α] [inst_1 : Mul α] [inst_2 : Add β] [inst_3 : Mul β] (f : α ≃+* β)
  (a : βᵐᵒᵖ), (RingEquiv.op f).symm a = MulOpposite.op (f.symm (MulOpposite.unop a))
-- Mathlib.Order.Hom.CompleteLattice
/-- Composition of `sInfHom`s as a `sInfHom`.  -/
sInfHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : InfSet α] → [inst_1 : InfSet β] → [inst_2 : InfSet γ] → sInfHom β γ → sInfHom α β → sInfHom α γ
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- **Alias** of `Memℓp.finsetSum`. -/
Memℓp.finset_sum : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {ι : Type u_5}
  (s : Finset ι) {f : ι → (i : α) → E i}, (∀ i ∈ s, Memℓp (f i) p) → Memℓp (fun a => ∑ i ∈ s, f i a) p
-- Mathlib.Data.Set.Function
Set.graphOn_univ_injective : ∀ {α : Type u_1} {β : Type u_2}, Function.Injective fun f => Set.graphOn f Set.univ
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- Flattening nested `iConvexComb`s.

See `iConvexComb_assoc'`, `iConvexComb_assoc''` for more dependent versions.  -/
Convexity.iConvexComb_assoc : ∀ {R : Type u_1} {M : Type u_3} {I : Type u_6} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] {J : Type u_9} (s : Convexity.StdSimplex R I)
  (f : I → Convexity.StdSimplex R J) (g : J → M),
  (Convexity.iConvexComb s fun i => Convexity.iConvexComb (f i) g) = Convexity.iConvexComb (Convexity.iConvexComb s f) g
-- Mathlib.LinearAlgebra.Projectivization.Action
/-- The special linear group `SpecialLinearGroup K V` acts primitively on `ℙ K V`.  -/
Projectivization.instIsPreprimitiveSpecialLinearGroup : ∀ {K : Type u_1} {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Field K] [inst_2 : Module K V],
  MulAction.IsPreprimitive (SpecialLinearGroup K V) (Projectivization K V)
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_sub_ofNat : ∀ (r : ENNReal) (n : ℕ) [inst : n.AtLeastTwo], ⌊r - OfNat.ofNat n⌋ₑ = ⌊r⌋ₑ - OfNat.ofNat n
-- Lean.Meta.LazyDiscrTree
/-- Contains the pre discrimination tree and any errors occurring during initialization of
the library search tree.
 -/
Lean.Meta.LazyDiscrTree.InitResults : Type → Type
-- Std.Data.Iterators.Lemmas.Producers.Monadic.List
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.List.0.Std.Iterators.Types.ListIterator.instIterator.match_1.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} (motive : Std.IterStep (Std.IterM m α) α → Sort u_3) (it' : Std.IterM m α)
  (out : α) (h_1 : (it' : Std.IterM m α) → (out : α) → motive (Std.IterStep.yield it' out))
  (h_2 : (it : Std.IterM m α) → motive (Std.IterStep.skip it)) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.getEntryLT! : {α : Type u} → {β : Type v} → [Ord α] → [Inhabited (α × β)] → α → (Std.DTreeMap.Internal.Impl α fun x => β) → α × β
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.lower_le_upper : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι), I.lower ≤ I.upper
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α} {h_mem : k ∈ t₁ \ t₂},
  Std.ExtDTreeMap.Const.get (t₁ \ t₂) k h_mem = Std.ExtDTreeMap.Const.get t₁ k ⋯
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.instHasPullbacks : CategoryTheory.Limits.HasPullbacks AlgebraicGeometry.Scheme
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- Postcomposing `f` with `Prod.snd` is `C^n` at `x`  -/
ContDiffWithinAt.snd : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {n : WithTop ℕ∞} {f : E → F × G} {x : E},
  ContDiffWithinAt 𝕜 n f s x → ContDiffWithinAt 𝕜 n (fun x => (f x).2) s x
-- Mathlib.Data.Finsupp.Weight
Finsupp.finite_of_degree_lt : ∀ {σ : Type u_1} [Finite σ] (n : ℕ), {f | Finsupp.degree f < n}.Finite
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
/-- Helper construction for `liftToFinsetColimIso`.  -/
CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimIso_aux : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type w}
  [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape (Finset (CategoryTheory.Discrete α)) C]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete α) C]
  (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) {J : Finset (CategoryTheory.Discrete α)} (j : ↥J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun x => F.obj ↑x) j)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj F) J)
        (CategoryTheory.Limits.colimit.isoColimitCocone
            (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone F)).inv) =
    CategoryTheory.Limits.colimit.ι F ↑j
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.centralMoment_one : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsZeroOrProbabilityMeasure μ], ProbabilityTheory.centralMoment X 1 μ = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMulticospan.right : {J : CategoryTheory.Limits.MulticospanShape} → J.R → CategoryTheory.Limits.WalkingMulticospan J
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.maxEntry_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → ∀ (h : t₁.Equiv t₂) {he : t₁.isEmpty = false}, t₁.maxEntry he = t₂.maxEntry ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The inclusion functor `WalkingMultispan (.ofLinearOrder ι) ⥤ WalkingMultispan (.prod ι)`.  -/
CategoryTheory.Limits.WalkingMultispan.inclusionOfLinearOrder : (ι : Type w) →
  [inst : LinearOrder ι] →
    CategoryTheory.Functor
      (CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι))
      (CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.MultispanShape.prod ι))
-- Mathlib.Data.PFun
PFun.prodMap.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) (x : α × β),
  f.prodMap g x = { Dom := (f x.1).Dom ∧ (g x.2).Dom, get := fun h => ((f x.1).get ⋯, (g x.2).get ⋯) }
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
LinearIsometryEquiv.differentiable : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (iso : E ≃ₗᵢ[𝕜] F), Differentiable 𝕜 ⇑iso
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_alter_eq_self_of_not_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, k ∉ t → (f t[k]?).isNone = true → (t.alter k f).size = t.size
-- Init.Prelude
Nat.ne_of_beq_eq_false : ∀ {n m : ℕ}, n.beq m = false → ¬n = m
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
/-- Semilinear sets are closed under additive closure.  -/
IsSemilinearSet.closure : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : Set M}, IsSemilinearSet s → IsSemilinearSet ↑(AddSubmonoid.closure s)
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.re_smul : ∀ (g : GL (Fin 2) ℝ) (z : UpperHalfPlane), (g • z).re = (UpperHalfPlane.num g ↑z / UpperHalfPlane.denom g ↑z).re
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.coe_toAlgEquiv : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B), ⇑e.toAlgEquiv = ⇑e
-- Mathlib.Analysis.Complex.AbelLimit
Complex.tendsto_tsum_powerSeries_nhdsWithin_lt : ∀ {f : ℕ → ℂ} {l : ℂ},
  Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds l) →
    Filter.Tendsto (fun z => ∑' (n : ℕ), f n * z ^ n) (Filter.map Complex.ofReal (nhdsWithin 1 (Set.Iio 1))) (nhds l)