mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
CategoryTheory.PreOneHypercover.IsStronglySeparatedFor.isSeparatedFor_presieve₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C} {E : CategoryTheory.PreOneHypercover X}
  {F : CategoryTheory.Functor Cᵒᵖ (Type u_3)},
  E.IsStronglySeparatedFor F → CategoryTheory.Presieve.IsSeparatedFor F E.presieve₀
-- Mathlib.Algebra.Ring.Ext
CommSemiring.ext_iff : ∀ {R : Type u} {inst₁ inst₂ : CommSemiring R}, inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
-- Mathlib.RingTheory.Kaehler.JacobiZariski
/-- Given algebras $R \to S \to T$, the sequence
$H_1(L_{T/R}) \to H_1(L_{T/S}) \to T \otimes_S \Omega_{S/R}$
is exact.  -/
Algebra.H1Cotangent.exact_map_δ : ∀ (R : Type u₁) (S : Type u₂) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u₃)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T],
  Function.Exact ⇑(Algebra.H1Cotangent.map R S T T) ⇑(Algebra.H1Cotangent.δ R S T)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toRingHom_trans : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} [inst : CommSemiring R] [inst_1 : Semiring A₁]
  [inst_2 : Semiring A₂] [inst_3 : Semiring A₃] [inst_4 : Algebra R A₁] [inst_5 : Algebra R A₂] [inst_6 : Algebra R A₃]
  (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃), ↑(e₁.trans e₂) = (↑e₂).comp ↑e₁
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₂₁_single_inv_mul_ρ_add_single : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (g h : G) (a : ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.d₂₁ A))
      ((fun₀ | (g⁻¹, g * h) => (A.ρ g⁻¹) a) + fun₀ | (g, h) => a) =
    (fun₀ | g⁻¹ => (A.ρ g⁻¹) a) + fun₀ | g => a
-- Mathlib.Dynamics.Flow
Flow.id_apply : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddZero τ] (t : τ),
  (Flow.id τ α).toFun t = id
-- Mathlib.Topology.MetricSpace.Closeds
Metric.lipschitz_infDist_set : ∀ {α : Type u_1} [inst : MetricSpace α] (x : α), LipschitzWith 1 fun s => Metric.infDist x ↑s
-- Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
ContinuousLinearMapWOT.ext_inner_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F] {A B : E →WOT[𝕜] F},
  A = B ↔ ∀ (x : E) (y : F), inner 𝕜 y (A x) = inner 𝕜 y (B x)
-- Std.Sat.AIG.Basic
/-- This datatype is isomorphic to a pair of a `Nat` and a `Bool`, however the `Bool` is stored in the
lowest bit of the `Nat` in order to save memory. It is used to describe an input to an `AIG` circuit
node which consists of a `Nat` describing the input node and a `Bool` saying whether there is an inverter
on the input.
 -/
Std.Sat.AIG.Fanin : Type
-- Init.Data.UInt.Basic
/-- Bitwise left shift for 16-bit unsigned integers. Usually accessed via the `<<<` operator.

This function is overridden at runtime with an efficient implementation.
 -/
UInt16.shiftLeft : UInt16 → UInt16 → UInt16
-- Init.Data.Order.Lemmas
/-- If a `Max α` instance satisfies typical properties in terms of a reflexive and antisymmetric `LE α`
instance, then the `LE α` instance represents a linear order.
 -/
