mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso_hom_app : ∀ {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_3, u_3} B]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'}
  {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) (X : A),
  (AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso eB hF).hom.app X =
    CategoryTheory.CategoryStruct.comp (eA.unitIso.hom.app X)
      (CategoryTheory.CategoryStruct.comp (eA.inverse.map (e'.unitIso.hom.app (eA.functor.obj X)))
        (CategoryTheory.CategoryStruct.comp (eA.inverse.map (e'.inverse.map (hF.hom.app X)))
          (eA.inverse.map (e'.inverse.map (eB.counitIso.inv.app (F.obj X))))))
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
LinearMap.ker_noncommProd_eq_of_supIndep_ker : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V] {ι : Type u_1} {f : ι → V →ₗ[K] V} (s : Finset ι)
  (comm : (↑s).Pairwise (Function.onFun Commute f)),
  (s.SupIndep fun i => (f i).ker) → (s.noncommProd f comm).ker = ⨆ i ∈ s, (f i).ker
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.erase0_rhs.inj : ∀ {c c_1 : Lean.Meta.Grind.AC.EqCnstr},
  Lean.Meta.Grind.AC.EqCnstrProof.erase0_rhs c = Lean.Meta.Grind.AC.EqCnstrProof.erase0_rhs c_1 → c = c_1
-- Mathlib.Order.Heyting.Basic
sup_sdiff_cancel' : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a ≤ b → b ≤ c → b ⊔ c \ a = c
-- Init.Data.BitVec.Decidable
BitVec.instDecidableForallBitVecSucc : {n : ℕ} →
  (P : BitVec (n + 1) → Prop) →
    [DecidablePred P] →
      [Decidable (∀ (x : Bool) (v : BitVec n), P (BitVec.cons x v))] → Decidable (∀ (v : BitVec (n + 1)), P v)
-- Mathlib.Algebra.BigOperators.Sym
Finset.sum_sym2_filter_not_isDiag : ∀ {ι : Type u_1} {M : Type u_2} [inst : LinearOrder ι] [inst_1 : AddCommMonoid M] (s : Finset ι) (p : Sym2 ι → M),
  ∑ i ∈ s.sym2 with ¬i.IsDiag, p i = ∑ i ∈ s.offDiag with i.1 < i.2, p s(i.1, i.2)
-- Mathlib.Data.Nat.Log
_private.Mathlib.Data.Nat.Log.0.Nat.log.go_aux : ∀ {n b fuel : ℕ}, 1 < b → n < b ^ (fuel + 1) → b ≤ n → n < (b * b) ^ fuel
-- Std.Async.System
/-- Information about a single CPU core.
 -/
Std.Async.System.CPUInfo : Type
-- Mathlib.Order.UpperLower.Principal
UpperSet.Ici_lt_top : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, UpperSet.Ici a < ⊤
-- Mathlib.Order.Quotient
Quotient.instLE_mathlib : {α : Type u_1} → {s : Setoid α} → [LE α] → LE (Quotient s)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_eq_getD_default : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α}
  [inst_1 : Inhabited (β a)], m.get! a = m.getD a default
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
/-- `p.Fiber S` is isomorphic to the quotient `Sₚ ⧸ pSₚ`.  -/
Ideal.Fiber.algEquivQuotient : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (p : Ideal R) →
            [inst_3 : p.IsPrime] →
              p.Fiber S ≃ₐ[S]
                Localization (Algebra.algebraMapSubmonoid S p.primeCompl) ⧸
                  Ideal.map
                    (algebraMap (Localization p.primeCompl) (Localization (Algebra.algebraMapSubmonoid S p.primeCompl)))
                    (IsLocalRing.maximalIdeal (Localization p.primeCompl))
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.AreSeparated.symm : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {s t : Set X}, Metric.AreSeparated s t → Metric.AreSeparated t s
-- Mathlib.Topology.Constructions
Homeomorph.piCurry_symm_apply : ∀ {X : Type u_9} {Y : Type u_10} {Z : Type u_11} [inst : TopologicalSpace Z] (a : X → Y → Z) (a_1 : X × Y),
  Homeomorph.piCurry.symm a a_1 = Function.uncurry a a_1
-- Init.Guard
/-- Reducible defeq matching for `guard_hyp` types  -/
Lean.Parser.colonR : Lean.ParserDescr
-- Mathlib.Data.List.Lattice
List.inter.eq_1 : ∀ {α : Type u_1} [inst : BEq α] (l₁ l₂ : List α), l₁.inter l₂ = List.filter (fun x => List.elem x l₂) l₁
-- Mathlib.Computability.DFA
/-- `M.eval x` evaluates `M` with input `x` starting from the state `M.start`.  -/
DFA.eval : {α : Type u} → {σ : Type v} → DFA α σ → List α → σ
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.hausdorffEDist_singleton : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α}, Metric.hausdorffEDist {x} {y} = edist x y
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instAddCommMonoid : {α : Type u_1} →
  {β : Type u_2} → [inst : MeasurableSpace α] → [AddCommMonoid β] → AddCommMonoid (MeasureTheory.SimpleFunc α β)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities.documentSymbolProvider : Lean.Lsp.ServerCapabilities → Bool
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming
Tactic.ComputeAsymptotics.MultiseriesExpansion.IsZero.const : ∀ {c : Tactic.ComputeAsymptotics.MultiseriesExpansion []}, c.toReal = 0 → c.IsZero
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.natTrans_ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {r : HomRel C} {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F G : CategoryTheory.Functor (CategoryTheory.Quotient r) D}
  (τ₁ τ₂ : F ⟶ G),
  (CategoryTheory.Quotient.functor r).whiskerLeft τ₁ = (CategoryTheory.Quotient.functor r).whiskerLeft τ₂ → τ₁ = τ₂
-- Mathlib.Algebra.Order.Group.Abs
eq_of_mabs_div_le_all : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [DenselyOrdered G] {x y : G},
  (∀ ε > 1, |x / y|ₘ ≤ ε) → x = y
-- Mathlib.Analysis.CStarAlgebra.Unitary.Maps
/-- Left multiplication by a unitary as a linear isometric equivalence.  -/
Unitary.mulLeft : (R : Type u_1) →
  (A : Type u_2) →
    [inst : NormedRing A] →
      [inst_1 : StarRing A] →
        [CStarRing A] → [inst_3 : Ring R] → [inst_4 : Module R A] → [SMulCommClass R A A] → ↥(unitary A) →* A ≃ₗᵢ[R] A
-- Lean.Elab.MutualDef
Lean.Elab.Term.linter.unusedSectionVars : Lean.Option Bool
-- Init.Data.Bool
Bool.ite_eq_true_distrib : ∀ (p : Prop) [h : Decidable p] (t f : Bool), ((if p then t else f) = true) = if p then t = true else f = true
-- Mathlib.MeasureTheory.Integral.Marginal
MeasureTheory.lmarginal_union' : ∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] (μ : (i : δ) → MeasureTheory.Measure (X i))
  [inst_1 : DecidableEq δ] [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] (f : ((i : δ) → X i) → ENNReal),
  Measurable f → ∀ {s t : Finset δ}, Disjoint s t → ∫⋯∫⁻_s ∪ t, f ∂μ = ∫⋯∫⁻_t, ∫⋯∫⁻_s, f ∂μ ∂μ
-- Mathlib.Geometry.Manifold.Submersion
/-- A choice of chart on the domain `M` of a submersion `f` at `x`:
w.r.t. this chart and the data `h.codChart` and `h.equiv`,
`f` will look like a projection `(u,v) ↦ u` in these extended charts.
The particular chart is arbitrary, but this choice matches the witnesses given by
`h.codChart` and `h.codChart`.  -/
Manifold.IsSubmersionAtOfComplement.domChart : {𝕜 : Type u_1} →
  {E'' : Type u_3} →
    {F : Type u_5} →
      {H : Type u_7} →
        {G : Type u_9} →
          {E : Type u} →
            [inst : NontriviallyNormedField 𝕜] →
              [inst_1 : NormedAddCommGroup E] →
                [inst_2 : NormedSpace 𝕜 E] →
                  [inst_3 : NormedAddCommGroup E''] →
                    [inst_4 : NormedSpace 𝕜 E''] →
                      [inst_5 : NormedAddCommGroup F] →
                        [inst_6 : NormedSpace 𝕜 F] →
                          [inst_7 : TopologicalSpace H] →
                            [inst_8 : TopologicalSpace G] →
                              {I : ModelWithCorners 𝕜 E H} →
                                {J : ModelWithCorners 𝕜 E'' G} →
                                  {M : Type u_11} →
                                    {N : Type u_13} →
                                      [inst_9 : TopologicalSpace M] →
                                        [inst_10 : ChartedSpace H M] →
                                          [inst_11 : TopologicalSpace N] →
                                            [inst_12 : ChartedSpace G N] →
                                              {n : WithTop ℕ∞} →
                                                {f : M → N} →
                                                  {x : M} →
                                                    Manifold.IsSubmersionAtOfComplement F I J n f x →
                                                      OpenPartialHomeomorph M H
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.HomotopyCategory.cases_on : ∀ {V : SSet.Truncated 2} {motive : V.HomotopyCategory → Prop},
  (∀ (x : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })),
      motive (SSet.Truncated.HomotopyCategory.mk x)) →
    ∀ (x : V.HomotopyCategory), motive x
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.coe_eval₂RingHom : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : CommSemiring S] (f : R →+* S) (x : S),
  ⇑(Polynomial.eval₂RingHom f x) = Polynomial.eval₂ f x
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
/-- Alternative formulation of `contravariant_sequence_exact₃`  -/
CategoryTheory.Abelian.Ext.contravariant_sequence_exact₃' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) (n₀ n₁ : ℕ)
  (h : 1 + n₀ = n₁),
  { X₁ := AddCommGrpCat.of (CategoryTheory.Abelian.Ext S.X₁ Y n₀),
      X₂ := AddCommGrpCat.of (CategoryTheory.Abelian.Ext S.X₃ Y n₁),
      X₃ := AddCommGrpCat.of (CategoryTheory.Abelian.Ext S.X₂ Y n₁), f := AddCommGrpCat.ofHom (hS.extClass.precomp Y h),
      g := AddCommGrpCat.ofHom ((CategoryTheory.Abelian.Ext.mk₀ S.g).precomp Y ⋯), zero := ⋯ }.Exact
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.find?_toList_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k k' : α} {v : β},
      List.find? (fun a => a.1 == k) m.toList = some (k', v) ↔ m.getKey? k = some k' ∧ m[k]? = some v
-- Mathlib.Order.OmegaCompletePartialOrder
Part.mem_chain_of_mem_ωSup : ∀ {α : Type u_2} {c : OmegaCompletePartialOrder.Chain (Part α)} {a : α}, a ∈ Part.ωSup c → Part.some a ∈ c
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
SimplexCategoryGenRel.toSimplexCategory_obj_mk : ∀ (n : ℕ), SimplexCategoryGenRel.toSimplexCategory.obj (SimplexCategoryGenRel.mk n) = { len := n }
-- Mathlib.FieldTheory.Fixed
/-- `MulSemiringAction.toAlgHom` is bijective.  -/
FixedPoints.toAlgHom_bijective : ∀ (G : Type u_2) (F : Type u_3) [inst : Group G] [inst_1 : Field F] [inst_2 : MulSemiringAction G F] [Finite G]
  [FaithfulSMul G F], Function.Bijective (MulSemiringAction.toAlgHom (↥(FixedPoints.subfield G F)) F)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.YonedaCollection.map₁_map₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C}
  {G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (η : F ⟶ G) {Y : C}
  (f : X ⟶ Y) (p : CategoryTheory.OverPresheafAux.YonedaCollection F Y),
  CategoryTheory.OverPresheafAux.YonedaCollection.map₂ G f (CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η p) =
    CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η (CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F f p)
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin_zero_of_not_accPt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜}, ¬AccPt x (Filter.principal s) → derivWithin f s x = 0
-- Mathlib.Algebra.Ring.CharZero
CharZero.NeZero.two : ∀ {R : Type u_2} [inst : AddMonoidWithOne R] [CharZero R], NeZero 2
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.OpenNhdsOf.mem : ∀ {α : Type u_2} [inst : TopologicalSpace α] {x : α} (U : TopologicalSpace.OpenNhdsOf x), x ∈ U
-- Mathlib.LinearAlgebra.CliffordAlgebra.Grading
CliffordAlgebra.GradedAlgebra.ι_sq_scalar : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (m : M),
  (CliffordAlgebra.GradedAlgebra.ι Q) m * (CliffordAlgebra.GradedAlgebra.ι Q) m =
    (algebraMap R (DirectSum (ZMod 2) fun i => ↥(CliffordAlgebra.evenOdd Q i))) (Q m)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.centerToMulOpposite_apply_coe : ∀ {R : Type u} [inst : NonAssocSemiring R] (r : ↥(Subsemigroup.center R)),
  ↑(Subsemiring.centerToMulOpposite r) = MulOpposite.op ↑r
-- Lean.Environment
Lean.instInhabitedPersistentEnvExtension : {α β σ : Type} → [Inhabited σ] → Inhabited (Lean.PersistentEnvExtension α β σ)
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.comp_right_differentiable_iff : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G},
  Differentiable 𝕜 (f ∘ ⇑iso) ↔ Differentiable 𝕜 f
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.UnitaryGroup.mul_val : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
  (A B : ↥(Matrix.unitaryGroup n α)), ↑(A * B) = ↑A * ↑B
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.homMk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {f f' : CategoryTheory.StructuredArrow S T} (g g_1 : f.right ⟶ f'.right)
  (e_g : g = g_1) (w : CategoryTheory.CategoryStruct.comp f.hom (T.map g) = f'.hom),
  CategoryTheory.StructuredArrow.homMk g w = CategoryTheory.StructuredArrow.homMk g_1 ⋯
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.mem_orbit_vadd : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (g : G) (a : α),
  a ∈ AddAction.orbit G (g +ᵥ a)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- Add the entries generated by `act name constInfo` to the `PreDiscrTree`.

Note: It is expensive to create two new `IO.Ref`s for every `MetaM` operation,
so instead we reuse the same refs `mstate` and `cstate`. These are also used to
remember the cache, and the name generator across the operations.
 -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.addConstToPreDiscrTree : {α : Type} →
  Lean.Core.Context →
    Lean.Environment →
      Lean.Name →
        Lean.Meta.RefinedDiscrTree.ImportErrorData✝ →
          IO.Ref Lean.Meta.State →
            IO.Ref Lean.Core.State →
              (Lean.Name →
                  Lean.ConstantInfo →
                    Lean.MetaM
                      (List (α × List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)))) →
                Lean.Meta.RefinedDiscrTree.PreDiscrTree α →
                  Lean.Name → Lean.ConstantInfo → BaseIO (Lean.Meta.RefinedDiscrTree.PreDiscrTree α)
-- Mathlib.Analysis.SpecialFunctions.Exp
Complex.locally_lipschitz_exp : ∀ {r : ℝ},
  0 ≤ r → r ≤ 1 → ∀ (x y : ℂ), ‖y - x‖ < r → ‖Complex.exp y - Complex.exp x‖ ≤ (1 + r) * ‖Complex.exp x‖ * ‖y - x‖
-- Mathlib.Logic.Equiv.Defs
Equiv.equivPUnit_symm_apply : ∀ (α : Sort u) [inst : Unique α] (a : PUnit.{v}), (Equiv.equivPUnit α).symm a = default
-- Mathlib.Topology.Order.IntermediateValue
/-- **Intermediate value theorem**: if `f` is continuous on an order-connected set `s` and `a`,
`b` are two points of this set, then `f` sends `s` to a superset of `Icc (f a) (f b)`.  -/
ContinuousOn.surjOn_Icc : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {s : Set α} [hs : s.OrdConnected] {f : α → δ},
  ContinuousOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → Set.SurjOn f s (Set.Icc (f a) (f b))
-- Init.Data.String.Iterator
String.Legacy.instInhabitedIterator : Inhabited String.Legacy.Iterator
-- Init.Prelude
/-- Returns the element at the provided index, counting from `0`. Returns the fallback value `v₀` if the
index is out of bounds.

To return an `Option` depending on whether the index is in bounds, use `a[i]?`. To panic if the
index is out of bounds, use `a[i]!`.

Examples:
 * `#["spring", "summer", "fall", "winter"].getD 2 "never" = "fall"`
 * `#["spring", "summer", "fall", "winter"].getD 0 "never" = "spring"`
 * `#["spring", "summer", "fall", "winter"].getD 4 "never" = "never"`
 -/
Array.getD : {α : Type u_1} → Array α → ℕ → α → α
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.uniformSpace_eq_iInf : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E},
  ContDiffMapSupportedIn.uniformSpace =
    ⨅ i, UniformSpace.comap (⇑(ContDiffMapSupportedIn.structureMapLM ℝ n i)) inferInstance
