mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.Integrable.comp_add_left : ∀ {G : Type u_4} {F : Type u_6} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.Measure G}
  [inst_2 : AddGroup G] [MeasurableAdd G] {f : G → F} [μ.IsAddLeftInvariant],
  MeasureTheory.Integrable f μ → ∀ (g : G), MeasureTheory.Integrable (fun t => f (g + t)) μ
-- Init.MetaTypes
Lean.Meta.Simp.ConfigCtx.mk : Lean.Meta.Simp.Config → Lean.Meta.Simp.ConfigCtx
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.log_inv_eq_ite : ∀ (x : ℂ), Complex.log x⁻¹ = if x.arg = Real.pi then -(starRingEnd ℂ) (Complex.log x) else -Complex.log x
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
/-- The property of objects in `HomotopyCategory C (.up ℤ)` whose
underlying cochain complex is bounded below. (Note: this property of
objects is not closed under isomorphisms.)  -/
HomotopyCategory.plus : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → CategoryTheory.ObjectProperty (HomotopyCategory C (ComplexShape.up ℤ))
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap' : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : Polynomial.MonicDegreeEq R n),
  (Polynomial.UniversalFactorizationRing.fromTensor m k hn p).comp (MvPolynomial.universalFactorizationMap R n m k hn) =
    (MvPolynomial.mapEquivMonic R (Polynomial.UniversalFactorizationRing m k hn p) n).symm
      (Polynomial.UniversalFactorizationRing.monicDegreeEq m k hn p)
-- Mathlib.Logic.Equiv.Defs
Equiv.ulift_apply : ∀ {α : Type v}, ⇑Equiv.ulift = ULift.down
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to0.trAux.eq_2 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (M : Λ → Turing.TM1.Stmt Γ Λ σ) (s : Γ) (x : σ) (a : Γ → σ → Γ)
  (q : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1to0.trAux M s (Turing.TM1.Stmt.write a q) x = ((some q, x), Turing.TM0.Stmt.write (a s x))
-- Mathlib.Algebra.Polynomial.Derivation
/-- `Polynomial.mkDerivation` as a linear equivalence.  -/
Polynomial.mkDerivationEquiv : (R : Type u_1) →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] →
        [inst_2 : Module R A] →
          [inst_3 : Module (Polynomial R) A] →
            [inst_4 : IsScalarTower R (Polynomial R) A] → A ≃ₗ[R] Derivation R (Polynomial R) A
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.gcd_mono : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s₁ s₂ : Finset β}
  {f : β → α}, s₁ ⊆ s₂ → s₂.gcd f ∣ s₁.gcd f
-- Mathlib.Topology.Algebra.InfiniteSum.Module
AddAction.automorphize.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_11} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [inst_2 : AddGroup α] [inst_3 : AddAction α β] (f : β → M),
  AddAction.automorphize f = Quotient.lift (fun b => ∑' (a : α), f (a +ᵥ b)) ⋯
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdUniformlyOn.mono : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] {t : Set β}, HasProdUniformlyOn f g t → s ⊆ t → HasProdUniformlyOn f g s
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_univ : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X}, ∫ (x : X) in Set.univ, f x ∂μ = ∫ (x : X), f x ∂μ
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.prevn : ∀ {s t₁ t₂ : String} {p : s.Pos},
  p.Splits t₁ t₂ →
    ∀ (n : ℕ),
      (p.prevn n).Splits (String.ofList (List.take (t₁.toList.length - n) t₁.toList))
        (String.ofList (List.drop (t₁.toList.length - n) t₁.toList) ++ t₂)
-- Batteries.Data.String.Lemmas
String.toList_take : ∀ (s : String) (n : ℕ), (String.Legacy.take s n).toList = List.take n s.toList
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- `P.HasPushoutsAlong f` states that for any morphism satisfying `P` with the same domain
as `f`, the pushout of that morphism along `f` exists.  -/
CategoryTheory.MorphismProperty.HasPushoutsAlong : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → {X Y : C} → (X ⟶ Y) → Prop
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rcc_succ_right_eq_push : ∀ {m n : ℕ}, m ≤ n + 1 → (m...=n + 1).toArray = (m...=n).toArray.push (n + 1)
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.map_le_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (P : CategoryTheory.MorphismProperty C) {F : CategoryTheory.Functor C D} (Q : CategoryTheory.MorphismProperty D)
  [Q.RespectsIso], P.map F ≤ Q ↔ P ≤ Q.inverseImage F
