mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type w}
  [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  (s : Finset (CategoryTheory.Discrete α)),
  (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj F).obj s = ∐ fun x => F.obj ↑x
-- Mathlib.Tactic.Linarith.Verification
/-- `step c pf npf coeff` assumes that `pf` is a proof of `t1 R1 0` and `npf` is a proof
of `t2 R2 0`. It uses `mkSingleCompZeroOf` to prove `t1 + coeff*t2 R 0`, and returns `R`
along with this proof.
 -/
_private.Mathlib.Tactic.Linarith.Verification.0.Mathlib.Tactic.Linarith.mkLTZeroProof.step : Mathlib.Ineq → Lean.Expr → Lean.Expr → ℕ → Lean.MetaM (Mathlib.Ineq × Lean.Expr)
-- Mathlib.Combinatorics.Additive.CauchyDavenport
_private.Mathlib.Combinatorics.Additive.CauchyDavenport.0.devosMulRel_of_le : ∀ {α : Type u_2} [inst : Group α] [inst_1 : DecidableEq α] {x y : Finset α × Finset α},
  (x.1 * x.2).card ≤ (y.1 * y.2).card → y.1.card + y.2.card < x.1.card + x.2.card → DevosMulRel✝ x y
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.add_int : ∀ {p x : ℝ}, LiouvilleWith p x → ∀ (m : ℤ), LiouvilleWith p (x + ↑m)
-- Mathlib.Analysis.ODE.Transform
IsIntegralCurveOn.comp_sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {s : Set ℝ},
  IsIntegralCurveOn γ v s → ∀ (dt : ℝ), IsIntegralCurveOn (γ ∘ fun x => x - dt) (v ∘ fun x => x - dt) (dt +ᵥ s)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α}, k ∉ t₂ → (t₁ \ t₂).get? k = t₁.get? k
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestRevMatchAt_iff_splits : ∀ {pat s : String.Slice} {pos₁ pos₂ : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAt pat pos₁ pos₂ ↔
    ∃ t₁ t₂, pos₁.Splits t₁ (pat.copy ++ t₂) ∧ pos₂.Splits (t₁ ++ pat.copy) t₂
-- Mathlib.Order.Interval.Set.Disjoint
Set.Iic_disjoint_Ioi : ∀ {α : Type v} [inst : Preorder α] {a b : α}, a ≤ b → Disjoint (Set.Iic a) (Set.Ioi b)
-- Std.Async.ContextAsync
/-- Launches a `ContextAsync` computation as an asynchronous task with a forked child context.
The child context is automatically cancelled when the task completes or fails.
 -/
Std.Async.ContextAsync.async : {α : Type} →
  Std.Async.ContextAsync α →
    optParam Task.Priority Task.Priority.default → Std.Async.ContextAsync (Std.Async.AsyncTask α)
-- Mathlib.CategoryTheory.Adjunction.Mates
/-- A component of a transposed form of the conjugation definition.  -/
CategoryTheory.unit_conjugateEquiv : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ L₂ : CategoryTheory.Functor C D} {R₁ R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂)
  (α : L₂ ⟶ L₁) (c : C),
  CategoryTheory.CategoryStruct.comp (adj₁.unit.app c) (((CategoryTheory.conjugateEquiv adj₁ adj₂) α).app (L₁.obj c)) =
    CategoryTheory.CategoryStruct.comp (adj₂.unit.app c) (R₂.map (α.app c))
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- Two oriented angles in oppositely-oriented right-angled triangles are equal if twice those
angles are equal.  -/
EuclideanGeometry.oangle_eq_oangle_rev_of_two_zsmul_eq_of_angle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₄ p₅ p₆ : P},
  2 • EuclideanGeometry.oangle p₂ p₃ p₁ = 2 • EuclideanGeometry.oangle p₄ p₆ p₅ →
    EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 →
      EuclideanGeometry.angle p₄ p₅ p₆ = Real.pi / 2 →
        EuclideanGeometry.oangle p₂ p₃ p₁ = EuclideanGeometry.oangle p₄ p₆ p₅
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.coe_compl : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s : Finset α), ↑sᶜ = (↑s)ᶜ
-- Init.Data.Int.Gcd
Int.gcd_sub_right_left_of_dvd : ∀ {m k : ℤ} (n : ℤ), m ∣ k → (n - k).gcd m = n.gcd m
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ D` creates limits, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` creates colimits.  -/
CategoryTheory.Limits.createsColimitsOfSizeOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] →
            CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op
