mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Instances.Matrix
summable_matrix_blockDiagonal : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [inst : AddCommMonoid R]
  [inst_1 : TopologicalSpace R] {L : SummationFilter X} [inst_2 : DecidableEq p] {f : X → p → Matrix m n R},
  Summable (fun x => Matrix.blockDiagonal (f x)) L ↔ Summable f L
-- Init.Grind.ToIntLemmas
Lean.Grind.IntInterval.lo?.eq_2 : ∀ (lo : ℤ), (Lean.Grind.IntInterval.ci lo).lo? = some lo
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A binary bicone for a pair of objects `P Q : C` consists of the cone point `X`,
maps from `X` to both `P` and `Q`, and maps from both `P` and `Q` to `X`,
so that `inl ≫ fst = 𝟙 P`, `inl ≫ snd = 0`, `inr ≫ fst = 0`, and `inr ≫ snd = 𝟙 Q`  -/
CategoryTheory.Limits.BinaryBicone.inl_fst : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q),
  CategoryTheory.CategoryStruct.comp self.inl self.fst = CategoryTheory.CategoryStruct.id P
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_alter_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {f : Option β → Option β}, (m.alter k f).getKey? k = if (f m[k]?).isSome = true then some k else none
-- Mathlib.RingTheory.Polynomial.SmallDegreeVieta
/-- **Vieta's formula** for quadratics as an iff (`aroots, Field` version).  -/
Polynomial.aroots_quadratic_eq_pair_iff_of_ne_zero' : ∀ {T : Type u_2} {S : Type u_3} [inst : CommRing T] [inst_1 : Field S] [inst_2 : Algebra T S] {a b c : T} {x1 x2 : S},
  (algebraMap T S) a ≠ 0 →
    ((Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).aroots S = {x1, x2} ↔
      x1 + x2 = -(algebraMap T S) b / (algebraMap T S) a ∧ x1 * x2 = (algebraMap T S) c / (algebraMap T S) a)
-- Mathlib.Data.Fin.Fin2
_private.Mathlib.Data.Fin.Fin2.0.Fin2.add.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match 0 with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_1 ()
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.mapAlgAut_apply : ∀ (R : Type u_1) {A : Type u_4} (M : Type u_7) [inst : CommSemiring R] [inst_1 : AddMonoid M] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] (f : A ≃ₐ[R] A), (AddMonoidAlgebra.mapAlgAut R M) f = AddMonoidAlgebra.mapAlgEquiv R M f
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCocycle.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : CategoryTheory.Functor Cᵒᵖ GrpCat} {I : Type w'}
  {U : I → C} (toOneCochain : CategoryTheory.PresheafOfGroups.OneCochain G U)
  (ev_trans :
    autoParam
      (∀ (i j k : I) ⦃T : C⦄ (a : T ⟶ U i) (b : T ⟶ U j) (c : T ⟶ U k),
        toOneCochain.ev i j a b * toOneCochain.ev j k b c = toOneCochain.ev i k a c)
      CategoryTheory.PresheafOfGroups.OneCocycle.ev_trans._autoParam)
  (toOneCochain_1 : CategoryTheory.PresheafOfGroups.OneCochain G U)
  (ev_trans_1 :
    autoParam
      (∀ (i j k : I) ⦃T : C⦄ (a : T ⟶ U i) (b : T ⟶ U j) (c : T ⟶ U k),
        toOneCochain_1.ev i j a b * toOneCochain_1.ev j k b c = toOneCochain_1.ev i k a c)
      CategoryTheory.PresheafOfGroups.OneCocycle.ev_trans._autoParam),
  ({ toOneCochain := toOneCochain, ev_trans := ev_trans } =
      { toOneCochain := toOneCochain_1, ev_trans := ev_trans_1 }) =
    (toOneCochain = toOneCochain_1)
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The composition of `C^n` functions at points in domains is `C^n`,
with a weaker condition on `s` and `t`.  -/
ContDiffWithinAt.comp_of_mem_nhdsWithin_image_of_eq : ∀ {𝕜 : 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] {n : WithTop ℕ∞} {s : Set E} {t : Set F} {g : F → G}
  {f : E → F} {y : F} (x : E),
  ContDiffWithinAt 𝕜 n g t y →
    ContDiffWithinAt 𝕜 n f s x → t ∈ nhdsWithin (f x) (f '' s) → f x = y → ContDiffWithinAt 𝕜 n (g ∘ f) s x
-- Mathlib.Data.Stream.Init
Stream'.even_interleave : ∀ {α : Type u} (s₁ s₂ : Stream' α), (s₁ ⋈ s₂).even = s₁
-- Mathlib.MeasureTheory.Function.AEEqOfLIntegral
MeasureTheory.ae_const_le_iff_forall_lt_measure_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_2} [inst : LinearOrder β]
  [inst_1 : TopologicalSpace β] [OrderTopology β] [FirstCountableTopology β] (f : α → β) (c : β),
  (∀ᵐ (x : α) ∂μ, c ≤ f x) ↔ ∀ b < c, μ {x | f x ≤ b} = 0
