mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.Group.List.Basic
AddCommute.list_sum_right : ∀ {M : Type u_4} [inst : AddMonoid M] (l : List M) (y : M), (∀ x ∈ l, AddCommute y x) → AddCommute y l.sum
-- Mathlib.Algebra.Group.Submonoid.Defs
SubmonoidClass.mk_pow : ∀ {M : Type u_5} [inst : Monoid M] {A : Type u_4} [inst_1 : SetLike A M] [inst_2 : SubmonoidClass A M] {S : A} (x : M)
  (hx : x ∈ S) (n : ℕ), ⟨x, hx⟩ ^ n = ⟨x ^ n, ⋯⟩
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pushoutCoconeOfLeftIso_ι_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.IsIso f],
  (CategoryTheory.Limits.pushoutCoconeOfLeftIso f g).ι.app CategoryTheory.Limits.WalkingSpan.left =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) g
-- Mathlib.Order.GameAdd
/-- **Alias** of `Sym2.GameAdd.recursion`.

---

Recursion on the well-founded `Sym2.GameAdd` relation.  -/
Sym2.GameAdd.fix : {α : Type u_1} →
  {rα : α → α → Prop} →
    {C : α → α → Sort u_3} →
      WellFounded rα →
        ((a₁ b₁ : α) → ((a₂ b₂ : α) → Sym2.GameAdd rα s(a₂, b₂) s(a₁, b₁) → C a₂ b₂) → C a₁ b₁) → (a b : α) → C a b
-- Init.Data.UInt.Lemmas
UInt32.le_total : ∀ (a b : UInt32), a ≤ b ∨ b ≤ a
-- Mathlib.Algebra.Group.Hom.Defs
iterate_map_div : ∀ {M : Type u_10} {F : Type u_11} [inst : Group M] [inst_1 : FunLike F M M] [MonoidHomClass F M M] (f : F) (n : ℕ)
  (x y : M), (⇑f)^[n] (x / y) = (⇑f)^[n] x / (⇑f)^[n] y
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.measurePreserving_add_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Add G] [MeasurableAdd G] (μ : MeasureTheory.Measure G)
  [μ.IsAddRightInvariant] (g : G), MeasureTheory.MeasurePreserving (fun x => x + g) μ μ
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.rightHom_inl : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  (S : AddGroupExtension N E G) (n : N), S.rightHom (S.inl n) = 0
-- Mathlib.Order.Basic
Pi.preorder : {ι : Type u_1} → {π : ι → Type u_4} → [(i : ι) → Preorder (π i)] → Preorder ((i : ι) → π i)
-- Mathlib.Topology.Compactness.LocallyCompact
/-- In a (possibly non-Hausdorff) locally compact space, for every compact set `K`,
`𝓝ˢ K` has a basis consisting of compact sets.  -/
IsCompact.nhdsSet_basis_isCompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyCompactSpace X] {K : Set X},
  IsCompact K → (nhdsSet K).HasBasis (fun L => L ∈ nhdsSet K ∧ IsCompact L) id
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.coe_finset_sup : ∀ {ι : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] (f : ι → TopologicalSpace.Closeds α) (s : Finset ι),
  ↑(s.sup f) = s.sup (SetLike.coe ∘ f)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.coe_refl : ∀ (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁], ⇑(AffineEquiv.refl k P₁) = id
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.biproduct_ι_comp_leftDistributor_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] (X : C) (f : J → C) (j : J),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j))
      (CategoryTheory.leftDistributor X f).hom =
    CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j
-- Aesop.RuleTac.RuleTerm
Aesop.instInhabitedRuleTerm : Inhabited Aesop.RuleTerm
-- Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
ProbabilityTheory.BrownianReal.integral_projectiveFamily : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (I : Finset NNReal) (f : (↥I → ℝ) → E),
  ∫ (x : ↥I → ℝ), f x ∂ProbabilityTheory.BrownianReal.projectiveFamily I =
    ∫ (x : EuclideanSpace ℝ ↥I),
      f x.ofLp ∂ProbabilityTheory.multivariateGaussian 0 (ProbabilityTheory.BrownianReal.covMatrix I)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_insertMany_empty_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α]
  [inst_2 : Inhabited α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false →
    (↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty l ⋯)).getKey! k = default
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- **Alias** of `SimpleGraph.maxDegree_of_subsingleton`. -/
SimpleGraph.maxDegree_of_isEmpty : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] [Subsingleton V], G.maxDegree = 0
-- Mathlib.Algebra.Group.Action.Defs
/-- The regular action of a monoid on itself by left addition.