-- Mathlib.Data.Complex.Basic
/-- This shortcut instance ensures we do not find `CommSemiring` via the noncomputable
`Complex.field` instance.  -/
Complex.instCommSemiring : CommSemiring ℂ
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Real.Angle.toCircle_add : ∀ (θ₁ θ₂ : Real.Angle), (θ₁ + θ₂).toCircle = θ₁.toCircle * θ₂.toCircle
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ResolveSimpIdResult.simproc.injEq : ∀ (declName declName_1 : Lean.Name),
  (Lean.Elab.Tactic.ResolveSimpIdResult.simproc declName = Lean.Elab.Tactic.ResolveSimpIdResult.simproc declName_1) =
    (declName = declName_1)
-- Mathlib.ModelTheory.Fraisse
/-- Any embedding from a finitely generated `S` to an ultrahomogeneous structure `M`
can be extended to an embedding from any structure with an embedding to `M`.  -/
FirstOrder.Language.IsUltrahomogeneous.extend_embedding : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M],
  L.IsUltrahomogeneous M →
    ∀ {S : Type u_1} [inst_1 : L.Structure S],
      FirstOrder.Language.Structure.FG L S →
        ∀ {T : Type u_2} [inst_2 : L.Structure T] [h : Nonempty (L.Embedding T M)] (f : L.Embedding S M)
          (g : L.Embedding S T), ∃ f', f = f'.comp g
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.mul.congr_simp : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A]
  [inst_5 : NonUnitalNonAssocSemiring B] [inst_6 : Module R B] [inst_7 : SMulCommClass R B B]
  [inst_8 : IsScalarTower R B B], Algebra.TensorProduct.mul = Algebra.TensorProduct.mul
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_map_right_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T × T)
  {X_1 Y : CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag T)} (g : X_1 ⟶ Y),
  ((CategoryTheory.StructuredArrow.ofDiagEquivalence.functor X).map g).right.right = g.right
