mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.H1InfRes_X₂ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal],
  (groupCohomology.H1InfRes A S).X₂ = groupCohomology A 1
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- `Set α` is an `AddCommMonoid` under pointwise operations if `α` is.  -/
Set.addCommMonoid : {α : Type u_2} → [AddCommMonoid α] → AddCommMonoid (Set α)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.HasZeroObject.zero_to_zero_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C] (f : 0 ⟶ 0),
  CategoryTheory.IsIso f
-- Mathlib.Logic.Relation
Relation.instIsPreorderReflTransGen : ∀ {α : Type u_1} {r : α → α → Prop}, IsPreorder α (Relation.ReflTransGen r)
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cone.postcomposeComp`.

---

Postcomposing a cone by the composite natural transformation `α ≫ β` is the same as
postcomposing by `α` and then by `β`.  -/
CategoryTheory.Limits.Cones.postcomposeComp : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F G H : CategoryTheory.Functor J C} →
          (α : F ⟶ G) →
            (β : G ⟶ H) →
              CategoryTheory.Limits.Cone.postcompose (CategoryTheory.CategoryStruct.comp α β) ≅
                (CategoryTheory.Limits.Cone.postcompose α).comp (CategoryTheory.Limits.Cone.postcompose β)
-- Mathlib.Data.Rat.Defs
Rat.addLeftCancelSemigroup : AddLeftCancelSemigroup ℚ
-- Init.GrindInstances.ToInt
Lean.Grind.instLTFinCoOfNatIntCast : ∀ {n : ℕ}, Lean.Grind.ToInt.LT (Fin n) (Lean.Grind.IntInterval.co 0 ↑n)
-- Init.Data.List.ToArray
List.setIfInBounds_toArray : ∀ {α : Type u_1} (l : List α) (i : ℕ) (a : α), l.toArray.setIfInBounds i a = (l.set i a).toArray
-- Mathlib.Tactic.Push.Attr
Mathlib.Tactic.Push.instInhabitedHead.default : Mathlib.Tactic.Push.Head
-- Mathlib.Analysis.Analytic.Linear
analyticAt_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {z : E}, AnalyticAt 𝕜 id z
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The composition of `C^n` functions is `C^n`.  -/
ContDiff.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] {n : WithTop ℕ∞} {g : F → G} {f : E → F},
  ContDiff 𝕜 n g → ContDiff 𝕜 n f → ContDiff 𝕜 n (g ∘ f)
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.VersionedHtml.html : ProofWidgets.RefreshComponent.VersionedHtml → ProofWidgets.Html
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
/-- `zero` approximates the zero function.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.zero_approximates : ∀ {basis : Tactic.ComputeAsymptotics.Basis}, Tactic.ComputeAsymptotics.MultiseriesExpansion.zero.Approximates
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.edges_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (p' : G.Walk v w),
  (p.append p').edges = p.edges ++ p'.edges
-- Lean.Elab.MutualInductive
/-- Given a list of `InductiveType` structures and some local variables of `mkInductiveDecl`,
rewrites the inductive types and their constructors in a way that signature contains parameters
representing the types being defined, and all the recursive occurrences of the inductive types
in constructor are replaced by applications of these parameters.

This function is used to implement coinductive predicates. For more details, see the comment in
`Elab.Coinductive`

Upon rewriting the inductive types, it adds the new inductive declaration to the environment,
following the same pattern as `mkInductiveDecl`.

We assume that numVars <= numParams, where numVars is the number of local variables.
 -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.mkFlatInductive : Array Lean.Elab.Command.InductiveView →
  Array Lean.Expr → List Lean.Name → ℕ → ℕ → List Lean.InductiveType → Lean.Elab.TermElabM Unit
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.ofFractionRing_zero : ∀ {K : Type u} [inst : CommRing K], { toFractionRing := 0 } = 0
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
/-- `ContinuousLinearMap.fst` has a continuous right inverse.  -/
ContinuousLinearMap.HasRightInverse.fst : ∀ {R : Type u_1} [inst : Semiring R] {F : Type u_4} {G : Type u_6} [inst_1 : TopologicalSpace F]
  [inst_2 : AddCommMonoid F] [inst_3 : Module R F] [inst_4 : TopologicalSpace G] [inst_5 : AddCommMonoid G]
  [inst_6 : Module R G], (ContinuousLinearMap.fst R F G).HasRightInverse
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.inv_c : ∀ {n : Type u_1} {R : Type u₂} [inst : CommRing R] (t : Matrix.TransvectionStruct n R), t.inv.c = -t.c
-- Mathlib.Topology.Order.LiminfLimsup
/-- If the liminf and the limsup of a filter coincide, then this filter converges to
their common value, at least if the filter is eventually bounded above and below.  -/
le_nhds_of_limsSup_eq_limsInf : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  {f : Filter α} {a : α},
  Filter.IsBounded (fun x1 x2 => x1 ≤ x2) f →
    Filter.IsBounded (fun x1 x2 => x1 ≥ x2) f → f.limsSup = a → f.limsInf = a → f ≤ nhds a
-- Mathlib.Data.Int.Init
Int.strongRec_of_lt : ∀ {m n : ℤ} {motive : ℤ → Sort u_1} {lt : (n : ℤ) → n < m → motive n}
  {ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n} (hn : n < m), Int.strongRec lt ge n = lt n hn
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
LinearIndependent.sum_type : ∀ {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] {v' : ι' → M},
  LinearIndependent R v →
    LinearIndependent R v' →
      Disjoint (Submodule.span R (Set.range v)) (Submodule.span R (Set.range v')) → LinearIndependent R (Sum.elim v v')
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.gcd_self : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (a : R), EuclideanDomain.gcd a a = a
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousOn_iff_preimage_Ioi : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → β} {s : Set α} [inst_1 : Preorder β],
  LowerSemicontinuousOn f s ↔ ∀ (b : β), ∃ u, IsOpen u ∧ s ∩ f ⁻¹' Set.Ioi b = s ∩ u
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `meromorphicAt_comp_add_const_iff_meromorphicAt`

---

`MeromorphicAt` is invariant under translation.  -/
meromorphicAt_fun_comp_add_const_iff_meromorphicAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x c : 𝕜} {f : 𝕜 → E}, MeromorphicAt (fun x => f (x + c)) x ↔ MeromorphicAt f (x + c)
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.SimplicialObject.equivalenceLeftToRight_left_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C)
  (G : CategoryTheory.SimplicialObject.Augmented.toArrow.obj X ⟶ F) (x : SimplexCategoryᵒᵖ),
  (CategoryTheory.SimplicialObject.equivalenceLeftToRight X F G).left.app x =
    CategoryTheory.Limits.WidePullback.lift
      (CategoryTheory.CategoryStruct.comp (X.hom.app x) (CategoryTheory.Arrow.Hom.right G))
      (fun i =>
        CategoryTheory.CategoryStruct.comp (X.left.map ({ len := 0 }.const (Opposite.unop x) i).op)
          (CategoryTheory.Arrow.Hom.left G))
      ⋯
-- Init.Data.BitVec.Lemmas
BitVec.ofBoolListLE.eq_def : ∀ (x : List Bool),
  BitVec.ofBoolListLE x =
    match x with
    | [] => 0#0
    | b :: bs => (BitVec.ofBoolListLE bs).concat b
-- Init.Data.Array.MinMax
Array.min_le_of_mem : ∀ {α : Type u_1} [inst : Min α] [inst_1 : LE α] [Std.IsLinearOrder α] [Std.LawfulOrderMin α] {xs : Array α} {a : α}
  (ha : a ∈ xs), xs.min ⋯ ≤ a
-- Mathlib.Algebra.BigOperators.Finprod
/-- The sum of the constant function `0` over any set equals `0`.  -/
finsum_mem_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (s : Set α), ∑ᶠ (i : α) (_ : i ∈ s), 0 = 0
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.τ₁_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) {G : CategoryTheory.Functor B A}
  (hG : eB.functor.comp e'.inverse ≅ G.comp eA.functor) (η : G.comp F ≅ eB.functor) (X : B),
  (AlgebraicTopology.DoldKan.Compatibility.τ₁ hF hG η).hom.app X =
    CategoryTheory.CategoryStruct.comp (e'.functor.map (hG.hom.app X))
      (CategoryTheory.CategoryStruct.comp (hF.hom.app (G.obj X)) (η.hom.app X))
-- Mathlib.Algebra.Central.TensorProduct
Algebra.TensorProduct.includeLeft_map_center_le : ∀ (K : Type u_1) (B : Type u_2) (C : Type u_3) [inst : CommSemiring K] [inst_1 : Semiring B] [inst_2 : Semiring C]
  [inst_3 : Algebra K B] [inst_4 : Algebra K C],
  Subalgebra.map Algebra.TensorProduct.includeLeft (Subalgebra.center K B) ≤ Subalgebra.center K (TensorProduct K B C)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instZero : {R : Type u_3} → {c₁ c₂ c₃ : R} → [Zero R] → Zero (QuaternionAlgebra R c₁ c₂ c₃)
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun.condIndepFun_prodMk_prodMk : ∀ {Ω : Type u_1} {ι : Type u_2} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {β : ι → Type u_5}
  {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i},
  ProbabilityTheory.iCondIndepFun m' hm' f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k l : ι),
        i ≠ k →
          i ≠ l →
            j ≠ k → j ≠ l → ProbabilityTheory.CondIndepFun m' hm' (fun a => (f i a, f j a)) (fun a => (f k a, f l a)) μ
-- Init.Data.SInt.Lemmas
ISize.sub_sub : ∀ (a b c : ISize), a - b - c = a - (b + c)
-- Init.Data.List.Scan.Lemmas
List.getLast?_scanl : ∀ {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : β → α → β},
  (List.scanl f b l).getLast? = some (List.foldl f b l)
-- Mathlib.Order.LatticeIntervals
Set.Icc.coe_top : ∀ {α : Type u_1} [inst : Preorder α] (a b : α) [inst_1 : Fact (a ≤ b)], ↑⊤ = b
-- Lean.Meta.TryThis
/-- Title of the code action that is displayed in the code action selection dialog.  -/
Lean.Meta.Tactic.TryThis.TryThisInfo.codeActionTitle : Lean.Meta.Tactic.TryThis.TryThisInfo → String
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- A polynomial law `M →ₚₗ[R] N` between `R`-modules is a functorial family of maps
`S ⊗[R] M → S ⊗[R] N`, for all `R`-algebras `S`.

For universe reasons, `S` has to be restricted to the same universe as `R`.  -/
PolynomialLaw : (R : Type u) →
  [inst : CommSemiring R] →
    (M : Type u_1) →
      [inst_1 : AddCommMonoid M] →
        [Module R M] → (N : Type u_2) → [inst_3 : AddCommMonoid N] → [Module R N] → Type (max (max (u + 1) u_1) u_2)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.containsThenInsert.size.eq_1 : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Impl.containsThenInsert.size Std.DTreeMap.Internal.Impl.leaf = 0
-- Mathlib.CategoryTheory.Join.Sum
CategoryTheory.Join.fromSum_map_inr : ∀ (C : Type u_1) {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {d d' : D} (f : d ⟶ d'),
  (CategoryTheory.Join.fromSum C D).map ((CategoryTheory.Sum.inr_ C D).map f) =
    (CategoryTheory.Join.inclRight C D).map f
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- If `S` a finite-dimensional ring extension of a PID `R` which is free as an `R`-module,
then any nonzero `S`-ideal `I` is free as an `R`-submodule of `S`, and we can
find a basis for `S` and `I` such that the inclusion map is a square diagonal
matrix; these are the entries of the diagonal matrix. See :
* `Ideal.ringBasis` for the basis on `S`,
* `Ideal.selfBasis` for the basis on `I`,
* `Ideal.selfBasis_def` for the proof that the inclusion map forms a square diagonal matrix.
 -/
Ideal.smithCoeffs : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      [IsDomain R] →
        [IsPrincipalIdealRing R] →
          {S : Type u_4} →
            [inst_3 : CommRing S] →
              [IsDomain S] → [inst_5 : Algebra R S] → [Finite ι] → Module.Basis ι R S → (I : Ideal S) → I ≠ ⊥ → ι → R
-- Batteries.Data.AssocList
Batteries.AssocList.beq_cons₂ : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} {t : Batteries.AssocList α β} {a' : α} {b' : β}
  {t' : Batteries.AssocList α β} [inst : BEq α] [inst_1 : BEq β],
  (Batteries.AssocList.cons a b t == Batteries.AssocList.cons a' b' t') = (a == a' && b == b' && t == t')
-- Mathlib.RingTheory.Grassmannian
/-- The map on Grassmannians induced by base change along an algebra map `A → B`.
Given a submodule `N` of `A ⊗[R] M`, the image is the kernel of the composition
B ⊗[R] M ≃ B ⊗[A] (A ⊗[R] M) → B ⊗[A] ((A ⊗[R] M) ⧸ N)`.  -/
Module.Grassmannian.map : {R : Type u} →
  [inst : CommRing R] →
    {M : Type v} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {k : ℕ} →
            {A : Type w} →
              [inst_3 : CommRing A] →
                [inst_4 : Algebra R A] →
                  {B : Type w} →
                    [inst_5 : CommRing B] →
                      [inst_6 : Algebra R B] →
                        (A →ₐ[R] B) →
                          Module.Grassmannian A (TensorProduct R A M) k → Module.Grassmannian B (TensorProduct R B M) k
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
/-- The **Riesz-Markov-Kakutani representation theorem**: given a positive linear functional `Λ`,
the (lower) Lebesgue integral of `f` with respect to the `rieszMeasure` associated to `Λ` is equal
to `Λ f`.  -/
NNRealRMK.lintegral_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.CategoryTheory.Monoidal.Closed.InternalCurrying
CategoryTheory.MonoidalClosed.ihomCurry_ihomUncurry_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x y z : C)
  [inst_2 : CategoryTheory.Closed x] [inst_3 : CategoryTheory.Closed y]
  [inst_4 : CategoryTheory.Closed (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)] {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj x y ⟹ z ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.ihomCurry x y z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.ihomUncurry x y z) h) =
    h
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.support_mk'_subset : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {f : (i : ι) → β i} {s : Multiset ι}
  {h : ∀ (i : ι), i ∈ s ∨ f i = 0}, { toFun := f, support' := Trunc.mk ⟨s, h⟩ }.support ⊆ s.toFinset
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.coe_compLeft : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  {γ : Type u_5} [inst_3 : TopologicalSpace γ] [inst_4 : Zero γ] {g : C(β, γ)},
  g 0 = 0 → ∀ (f : CompactlySupportedContinuousMap α β), ⇑(CompactlySupportedContinuousMap.compLeft g f) = ⇑g ∘ ⇑f
-- Mathlib.RingTheory.SimpleModule.IsAlgClosed
/-- The **Wedderburn–Artin Theorem** over algebraically closed fields: a finite-dimensional
semisimple algebra over an algebraically closed field is isomorphic to a product of matrix algebras
over the field.  -/
IsSemisimpleRing.exists_algEquiv_pi_matrix_of_isAlgClosed : ∀ (F : Type u_1) (R : Type u_2) [inst : Field F] [IsAlgClosed F] [inst_2 : Ring R] [inst_3 : Algebra F R]
  [IsSemisimpleRing R] [FiniteDimensional F R],
  ∃ n d, (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (R ≃ₐ[F] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) F)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
/-- The `X`-coordinate of a representative of `2 • P` for a Jacobian point representative `P` on a
Weierstrass curve.  -/
WeierstrassCurve.Jacobian.dblX : {R : Type r} → [CommRing R] → WeierstrassCurve.Jacobian R → (Fin 3 → R) → R
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.mem_range_veblenWith : ∀ {f : Ordinal.{u} → Ordinal.{u}} {o a : Ordinal.{u}},
  Order.IsNormal f → o ≠ 0 → (a ∈ Set.range (Ordinal.veblenWith f o) ↔ ∀ b < o, Ordinal.veblenWith f b a = a)
-- Std.Http.Data.Method
/-- Replace a resource with new data.
Source: https://httpwg.org/specs/rfc9110.html#section-9.3.4
 -/
Std.Http.Method.put : Std.Http.Method
-- Mathlib.Algebra.Category.ModuleCat.Subobject
ModuleCat.wellPowered_moduleCat : ∀ {R : Type u} [inst : Ring R], CategoryTheory.WellPowered.{v, v, max (v + 1) u} (ModuleCat R)
-- Init.Data.Nat.Basic
Nat.blt_eq : ∀ {x y : ℕ}, (x.blt y = true) = (x < y)
-- Mathlib.Combinatorics.Enumerative.Catalan.Tree
BinaryTree.mem_treesOfNumNodesEq : ∀ {x : BinaryTree Unit} {n : ℕ}, x ∈ BinaryTree.treesOfNumNodesEq n ↔ x.numNodes = n
-- Mathlib.Analysis.Convex.StdSimplex
/-- The (sup metric) diameter of a standard simplex is less than or equal to 1.  -/
diam_stdSimplex_le : ∀ {ι : Type u_1} [inst : Fintype ι], Metric.diam (stdSimplex ℝ ι) ≤ 1
-- Std.Time.Format
/-- Parses a `String` and returns a `PlainDateTime`.
 -/
Std.Time.PlainDateTime.fromDateTimeString : String → Except String Std.Time.PlainDateTime
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_apply_ne_zero : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] {s : Set α} {f : α → M} {a : α},
  s.indicator f a ≠ 0 ↔ a ∈ s ∩ Function.support f
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanOrder.instInhabited : {M : Type u_1} → [Inhabited M] → Inhabited (MulArchimedeanOrder M)
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.Hom.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasFiniteProducts C}
  {inst_2 : CategoryTheory.Limits.HasPullbacks C} {X Y : CategoryTheory.Dial C} {x y : X.Hom Y},
  x = y ↔ x.f = y.f ∧ x.F = y.F
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.mk.inj : ∀ {α : Type u_3} {inst : MeasurableSpace α} {M : Type u_4} {inst_1 : AddCommMonoid M} {inst_2 : TopologicalSpace M}
  {measureOf' : Set α → M} {empty' : measureOf' ∅ = 0}
  {not_measurable' : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf' i = 0}
  {m_iUnion' :
    ∀ ⦃f : ℕ → Set α⦄,
      (∀ (i : ℕ), MeasurableSet (f i)) →
        Pairwise (Function.onFun Disjoint f) → HasSum (fun i => measureOf' (f i)) (measureOf' (⋃ i, f i))}
  {measureOf'_1 : Set α → M} {empty'_1 : measureOf'_1 ∅ = 0}
  {not_measurable'_1 : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf'_1 i = 0}
  {m_iUnion'_1 :
    ∀ ⦃f : ℕ → Set α⦄,
      (∀ (i : ℕ), MeasurableSet (f i)) →
        Pairwise (Function.onFun Disjoint f) → HasSum (fun i => measureOf'_1 (f i)) (measureOf'_1 (⋃ i, f i))},
  { measureOf' := measureOf', empty' := empty', not_measurable' := not_measurable', m_iUnion' := m_iUnion' } =
      { measureOf' := measureOf'_1, empty' := empty'_1, not_measurable' := not_measurable'_1,
        m_iUnion' := m_iUnion'_1 } →
    measureOf' = measureOf'_1
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- The dependent version of `MultilinearMap.domDomCongrLinearEquiv`.  -/
MultilinearMap.domDomCongrLinearEquiv' : (R : Type uR) →
  (S : Type uS) →
    {ι : Type uι} →
      (M₁ : ι → Type v₁) →
        (M₂ : Type v₂) →
          [inst : Semiring R] →
            [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
              [inst_2 : (i : ι) → Module R (M₁ i)] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : Module R M₂] →
                    [inst_5 : Semiring S] →
                      [inst_6 : Module S M₂] →
                        [inst_7 : SMulCommClass R S M₂] →
                          {ι' : Type u_1} →
                            (σ : ι ≃ ι') → MultilinearMap R M₁ M₂ ≃ₗ[S] MultilinearMap R (fun i => M₁ (σ.symm i)) M₂
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVUnOp.toString : Std.Tactic.BVDecide.BVUnOp → String
-- Mathlib.Data.Matrix.Basic
/-- Matrices over a Pi type are in canonical bijection with tuples of matrices.  -/
Matrix.piEquiv : {m : Type u_2} →
  {n : Type u_3} → {ι : Type u_14} → {β : ι → Type u_15} → Matrix m n ((i : ι) → β i) ≃ ((i : ι) → Matrix m n (β i))
-- Mathlib.Data.List.OffDiag
List.length_offDiag' : ∀ {α : Type u_1} (l : List α), l.offDiag.length = l.length * (l.length - 1)
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netEntropyInfEntourage.eq_1 : ∀ {X : Type u_1} (T : X → X) (F : Set X) (U : SetRel X X),
  Dynamics.netEntropyInfEntourage T F U = ExpGrowth.expGrowthInf fun n => ↑(Dynamics.netMaxcard T F U n)
-- Aesop.Script.CtorNames
Aesop.CtorNames.mk.inj : ∀ {ctor : Lean.Name} {args : Array Lean.Name} {hasImplicitArg : Bool} {ctor_1 : Lean.Name} {args_1 : Array Lean.Name}
  {hasImplicitArg_1 : Bool},
  { ctor := ctor, args := args, hasImplicitArg := hasImplicitArg } =
      { ctor := ctor_1, args := args_1, hasImplicitArg := hasImplicitArg_1 } →
    ctor = ctor_1 ∧ args = args_1 ∧ hasImplicitArg = hasImplicitArg_1
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.colimitOpIsoOpLimit.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasLimit F],
  CategoryTheory.Limits.colimitOpIsoOpLimit F =
    CategoryTheory.Limits.colimit.isoColimitCocone
      { cocone := (CategoryTheory.Limits.limit.cone F).op, isColimit := (CategoryTheory.Limits.limit.isLimit F).op }
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.write.sizeOf_spec : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : SizeOf Γ] [inst_1 : SizeOf Λ] [inst_2 : SizeOf σ] (a : Γ → σ → Γ)
  (a_1 : Turing.TM1.Stmt Γ Λ σ), sizeOf (Turing.TM1.Stmt.write a a_1) = 1 + sizeOf a_1
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.isGE_iff_isZero_truncLE_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n₀ n₁ : ℤ),
  n₀ + 1 = n₁ → ∀ (X : C), t.IsGE X n₁ ↔ CategoryTheory.Limits.IsZero ((t.truncLE n₀).obj X)
-- Init.WFExtrinsicFix
WellFounded.partialExtrinsicFix₃_eq_apply_of_acc : ∀ {α : Sort u_2} {β : α → Sort u_4} {γ : (a : α) → β a → Sort u_3} {C₃ : (a : α) → (b : β a) → γ a b → Sort u_1}
  [inst : ∀ (a : α) (b : β a) (c : γ a b), Nonempty (C₃ a b c)]
  {R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop}
  {F :
    (a : α) →
      (b : β a) →
        (c : γ a b) → ((a' : α) → (b' : β a') → (c' : γ a' b') → R ⟨a', ⟨b', c'⟩⟩ ⟨a, ⟨b, c⟩⟩ → C₃ a' b' c') → C₃ a b c}
  {a : α} {b : β a} {c : γ a b},
  Acc R ⟨a, ⟨b, c⟩⟩ →
    WellFounded.partialExtrinsicFix₃ R F a b c =
      F a b c fun a_1 b_1 c_1 x => WellFounded.partialExtrinsicFix₃ R F a_1 b_1 c_1
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceFMod : Lean.Meta.Simp.DSimproc