mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- An isomorphism of short complexes `S₁ ≅ S₂` induces an isomorphism on the `H` fields
of right homology data of `S₁` and `S₂`.  -/
CategoryTheory.ShortComplex.rightHomologyMapIso' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (S₁ ≅ S₂) → (h₁ : S₁.RightHomologyData) → (h₂ : S₂.RightHomologyData) → h₁.H ≅ h₂.H
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- the unit morphism of a lax monoidal functor  -/
CategoryTheory.Functor.LaxMonoidal.ε : {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) →
              [self : F.LaxMonoidal] →
                CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶
                  F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.null_iff_of_isAddLeftInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : AddGroup G] [IsTopologicalAddGroup G] [μ.IsAddLeftInvariant] [μ.Regular] {s : Set G},
  IsOpen s → (μ s = 0 ↔ s = ∅ ∨ μ = 0)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited γ] {f : α → β → Option γ} {k k' : α},
  m.getKey? k = some k' → (Std.HashMap.filterMap f m)[k]! = (m[k]?.bind (f k')).get!
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.smulZeroClass : {R : Type u_1} →
  {M : Type u_4} → [inst : Semiring R] → {A : Type u_8} → [SMulZeroClass A R] → SMulZeroClass A (MonoidAlgebra R M)
-- Std.Data.ExtDTreeMap.Basic
/-- Carries out a monadic action on each mapping in the tree map in ascending order.  -/
Std.ExtDTreeMap.Const.forMUncurried : {α : Type u} →
  {cmp : α → α → Ordering} →
    {m : Type w → Type w₂} →
      [inst : Monad m] →
        [LawfulMonad m] →
          {β : Type v} →
            [Std.TransCmp cmp] → (α × β → m PUnit.{w + 1}) → Std.ExtDTreeMap α (fun x => β) cmp → m PUnit.{w + 1}
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_top : ∀ {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [inst : SeminormedAddCommGroup F'] [inst_1 : NormedAddCommGroup E'']
  {g' : α → F'} {f'' : α → E''}, f'' =o[⊤] g' ↔ ∀ (x : α), f'' x = 0
-- Init.Omega.Constraint
Lean.Omega.Constraint.flip.eq_1 : ∀ (c : Lean.Omega.Constraint), c.flip = { lowerBound := c.upperBound, upperBound := c.lowerBound }
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.coe_translate : ∀ {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] (f : F)
  [inst_1 : ModularFormClass F Γ k] (g : GL (Fin 2) ℝ), ⇑(ModularForm.translate f g) = SlashAction.map k g ⇑f
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentHighlight.kind? : Lean.Lsp.DocumentHighlight → Option Lean.Lsp.DocumentHighlightKind
-- Mathlib.Data.Sum.Interval
Sum.Lex.Ici_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrderTop α]
  [inst_3 : Fintype β] [inst_4 : LocallyFiniteOrderTop β] (b : β),
  Finset.Ici (Sum.inrₗ b) = Finset.map (Function.Embedding.inr.trans toLex.toEmbedding) (Finset.Ici b)
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.instIsIsoFunctorToRightDerivedZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [CategoryTheory.Limits.PreservesFiniteLimits F], CategoryTheory.IsIso F.toRightDerivedZero
-- Mathlib.Probability.Moments.Tilted
ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_cgf : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} [MeasureTheory.SFinite μ]
  (s : Set Ω),
  MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
    (μ.tilted fun x => t * X x) s = ENNReal.ofReal (∫ (a : Ω) in s, Real.exp (t * X a - ProbabilityTheory.cgf X μ t) ∂μ)
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.triangle_obj₃ : ∀ {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.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  (X : CategoryTheory.Triangulated.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
  (X.triangle f g).obj₃ = X.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ g)
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- If a family is affinely independent, a point in the family is in
the span of some of the points given by a subset of the index type if
and only if that point's index is in the subset, if the underlying
ring is nontrivial.  -/
AffineIndependent.mem_affineSpan_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} [Nontrivial k] {p : ι → P},
  AffineIndependent k p → ∀ (i : ι) (s : Set ι), p i ∈ affineSpan k (p '' s) ↔ i ∈ s