-- Mathlib.Analysis.ODE.ExistUnique
/-- **Picard-Lindelöf (Cauchy-Lipschitz) theorem**, differential form.  -/
IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt₀ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E}
  {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a L K : NNReal},
  IsPicardLindelof f t₀ x₀ a 0 L K →
    ∃ α, α ↑t₀ = x₀ ∧ ∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Set.Icc tmin tmax) t
-- Init.Data.Vector.Lex
Vector.lex_toList : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {lt : α → α → Bool} {xs ys : Vector α n},
  xs.toList.lex ys.toList lt = xs.lex ys lt
-- Mathlib.Order.Basic
LT.lt.lt_or_gt : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, b < a → ∀ (c : α), c < a ∨ b < c
-- Mathlib.CategoryTheory.EssentialImage
CategoryTheory.Functor.essImage.liftFunctorCompIso_hom_app : ∀ {J : Type u_1} {C : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  (G : CategoryTheory.Functor J D) (F : CategoryTheory.Functor C D) [inst_3 : F.Full] [inst_4 : F.Faithful]
  (hG : ∀ (j : J), F.essImage (G.obj j)) (X : J),
  (CategoryTheory.Functor.essImage.liftFunctorCompIso G F hG).hom.app X =
    (F.toEssImage.objObjPreimageIso { obj := G.obj X, property := ⋯ }).hom.hom
-- Lean.Declaration
Lean.ConstructorVal.mk.sizeOf_spec : ∀ (toConstantVal : Lean.ConstantVal) (induct : Lean.Name) (cidx numParams numFields : ℕ) (isUnsafe : Bool),
  sizeOf
      { toConstantVal := toConstantVal, induct := induct, cidx := cidx, numParams := numParams, numFields := numFields,
        isUnsafe := isUnsafe } =
    1 + sizeOf toConstantVal + sizeOf induct + sizeOf cidx + sizeOf numParams + sizeOf numFields + sizeOf isUnsafe
-- Mathlib.Data.Fin.VecNotation
Matrix.vecHead_vecAlt1 : ∀ {α : Type u} {m n : ℕ} (hm : m + 2 = n + 1 + (n + 1)) (v : Fin (m + 2) → α),
  Matrix.vecHead (Matrix.vecAlt1 hm v) = v 1
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_dvd_prod_of_subset_of_dvd : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] {f1 f2 : α →₀ M}
  {g1 g2 : α → M → N}, f1.support ⊆ f2.support → (∀ a ∈ f1.support, g1 a (f1 a) ∣ g2 a (f2 a)) → f1.prod g1 ∣ f2.prod g2