This is promoted to an `AddTorsor` by `addGroup_is_addTorsor`.  -/
AddMonoid.toAddAction : (M : Type u_1) → [inst : AddMonoid M] → AddAction M M
-- Mathlib.Data.Fintype.Pi
Set.iUnion_snoc : ∀ {α : Type u_1} {n : ℕ} (f : Fin n → Set α) (s : Set α), Set.iUnion (Fin.snoc f s) = (⋃ i, f i) ∪ s
-- Mathlib.Algebra.Order.Module.Defs
SMulPosReflectLT.lift : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : SMul α β] [inst_4 : SMul α γ] (f : β → γ) [inst_5 : Zero β] [inst_6 : Zero γ] [SMulPosReflectLT α γ],
  (∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂) → (∀ (a : α) (b : β), f (a • b) = a • f b) → f 0 = 0 → SMulPosReflectLT α β
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
/-- The cardinality of even permutations of given `cycleType`  -/
AlternatingGroup.card_of_cycleType : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : DecidableEq α] (m : Multiset ℕ),
  {g | (↑g).cycleType = m}.card =
    if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card) then
      (Fintype.card α).factorial /
        ((Fintype.card α - m.sum).factorial * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m).factorial))
    else 0
-- Mathlib.Data.Setoid.Basic
Setoid.comap_surjective : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Function.Injective f → Function.Surjective (Setoid.comap f)
-- Mathlib.Algebra.Order.Monovary
Monovary.nsmul_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {f : ι → α} {g : ι → β}, Monovary f g → ∀ (n : ℕ), Monovary (n • f) g
-- Lean.Compiler.IR.Basic
/-- Constructor information.

   - `name` is the Name of the Constructor in Lean.
   - `cidx` is the Constructor index (aka tag).
   - `size` is the number of arguments of type `object/tobject`.
   - `usize` is the number of arguments of type `usize`.
   - `ssize` is the number of bytes used to store scalar values.

Recall that a Constructor object contains a header, then a sequence of
pointers to other Lean objects, a sequence of `USize` (i.e., `size_t`)
scalar values, and a sequence of other scalar values.  -/
Lean.IR.CtorInfo : Type
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- A concrete counterexample shows that `Continuous.homeoOfEquivCompactToT2`
cannot be generalized from `T2Space` to `T1Space`.

Let `α = OnePoint ℕ` be the one-point compactification of `ℕ`, and let `β` be the same space
`OnePoint ℕ` with the cofinite topology.  Then `α` is compact, `β` is T1, and the identity map
`id : α → β` is a continuous equivalence that is not a homeomorphism.
 -/
