mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.map_apply : ∀ {K : Type u} [inst : Field K] {R : Type u_1} {F : Type u_2} [inst_1 : CommRing R] [inst_2 : IsDomain R]
  [inst_3 : FunLike F (Polynomial K) (Polynomial R)] [inst_4 : MonoidHomClass F (Polynomial K) (Polynomial R)] (φ : F)
  (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial R))) (f : RatFunc K),
  (RatFunc.map φ hφ) f =
    (algebraMap (Polynomial R) (RatFunc R)) (φ f.num) / (algebraMap (Polynomial R) (RatFunc R)) (φ f.denom)
-- Mathlib.Combinatorics.Quiver.Symmetric
/-- A quiver `HasReverse` if we can reverse an arrow `p` from `a` to `b` to get an arrow
`p.reverse` from `b` to `a`.  -/
Quiver.HasReverse : (V : Type u_2) → [Quiver V] → Type (max u_2 v)
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
PartialDiffeomorph.toOpenPartialHomeomorph_toPartialHomeomorph_toPartialEquiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} (Φ : PartialDiffeomorph I J M N n),
  Φ.toOpenPartialHomeomorph.toPartialEquiv = Φ.toPartialEquiv
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoLocallyUniformly.div` -/
TendstoLocallyUniformly.fun_div : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {l : Filter ι},
  TendstoLocallyUniformly F f l →
    TendstoLocallyUniformly G g l → TendstoLocallyUniformly (fun i i_1 => F i i_1 / G i i_1) (fun i => f i / g i) l
-- Mathlib.MeasureTheory.Order.UpperLower
IsAntichain.volume_eq_zero : ∀ {ι : Type u_1} [inst : Fintype ι] {s : Set (ι → ℝ)} [Nonempty ι],
  IsAntichain (fun x1 x2 => x1 ≤ x2) s → MeasureTheory.volume s = 0
-- Std.Http.Protocol.H1
/-- Set a known size for the message body, replacing any previous value.
 -/
Std.Http.Protocol.H1.Machine.setKnownSize : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Std.Http.Body.Length → Std.Http.Protocol.H1.Machine dir
-- Init.Data.List.Sublist
List.sublist_append_iff : ∀ {α : Type u_1} {r₁ r₂ l : List α}, l.Sublist (r₁ ++ r₂) ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.Sublist r₁ ∧ l₂.Sublist r₂
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_erase_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k fallback : α}, (m.erase k).getD k fallback = fallback
-- Lean.MetavarContext
Lean.DependsOn.State : Type
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {F G : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (η : F ⟶ G) {a : B} {a' : CategoryTheory.Cat} (f : G.obj a ⟶ a') (X : ↑(F.obj a)),
  CategoryTheory.CategoryStruct.comp
      (f.toFunctor.map ((η.naturality (CategoryTheory.CategoryStruct.id a)).hom.toNatTrans.app X))
      (f.toFunctor.map ((G.mapId a).hom.toNatTrans.app ((η.app a).toFunctor.obj X))) =
    CategoryTheory.CategoryStruct.comp (f.toFunctor.map ((η.app a).toFunctor.map ((F.mapId a).hom.toNatTrans.app X)))
      (CategoryTheory.CategoryStruct.comp
        (f.toFunctor.map
          (CategoryTheory.CategoryStruct.id
            ((η.app a).toFunctor.obj ((CategoryTheory.CategoryStruct.id (F.obj a)).toFunctor.obj X))))
        (f.toFunctor.map (CategoryTheory.CategoryStruct.id ((η.app a).toFunctor.obj X))))
-- Mathlib.MeasureTheory.Integral.Layercake
/-- The standard case of the layer cake formula / Cavalieri's principle / tail probability formula:

For a nonnegative function `f` on a measure space, the Lebesgue integral of `f` can
be written (roughly speaking) as: `∫⁻ f ∂μ = ∫⁻ t in 0..∞, μ {ω | f(ω) > t}`.

See `lintegral_eq_lintegral_meas_le` for a version with sets of the form `{ω | f(ω) ≥ t}`
instead.  -/
MeasureTheory.lintegral_eq_lintegral_meas_lt : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℝ} (μ : MeasureTheory.Measure α),
  0 ≤ᵐ[μ] f → AEMeasurable f μ → ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t < f a}
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.differentiableWithinAt_aeval : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {R : Type u_1} [inst_1 : CommSemiring R]
  [inst_2 : Algebra R 𝕜] (q : Polynomial R), DifferentiableWithinAt 𝕜 (fun x => (Polynomial.aeval x) q) s x
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.coe_reindexLinearEquiv : ∀ {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} (R : Type u_11) (A : Type u_12) [inst : Semiring R]
  [inst_1 : AddCommMonoid A] [inst_2 : Module R A] (eₘ : m ≃ m') (eₙ : n ≃ n'),
  ⇑(Matrix.reindexLinearEquiv R A eₘ eₙ) = ⇑(Matrix.reindex eₘ eₙ)
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.coePolynomial.congr_simp : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (P P_1 : Polynomial K), P = P_1 → ↑P = ↑P_1
-- Mathlib.Topology.Order.Basic
pi_Ico_mem_nhds : ∀ {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [inst : (i : ι) → LinearOrder (X i)]
  [inst_1 : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a b x : (i : ι) → X i} [Nonempty ι],
  (∀ (i : ι), x i < a i) → (∀ (i : ι), b i < x i) → Set.Ico b a ∈ nhds x
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithUpperSet.instPreorder : {α : Type u_1} → [Preorder α] → Preorder (Topology.WithUpperSet α)
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.CofanMapObjFun.mk.eq_1 : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  (X : CategoryTheory.GradedObject I C) (p : I → J) (j : J) (pt : C) (ι' : (i : I) → p i = j → (X i ⟶ pt)),
  CategoryTheory.GradedObject.CofanMapObjFun.mk X p j pt ι' =
    CategoryTheory.Limits.Cofan.mk pt fun x =>
      match x with
      | ⟨i, hi⟩ => ι' i hi
-- Mathlib.RingTheory.Valuation.Basic
Valuation.le_one_of_subsingleton : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] [Subsingleton R]
  (v : Valuation R Γ₀) {x : R}, v x ≤ 1
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.lowerCentralSeriesLast_le_max_triv : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  LieModule.lowerCentralSeriesLast R L M ≤ LieModule.maxTrivSubmodule R L M
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.continuousAt_log : ∀ {x : ℝ}, x ≠ 0 → ContinuousAt Real.log x
-- Mathlib.NumberTheory.Divisors
Nat.right_ne_zero_of_mem_divisorsAntidiagonal : ∀ {n : ℕ} {p : ℕ × ℕ}, p ∈ n.divisorsAntidiagonal → p.2 ≠ 0
-- Mathlib.Order.BooleanAlgebra.Basic
sup_lt_of_lt_sdiff_right : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], x < z \ y → y ≤ z → x ⊔ y < z
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
SSet.Truncated.HomotopyCategory₂.mk : {A : SSet.Truncated 2} →
  A.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 }) → A.HomotopyCategory₂
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.comp_assoc : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {V₃ : Type u_6} {V₄ : Type u_7} {P : Type u_10} {P₂ : Type u_11}
  {P₃ : Type u_12} {P₄ : Type u_13} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P]
  [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂] [inst_7 : PseudoMetricSpace P₂]
  [inst_8 : NormedAddTorsor V₂ P₂] [inst_9 : SeminormedAddCommGroup V₃] [inst_10 : NormedSpace 𝕜 V₃]
  [inst_11 : PseudoMetricSpace P₃] [inst_12 : NormedAddTorsor V₃ P₃] [inst_13 : SeminormedAddCommGroup V₄]
  [inst_14 : NormedSpace 𝕜 V₄] [inst_15 : PseudoMetricSpace P₄] [inst_16 : NormedAddTorsor V₄ P₄] (f : P₃ →ᵃⁱ[𝕜] P₄)
  (g : P₂ →ᵃⁱ[𝕜] P₃) (h : P →ᵃⁱ[𝕜] P₂), (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.Topology.Neighborhoods
/-- To show a filter is above the neighborhood filter at `x`, it suffices to show that it is above
the principal filter of some open set `s` containing `x`.  -/
nhds_le_of_le : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X} {f : Filter X},
  x ∈ s → IsOpen s → Filter.principal s ≤ f → nhds x ≤ f
-- Mathlib.NumberTheory.Harmonic.Bounds
log_add_one_le_harmonic : ∀ (n : ℕ), Real.log ↑(n + 1) ≤ ↑(harmonic n)
-- Std.Data.DTreeMap.Internal.Ordered
Std.DTreeMap.Internal.Impl.Ordered.compare_right : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {sz : ℕ} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  (Std.DTreeMap.Internal.Impl.inner sz k v l r).Ordered →
    ∀ {k' : (a : α) × β a}, k' ∈ r.toListModel → compare k k'.fst = Ordering.lt
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.alphaEqv : Lean.IR.IndexRenaming → Lean.IR.FnBody → Lean.IR.FnBody → Bool
-- Lean.DocString.Parser
Lean.Doc.Parser.instBEqOrderedListType.beq : Lean.Doc.Parser.OrderedListType → Lean.Doc.Parser.OrderedListType → Bool
-- Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
/-- For a convex continuous function `f` on `[0, ∞)`, if `μ` is absolutely continuous
with respect to a probability measure `ν`, then
`f μ.real univ ≤ ∫ x, f (μ.rnDeriv ν x).toReal ∂ν`.  -/
MeasureTheory.le_integral_rnDeriv_of_ac : ∀ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsProbabilityMeasure ν],
  ConvexOn ℝ (Set.Ici 0) f →
    ContinuousWithinAt f (Set.Ici 0) 0 →
      MeasureTheory.Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν →
        μ.AbsolutelyContinuous ν → f (μ.real Set.univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
-- Mathlib.Topology.NhdsWithin
eventually_nhdsWithin_of_forall : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {a : α} {p : α → Prop},
  (∀ x ∈ s, p x) → ∀ᶠ (x : α) in nhdsWithin a s, p x
-- Mathlib.Tactic.ClickSuggestions.Util
/-- The token for updating the main HTML body of suggestions.
This is used for displaying a message that no progress has happened.  -/
Mathlib.Tactic.ClickSuggestions.Context.masterToken : Mathlib.Tactic.ClickSuggestions.Context → ProofWidgets.RefreshToken
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.functor_obj : ∀ (α : Type w₂) {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasCoproductsOfShape α C] (f : α → C),
  (CategoryTheory.Limits.Sigma.functor α).obj f = ∐ f
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- The infimum of two graphs `x ⊓ y` has edges where both `x` and `y` have edges.  -/
SimpleGraph.instMin : {V : Type u} → Min (SimpleGraph V)
-- Mathlib.GroupTheory.Congruence.Defs
/-- The map sending an additive congruence relation to its underlying binary relation
is injective.  -/
AddCon.ext' : ∀ {M : Type u_1} [inst : Add M] {c d : AddCon M}, ⇑c = ⇑d → c = d
-- Lean.Meta.DiscrTree.Main
/-- Get all results under key `k`.
 -/
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.getAllValuesForKey : {α : Type} → Lean.Meta.DiscrTree α → Lean.Meta.DiscrTree.Key → Array α → Array α
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.not_vgt_of_veq : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y : R}, x =ᵥ y → ¬y <ᵥ x
-- Mathlib.NumberTheory.FLT.Polynomial
_private.Mathlib.NumberTheory.FLT.Polynomial.0.rot_coprime : ∀ {k : Type u_1} [inst : Field k] {p q r : ℕ} {a b c : Polynomial k} {u v w : k} {hp : p ≠ 0} {hq : q ≠ 0} {hr : r ≠ 0}
  {hu : u ≠ 0} {hv : v ≠ 0} {hw : w ≠ 0},
  Polynomial.C u * a ^ p + Polynomial.C v * b ^ q + Polynomial.C w * c ^ r = 0 → IsCoprime a b → IsCoprime b c
-- Mathlib.Analysis.Normed.Group.Defs
/-- An enormed monoid is a monoid endowed with a continuous enorm,
which is positive definite: in other words, this is an `ESeminormedMonoid` with a positive
definiteness condition added.  -/
ENormedMonoid : (E : Type u_8) → [TopologicalSpace E] → Type u_8
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
/-- `coeff x` is the additive group homomorphism `FreeAbelianGroup X →+ ℤ`
that sends `a` to the multiplicity of `x : X` in `a`.  -/
FreeAbelianGroup.coeff : {X : Type u_1} → X → FreeAbelianGroup X →+ ℤ
-- Mathlib.Analysis.InnerProductSpace.NormDet
ContinuousLinearMap.det.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (A : M →L[R] M), A.det = LinearMap.det ↑A
-- Init.Data.BitVec.Lemmas
BitVec.sshiftRight_and_distrib : ∀ {w : ℕ} (x y : BitVec w) (n : ℕ), (x &&& y).sshiftRight n = x.sshiftRight n &&& y.sshiftRight n
-- Mathlib.Topology.Order.NhdsSet
Icc_mem_nhdsSet_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c d : α},
  a ≤ b → c < d → Set.Icc a d ∈ nhdsSet (Set.Ioc b c)
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.zero_mul : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop}
  (x : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation.below ⋯
-- Lean.Elab.Tactic.ElabTerm
Lean.Elab.Tactic.sortMVarIdsByIndex : {m : Type → Type} → [Lean.MonadMCtx m] → [Monad m] → Array Lean.MVarId → m (Array Lean.MVarId)
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.isCofiltered_op_of_isFiltered : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C], CategoryTheory.IsCofiltered Cᵒᵖ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getEntryLT!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited ((a : α) × β a)] {k : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryLT! k = t₂.getEntryLT! k
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.braiding_tensor_right_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (β_ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).inv h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (β_ X Z).inv)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Y).inv Z)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom h))))
-- Mathlib.Algebra.GroupWithZero.Subgroup
AddSubgroup.pointwise_smul_le_pointwise_smul_iff : ∀ {G : Type u_2} {A : Type u_4} [inst : Group G] [inst_1 : AddGroup A] [inst_2 : DistribMulAction G A]
  {S T : AddSubgroup A} {a : G}, a • S ≤ a • T ↔ S ≤ T
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabSigmaCore : Bool → Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.MeasureTheory.Measure.Map
AEMeasurable.of_map_ne_zero : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β}
  {μ : MeasureTheory.Measure α}, MeasureTheory.Measure.map f μ ≠ 0 → AEMeasurable f μ
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_zero : ∀ (α : Type u_1) (M : Type u_2) (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Finsupp.linearCombination R 0 = 0
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getKey!.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Inhabited α] (a : α) (x : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.getKey! a x =
    match x with
    | Std.DHashMap.Internal.AssocList.nil =>
      panicWithPosWithDecl "Std.Data.DHashMap.Internal.AssocList.Basic" "Std.DHashMap.Internal.AssocList.getKey!" 168 11
        "key is not present in hash table"
    | Std.DHashMap.Internal.AssocList.cons k value es =>
      if (k == a) = true then k else Std.DHashMap.Internal.AssocList.getKey! a es
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.isGE_of_isZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X : C}, CategoryTheory.Limits.IsZero X → ∀ (n : ℤ), t.IsGE X n
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_nonpos_of_nonpos_of_neg : ∀ {n s : ℤ}, n ≤ 0 → 0 < s → n / s ≤ 0
-- Mathlib.Control.ULiftable
/-- The most common practical use `ULiftable` (together with `down`), the function `up.{v}` takes
`x : M.{u} α` and lifts it to `M.{max u v} (ULift.{v} α)`  -/
ULiftable.up : {f : Type u₀ → Type u₁} → {g : Type (max u₀ v) → Type v₁} → [ULiftable f g] → {α : Type u₀} → f α → g (ULift.{v, u₀} α)
-- Std.Http.Protocol.H1
/-- Transitions the reader into `.failed`, records an error, and emits a `.failed`
event in one operation.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.setFailure : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Error → Std.Http.Protocol.H1.Machine dir
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
/-- The empty list as a `Products`  -/
Profinite.NobelingProof.Products.nil : {I : Type u} → [inst : LinearOrder I] → Profinite.NobelingProof.Products I
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasFDerivAtFilter_fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {L : Filter ((E × F) × E × F)}, HasFDerivAtFilter Prod.fst (ContinuousLinearMap.fst 𝕜 E F) L
-- Mathlib.Logic.Small.Basic
small_set : ∀ {α : Type u_1} [Small.{w, u_1} α], Small.{w, u_1} (Set α)
-- Mathlib.Topology.Constructions.SumProd
Topology.IsClosedEmbedding.sumElim : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Z} {g : Y → Z},
  Topology.IsClosedEmbedding f →
    Topology.IsClosedEmbedding g → Function.Injective (Sum.elim f g) → Topology.IsClosedEmbedding (Sum.elim f g)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isClosed_zeroLocus : ∀ {R : Type u} [inst : CommSemiring R] (s : Set R), IsClosed (PrimeSpectrum.zeroLocus s)
-- Mathlib.CategoryTheory.Triangulated.Generators
CategoryTheory.ObjectProperty.triangEnvelope_le_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) {Q : CategoryTheory.ObjectProperty C} [Q.IsStableUnderRetracts]
  [Q.IsTriangulated], P.triangEnvelope ≤ Q ↔ P ≤ Q
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.conj_eqToHom_iff_heq' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y)
  (h' : Z = X),
  f =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h)
        (CategoryTheory.CategoryStruct.comp g (CategoryTheory.eqToHom h')) ↔
    f ≍ g
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Map a Schwartz function to an `Lp` function for any `p`.  -/
SchwartzMap.toLp : {E : Type u_5} →
  {F : Type u_6} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℝ F] →
            [inst_4 : MeasurableSpace E] →
              [OpensMeasurableSpace E] →
                [SecondCountableTopologyEither E F] →
                  SchwartzMap E F →
                    (p : ENNReal) →
                      (μ : autoParam (MeasureTheory.Measure E) SchwartzMap.toLp._auto_1) →
                        [hμ : μ.HasTemperateGrowth] → ↥(MeasureTheory.Lp F p μ)
-- Mathlib.Algebra.Module.Submodule.LinearMap
LinearMap.coe_domRestrict : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M), ⇑(f.domRestrict p) = (↑p).domRestrict ⇑f
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_neg : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (T : Set α → E →L[ℝ] F),
  MeasureTheory.FinMeasAdditive μ T →
    ∀ {f : MeasureTheory.SimpleFunc α E},
      MeasureTheory.Integrable (⇑f) μ →
        MeasureTheory.SimpleFunc.setToSimpleFunc T (-f) = -MeasureTheory.SimpleFunc.setToSimpleFunc T f
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsStronglyProgressive.div' : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u v : ι → Ω → β} [inst_2 : MeasurableSpace ι] [inst_3 : Group β]
  [ContinuousDiv β],
  MeasureTheory.IsStronglyProgressive f u →
    MeasureTheory.IsStronglyProgressive f v → MeasureTheory.IsStronglyProgressive f fun i ω => u i ω / v i ω
-- Mathlib.Order.Hom.Basic
OrderIso.trans_refl : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β), e.trans (OrderIso.refl β) = e
-- Mathlib.Analysis.RCLike.Basic
RCLike.map_apply : ∀ (𝕜 : Type u_3) (𝕜' : Type u_4) [inst : RCLike 𝕜] [inst_1 : RCLike 𝕜'] (x : 𝕜),
  (RCLike.map 𝕜 𝕜') x = ↑(RCLike.re x) + ↑(RCLike.im x) * RCLike.I
-- Init.Data.Rat.Lemmas
Rat.mkRat_mul_left : ∀ {n : ℤ} {d a : ℕ}, a ≠ 0 → mkRat (↑a * n) (a * d) = mkRat n d
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instNegZeroClassOfAddOpposite : {M : Type u_1} → [NegZeroClass Mᵃᵒᵖ] → NegZeroClass Mᵈᵃᵃ
-- Lean.Message
/-- Eagerly formatted text with info annotations.
This constructor is inspected in various hacks.  -/
Lean.MessageData.ofFormatWithInfos : Lean.FormatWithInfos → Lean.MessageData
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.not_isHamiltonian_bot_of_card_ne_one : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α], Fintype.card α ≠ 1 → ¬⊥.IsHamiltonian
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.opcyclesIsoSc'.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology],
  K.opcyclesIsoSc' i j k hi hk = K.opcyclesIsoSc' i j k hi hk