mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens)
  {Z : CommRingCat} (h : Y.presheaf.obj (Opposite.op (AlgebraicGeometry.Scheme.Hom.opensRange f ⊓ U)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsOpenImmersion.ΓIso f U).hom h) =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) h
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput.rhs_cast : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig1 aig2 : Std.Sat.AIG α}
  (s : Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig1) (hcast : aig1.decls.size ≤ aig2.decls.size),
  (s.cast hcast).rhs = s.rhs.cast hcast
-- Mathlib.Algebra.CharP.Lemmas
add_pow_char : ∀ {R : Type u_1} [inst : CommSemiring R] (x y : R) (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p],
  (x + y) ^ p = x ^ p + y ^ p
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
/-- The (local) interval version of the *Lebesgue Differentiation Theorem*: if `f : ℝ → E` is
interval integrable on `a..b`, then for almost every `x ∈ uIcc a b`, for any `c ∈ uIcc a b`, the
derivative of `∫ (t : ℝ) in c..x, f t` at `x` is equal to `f x`.  -/
IntervalIntegrable.ae_hasDerivAt_integral : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    ∀ᵐ (x : ℝ), x ∈ Set.uIcc a b → ∀ c ∈ Set.uIcc a b, HasDerivAt (fun x => ∫ (t : ℝ) in c..x, f t) (f x) x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKeyD_eq_headD_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {fallback : α}, t.minKeyD fallback = t.keys.headD fallback
-- Init.Data.List.Nat.Sum
List.sum_div_length_le_max_nat : ∀ {xs : List ℕ} (h : xs ≠ []), xs.sum / xs.length ≤ xs.max h
-- Mathlib.RingTheory.FilteredAlgebra.Basic
/-- For `F` satisfying `IsRingFiltration F F_lt` in a semiring `R` and `σM` a family of subsets of
an `R`-module `M`, an increasing series `FM` in `σM` is a module filtration if `IsFiltration F F_lt`
and the pointwise scalar multiplication of `F i` and `FM j` is in `F (i +ᵥ j)`.

The index set `ιM` for the module can be more general, however usually we take `ιM = ι`.  -/
IsModuleFiltration : {ι : Type u_1} →
  {ιM : Type u_2} →
    {R : Type u_3} →
      {M : Type u_4} →
        {σ : Type u_5} →
          {σM : Type u_6} →
            [inst : AddMonoid ι] →
              [inst_1 : PartialOrder ι] →
                [PartialOrder ιM] →
                  [VAdd ι ιM] →
                    [inst_4 : Preorder σ] →
                      [inst_5 : Semiring R] →
                        [inst_6 : SetLike σ R] →
                          [Preorder σM] →
                            [inst_8 : AddCommMonoid M] →
                              [Module R M] →
                                [SetLike σM M] →
                                  (F : ι → σ) →
                                    (F_lt : outParam (ι → σ)) →
                                      [IsRingFiltration F F_lt] → (ιM → σM) → outParam (ιM → σM) → Prop
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
Prod.instLieGroup : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] [LieGroup I n G] {E' : Type u_5}
  [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_10 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_7} [inst_11 : TopologicalSpace G'] [inst_12 : ChartedSpace H' G']
  [inst_13 : Group G'] [LieGroup I' n G'], LieGroup (I.prod I') n (G × G')
-- Mathlib.Analysis.Seminorm
Seminorm.finset_sup_apply_le : ∀ {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] {p : ι → Seminorm 𝕜 E} {s : Finset ι} {x : E} {a : ℝ},
  0 ≤ a → (∀ i ∈ s, (p i) x ≤ a) → (s.sup p) x ≤ a
-- Mathlib.Logic.Hydra
Relation.cutExpand_le_invImage_lex : ∀ {α : Type u_1} {r : α → α → Prop} [inst : DecidableEq α] [Std.Irrefl r],
  Relation.CutExpand r ≤ InvImage (Finsupp.Lex (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) fun x1 x2 => x1 < x2) ⇑Multiset.toFinsupp
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.foldl_eq_foldl_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : δ → α → β → δ} {init : δ},
  Std.ExtDTreeMap.foldl f init t = List.foldl (fun a b => f a b.1 b.2) init (Std.ExtDTreeMap.Const.toList t)
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
/-- A rational number has only finitely many good rational approximations.  -/
Rat.finite_rat_abs_sub_lt_one_div_den_sq : ∀ (ξ : ℚ), {q | |ξ - q| < 1 / ↑q.den ^ 2}.Finite
-- Mathlib.Analysis.Meromorphic.Divisor
/-- The divisor of a constant function is `0`.
 -/
MeromorphicOn.divisor_intCast : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} (n : ℤ), MeromorphicOn.divisor (↑n) U = 0
-- Mathlib.Algebra.Group.Defs
IsAddCyclic.mk : ∀ {G : Type u} [inst : SMul ℤ G], (∃ g, Function.Surjective fun x => x • g) → IsAddCyclic G
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicones.functoriality_map_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type uD} [inst_2 : CategoryTheory.Category.{uD', uD} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (P Q : C) (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms]
  {X Y : CategoryTheory.Limits.BinaryBicone P Q} (f : X ⟶ Y),
  ((CategoryTheory.Limits.BinaryBicones.functoriality P Q F).map f).hom = F.map f.hom
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.evaluation_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (X : Cᵒᵖ)
  (M : PresheafOfModules R), (PresheafOfModules.evaluation R X).obj M = M.obj X
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
/-- For each nonempty, directed set `s` which is bounded above, `sSup s` is
the least upper bound of `s`.  -/
ConditionallyCompletePartialOrderSup.isLUB_csSup_of_directed : ∀ {α : Type u_3} [self : ConditionallyCompletePartialOrderSup α] (s : Set α),
  DirectedOn (fun x1 x2 => x1 ≤ x2) s → s.Nonempty → BddAbove s → IsLUB s (sSup s)