mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.functor_map_id : ∀ {J : Type v₁} {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C]
  (F : CategoryTheory.Functor (CategoryTheory.Discrete J) C) {j : CategoryTheory.Discrete J} (f : j ⟶ j),
  F.map f = CategoryTheory.CategoryStruct.id (F.obj j)
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey_le : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {he : l.isEmpty = false},
      (compare (Std.Internal.List.maxKey l he) k).isLE = true ↔
        ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k' k).isLE = true
-- Init.Prelude
String.ofByteArray : (toByteArray : ByteArray) → toByteArray.IsValidUTF8 → String
-- Mathlib.Topology.MetricSpace.Gluing
Metric.inhabitedRight : {X : Type u} →
  {Y : Type v} →
    {Z : Type w} →
      [inst : Nonempty Z] →
        [inst_1 : MetricSpace Z] →
          [inst_2 : MetricSpace X] →
            [inst_3 : MetricSpace Y] →
              {Φ : Z → X} →
                {Ψ : Z → Y} → (hΦ : Isometry Φ) → (hΨ : Isometry Ψ) → [Inhabited Y] → Inhabited (Metric.GlueSpace hΦ hΨ)
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.mk₁_homEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {x y : CategoryTheory.ComposableArrows C 0}
  (e : SSet.Edge x y),
  CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.nerve.homEquiv e) =
    CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.ComposableArrows.hom e.edge)
-- Mathlib.Order.Category.HeytAlg
HeytAlg.hom_comp : ∀ {X Y Z : HeytAlg} (f : X ⟶ Y) (g : Y ⟶ Z),
  HeytAlg.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (HeytAlg.Hom.hom g).comp (HeytAlg.Hom.hom f)
-- Mathlib.Algebra.Group.Action.Defs
/-- `+ᵥ` is left commutative  -/
VAddCommClass.vadd_comm : ∀ {M : Type u_9} {N : Type u_10} {α : Type u_11} {inst : VAdd M α} {inst_1 : VAdd N α} [self : VAddCommClass M N α]
  (m : M) (n : N) (a : α), m +ᵥ n +ᵥ a = n +ᵥ m +ᵥ a
