mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.wordProd_surjective : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W),
  Function.Surjective cs.wordProd
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_alter!_eq_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (Std.DTreeMap.Internal.Impl.alter! k f t).minKey? = some k ↔
        (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (compare k k').isLE = true
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.Hom.mk.injEq : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} {X Y : F.Grothendieck}
  (base : X.base ⟶ Y.base) (fiber : (F.map base.toLoc).toFunctor.obj X.fiber ⟶ Y.fiber) (base_1 : X.base ⟶ Y.base)
  (fiber_1 : (F.map base_1.toLoc).toFunctor.obj X.fiber ⟶ Y.fiber),
  ({ base := base, fiber := fiber } = { base := base_1, fiber := fiber_1 }) = (base = base_1 ∧ fiber ≍ fiber_1)
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.instOfFinite : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Finite R S],
  Algebra.QuasiFinite R S
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.MorphismProperty.isClosedUnderColimitsOfShape_isLocal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] [CategoryTheory.EssentiallySmall.{w, v', u'} J] (κ : Cardinal.{w})
  [inst_3 : Fact κ.IsRegular] [CategoryTheory.IsCardinalFiltered J κ],
  (∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → CategoryTheory.IsCardinalPresentable X κ ∧ CategoryTheory.IsCardinalPresentable Y κ) →
    W.isLocal.IsClosedUnderColimitsOfShape J
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.HasImageMap.mk' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] {sq : f ⟶ g},
  Nonempty (CategoryTheory.Limits.ImageMap sq) → CategoryTheory.Limits.HasImageMap sq
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag_apply : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (M : Matrix (m × o) (n × o) α) (k : o) (i : m) (j : n),
  M.blockDiag k i j = M (i, k) (j, k)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
SSet.strongInnerAnodyneExtensions_le_innerAnodyneExtensions : SSet.strongInnerAnodyneExtensions ≤ SSet.innerAnodyneExtensions
-- Std.Do.SPred.SPred
Std.Do.SPred.conjunction.eq_2 : ∀ {σs : List (Type u)} (P : Std.Do.SPred σs) (env_2 : List (Std.Do.SPred σs)),
  Std.Do.SPred.conjunction (P :: env_2) = spred(P ∧ Std.Do.SPred.conjunction env_2)
-- Mathlib.CategoryTheory.FinCategory.AsType
/-- The constructed category (`AsType α`) is equivalent to `ObjAsType α`.  -/
CategoryTheory.FinCategory.asTypeEquivObjAsType : (α : Type u_1) →
  [inst : Fintype α] →
    [inst_1 : CategoryTheory.SmallCategory α] →
      [inst_2 : CategoryTheory.FinCategory α] →
        CategoryTheory.FinCategory.AsType α ≌ CategoryTheory.FinCategory.ObjAsType α
-- Mathlib.Data.Stream.Defs
/-- An auxiliary definition for `Stream'.cycle` corecursive def  -/
Stream'.cycleF : {α : Type u} → α × List α × α × List α → α
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pullbackCoverOfLeft_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X) {Y Z : C}
  (f : X ⟶ Z) (g : Y ⟶ Z) [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.f i) f) g]
  (i : E.I₀),
  (E.pullbackCoverOfLeft f g).X i = CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (E.f i) f) g
-- Mathlib.RepresentationTheory.Irreducible
Representation.irreducible_iff_isSimpleModule_asModule : ∀ {G : Type u_1} {k : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Field k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V), ρ.IsIrreducible ↔ IsSimpleModule (MonoidAlgebra k G) ρ.asModule
-- Mathlib.Algebra.Ring.Equiv
RingEquivClass.mk : ∀ {F : Type u_7} {R : Type u_8} {S : Type u_9} [inst : Mul R] [inst_1 : Add R] [inst_2 : Mul S] [inst_3 : Add S]
  [inst_4 : EquivLike F R S] [toMulEquivClass : MulEquivClass F R S],
  (∀ (f : F) (a b : R), f (a + b) = f a + f b) → RingEquivClass F R S