Std.IsLinearOrder.of_refl_of_antisymm_of_lawfulOrderMax : ∀ {α : Type u} [inst : LE α] [inst_1 : Max α] [Std.Refl fun x1 x2 => x1 ≤ x2] [Std.Antisymm fun x1 x2 => x1 ≤ x2]
  [Std.LawfulOrderMax α], Std.IsLinearOrder α
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.dvd_prod_of_mem : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] (f : ι → M) {a : ι} {s : Finset ι}, a ∈ s → f a ∣ ∏ i ∈ s, f i
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.isOpenImmersion_isMultiplicative : AlgebraicGeometry.IsOpenImmersion.IsMultiplicative
-- Mathlib.CategoryTheory.Localization.Predicate
/-- A chosen equivalence of categories `W.Localization ≅ D` for a functor
`L : C ⥤ D` which satisfies `L.IsLocalization W`. This shall be used in
order to deduce properties of `L` from properties of `W.Q`.  -/
CategoryTheory.Localization.equivalenceFromModel : {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] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) → [L.IsLocalization W] → W.Localization ≌ D
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey!_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {f : β → β},
  t.modify k f ≠ ∅ → (t.modify k f).minKey! = if cmp t.minKey! k = Ordering.eq then k else t.minKey!
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- If the additive action of `M` on `α` is faithful,
then `fixedBy α m = Set.univ` implies that `m = 1`.  -/
AddAction.fixedBy_eq_univ_iff_eq_zero : ∀ {α : Type u_1} {M : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α] [FaithfulVAdd M α] {m : M},
  AddAction.fixedBy α m = Set.univ ↔ m = 0
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.Proj.toSheafedSpace.eq_1 : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜],
  AlgebraicGeometry.Proj.toSheafedSpace 𝒜 =
    { carrier := TopCat.of (ProjectiveSpectrum 𝒜),
      presheaf := (AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj, IsSheaf := ⋯ }
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Atom₁.mk : Lean.Expr → Mathlib.Tactic.BicategoryLike.Obj → Mathlib.Tactic.BicategoryLike.Obj → Mathlib.Tactic.BicategoryLike.Atom₁
-- Mathlib.Order.SuccPred.Relation
/-- For `n < m`, `(n, m)` is in the transitive closure of a relation `~` if `i ~ succ i`
for all `i` between `n` and `m`.  -/
transGen_of_succ_of_lt : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] (r : α → α → Prop) {n m : α},
  (∀ i ∈ Set.Ico n m, r i (Order.succ i)) → n < m → Relation.TransGen r n m
-- Mathlib.Topology.Algebra.Order.Field
/-- In a linearly ordered field with the order topology, if `f` tends to `Filter.atTop` and `g`
tends to a negative constant `C` then `f * g` tends to `Filter.atBot`.  -/
Filter.Tendsto.atTop_mul_neg : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜},
  C < 0 →
    Filter.Tendsto f l Filter.atTop → Filter.Tendsto g l (nhds C) → Filter.Tendsto (fun x => f x * g x) l Filter.atBot
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_associator_hom_assoc : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [inst_3 : X₁.HasTensor X₂]
  [inst_4 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [inst_5 : X₂.HasTensor X₃]
  [inst_6 : X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)]
  [inst_7 : X₁.HasGoodTensor₁₂Tensor X₂ X₃] [inst_8 : X₁.HasGoodTensorTensor₂₃ X₂ X₃] (i₁ i₂ i₃ j : I)
  (h : i₁ + i₂ + i₃ = j) {Z : C}
  (h_1 :
    CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ X₃).hom j) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (X₁ i₁) (X₂ i₂) (X₃ i₃)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) h_1)
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.MorphismProperty.nonempty_cokernels : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (W : CategoryTheory.MorphismProperty C) {X₁ X₂ : C} (f : X₁ ⟶ X₂),
  W f → ∀ [CategoryTheory.Limits.HasCokernel f], W.cokernels.Nonempty
-- Aesop.Tree.Tracing
Aesop.Goal.traceTree : Aesop.Goal → Aesop.TraceOption → Lean.MetaM Unit
-- Mathlib.Topology.Maps.Basic
Topology.IsOpenEmbedding.of_isEmbedding_isOpenMap : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsEmbedding f → IsOpenMap f → Topology.IsOpenEmbedding f
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.MorphismProperty.LeftFraction.comp₀.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z)
  (z₃ z₃_1 : W.LeftFraction z₁.Y' z₂.Y'), z₃ = z₃_1 → z₁.comp₀ z₂ z₃ = z₁.comp₀ z₂ z₃_1