-- Mathlib.CategoryTheory.Limits.Types.Yoneda
CategoryTheory.Limits.compYonedaSectionsEquiv_symm_apply_coe : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] (F : CategoryTheory.Functor J Cᵒᵖ) (X : C)
  (τ : (CategoryTheory.Functor.const J).obj (Opposite.op X) ⟶ F) (j : J),
  ↑((CategoryTheory.Limits.compYonedaSectionsEquiv F X).symm τ) j = (τ.app j).unop
-- Mathlib.Order.Hom.Bounded
/-- `id` as a `BotHom`.  -/
BotHom.id : (α : Type u_2) → [inst : Bot α] → BotHom α α
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.domCongr.eq_1 : ∀ (R : Type u_1) (A : Type u_4) {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N] (e : M ≃* N),
  MonoidAlgebra.domCongr R A e =
    { toEquiv := (MonoidAlgebra.mapDomainRingEquiv A e).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, panicking if no such pair exists.
 -/
Std.TreeMap.Raw.getEntryGE! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited (α × β)] → Std.TreeMap.Raw α β cmp → α → α × β
-- Lean.Data.Lsp.Internal
/-- Name of the module that this identifier is in.  -/
Lean.Lsp.LeanDeclIdent.module : Lean.Lsp.LeanDeclIdent → Lean.Name
-- Lean.Meta.Tactic.Grind.PropagatorAttr
Lean.Meta.Grind.BuiltinPropagators.up : Lean.Meta.Grind.BuiltinPropagators → Lean.Meta.Grind.PropagatorMap
-- Init.Data.Vector.Attach
/-- A synonym for `xs.map (·.val)`. Mostly this should not be needed by users.
It is introduced as in intermediate step by lemmas such as `map_subtype`,
and is ideally subsequently simplified away by `unattach_attach`.