-- Mathlib.Geometry.Manifold.Notation
/-- `CMDiff n f` elaborates to `ContMDiff I J n f`,
trying to determine `I` and `J` from the local context.
`n` is coerced to `WithTop ℕ∞` if necessary (so passing a `ℕ`, `∞` or `ω` are all supported).  -/
Manifold.termCMDiff____ : Lean.ParserDescr
-- Init.Data.BitVec.Lemmas
BitVec.ult_iff_toNat_lt : ∀ {w : ℕ} {x y : BitVec w}, x.ult y = true ↔ x.toNat < y.toNat
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.mk.injEq : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {A B : HomologicalComplex V c}
  (f : (i : ι) → A.X i ⟶ B.X i)
  (comm' :
    autoParam
      (∀ (i j : ι),
        c.Rel i j →
          CategoryTheory.CategoryStruct.comp (f i) (B.d i j) = CategoryTheory.CategoryStruct.comp (A.d i j) (f j))
      HomologicalComplex.Hom.comm'._autoParam)
  (f_1 : (i : ι) → A.X i ⟶ B.X i)
  (comm'_1 :
    autoParam
      (∀ (i j : ι),
        c.Rel i j →
          CategoryTheory.CategoryStruct.comp (f_1 i) (B.d i j) = CategoryTheory.CategoryStruct.comp (A.d i j) (f_1 j))
      HomologicalComplex.Hom.comm'._autoParam),
  ({ f := f, comm' := comm' } = { f := f_1, comm' := comm'_1 }) = (f = f_1)
-- Lean.Elab.Open
Lean.Elab.OpenDecl.State.mk : List Lean.OpenDecl → Lean.Name → Lean.Elab.OpenDecl.State
-- Mathlib.Topology.FiberBundle.Basic
FiberPrebundle.isOpen_target_of_mem_pretrivializationAtlas_inter : ∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : (x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E)
  (e e' : Bundle.Pretrivialization F Bundle.TotalSpace.proj),
  e' ∈ a.pretrivializationAtlas → IsOpen (e'.target ∩ ↑e'.symm ⁻¹' e.source)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddEquiv.ofLeftInverse'_symm_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N) {g : N → M}
  (h : Function.LeftInverse g ⇑f) (a : ↥(AddMonoidHom.mrange f)), (AddEquiv.ofLeftInverse' f h).symm a = g ↑a
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.prod_norm_sq : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {E : Type u_2} {F : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : Module ℂ E] [inst_4 : SMul A E] [inst_5 : NormedAddCommGroup F]
  [inst_6 : Module ℂ F] [inst_7 : SMul A F] [inst_8 : CStarModule A E] [inst_9 : CStarModule A F]
  (x : WithCStarModule A (E × F)), ‖x‖ ^ 2 = ‖inner A x.1 x.1 + inner A x.2 x.2‖
-- Init.Data.String.Defs
String.Pos.lt_trans : ∀ {s : String} {p q r : s.Pos}, p < q → q < r → p < r
-- Std.Http.Data.Method
Std.Http.Method.trace.sizeOf_spec : sizeOf Std.Http.Method.trace = 1
-- Mathlib.CategoryTheory.Bicategory.Free
/-- Canonical prefunctor from `B` to `free_bicategory B`.  -/
CategoryTheory.FreeBicategory.of : {B : Type u} → [inst : Quiver B] → B ⥤q CategoryTheory.FreeBicategory B
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
/-- The characteristic polynomial of a matrix `M` is given by $\det (t I - M)$.  -/
Matrix.charpoly : {R : Type u_1} → [inst : CommRing R] → {n : Type u_4} → [DecidableEq n] → [Fintype n] → Matrix n n R → Polynomial R
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.im_smul : ∀ {d : ℤ} (a : ℤ) (b : ℤ√d), (↑a * b).im = a * b.im
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Cache.Key.mk.sizeOf_spec : ∀ (w : ℕ) (expr : Std.Tactic.BVDecide.BVExpr w), sizeOf { w := w, expr := expr } = 1 + sizeOf w + sizeOf expr
-- Mathlib.Algebra.Homology.ConcreteCategory
CategoryTheory.ShortComplex.ShortExact.δ_apply' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.HasForget₂ C Ab] [inst_4 : CategoryTheory.Abelian C]
  [inst_5 : (CategoryTheory.forget₂ C Ab).Additive] [(CategoryTheory.forget₂ C Ab).PreservesHomology] {ι : Type u_2}
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι)
  (hij : c.Rel i j) (x₃ : ↑((CategoryTheory.forget₂ C Ab).obj (S.X₃.homology i)))
  (x₂ : ↑((CategoryTheory.forget₂ C Ab).obj (S.X₂.opcycles i)))
  (x₁ : ↑((CategoryTheory.forget₂ C Ab).obj (S.X₁.cycles j))),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map (HomologicalComplex.opcyclesMap S.g i))) x₂ =
      (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map (S.X₃.homologyι i))) x₃ →
    (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map (HomologicalComplex.cyclesMap S.f j))) x₁ =
        (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map (S.X₂.opcyclesToCycles i j))) x₂ →
      (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map (hS.δ i j hij))) x₃ =
        (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map (S.X₁.homologyπ j))) x₁