-- Mathlib.Algebra.Group.Irreducible.Defs
irreducible_or_factor : ∀ {M : Type u_1} [inst : Monoid M] {p : M}, ¬IsUnit p → Irreducible p ∨ ∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ p = a * b
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Cokleisli.Hom.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {U : CategoryTheory.Comonad C} → {c c' : CategoryTheory.Cokleisli U} → (U.obj c.of ⟶ c'.of) → c.Hom c'
-- Mathlib.Algebra.Order.Group.PosPart
negPart_pos : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a : α} [AddLeftMono α], a < 0 → 0 < a⁻
-- Mathlib.LinearAlgebra.Matrix.Action
Matrix.instIsScalarTowerMulOppositeForallOfSMulCommClass : ∀ {n : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : DistribSMul S R] [SMulCommClass S R R], IsScalarTower S (Matrix n n R)ᵐᵒᵖ (n → R)
-- Mathlib.Analysis.Asymptotics.TVS
/-- A version of `IsLittleOTVS.exists_eventuallyLE_mul`
where `ε` is quantified over `ℝ≥0∞` instead of `ℝ≥0`.  -/
Asymptotics.IsLittleOTVS.exists_eventuallyLE_mul_ennreal : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {f : α → E} {g : α → F} {l : Filter α},
  f =o[𝕜; l] g →
    ∀ {U : Set E},
      U ∈ nhds 0 →
        ∃ V ∈ nhds 0, ∀ (ε : ENNReal), ε ≠ 0 → (fun x => egauge 𝕜 U (f x)) ≤ᶠ[l] fun x => ε * egauge 𝕜 V (g x)
-- Mathlib.Analysis.SpecialFunctions.Arcosh
Real.cosh_injOn : Set.InjOn Real.cosh (Set.Ici 0)
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
/-- The function `log⁺` equals `log` for all natural numbers.  -/
Real.log_of_nat_eq_posLog : ∀ {n : ℕ}, (↑n).posLog = Real.log ↑n
-- Mathlib.Data.Set.NAry
Set.image2_comm : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {g : β → α → γ},
  (∀ (a : α) (b : β), f a b = g b a) → Set.image2 f s t = Set.image2 g t s
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- A module with a nonzero vector `v` has dimension 1 iff every vector is a multiple of `v`.
 -/
finrank_eq_one_iff_of_nonzero' : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (v : V),
  v ≠ 0 → (Module.finrank K V = 1 ↔ ∀ (w : V), ∃ c, c • v = w)
-- Mathlib.Topology.Connected.PathConnected
/-- Constructor for maps from `ZerothHomotopy X`.  -/
ZerothHomotopy.lift : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {T : Type u_4} → (f : X → T) → (∀ ⦃x y : X⦄ (x_1 : Path x y), f x = f y) → ZerothHomotopy X → T
-- Mathlib.Probability.Independence.Kernel.Indep
/-- **Alias** of the forward direction of `ProbabilityTheory.Kernel.iIndep_congr`. -/
ProbabilityTheory.Kernel.iIndep.congr : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m : ι → MeasurableSpace Ω}
  {_mΩ : MeasurableSpace Ω} {κ η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α},
  ⇑κ =ᵐ[μ] ⇑η → ProbabilityTheory.Kernel.iIndep m κ μ → ProbabilityTheory.Kernel.iIndep m η μ