Continuous.homeoOfEquivCompactToT2.t1_counterexample : ∃ α β x x_1, CompactSpace α ∧ T1Space β ∧ ∃ f, Continuous ⇑f ∧ ¬Continuous ⇑f.symm
-- Mathlib.RingTheory.PowerBasis
PowerBasis.dim_pos : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] [Nontrivial S]
  (pb : PowerBasis R S), 0 < pb.dim
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.univ_pow : ∀ {α : Type u_2} [inst : Monoid α] {n : ℕ}, n ≠ 0 → Set.univ ^ n = Set.univ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey!_eq_back!_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.maxKey! = t.keysArray.back!
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetResult.Ioi : Lean.Term → BigOperators.FinsetResult✝
-- Batteries.Tactic.Case
/-- Given a `casePattBody`, either give a synthetic hole or a tactic sequence
(along with the syntax for the `=>`).
Converts holes into synthetic holes since they are processed with `elabTermWithHoles`.  -/
Batteries.Tactic.processCasePattBody : Lean.TSyntax `Batteries.Tactic.casePattTac →
  Lean.Elab.Tactic.TacticM (Lean.Term ⊕ Lean.Syntax × Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.Y_eq_of_equiv : ∀ {R : Type r} [inst : CommRing R] {P Q : Fin 3 → R}, P ≈ Q → P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- A non-unital subalgebra is a sub(semi)ring that is also a submodule.  -/
NonUnitalSubalgebra : (R : Type u) → (A : Type v) → [inst : CommSemiring R] → [inst_1 : NonUnitalNonAssocSemiring A] → [Module R A] → Type v
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex
MvPolynomial.degree_degLexDegree : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {f : MvPolynomial σ R} [inst_1 : LinearOrder σ]
  [inst_2 : WellFoundedGT σ], Finsupp.degree (MonomialOrder.degLex.degree f) = f.totalDegree
-- Init.Data.Option.Lemmas
Option.not_rel_some_none : ∀ {α : Type u_1} {β : Type u_2} {a : α} {r : α → β → Prop}, ¬Option.Rel r (some a) none
-- Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
/-- The ramification index of the ideal corresponding to the class of `Q ∈ ℤ[X]` modulo `p` via
`NumberField.Ideal.primesOverSpanEquivMonicFactorsMod` is equal to the multiplicity of `Q mod p` in
`minpoly ℤ θ`.
 -/
NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply : ∀ {K : Type u_1} [inst : Field K] {θ : NumberField.RingOfIntegers K} {p : ℕ} [inst_1 : Fact (Nat.Prime p)]
  [inst_2 : NumberField K] (hp : ¬p ∣ RingOfIntegers.exponent θ) {Q : Polynomial ℤ}
  (hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ RingOfIntegers.monicFactorsMod θ p),
  (↑((NumberField.Ideal.primesOverSpanEquivMonicFactorsMod hp).symm
            ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩)).ramificationIdx
      ℤ =
    multiplicity (Polynomial.map (Int.castRingHom (ZMod p)) Q) (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))
-- Mathlib.Data.Num.Lemmas
PosNum.add_succ : ∀ (m n : PosNum), m + n.succ = (m + n).succ
-- Std.Http.Data.Status
/-- 421 Misdirected Request
 -/
Std.Http.Status.misdirectedRequest : Std.Http.Status
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_sSup : ∀ {s : Set NNReal}, BddAbove s → ↑(sSup s) = ⨆ a ∈ s, ↑a
-- Mathlib.Data.W.Constructions
_private.Mathlib.Data.W.Constructions.0.WType.toNat.match_1.splitter : (motive : WType WType.Natβ → Sort u_1) →
  (x : WType WType.Natβ) →
    ((f : WType.Natβ WType.Natα.zero → WType WType.Natβ) → motive (WType.mk WType.Natα.zero f)) →
      ((f : WType.Natβ WType.Natα.succ → WType WType.Natβ) → motive (WType.mk WType.Natα.succ f)) → motive x
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.MonoidalPreadditive.instAdditiveTensorLeft : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (X : C),
  (CategoryTheory.MonoidalCategory.tensorLeft X).Additive
-- Mathlib.MeasureTheory.Measure.Sub
MeasureTheory.Measure.isFiniteMeasure_sub : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.IsFiniteMeasure (μ - ν)
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_smul_left : ∀ {R : Type u_1} {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11}
  {p : Type u_12} [inst : SMul R α] [inst_1 : SMul R γ] (f : α → β → γ) (r : R),
  (∀ (a : α) (b : β), f (r • a) b = r • f a b) →
    ∀ (A : Matrix l m α) (B : Matrix n p β), Matrix.kroneckerMap f (r • A) B = r • Matrix.kroneckerMap f A B
-- Mathlib.Data.EReal.Operations
EReal.toReal_sub : ∀ {x y : EReal}, x ≠ ⊤ → x ≠ ⊥ → y ≠ ⊤ → y ≠ ⊥ → (x - y).toReal = x.toReal - y.toReal
-- Init.Data.UInt.Lemmas
USize.ofNatLT_le_iff_le : ∀ {a b : ℕ} (ha : a < USize.size) (hb : b < USize.size), USize.ofNatLT a ha ≤ USize.ofNatLT b hb ↔ a ≤ b
-- Init.Data.List.Lemmas
List.flatMap_singleton' : ∀ {α : Type u_1} (l : List α), List.flatMap (fun x => [x]) l = l
-- Mathlib.CategoryTheory.Limits.Lattice
CategoryTheory.Limits.CompleteLattice.hasFiniteLimits_of_semilatticeInf_orderTop : ∀ {α : Type u} [inst : SemilatticeInf α] [OrderTop α], CategoryTheory.Limits.HasFiniteLimits α
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedMonoid.toMulLeftMono : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α], MulLeftMono α
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The faceOppositeCentroid is the centroid of the face opposite to the vertex indexed by `i`.  -/
Affine.Simplex.faceOppositeCentroid : {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] → {n : ℕ} → [NeZero n] → Affine.Simplex k P n → Fin (n + 1) → P
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.alter.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (f : Option (β a) → Option (β a)),
  Std.DHashMap.Internal.AssocList.alter a f Std.DHashMap.Internal.AssocList.nil =
    match f none with
    | none => Std.DHashMap.Internal.AssocList.nil
    | some b => Std.DHashMap.Internal.AssocList.cons a b Std.DHashMap.Internal.AssocList.nil
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Prod.sectR_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (Z : C) (D : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {X Y : D} (f : X ⟶ Y),
  (CategoryTheory.Prod.sectR Z D).map f = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id Z) f
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.enum : Lean.Lsp.CompletionItemKind
-- Std.Http.Protocol.H1
/-- Returns `true` if the reader has completed successfully.
 -/
Std.Http.Protocol.H1.Machine.isReaderComplete : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Bool
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toArray_rcc_eq_zero : ∀ {m n : ℤ} {i : ℕ}, (n + 1 - m).toNat ≤ i → (m...=n).toArray[i]! = 0
-- Mathlib.Analysis.RCLike.Basic
RCLike.nnnorm_conj : ∀ {K : Type u_1} [inst : RCLike K] (z : K), ‖(starRingEnd K) z‖₊ = ‖z‖₊
-- Mathlib.Algebra.Order.Module.Defs
/-- Constructor for `PosSMulMono` when the semimodule is in fact a group.  -/
PosSMulMono.of_smul_nonneg : ∀ {α : Type u_1} {β : Type u_2} [inst : Semiring α] [inst_1 : AddCommGroup β] [inst_2 : Module α β]
  [inst_3 : PartialOrder α] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β],
  (∀ (a : α), 0 ≤ a → ∀ (b : β), 0 ≤ b → 0 ≤ a • b) → PosSMulMono α β
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Cache.Key.mk : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Std.Tactic.BVDecide.BVExpr.Cache.Key
-- Mathlib.Data.Finsupp.Interval
Finsupp.card_Iic : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsBotZeroClass α]
  [inst_3 : OrderBot α] [inst_4 : LocallyFiniteOrder α] [inst_5 : DecidableEq ι] [inst_6 : DecidableEq α] (f : ι →₀ α),
  (Finset.Iic f).card = ∏ i ∈ f.support, (Finset.Iic (f i)).card
-- Init.Data.Slice.Array.Basic
instSliceableSubarrayNat_4 : {α : Type u} → Std.Roo.Sliceable (Subarray α) ℕ (Subarray α)
-- Init.Data.ToString.Name
/-- Creates a round-trippable string name component if possible, otherwise returns `none`.
Names that are valid identifiers are not escaped, and otherwise, if they do not contain `»`, they are escaped.
- If `force` is `true`, then even valid identifiers are escaped.
 -/
Lean.Name.escapePart : String → optParam Bool false → Option String
-- Mathlib.RingTheory.WittVector.MulP
WittVector.wittMulN.eq_2 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ),
  WittVector.wittMulN p n.succ = fun k =>
    (MvPolynomial.bind₁ (Function.uncurry ![WittVector.wittMulN p n, MvPolynomial.X])) (WittVector.wittAdd p k)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
_private.Mathlib.Combinatorics.SimpleGraph.Walk.Traversal.0.SimpleGraph.Walk.getVert.match_1.eq_1 : ∀ {V : Type u_1} {G : SimpleGraph V} {u : V} (motive : (v : V) → G.Walk u v → ℕ → Sort u_2) (x : ℕ)
  (h_1 : (x : ℕ) → motive u SimpleGraph.Walk.nil x)
  (h_2 : (v v_1 : V) → (h : G.Adj u v_1) → (p : G.Walk v_1 v) → motive v (SimpleGraph.Walk.cons h p) 0)
  (h_3 : (v v_1 : V) → (h : G.Adj u v_1) → (q : G.Walk v_1 v) → (n : ℕ) → motive v (SimpleGraph.Walk.cons h q) n.succ),
  (match u, SimpleGraph.Walk.nil, x with
    | .(u), SimpleGraph.Walk.nil, x => h_1 x
    | v, SimpleGraph.Walk.cons h p, 0 => h_2 v v_1 h p
    | v, SimpleGraph.Walk.cons h q, n.succ => h_3 v v_1 h q n) =
    h_1 x
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polarSym2_sym2Mk : ∀ {M : Type u_4} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] (f : M → N) (x y : M),
  QuadraticMap.polarSym2 f s(x, y) = QuadraticMap.polar f x y
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_predicate : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (a : A),
  p (cfc f a)
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.AddConstAsyncResult.constPromise : Lean.Environment.AddConstAsyncResult → IO.Promise Lean.Environment.ConstPromiseVal✝
-- Mathlib.Analysis.Polynomial.MahlerMeasure
/-- The logarithmic Mahler measure of a polynomial is the `log` of the absolute value of its leading
coefficient plus the sum of the `log`s of the absolute values of its roots lying outside the unit
disk.  -/
Polynomial.logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots : ∀ (p : Polynomial ℂ), p.logMahlerMeasure = Real.log ‖p.leadingCoeff‖ + (Multiset.map (fun a => ‖a‖.posLog) p.roots).sum
-- Aesop.RuleTac.RuleTerm
Aesop.ElabRuleTerm.const : Lean.Name → Aesop.ElabRuleTerm
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- This is a linear map version of `SeparatingDual.exists_eq_one` in a projective module.  -/
Module.Projective.exists_dual_eq_one : ∀ {V : Type uV} [inst : AddCommMonoid V] (K : Type u_1) [inst_1 : Semifield K] [inst_2 : Module K V]
  [Module.Projective K V] {x : V}, x ≠ 0 → ∃ f, f x = 1
-- Mathlib.Analysis.Complex.BorelCaratheodory
/-- If `w = z / (2M - z)`, then `z = 2M * w / (1 + w)`. This is the inverse of the
Schwarz transform used in the proof of the Borel-Carathéodory theorem.  -/
_private.Mathlib.Analysis.Complex.BorelCaratheodory.0.Complex.eq_mul_div_one_add_of_eq_div_sub : ∀ {M : ℝ} {z w : ℂ}, M ≠ 0 → 2 * ↑M - z ≠ 0 → w = z / (2 * ↑M - z) → z = 2 * ↑M * w / (1 + w)
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.weakLimit.cone_π : ∀ {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],
  (CategoryTheory.Limits.weakLimit.cone F).π.app = CategoryTheory.Limits.weakLimit.π F
-- Mathlib.Logic.Basic
/-- Swaps two pairs of arguments to a function.  -/
Function.swap₂ : {ι₁ : Sort u_2} →
  {ι₂ : Sort u_3} →
    {κ₁ : ι₁ → Sort u_4} →
      {κ₂ : ι₂ → Sort u_5} →
        {φ : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → Sort u_6} →
          ((i₁ : ι₁) → (j₁ : κ₁ i₁) → (i₂ : ι₂) → (j₂ : κ₂ i₂) → φ i₁ j₁ i₂ j₂) →
            (i₂ : ι₂) → (j₂ : κ₂ i₂) → (i₁ : ι₁) → (j₁ : κ₁ i₁) → φ i₁ j₁ i₂ j₂
-- Init.GrindInstances.ToInt
Lean.Grind.instAddBitVecUint : ∀ {v : ℕ}, Lean.Grind.ToInt.Add (BitVec v) (Lean.Grind.IntInterval.uint v)
-- Mathlib.Analysis.SumIntegralComparisons
/-- Converse to the integral test: a nonnegative, integrable, summable function is integrable.  -/
AntitoneOn.integrableOn_Ioi_of_summable_comp_add : ∀ {f : ℝ → ℝ} {N : ℕ},
  AntitoneOn f (Set.Ici ↑N) →
    (Summable fun n => f ↑(n + N)) →
      (∀ t ∈ Set.Ioi ↑N, 0 ≤ f t) → MeasureTheory.IntegrableOn f (Set.Ioi ↑N) MeasureTheory.volume
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformFun.dist_le : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace β] [inst_1 : BoundedSpace β] {f g : UniformFun α β} {C : ℝ},
  0 ≤ C → (dist f g ≤ C ↔ ∀ (x : α), dist (UniformFun.toFun f x) (UniformFun.toFun g x) ≤ C)
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁'_obj_obj_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (G H : C)
  {X Y : C} (f : X ⟶ Y),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁' C).obj G).obj H).map f =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft H (CategoryTheory.MonoidalCategoryStruct.whiskerRight f G)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.map_comp_map : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g h : α → C}
  [inst_1 : CategoryTheory.Limits.HasProduct f] [inst_2 : CategoryTheory.Limits.HasProduct g]
  [inst_3 : CategoryTheory.Limits.HasProduct h] (q : (a : α) → f a ⟶ g a) (q' : (a : α) → g a ⟶ h a),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map q) (CategoryTheory.Limits.Pi.map q') =
    CategoryTheory.Limits.Pi.map fun a => CategoryTheory.CategoryStruct.comp (q a) (q' a)
-- Std.Time.Format.Basic
Std.Time.FormatType.eq_1 : ∀ (result : Type) (entry : Std.Time.Modifier) (xs : List Std.Time.FormatPart),
  Std.Time.FormatType result (Std.Time.FormatPart.modifier entry :: xs) =
    (Std.Time.TypeFormat entry → Std.Time.FormatType result xs)
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_fst_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] {X A B : C}
  {f : A ⟶ X} {g : B ⟶ X} (a : (F.obj A).obj) (b : (F.obj B).obj)
  (h : (CategoryTheory.ConcreteCategory.hom (F.map f)) a = (CategoryTheory.ConcreteCategory.hom (F.map g)) b),
  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.Limits.pullback.fst f g)))
      ((CategoryTheory.PreGaloisCategory.fiberPullbackEquiv F f g).symm ⟨(a, b), h⟩) =
    a
-- Mathlib.Algebra.Order.Antidiag.Nat
/-- The `Finset` of all `d`-tuples of natural numbers whose product is `n`. Defined to be `∅` when
`n = 0`.  -/
Nat.finMulAntidiag : (d : ℕ) → ℕ → Finset (Fin d → ℕ)
-- Mathlib.Order.LiminfLimsup
Filter.le_limsup_of_le : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {a : α},
  autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) Filter.le_limsup_of_le._auto_1 →
    (∀ (b : α), (∀ᶠ (n : β) in f, u n ≤ b) → a ≤ b) → a ≤ Filter.limsup u f
-- Mathlib.Topology.Algebra.Module.Star
/-- Continuous linear equivalences between modules. We only put the type classes that are necessary
for the definition, although in applications `M` and `M₂` will be topological modules over the
topological semiring `R`.  -/
«term_≃L⋆[_]_» : Lean.TrailingParserDescr
-- Aesop.Rule
Aesop.instLEUnsafeRuleInfo : LE Aesop.UnsafeRuleInfo
-- Mathlib.Order.SemiconjSup
isOrderRightAdjoint_sSup : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteSemilatticeSup α] [inst_1 : Preorder β] (f : α → β),
  IsOrderRightAdjoint f fun y => sSup {x | f x ≤ y}