-- Mathlib.Data.SetLike.Basic
SetLike.not_le_iff_exists : ∀ {A : Type u_1} {B : Type u_2} [inst : SetLike A B] [inst_1 : LE A] [IsConcreteLE A B] {p q : A},
  ¬p ≤ q ↔ ∃ x ∈ p, x ∉ q
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
/-- If `e` is not primitive, then `e.mulShift d = 1` for some proper divisor `d` of `N`.  -/
AddChar.exists_divisor_of_not_isPrimitive : ∀ {N : ℕ} [NeZero N] {R : Type u_1} [inst : CommRing R] (e : AddChar (ZMod N) R),
  ¬e.IsPrimitive → ∃ d, d ∣ N ∧ d < N ∧ e.mulShift ↑d = 1
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] {M : Type u_1} [inst_1 : L.Structure M]
  (S : ι →o L.Substructure M),
  DirectedSystem (fun i => ↥(S i)) fun x x_1 h => ⇑(FirstOrder.Language.Substructure.inclusion ⋯)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.snoc_injective_iff : ∀ {n : ℕ} {α : Type u_2} {x₀ : α} {x : Fin n → α},
  Function.Injective (Fin.snoc x x₀) ↔ Function.Injective x ∧ x₀ ∉ Set.range x
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.update.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (p : SkewPolynomial R) (n : ℕ) (a : R),
  p.update n a = SkewMonoidAlgebra.update p (Multiplicative.ofAdd n) a
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.mem_normalizedFactors_eq_of_associated : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {a b c : α},
  a ∈ UniqueFactorizationMonoid.normalizedFactors c →
    b ∈ UniqueFactorizationMonoid.normalizedFactors c → Associated a b → a = b
-- Mathlib.Order.Basic
eq_or_lt_of_le' : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, b ≤ a → a = b ∨ b < a
-- Mathlib.FieldTheory.PerfectClosure
/-- `PerfectClosure.R` is the relation `(n, x) ∼ (n + 1, x ^ p)` for `n : ℕ` and `x : K`.
`PerfectClosure K p` is the quotient by this relation.  -/
PerfectClosure.R : (K : Type u) → [inst : CommRing K] → (p : ℕ) → [Fact (Nat.Prime p)] → [CharP K p] → ℕ × K → ℕ × K → Prop
-- Mathlib.Data.Real.ENatENNReal
ENat.toENNReal_lt : ∀ {m n : ℕ∞}, ↑m < ↑n ↔ m < n
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.neg_pi : ∀ {ι : Type u_5} {α : ι → Type u_6} [inst : (i : ι) → Neg (α i)] (s : Set ι) (t : (i : ι) → Set (α i)),
  -s.pi t = s.pi fun i => -t i
-- Init.Data.BitVec.Bootstrap
BitVec.getElem_setWidth' : ∀ {w v : ℕ} (x : BitVec w) (i : ℕ) (h : w ≤ v) (hi : i < v), (BitVec.setWidth' h x)[i] = x.getLsbD i
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.natIsoFunctor_hom_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁}
  {F : CategoryTheory.Functor (CategoryTheory.Discrete I) C} (X : CategoryTheory.Discrete I),
  CategoryTheory.Discrete.natIsoFunctor.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.CategoryTheory.Monoidal.Limits.HasLimits
CategoryTheory.MonoidalCategory.Limits.colimit.ι_desc_whiskerRight_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {J : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} J] {F : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasColimit F] (c : CategoryTheory.Limits.Cocone F) (j : J) {Q Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj c.pt Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.colimit.ι F j) Q)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.colimit.desc F c) Q) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (c.ι.app j) Q) h
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.of_isPullback_of_descendsAlong : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.MorphismProperty C} {A X Y Z : C}
  {fst : A ⟶ X} {snd : A ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} [P.DescendsAlong Q],
  CategoryTheory.IsPullback fst snd f g → Q f → P fst → P g
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.den_add : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} (x : Submonoid A) [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι]
  [inst_5 : GradedRing 𝒜] (c1 c2 : HomogeneousLocalization.NumDenSameDeg 𝒜 x), ↑(c1 + c2).den = ↑c1.den * ↑c2.den