-- Mathlib.Topology.Order.OrderClosed
frontier_Iic_subset : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] (a : α),
  frontier (Set.Iic a) ⊆ {a}
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- **Alias** of `add_apply`. -/
SchwartzMap.add_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Add β}
  {inst_2 : Add F} [self : IsAddApply F α β] (f g : F) (x : α), (f + g) x = f x + g x
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsNonloop.of_isRestriction : ∀ {α : Type u_1} {M N : Matroid α} {e : α}, N.IsNonloop e → N.IsRestriction M → M.IsNonloop e
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.convolution_indicator_one_right : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {F : Type u_6} [inst : Monoid M] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid F] [inst_4 : Module S E] [inst_5 : Module S F]
  [inst_6 : TopologicalSpace F] (L : F →ₗ[S] E →ₗ[S] F) (f : M → F) (e : E),
  (∀ (y : F), (L y) e = y) → DiscreteConvolution.convolution L f ({1}.indicator fun x => e) = f
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.ctor.sizeOf_spec : ∀ (a : Lean.Name) (a_1 : List Lean.Meta.Match.Example),
  sizeOf (Lean.Meta.Match.Example.ctor a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- If `m` is a proper divisor of `n`, then `X ^ m - 1` divides
`∏ i ∈ Nat.properDivisors n, cyclotomic i R`.  -/
Polynomial.X_pow_sub_one_dvd_prod_cyclotomic : ∀ (R : Type u_1) [inst : CommRing R] {n m : ℕ},
  0 < n → m ∣ n → m ≠ n → Polynomial.X ^ m - 1 ∣ ∏ i ∈ n.properDivisors, Polynomial.cyclotomic i R
-- Mathlib.RingTheory.Localization.Away.Basic
Localization.awayMap_injective_iff : ∀ {S : Type u_2} [inst : CommSemiring S] {R : Type u_4} [inst_1 : CommRing R] {f : R →+* S} {r : R},
  Function.Injective ⇑(Localization.awayMap f r) ↔ ∀ (a : R), f a = 0 → ∃ n, r ^ n * a = 0
-- Mathlib.Topology.Category.LightProfinite.Extend
LightProfinite.Extend.functorOp_obj : ∀ {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite))
  (X : ℕ), (LightProfinite.Extend.functorOp c).obj X = CategoryTheory.CostructuredArrow.mk (c.π.app (Opposite.op X)).op
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.inl_isoPushout_inv_whiskerRight_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr)
  [inst_2 : CategoryTheory.Limits.HasPushout f g] {Q Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj P Q ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushout.inl f g) Q)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight hP.isoPushout.inv Q) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight inl Q) h
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.ShouldCanonResult.visit.sizeOf_spec : sizeOf Lean.Meta.Sym.Canon.ShouldCanonResult.visit✝ = 1
-- Mathlib.Topology.Filter
/-- **Alias** of `Filter.isOpen_setOfPred_mem`. -/
Filter.isOpen_setOf_mem : ∀ {α : Type u_2} {s : Set α}, IsOpen {l | s ∈ l}
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.card' : ∀ (K : Type u_1) [inst : Field K] [inst_1 : Fintype K], ∃ p, CharP K p ∧ ∃ n, Nat.Prime p ∧ Fintype.card K = p ^ ↑n
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `1` and `⁻¹` is a `InvOneClass`, if it admits an injective map that
preserves `1` and `⁻¹` to a `InvOneClass`.  See note [reducible non-instances].  -/
Function.Injective.invOneClass : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : One M₁] →
      [inst_1 : Inv M₁] →
        [inst_2 : InvOneClass M₂] →
          (f : M₁ → M₂) → Function.Injective f → f 1 = 1 → (∀ (x : M₁), f x⁻¹ = (f x)⁻¹) → InvOneClass M₁