-- Init.Grind.AC
Lean.Grind.AC.superpose_ac_cert.eq_1 : ∀ (r₁ c r₂ lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs : Lean.Grind.AC.Seq),
  Lean.Grind.AC.superpose_ac_cert r₁ c r₂ lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs =
    (((lhs₁.beq' (c.union_k r₁)).and' (lhs₂.beq' (c.union_k r₂))).and' (lhs.beq' (r₂.union_k rhs₁))).and'
      (rhs.beq' (r₁.union_k rhs₂))
-- Mathlib.Order.Compare
cmp_toDual : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] (x y : α),
  cmp (OrderDual.toDual x) (OrderDual.toDual y) = cmp y x
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.instSingleton : {α : Type u_1} → [inst : TopologicalSpace α] → Singleton α (TopologicalSpace.NonemptyCompacts α)
-- Mathlib.Data.List.Cycle
Cycle.subsingleton_reverse_iff : ∀ {α : Type u_1} {s : Cycle α}, s.reverse.Subsingleton ↔ s.Subsingleton
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.one_le_floor_iff : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R]
  (x : R), 1 ≤ ⌊x⌋₊ ↔ 1 ≤ x
-- Mathlib.Probability.Kernel.Category.SFinKer
instCoeSortSFinKerType : CoeSort SFinKer (Type u_1)
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
bddAbove_inv : ∀ {G : Type u_2} [inst : Group G] [inst_1 : Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G},
  BddAbove s⁻¹ ↔ BddBelow s
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.partNum_eq_s_a : ∀ {α : Type u_1} {g : GenContFract α} {n : ℕ} {gp : GenContFract.Pair α},
  g.s.get? n = some gp → g.partNums.get? n = some gp.a
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.congr_zpow : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f : M ≃ₗ[R] M) (g : N ≃ₗ[R] N) (n : ℤ),
  TensorProduct.congr f g ^ n = TensorProduct.congr (f ^ n) (g ^ n)
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presheaf.IsSheaf.isSheafFor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {P : CategoryTheory.Functor Cᵒᵖ (Type w)},
  CategoryTheory.Presheaf.IsSheaf J P → ∀ {X : C}, ∀ S ∈ J X, CategoryTheory.Presieve.IsSheafFor P S.arrows
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.functorExtension_map_app : ∀ (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] [inst_2 : CategoryTheory.IsIdempotentComplete D]
  {X Y : CategoryTheory.Functor C D} (f : X ⟶ Y) (X_1 : CategoryTheory.Idempotents.Karoubi C),
  ((CategoryTheory.Idempotents.functorExtension C D).map f).app X_1 =
    (CategoryTheory.Idempotents.toKaroubiEquivalence D).inverse.map
      (((CategoryTheory.Idempotents.functorExtension₂ C D).map f).app X_1)
-- Mathlib.Topology.Neighborhoods
/-- The open sets containing `x` are a basis for the neighborhood filter. See `nhds_basis_opens'`
for a variant using open neighborhoods instead.  -/
nhds_basis_opens : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X), (nhds x).HasBasis (fun s => x ∈ s ∧ IsOpen s) fun s => s
-- Init.Data.List.Int.Sum
List.sum_append_int : ∀ {l₁ l₂ : List ℤ}, (l₁ ++ l₂).sum = l₁.sum + l₂.sum
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.takeWhile.go.eq_def : ∀ {α : Type u} (p : α → Bool) (as : Array α) (i : ℕ) (acc : Array α),
  Array.takeWhile.go✝ p as i acc =
    if h : i < as.size then
      have a := as[i];
      if p a = true then Array.takeWhile.go✝ p as (i + 1) (acc.push a) else acc
    else acc
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasLimit_op_iff_hasColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  {F : CategoryTheory.Functor J C}, CategoryTheory.Limits.HasLimit F.op ↔ CategoryTheory.Limits.HasColimit F
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
/-- The type of extensions of a given basis, defined as an inductive type.
Given a `basis : Basis` and `ex : BasisExtension basis` of it, one can use `getBasis` to produce a
basis `basis'` for which `basis <+ basis'`. Moreover, all such bases for which `basis` is a sublist
can be obtained in this manner. In this sense `BasisExtension` is a `Type`-valued analogue
of `List.Sublist`.  -/
Tactic.ComputeAsymptotics.BasisExtension : Tactic.ComputeAsymptotics.Basis → Type
-- Init.Control.Except
/-- Handles exceptions thrown in the `Except ε` monad.

If `ma` is successful, its result is returned. If it throws an exception, then `handle` is invoked
on the exception's value.

Examples:
 * `(pure 2 : Except String Nat).tryCatch (pure ·.length) = pure 2`
 * `(throw "Error" : Except String Nat).tryCatch (pure ·.length) = pure 5`
 * `(throw "Error" : Except String Nat).tryCatch (fun x => throw ("E: " ++ x)) = throw "E: Error"`
 -/
Except.tryCatch : {ε : Type u} → {α : Type u_1} → Except ε α → (ε → Except ε α) → Except ε α
-- Mathlib.ModelTheory.Syntax
/-- Restricts a bounded formula to only use a particular set of free variables.  -/
FirstOrder.Language.BoundedFormula.restrictFreeVar : {L : FirstOrder.Language} →
  {α : Type u'} →
    {β : Type v'} →
      [inst : DecidableEq α] → {n : ℕ} → (φ : L.BoundedFormula α n) → (↥φ.freeVarFinset → β) → L.BoundedFormula β n
-- Mathlib.Topology.Algebra.Group.CompactOpen
/-- `ContinuousAddMonoidHom _ f` is a functor.  -/
ContinuousAddMonoidHom.compLeft : {A : Type u_2} →
  {B : Type u_3} →
    (E : Type u_6) →
      [inst : AddMonoid A] →
        [inst_1 : AddMonoid B] →
          [inst_2 : AddCommGroup E] →
            [inst_3 : TopologicalSpace A] →
              [inst_4 : TopologicalSpace B] →
                [inst_5 : TopologicalSpace E] → [inst_6 : IsTopologicalAddGroup E] → (A →ₜ+ B) → (B →ₜ+ E) →ₜ+ A →ₜ+ E
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_union_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₂.contains k = false → (m₁.union m₂).getKey? k = m₁.getKey? k
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.card_vadd_finset : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : AddGroup α] [inst_2 : AddAction α β] (a : α)
  (s : Finset β), (a +ᵥ s).card = s.card
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_X₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE._auto_3),
  (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₃ = X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
-- Lean.Elab.DeclModifiers
Lean.Elab.Modifiers.isPrivate : Lean.Elab.Modifiers → Bool
-- Mathlib.Algebra.Group.Nat.Hom
/-- Additive homomorphisms from `ℕ` are defined by the image of `1`.  -/
multiplesHom : (M : Type u_1) → [inst : AddMonoid M] → M ≃ (ℕ →+ M)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.mem_slitPlane : ∀ (z : UpperHalfPlane), ↑z ∈ Complex.slitPlane
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mul_le_max : ∀ (a b : Cardinal.{u_1}), a * b ≤ max (max a b) Cardinal.aleph0
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instHashableLambdaTheoremType : Hashable Mathlib.Meta.FunProp.LambdaTheoremType
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- The lemma name with hover information  -/
Mathlib.Tactic.LibraryRewrite.RewriteInterface.prettyLemma : Mathlib.Tactic.LibraryRewrite.RewriteInterface → Lean.Widget.CodeWithInfos
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instInv.eq_1 : ∀ {α : Type u_1} [inst : Inv α], Lex.instInv = inst
-- Mathlib.Data.EReal.Operations
EReal.mul_sub_of_nonneg_of_nonpos : ∀ {a b c : EReal}, 0 ≤ b → c ≤ 0 → a * (b - c) = a * b - a * c
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.le_rpow_inv_iff_of_neg : ∀ {x y z : ℝ}, 0 < x → 0 < y → z < 0 → (x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.standardσ_cons_assoc : ∀ (L : List ℕ) (a : ℕ) {m₁ m₂ : ℕ} (h : m₂ + (a :: L).length = m₁) {Z : SimplexCategoryGenRel}
  (h_1 : SimplexCategoryGenRel.mk m₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.standardσ (a :: L) h) h_1 =
    CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.standardσ L ⋯)
      (CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.σ (Fin.ofNat (m₂ + 1) a)) h_1)
-- Init.Data.Int.Order
Int.ofNat_succ_pos : ∀ (n : ℕ), 0 < ↑n.succ
-- Mathlib.Data.FinEnum
FinEnum.instInt64 : FinEnum Int64
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.hom_comp : ∀ {R : Type u} [inst : CommRing R] {A B C : CommAlgCat R} (f : A ⟶ B) (g : B ⟶ C),
  CommAlgCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (CommAlgCat.Hom.hom g).comp (CommAlgCat.Hom.hom f)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.IsQuasicoherent.of_coversTop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat]
  [inst_3 : ∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasSheafify ((J.over X).over Y) AddCommGrpCat]
  [inst_4 : ∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat]
  {R : CategoryTheory.Sheaf J RingCat} (M : SheafOfModules R) {I : Type u} (X : I → C),
  J.CoversTop X → ∀ [∀ (i : I), (M.over (X i)).IsQuasicoherent], M.IsQuasicoherent
-- Mathlib.Data.Set.Sups
Set.image_infs : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β]
  [inst_2 : FunLike F α β] [InfHomClass F α β] (f : F) (s t : Set α), ⇑f '' (s ⊼ t) = ⇑f '' s ⊼ ⇑f '' t
