mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Tactics
/-- Theorems tagged with the `method_specs_simp` attribute are used by `@[method_specs]` to further
rewrite the theorem statement. This is primarily used to rewrite type class methods further to
the desired user-visible form, e.g. from `Append.append` to `HAppend.hAppend`, which has the familiar
notation associated.

The `method_specs` theorems are created on demand (using the realizable constant feature). Thus,
this simp set should behave the same in all modules. Do not add theorems to it except in the module
defining the thing you are rewriting.
 -/
Lean.Parser.Attr.method_specs_simp : Lean.ParserDescr
-- Std.Http.Transport
/-- Creates a mock server and client that are connected to each other and share the
same underlying state, enabling bidirectional communication.
 -/
Std.Http.Internal.Mock.new : BaseIO (Std.Http.Internal.Mock.Client × Std.Http.Internal.Mock.Server)
-- Mathlib.Order.RelIso.Set
Subrel.instIsWellOrderSubtype : ∀ {α : Type u_1} (r : α → α → Prop) [IsWellOrder α r] (p : α → Prop), IsWellOrder (Subtype p) (Subrel r p)
-- Mathlib.Logic.Denumerable
/-- The lift of a denumerable type is denumerable.  -/
Denumerable.plift : {α : Type u_1} → [Denumerable α] → Denumerable (PLift α)
-- Mathlib.Analysis.Normed.Operator.Bilinear
LinearMap.mkContinuous₂_apply : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  [inst_9 : RingHomIsometric σ₂₃] (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) {C : ℝ}
  (hC : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖) (x : E) (y : F), ((f.mkContinuous₂ C hC) x) y = (f x) y
-- Init.Data.Array.Sort.Basic
Array.mergeSort : {α : Type u_1} → Array α → autoParam (α → α → Bool) Array.mergeSort._auto_1 → Array α
-- Mathlib.Algebra.Lie.Ideal
LieHom.range_eq_top : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L'), f.range = ⊤ ↔ Function.Surjective ⇑f
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.inc.sizeOf_spec : ∀ (x : Lean.IR.VarId) (n : ℕ) (c persistent : Bool) (b : Lean.IR.FnBody),
  sizeOf (Lean.IR.FnBody.inc x n c persistent b) = 1 + sizeOf x + sizeOf n + sizeOf c + sizeOf persistent + sizeOf b
-- Aesop.Forward.Match
Aesop.CompleteMatch.toMessageData : Aesop.ForwardRule → Aesop.CompleteMatch → Lean.MessageData
-- Mathlib.CategoryTheory.Limits.Elements
CategoryTheory.CategoryOfElements.instCreatesLimitElementsπ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor C (Type w)} →
      {I : Type u₁} →
        [inst_1 : CategoryTheory.Category.{v₁, u₁} I] →
          [Small.{w, u₁} I] →
            [CategoryTheory.Limits.HasLimitsOfShape I C] →
              [CategoryTheory.Limits.PreservesLimitsOfShape I A] →
                (F : CategoryTheory.Functor I A.Elements) →
                  CategoryTheory.CreatesLimit F (CategoryTheory.CategoryOfElements.π A)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {a : α} {b : β}, (t.insert a b).getKey! a = a
-- Mathlib.Dynamics.Ergodic.Ergodic
QuasiErgodic.toPreErgodic : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {μ : autoParam (MeasureTheory.Measure α) QuasiErgodic._auto_1},
  QuasiErgodic f μ → PreErgodic f μ
