mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.NormNum.Ineq
Mathlib.Meta.NormNum.isInt_lt_false : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] {a b : α} {a' b' : ℤ},
  Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → decide (b' ≤ a') = true → ¬a < b
-- Mathlib.Algebra.Module.Injective
/-- The maximal element of every nonempty chain of `extension_of i f`.  -/
Module.Baer.ExtensionOf.max : {R : Type u} →
  [inst : Ring R] →
    {Q : Type v} →
      [inst_1 : AddCommGroup Q] →
        [inst_2 : Module R Q] →
          {M : Type u_1} →
            {N : Type u_2} →
              [inst_3 : AddCommGroup M] →
                [inst_4 : AddCommGroup N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] →
                      {i : M →ₗ[R] N} →
                        {f : M →ₗ[R] Q} →
                          {c : Set (Module.Baer.ExtensionOf i f)} →
                            IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → Module.Baer.ExtensionOf i f
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_X_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)) (n : ι),
  ((CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj P).X n).X = P.X.X n
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyMap'_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) (h₁ : S₁.RightHomologyData)
  (h₂ : S₂.RightHomologyData) (h₃ : S₃.RightHomologyData),
  CategoryTheory.ShortComplex.rightHomologyMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' φ₁ h₁ h₂)
      (CategoryTheory.ShortComplex.rightHomologyMap' φ₂ h₂ h₃)
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.mem_def : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) {x : ι → ℝ}, x ∈ I ↔ ∀ (i : ι), x i ∈ Set.Ioc (I.lower i) (I.upper i)
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- A category `C` which has coproducts is said to have `AB4` provided that
coproducts are exact.
 -/
CategoryTheory.AB4 : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasCoproducts C] → Prop
-- Init.Data.List.Sublist
List.isSuffixOf_cons_nil : ∀ {α : Type u_1} [inst : BEq α] {a : α} {as : List α}, (a :: as).isSuffixOf [] = false
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- Every `SmoothBumpCovering` defines a smooth partition of unity.  -/
SmoothBumpCovering.toSmoothPartitionOfUnity : {ι : Type uι} →
  {E : Type uE} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        {H : Type uH} →
          [inst_2 : TopologicalSpace H] →
            {I : ModelWithCorners ℝ E H} →
              {M : Type uM} →
                [inst_3 : TopologicalSpace M] →
                  [inst_4 : ChartedSpace H M] →
                    [inst_5 : FiniteDimensional ℝ E] →
                      {s : Set M} →
                        SmoothBumpCovering ι I M s →
                          [T2Space M] → [IsManifold I (↑⊤) M] → SmoothPartitionOfUnity ι I M s
-- Mathlib.Data.Set.Image
Set.image_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {β' : Type u_5} {f : β → γ} {g : α → β} {f' : α → β'}
  {g' : β' → γ}, (∀ (a : α), f (g a) = g' (f' a)) → f '' g '' s = g' '' f' '' s
-- Mathlib.Data.Quot
/-- A binary version of `Quot.recOnSubsingleton`.  -/
Quot.recOnSubsingleton₂ : {α : Sort u_1} →
  {β : Sort u_2} →
    {r : α → α → Prop} →
      {s : β → β → Prop} →
        {φ : Quot r → Quot s → Sort u_5} →
          [h : ∀ (a : α) (b : β), Subsingleton (φ (Quot.mk r a) (Quot.mk s b))] →
            (q₁ : Quot r) → (q₂ : Quot s) → ((a : α) → (b : β) → φ (Quot.mk r a) (Quot.mk s b)) → φ q₁ q₂
-- Mathlib.Data.List.Cycle
List.nextOr_eq_getElem?_idxOf_succ_of_mem_dropLast : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {a : α},
  a ∈ l.dropLast → ∀ (d : α), some (l.nextOr a d) = l[List.idxOf a l + 1]?
