mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Stirling
Stirling.log_stirlingSeq_formula : ∀ (n : ℕ),
  Real.log (Stirling.stirlingSeq n) =
    Real.log ↑n.factorial - 1 / 2 * Real.log (2 * ↑n) - ↑n * Real.log (↑n / Real.exp 1)
-- Mathlib.Topology.Category.LightProfinite.Basic
FintypeCat.toLightProfinite_obj : ∀ (A : FintypeCat), FintypeCat.toLightProfinite.obj A = LightProfinite.of A.obj
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
IsFreeGroupoid.SpanningTree.functorOfMonoidHom_map : ∀ {G : Type u} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G]
  (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G)))
  [inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)]
  {X : Type u_1} [inst_3 : Monoid X] (f : CategoryTheory.End (IsFreeGroupoid.SpanningTree.root'✝ T) →* X) {X_1 Y : G}
  (p : X_1 ⟶ Y),
  (IsFreeGroupoid.SpanningTree.functorOfMonoidHom T f).map p = f (IsFreeGroupoid.SpanningTree.loopOfHom T p)
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.listDecode.eq_5 : ∀ {L : FirstOrder.Language} {α : Type u'} (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
  FirstOrder.Language.BoundedFormula.listDecode (Sum.inr (Sum.inr 1) :: l) =
    if h : 1 ≤ (FirstOrder.Language.BoundedFormula.listDecode l).length then
      FirstOrder.Language.BoundedFormula.sigmaAll (FirstOrder.Language.BoundedFormula.listDecode l)[0] ::
        List.drop 1 (FirstOrder.Language.BoundedFormula.listDecode l)
    else []
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.compl_adjMatrix_eq_adjMatrix_compl : ∀ (α : Type u_1) {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : DecidableEq V]
  [inst_2 : DecidableEq α] [inst_3 : Zero α] [inst_4 : One α],
  (SimpleGraph.adjMatrix α G).compl = SimpleGraph.adjMatrix α Gᶜ
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.ofFixingSubgroup_of_eq_bijective : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s t : Set α} {hst : s = t},
  Function.Bijective ⇑(SubMulAction.ofFixingSubgroup_of_eq M hst)
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_tryCatch_Option_apply_eq : ∀ {α : Type u_1} {post : α → Prop} {epost : Prop} (x : Option α) (h : PUnit.{1} → Option α),
  Std.Internal.Do.wp (MonadExceptOf.tryCatch x h) post epost =
    Std.Internal.Do.wp x post (Std.Internal.Do.wp (h PUnit.unit) post epost)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.ofVal_surjective : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀),
  Function.Surjective WithVal.ofVal
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : ChainComplex C ℕ) [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] {Δ Δ' : SimplexCategoryᵒᵖ}
  (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) {θ : Δ ⟶ Δ'} {Δ'' : SimplexCategory}
  {e : Opposite.unop Δ' ⟶ Δ''} {i : Δ'' ⟶ Opposite.unop A.fst} [inst_3 : CategoryTheory.Epi e]
  [inst_4 : CategoryTheory.Mono i],
  CategoryTheory.CategoryStruct.comp e i = CategoryTheory.CategoryStruct.comp θ.unop A.e →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ) A)
        (AlgebraicTopology.DoldKan.Γ₀.Obj.map K θ) =
      CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i)
        (CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ')
          (CategoryTheory.SimplicialObject.Splitting.IndexSet.mk e))
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
instRepresentablyFlatOpensCarrierMap : ∀ {X Y : TopCat} (f : X ⟶ Y), CategoryTheory.RepresentablyFlat (TopologicalSpace.Opens.map f)
-- Mathlib.Probability.Kernel.CondDistrib
MeasureTheory.Integrable.comp_snd_map_prodMk : ∀ {β : Type u_2} {F : Type u_4} [inst : NormedAddCommGroup F] {mβ : MeasurableSpace β} {Ω : Type u_5}
  {mΩ : MeasurableSpace Ω} (X : Ω → β) {μ : MeasureTheory.Measure Ω} {f : Ω → F},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable (fun x => f x.2) (MeasureTheory.Measure.map (fun ω => (X ω, ω)) μ)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.forget_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat) (F : SheafOfModules R), (SheafOfModules.forget R).obj F = F.val
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
edist_lt_ofReal : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {r : ℝ}, edist x y < ENNReal.ofReal r ↔ dist x y < r
-- Mathlib.Data.Nat.Fib.Basic
Nat.fib_add_one : ∀ {n : ℕ}, n ≠ 0 → Nat.fib (n + 1) = Nat.fib (n - 1) + Nat.fib n
-- Mathlib.Data.Fintype.Pi
Fintype.piFinset_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {δ : α → Type u_4} (f : (i : α) → δ i),
  (Fintype.piFinset fun i => {f i}) = {f}
