mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.toBitVec_eq_of_parseFirstByte_eq_done : ∀ {b : UInt8},
  ByteArray.utf8DecodeChar?.parseFirstByte b = ByteArray.utf8DecodeChar?.FirstByte.done →
    b.toBitVec = 0#1 ++ BitVec.setWidth 7 b.toBitVec
-- Mathlib.Algebra.MvPolynomial.PDeriv
MvPolynomial.pderiv_X : ∀ {R : Type u} {σ : Type v} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (i j : σ),
  (MvPolynomial.pderiv i) (MvPolynomial.X j) = Pi.single i 1 j
-- Mathlib.Analysis.BoxIntegral.Box.Basic
/-- Face of a box in `ℝⁿ⁺¹ = Fin (n + 1) → ℝ`: the box in `ℝⁿ = Fin n → ℝ` with corners at
`I.lower ∘ Fin.succAbove i` and `I.upper ∘ Fin.succAbove i`.  -/
BoxIntegral.Box.face : {n : ℕ} → BoxIntegral.Box (Fin (n + 1)) → Fin (n + 1) → BoxIntegral.Box (Fin n)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instCommGroupOfMulOpposite : {M : Type u_1} → [CommGroup Mᵐᵒᵖ] → CommGroup Mᵈᵐᵃ
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.integral_eq_tsum'' : ∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α]
  [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] [inst_7 : NormedSpace ℝ E],
  MeasureTheory.IsFundamentalDomain G s μ →
    ∀ (f : α → E), MeasureTheory.Integrable f μ → ∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in s, f (g • x) ∂μ
-- Aesop.Rule.Name
Aesop.DisplayRuleName.instCoeRuleName : Coe Aesop.RuleName Aesop.DisplayRuleName
-- Mathlib.ModelTheory.Definability
Set.termDefinable_empty_withConstants_iff : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {f : (α → M) → M},
  ∅.TermDefinable (L.withConstants ↑A) f ↔ A.TermDefinable L f
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.removePosAssignment.eq_3 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.both.removePosAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg
-- Mathlib.Order.Atoms
IsCoatom.not_le_iff_codisjoint : ∀ {α : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b : α}, IsCoatom a → (¬b ≤ a ↔ Codisjoint a b)
-- Mathlib.Algebra.Symmetrized
SymAlg.sym_bijective : ∀ {α : Type u_1}, Function.Bijective ⇑SymAlg.sym
-- Init.Data.Sum.Lemmas
Sum.elim_comp_map : ∀ {α : Type u_1} {β : Type u_2} {ε : Sort u_3} {γ : Type u_4} {δ : Type u_5} {f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ}
  {g₂ : δ → ε}, Sum.elim f₂ g₂ ∘ Sum.map f₁ g₁ = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁)
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.IsLeftDerivedFunctor.mk : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_2} D] [inst_2 : CategoryTheory.Category.{v_5, u_3} H]
  {LF : CategoryTheory.Functor D H} {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  {α : L.comp LF ⟶ F} {W : CategoryTheory.MorphismProperty C} [inst_3 : L.IsLocalization W],
  LF.IsRightKanExtension α → LF.IsLeftDerivedFunctor α W
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {h_mem : k ∈ t₁ ∩ t₂}, Std.DTreeMap.Const.get (t₁ ∩ t₂) k h_mem = Std.DTreeMap.Const.get t₁ k ⋯
-- Std.Async.ContextAsync
/-- Launches a `ContextAsync` computation in the background, discarding its result. It's similar to `background`,
but the child context is not automatically cancelled when the action completes. This allows the disowned
computation to continue running independently, even if the parent context is cancelled. The child context
will remain alive as long as the computation needs it. See also `background` for launching tasks that are
cancelled when the parent finishes.
 -/
Std.Async.ContextAsync.disown : {α : Type} → Std.Async.ContextAsync α → optParam Task.Priority Task.Priority.default → Std.Async.ContextAsync Unit
-- Init.Data.Array.Lemmas
Array.mem_flatten : ∀ {α : Type u_1} {a : α} {xss : Array (Array α)}, a ∈ xss.flatten ↔ ∃ xs ∈ xss, a ∈ xs
-- Mathlib.Tactic.Ring.Compare
Mathlib.Tactic.Ring.ExceptType.tooSmall.sizeOf_spec : sizeOf Mathlib.Tactic.Ring.tooSmall = 1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.edgeSet_reverse : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.reverse.edgeSet = p.edgeSet
-- Init.Omega.Logic
Lean.Omega.Decidable.not_iff_iff_and_not_or_not_and : ∀ {a b : Prop} [Decidable a] [Decidable b], ¬(a ↔ b) ↔ a ∧ ¬b ∨ ¬a ∧ b
-- Mathlib.CategoryTheory.Abelian.LeftDerived
/-- We can compute a left derived functor on a morphism using a descent of that morphism
to a chain map between chosen projective resolutions.
 -/
CategoryTheory.Functor.leftDerived_map_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (n : ℕ) {X Y : C}
  (f : X ⟶ Y) {P : CategoryTheory.ProjectiveResolution X} {Q : CategoryTheory.ProjectiveResolution Y}
  (g : P.complex ⟶ Q.complex),
  CategoryTheory.CategoryStruct.comp g Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f) →
    (F.leftDerived n).map f =
      CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).hom
        (CategoryTheory.CategoryStruct.comp
          (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp
                (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)).map
            g)
          (Q.isoLeftDerivedObj F n).inv)
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The action map  -/
CategoryTheory.ModObj.smul : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {D : Type u₂} →
        {inst_2 : CategoryTheory.Category.{v₂, u₂} D} →
          {inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D} →
            {M : C} →
              {inst_4 : CategoryTheory.MonObj M} →
                {X : D} →
                  [self : CategoryTheory.ModObj M X] →
                    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj M X ⟶ X
