mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.TensorProduct.Free
Module.Basis.baseChange_linearMap : ∀ {R : Type u_1} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Fintype ι] {ι' : Type u_3} {N : Type u_4} [inst_4 : Fintype ι'] [inst_5 : DecidableEq ι']
  [inst_6 : AddCommMonoid N] [inst_7 : Module R N] (A : Type u_5) [inst_8 : CommSemiring A] [inst_9 : Algebra R A]
  (b : Module.Basis ι R M) (b' : Module.Basis ι' R N) (ij : ι × ι'),
  LinearMap.baseChange A ((b'.linearMap b) ij) =
    ((Algebra.TensorProduct.basis A b').linearMap (Algebra.TensorProduct.basis A b)) ij
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.measurePreserving_funUnique : ∀ {β : Type u} {_m : MeasurableSpace β} (μ : MeasureTheory.Measure β) (α : Type v) [inst : Unique α],
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.funUnique α β)) (MeasureTheory.Measure.pi fun x => μ) μ
-- Mathlib.Order.Cover
/-- If `a`, `b`, `c` are consecutive and `a < x < c` then `x = b`.  -/
CovBy.eq_of_between : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c x : α}, a ⋖ b → b ⋖ c → a < x → x < c → x = b
-- Mathlib.Tactic.DefEqTransformations
/-- `eta_reduce at loc` eta reduces all sub-expressions at the given location.
This also exists as a `conv`-mode tactic.

For example, `fun x y => f x y` becomes `f` after eta reduction.
 -/
Mathlib.Tactic.convEta_reduce : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
CategoryTheory.MonoidalCategory.externalProductCompDiagIso_hom_app_app : ∀ (J₁ : Type u₁) (C : Type u₃) [inst : CategoryTheory.Category.{v₁, u₁} J₁]
  [inst_1 : CategoryTheory.Category.{v₃, u₃} C] [inst_2 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Functor J₁ C × CategoryTheory.Functor J₁ C) (X_1 : J₁),
  ((CategoryTheory.MonoidalCategory.externalProductCompDiagIso J₁ C).hom.app X).app X_1 =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (X.1.obj X_1) (X.2.obj X_1))
-- Mathlib.Order.Heyting.Hom
HeytingHom.instInhabited : {α : Type u_2} → [inst : HeytingAlgebra α] → Inhabited (HeytingHom α α)
-- Mathlib.Analysis.Convex.Between
Wbtw.trans_right_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {w x y z : P},
  Wbtw R w x z → Wbtw R x y z → Wbtw R w x y
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.fst_comp_inr : ∀ (R : Type u) {M : Type v} [inst : Zero R], TrivSqZeroExt.fst ∘ TrivSqZeroExt.inr = 0
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.EffectiveEquivalenceRelation.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R A : C} →
      {p₁ p₂ : R ⟶ A} →
        CategoryTheory.EquivalenceRelation p₁ p₂ →
          (B : C) →
            (π : A ⟶ B) →
              CategoryTheory.IsKernelPair π p₁ p₂ →
                CategoryTheory.IsPushout p₁ p₂ π π → CategoryTheory.EffectiveEquivalenceRelation p₁ p₂
-- Mathlib.Algebra.GradedMonoid
/-- If `R` acts on each `A i`, then it acts on `GradedMonoid A` via the `.2` projection.  -/
GradedMonoid.instSMul : {ι : Type u_1} → {α : Type u_3} → {A : ι → Type u_2} → [(i : ι) → SMul α (A i)] → SMul α (GradedMonoid A)
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.CoreUnitCounit.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {unit : CategoryTheory.Functor.id C ⟶ F.comp G}
  {counit : G.comp F ⟶ CategoryTheory.Functor.id D}
  {left_triangle :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight unit F)
          (CategoryTheory.CategoryStruct.comp (F.associator G F).hom (F.whiskerLeft counit)) =
        CategoryTheory.NatTrans.id ((CategoryTheory.Functor.id C).comp F))
      CategoryTheory.Adjunction.CoreUnitCounit.left_triangle._autoParam}
  {right_triangle :
    autoParam
      (CategoryTheory.CategoryStruct.comp (G.whiskerLeft unit)
          (CategoryTheory.CategoryStruct.comp (G.associator F G).inv (CategoryTheory.Functor.whiskerRight counit G)) =
        CategoryTheory.NatTrans.id (G.comp (CategoryTheory.Functor.id C)))
      CategoryTheory.Adjunction.CoreUnitCounit.right_triangle._autoParam}
  {unit_1 : CategoryTheory.Functor.id C ⟶ F.comp G} {counit_1 : G.comp F ⟶ CategoryTheory.Functor.id D}
  {left_triangle_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight unit_1 F)
          (CategoryTheory.CategoryStruct.comp (F.associator G F).hom (F.whiskerLeft counit_1)) =
        CategoryTheory.NatTrans.id ((CategoryTheory.Functor.id C).comp F))
      CategoryTheory.Adjunction.CoreUnitCounit.left_triangle._autoParam}
  {right_triangle_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp (G.whiskerLeft unit_1)
          (CategoryTheory.CategoryStruct.comp (G.associator F G).inv (CategoryTheory.Functor.whiskerRight counit_1 G)) =
        CategoryTheory.NatTrans.id (G.comp (CategoryTheory.Functor.id C)))
      CategoryTheory.Adjunction.CoreUnitCounit.right_triangle._autoParam},
  { unit := unit, counit := counit, left_triangle := left_triangle, right_triangle := right_triangle } =
      { unit := unit_1, counit := counit_1, left_triangle := left_triangle_1, right_triangle := right_triangle_1 } →
    unit = unit_1 ∧ counit = counit_1