-- Mathlib.CategoryTheory.EpiMono
/-- The opposite of a split epi is a split mono.  -/
CategoryTheory.SplitEpi.op : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → {f : X ⟶ Y} → CategoryTheory.SplitEpi f → CategoryTheory.SplitMono f.op
-- Init.Data.UInt.Lemmas
UInt16.toUInt32_ofNatLT : ∀ {n : ℕ} (h : n < UInt16.size), (UInt16.ofNatLT n h).toUInt32 = UInt32.ofNatLT n ⋯
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
norm_cfcₙ_lt_iff : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) (c : ℝ),
  autoParam (ContinuousOn f (quasispectrum 𝕜 a)) norm_cfcₙ_lt_iff._auto_1 →
    autoParam (f 0 = 0) norm_cfcₙ_lt_iff._auto_3 →
      autoParam (p a) norm_cfcₙ_lt_iff._auto_5 → (‖cfcₙ f a‖ < c ↔ ∀ x ∈ quasispectrum 𝕜 a, ‖f x‖ < c)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.isTrivialOn_iff : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀} {A : Type u_7}
  [inst_3 : CommSemiring A] [inst_4 : Algebra A R],
  v₁.IsEquiv v₂ → (Valuation.IsTrivialOn A v₁ ↔ Valuation.IsTrivialOn A v₂)
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.sc₂_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ : ℤ),
  (X.sc₂ f g fg h n₀).f = (X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonHover : Lean.FromJson Lean.Lsp.Hover
-- Lean.InternalExceptionId
Lean.InternalExceptionId.mk.sizeOf_spec : ∀ (idx : ℕ), sizeOf { idx := idx } = 1 + sizeOf idx
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.WideSubcategory.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {_P : CategoryTheory.MorphismProperty C}
  {inst_1 : _P.IsMultiplicative} {obj obj_1 : C}, { obj := obj } = { obj := obj_1 } → obj = obj_1
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.hom_inv_apply : ∀ {X Y : CommGrpCat} (e : X ≅ Y) (s : ↑Y),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Mathlib.Analysis.Calculus.FDeriv.Prod
differentiableOn_snd : ∀ {𝕜 : 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]
  {s : Set (E × F)}, DifferentiableOn 𝕜 Prod.snd s
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthSup_add_le : ∀ {u v : ℕ → EReal},
  LinearGrowth.linearGrowthSup u ≠ ⊥ ∨ LinearGrowth.linearGrowthSup v ≠ ⊤ →
    LinearGrowth.linearGrowthSup u ≠ ⊤ ∨ LinearGrowth.linearGrowthSup v ≠ ⊥ →
      LinearGrowth.linearGrowthSup (u + v) ≤ LinearGrowth.linearGrowthSup u + LinearGrowth.linearGrowthSup v
-- Mathlib.GroupTheory.Congruence.Basic
Con.quotientKerEquivOfSurjective.eq_1 : ∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] (f : M →* P)
  (hf : Function.Surjective ⇑f),
  Con.quotientKerEquivOfSurjective f hf = Con.quotientKerEquivOfRightInverse f (Exists.choose ⋯) ⋯
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.L1.aemeasurable_coeFn : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  [inst_1 : MeasurableSpace β] [BorelSpace β] (f : ↥(MeasureTheory.Lp β 1 μ)), AEMeasurable (↑↑f) μ
-- Mathlib.Topology.Algebra.ConstMulAction
isHomeomorph_smul₀ : ∀ {α : Type u_2} {G₀ : Type u_4} [inst : TopologicalSpace α] [inst_1 : GroupWithZero G₀] [inst_2 : MulAction G₀ α]
  [ContinuousConstSMul G₀ α] {c : G₀}, c ≠ 0 → IsHomeomorph fun x => c • x
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Path.cons_isCycle : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Path v u) (h : G.Adj u v),
  s(u, v) ∉ (↑p).edges → (SimpleGraph.Walk.cons h ↑p).IsCycle
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblX_of_Z_eq_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P : Fin 3 → R},
  W'.Equation P → P 2 = 0 → W'.dblX P = 0
-- Init.Omega.Constraint
Lean.Omega.instReprConstraint : Repr Lean.Omega.Constraint
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Subspace.IsMono.eq_1 : ∀ {η : Type u_5} {α : Type u_6} {ι : Type u_7} {κ : Type u_8} (C : (ι → α) → κ) (l : Combinatorics.Subspace η α ι),
  Combinatorics.Subspace.IsMono C l = ∃ c, ∀ (x : η → α), C (↑l x) = c
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.instFirstCountableTopology : ∀ {M : Type u_1} [inst : TopologicalSpace M] [FirstCountableTopology M], FirstCountableTopology Mᵈᵐᵃ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.foldr_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} {δ : Type w} [Std.TransCmp cmp]
  {f : (a : α) → β a → δ → δ} {init : δ}, t₁.Equiv t₂ → Std.DTreeMap.foldr f init t₁ = Std.DTreeMap.foldr f init t₂
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.instInhabitedCommSemiring.default : Lean.Meta.Sym.Arith.CommSemiring
-- Mathlib.Topology.UnitInterval
Set.Icc.convexComb_assoc : ∀ {a b : ℝ} (x y z : ↑(Set.Icc a b)) (s t : ↑unitInterval),
  Set.Icc.convexComb x (Set.Icc.convexComb y z t) s =
    Set.Icc.convexComb (Set.Icc.convexComb x y (Set.Icc.convexComb_assoc_coeff₁ s t)) z
      (Set.Icc.convexComb_assoc_coeff₂ s t)
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lt_lift_iff : ∀ {a : Cardinal.{u}} {b : Cardinal.{max u v}}, b < Cardinal.lift.{v, u} a ↔ ∃ a' < a, Cardinal.lift.{v, u} a' = b
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_natCast_mul_add : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ), toIcoMod hp a (↑m * p + b) = toIcoMod hp a b
-- Mathlib.Analysis.Calculus.TangentCone.Basic
UniqueDiffWithinAt.closure : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Semiring 𝕜] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {s : Set E} {x : E}, UniqueDiffWithinAt 𝕜 s x → UniqueDiffWithinAt 𝕜 (closure s) x
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.comp_r : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {X Y Z : CategoryTheory.Bicategory.Adj B}
  (f : CategoryTheory.Bicategory.Adj.Hom X.obj Y.obj) (g : CategoryTheory.Bicategory.Adj.Hom Y.obj Z.obj),
  (CategoryTheory.CategoryStruct.comp f g).r = CategoryTheory.CategoryStruct.comp g.r f.r