-- Mathlib.LinearAlgebra.Reflection
/-- A formula for $(r_1 r_2)^m$, where $m$ is an integer.  -/
Module.reflection_mul_reflection_zpow : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M}
  {f g : Module.Dual R M} (hf : f x = 2) (hg : g y = 2) (m : ℤ) (t : optParam R (f y * g x - 2)),
  autoParam (t = f y * g x - 2) Module.reflection_mul_reflection_zpow._auto_1 →
    ↑((Module.reflection hf * Module.reflection hg) ^ m) =
      LinearMap.id +
          (Polynomial.eval t (Polynomial.Chebyshev.S R ((m - 2) / 2)) *
              (Polynomial.eval t (Polynomial.Chebyshev.S R ((m - 1) / 2)) +
                Polynomial.eval t (Polynomial.Chebyshev.S R ((m - 3) / 2)))) •
            (LinearMap.smulRight (g x • f - g) y - LinearMap.smulRight f x) +
        (Polynomial.eval t (Polynomial.Chebyshev.S R ((m - 1) / 2)) *
            (Polynomial.eval t (Polynomial.Chebyshev.S R (m / 2)) +
              Polynomial.eval t (Polynomial.Chebyshev.S R ((m - 2) / 2)))) •
          (LinearMap.smulRight (f y • g - f) x - LinearMap.smulRight g y)
-- Mathlib.Order.GaloisConnection.Basic
sInf_image2_eq_sSup_sSup : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : CompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β},
  (∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ u₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) →
    (∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ u₂ a) (u a ∘ ⇑OrderDual.ofDual)) →
      sInf (Set.image2 u s t) = u (sSup s) (sSup t)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.diff.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m₁ m₁_1 : Std.ExtHashMap α β), m₁ = m₁_1 → ∀ (m₂ m₂_1 : Std.ExtHashMap α β), m₂ = m₂_1 → m₁.diff m₂ = m₁_1.diff m₂_1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_eq_some_iff : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {k k' : α}, m.WF → (m.getKey? k = some k' ↔ ∃ (h : k ∈ m), m.getKey k h = k')
-- Init.Data.List.Nat.TakeDrop
List.drop_eq_drop_min : ∀ {α : Type u_1} {l : List α} {i : ℕ}, List.drop i l = List.drop (min i l.length) l
-- Lean.Meta.Tactic.UnifyEq
Lean.Meta.UnifyEqResult.mvarId : Lean.Meta.UnifyEqResult → Lean.MVarId
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMon.Hom.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.AddMon C} (hom hom_1 : M.X ⟶ N.X) (e_hom : hom = hom_1)
  [isAddMonHom_hom : CategoryTheory.IsAddMonHom hom],
  { hom := hom, isAddMonHom_hom := isAddMonHom_hom } = { hom := hom_1, isAddMonHom_hom := ⋯ }
-- Mathlib.Algebra.Star.LinearMap
LinearMap.toMatrix'_intrinsicStar : ∀ {R : Type u_4} {m : Type u_5} {n : Type u_6} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Fintype m]
  [inst_3 : DecidableEq m] (f : WithConv ((m → R) →ₗ[R] n → R)),
  LinearMap.toMatrix' (star f).ofConv = (LinearMap.toMatrix' f.ofConv).map star
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.inl_v_desc_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cochain K M 0) (β : CochainComplex.HomComplex.Cocycle L M 1)
  (hαβ : CochainComplex.HomComplex.δ 0 1 α + (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯ = 0) (p : ℤ) {Z : C}
  (h : M.X p ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.inl φ).v p p ⋯)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.desc φ α β hαβ).f p) h) =
    CategoryTheory.CategoryStruct.comp (α.v p p ⋯) h
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.div.inj : ∀ {k : ℤ} {e : Lean.Meta.Grind.Arith.CommRing.EqCnstr} {k_1 : ℤ} {e_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr},
  Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.div k e = Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.div k_1 e_1 →
    k = k_1 ∧ e = e_1
-- Std.Time.Internal.Bounded
/-- Convert a `Nat` to a `Bounded.LE` if it checks.
 -/