-- Mathlib.Algebra.Polynomial.Inductions
Polynomial.divX_one : ∀ {R : Type u} [inst : Semiring R], Polynomial.divX 1 = 0
-- Aesop.Forward.State
Aesop.ForwardState.mk : Lean.PHashMap Aesop.RuleName Aesop.RuleState →
  Lean.PHashMap Lean.FVarId (Lean.PArray (Aesop.RuleName × Aesop.PremiseIndex)) →
    Lean.PHashMap Aesop.PatSubstSource (Lean.PArray (Aesop.RuleName × Aesop.Substitution)) → Aesop.ForwardState
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget TopCat)
-- Init.Data.Nat.Lcm
Nat.lcm_lcm_self_left_left : ∀ (m n : ℕ), (m.lcm n).lcm m = n.lcm m
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₂₃_p : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃),
  CategoryTheory.CategoryStruct.comp h.p₂₃ h₂₃.p = h.p
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.norm_eq_of_L2 : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] (x : PiLp 2 β),
  ‖x‖ = √(∑ i, ‖x.ofLp i‖ ^ 2)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.prod_rightr : ∀ {α : Type u_1} {E : Type u_3} {E' : Type u_6} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup E']
  [inst_2 : SeminormedAddCommGroup F'] {c : ℝ} {f : α → E} (f' : α → E') {g' : α → F'} {l : Filter α},
  Asymptotics.IsBigOWith c l f g' → 0 ≤ c → Asymptotics.IsBigOWith c l f fun x => (f' x, g' x)
-- Lean.Widget.UserWidget
Lean.Widget.evalWidgetInstance : Lean.Expr → Lean.MetaM Lean.Widget.WidgetInstance
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.leftUnitor_inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasTerminal C]
  [inst_2 : CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor X).inv
      (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id (⊤_ C)) f) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.prod.leftUnitor Y).inv
-- Mathlib.Data.Real.Basic
Real.instZero : Zero ℝ
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.ReflectsColimit.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D},
  (∀ {c : CategoryTheory.Limits.Cocone K} (hc : CategoryTheory.Limits.IsColimit (F.mapCocone c)),
      Nonempty (CategoryTheory.Limits.IsColimit c)) →
    CategoryTheory.Limits.ReflectsColimit K F
-- Mathlib.FieldTheory.Laurent
RatFunc.laurent_injective : ∀ {R : Type u} [inst : CommRing R] (r : R) [inst_1 : IsDomain R], Function.Injective ⇑(RatFunc.laurent r)
-- Mathlib.Analysis.LocallyConvex.Separation
RCLike.geometric_hahn_banach_compact_closed : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E]
  {s t : Set E} [inst_3 : RCLike 𝕜] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E]
  [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E],
  Convex ℝ s →
    IsCompact s →
      Convex ℝ t →
        IsClosed t → Disjoint s t → ∃ f u v, (∀ a ∈ s, RCLike.re (f a) < u) ∧ u < v ∧ ∀ b ∈ t, v < RCLike.re (f b)
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.reflectionCircumcenterWeightsWithCircumcenter.eq_2 : ∀ {n : ℕ} (i₁ i₂ : Fin (n + 1)),
  Affine.Simplex.reflectionCircumcenterWeightsWithCircumcenter i₁ i₂
      Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex =
    -1
-- Mathlib.Order.Hom.Bounded
/-- Reinterpret a bot homomorphism as a top homomorphism between the dual lattices.  -/
BotHom.dual : {α : Type u_2} →
  {β : Type u_3} →
    [inst : LE α] → [inst_1 : OrderBot α] → [inst_2 : LE β] → [inst_3 : OrderBot β] → BotHom α β ≃ TopHom αᵒᵈ βᵒᵈ
-- Mathlib.Analysis.Normed.Module.Bases
/-- An unconditional Schauder basis indexed by `β`.

In the literature, this is known as:
* An **Extended Basis** [Marti, Jürg T., Introduction to the theory of bases][MartiJurg1969]:
Defined via convergence of the net of finite partial sums.
* An **Unconditional Basis** [Singer, Ivan., Bases in Banach spaces][Singer_1970]: On an arbitrary
set, convergence is necessarily unconditional.

This structure generalizes the classical Schauder basis by replacing sequential
convergence with summability over the directed set of finite subsets.
 -/
UnconditionalSchauderBasis : Type u_4 →
  (𝕜 : Type u_5) →
    (X : Type u_6) →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup X] → [NormedSpace 𝕜 X] → Type (max (max u_4 u_5) u_6)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.length_bypass_le_length : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] (p : G.Walk u v), p.bypass.length ≤ p.length