-- Batteries.Data.List.Lemmas
List.getElem_getElem_idxsOf_sub_of_lawful : ∀ {α : Type u_1} {i : ℕ} {xs : List α} {x : α} [inst : BEq α] [LawfulBEq α] (s : ℕ)
  (h : i < (List.idxsOf x xs s).length), xs[(List.idxsOf x xs s)[i] - s] = x
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Equivalence.mapCommGrp_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D] (e : C ≌ D)
  [inst_6 : e.functor.Braided] [inst_7 : e.inverse.Braided], e.mapCommGrp.inverse = e.inverse.mapCommGrp
-- Mathlib.Algebra.Category.Grp.EnoughInjectives
CommGrpCat.enoughInjectives : CategoryTheory.EnoughInjectives CommGrpCat
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.isoMk_inv_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentData f} (e : (i : ι) → D₁.obj i ≅ D₂.obj i)
  (comm :
    autoParam
      (∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂)
        (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
        (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q),
        CategoryTheory.CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (e i₁).hom) (D₂.hom q f₁ f₂ ⋯ ⋯) =
          CategoryTheory.CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯) ((F.map f₂.op.toLoc).toFunctor.map (e i₂).hom))
      CategoryTheory.Pseudofunctor.DescentData.isoMk._auto_1)
  (i : ι), (CategoryTheory.Pseudofunctor.DescentData.isoMk e comm).inv.hom i = (e i).inv