If not, usually the right approach is `simp [Vector.unattach, -Vector.map_subtype]` to unfold.
 -/
Vector.unattach : {n : ℕ} → {α : Type u_1} → {p : α → Prop} → Vector { x // p x } n → Vector α n
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.dualAnnihilator_iSup_eq : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_3}
  (U : ι → Submodule R M), (⨆ i, U i).dualAnnihilator = ⨅ i, (U i).dualAnnihilator
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
/-- The **Riesz-Markov-Kakutani representation theorem**: given a positive linear functional `Λ`,
the (Bochner) integral of `f` (as a `ℝ`-valued function) with respect to the `rieszMeasure`
associated to `Λ` is equal to `Λ f`.  -/
NNRealRMK.integral_rieszMeasure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] [inst_2 : LocallyCompactSpace X]
  [inst_3 : MeasurableSpace X] [inst_4 : BorelSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal)
  (f : CompactlySupportedContinuousMap X NNReal), ∫ (x : X), ↑(f x) ∂NNRealRMK.rieszMeasure Λ = ↑(Λ f)
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.originalTop.eq_1 : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (Ω : TopologicalSpace.Opens E) (F : Type u_4)
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] (n : ℕ∞),
  TestFunction.originalTop Ω F n =
    ⨆ K,
      ⨆ (K_sub_Ω : ↑K ⊆ ↑Ω),
        TopologicalSpace.coinduced (TestFunction.ofSupportedIn K_sub_Ω) ContDiffMapSupportedIn.topologicalSpace