-- Mathlib.MeasureTheory.Function.Floor
MeasurableSet.image_fract : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [inst_3 : TopologicalSpace R]
  [OrderTopology R] [inst_5 : MeasurableSpace R] [IsStrictOrderedRing R] [BorelSpace R] {s : Set R},
  MeasurableSet s → MeasurableSet (Int.fract '' s)
-- Mathlib.Order.SymmDiff
sup_sdiff_symmDiff : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a b : α), (a ⊔ b) \ symmDiff a b = a ⊓ b
-- Mathlib.Algebra.Group.Action.Sigma
Sigma.vadd_mk : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → VAdd M (α i)] (a : M) (i : ι) (b : α i),
  a +ᵥ ⟨i, b⟩ = ⟨i, a +ᵥ b⟩
-- Mathlib.Analysis.Polynomial.Norm
Polynomial.le_supNorm : ∀ {A : Type u_1} [inst : SeminormedRing A] (p : Polynomial A) (i : ℕ), ‖p.coeff i‖ ≤ p.supNorm
-- Mathlib.Algebra.Order.Monovary
MonovaryOn.add_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : AddCommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedAddMonoid β] {s : Set ι} {f : ι → α} {g₁ g₂ : ι → β},
  MonovaryOn f g₁ s → MonovaryOn f g₂ s → MonovaryOn f (g₁ + g₂) s
-- Mathlib.Algebra.Algebra.Spectrum.Basic
_private.Mathlib.Algebra.Algebra.Spectrum.Basic.0.spectrum.«term↑ₐ» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Units.Defs
Units.ext : ∀ {α : Type u} [inst : Monoid α] {u v : αˣ}, ↑u = ↑v → u = v
-- Aesop.Options.Public
Aesop.instReprStrategy.repr : Aesop.Strategy → ℕ → Std.Format
-- Init.Data.ToString.Basic
instToStringUInt16 : ToString UInt16
-- Init.SimpLemmas
or_self_left : ∀ {a b : Prop}, a ∨ a ∨ b ↔ a ∨ b
-- Mathlib.Analysis.Quaternion
Quaternion.continuous_imI : Continuous fun q => q.imI
-- Lean.Parser.Term
Lean.Parser.Term.whereFinallySubsection.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.Polynomial.Vieta
/-- Vieta's formula for the coefficients of the product of linear terms `X + λ` where `λ` runs
through a multiset `s` : the `k`th coefficient is the symmetric function `esymm (card s - k) s`.  -/
Multiset.prod_X_add_C_coeff : ∀ {R : Type u_1} [inst : CommSemiring R] (s : Multiset R) {k : ℕ},
  k ≤ s.card → (Multiset.map (fun r => Polynomial.X + Polynomial.C r) s).prod.coeff k = s.esymm (s.card - k)
-- Init.PropLemmas
left_iff_ite_iff : ∀ {p : Prop} [inst : Decidable p] {x y : Prop}, (x ↔ if p then x else y) ↔ ¬p → x = y
-- Mathlib.Algebra.Category.Ring.FilteredColimits
/-- The proposed colimit cocone is a colimit in `SemiRingCat`.  -/
SemiRingCat.FilteredColimits.colimitCoconeIsColimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J SemiRingCat) →
      [inst_1 : CategoryTheory.IsFiltered J] →
        CategoryTheory.Limits.IsColimit (SemiRingCat.FilteredColimits.colimitCocone F)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.instSetLike : {α : Type u_1} → [inst : TopologicalSpace α] → SetLike (TopologicalSpace.Compacts α) α
-- Mathlib.CategoryTheory.Limits.Connected
CategoryTheory.parallelPairInhabited : Inhabited CategoryTheory.Limits.WalkingParallelPair
-- Mathlib.RingTheory.Artinian.Module
instIsArtinianRingForallOfFinite : ∀ {ι : Type u_2} [Finite ι] {R : ι → Type u_1} [inst : (i : ι) → Semiring (R i)] [∀ (i : ι), IsArtinianRing (R i)],
  IsArtinianRing ((i : ι) → R i)
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.hom_comp : ∀ {R S T : RingCat} (f : R ⟶ S) (g : S ⟶ T),
  RingCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (RingCat.Hom.hom g).comp (RingCat.Hom.hom f)
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
/-- Typeclass to track whether the support of a preordering forms an ideal.  -/
RingPreordering.HasIdealSupport : {R : Type u_1} → [inst : CommRing R] → RingPreordering R → Prop
-- Lean.Meta.PPGoal
Lean.Meta.pp.auxDecls : Lean.Option Bool
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_snd_assoc : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.X z ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f z))
          (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x)))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f y) (𝒰.f z)) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y))
        (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f z)) h)