Std.Time.Internal.Bounded.LE.ofNat? : {hi : ℕ} → ℕ → Option (Std.Time.Internal.Bounded.LE 0 ↑hi)
-- Mathlib.Combinatorics.Matroid.Closure
/-- A version of `Matroid.spanning_iff_exists_isBase_subset` in which the `S ⊆ M.E` condition
appears in the RHS of the equivalence rather than as a hypothesis.  -/
Matroid.spanning_iff_exists_isBase_subset' : ∀ {α : Type u_2} {M : Matroid α} {S : Set α}, M.Spanning S ↔ (∃ B, M.IsBase B ∧ B ⊆ S) ∧ S ⊆ M.E
-- Lean.Elab.Do.Basic
/-- Throw an error if the given names are not declared `mut` variables.  -/
Lean.Elab.Do.throwUnlessMutVarsDeclared : Array Lean.Ident → Lean.Elab.Do.DoElabM Unit
-- Init.Data.Option.Lemmas
Option.pelim_some : ∀ {α : Type u_1} {a : α} {α_1 : Sort u_2} {b : α_1} {f : (a_1 : α) → some a = some a_1 → α_1},
  (some a).pelim b f = f a ⋯
-- Mathlib.Topology.Continuous
ClusterPt.map : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {x : X}
  {lx : Filter X} {ly : Filter Y}, ClusterPt x lx → ContinuousAt f x → Filter.Tendsto f lx ly → ClusterPt (f x) ly
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.coe_toLin : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (A : GL n R),
  ↑(Matrix.GeneralLinearGroup.toLin A) = (↑A).mulVecLin
-- Mathlib.Order.SupIndep
LE.le.hcongr_4 : ∀ (α α' : Type u),
  α = α' →
    ∀ (self : LE α) (self' : LE α'),
      self ≍ self' → ∀ (a : α) (a' : α'), a ≍ a' → ∀ (a_1 : α) (a'_1 : α'), a_1 ≍ a'_1 → (a ≤ a_1) ≍ (a' ≤ a'_1)
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Metric.closure_closedBall : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, closure (Metric.closedBall x ε) = Metric.closedBall x ε
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- For `A B` two finite sets whose product has cardinality at least 2,
we can find at least two unique pairs.  -/
TwoUniqueProds.uniqueMul_of_one_lt_card : ∀ {G : Type u_1} {inst : Mul G} [self : TwoUniqueProds G] {A B : Finset G},
  1 < A.card * B.card → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
-- Mathlib.RepresentationTheory.Basic
/-- Given representations of `G` on `V` and `W`, there is a natural representation of `G` on their
tensor product `V ⊗[k] W`.
 -/
Representation.tprod : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : CommSemiring k] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : Module k V] →
                [inst_4 : AddCommMonoid W] →
                  [inst_5 : Module k W] →
                    Representation k G V → Representation k G W → Representation k G (TensorProduct k V W)