-- Mathlib.Order.InitialSeg
PrincipalSeg.coe_coe_fn' : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : IsTrans β s] (f : PrincipalSeg r s),
  ⇑{ toRelEmbedding := f.toRelEmbedding, mem_range_of_rel' := ⋯ } = ⇑f.toRelEmbedding
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.ι_gluedIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [inst_1 : CategoryTheory.Category.{v, u₂} C']
  (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C')
  [inst_2 : CategoryTheory.Limits.HasMulticoequalizer D.diagram]
  [inst_3 : CategoryTheory.Limits.PreservesColimit D.diagram.multispan F]
  [inst_4 : ∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F]
  (i : D.J), CategoryTheory.CategoryStruct.comp (F.map (D.ι i)) (D.gluedIso F).hom = (D.mapGlueData F).ι i
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.instInhabitedSuggestion.default : Lean.Meta.Tactic.TryThis.Suggestion
-- Mathlib.GroupTheory.Congruence.Hom
/-- A specialization of 'the smallest additive congruence relation containing
an additive congruence relation `c` equals `c`'.  -/
AddCon.mapOfSurjective_eq_mapGen : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_4} [inst : Add M] [inst_1 : Add N] [inst_2 : FunLike F M N]
  [inst_3 : AddHomClass F M N] {c : AddCon M} {f : F} (h : AddCon.ker f ≤ c) (hf : Function.Surjective ⇑f),
  AddCon.mapGen ⇑f = AddCon.mapOfSurjective f h hf
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.edist_le_mul_of_le : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β}
  {x y : α} {r : ENNReal}, LipschitzWith K f → edist x y ≤ r → edist (f x) (f y) ≤ ↑K * r
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.erase_dup.injEq : ∀ (c c_1 : Lean.Meta.Grind.AC.DiseqCnstr),
  (Lean.Meta.Grind.AC.DiseqCnstrProof.erase_dup c = Lean.Meta.Grind.AC.DiseqCnstrProof.erase_dup c_1) = (c = c_1)
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.OpenNhdsOf.basis_nhds : ∀ {α : Type u_2} [inst : TopologicalSpace α] {x : α}, (nhds x).HasBasis (fun x => True) SetLike.coe
-- Lean.Elab.Do.Legacy
/-- "Concatenate" `c` with `doSeqToCode doElems`  -/
Lean.Elab.Term.Do.ToCodeBlock.concatWith : Lean.Elab.Term.Do.CodeBlock → List Lean.Syntax → Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock
-- Init.Prelude
/-- Make name `s₁.s₂.s₃.s₄.s₅.s₆`  -/
Lean.Name.mkStr6 : String → String → String → String → String → String → Lean.Name
-- Mathlib.Data.ZMod.Defs
ZMod.instUnique : Unique (ZMod 1)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
/-- Compose an edge-labeling, by an injection into the vertex type. This must be an injection, else
we don't know how to color `x ~ y` in the case `f x = f y`.
 -/
SimpleGraph.TopEdgeLabeling.pullback : {V : Type u_1} →
  {V' : Type u_2} → {K : Type u_3} → SimpleGraph.TopEdgeLabeling V K → (V' ↪ V) → SimpleGraph.TopEdgeLabeling V' K
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
Fin.addRothNumber_le_rothNumberNat : ∀ {n : ℕ} (k : Fin (n + 1)), addRothNumber (Finset.Iio k) ≤ rothNumberNat ↑k
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.List.HashesTo : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → List ((a : α) × β a) → ℕ → ℕ → Prop
-- Init.Data.List.Lemmas
List.singleton_inj : ∀ {α : Type u_1} {a b : α}, [a] = [b] ↔ a = b
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_eq_subst_cert.eq_1 : ∀ (x : Int.Internal.Linear.Var) (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.eq_eq_subst_cert x p₁ p₂ p₃ =
    p₃.beq' (Int.Internal.Linear.Poly.combine_mul_k (p₂.coeff_k x) (-p₁.coeff_k x) p₁ p₂)
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.val_toOrderTopSubOnePos_coe : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] {x : HahnSeries Γ R} (h : 0 < (x - 1).orderTop), ↑↑(HahnSeries.toOrderTopSubOnePos h) = x
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.ringEquivOfRingEquiv.eq_1 : ∀ {A : Type u_8} {K : Type u_9} {B : Type u_10} {L : Type u_11} [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : CommRing K] [inst_3 : CommRing L] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K]
  [inst_6 : Algebra B L] [inst_7 : IsFractionRing B L] (h : A ≃+* B),
  IsFractionRing.ringEquivOfRingEquiv h = IsLocalization.ringEquivOfRingEquiv K L h ⋯
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey_erase_eq_of_not_compare_eq_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t.erase k ≠ ∅}, ¬cmp k (t.minKey ⋯) = Ordering.eq → (t.erase k).minKey he = t.minKey ⋯
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_inter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, (m₁ ∩ m₂).getKey? k = if k ∈ m₂ then m₁.getKey? k else none
-- Init.Conv
/-- `fail_if_success t` fails if the tactic `t` succeeds.  -/
Lean.Parser.Tactic.Conv.failIfSuccess : Lean.ParserDescr
-- Mathlib.Algebra.Order.Module.Equiv
symm_toLexLinearEquiv : ∀ (α : Type u_1) (β : Type u_2) [inst : Semiring α] [inst_1 : AddCommMonoid β] [inst_2 : Module α β],
  (toLexLinearEquiv α β).symm = ofLexLinearEquiv α β