-- Lean.Parser.Term.Basic
Lean.Parser.tacticParser : optParam ℕ 0 → Lean.Parser.Parser
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (A : Rep.{u, u, u} k G) (g : G)
  (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (hi : Odd i) (x : ↥(Rep.Hom.hom A.norm).ker),
  (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupCohomologyπOdd A g hg i hi)) x = 0 ↔
    ↑x ∈ (Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).range
-- Mathlib.Order.Ideal
/-- A proper ideal is one that is not the whole set.
Note that the whole set might not be an ideal.  -/
Order.Ideal.IsProper : {P : Type u_1} → [inst : LE P] → Order.Ideal P → Prop
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.Respects.toRespectsRight : ∀ {C : Type u} {inst : CategoryTheory.CategoryStruct.{v, u} C} {P Q : CategoryTheory.MorphismProperty C}
  [self : P.Respects Q], P.RespectsRight Q
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.map_updateCol : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {M : Matrix m n α} {j : n} {c : m → α} [inst : DecidableEq n]
  (f : α → β), (M.updateCol j c).map f = (M.map f).updateCol j (f ∘ c)
-- Mathlib.Data.Finsupp.ToDFinsupp
sigmaFinsuppLequivDFinsupp_symm_apply : ∀ {ι : Type u_1} (R : Type u_2) {η : ι → Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid N]
  [inst_2 : Module R N] (a : Π₀ (i : ι), η i →₀ N),
  (sigmaFinsuppLequivDFinsupp R).symm a = sigmaFinsuppAddEquivDFinsupp.invFun a
-- Mathlib.SetTheory.Cardinal.NatCount
Nat.count_le_setNCard : ∀ {p : ℕ → Prop} [inst : DecidablePred p] (n : ℕ), {k | p k}.Finite → Nat.count p n ≤ {k | p k}.ncard
-- Init.Data.UInt.Lemmas
UInt16.ofNatTruncate_eq_ofNat : ∀ n < UInt16.size, UInt16.ofNatClamp n = UInt16.ofNat n
-- Mathlib.Data.Num.Bitwise
SNum.instMul : Mul SNum
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.iter : String.Slice → (s : String.Slice) → Std.Iter (String.Slice.Pattern.SearchStep s)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.monomial_zero_left : ∀ {R : Type u_1} [inst : Semiring R] ⦃a : R⦄, (SkewPolynomial.monomial 0) a = SkewPolynomial.C a
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_insertList_of_contains_eq_false_right : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} {fallback : β},
  Std.Internal.List.containsKey k toInsert = false →
    Std.Internal.List.getValueD k (Std.Internal.List.insertList l toInsert) fallback =
      Std.Internal.List.getValueD k l fallback