-- Init.Data.Slice.Array.Lemmas
Subarray.toList_mkSlice_roc : ∀ {α : Type u_1} {xs : Subarray α} {lo hi : ℕ},
  Std.Slice.toList (Std.Roc.Sliceable.mkSlice xs lo<...=hi) =
    List.drop (lo + 1) (List.take (hi + 1) (Std.Slice.toList xs))
-- Batteries.Data.Int
Int.testBit_ofBits_lt : ∀ {n i : ℕ} {f : Fin n → Bool} (h : i < n), (Int.ofBits f).testBit i = f ⟨i, h⟩
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.balance2.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → α → RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α)
  (b : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α) (z : α) (d : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive a x (RBTree.RBNode.node RBTree.RBColor.red b y (RBTree.RBNode.node RBTree.RBColor.red c z d)))
  (h_2 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive a x (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red b y c) z d))
  (h_3 : (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive a x b),
  (match a, x, RBTree.RBNode.node RBTree.RBColor.red b y (RBTree.RBNode.node RBTree.RBColor.red c z d) with
    | a, x, RBTree.RBNode.node RBTree.RBColor.red b y (RBTree.RBNode.node RBTree.RBColor.red c z d) => h_1 a x b y c z d
    | a, x, RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red b y c) z d => h_2 a x b y c z d
    | a, x, b => h_3 a x b) =
    h_1 a x b y c z d
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translationNumber_one : CircleDeg1Lift.translationNumber 1 = 0
-- Lean.Parser.Extension
_private.Lean.Parser.Extension.0.Lean.Parser.addTokenConfig : Lean.Parser.TokenTable → Lean.Parser.Token → Except String Lean.Parser.TokenTable
-- Init.Data.Ord.Basic
/-- Compares two values by comparing the results of applying a function.

In particular, `x` is compared to `y` by comparing `f x` and `f y`.

Examples:
* `compareOn (·.length) "apple" "banana" = .lt`
* `compareOn (· % 3) 5 6 = .gt`
* `compareOn (·.foldl max 0) [1, 2, 3] [3, 2, 1] = .eq`
 -/