-- Mathlib.Topology.MetricSpace.IsometricSMul
dist_neg_neg : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoMetricSpace G] [IsIsometricVAdd G G] [IsIsometricVAdd Gᵃᵒᵖ G]
  (a b : G), dist (-a) (-b) = dist a b
-- Mathlib.GroupTheory.GroupAction.SubMulAction
Units.instMulActionSubtypeNeOfNat : (R : Type u_1) →
  (M : Type u_2) → [inst : Monoid R] → [inst_1 : AddCommMonoid M] → [DistribMulAction R M] → MulAction Rˣ { x // x ≠ 0 }
-- Mathlib.Combinatorics.Quiver.Basic
/-- The bijection `(X ⟶ Y) ≃ (op Y ⟶ op X)`.  -/
Quiver.Hom.opEquiv : {V : Type u_1} → [inst : Quiver V] → {X Y : V} → (X ⟶ Y) ≃ (Opposite.op Y ⟶ Opposite.op X)
-- Aesop.Script.SpecificTactics
Aesop.unfoldManyTargetS : (Lean.Name → Option (Option Lean.Name)) → Lean.MVarId → Aesop.ScriptM (Option (Lean.MVarId × Array Lean.Name))
-- Mathlib.Data.Nat.Fib.Basic
Nat.fib_two_mul : ∀ (n : ℕ), Nat.fib (2 * n) = Nat.fib n * (2 * Nat.fib (n + 1) - Nat.fib n)
-- Std.Data.DTreeMap.Raw.Basic
Std.DTreeMap.Raw.instUnion : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Union (Std.DTreeMap.Raw α β cmp)
-- Mathlib.Order.Filter.Cofinite
Function.Surjective.le_map_cofinite : ∀ {α : Type u_2} {β : Type u_3} {f : α → β}, Function.Surjective f → Filter.cofinite ≤ Filter.map f Filter.cofinite
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.NatTrans.prod'_app_snd : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor A B}
  {H K : CategoryTheory.Functor A C} (α : F ⟶ G) (β : H ⟶ K) (X : A),
  ((CategoryTheory.NatTrans.prod' α β).app X).2 = β.app X
-- Mathlib.Algebra.Group.Units.Equiv
/-- Right addition of an additive unit is a permutation of the underlying type.  -/
AddUnits.addRight : {M : Type u_3} → [inst : AddMonoid M] → AddUnits M → Equiv.Perm M
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.instIsMonHomε : ∀ {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 D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal],
  CategoryTheory.IsMonHom (CategoryTheory.Functor.LaxMonoidal.ε F)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_multiset_count_of_subset : ∀ {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : DecidableEq M] (m : Multiset M) (s : Finset M),
  m.toFinset ⊆ s → m.sum = ∑ i ∈ s, Multiset.count i m • i
-- Mathlib.Topology.Algebra.Monoid
/-- This lemma exists to ensure that we can still do the simplification
`pure_le_nhds_iff` after simplifying with `pure_zero`.  -/
nonneg_nhds_iff : ∀ {X : Type u_5} [inst : TopologicalSpace X] [T1Space X] [inst_2 : Zero X] {b : X}, 0 ≤ nhds b ↔ 0 = b
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph_EulerianCircuit.eq_1 : SimpleGraph.cycleGraph_EulerianCircuit = SimpleGraph.cycleGraph.cycle