-- Mathlib.Probability.CondVar
ProbabilityTheory.condVar_of_not_sigmaFinite : ∀ {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {hm : m ≤ m₀} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  ¬MeasureTheory.SigmaFinite (μ.trim hm) → ProbabilityTheory.condVar m X μ = 0
-- Mathlib.Order.Filter.Basic
Filter.frequently_iff_neBot : ∀ {α : Type u} {l : Filter α} {p : α → Prop}, (∃ᶠ (x : α) in l, p x) ↔ (l ⊓ Filter.principal {x | p x}).NeBot
-- Init.Grind.AC
Lean.Grind.AC.instReprSeq : Repr Lean.Grind.AC.Seq
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.decompose'_apply : ∀ (R : Type u_1) {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} (w : σ → M) [inst_1 : AddCommMonoid M]
  [inst_2 : DecidableEq M] (φ : MvPolynomial σ R) (m : M),
  ↑((MvPolynomial.decompose' R w φ) m) = (MvPolynomial.weightedHomogeneousComponent w m) φ
-- Mathlib.RingTheory.NoetherNormalization
/-- `eqv2` is the isomorphism from `k[X_0,...,X_n]/T(I)` into `k[X_0,...,X_n]/I`,
induced by `T`.  -/
_private.Mathlib.RingTheory.NoetherNormalization.0.NoetherNormalization.eqv2 : {k : Type u_1} →
  [inst : Field k] →
    {n : ℕ} →
      (f : MvPolynomial (Fin (n + 1)) k) →
        (I : Ideal (MvPolynomial (Fin (n + 1)) k)) →
          (MvPolynomial (Fin (n + 1)) k ⧸ Ideal.map (NoetherNormalization.T✝ f) I) ≃ₐ[k]
            MvPolynomial (Fin (n + 1)) k ⧸ I
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- Like `isRflTheorem`, but also returns `true` for `@[backward_defeq]` theorems.  -/
Lean.Meta.isBackwardRflTheorem : Lean.Name → Lean.CoreM Bool
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- The monoidal product is a measurable function from the product of probability spaces over
`α` and `β` into the type of probability spaces over `α × β`. Lemma 4.1 of [A synthetic approach to
Markov kernels, conditional independence and theorems on sufficient statistics][fritz2020].  -/
MeasureTheory.ProbabilityMeasure.measurable_fun_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β],
  Measurable fun μ => (↑μ.1).prod ↑μ.2
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
_private.Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound.0.Std.Tactic.BVDecide.LRAT.Internal.WellFormedAction.match_1.eq_2 : ∀ {α : Type u_2} {β : Type u_1} (motive : Std.Tactic.BVDecide.LRAT.Action β α → Sort u_3)
  (x : Std.Tactic.BVDecide.LRAT.Action β α)
  (h_1 :
    (id : ℕ) →
      (c : β) →
        (p : Std.Sat.Literal α) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) → motive (Std.Tactic.BVDecide.LRAT.Action.addRat id c p rupHints ratHints))
  (h_2 : (x : Std.Tactic.BVDecide.LRAT.Action β α) → motive x),
  (∀ (id : ℕ) (c : β) (p : Std.Sat.Literal α) (rupHints : Array ℕ) (ratHints : Array (ℕ × Array ℕ)),
      x = Std.Tactic.BVDecide.LRAT.Action.addRat id c p rupHints ratHints → False) →
    (match x with
      | Std.Tactic.BVDecide.LRAT.Action.addRat id c p rupHints ratHints => h_1 id c p rupHints ratHints
      | x => h_2 x) =
      h_2 x
-- Mathlib.Analysis.Normed.Group.Basic
dist_norm_norm_le_norm_inv_mul : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a b : E), dist ‖a‖ ‖b‖ ≤ ‖a⁻¹ * b‖
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenModifier.names : Array String
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
/-- Given a property of germs of functions and sets in the model space, then one defines
a corresponding property of functions on sets in a charted space, by requiring that it holds
around each point of the set, in the preferred charts.  -/
ChartedSpace.LiftPropOn : {H : Type u_1} →
  {M : Type u_2} →
    {H' : Type u_3} →
      {M' : Type u_4} →
        [inst : TopologicalSpace H] →
          [inst_1 : TopologicalSpace M] →
            [ChartedSpace H M] →
              [inst : TopologicalSpace H'] →
                [inst_2 : TopologicalSpace M'] →
                  [ChartedSpace H' M'] → ((H → H') → Set H → H → Prop) → (M → M') → Set M → Prop
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.norm_mul_cos_arg : ∀ (x : ℂ), ‖x‖ * Real.cos x.arg = x.re
-- Mathlib.Order.Filter.Basic
Filter.Eventually.exists : ∀ {α : Type u} {p : α → Prop} {f : Filter α} [f.NeBot], (∀ᶠ (x : α) in f, p x) → ∃ x, p x
-- Mathlib.Algebra.Lie.DirectSum
DFinsupp.lsingle.eq_1 : ∀ {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] (i : ι),
  DFinsupp.lsingle i = { toFun := DFinsupp.single i, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.subcomplex_injective : ∀ {X : SSet} {x y : X.N}, x.subcomplex = y.subcomplex → x = y
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.edges_take : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ), (p.take n).edges = List.take n p.edges
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [Std.LawfulEqOrd α],
  t.WF → t.isEmpty = false → ∀ {km fallback : α}, t.maxKeyD fallback = km ↔ km ∈ t ∧ ∀ k ∈ t, (compare k km).isLE = true
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_eq_pow : ∀ (x : ENNReal) (y : ℝ), x.rpow y = x ^ y
-- Mathlib.CategoryTheory.Abelian.Preradical.Radical
/-- A preradical `Φ` is radical if and only if it `Φ` vanishes on the quotient `Φ.quotient`.  -/
CategoryTheory.Abelian.Preradical.isRadical_iff_isZero : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C),
  CategoryTheory.Abelian.Preradical.isRadical C Φ ↔ CategoryTheory.Limits.IsZero (Φ.quotient.comp Φ.r)
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
SemiSimplexCategory.hom_ext_iff : ∀ {a b : SemiSimplexCategory} {f g : a ⟶ b}, f = g ↔ SemiSimplexCategory.homEquiv f = SemiSimplexCategory.homEquiv g
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.map'_eq_hom₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.ComposableArrows C 1),
  F.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 CategoryTheory.ComposableArrows.homMk₁._proof_5 = F.hom
-- Std.Data.TreeMap.Lemmas
/-- Variant of `getD_map` that holds without `LawfulEqCmp`.  -/
Std.TreeMap.getD_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → γ} {k : α} {fallback : γ},
  (Std.TreeMap.map f t).getD k fallback = (Option.pmap (fun v h => f (t.getKey k h) v) t[k]? ⋯).getD fallback
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.Skeleton.instInhabited : Inhabited FintypeCat.Skeleton
-- Mathlib.Order.Bounded
Set.bounded_ge_iff_bounded_gt : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α] [NoMinOrder α],
  Set.Bounded (fun x1 x2 => x1 ≥ x2) s ↔ Set.Bounded (fun x1 x2 => x1 > x2) s
-- Init.Data.SInt.Bitwise
Int64.not_or_self : ∀ {a : Int64}, ~~~a ||| a = -1
-- Mathlib.Analysis.Normed.Algebra.Spectrum
/-- If `S` is a closed subalgebra of a Banach algebra `A`, then for any `x : S`, the boundary of
the spectrum of `x` relative to `S` is a subset of the boundary of the spectrum of `↑x : A`
relative to `A`.  -/
Subalgebra.frontier_subset_frontier : ∀ {𝕜 : Type u_3} {A : Type u_4} {SA : Type u_5} [inst : NormedRing A] [CompleteSpace A] [inst_2 : SetLike SA A]
  [inst_3 : SubringClass SA A] [inst_4 : NormedField 𝕜] [inst_5 : NormedAlgebra 𝕜 A] [instSMulMem : SMulMemClass SA 𝕜 A]
  (S : SA) [hS : IsClosed ↑S] (x : ↥S), frontier (spectrum 𝕜 x) ⊆ frontier (spectrum 𝕜 ↑x)
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.comp_assoc : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_10} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P]
  [inst_3 : Mul Q] (f : M →ₙ* N) (g : N →ₙ* P) (h : P →ₙ* Q), (h.comp g).comp f = h.comp (g.comp f)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.toString.match_1.splitter : (motive : Substring.Raw → Sort u_1) →
  (x : Substring.Raw) →
    ((s : String) → (b e : String.Pos.Raw) → motive { str := s, startPos := b, stopPos := e }) → motive x
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_range_succ' : ∀ {M : Type u_4} [inst : AddCommMonoid M] (f : ℕ → M) (n : ℕ),
  ∑ k ∈ Finset.range (n + 1), f k = ∑ k ∈ Finset.range n, f (k + 1) + f 0
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.weakLimit.lift_π_assoc : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] {F : CategoryTheory.Functor J C}
  [inst_2 : CategoryTheory.Limits.HasWeakLimit F] (c : CategoryTheory.Limits.Cone F) (j : J) {Z : C} (h : F.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakLimit.lift F c)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakLimit.π F j) h) =
    CategoryTheory.CategoryStruct.comp (c.π.app j) h
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso_inv_τ₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso._auto_3),
  (X.kernelSequenceOpcyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv.τ₃ =
    CategoryTheory.CategoryStruct.id ((X.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ f₁))
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Polarization identity: The real inner product, in terms of the norm.  -/
real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F),
  inner ℝ x y = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsNontrivial.nontrivial_codomain : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  [hv : v.IsNontrivial], Nontrivial Γ₀