compareOn : {β : Type u_1} → {α : Sort u_2} → [ord : Ord β] → (α → β) → α → α → Ordering
-- Mathlib.NumberTheory.ModularForms.LevelOne.Basic
SlashInvariantForm.slash_action_generators_SL2Z : ∀ {f : UpperHalfPlane → ℂ} {k : ℤ},
  SlashAction.map k ModularGroup.S f = f →
    SlashAction.map k ModularGroup.T f = f → ∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ), SlashAction.map k γ f = f
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
AEMeasurable.coe_real_ereal : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → ℝ} {μ : MeasureTheory.Measure α},
  AEMeasurable f μ → AEMeasurable (fun x => ↑(f x)) μ
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.ComonObj.instTensorUnit_comul : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.ComonObj.comul =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.prod_leftInvSeq : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B),
  (cs.leftInvSeq ω).prod = (cs.wordProd ω)⁻¹
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.indToCoindAux_of_not_rel : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] {A : Rep.{w, u, v} k ↥S} (g g₁ : G) (a : ↑A),
  ¬(QuotientGroup.rightRel S) g₁ g → (A.indToCoindAux g) a g₁ = 0
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.coe_vadd : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {R : Type u_4} [inst_1 : VAdd R Y] (r : R)
  (f : LocallyConstant X Y), ⇑(r +ᵥ f) = r +ᵥ ⇑f
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiff_of_contMDiffOn_iUnion_of_isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {f : M → M'}
  {n : WithTop ℕ∞} {ι : Type u_11} {s : ι → Set M},
  (∀ (i : ι), ContMDiffOn I I' n f (s i)) → (∀ (i : ι), IsOpen (s i)) → ⋃ i, s i = Set.univ → ContMDiff I I' n f
-- Mathlib.Algebra.Order.Pi
Pi.single_nonneg : ∀ {ι : Type u_6} {α : ι → Type u_7} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (α i)]
  [inst_2 : (i : ι) → Preorder (α i)] {i : ι} {a : α i}, 0 ≤ Pi.single i a ↔ 0 ≤ a
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.id_tensor_associator_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z Z' : C}
  (h : Z ⟶ Z') {Z_1 : C}
  (h_1 :
    CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z') ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom
        (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z').hom h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X)
          (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id Y) h))
        h_1)
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.add_neg_eq_iff_eq_add : ∀ {α : Type u} [inst : SubtractionMonoid α] {a b c : α}, IsAddUnit b → (a + -b = c ↔ a = c + b)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₁₀.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.d₁₀ A = ModuleCat.ofHom ((Finsupp.lsum k) fun g => A.ρ g⁻¹ - LinearMap.id)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- the second component of `f : Hom x y` is a morphism `x.snd ⟶ y.snd`  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.snd : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                {X : Type u₄} →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] →
                    {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} →
                      CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom X x y → (x.snd ⟶ y.snd)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.support_nodup : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.IsPath → p.support.Nodup
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.denoteS_ofMon : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (m : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.Poly.denoteS ctx (Lean.Grind.CommRing.Poly.ofMon m) = Lean.Grind.CommRing.Mon.denote ctx m
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.instLattice.eq_1 : ∀ {E : Type u_3} [inst : CommGroup E],
  GroupSeminorm.instLattice =
    { toSemilatticeSup := GroupSeminorm.semilatticeSup, inf := fun x1 x2 => x1 ⊓ x2, inf_le_left := ⋯,
      inf_le_right := ⋯, le_inf := ⋯ }
-- Mathlib.CategoryTheory.Abelian.Ext
/-- `Ext` can be computed using a projective resolution.  -/
CategoryTheory.ProjectiveResolution.isoExt : {R : Type u_1} →
  [inst : Ring R] →
    {C : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
        [inst_2 : CategoryTheory.Abelian C] →
          [inst_3 : CategoryTheory.Linear R C] →
            [inst_4 : CategoryTheory.EnoughProjectives C] →
              {X : C} →
                (P : CategoryTheory.ProjectiveResolution X) →
                  (n : ℕ) →
                    (Y : C) →
                      ((Ext R C n).obj (Opposite.op X)).obj Y ≅
                        HomologicalComplex.homology (P.complex.linearYonedaObj R Y) n
-- Init.Prelude
HAdd.mk : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → (α → β → γ) → HAdd α β γ
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.IsBilimit.mk : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {F : J → C} →
          {B : CategoryTheory.Limits.Bicone F} →
            CategoryTheory.Limits.IsLimit B.toCone → CategoryTheory.Limits.IsColimit B.toCocone → B.IsBilimit
-- Init.Data.List.Scan.Lemmas
_private.Init.Data.List.Scan.Lemmas.0.List.scanAuxM.go_eq_append_map : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_3} {xs : List β} {last : α} {acc : List α} [inst : Monad m]
  [LawfulMonad m] {f : α → β → m α}, List.scanAuxM.go✝ f xs last acc = (fun x => x ++ acc) <$> List.scanAuxM✝ f last xs
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.algebraMap_injective : ∀ {A : Type u_2} [inst : Ring A] {K : Type u_5} [inst_1 : Field K] [inst_2 : Algebra K A] {ΓA : Type u_7}
  {ΓK : Type u_8} [inst_3 : LinearOrderedCommGroupWithZero ΓK] [inst_4 : LinearOrderedCommGroupWithZero ΓA]
  {vK : Valuation K ΓK} {vA : Valuation A ΓA} [inst_5 : vK.HasExtension vA] [Nontrivial A],
  Function.Injective ⇑(algebraMap ↥vK.integer ↥vA.integer)
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.instSub : {𝕜 : Type u_2} → {α : Type u_5} → [inst : AddGroup 𝕜] → [inst_1 : LE α] → Sub (IncidenceAlgebra 𝕜 α)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- Let `A` be a graded ring and `P ≤ Q` be two submonoids, then the homogeneous localization of `A`
at `P` embeds into the homogeneous localization of `A` at `Q`.
 -/
HomogeneousLocalization.mapId : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubgroupClass σ A] →
            [inst_3 : AddCommMonoid ι] →
              [inst_4 : DecidableEq ι] →
                (𝒜 : ι → σ) →
                  [inst_5 : GradedRing 𝒜] →
                    {P Q : Submonoid A} → P ≤ Q → HomogeneousLocalization 𝒜 P →+* HomogeneousLocalization 𝒜 Q