-- Mathlib.GroupTheory.GroupAction.Period
MulAction.period_one : ∀ {α : Type v} (M : Type u) [inst : Monoid M] [inst_1 : MulAction M α] (a : α), MulAction.period 1 a = 1
-- Mathlib.LinearAlgebra.Dimension.LinearMap
LinearMap.rank_comp_le_right : ∀ {K : Type u} {V : Type v} {V' V'₁ : Type v'} [inst : Semiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V'] [inst_4 : Module K V'] [inst_5 : AddCommGroup V'₁] [inst_6 : Module K V'₁]
  (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁), (f ∘ₗ g).rank ≤ g.rank
-- Lean.Meta.Sym.AlphaShareCommon
Lean.Meta.Sym.AlphaShareCommon.Context.mk.injEq : ∀ (env : Lean.Environment) (checkReducible checkProj : Bool) (env_1 : Lean.Environment)
  (checkReducible_1 checkProj_1 : Bool),
  ({ env := env, checkReducible := checkReducible, checkProj := checkProj } =
      { env := env_1, checkReducible := checkReducible_1, checkProj := checkProj_1 }) =
    (env = env_1 ∧ checkReducible = checkReducible_1 ∧ checkProj = checkProj_1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.distinct_keys_toList : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) t.toList
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
/-- Constructor for cochains to a single complex.  -/
CochainComplex.HomComplex.Cochain.toSingleMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        {X : C} →
          {K : CochainComplex C ℤ} →
            {p q : ℤ} →
              (K.X p ⟶ X) →
                {n : ℤ} → p + n = q → CochainComplex.HomComplex.Cochain K ((CochainComplex.singleFunctor C q).obj X) n
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.isConstant_coe : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter α} {b : β}, (∀ (x' : α), f x' = b) → (↑f).IsConstant
-- Init.Data.Order.Ord
Std.OrientedCmp.eq_symm : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {a b : α}, cmp a b = Ordering.eq → cmp b a = Ordering.eq
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_unitOfList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] [inst_2 : Inhabited α]
  {l : List α} {k : α}, l.contains k = false → (Std.TreeMap.Raw.unitOfList l cmp).getKey! k = default
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.coe_zetaUnit : ∀ {R : Type u_1} [inst : CommRing R], ↑ArithmeticFunction.zetaUnit = ↑ArithmeticFunction.zeta
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Functor.asEquivalence_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.IsEquivalence], F.asEquivalence.inverse = F.inv
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Set.Nonempty.ciSup_mem_image : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] (f : ι → α) {s : Set ι},
  s.Nonempty → s.Finite → ⨆ i ∈ s, f i ∈ f '' s
-- Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Polynomial.residueFieldMapCAlgEquiv_symm_C : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [inst_1 : I.IsPrime] (J : Ideal (Polynomial R)) [inst_2 : J.IsPrime]
  [inst_3 : J.LiesOver I] [inst_4 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)]
  [inst_5 : Localization.AtPrime.IsLiesOverAlgebra I J] (hJ : J = Ideal.map Polynomial.C I) (r : I.ResidueField),
  (Polynomial.residueFieldMapCAlgEquiv I J hJ).symm (RatFunc.C r) = (algebraMap I.ResidueField J.ResidueField) r
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- The `SlashInvariantForm` corresponding to `Function.const _ x`.  -/
SlashInvariantForm.constℝ : {Γ : Subgroup (GL (Fin 2) ℝ)} → [Γ.HasDetPlusMinusOne] → ℝ → SlashInvariantForm Γ 0
-- Init.Data.List.SplitOn.Lemmas
/-- When a list of the form `[...xs, sep, ...as]` is split at `a`, the first element is `xs`,
assuming no element in `xs` is equal to `a` but `sep` is equal to `a`.  -/
List.splitOn_append_cons_of_forall_mem_beq_eq_false : ∀ {α : Type u_1} {xs : List α} [inst : BEq α] {a : α},
  (∀ x ∈ xs, (x == a) = false) →
    ∀ (sep : α), (sep == a) = true → ∀ (as : List α), List.splitOn a (xs ++ sep :: as) = xs :: List.splitOn a as
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- **Alias** of `SimpleGraph.isAcyclic_iff_forall_isBridge`. -/
SimpleGraph.isAcyclic_iff_forall_edge_isBridge : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsAcyclic ↔ ∀ ⦃e : Sym2 V⦄, e ∈ G.edgeSet → G.IsBridge e
-- Mathlib.CategoryTheory.Monoidal.Hopf_
CategoryTheory.HopfObj.toBimonObj : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {inst_2 : CategoryTheory.BraidedCategory C} →
        {X : C} → [self : CategoryTheory.HopfObj X] → CategoryTheory.BimonObj X