-- Init.Data.SInt.IntToBitVec
ISize.le_iff_toBitVec64_sle : ∀ {a b : ISize} (h : System.Platform.numBits = 64), a ≤ b ↔ (a.toBitVec64 h).sle (b.toBitVec64 h) = true
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
/-- The subgroup generated by an element.  -/
Subgroup.zpowers : {G : Type u_1} → [inst : Group G] → G → Subgroup G
-- Mathlib.NumberTheory.ModularForms.SlashActions
/-- The constant function 1 is invariant under any element of `SL(2, ℤ)`.  -/
ModularForm.is_invariant_one : ∀ (A : Matrix.SpecialLinearGroup (Fin 2) ℤ), SlashAction.map 0 A 1 = 1
-- Lean.Parser.Tactic
Lean.Parser.Tactic.matchRhs.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Antitone.measurable : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  [inst_2 : TopologicalSpace β] {mβ : MeasurableSpace β} [BorelSpace β] [inst_4 : LinearOrder α] [OrderTopology α]
  [SecondCountableTopology α] [inst : LinearOrder β] [OrderClosedTopology β] {f : β → α}, Antitone f → Measurable f
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- The map on each component.  -/
CategoryTheory.Limits.FormalCoproduct.Hom.φ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : CategoryTheory.Limits.FormalCoproduct C} → (self : X.Hom Y) → (i : X.I) → X.obj i ⟶ Y.obj (self.f i)
-- Mathlib.GroupTheory.OrderOfElement
IsUnit.orderOf_eq_one : ∀ {G : Type u_1} [inst : Monoid G] [Subsingleton Gˣ] {x : G}, IsUnit x → orderOf x = 1
-- Mathlib.Order.WellFoundedSet
Finset.partiallyWellOrderedOn : ∀ {α : Type u_2} {r : α → α → Prop} [Std.Refl r] (s : Finset α), (↑s).PartiallyWellOrderedOn r
-- Std.Http.Protocol.H1.Parser
/-- Parses a request-target URI, up to `limits.maxUriLength` bytes.
Fails with `"uri too long"` if the target exceeds the configured limit.
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.parseURI : Std.Http.Protocol.H1.Config → Std.Internal.Parsec.ByteArray.Parser ByteArray
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.HeadCheck.other.injEq : ∀ (pat pat_1 : Lean.Syntax),
  (Lean.Elab.Term.Quotation.HeadCheck.other pat = Lean.Elab.Term.Quotation.HeadCheck.other pat_1) = (pat = pat_1)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : Option (β k) → Option (β k)},
  (m.alter k f).getKey? k' =
    if (k == k') = true then if (f (m.get? k)).isSome = true then some k else none else m.getKey? k'
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {k k' fallback : α}, cmp k k' = Ordering.eq → t.getKeyD k fallback = t.getKeyD k' fallback
-- Mathlib.Order.FixedPoints
OrderHom.le_gfp : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {a : α}, a ≤ f a → a ≤ OrderHom.gfp f
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.Choice.mk.sizeOf_spec : ∀ (cnstrs : List Lean.Meta.Grind.EMatch.Cnstr) (gen : ℕ) (assignment : Array Lean.Expr)
  (sources : Lean.PHashSet Lean.Meta.Grind.EMatchDiagNode),
  sizeOf { cnstrs := cnstrs, gen := gen, assignment := assignment, sources := sources } =
    1 + sizeOf cnstrs + sizeOf gen + sizeOf assignment + sizeOf sources
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {h_mem : k ∈ t₁ \ t₂}, (t₁ \ t₂).getKey k h_mem = t₁.getKey k ⋯
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- Given a measurable embedding to a Borel space which is also a topological embedding, then the
source space is also a Borel space.  -/
MeasurableEmbedding.borelSpace : ∀ {α : Type u_6} {β : Type u_7} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [inst_2 : MeasurableSpace β]
  [inst_3 : TopologicalSpace β] [hβ : BorelSpace β] {e : α → β},
  MeasurableEmbedding e → Topology.IsInducing e → BorelSpace α
-- Init.Data.Array.Lemmas
Array.all_toList : ∀ {α : Type u_1} {p : α → Bool} {as : Array α}, as.toList.all p = as.all p
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- **Alias** of `SymbolicDynamics.FullShift.finite_setOfPred_pattern_support_eq`.

---

Patterns with support exactly `U` form a finite set.  -/
SymbolicDynamics.FullShift.finite_setOf_pattern_support_eq : ∀ {A : Type u_3} {G : Type u_4} [Finite A] [inst : Inhabited A] (U : Finset G), {p | p.support = U}.Finite
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ : B} (f : b₀ ⟶ b₁),
  (F.mapComp' (CategoryTheory.CategoryStruct.id b₀) f f ⋯).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId b₀).hom (F.map f))
      (CategoryTheory.Bicategory.leftUnitor (F.map f)).hom
-- Mathlib.Algebra.Group.Pointwise.Finset.Interval
Finset.Ioc_add_Ico_subset : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] [inst_2 : DecidableEq α] [AddLeftStrictMono α]
  [AddRightStrictMono α] [inst_5 : LocallyFiniteOrder α] (a b c d : α),
  Finset.Ioc a b + Finset.Ico c d ⊆ Finset.Ioo (a + c) (b + d)
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.MVarValue.expr : Lean.Expr → Aesop.EqualUpToIds.MVarValue
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.card_interedges_finpartition_left : ∀ {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)] {s : Finset α}
  [inst_1 : DecidableEq α] (P : Finpartition s) (t : Finset β),
  (Rel.interedges r s t).card = ∑ a ∈ P.parts, (Rel.interedges r a t).card
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- In the characteristic zero case, the centroid lies in the affine
span if the number of points is `n + 1`.  -/
centroid_mem_affineSpan_of_card_eq_add_one : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} [CharZero k] {s : Finset ι} (p : ι → P) {n : ℕ},
  s.card = n + 1 → Finset.centroid k s p ∈ affineSpan k (Set.range p)