-- Mathlib.Order.Copy
/-- A function to create a provable equal copy of a bottom order
with possibly different definitional equalities.  -/
OrderBot.copy : {α : Type u} → {h h' : LE α} → (c : OrderBot α) → (bot : α) → bot = ⊥ → (∀ (x y : α), x ≤ y ↔ x ≤ y) → OrderBot α
-- Mathlib.Order.Nucleus
Nucleus.instFrame : {X : Type u_1} → [inst : Order.Frame X] → Order.Frame (Nucleus X)
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.coe_ofBijective : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) (hf : Function.Bijective ⇑f),
  ⇑(f.ofBijective hf) = ⇑f
-- Std.Time.Format.Modifier
/-- `Q`: Quarter of year as number or text (e.g., 3, 03, Q3, 3rd quarter).
 -/
Std.Time.Modifier.Q : Std.Time.Number ⊕ Std.Time.Text → Std.Time.Modifier
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.WorkspaceEditClientCapabilities.mk.sizeOf_spec : ∀ (documentChanges? : Option Bool) (changeAnnotationSupport? : Option Lean.Lsp.ChangeAnnotationSupport)
  (resourceOperations? : Option (Array String)),
  sizeOf
      { documentChanges? := documentChanges?, changeAnnotationSupport? := changeAnnotationSupport?,
        resourceOperations? := resourceOperations? } =
    1 + sizeOf documentChanges? + sizeOf changeAnnotationSupport? + sizeOf resourceOperations?
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
SemiSimplexCategory.instMono : ∀ {n m : SemiSimplexCategory} (f : n ⟶ m), CategoryTheory.Mono f
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.cyclesMap'_neg : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
  CategoryTheory.ShortComplex.cyclesMap' (-φ) h₁ h₂ = -CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the angle between three points is nonzero, the first two points are not equal.  -/