-- Std.Time.Date.Unit.Day
Std.Time.Day.instDecidableLtOffset : {x y : Std.Time.Day.Offset} → Decidable (x < y)
-- Mathlib.CategoryTheory.Shift.Linear
CategoryTheory.Shift.instLinearLocalizationShiftFunctorOfCommShiftOfQ : ∀ (R : Type u_1) [inst : Ring R] {C : Type u_4} [inst_1 : CategoryTheory.Category.{v_1, u_4} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {M : Type u_3} [inst_4 : AddMonoid M]
  [inst_5 : CategoryTheory.HasShift C M] [∀ (n : M), CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor C n)]
  (W : CategoryTheory.MorphismProperty C) [inst_7 : CategoryTheory.HasShift W.Localization M] [W.Q.CommShift M]
  [inst_9 : CategoryTheory.Preadditive W.Localization] [inst_10 : CategoryTheory.Linear R W.Localization]
  [CategoryTheory.Functor.Linear R W.Q] (n : M),
  CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor W.Localization n)
-- Mathlib.Data.NNReal.Defs
Real.lt_of_toNNReal_lt : ∀ {r p : ℝ}, r.toNNReal < p.toNNReal → r < p
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppScalarRight_apply_tmul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {ι : Type u_5}
  [inst_7 : DecidableEq ι] (m : M) (p : ι →₀ R),
  (TensorProduct.finsuppScalarRight R S M ι) (m ⊗ₜ[R] p) = p.sum fun i n => fun₀ | i => n • m
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- Auxiliary definition for `ComonToMonOpOpObj`.  -/
CategoryTheory.Comon.ComonToMonOpOpObjMon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (A : CategoryTheory.Comon C) → CategoryTheory.MonObj (Opposite.op A.X)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.instIsScalarTowerSubtypeMem : ∀ {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [inst : SetLike S α] [inst_1 : SMul M N] [inst_2 : SMul M α]
  [inst_3 : Monoid N] [inst_4 : MulAction N α] [inst_5 : SMulMemClass S N α] [inst_6 : IsScalarTower M N α] (s : S),
  IsScalarTower M N ↥s
-- Mathlib.Algebra.Group.Hom.Defs
Monoid.End.instFunLike.eq_1 : ∀ (M : Type u_4) [inst : MulOne M],
  Monoid.End.instFunLike M = { coe := Monoid.End.instFunLike._aux_1 M, coe_injective := ⋯ }
-- Std.Data.DTreeMap.Basic
/-- Support for the `for` loop construct in `do` blocks. Iteration happens in ascending order.  -/
Std.DTreeMap.forIn : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {δ : Type w} →
        {m : Type w → Type w₂} → [Monad m] → ((a : α) → β a → δ → m (ForInStep δ)) → δ → Std.DTreeMap α β cmp → m δ
-- Mathlib.Algebra.Group.Finsupp
/-- `Finsupp.mapRange.AddMonoidHom` as an equiv.  -/
Finsupp.mapRange.addEquiv : {ι : Type u_1} →
  {M : Type u_3} →
    {N : Type u_4} → [inst : AddCommMonoid M] → [inst_1 : AddCommMonoid N] → M ≃+ N → (ι →₀ M) ≃+ (ι →₀ N)
-- Mathlib.GroupTheory.Subgroup.Center
IsConj.eq_of_right_mem_center : ∀ {M : Type u_2} [inst : Monoid M] {g h : M}, IsConj g h → h ∈ Set.center M → g = h
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
CategoryTheory.Preadditive.toCommGrp_obj_X : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C] (X : C),
  ((CategoryTheory.Preadditive.toCommGrp C).obj X).X = X