-- Mathlib.Analysis.Calculus.Deriv.AffineMap
AffineMap.hasDerivAtFilter : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) {L : Filter (𝕜 × 𝕜)}, HasDerivAtFilter (⇑f) (f.linear 1) L
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
IsCyclic.image_range_card : ∀ {α : Type u_1} {a : α} [inst : Group α] [inst_1 : Fintype α] [inst_2 : DecidableEq α],
  (∀ (x : α), x ∈ Subgroup.zpowers a) → Finset.image (fun i => a ^ i) (Finset.range (Nat.card α)) = Finset.univ
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
/-- This instance is required to see through the defeq `volume = volume.prod volume`.  -/
instIsAddHaarMeasureProdRealVolume : MeasureTheory.volume.IsAddHaarMeasure
-- Init.Data.Option.Lemmas
Option.guard_eq_ite : ∀ {α : Type u_1} {p : α → Bool} {x : α}, Option.guard p x = if p x = true then some x else none
-- Mathlib.Analysis.CStarAlgebra.Hom
/-- A non-unital star algebra monomorphism of complex C⋆-algebras is isometric.  -/
NonUnitalStarAlgHom.norm_map : ∀ {F : Type u_1} {A : Type u_2} {B : Type u_3} [inst : NonUnitalCStarAlgebra A] [inst_1 : NonUnitalCStarAlgebra B]
  [inst_2 : FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] (φ : F),
  Function.Injective ⇑φ → ∀ (a : A), ‖φ a‖ = ‖a‖
-- Mathlib.Order.CompleteLatticeIntervals
/-- The `sSup` function on a nonempty `OrdConnected` set `s` in a conditionally complete linear
order takes values within `s`, for all nonempty bounded-above subsets of `s`.  -/
sSup_within_of_ordConnected : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} [hs : s.OrdConnected] ⦃t : Set ↑s⦄,
  t.Nonempty → BddAbove t → sSup (Subtype.val '' t) ∈ s
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- An independent set in a graph is a set of vertices that are pairwise not adjacent.  -/
SimpleGraph.IsIndepSet : {α : Type u_1} → SimpleGraph α → Set α → Prop
-- Mathlib.Data.Nat.Nth
Nat.count_nth_of_infinite : ∀ {p : ℕ → Prop} [inst : DecidablePred p], (Set.ofPred p).Infinite → ∀ (n : ℕ), Nat.count p (Nat.nth p n) = n
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLT.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k k_1 : α) (e_k : k = k_1)
  (t t_1 : Std.DTreeMap.Internal.Impl α β) (e_t : t = t_1) (ho : t.Ordered) (he : ∃ a ∈ t, compare a k = Ordering.lt),
  Std.DTreeMap.Internal.Impl.getEntryLT k t ho he = Std.DTreeMap.Internal.Impl.getEntryLT k_1 t_1 ⋯ ⋯
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroupClass.subtype_apply : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_4} {H : S} [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G]
  (x : ↥H), ↑H x = ↑x
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.instFintypeElemSym2EdgeSetFromEdgeSetOfDecidableEq : {V : Type u} → (s : Set (Sym2 V)) → [DecidableEq V] → [Fintype ↑s] → Fintype ↑(SimpleGraph.fromEdgeSet s).edgeSet
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyIsoSc'_hom_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology],
  CategoryTheory.CategoryStruct.comp (K.homologyIsoSc' i j k hi hk).hom (K.sc' i j k).homologyι =
    CategoryTheory.CategoryStruct.comp (K.homologyι j) (K.opcyclesIsoSc' i j k hi hk).hom
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanQueryModuleParams.mk.inj : ∀ {sourceRequestID : Lean.JsonRpc.RequestID} {queries : Array Lean.Lsp.LeanModuleQuery}
  {sourceRequestID_1 : Lean.JsonRpc.RequestID} {queries_1 : Array Lean.Lsp.LeanModuleQuery},
  { sourceRequestID := sourceRequestID, queries := queries } =
      { sourceRequestID := sourceRequestID_1, queries := queries_1 } →
    sourceRequestID = sourceRequestID_1 ∧ queries = queries_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.toCharNeTwoNF_spec : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : Invertible 2],
  (W.toCharNeTwoNF • W).IsCharNeTwoNF