-- Mathlib.Topology.Instances.Int
Int.cofinite_eq : Filter.cofinite = Filter.atBot ⊔ Filter.atTop
-- Mathlib.Data.PNat.Xgcd
PNat.gcd_rel_right : ∀ (a b : ℕ+), ↑(a.gcdW b) * ↑b = a.gcdY b * ↑a + ↑(a.gcd b)
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.IsDedekindDomain.ramificationIdx'_le_ramificationIdx' : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDedekindDomain S]
  [IsDomain R] [Module.IsTorsionFree R S] {S₀ : Type u_2} [inst_6 : CommRing S₀] [inst_7 : Algebra R S₀]
  [inst_8 : Algebra S₀ S] [IsScalarTower R S₀ S] (p : Ideal R) (P : Ideal S₀) (Q : Ideal S) [Q.LiesOver p]
  [hP : P.LiesOver p] [Q.IsPrime], p ≠ ⊥ → P.ramificationIdx' Q ≤ p.ramificationIdx' Q
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.forIn_filter : ∀ {α β γ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [inst : Std.Iterator α Id β] [inst_1 : Monad n]
  [inst_2 : Std.Internal.Do.Assertion Pred] [inst_3 : Std.Internal.Do.Assertion EPred]
  [inst_4 : Std.Internal.Do.WPMonad n Pred EPred] [Std.Iterators.Finite α Id] [inst_6 : Std.IteratorLoop α Id n]
  [Std.LawfulIteratorLoop α Id n] {it : Std.Iter β} {f : β → Bool} {init : γ} {g : β → γ → n (ForInStep γ)} {P : Pred}
  {Q : γ → Pred} {eQ : EPred},
  ⦃ P ⦄ forIn it init fun out acc => if f out = true then g out acc else pure (ForInStep.yield acc) ⦃ Q; eQ ⦄ →
    ⦃ P ⦄ forIn (Std.Iter.filter f it) init g ⦃ Q; eQ ⦄
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDateTime.instHAddOffset : HAdd Std.Time.PlainDateTime Std.Time.Day.Offset Std.Time.PlainDateTime
-- Mathlib.Tactic.FunProp.Mor
/-- Weak normal head form of an expression involving morphism applications. Additionally, `pred`
can specify which when to unfold definitions.

For example calling this on `coe (f a) b` will put `f` in weak normal head form instead of `coe`.
 -/
Mathlib.Meta.FunProp.Mor.whnfPred : Lean.Expr → (Lean.Expr → Lean.MetaM Bool) → Lean.MetaM Lean.Expr
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The underlying `Mor₂` term of a `WhiskerRight` term.  -/
Mathlib.Tactic.BicategoryLike.WhiskerRight.e : Mathlib.Tactic.BicategoryLike.WhiskerRight → Mathlib.Tactic.BicategoryLike.Mor₂
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsInt.nonneg_to_eq : ∀ {α : Type u_1} [inst : Ring α] {n : ℕ} {a a' : α}, Mathlib.Meta.NormNum.IsInt a (Int.ofNat n) → ↑n = a' → a = a'
-- Mathlib.LinearAlgebra.Complex.Determinant
/-- The determinant of `conjAe`, as a linear equiv.  -/
Complex.linearEquiv_det_conjAe : LinearEquiv.det ↑Complex.conjAe = -1
-- Mathlib.Topology.Closure
closure_union : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, closure (s ∪ t) = closure s ∪ closure t
-- Std.Sat.AIG.CNF
/-- The invariant to make sure that `marks` is well formed with respect to the `cnf`
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.Cache.inv : ∀ {aig : Std.Sat.AIG ℕ} {cnf : Std.Sat.CNF ℕ} (self : Std.Sat.AIG.toCNF.Cache✝ aig cnf),
  Std.Sat.AIG.toCNF.Cache.Inv✝ aig cnf (Std.Sat.AIG.toCNF.Cache.marks✝ self) ⋯
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.maxKey_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → ∀ (h : t₁.Equiv t₂) (h' : t₁.isEmpty = false), t₁.maxKey h' = t₂.maxKey ⋯
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.tag_apply : ∀ {ι : Type u_1} (n : ℕ) (ν : ι → ℤ) (i : ι), BoxIntegral.unitPartition.tag n ν i = (↑(ν i) + 1) / ↑n
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the identity `𝟙 f`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂.id₂M : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadMor₂ m] →
    Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.Mor₂
-- Lean.Linter.Init
Lean.Linter.LinterOptions.mk : Lean.Options → Lean.Linter.LinterSets → Lean.Linter.LinterOptions
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.gluing_U : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).U i =
    CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
/-- Every self-adjoint `LinearPMap` has dense domain.

This is not true by definition since we define the adjoint without the assumption that the
domain is dense, but the choice of the junk value implies that a `LinearPMap` cannot be self-adjoint
if it does not have dense domain.  -/
IsSelfAdjoint.dense_domain : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {A : E →ₗ.[𝕜] E}, IsSelfAdjoint A → Dense ↑A.domain
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.ofList_nil : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v}, Std.DHashMap.Const.ofList [] = ∅
-- Mathlib.Algebra.Ring.CharZero
Function.support_natCast : ∀ {α : Type u_1} {R : Type u_2} {n : ℕ} [inst : AddMonoidWithOne R] [CharZero R], n ≠ 0 → Function.support ↑n = Set.univ
-- Batteries.Data.Array.Basic
/-- Returns the first minimal element among `d` and elements of the array.
If `start` and `stop` are given, only the subarray `xs[start...stop]` is
considered (in addition to `d`).
 -/