-- Mathlib.Logic.Equiv.Set
Equiv.preimage_piEquivPiSubtypeProd_symm_pi : ∀ {α : Type u_3} {β : α → Type u_4} (p : α → Prop) [inst : DecidablePred p] (s : (i : α) → Set (β i)),
  ⇑(Equiv.piEquivPiSubtypeProd p β).symm ⁻¹' Set.univ.pi s = (Set.univ.pi fun i => s ↑i) ×ˢ Set.univ.pi fun i => s ↑i
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_insert_le_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k : α} {v : β k},
  (compare (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.minKey! k).isLE = true
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int16.reduceGT : Lean.Meta.Simp.Simproc
-- Mathlib.Data.List.InsertIdx
List.insertIdx_injective : ∀ {α : Type u} (n : ℕ) (x : α), Function.Injective fun l => l.insertIdx n x
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigOWith_iff_exists_eq_mul : ∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {c : ℝ} {l : Filter α} {u v : α → 𝕜},
  0 ≤ c → (Asymptotics.IsBigOWith c l u v ↔ ∃ φ, (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v)
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData'.t_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData' C) (i j : self.J)
  (hij : i ≠ j),
  CategoryTheory.CategoryStruct.comp (self.t i j hij) (self.t j i ⋯) = CategoryTheory.CategoryStruct.id (self.V i j hij)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_closedBall : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → MetricSpace (α i)] (x : (i : ι) → α i) {r : ℝ},
  0 ≤ r → (MeasureTheory.Measure.pi μ) (Metric.closedBall x r) = ∏ i, (μ i) (Metric.closedBall (x i) r)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- A preorder on a ring is said to be "valuative" if it agrees with the
valuative relation.  -/
ValuativePreorder : (R : Type u_1) → [inst : Semiring R] → [ValuativeRel R] → [Preorder R] → Prop
-- Lean.Parser.Types
Lean.Parser.CacheableParserContext.savedPos? : Lean.Parser.CacheableParserContext → Option String.Pos.Raw
-- Mathlib.RingTheory.Kaehler.JacobiZariski
_private.Mathlib.RingTheory.Kaehler.JacobiZariski.0.Algebra.Generators.H1Cotangent.auxMemKer : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ)
  (z : TensorProduct S T P.toExtension.H1Cotangent),
  (LinearMap.liftBaseChange T (Algebra.Extension.Cotangent.map (Q.toComp P).toExtensionHom))
      ((LinearMap.lTensor T Algebra.Extension.h1Cotangentι) z) ∈
    (Q.comp P).toExtension.cotangentComplex.ker
-- Init.Core
Lean.Name.str.injEq : ∀ (pre : Lean.Name) (str : String) (pre_1 : Lean.Name) (str_1 : String),
  (pre.str str = pre_1.str str_1) = (pre = pre_1 ∧ str = str_1)
-- Mathlib.Algebra.Group.Pi.Basic
Function.extend_zero : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero γ] (f : α → β), Function.extend f 0 0 = 0
-- Mathlib.Topology.Compactness.Compact
Set.Infinite.exists_accPt_of_subset_isCompact : ∀ {X : Type u} [inst : TopologicalSpace X] {s K : Set X},
  s.Infinite → IsCompact K → s ⊆ K → ∃ x ∈ K, AccPt x (Filter.principal s)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.sup : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_8} [inst : NormedAddCommGroup β]
  [inst_1 : Lattice β] [HasSolidNorm β] [IsOrderedAddMonoid β] {f g : α → β},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → MeasureTheory.Integrable (f ⊔ g) μ
-- Mathlib.MeasureTheory.Constructions.Cylinders
/-- The measurable cylinders generate the product σ-algebra.  -/
MeasureTheory.generateFrom_measurableCylinders : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)],
  MeasurableSpace.generateFrom (MeasureTheory.measurableCylinders α) = MeasurableSpace.pi
-- Mathlib.Data.ENNReal.Inv
ENNReal.mul_le_of_forall_lt : ∀ {a b c : ENNReal}, (∀ a' < a, ∀ b' < b, a' * b' ≤ c) → a * b ≤ c
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false)
  {h : k ∈ Std.ExtDHashMap.Const.insertMany m l},
  Std.ExtDHashMap.Const.get (Std.ExtDHashMap.Const.insertMany m l) k h = Std.ExtDHashMap.Const.get m k ⋯
-- Mathlib.Algebra.Opposites
MulOpposite.op_surjective : ∀ {α : Type u_1}, Function.Surjective MulOpposite.op
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.toList_sum : ∀ {α : Type u_1} (xs : List (FreeAddMonoid α)),
  FreeAddMonoid.toList xs.sum = (List.map (⇑FreeAddMonoid.toList) xs).flatten