-- Aesop.Tree.TreeM
Aesop.incrementNumRapps : optParam ℕ 1 → Aesop.TreeM Unit
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.sigmaSigmaIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} (f : ι → Type u_2) (g : (i : ι) → f i → C)
  [inst_1 : ∀ (i : ι), CategoryTheory.Limits.HasCoproduct (g i)]
  [inst_2 : CategoryTheory.Limits.HasCoproduct fun i => ∐ g i],
  (CategoryTheory.Limits.sigmaSigmaIso f g).inv =
    CategoryTheory.Limits.Sigma.desc fun x =>
      match x with
      | ⟨i, x⟩ =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (g i) x)
          (CategoryTheory.Limits.Sigma.ι (fun i => ∐ g i) i)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ParameterInformationLabel.range.injEq : ∀ (startUtf16Offset endUtf16Offset startUtf16Offset_1 endUtf16Offset_1 : ℕ),
  (Lean.Lsp.ParameterInformationLabel.range startUtf16Offset endUtf16Offset =
      Lean.Lsp.ParameterInformationLabel.range startUtf16Offset_1 endUtf16Offset_1) =
    (startUtf16Offset = startUtf16Offset_1 ∧ endUtf16Offset = endUtf16Offset_1)
-- Mathlib.Topology.VectorBundle.Basic
VectorPrebundle.mk.injEq : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : (x : B) → TopologicalSpace (E x)]
  (pretrivializationAtlas : Set (Bundle.Pretrivialization F Bundle.TotalSpace.proj))
  (pretrivialization_linear' : ∀ e ∈ pretrivializationAtlas, Bundle.Pretrivialization.IsLinear R e)
  (pretrivializationAt : B → Bundle.Pretrivialization F Bundle.TotalSpace.proj)
  (mem_base_pretrivializationAt : ∀ (x : B), x ∈ (pretrivializationAt x).baseSet)
  (pretrivialization_mem_atlas : ∀ (x : B), pretrivializationAt x ∈ pretrivializationAtlas)
  (exists_coordChange :
    ∀ e ∈ pretrivializationAtlas,
      ∀ e' ∈ pretrivializationAtlas,
        ∃ f,
          ContinuousOn f (e.baseSet ∩ e'.baseSet) ∧
            ∀ b ∈ e.baseSet ∩ e'.baseSet, ∀ (v : F), (f b) v = (↑e' ⟨b, e.symm b v⟩).2)
  (totalSpaceMk_isInducing : ∀ (b : B), Topology.IsInducing (↑(pretrivializationAt b) ∘ Bundle.TotalSpace.mk b))
  (pretrivializationAtlas_1 : Set (Bundle.Pretrivialization F Bundle.TotalSpace.proj))
  (pretrivialization_linear'_1 : ∀ e ∈ pretrivializationAtlas_1, Bundle.Pretrivialization.IsLinear R e)
  (pretrivializationAt_1 : B → Bundle.Pretrivialization F Bundle.TotalSpace.proj)
  (mem_base_pretrivializationAt_1 : ∀ (x : B), x ∈ (pretrivializationAt_1 x).baseSet)
  (pretrivialization_mem_atlas_1 : ∀ (x : B), pretrivializationAt_1 x ∈ pretrivializationAtlas_1)
  (exists_coordChange_1 :
    ∀ e ∈ pretrivializationAtlas_1,
      ∀ e' ∈ pretrivializationAtlas_1,
        ∃ f,
          ContinuousOn f (e.baseSet ∩ e'.baseSet) ∧
            ∀ b ∈ e.baseSet ∩ e'.baseSet, ∀ (v : F), (f b) v = (↑e' ⟨b, e.symm b v⟩).2)
  (totalSpaceMk_isInducing_1 : ∀ (b : B), Topology.IsInducing (↑(pretrivializationAt_1 b) ∘ Bundle.TotalSpace.mk b)),
  ({ pretrivializationAtlas := pretrivializationAtlas, pretrivialization_linear' := pretrivialization_linear',
        pretrivializationAt := pretrivializationAt, mem_base_pretrivializationAt := mem_base_pretrivializationAt,
        pretrivialization_mem_atlas := pretrivialization_mem_atlas, exists_coordChange := exists_coordChange,
        totalSpaceMk_isInducing := totalSpaceMk_isInducing } =
      { pretrivializationAtlas := pretrivializationAtlas_1, pretrivialization_linear' := pretrivialization_linear'_1,
        pretrivializationAt := pretrivializationAt_1, mem_base_pretrivializationAt := mem_base_pretrivializationAt_1,
        pretrivialization_mem_atlas := pretrivialization_mem_atlas_1, exists_coordChange := exists_coordChange_1,
        totalSpaceMk_isInducing := totalSpaceMk_isInducing_1 }) =
    (pretrivializationAtlas = pretrivializationAtlas_1 ∧ pretrivializationAt = pretrivializationAt_1)
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
spinGroup.toUnits_injective : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M}, Function.Injective ⇑spinGroup.toUnits
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.instIsEquiv : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X}, IsEquiv (Path x₀ x₁) Path.Homotopic
-- Mathlib.GroupTheory.QuotientGroup.Finite
/-- If `ker(G →+ H)` and `H` are finite, then `G` is finite.  -/
AddGroup.fintypeOfKerOfCodom : {G : Type u_2} →
  {H : Type u_3} →
    [inst : AddGroup G] → [inst_1 : AddGroup H] → [Fintype H] → (g : G →+ H) → [Fintype ↥g.ker] → Fintype G
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.face_inter_face : ∀ {n : ℕ} (S₁ S₂ : Finset (Fin (n + 1))),
  SSet.stdSimplex.face S₁ ⊓ SSet.stdSimplex.face S₂ = SSet.stdSimplex.face (S₁ ⊓ S₂)
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.SimpCongrTheorems.mk.inj : ∀ {lemmas lemmas_1 : Lean.SMap Lean.Name (List Lean.Meta.SimpCongrTheorem)},
  { lemmas := lemmas } = { lemmas := lemmas_1 } → lemmas = lemmas_1