-- Mathlib.Logic.Function.Iterate
Function.Bijective.iterate : ∀ {α : Type u} {f : α → α}, Function.Bijective f → ∀ (n : ℕ), Function.Bijective f^[n]
-- Mathlib.LinearAlgebra.RootSystem.Defs
/-- A parametrized family of dual vectors, called coroots.  -/
RootPairing.coroot : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] → [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → RootPairing ι R M N → ι ↪ N
-- Mathlib.Data.PNat.Interval
PNat.uIcc_eq_finset_subtype : ∀ (a b : ℕ+), Finset.uIcc a b = Finset.subtype (fun n => 0 < n) (Finset.uIcc ↑a ↑b)
-- Mathlib.Data.List.Iterate
List.getElem_iterate : ∀ {α : Type u_1} (f : α → α) (a : α) (n i : ℕ) (h : i < (List.iterate f a n).length), (List.iterate f a n)[i] = f^[i] a
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- The restriction of the diagonal `X ⟶ X ×ₛ X` to `𝒱 i j ×[𝒰 i] 𝒱 i j` is the diagonal
`𝒱 i j ⟶ 𝒱 i j ×[𝒰 i] 𝒱 i j`.  -/
AlgebraicGeometry.Scheme.Pullback.diagonalRestrictIsoDiagonal : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    (𝒰 : Y.OpenCover) →
      (𝒱 :
          (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) →
            ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover) →
        (i : (AlgebraicGeometry.Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) →
          (j : (𝒱 i).I₀) →
            CategoryTheory.Arrow.mk
                (CategoryTheory.Limits.pullback.diagonal f ∣_
                  AlgebraicGeometry.Scheme.Hom.opensRange
                    ((AlgebraicGeometry.Scheme.Pullback.diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩)) ≅
              CategoryTheory.Arrow.mk
                (CategoryTheory.Limits.pullback.diagonal
                  (CategoryTheory.CategoryStruct.comp ((𝒱 i).f j) (CategoryTheory.Limits.pullback.snd f (𝒰.f i))))
-- Init.Grind.Config
/-- A `grind` configuration that only uses `order`.
 -/
Lean.Grind.OrderConfig : Type
-- Mathlib.Order.Bounds.Basic
IsLeast.isGLB : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α}, IsLeast s a → IsGLB s a
-- Lean.Server.Completion.CompletionUtils
_private.Lean.Server.Completion.CompletionUtils.0.Lean.String.charactersIn.goFastScalar : String → String → String.Pos.Raw → String.Pos.Raw → Bool
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- In the canonical isometric isomorphism between a Hilbert sum `E` of `G` and `lp G 2`,
a vector `w : lp G 2` is the image of the infinite sum of the associated elements in `E`, and this
sum indeed converges.  -/
IsHilbertSum.hasSum_linearIsometryEquiv_symm : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {G : ι → Type u_4} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] [inst_5 : CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E}
  (hV : IsHilbertSum 𝕜 G V) (w : ↥(lp G 2)), HasSum (fun i => (V i) (↑w i)) (hV.linearIsometryEquiv.symm w)
-- Mathlib.NumberTheory.RamificationInertia.Inertia
Ideal.inertiaDeg'_map_eq : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  {S₁ : Type u_1} [inst_3 : CommRing S₁] [inst_4 : Algebra R S₁] (P : Ideal S) {E : Type u_2}
  [inst_5 : EquivLike E S S₁] [AlgEquivClass E R S S₁] (e : E), p.inertiaDeg' (Ideal.map e P) = p.inertiaDeg' P
-- Mathlib.Algebra.Order.Group.PosPart
posPart_eq_ite : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : AddGroup α] {a : α}, a⁺ = if 0 ≤ a then a else 0
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.inl_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z) {Z_1 : C} (h : CategoryTheory.Limits.cokernel (CategoryTheory.CategoryStruct.comp f g) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.kernelCokernelCompSequence.π f g) h) =
    CategoryTheory.CategoryStruct.comp g
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (CategoryTheory.CategoryStruct.comp f g)) h)
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.SubgoalsResult.subgoals : Lean.Meta.SynthInstance.SubgoalsResult → List Lean.Expr
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.card_support_ne_one : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α), f.support.card ≠ 1
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.HaveLebesgueDecomposition.conv : ∀ {G : Type u_3} [inst : AddGroup G] {mG : MeasurableSpace G} [MeasurableAdd₂ G] [MeasurableNeg G]
  {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] [MeasureTheory.SFinite μ] {ν₁ ν₂ : MeasureTheory.Measure G}
  [ν₁.HaveLebesgueDecomposition μ] [ν₂.HaveLebesgueDecomposition μ],
  ν₁.AbsolutelyContinuous μ → ν₂.AbsolutelyContinuous μ → (ν₁.conv ν₂).HaveLebesgueDecomposition μ
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.op_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C),
  Quiver.Hom.op 0 = 0
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_sdiff_sdiff_cancel_left : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], z ≤ x → (x \ y) \ (x \ z) = z \ y
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.Hom.ext : ∀ {R : Type u} {inst : CommRing R} {A B : CommBialgCat R} {x y : A.Hom B}, x.hom' = y.hom' → x = y
-- Mathlib.Data.Num.Lemmas
PosNum.bit1_of_bit1 : ∀ (n : PosNum), n + n + 1 = n.bit1
-- Mathlib.Analysis.Complex.Basic
Complex.norm_eq_one_of_pow_eq_one : ∀ {ζ : ℂ} {n : ℕ}, ζ ^ n = 1 → n ≠ 0 → ‖ζ‖ = 1
-- Mathlib.Analysis.Complex.Basic
Complex.re_tsum : ∀ {α : Type u_1} {L : SummationFilter α} [L.NeBot] {f : α → ℂ},
  Summable f L → (∑'[L] (a : α), f a).re = ∑'[L] (a : α), (f a).re
-- Mathlib.Algebra.Ring.Defs
NonUnitalNonAssocCommRing.mk : {α : Type u} →
  [toNonUnitalNonAssocRing : NonUnitalNonAssocRing α] → (∀ (a b : α), a * b = b * a) → NonUnitalNonAssocCommRing α
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntry!.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Inhabited ((a : α) × β a)] (k : α) (size : ℕ) (k' : α)
  (v : β k') (l r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k' v l r).getEntry! k =
    match compare k k' with
    | Ordering.lt => l.getEntry! k
    | Ordering.gt => r.getEntry! k
    | Ordering.eq => ⟨k', v⟩
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.size_balanceRErase : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} (hlb : l.Balanced)
  (hrb : r.Balanced) (hlr : Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size l.size),
  (Std.DTreeMap.Internal.Impl.balanceRErase k v l r hlb hrb hlr).size = l.size + 1 + r.size