-- Init.Prelude
instInhabitedUInt32 : Inhabited UInt32
-- Mathlib.Logic.Equiv.PartialEquiv
/-- The proposition that elements of `source` are mapped to elements of `target`.  -/
PartialEquiv.map_source' : ∀ {α : Type u_5} {β : Type u_6} (self : PartialEquiv α β) ⦃x : α⦄, x ∈ self.source → ↑self x ∈ self.target
-- Mathlib.Analysis.RCLike.Basic
RCLike.div_im : ∀ {K : Type u_1} [inst : RCLike K] (z w : K),
  RCLike.im (z / w) = RCLike.im z * RCLike.re w / RCLike.normSq w - RCLike.re z * RCLike.im w / RCLike.normSq w
-- Init.Data.SInt.Bitwise
ISize.not_ne_self : ∀ {a : ISize}, ~~~a ≠ a
-- Std.Data.Internal.List.Associative
Std.Internal.List.mem_iff_getEntry?_eq_some : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {p : (a : α) × β a},
  Std.Internal.List.DistinctKeys l → (p ∈ l ↔ Std.Internal.List.getEntry? p.fst l = some p)
-- Lean.SubExpr
/-- Returns true if the selected subexpression is the topmost one.  -/
Lean.SubExpr.isRoot : Lean.SubExpr → Bool
-- Std.Internal.UV.System
Std.Internal.UV.System.UnameInfo.mk : String → String → String → String → Std.Internal.UV.System.UnameInfo
-- Mathlib.RingTheory.Flat.Equalizer
LinearMap.tensorEqLocusInv.eq_1 : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  {P : Type u_5} [inst_7 : AddCommGroup N] [inst_8 : AddCommGroup P] [inst_9 : Module R N] [inst_10 : Module R P]
  (f g : N →ₗ[R] P) [inst_11 : Module.Flat R M],
  LinearMap.tensorEqLocusInv S M f g =
    (((TensorProduct.AlgebraTensorModule.lTensor S M) f).eqLocus
            ((TensorProduct.AlgebraTensorModule.lTensor S M) g)).subtype.codRestrictOfInjective
      ((TensorProduct.AlgebraTensorModule.lTensor S M) (f.eqLocus g).subtype) ⋯ ⋯