-- Mathlib.RingTheory.Localization.NumDen
IsFractionRing.num_den_reduced : ∀ (A : Type u_1) [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] (x : K),
  IsRelPrime (IsFractionRing.num A x) ↑(IsFractionRing.den A x)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumUniformlyOn.tendstoUniformlyOn_finsetRange : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] {g : β → α} {s : Set β} [inst_1 : UniformSpace α]
  {f : ℕ → β → α},
  HasSumUniformlyOn f g s → TendstoUniformlyOn (fun x1 x2 => ∑ i ∈ Finset.range x1, f i x2) g Filter.atTop s
-- Mathlib.Order.Interval.Multiset
Multiset.mem_Icc : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b x : α}, x ∈ Multiset.Icc a b ↔ a ≤ x ∧ x ≤ b
-- Mathlib.Order.Filter.CountableSeparatingOn
HasCountableSeparatingOn.exists_countable_separating : ∀ {α : Type u_1} {p : Set α → Prop} {t : Set α} [self : HasCountableSeparatingOn α p t],
  ∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- If `𝕜` is a nontrivially normed field, any T2 topology on `𝕜` which makes it a topological
vector space over itself (with the norm topology) is *equal* to the norm topology.  -/
unique_topology_of_t2 : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {t : TopologicalSpace 𝕜},
  IsTopologicalAddGroup 𝕜 → ContinuousSMul 𝕜 𝕜 → T2Space 𝕜 → t = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