-- Lean.Data.Lsp.Workspace
Lean.Lsp.WorkspaceFolder : Type
-- Mathlib.Algebra.DirectSum.Module
/-- The inclusion of a subset of the direct summands
into a larger subset of the direct summands, as a linear map.  -/
DirectSum.lsetToSet : (R : Type u) →
  [inst : Semiring R] →
    {ι : Type v} →
      {M : ι → Type w} →
        [inst_1 : (i : ι) → AddCommMonoid (M i)] →
          [inst_2 : (i : ι) → Module R (M i)] →
            [DecidableEq ι] → (S T : Set ι) → S ⊆ T → (DirectSum ↑S fun i => M ↑i) →ₗ[R] DirectSum ↑T fun i => M ↑i
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.frequently_ae_mem_iff : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s : Set α}, (∃ᵐ (a : α) ∂μ, a ∈ s) ↔ μ s ≠ 0
-- Mathlib.Control.Monad.Writer
WriterT.run_map : ∀ {M : Type u → Type v} {α β ω : Type u} [inst : Monad M] (empty : ω) (append : ω → ω → ω) (f : α → β)
  (cmd : WriterT ω M α),
  (f <$> cmd).run =
    (fun x =>
        match x with
        | (a, w) => (f a, w)) <$>
      cmd.run