-- Mathlib.NumberTheory.Bernoulli
PowerSeries.evalNegHom.eq_1 : ∀ {A : Type u_2} [inst : CommRing A], PowerSeries.evalNegHom = PowerSeries.rescale (-1)
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_ofNatClamp_of_lt : ∀ {n : ℕ} (hn : n < UInt16.size), (UInt16.ofNatClamp n).toBitVec = n#'hn
-- Mathlib.Analysis.Analytic.Composition
/-- Eta-expanded form of `CPolynomialAt.comp`

---

If two functions `g` and `f` are continuously polynomial respectively at `f x` and `x`,
then `g ∘ f` is continuously polynomial at `x`.  -/
CPolynomialAt.fun_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F} {x : E},
  CPolynomialAt 𝕜 g (f x) → CPolynomialAt 𝕜 f x → CPolynomialAt 𝕜 (fun x => g (f x)) x
-- Mathlib.GroupTheory.Subgroup.Center
AddSubgroup.centerCongr_symm_apply_coe : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_2} [inst_1 : AddGroup H] (e : G ≃+ H)
  (s : ↥(AddSubsemigroup.center H)), ↑((AddSubgroup.centerCongr e).symm s) = e.symm ↑s
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- This is not made into a global instance to avoid diamonds.  -/
ValuativeRel.isUniformAddGroup : ∀ (R : Type u_1) [inst : Ring R] [inst_1 : ValuativeRel R], IsUniformAddGroup R
-- Mathlib.Order.Interval.Set.Image
Monotone.mapsTo_Ici : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a : α},
  Monotone f → Set.MapsTo f (Set.Ici a) (Set.Ici (f a))
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.instHasBiproductSigmaFstSndOfBiproduct : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_3} (f : ι → Type u_2) (g : (i : ι) → f i → C)
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBiproduct (g i)] [CategoryTheory.Limits.HasBiproduct fun i => ⨁ g i],
  CategoryTheory.Limits.HasBiproduct fun p => g p.fst p.snd
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.divisionMonoid.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : DivisionMonoid α],
  Finset.divisionMonoid = Function.Injective.divisionMonoid SetLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.mk_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N)
  (hadd : ∀ (x y : M), f (x + y) = f x + f y), { toFun := ⇑f, map_add' := hadd } = f
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- For `f : Lp E p μ`, we can define an element of `Lp E p (μ.restrict s)` by
`(Lp.memLp f).restrict s).toLp f`. This map is non-expansive.  -/
MeasureTheory.norm_Lp_toLp_restrict_le : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure X} (s : Set X) (f : ↥(MeasureTheory.Lp E p μ)), ‖MeasureTheory.MemLp.toLp ↑↑f ⋯‖ ≤ ‖f‖
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toList_rcc' : ∀ {m n k : ℕ}, List.map (fun x => k + x) (m...=n).toList = ((k + m)...=k + n).toList
-- Mathlib.FieldTheory.Normal.Closure
/-- [Stacks Tag 0BMG](https://stacks.math.columbia.edu/tag/0BMG) (When `L` is normal over `K`, this agrees with 0BMG (1) finiteness.) -/
normalClosure.is_finiteDimensional : ∀ (F : Type u_1) (K : Type u_2) (L : Type u_3) [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra F K] [inst_4 : Algebra F L] [FiniteDimensional F K],
  FiniteDimensional F ↥(IntermediateField.normalClosure F K L)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_zero_index : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] {h : α → M → N},
  Finsupp.sum 0 h = 0