-- Mathlib.Data.ENNReal.Inv
ENNReal.ofReal_inv_le : ∀ {x : ℝ}, ENNReal.ofReal x⁻¹ ≤ (ENNReal.ofReal x)⁻¹
-- Mathlib.Algebra.Group.Action.Pi
Pi.faithfulVAdd : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [Nonempty ι] [inst : (i : ι) → VAdd M (α i)]
  [∀ (i : ι), Nonempty (α i)] [∀ (i : ι), FaithfulVAdd M (α i)], FaithfulVAdd M ((i : ι) → α i)
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.IsLoop.of_isMinor : ∀ {α : Type u_1} {M N : Matroid α} {e : α}, M.IsLoop e → e ∈ N.E → N ≤m M → N.IsLoop e
-- Mathlib.LinearAlgebra.Matrix.IsDiag
/-- A symmetric block matrix `A.fromBlocks B C D` is diagonal
if `A` and `D` are diagonal and `B` is `0`.  -/
Matrix.IsDiag.fromBlocks_of_isSymm : ∀ {α : Type u_1} {n : Type u_4} {m : Type u_5} [inst : Zero α] {A : Matrix m m α} {C : Matrix n m α} {D : Matrix n n α},
  (Matrix.fromBlocks A 0 C D).IsSymm → A.IsDiag → D.IsDiag → (Matrix.fromBlocks A 0 C D).IsDiag
-- Mathlib.MeasureTheory.Measure.AEMeasurable
aemeasurable_uIoc_iff : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  [inst_1 : LinearOrder α] {f : α → β} {a b : α},
  AEMeasurable f (μ.restrict (Set.uIoc a b)) ↔
    AEMeasurable f (μ.restrict (Set.Ioc a b)) ∧ AEMeasurable f (μ.restrict (Set.Ioc b a))
-- Mathlib.RingTheory.Ideal.Over
Ideal.over_under : ∀ {A : Type u_2} [inst : CommSemiring A] {B : Type u_3} [inst_1 : Semiring B] [inst_2 : Algebra A B] (P : Ideal B),
  P.LiesOver (Ideal.under A P)
-- Mathlib.NumberTheory.Chebyshev
Nat.lcmUpto_dvd_factorial : ∀ (n : ℕ), n.lcmUpto ∣ n.factorial
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.Abelian.image.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C}
  (f f_1 : P ⟶ Q) (e_f : f = f_1) [inst_2 : CategoryTheory.Limits.HasCokernel f]
  [inst_3 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)],
  CategoryTheory.Abelian.image f = CategoryTheory.Abelian.image f_1
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.order_mul_of_ne_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R},
  x.leadingCoeff * y.leadingCoeff ≠ 0 → (x * y).order = x.order + y.order
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.NatTrans.app_homology : ∀ {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.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {F G : CategoryTheory.Functor C D} (τ : F ⟶ G)
  (S : CategoryTheory.ShortComplex C) [inst_4 : S.HasHomology] [inst_5 : F.PreservesZeroMorphisms]
  [inst_6 : G.PreservesZeroMorphisms] [inst_7 : F.PreservesLeftHomologyOf S] [inst_8 : G.PreservesLeftHomologyOf S]
  [inst_9 : F.PreservesRightHomologyOf S] [inst_10 : G.PreservesRightHomologyOf S],
  τ.app S.homology =
    CategoryTheory.CategoryStruct.comp (S.mapHomologyIso F).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (S.mapNatTrans τ))
        (S.mapHomologyIso G).hom)
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.expansion_nonneg : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {A S : Finset G},
  K ≤ 1 → S.Nonempty → 0 ≤ Finset.expansion✝ K S A
-- Init.Data.Rat.Lemmas
Rat.den_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).den = 1
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.Slice.intercalate.go.match_1.eq_2 : ∀ (motive : List String.Slice → Sort u_1) (h_1 : (a : String.Slice) → (as : List String.Slice) → motive (a :: as))
  (h_2 : Unit → motive []),
  (match [] with
    | a :: as => h_1 a as
    | [] => h_2 ()) =
    h_2 ()