-- Mathlib.Analysis.Convex.Basic
Convex.add_half_self_eq_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s : Set E}, Convex 𝕜 s → 2⁻¹ • s + 2⁻¹ • s = s
-- Mathlib.Algebra.GroupWithZero.Action.Prod
Prod.smul_mk_zero : ∀ {M : Type u_1} {α : Type u_3} [inst : SMul M α] {β : Type u_5} [inst_1 : Monoid M] [inst_2 : AddMonoid β]
  [inst_3 : DistribMulAction M β] (a : M) (b : α), a • (b, 0) = (a • b, 0)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_single : ∀ {α : Type u_1} {M : Type u_8} [inst : AddCommMonoid M] (f : α →₀ M), f.sum Finsupp.single = f
-- Mathlib.Combinatorics.Colex
Finset.Colex.cons_lt_cons : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Finset α} {a b : α} (ha : a ∉ s) (hb : b ∉ s),
  toColex (Finset.cons a s ha) < toColex (Finset.cons b s hb) ↔ a < b
-- Mathlib.Algebra.Group.Commute.Basic
Commute.self_zpow : ∀ {G : Type u_1} [inst : Group G] (a : G) (n : ℤ), Commute a (a ^ n)
-- Mathlib.LinearAlgebra.AffineSpace.Slope
eq_of_slope_eq_zero : ∀ {k : Type u_1} {E : Type u_2} {PE : Type u_3} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
  [inst_3 : AddTorsor E PE] {f : k → PE} {a b : k}, slope f a b = 0 → f a = f b
-- Mathlib.Order.WithBot
/-- The equivalence between the non-bottom elements of `WithBot α` and `α`.  -/
Equiv.withBotSubtypeNe : {α : Type u_1} → { y // y ≠ ⊥ } ≃ α
-- Std.Data.DTreeMap.Raw.Basic
/-- Check if all elements satisfy the predicate, short-circuiting if a predicate fails.  -/
Std.DTreeMap.Raw.all : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → ((a : α) → β a → Bool) → Bool
-- Init.Data.Iterators.Consumers.Monadic.Access
Std.IterM.IsPlausibleNthOutputStep.below.yield : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β]
  {motive :
    (a : ℕ) →
      (a_1 : Std.IterM m β) →
        (a_2 : Std.IterStep (Std.IterM m β) β) → Std.IterM.IsPlausibleNthOutputStep a a_1 a_2 → Prop}
  {n : ℕ} {it it' : Std.IterM m β} {out : β} {step : Std.IterStep (Std.IterM m β) β}
  (a : it.IsPlausibleStep (Std.IterStep.yield it' out)) (a_1 : Std.IterM.IsPlausibleNthOutputStep n it' step),
  Std.IterM.IsPlausibleNthOutputStep.below a_1 → motive n it' step a_1 → Std.IterM.IsPlausibleNthOutputStep.below ⋯
-- Mathlib.Analysis.Calculus.Taylor
taylorWithin_succ : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℝ → E) (n : ℕ) (s : Set ℝ) (x₀ : ℝ),
  taylorWithin f (n + 1) s x₀ =
    taylorWithin f n s x₀ +
      (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀))
        (PolynomialModule.single ℝ (n + 1) (taylorCoeffWithin f (n + 1) s x₀))
-- Mathlib.Topology.Instances.Rat
Rat.instIsUniformAddGroup : IsUniformAddGroup ℚ
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
_private.Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas.0.Nat.nthRoot.pow_go_le : ∀ {guess fuel : ℕ}, guess ≤ fuel → ∀ (n a : ℕ), Nat.nthRoot.go n a fuel guess ^ (n + 2) ≤ a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.map_map : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {A : Type v} [inst_1 : CommRing A] (f : R →+* A)
  {B : Type w} [inst_2 : CommRing B] (g : A →+* B), (W.map f).map g = W.map (g.comp f)