-- Std.Data.DTreeMap.Internal.Queries
/-- Returns the value for the key `k`, or `fallback` if such a key does not exist.  -/
Std.DTreeMap.Internal.Impl.Const.getD : {α : Type u} → {δ : Type w} → [Ord α] → (Std.DTreeMap.Internal.Impl α fun x => δ) → α → δ → δ
-- Mathlib.Data.Nat.Factors
_private.Mathlib.Data.Nat.Factors.0.Nat.primeFactorsList.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (k : ℕ) → motive k.succ.succ),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | k.succ.succ => h_3 k) =
    h_2 ()
-- Mathlib.Order.Booleanisation
Booleanisation.lift_le_comp : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {a b : α},
  Booleanisation.lift a ≤ Booleanisation.comp b ↔ Disjoint a b
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
SSet.instRespectsIsoStrongInnerAnodyneExtensions : SSet.strongInnerAnodyneExtensions.RespectsIso
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instNegZeroClass : {G : Type u_1} →
  [inst : TopologicalSpace G] → [inst_1 : NegZeroClass G] → [ContinuousNeg G] → NegZeroClass (SeparationQuotient G)
-- Mathlib.GroupTheory.Coset.Basic
AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] {s t : AddSubgroup α} (H : AddSubgroup α) (h : s ≤ t),
  AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE H h =
    { toFun := Quotient.map' ⇑(AddSubgroup.inclusion h) ⋯, inj' := ⋯ }
-- ProofWidgets.Component.PenroseDiagram
/-- The Penrose substance program.
Note that `embeds` are added lazily at the end.  -/
ProofWidgets.Penrose.DiagramState.sub : ProofWidgets.Penrose.DiagramState → String
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.nonlinearRightInverseOfSurjective_def : ∀ {𝕜 : Type u_5} {𝕜' : Type u_6} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_7} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_8}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [inst_6 : RingHomInvPair σ σ']
  [inst_7 : RingHomIsometric σ] [inst_8 : RingHomIsometric σ'] [inst_9 : CompleteSpace F] [inst_10 : CompleteSpace E]
  (f : E →SL[σ] F) (hsurj : (↑f).range = ⊤), f.nonlinearRightInverseOfSurjective hsurj = Classical.choose ⋯
-- Mathlib.Data.List.Sigma
List.kerase_nil : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α}, List.kerase a [] = []
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- **Alias** of `PathConnectedSpace.of_locallyPathConnectedSpace`. -/
PathConnectedSpace.of_locPathConnectedSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X] [ConnectedSpace X], PathConnectedSpace X
-- Mathlib.Data.ZMod.Basic
ZModModule.char_ne_one : ∀ (n : ℕ) (G : Type u_2) [inst : AddCommGroup G] [Module (ZMod n) G] [Nontrivial G], n ≠ 1
-- Mathlib.Analysis.Real.Pi.Irrational
_private.Mathlib.Analysis.Real.Pi.Irrational.0.cosPoly.eq_1 : cosPoly✝ 0 = 0
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.surjective_χ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C]
  (𝒞 : CategoryTheory.Subobject.Classifier C) {X : C} (φ : X ⟶ 𝒞.Ω), ∃ Z i, ∃ (x : CategoryTheory.Mono i), φ = 𝒞.χ i