-- Lean.Data.Lsp.Client
Lean.Lsp.RegistrationParams.mk.inj : ∀ {registrations registrations_1 : Array Lean.Lsp.Registration},
  { registrations := registrations } = { registrations := registrations_1 } → registrations = registrations_1
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Given an AddMonoidHom `f : M →+ N` and Submonoid `S ⊆ M` such that
`f(S) ⊆ AddUnits N`, for all `y, z ∈ S`, we have `- (f y) = - (f z) → f y = f z`.  -/
AddSubmonoid.LocalizationMap.neg_inj : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {f : M →+ N}
  (hf : ∀ (y : ↥S), IsAddUnit (f ↑y)) {y z : ↥S},
  -(IsAddUnit.liftRight (f.domRestrict S) hf) y = -(IsAddUnit.liftRight (f.domRestrict S) hf) z → f ↑y = f ↑z
-- Batteries.Data.DList.Basic
Batteries.DList.mk : {α : Type u} → (apply : List α → List α) → (∀ (l : List α), apply l = apply [] ++ l) → Batteries.DList α
-- Mathlib.RingTheory.HopfAlgebra.Convolution
LinearMap.id_mul_antipode : ∀ {R : Type u_1} {C : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring C] [inst_2 : HopfAlgebra R C],
  WithConv.toConv LinearMap.id * WithConv.toConv (HopfAlgebraStruct.antipode R) = 1
-- Mathlib.Topology.UniformSpace.Equiv
/-- Uniform continuity of the inverse  -/
UniformEquiv.uniformContinuous_invFun : ∀ {α : Type u_4} {β : Type u_5} [inst : UniformSpace α] [inst_1 : UniformSpace β] (self : α ≃ᵤ β),
  UniformContinuous self.invFun