-- Mathlib.Algebra.BigOperators.Finprod
/-- The sum of `f y` over `y ∈ Set.range g` equals the sum of `f (g i)` over all `i`
provided that `g` is injective on `support (f ∘ g)`.  -/
finsum_mem_range' : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {g : β → α},
  Set.InjOn g (Function.support (f ∘ g)) → ∑ᶠ (i : α) (_ : i ∈ Set.range g), f i = ∑ᶠ (j : β), f (g j)
-- Init.Data.Array.BinSearch
/-- Binary search for an element equivalent to `k` in the sorted array `as`. Returns the element from
the array, if it is found, or `none` otherwise.

The array `as` must be sorted according to the comparison operator `lt`, which should be a total
order.

The optional parameters `lo` and `hi` determine the region of the array indices to be searched. Both
are inclusive, and default to searching the entire array.
 -/
Array.binSearch : {α : Type} → (as : Array α) → α → (α → α → Bool) → optParam ℕ 0 → optParam ℕ (as.size - 1) → Option α
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.brecOn_1.eq : ∀ {motive_1 : Lean.IR.IRType → Sort u} {motive_2 : Array Lean.IR.IRType → Sort u}
  {motive_3 : List Lean.IR.IRType → Sort u} (t : Array Lean.IR.IRType)
  (F_1 : (t : Lean.IR.IRType) → t.below → motive_1 t)
  (F_2 : (t : Array Lean.IR.IRType) → Lean.IR.IRType.below_1 t → motive_2 t)
  (F_3 : (t : List Lean.IR.IRType) → Lean.IR.IRType.below_2 t → motive_3 t),
  Lean.IR.IRType.brecOn_1 t F_1 F_2 F_3 = F_2 t (Lean.IR.IRType.brecOn_1.go t F_1 F_2 F_3).2
-- Mathlib.CategoryTheory.Filtered.Small
/-- The surjection from the abstract filtered closure to the actual filtered closure in `C`.  -/
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsFilteredOrEmpty C] →
      {α : Type w} → (f : α → C) → CategoryTheory.IsFiltered.FilteredClosureSmall.AbstractFilteredClosure✝ f → C
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.forInStep_eq_foldlM.match_1.eq_2 : ∀ {δ : Type u_1} (motive : ForInStep δ → Sort u_2) (d : δ) (h_1 : (d : δ) → motive (ForInStep.yield d))
  (h_2 : (d : δ) → motive (ForInStep.done d)),
  (match ForInStep.done d with
    | ForInStep.yield d => h_1 d
    | ForInStep.done d => h_2 d) =
    h_2 d