-- Mathlib.CategoryTheory.Functor.Basic
CategoryTheory.Functor.id_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D), (CategoryTheory.Functor.id C).comp F = F
-- Mathlib.Algebra.Group.Int.Defs
Int.instAddMonoid : AddMonoid ℤ
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.weightedHomogeneousComponent_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {w : σ → M} (n : M)
  (φ : MvPolynomial σ R) [inst_2 : DecidableEq M],
  (MvPolynomial.weightedHomogeneousComponent w n) φ =
    ∑ d ∈ φ.support with (Finsupp.weight w) d = n, (MvPolynomial.monomial d) (MvPolynomial.coeff d φ)
-- Mathlib.Order.CompleteBooleanAlgebra
CompleteAtomicBooleanAlgebra.iInf_iSup_eq : ∀ {α : Type u} [self : CompleteAtomicBooleanAlgebra α] {ι : Type u} {κ : ι → Type u} (f : (a : ι) → κ a → α),
  ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.findFinIdx?_loop_toArray : ∀ {α : Type u_1} {l' : List α} {p : α → Bool} {j : ℕ} {l : List α} {h : l'.length + j = l.length},
  l' = List.drop j l → Array.findFinIdx?.loop✝ p l.toArray j = List.findFinIdx?.go p l l' j h
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G],
  (CategoryTheory.forget₂ (Rep.{w, u, v} k G) (ModuleCat k)).Additive
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.Rel.below.add_right : ∀ {R : Type u} {X : Type v} [inst : CommRing R]
  {motive : (a a_1 : FreeNonUnitalNonAssocAlgebra R X) → FreeLieAlgebra.Rel R X a a_1 → Prop}
  {a b : FreeNonUnitalNonAssocAlgebra R X} (c : FreeNonUnitalNonAssocAlgebra R X) (a_1 : FreeLieAlgebra.Rel R X a b),
  FreeLieAlgebra.Rel.below a_1 → motive a b a_1 → FreeLieAlgebra.Rel.below ⋯
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.instInnerRegularOfIsHaarMeasureOfCompactSpace : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] [inst_3 : MeasurableSpace G]
  [BorelSpace G] [CompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsMulLeftInvariant]
  [MeasureTheory.IsFiniteMeasureOnCompacts μ], μ.InnerRegular
-- Std.Internal.Parsec.ByteArray
_private.Std.Internal.Parsec.ByteArray.0.Std.Internal.Parsec.ByteArray.digitsCore.go : ByteArray.Iterator → ℕ → ℕ × ByteArray.Iterator
-- Mathlib.Algebra.Order.Antidiag.Prod
/-- See also `Finset.map_prodComm_mulAntidiagonal`.  -/
Finset.HasMulAntidiagonal.map_swap_mulAntidiagonal : ∀ {A : Type u_1} [inst : CommMonoid A] [inst_1 : Finset.HasMulAntidiagonal A] {n : A},
  Finset.map { toFun := Prod.swap, inj' := ⋯ } (Finset.HasMulAntidiagonal.mulAntidiagonal n) =
    Finset.HasMulAntidiagonal.mulAntidiagonal n
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_diff_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  k ∈ t₂ → (t₁ \ t₂).get! k = default
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.quotient.eq_1 : ∀ {G : Type u} (X : Type v) [inst : Group G] [inst_1 : Monoid X] [inst_2 : MulAction X G] (H : Subgroup G)
  [inst_3 : MulAction.QuotientAction X H],
  MulAction.quotient X H = { smul := fun b => Quotient.map' (fun x => b • x) ⋯, mul_smul := ⋯, one_smul := ⋯ }
-- Std.Http.Data.Request
Std.Http.Request.instReprHead : Repr Std.Http.Request.Head