-- Init.Data.Char.Lemmas
Char.ofNat.eq_1 : ∀ (n : ℕ),
  Char.ofNat n =
    if h : n.isValidChar then Char.ofNatAux n h
    else { val := { toBitVec := 0#'Char.ofNat._proof_1 }, valid := Char.ofNat._proof_2 }
-- Mathlib.Algebra.Group.Defs
nsmulBinRec_succ : ∀ {M : Type u_2} [inst : AddSemigroup M] [inst_1 : Zero M] (n : ℕ) (m : M), nsmulBinRec (n + 1) m = nsmulBinRec n m + m
-- Init.Data.SInt.Lemmas
Int32.toInt_div : ∀ (a b : Int32), (a / b).toInt = (a.toInt.tdiv b.toInt).bmod (2 ^ 32)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.A : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.Millisecond.Offset
-- Mathlib.Order.Hom.Lattice
/-- The type of `⊓`-preserving functions from `α` to `β`.  -/
InfHom : (α : Type u_6) → (β : Type u_7) → [Min α] → [Min β] → Type (max u_6 u_7)
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.OplaxTrans.Modification.id_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Lax.OplaxTrans.Modification.id η).app a = CategoryTheory.CategoryStruct.id (η.app a)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k a fallback : α},
      (t.erase k).getKeyD a fallback = if cmp k a = Ordering.eq then fallback else t.getKeyD a fallback
-- Aesop.Rule.Forward
Aesop.ForwardRule.mk.injEq : ∀ (toForwardRuleInfo : Aesop.ForwardRuleInfo) (name : Aesop.RuleName) (term : Aesop.RuleTerm)
  (prio : Aesop.ForwardRulePriority) (toForwardRuleInfo_1 : Aesop.ForwardRuleInfo) (name_1 : Aesop.RuleName)
  (term_1 : Aesop.RuleTerm) (prio_1 : Aesop.ForwardRulePriority),
  ({ toForwardRuleInfo := toForwardRuleInfo, name := name, term := term, prio := prio } =
      { toForwardRuleInfo := toForwardRuleInfo_1, name := name_1, term := term_1, prio := prio_1 }) =
    (toForwardRuleInfo = toForwardRuleInfo_1 ∧ name = name_1 ∧ term = term_1 ∧ prio = prio_1)
-- Mathlib.Topology.UnitInterval
unitInterval.coe_unitIntervalSubmonoid : ↑unitInterval.submonoid = unitInterval
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.LimitPresentation.map_diag : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (P : CategoryTheory.Limits.LimitPresentation J X) {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D)
  [inst_3 : CategoryTheory.Limits.PreservesLimitsOfShape J F], (P.map F).diag = P.diag.comp F
-- Init.Data.UInt.Lemmas
UInt32.ofNatLT_div : ∀ {a b : ℕ} (ha : a < 2 ^ 32) (hb : b < 2 ^ 32), UInt32.ofNatLT (a / b) ⋯ = UInt32.ofNatLT a ha / UInt32.ofNatLT b hb
-- Lean.Meta.Basic
/-- Return the binder information for the given free variable.  -/
Lean.FVarId.getBinderInfo : Lean.FVarId → Lean.MetaM Lean.BinderInfo
-- Mathlib.Algebra.GradedMonoid
SetLike.gMul : {ι : Type u_1} →
  {R : Type u_2} →
    {S : Type u_3} →
      [inst : SetLike S R] →
        [inst_1 : Mul R] → [inst_2 : Add ι] → (A : ι → S) → [SetLike.GradedMul A] → GradedMonoid.GMul fun i => ↥(A i)