-- Mathlib.Algebra.CharZero.Infinite
CharZero.infinite : ∀ (M : Type u_1) [inst : AddMonoidWithOne M] [CharZero M], Infinite M
-- Mathlib.RingTheory.DedekindDomain.Factorization
IsDedekindDomain.HeightOneSpectrum.multiplicity_iSup : ∀ {R : Type u_3} [inst : CommRing R] [IsDedekindDomain R] (p : IsDedekindDomain.HeightOneSpectrum R) {ι : Type u_4}
  [Finite ι] [Nonempty ι] {I : ι → Ideal R},
  (∀ (i : ι), I i ≠ ⊥) → multiplicity p.asIdeal (⨆ i, I i) = ⨅ i, multiplicity p.asIdeal (I i)
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.lattice : {α : Type u_1} → [inst : HeytingAlgebra α] → Lattice (Heyting.Regular α)
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.prop_of_isLimit_binaryFan : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderBinaryProducts] {X Y : C} {B : CategoryTheory.Limits.BinaryFan X Y}
  (hB : CategoryTheory.Limits.IsLimit B), P X → P Y → P B.pt
-- Mathlib.RingTheory.MvPowerSeries.GaussNorm
MvPowerSeries.le_gaussNorm : ∀ {R : Type u_1} {σ : Type u_2} (v : R → ℝ) (c : σ → ℝ) (f : MvPowerSeries σ R) [inst : Semiring R],
  MvPowerSeries.HasGaussNorm v c f →
    ∀ (t : σ →₀ ℕ), (v ((MvPowerSeries.coeff t) f) * t.prod fun x1 x2 => c x1 ^ x2) ≤ MvPowerSeries.gaussNorm v c f