-- Mathlib.CategoryTheory.Limits.Creates
/-- Dual of definition 3.3.1 of [Riehl].
We say that `F` creates colimits of `K` if, given any limit cocone `c` for
`K ⋙ F` (i.e. below) we can lift it to a cocone "above", and further that `F`
reflects limits for `K`.

If `F` reflects isomorphisms, it suffices to show only that the lifted cocone is
a limit - see `createsColimitOfReflectsIso`.
 -/
CategoryTheory.CreatesColimit : {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] →
            CategoryTheory.Functor J C → CategoryTheory.Functor C D → Type (max (max (max (max u₁ u₂) v₁) v₂) w)
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.flipIsoCurrySwapUncurry_hom_app_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : D) (X_1 : C),
  (F.flipIsoCurrySwapUncurry.hom.app X).app X_1 = CategoryTheory.CategoryStruct.id ((F.obj X_1).obj X)
-- Mathlib.Data.PEquiv
Equiv.toPEquiv_trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α ≃ β) (g : β ≃ γ),
  (f.trans g).toPEquiv = f.toPEquiv.trans g.toPEquiv
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.subsingleton_of_ediam_eq_zero : ∀ {α : Type u_1} {G : SimpleGraph α}, G.ediam = 0 → Subsingleton α
-- Mathlib.Tactic.ClickSuggestions.Rewrite
/-- The outer expression in which the rewrite takes place.  -/
Mathlib.Tactic.ClickSuggestions.RwInfo.rootExpr : Mathlib.Tactic.ClickSuggestions.RwInfo → Lean.Expr
-- Mathlib.Data.Finsupp.WellFounded
Finsupp.wellFoundedLT_of_finite : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] [Finite α] [inst_2 : Preorder N] [WellFoundedLT N],
  WellFoundedLT (α →₀ N)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.comp.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N O : CategoryTheory.AddMon C} (f : M.Hom N) (g : N.Hom O),
  CategoryTheory.AddMon.comp f g = { hom := CategoryTheory.CategoryStruct.comp f.hom g.hom, isAddMonHom_hom := ⋯ }