-- Mathlib.Data.Int.Cast.Lemmas
zpowersHom_symm_apply : ∀ (α : Type u_3) [inst : Group α] (f : Multiplicative ℤ →* α), (zpowersHom α).symm f = f (Multiplicative.ofAdd 1)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.fiberwise_right : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {l : Filter α}
  {f : α × β → E} {g : α × β → F} {l' : Filter β},
  f =O[l ×ˢ l'] g → ∀ᶠ (a : α) in l, (fun x => f (a, x)) =O[l'] fun x => g (a, x)
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.AdicCauchySequence.instSMul : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u_4) →
        [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → SMul R (AdicCompletion.AdicCauchySequence I M)
-- Init.Core
/-- `a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.


Conventions for notations in identifiers:

 * The recommended spelling of `≠` in identifiers is `ne`. -/
«term_≠_» : Lean.TrailingParserDescr
-- Aesop.Search.Expansion.Norm
Aesop.getForwardState : Aesop.NormM Aesop.ForwardState
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- The second projection `Triangle C ⥤ C`.  -/
CategoryTheory.Pretriangulated.Triangle.π₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] → CategoryTheory.Functor (CategoryTheory.Pretriangulated.Triangle C) C
-- Mathlib.CategoryTheory.Shift.Pullback
CategoryTheory.pullbackShiftIso.congr_simp : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] [inst_3 : CategoryTheory.HasShift C B] (φ : A →+ B) (a : A) (b : B) (h : b = φ a),
  CategoryTheory.pullbackShiftIso C φ a b h = CategoryTheory.pullbackShiftIso C φ a b h
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.Const.insertListIfNewUnitₘ.eq_1 : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit),
  Std.DHashMap.Internal.Raw₀.Const.insertListIfNewUnitₘ m [] = m
-- Mathlib.Analysis.Real.Sqrt
Real.sq_lt : ∀ {x y : ℝ}, x ^ 2 < y ↔ -√y < x ∧ x < √y
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.IsWeaklyRegular.prototype_perm : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {rs : List R},
  RingTheory.Sequence.IsWeaklyRegular M rs →
    ∀ {rs' : List R},
      rs.Perm rs' →
        (∀ (a b : R) (rs' : List R),
            (a :: b :: rs').Subperm rs →
              have K := Submodule.torsionBy R (M ⧸ Ideal.ofList rs' • ⊤) b;
              K = a • K → K = ⊥) →
          RingTheory.Sequence.IsWeaklyRegular M rs'
-- Mathlib.Combinatorics.Quiver.Schreier
/-- The costar map of the labelling prefunctor as an equivalence.  -/
Quiver.SchreierGraph.labellingCostarEquiv : {V : Type u_1} →
  {M : Type u_2} →
    [inst : Group M] →
      [inst_1 : MulAction M V] →
        {S : Type u_3} →
          (ι : S → M) → (x : Quiver.SchreierGraph V ι) → Quiver.Costar x ≃ Quiver.Costar (Quiver.SingleObj.star S)
-- Mathlib.LinearAlgebra.TensorProduct.Free
Algebra.TensorProduct.equivFinsuppOfBasis_symm_apply : ∀ {R : Type u_1} (A : Type u_2) {V : Type u_3} [inst : CommSemiring A] [inst_1 : CommSemiring R] [inst_2 : Algebra R A]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] {ι : Type u_4} (b : Module.Basis ι R V) (a : ι →₀ A),
  (Algebra.TensorProduct.equivFinsuppOfBasis A b).symm a =
    (LinearEquiv.baseChange R A V (ι →₀ R) b.repr).symm ((TensorProduct.finsuppScalarRight R A A ι).symm a)
-- Mathlib.Data.Finset.Sort
/-- The bijection `orderEmbOfFin s h` sends `0` to the minimum of `s`.  -/
Finset.orderEmbOfFin_zero : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {k : ℕ} (h : s.card = k) (hz : 0 < k),
  (s.orderEmbOfFin h) ⟨0, hz⟩ = s.min' ⋯
-- Mathlib.Tactic.Abel
_private.Mathlib.Tactic.Abel.0.Mathlib.Tactic.Abel.instEvalExprConfig_1 : Lean.Elab.ConfigEval.EvalExpr Mathlib.Tactic.Abel.AbelNF.Config
-- Lean.Meta.WHNF
/-- Auxiliary method for unfolding a class projection when transparency is set to `TransparencyMode.instances`.
Recall that class instance projections are not marked with `[reducible]` because we want them to be
in "reducible canonical form".
See `unfoldProjInst?`
 -/
Lean.Meta.unfoldProjInstWhenInstances? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instOneOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : One Mᵐᵒᵖ], DomMulAct.instOneOfMulOpposite = inst
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- Naturality of the oplax functoriality constraint, on the left.  -/
CategoryTheory.OplaxFunctor.mapComp_naturality_left : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.OplaxFunctor B C) {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)) (self.mapComp f' g) =
    CategoryTheory.CategoryStruct.comp (self.mapComp f g)
      (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) (self.map g))
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.transpose_inj : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {A B : Matrix m n α}, A.transpose = B.transpose ↔ A = B
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.sum_congr' : ∀ {α : Type u_1} {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {l : Filter α} {ι : Type u_18} {A : ι → α → E'}
  {B : ι → α → ℝ} {i : α → Finset ι},
  Function.uncurry A =o[⊤ ×ˢ l] Function.uncurry B → (fun H => ∑ j ∈ i H, A j H) =o[l] fun H => ∑ j ∈ i H, ‖B j H‖
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instCommMonoidOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid Mᵐᵒᵖ], DomMulAct.instCommMonoidOfMulOpposite = inst
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.tendsto_const : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u : α → β} {l : Filter α} {c : β},
  Asymptotics.IsEquivalent l u (Function.const α c) → Filter.Tendsto u l (nhds c)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LetRecToLift.shortDeclName : Lean.Elab.Term.LetRecToLift → Lean.Name
-- Mathlib.Analysis.Fourier.AddCircle
/-- The subalgebra of `C(AddCircle T, ℂ)` generated by `fourier n` for `n ∈ ℤ`
separates points.  -/
fourierSubalgebra_separatesPoints : ∀ {T : ℝ} [hT : Fact (0 < T)], fourierSubalgebra.SeparatesPoints
-- Mathlib.Algebra.Order.Sub.WithTop
WithTop.map_sub : ∀ {α : Type u_1} {β : Type u_2} [inst : Sub α] [inst_1 : Bot α] [inst_2 : Sub β] [inst_3 : Bot β] {f : α → β},
  (∀ (x y : α), f (x - y) = f x - f y) →
    f ⊥ = ⊥ → ∀ (x y : WithTop α), WithTop.map f (x - y) = WithTop.map f x - WithTop.map f y
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.IsLocalizationMap.addEquiv_comp : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] {f : M → N},
  S.IsLocalizationMap f →
    ∀ {E : Type u_4} [inst_3 : EquivLike E N P] [AddEquivClass E N P] (e : E), S.IsLocalizationMap (⇑e ∘ f)
-- Aesop.Index.DiscrTreeConfig
/-- The configuration used by all Aesop indices.  -/
Aesop.indexConfig : Lean.Meta.ConfigWithKey
-- Mathlib.RingTheory.Idempotents
CompleteOrthogonalIdempotents.bijective_pi' : ∀ {R : Type u_1} [inst : CommRing R] {I : Type u_3} [inst_1 : Fintype I] {e : I → R},
  (CompleteOrthogonalIdempotents fun x => 1 - e x) →
    Function.Bijective ⇑(RingHom.pi fun i => Ideal.Quotient.mk (Ideal.span {e i}))
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charmatrix_toSquareBlock : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R)
  {α : Type u_5} [inst_3 : DecidableEq α] {b : n → α} {a : α},
  (M.toSquareBlock b a).charmatrix = M.charmatrix.toSquareBlock b a
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.assoc_symm_comp_map_map_comp : ∀ {R : Type u_1} {M : Type u_3} {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {N₁ : Type u_14} {N₂ : Type u_15}
  {N₃ : Type u_16} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid M₁]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid M₃] [inst_6 : AddCommMonoid N₁] [inst_7 : AddCommMonoid N₂]
  [inst_8 : AddCommMonoid N₃] [inst_9 : Module R M₁] [inst_10 : Module R M₂] [inst_11 : Module R M₃]
  [inst_12 : Module R N₁] [inst_13 : Module R N₂] [inst_14 : Module R N₃] (f₁ : M₁ →ₗ[R] N₁) (f₂ : M₂ →ₗ[R] N₂)
  (f₃ : M₃ →ₗ[R] N₃) (f₂₃ : M →ₗ[R] TensorProduct R M₂ M₃),
  ↑(TensorProduct.assoc R N₁ N₂ N₃).symm ∘ₗ TensorProduct.map f₁ (TensorProduct.map f₂ f₃ ∘ₗ f₂₃) =
    TensorProduct.map (TensorProduct.map f₁ f₂) f₃ ∘ₗ
      ↑(TensorProduct.assoc R M₁ M₂ M₃).symm ∘ₗ TensorProduct.map LinearMap.id f₂₃
-- Mathlib.Topology.Separation.GDelta
T6Space.toPerfectlyNormalSpace : ∀ {X : Type u} {inst : TopologicalSpace X} [self : T6Space X], PerfectlyNormalSpace X
-- Mathlib.Tactic.Translate.Core
/-- The arguments that should be reordered when translating, using disjoint cycle notation.  -/
Mathlib.Tactic.Translate.TranslationInfo.reorder : Mathlib.Tactic.Translate.TranslationInfo → Mathlib.Tactic.Translate.Reorder
-- Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
SSet.hasDimensionLE_prod : ∀ (X₁ X₂ : SSet) (d₁ d₂ : ℕ) [X₁.HasDimensionLE d₁] [X₂.HasDimensionLE d₂] (n : ℕ),
  autoParam (d₁ + d₂ ≤ n) SSet.hasDimensionLE_prod._auto_1 →
    (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂).HasDimensionLE n
-- Mathlib.Data.Nat.Choose.Sum
Int.alternating_sum_range_choose : ∀ {n : ℕ}, ∑ m ∈ Finset.range (n + 1), (-1) ^ m * ↑(n.choose m) = if n = 0 then 1 else 0
-- Mathlib.FieldTheory.IsAlgClosed.Spectrum
/-- Half of the spectral mapping theorem for polynomials. We prove it separately
because it holds over any field, whereas `spectrum.map_polynomial_aeval_of_degree_pos` and
`spectrum.map_polynomial_aeval_of_nonempty` need the field to be algebraically closed.  -/
spectrum.subset_polynomial_aeval : ∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A) (p : Polynomial 𝕜),
  (fun x => Polynomial.eval x p) '' spectrum 𝕜 a ⊆ spectrum 𝕜 ((Polynomial.aeval a) p)
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Matrix.ProjGenLinGroup.map_id : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R],
  Matrix.ProjGenLinGroup.map (RingHom.id R) = MonoidHom.id (Matrix.ProjGenLinGroup n R)
-- Mathlib.FieldTheory.RatFunc.IntermediateField
/-- The minimal polynomial of `X` over `K⟮f⟯`. It is defined as `f.num - f * f.denom`, viewed
as a polynomial with coefficients in `A`, where `A` is a `K[f]`-algebra.  -/
RatFunc.minpolyX : {K : Type u_1} →
  [inst : Field K] →
    (f : RatFunc K) → (A : Type u_2) → [inst_1 : CommRing A] → [Algebra K A] → [Algebra (↥K[f]) A] → Polynomial A
-- Mathlib.LinearAlgebra.InvariantBasisNumber
/-- Any nontrivial Noetherian ring satisfies the strong rank condition,
since it satisfies Orzech property.  -/
IsNoetherianRing.strongRankCondition : ∀ (R : Type u) [inst : Ring R] [Nontrivial R] [IsNoetherianRing R], StrongRankCondition R
-- Mathlib.Computability.Partrec
Nat.Partrec.below.comp : ∀ {motive : (a : ℕ →. ℕ) → Nat.Partrec a → Prop} {f g : ℕ →. ℕ} (a : Nat.Partrec f) (a_1 : Nat.Partrec g),
  Nat.Partrec.below a → motive f a → Nat.Partrec.below a_1 → motive g a_1 → Nat.Partrec.below ⋯
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.ringFunc.mul : FirstOrder.ringFunc 2
-- Mathlib.Algebra.Homology.DifferentialObject
/-- The unit isomorphism for `dgoEquivHomologicalComplex`.
 -/
HomologicalComplex.dgoEquivHomologicalComplexUnitIso : {β : Type u_1} →
  [inst : AddCommGroup β] →
    (b : β) →
      (V : Type u_2) →
        [inst_1 : CategoryTheory.Category.{v_1, u_2} V] →
          [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] →
            CategoryTheory.Functor.id (CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) ≅
              (HomologicalComplex.dgoToHomologicalComplex b V).comp (HomologicalComplex.homologicalComplexToDGO b V)
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
/-- If the left cosets of `t` by elements of `s` are disjoint (but not necessarily distinct!), then
the size of `t` divides the size of `s • t`.  -/
Finset.card_dvd_card_smul_right₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : GroupWithZero α] [inst_2 : MulAction α β]
  {t : Finset β} {s : Finset α}, (∀ a ∈ s, a ≠ 0) → ((fun x => x • t) '' ↑s).PairwiseDisjoint id → t.card ∣ (s • t).card