-- Mathlib.Order.CompleteBooleanAlgebra
Prod.instCoframe : {α : Type u} → {β : Type v} → [Order.Coframe α] → [Order.Coframe β] → Order.Coframe (α × β)
-- Std.Async.Basic
Std.Async.instMonadAwaitStateRefT' : {t m : Type → Type} → {s n : Type} → [Std.Async.MonadAwait t m] → Std.Async.MonadAwait t (StateRefT' s n m)
-- Init.Data.String.TakeDrop
/-- If `pat` matches at `pos`, returns the position after the end of the match.
Returns `none` otherwise.

This function is generic over all currently supported patterns.
 -/
String.Pos.skip? : {ρ : Type} → {s : String} → s.Pos → (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → Option s.Pos
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
CategoryTheory.Monoidal.tensorUnit : CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Cat = CategoryTheory.Cat.chosenTerminal
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.toContinuousLinearEquiv_toSpanSingletonLIE : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E], ↑(ContinuousLinearMap.toSpanSingletonLIE 𝕜 E) = ContinuousLinearMap.toSpanSingletonCLE
-- Mathlib.Algebra.Group.Hom.Basic
/-- Inversion on a commutative group, considered as a monoid homomorphism.  -/
invMonoidHom : {α : Type u_1} → [inst : DivisionCommMonoid α] → α →* α
-- Mathlib.Algebra.Algebra.Spectrum.Basic
IsUnit.val_inv_subInvSMul : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : Rˣ} {s : R} {a : A}
  (h : IsUnit (r • (algebraMap R A) s - a)), ↑h.subInvSMul⁻¹ = r • ↑h.unit⁻¹
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.ext_iff : ∀ {A : Type u_2} {B : Type u_3} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] {f g : A →ₜ+ B}, f = g ↔ ∀ (x : A), f x = g x
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.below.filter₀ : ∀ {α : Type u}
  {motive : {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (a : Std.DHashMap.Raw α β) → a.WF → Prop}
  {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size}
  {f : (a : α) → β a → Bool} (a : m.WF), Std.DHashMap.Raw.WF.below a → motive m a → Std.DHashMap.Raw.WF.below ⋯
-- Lean.Meta.Tactic.Acyclic
_private.Lean.Meta.Tactic.Acyclic.0.Lean.MVarId.acyclic.go : Lean.MVarId → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Plausible.Testable
Plausible.TestResult.success.sizeOf_spec : ∀ {p : Prop} [inst : SizeOf p] (a : Unit ⊕' p), sizeOf (Plausible.TestResult.success a) = 1 + sizeOf a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
CategoryTheory.IsPushout.of_has_biproduct : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.IsPushout 0 0 CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.inr
-- Mathlib.Topology.Gluing
TopCat.GlueData.preimage_image_eq_image' : ∀ (D : TopCat.GlueData) (i j : D.J) (U : Set ↑(D.U i)),
  ⇑(CategoryTheory.ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(CategoryTheory.ConcreteCategory.hom (D.ι i)) '' U =
    ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (D.t i j) (D.f j i))) ''
      ⇑(CategoryTheory.ConcreteCategory.hom (D.f i j)) ⁻¹' U
-- Init.Data.Array.Lemmas
Array.flatten_filter_ne_empty : ∀ {α : Type u_1} [inst : DecidablePred fun xs => xs ≠ #[]] {xss : Array (Array α)},
  (Array.filter (fun xs => decide (xs ≠ #[])) xss).flatten = xss.flatten
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Triangle inequality** for the norm.  -/
norm_mul₃_le' : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a b c : E}, ‖a * b * c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖
-- Mathlib.Topology.Algebra.Group.Basic
Prod.instIsTopologicalGroup : ∀ {G : Type w} {H : Type x} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G]
  [inst_3 : TopologicalSpace H] [inst_4 : Group H] [IsTopologicalGroup H], IsTopologicalGroup (G × H)