-- Mathlib.Algebra.CubicDiscriminant
Cubic.natDegree_of_a_eq_zero' : ∀ {R : Type u_1} {b c d : R} [inst : Semiring R], { a := 0, b := b, c := c, d := d }.toPoly.natDegree ≤ 2
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Inhabited α]
  [Std.TransCmp cmp] {k : α}, (t₁ ∩ t₂).getKey! k = if k ∈ t₂ then t₁.getKey! k else default
-- Mathlib.Combinatorics.Quiver.Subquiver
/-- the source vertex of an arrow  -/
Quiver.Total.left : {V : Type u} → [inst : Quiver V] → Quiver.Total V → V
-- Mathlib.Topology.Order.Basic
pi_Ici_mem_nhds' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι]
  {a' x' : ι → α}, (∀ (i : ι), a' i < x' i) → Set.Ici a' ∈ nhds x'
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
/-- If the set of all `f i j` is bounded below, then so is the set of the infimums of every row  -/
BddBelow.range_iInf_of_iUnion_range : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {κ : ι → Sort u_5} {f : (i : ι) → κ i → α},
  BddBelow (⋃ i, Set.range (f i)) → BddBelow (Set.range fun i => ⨅ j, f i j)
-- Init.Data.Order.MinMaxOn
maxOn_assoc : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x y z : α},
  maxOn f (maxOn f x y) z = maxOn f x (maxOn f y z)
-- Mathlib.Analysis.Calculus.Deriv.Abs
HasFDerivWithinAt.abs_of_neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {s : Set E}
  {x : E}, HasFDerivWithinAt f f' s x → f x < 0 → HasFDerivWithinAt (fun x => |f x|) (-f') s x
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- A morphism between coalgebras of an endofunctor `F`  -/
CategoryTheory.Endofunctor.Coalgebra.Hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} →
      CategoryTheory.Endofunctor.Coalgebra F → CategoryTheory.Endofunctor.Coalgebra F → Type v
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.res_succ : ∀ {α : Type u_2} (x : ℕ → α) (n : ℕ), PiNat.res x n.succ = x n :: PiNat.res x n
-- Init.Data.Int.DivMod.Bootstrap
Int.ediv_neg : ∀ (a b : ℤ), a / -b = -(a / b)
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.preOmega_natCast : ∀ (n : ℕ), Ordinal.preOmega ↑n = ↑n
-- Batteries.Control.Monad
/-- **Alias** of `map_inj_right_of_nonempty`. -/
LawfulFunctor.map_inj_right_of_nonempty : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Functor m] [LawfulFunctor m] [Nonempty α] {f : α → β},
  (∀ {x y : α}, f x = f y → x = y) → ∀ {x y : m α}, f <$> x = f <$> y ↔ x = y
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
isTranscendenceBasis_equiv' : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] (e : ι ≃ ι') {f : ι' → A} {g : ι → A},
  f ∘ ⇑e = g → (IsTranscendenceBasis R g ↔ IsTranscendenceBasis R f)