-- Mathlib.Algebra.CharP.Lemmas
sub_pow_eq_mul_pow_sub_pow_div_char : ∀ {R : Type u_1} [inst : CommRing R] (x y : R) (n : ℕ) {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p],
  (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- A category has strong epi-mono factorisations if every morphism admits a strong epi-mono
factorisation.  -/
CategoryTheory.Limits.HasStrongEpiMonoFactorisations.has_fac : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasStrongEpiMonoFactorisations C]
  {X Y : C} (f : X ⟶ Y), Nonempty (CategoryTheory.Limits.StrongEpiMonoFactorisation f)
-- Mathlib.Order.Category.Lat
_private.Mathlib.Order.Category.Lat.0.Lat.Hom.mk.sizeOf_spec : ∀ {X Y : Lat} (hom' : LatticeHom ↑X ↑Y), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.Order.Defs.LinearOrder
max_comm : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), max a b = max b a
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
SSet.π₀.mk_surjective : ∀ {X : SSet}, Function.Surjective SSet.π₀.mk
-- Mathlib.RingTheory.Invariant.Basic
IsFractionRing.stabilizerHom.eq_1 : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (G : Type u_3)
  [inst_3 : Group G] [inst_4 : MulSemiringAction G B] [inst_5 : SMulCommClass G A B] (P : Ideal A) (Q : Ideal B)
  [inst_6 : Q.LiesOver P] (K : Type u_4) (L : Type u_5) [inst_7 : Field K] [inst_8 : Field L]
  [inst_9 : Algebra (A ⧸ P) K] [inst_10 : Algebra (B ⧸ Q) L] [inst_11 : Algebra (A ⧸ P) L]
  [inst_12 : IsScalarTower (A ⧸ P) (B ⧸ Q) L] [inst_13 : Algebra K L] [inst_14 : IsScalarTower (A ⧸ P) K L]
  [inst_15 : IsFractionRing (A ⧸ P) K] [inst_16 : IsFractionRing (B ⧸ Q) L],
  IsFractionRing.stabilizerHom G P Q K L =
    (IsFractionRing.fieldEquivOfAlgEquivHom K L).comp (Ideal.Quotient.stabilizerHom Q P G)
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Trie.brecOn.go : {α : Type} →
  {motive_1 : Lean.Meta.DiscrTree.Trie α → Sort u} →
    {motive_2 : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) → Sort u} →
      {motive_3 : List (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) → Sort u} →
        {motive_4 : Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α → Sort u} →
          (t : Lean.Meta.DiscrTree.Trie α) →
            ((t : Lean.Meta.DiscrTree.Trie α) → t.below → motive_1 t) →
              ((t : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)) →
                  Lean.Meta.DiscrTree.Trie.below_1 t → motive_2 t) →
                ((t : List (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)) →
                    Lean.Meta.DiscrTree.Trie.below_2 t → motive_3 t) →
                  ((t : Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) →
                      Lean.Meta.DiscrTree.Trie.below_3 t → motive_4 t) →
                    motive_1 t ×' t.below
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
SimpleGraph.isHermitian_adjMatrix : ∀ {V : Type u_1} (R : Type u_2) (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : NonAssocSemiring R]
  [inst_2 : StarRing R], (SimpleGraph.adjMatrix R G).IsHermitian
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.coe_copy : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (f : A →ₗc[R] B) (f' : A → B) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioo_subset_Ioc_union_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ioo a c ⊆ Set.Ioc a b ∪ Set.Ico b c
-- Mathlib.Analysis.Normed.Module.Bases
/-- The `enorm` of any projection is bounded by the basis constant.  -/
UnconditionalSchauderBasis.enorm_proj_le_enormProjBound : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {β : Type u_3} (b : UnconditionalSchauderBasis β 𝕜 X) (A : Finset β),
  ‖GeneralSchauderBasis.proj b A‖ₑ ≤ b.enormProjBound
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_mono : Monotone Real.arctan