-- Lean.Elab.Coinductive
Lean.Elab.Command.CoinductiveElabData.mk : Lean.Syntax →
  Lean.Name → Lean.Syntax → Lean.Elab.Modifiers → Array Lean.Syntax → Bool → Lean.Elab.Command.CoinductiveElabData
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_filter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  {f : α → β → Bool} {k : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.getKey? k =
    (t.getKey? k).pfilter fun x h' => f x (Std.DTreeMap.Internal.Impl.Const.get t x ⋯)
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.zpow_mem : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) {x : K}, x ∈ s → ∀ (n : ℤ), x ^ n ∈ s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_insertManyIfNewUnit!_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] [inst : Inhabited α],
  t.WF →
    ∀ {l : List α} {k : α},
      k ∈ t → (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l)).getKey! k = t.getKey! k
-- Mathlib.Order.Preorder.Chain
isChain_univ_iff : ∀ {α : Type u_1} {r : α → α → Prop}, IsChain r Set.univ ↔ Std.Trichotomous r
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.cancelDen.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr) (val : ℤ) (x n : Lean.Grind.Linarith.Var),
  sizeOf (Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.cancelDen c val x n) =
    1 + sizeOf c + sizeOf val + sizeOf x + sizeOf n
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- The two subgroups are commensurable.  -/
IsHeckeTriple.commensurable : ∀ {G : Type u_1} {inst : Group G} (Δ : Submonoid G) {H₁ H₂ : Subgroup G} [self : IsHeckeTriple Δ H₁ H₂],
  H₁.Commensurable H₂
-- Mathlib.Topology.Order.OrderClosed
Iic_mem_nhds : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b : α},
  b < a → Set.Iic a ∈ nhds b
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α},
  List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
    (∀ a ∈ t, l.contains a = false) → (t.insertManyIfNewUnit l).size = t.size + l.length
-- Lean.Elab.DefView
Lean.Elab.DefKind.def.sizeOf_spec : sizeOf Lean.Elab.DefKind.def = 1
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.isEmpty_toType_iff : ∀ {o : Ordinal.{u_1}}, IsEmpty o.ToType ↔ o = 0
-- Mathlib.SetTheory.ZFC.Class
Class.congToClass_empty : Class.congToClass ∅ = ∅
-- Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Finset.support_prod : ∀ {ι : Type u_1} {κ : Type u_2} {M₀ : Type u_4} [inst : CommMonoidWithZero M₀] [Nontrivial M₀] [NoZeroDivisors M₀]
  (s : Finset ι) (f : ι → κ → M₀), (Function.support fun j => ∏ i ∈ s, f i j) = ⋂ i ∈ s, Function.support (f i)
-- Init.Grind.ToInt
Lean.Grind.instDecidableEqIntInterval.decEq : (x x_1 : Lean.Grind.IntInterval) → Decidable (x = x_1)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
AddEquiv.withBotCongr_trans : ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : Add α] [inst_1 : Add β] [inst_2 : Add γ] (e₁ : α ≃+ β) (e₂ : β ≃+ γ),
  (e₁.trans e₂).withBotCongr = e₁.withBotCongr.trans e₂.withBotCongr
-- Mathlib.Algebra.Group.ULift
ULift.addSemigroup : {α : Type u} → [AddSemigroup α] → AddSemigroup (ULift.{u_1, u} α)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.beq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {m₁ m₂ : Std.DTreeMap α β cmp} [inst : (k : α) → BEq (β k)]
  [inst_1 : Std.LawfulEqCmp cmp] [Std.TransCmp cmp] [∀ (k : α), ReflBEq (β k)], m₁.Equiv m₂ → (m₁ == m₂) = true
-- Mathlib.Algebra.Order.Ring.Basic
/-- A function `f : α → R` is nonarchimedean if it satisfies the ultrametric inequality
`f (a + b) ≤ max (f a) (f b)` for all `a b : α`.  -/
IsNonarchimedean : {R : Type u_3} → [LinearOrder R] → {α : Type u_4} → [Add α] → (α → R) → Prop