EuclideanGeometry.left_ne_of_oangle_ne_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, EuclideanGeometry.oangle p₁ p₂ p₃ ≠ 0 → p₁ ≠ p₂
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.mintroPat_ : Lean.ParserDescr
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
AlgebraicClosure.spanCoeffs_ne_top : ∀ (k : Type u) [inst : Field k], AlgebraicClosure.spanCoeffs k ≠ ⊤
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- When `Φ : LocalizerMorphism W₁ W₂` and that `L₁` and `L₂` are localization functors
for `W₁` and `W₂`, then `Φ.localizedFunctor L₁ L₂` is the induced functor on the
localized categories.  -/
CategoryTheory.LocalizerMorphism.localizedFunctor : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {D₁ : Type u₄} →
      {D₂ : Type u₅} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₄, u₄} D₁] →
              [inst_3 : CategoryTheory.Category.{v₅, u₅} D₂] →
                {W₁ : CategoryTheory.MorphismProperty C₁} →
                  {W₂ : CategoryTheory.MorphismProperty C₂} →
                    CategoryTheory.LocalizerMorphism W₁ W₂ →
                      (L₁ : CategoryTheory.Functor C₁ D₁) →
                        [L₁.IsLocalization W₁] →
                          (L₂ : CategoryTheory.Functor C₂ D₂) → [L₂.IsLocalization W₂] → CategoryTheory.Functor D₁ D₂
-- Mathlib.Order.Filter.Basic
Filter.Eventually.ne_top_of_lt : ∀ {α : Type u} {β : Type v} [inst : Preorder β] [inst_1 : OrderTop β] {l : Filter α} {f g : α → β},
  (∀ᶠ (x : α) in l, f x < g x) → ∀ᶠ (x : α) in l, f x ≠ ⊤
-- Mathlib.Analysis.InnerProductSpace.Affine
inner_vsub_vsub_right_eq_dist_sq_left_iff : ∀ {V : Type u_2} {P : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b c : P}, inner ℝ (a -ᵥ c) (b -ᵥ c) = dist a c ^ 2 ↔ inner ℝ (a -ᵥ c) (b -ᵥ a) = 0
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.sConvexComb_sConvexComb : ∀ {R : Type u_1} {M : Type u_3} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R M] (f : Convexity.StdSimplex R (Convexity.StdSimplex R M)),
  Convexity.sConvexComb (Convexity.sConvexComb f) =
    Convexity.sConvexComb (Convexity.StdSimplex.map Convexity.sConvexComb f)
-- Init.Core
PSum.inr.injEq : ∀ {α : Sort u} {β : Sort v} (val val_1 : β), (PSum.inr val = PSum.inr val_1) = (val = val_1)
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ofCLM_add : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  {f g : E →SL[σ] F},
  ContinuousLinearMapWOT.ofCLM (f + g) = ContinuousLinearMapWOT.ofCLM f + ContinuousLinearMapWOT.ofCLM g
-- Mathlib.LinearAlgebra.Dimension.Free
/-- **Alias** of `Module.nonempty_linearEquiv_iff_lift_rank_eq`.

---

Two vector spaces are isomorphic if and only if they have the same dimension.  -/
LinearEquiv.nonempty_equiv_iff_lift_rank_eq : ∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Free R M] [inst_4 : AddCommMonoid M'] [inst_5 : Module R M'] [Module.Free R M'] [StrongRankCondition R],
  Nonempty (M ≃ₗ[R] M') ↔ Cardinal.lift.{v', v} (Module.rank R M) = Cardinal.lift.{v, v'} (Module.rank R M')
-- Mathlib.Order.Filter.Pointwise
/-- An additive action of an additive monoid on a type `β` gives an additive action on
`Filter β`.  -/
Filter.addActionFilter : {α : Type u_2} → {β : Type u_3} → [inst : AddMonoid α] → [AddAction α β] → AddAction α (Filter β)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens}, IsCompact ↑U ↔ ∃ s, s.Finite ∧ U = ⨆ i ∈ s, ↑i
-- Init.Data.Array.Erase
Array.eraseP_replicate_of_pos : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {a : α}, p a = true → (Array.replicate n a).eraseP p = Array.replicate (n - 1) a
-- Init.Data.String.Iterator
/-- The string being iterated over.  -/
String.Legacy.Iterator.toString : String.Legacy.Iterator → String
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_minKey! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.getKey? t.minKey! = some t.minKey!