Array.rangeMinWith : {α : Type u_1} → [ord : Ord α] → (xs : Array α) → α → optParam ℕ 0 → optParam ℕ xs.size → α
-- Mathlib.Data.Multiset.ZeroCons
Multiset.recOn_0 : ∀ {α : Type u_1} {C : Multiset α → Sort u_3} {C_0 : C 0} {C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)}
  {C_cons_heq :
    ∀ (a a' : α) (m : Multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)},
  Multiset.recOn 0 C_0 C_cons C_cons_heq = C_0
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.toComplex_add : ∀ (x y : GaussianInt), GaussianInt.toComplex (x + y) = GaussianInt.toComplex x + GaussianInt.toComplex y
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The definition of a Monge plane.  -/
Affine.Simplex.mongePlane_def : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 2)) (i₁ i₂ : Fin (n + 3)),
  s.mongePlane i₁ i₂ =
    AffineSubspace.mk' (Finset.centroid ℝ {i₁, i₂}ᶜ s.points) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓
      affineSpan ℝ (Set.range s.points)
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.lex_le_iff_of_unique : ∀ {σ : Type u_1} [inst : LinearOrder σ] [inst_1 : Unique σ] {c d : σ →₀ ℕ},
  MonomialOrder.lex.toSyn c ≤ MonomialOrder.lex.toSyn d ↔ c default ≤ d default
-- Lean.Setup
Lean.IRPhases.runtime.sizeOf_spec : sizeOf Lean.IRPhases.runtime = 1
-- Mathlib.Algebra.Group.Prod
Prod.instGroup : {G : Type u_1} → {H : Type u_2} → [Group G] → [Group H] → Group (G × H)
-- Lean.Elab.Do.Basic
Lean.Elab.Do.elabDoSeq : Lean.DoSeq → Lean.Elab.Do.DoElemCont → optParam Bool true → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.Analysis.Convex.Function
OrderIso.strictConcaveOn_symm : ∀ {𝕜 : Type u_1} {α : Type u_4} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid α]
  [inst_3 : PartialOrder α] [inst_4 : SMul 𝕜 α] [inst_5 : AddCommMonoid β] [inst_6 : PartialOrder β] [inst_7 : SMul 𝕜 β]
  (f : α ≃o β), StrictConvexOn 𝕜 Set.univ ⇑f → StrictConcaveOn 𝕜 Set.univ ⇑f.symm
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyIncomingCall.mk : Lean.Lsp.CallHierarchyItem → Array Lean.Lsp.Range → Lean.Lsp.CallHierarchyIncomingCall
-- Mathlib.Data.Nat.ModEq
Nat.chineseRemainder.congr_simp : ∀ {m n : ℕ} (co : n.Coprime m) (a b : ℕ), Nat.chineseRemainder co a b = Nat.chineseRemainder co a b
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.inv_inv_inv : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α),
  A⁻¹⁻¹⁻¹ = A⁻¹