-- Init.Data.ByteArray.Bootstrap
List.toByteArray.loop.induct_unfolding : ∀ (motive : List UInt8 → ByteArray → ByteArray → Prop),
  (∀ (r : ByteArray), motive [] r r) →
    (∀ (b : UInt8) (bs : List UInt8) (r : ByteArray),
        motive bs (r.push b) (List.toByteArray.loop bs (r.push b)) →
          motive (b :: bs) r (List.toByteArray.loop bs (r.push b))) →
      ∀ (x : List UInt8) (x_1 : ByteArray), motive x x_1 (List.toByteArray.loop x x_1)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.leadingExp_nil : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil.leadingExp = ⊥
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.isIntegral_of_irreducibleSpace_of_isReduced : ∀ (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsReduced X] [H : IrreducibleSpace ↥X],
  AlgebraicGeometry.IsIntegral X
-- Mathlib.Algebra.Lie.Cochain
LieModule.Cohomology.instLinearMapClassSubtypeLinearMapIdMemSubmoduleTwoCochain : ∀ {R : Type u_1} [inst : CommRing R] {L : Type u_2} [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M],
  LinearMapClass (↥(LieModule.Cohomology.twoCochain R L M)) R L (L →ₗ[R] M)
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.listDecode.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u'} (n₁ : ℕ) (t₁ : L.Term (α ⊕ Fin n₁)) (n₂ : ℕ) (t₂ : L.Term (α ⊕ Fin n₂))
  (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
  FirstOrder.Language.BoundedFormula.listDecode (Sum.inl ⟨n₁, t₁⟩ :: Sum.inl ⟨n₂, t₂⟩ :: l) =
    (if h : n₁ = n₂ then ⟨n₁, FirstOrder.Language.BoundedFormula.equal t₁ (⋯.mp t₂)⟩ else default) ::
      FirstOrder.Language.BoundedFormula.listDecode l
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsNonloop.mk : ∀ {α : Type u_1} {M : Matroid α} {e : α}, ¬M.IsLoop e → e ∈ M.E → M.IsNonloop e
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.then_gt : ∀ (o : Ordering), ¬o.then Ordering.gt = Ordering.eq
-- Init.Data.BitVec.Lemmas
BitVec.toNat_of_zero_length : ∀ {w : ℕ}, w = 0 → ∀ (x : BitVec w), x.toNat = 0
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.upperCentralSeries_zero`. -/
upperCentralSeries_zero : ∀ (G : Type u_1) [inst : Group G], Subgroup.upperCentralSeries G 0 = ⊥
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.functoriality_map_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C)
  (G : CategoryTheory.Functor C D) {Y X : CategoryTheory.Limits.Cocone F} (f : Y ⟶ X),
  ((CategoryTheory.Limits.Cocone.functoriality F G).map f).hom = G.map f.hom
-- Std.Http.Data.Status
Std.Http.Status.expectationFailed.sizeOf_spec : sizeOf Std.Http.Status.expectationFailed = 1
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.instIteratorLoop.loop.congr_simp : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  {n : Type u → Type w} [inst_2 : Monad n] (γ : Type u) (Pl : α → γ → ForInStep γ → Prop) (LargeEnough : α → Prop)
  (hl : ∀ (a b : α), Std.PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b) (acc acc_1 : γ),
  acc = acc_1 →
    ∀ (next next_1 : α) (e_next : next = next_1) (h : LargeEnough next)
      (f f_1 : (out : α) → LargeEnough out → (c : γ) → n (Subtype (Pl out c))),
      f = f_1 →
        Std.Rxi.Iterator.instIteratorLoop.loop γ Pl LargeEnough hl acc next h f =
          Std.Rxi.Iterator.instIteratorLoop.loop γ Pl LargeEnough hl acc_1 next_1 ⋯ f_1
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.eval₂_evalRingHom : ∀ {R : Type u_1} [inst : CommSemiring R] (x : R), Polynomial.eval₂ (Polynomial.evalRingHom x) = Polynomial.evalEval x
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instUniqueBot : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → Unique ↥⊥
-- Mathlib.Data.Fintype.CardEmbedding
_private.Mathlib.Data.Fintype.CardEmbedding.0.«term‖_‖» : Lean.ParserDescr
-- Mathlib.Data.Multiset.MapFold
/-- If each element of `s : Multiset α` can be lifted to `β`, then `s` can be lifted to
`Multiset β`.  -/
Multiset.canLift : ∀ {α : Type u_1} {β : Type v} (c : β → α) (p : α → Prop) [CanLift α β c p],
  CanLift (Multiset α) (Multiset β) (Multiset.map c) fun s => ∀ x ∈ s, p x
-- Init.Notation
/-- `p,*` is shorthand for `sepBy(p, ",")`. It parses 0 or more occurrences of
`p` separated by `,`, that is: `empty | p | p,p | p,p,p | ...`.

It produces a `nullNode` containing a `SepArray` with the interleaved parser
results. It has arity 1, and auto-groups its component parser if needed.
 -/
«stx_,*» : Lean.TrailingParserDescr
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_eq_of_contains : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  (↑m).WF → ∀ {k fallback : α}, m.contains k = true → m.getKeyD k fallback = k
-- Mathlib.Order.Preorder.Finite
Set.Finite.exists_minimalFor : ∀ {ι : Type u_1} {α : Type u_2} [inst : LE α] [IsTrans α fun a a_1 => a_1 ≤ a] (f : ι → α) (s : Set ι),
  s.Finite → s.Nonempty → ∃ i, MinimalFor (fun x => x ∈ s) f i
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.SignedMeasure.instIsFiniteMeasureTotalVariation : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α),
  MeasureTheory.IsFiniteMeasure s.totalVariation
-- Init.Data.List.Find
List.findIdx.eq_1 : ∀ {α : Type u} (p : α → Bool) (l : List α), List.findIdx p l = List.findIdx.go p l 0
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.reverse.match_1.eq_1 : ∀ (motive : (x : ℕ) → BitVec x → Sort u_1) (x : BitVec 0) (h_1 : (x : BitVec 0) → motive 0 x)
  (h_2 : (w : ℕ) → (x : BitVec (w + 1)) → motive w.succ x),
  (match 0, x with
    | 0, x => h_1 x
    | w.succ, x => h_2 w x) =
    h_1 x
-- Mathlib.Algebra.Ring.BooleanRing
/-- Order isomorphism between `α` considered as a Boolean ring considered as a Boolean algebra and
`α`.  -/
OrderIso.asBoolAlgAsBoolRing : (α : Type u_4) → [inst : BooleanAlgebra α] → AsBoolAlg (AsBoolRing α) ≃o α
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addIndex_pos : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  (K : TopologicalSpace.PositiveCompacts G) {V : Set G},
  (interior V).Nonempty → 0 < MeasureTheory.Measure.haar.addIndex (↑K) V
-- Init.Control.MonadAttach
WeaklyLawfulMonadAttach.mk : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : MonadAttach m],
  (∀ {α : Type u} {x : m α}, Subtype.val <$> MonadAttach.attach x = x) → WeaklyLawfulMonadAttach m
-- Mathlib.Logic.Function.FiberPartition
Function.Fiber.mk_image : ∀ {Y : Type u_2} {Z : Type u_3} (f : Y → Z) (y : Y), Function.Fiber.image f (Function.Fiber.mk f y) = f y
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.mk : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} →
              {X₁ Y₁ : C₁} →
                {f₁ : X₁ ⟶ Y₁} →
                  {X₂ Y₂ : C₂} →
                    {f₂ : X₂ ⟶ Y₂} →
                      (pt : C₃) →
                        (inl : (F.obj Y₁).obj X₂ ⟶ pt) →
                          (inr : (F.obj X₁).obj Y₂ ⟶ pt) →
                            CategoryTheory.IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) inl inr →
                              (ι : pt ⟶ (F.obj Y₁).obj Y₂) →
                                autoParam (CategoryTheory.CategoryStruct.comp inl ι = (F.obj Y₁).map f₂)
                                    CategoryTheory.Functor.PushoutObjObj.inl_ι._autoParam →
                                  autoParam (CategoryTheory.CategoryStruct.comp inr ι = (F.map f₁).app Y₂)
                                      CategoryTheory.Functor.PushoutObjObj.inr_ι._autoParam →
                                    F.PushoutObjObj f₁ f₂
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Cell.get?.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : Option ((a : α) × β a) → Sort u_3) →
      (x : Option ((a : α) × β a)) →
        (x = none → motive none) → ((p : (a : α) × β a) → x = some p → motive (some p)) → motive x