-- Lean.Compiler.LCNF.Basic
/-- Return `true` if the given declaration has been annotated with `[inline]`, `[inline_if_reduce]`, `[macro_inline]`, or `[always_inline]`  -/
Lean.Compiler.LCNF.Decl.inlineable : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Decl pu → Bool
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.mul_eq_one_iff_eq_inv : ∀ {α : Type u} [inst : DivisionMonoid α] {a b : α}, IsUnit b → (a * b = 1 ↔ a = b⁻¹)
-- Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
/-- `𝔸ᶠ[R, K]` is notation for `IsDedekindDomain.FiniteAdeleRing R K`.  -/
IsDedekindDomain.FiniteAdeleRing.«term𝔸ᶠ[_,_]» : Lean.ParserDescr
-- Mathlib.Order.Bounded
Set.unbounded_gt_of_unbounded_ge : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α],
  Set.Unbounded (fun x1 x2 => x1 ≥ x2) s → Set.Unbounded (fun x1 x2 => x1 > x2) s
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithLowerSet.instInhabited : {α : Type u_1} → [Inhabited α] → Inhabited (Topology.WithLowerSet α)
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.LinarithData.mk.injEq : ∀ (maxVar : ℕ) (comps : Mathlib.Tactic.Linarith.PCompSet) (maxVar_1 : ℕ) (comps_1 : Mathlib.Tactic.Linarith.PCompSet),
  ({ maxVar := maxVar, comps := comps } = { maxVar := maxVar_1, comps := comps_1 }) =
    (maxVar = maxVar_1 ∧ comps = comps_1)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.map_mono : ∀ {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] [inst_7 : LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N N₂ : LieSubmodule R L M},
  N ≤ N₂ → LieSubmodule.map f N ≤ LieSubmodule.map f N₂
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- As `J` is nonempty, we can pick an arbitrary object `j₀ : J`. We use this object to define the
"one" in the colimit as the equivalence class of `⟨j₀, 1 : F.obj j₀⟩`.
 -/
MonCat.FilteredColimits.colimitOne : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J MonCat) → [CategoryTheory.IsFiltered J] → One (MonCat.FilteredColimits.M F)
-- Std.Http.Server
/-- Triggers cancellation of all requests and the accept loop, then waits for the server to fully shut down.
This is a convenience function combining `shutdown` and then `waitShutdown`.
 -/
Std.Http.Server.shutdownAndWait : Std.Http.Server → Std.Async.Async Unit
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₃Map_app_app : ∀ {C₁ : Type u_1} (C₂ : Type u_2) (C₃ : Type u_3) {D₁ : Type u_4} (D₂ : Type u_5) (D₃ : Type u_6)
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7)
  [inst_6 : CategoryTheory.Category.{v_7, u_7} E] {F₁ F₁' : CategoryTheory.Functor C₁ D₁} (τ₁ : F₁ ⟶ F₁')
  (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃),
  ((CategoryTheory.Functor.whiskeringLeft₃Map C₂ C₃ D₂ D₃ E τ₁).app F₂).app F₃ =
    ((CategoryTheory.Functor.whiskeringRight D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))
              (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))).obj
          (((CategoryTheory.Functor.whiskeringLeft₂ E).obj F₂).obj F₃)).whiskerLeft
      ((CategoryTheory.Functor.whiskeringLeft C₁ D₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))).map τ₁)
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- `PreSubmersivePresentation.differential` pushed forward to `S` via `aeval P.val`.  -/
Algebra.PreSubmersivePresentation.aevalDifferential : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] → Algebra.PreSubmersivePresentation R S ι σ → [Finite σ] → (σ → S) →ₗ[S] σ → S
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.ofLE_refl : ∀ {V : Type u_1} {G : SimpleGraph V}, SimpleGraph.Copy.ofLE G G ⋯ = SimpleGraph.Copy.id G
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The 2nd group homology of `A`, defined as the 2nd homology of the complex of inhomogeneous
chains, is isomorphic to `cycles₂ A ⧸ boundaries₂ A`, which is a simpler type.  -/
groupHomology.H2Iso : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) → groupHomology.H2 A ≅ (groupHomology.shortComplexH2 A).moduleCatLeftHomologyData.H
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
_private.Lean.Meta.Tactic.Grind.Arith.CommRing.RingId.0.Lean.Meta.Grind.Arith.CommRing.setCommSemiringId : ℕ → ℕ → Lean.Meta.Grind.GoalM Unit
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.ext_row_iff : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {A B : Matrix m n α}, A = B ↔ ∀ (i : m), A.row i = B.row i
-- Mathlib.Data.List.Lex
List.head!_le_of_lt : ∀ {α : Type u} [inst : Preorder α] [inst_1 : Inhabited α] (l l' : List α), l' < l → l' ≠ [] → l'.head! ≤ l.head!