mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Elements
/-- (implementation) A system `(Fi, fi)_i` of elements induces an element in `A(lim_i Fi)`.  -/
CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor C (Type w)} →
      {I : Type u₁} →
        [inst_1 : CategoryTheory.Category.{v₁, u₁} I] →
          [Small.{w, u₁} I] →
            (F : CategoryTheory.Functor I A.Elements) →
              [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I C] →
                [CategoryTheory.Limits.PreservesLimitsOfShape I A] →
                  A.obj (CategoryTheory.Limits.limit (F.comp (CategoryTheory.CategoryOfElements.π A)))
-- Qq.Macro
Qq.Impl.addSyntaxDollar : Lean.Syntax → Lean.Syntax
-- Mathlib.CategoryTheory.Monoidal.Bimod
π_tensor_id_preserves_coequalizer_inv_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {W X Y Z : C} (f g : X ⟶ Y) (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z ⟶ W)
  (wh :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) h =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Z) h),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.coequalizer.π f g) Z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.PreservesCoequalizer.iso (CategoryTheory.MonoidalCategory.tensorRight Z) f g).inv
        (CategoryTheory.Limits.coequalizer.desc h wh)) =
    h
-- Init.Data.Vector.Lemmas
Vector.foldr_empty : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → β} {init : β}, Vector.foldr f init #v[] = init
-- Init.SimpLemmas
Bool.not_true : (!true) = false
-- Mathlib.Data.Set.Card
Set.ncard_coe_finset : ∀ {α : Type u_1} (s : Finset α), (↑s).ncard = s.card
-- Mathlib.Order.Booleanisation
Booleanisation.not_comp_le_lift : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {a b : α}, ¬Booleanisation.comp a ≤ Booleanisation.lift b
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.Measure.eq_of_le_of_isProbabilityMeasure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.IsProbabilityMeasure ν], μ ≤ ν → μ = ν
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.take_isSubwalk_take : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} {n k : ℕ} (p : G.Walk u v), n ≤ k → (p.take n).IsSubwalk (p.take k)
-- Mathlib.Algebra.Group.Defs
AddLeftCancelMonoid.toAddLeftCancelSemigroup : {M : Type u} → [self : AddLeftCancelMonoid M] → AddLeftCancelSemigroup M
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.prod_id' : ∀ {C : Type u₁} [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] {D : Type u₂}
  [inst_1 : CategoryTheory.CategoryStruct.{v₂, u₂} D] (X : C) (Y : D),
  CategoryTheory.CategoryStruct.id (X, Y) = (CategoryTheory.CategoryStruct.id X, CategoryTheory.CategoryStruct.id Y)
-- Init.Data.List.Lemmas
List.eraseDupsBy.loop.eq_def : ∀ {α : Type u_1} (r : α → α → Bool) (a a_1 : List α),
  List.eraseDupsBy.loop r a a_1 =
    match a, a_1 with
    | [], bs => bs.reverse
    | a :: as, bs =>
      match bs.any (r a) with
      | true => List.eraseDupsBy.loop r as bs
      | false => List.eraseDupsBy.loop r as (a :: bs)
-- Mathlib.Order.Hom.Lattice
SupHom.coe_const : ∀ (α : Type u_2) {β : Type u_3} [inst : Max α] [inst_1 : SemilatticeSup β] (b : β),
  ⇑(SupHom.const α b) = Function.const α b
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_map_equiv : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {β : Type u_10}
  [inst_6 : MeasurableSpace β] (e : X ≃ᵐ β) (f : β → E), ∫ᵛ (y : β), f y ∂[B; μ.map ⇑e] = ∫ᵛ (x : X), f (e x) ∂[B; μ]
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.X_add_C : ∀ {R : Type u_1} [inst : Semiring R] (a : R), (Polynomial.X + Polynomial.C a).Splits
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- If `Y` is a zero object, `X ≅ X ⊞ Y` for any `X`.  -/
CategoryTheory.Limits.isoBiprodZero : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} → [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] → CategoryTheory.Limits.IsZero Y → (X ≅ X ⊞ Y)
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree.eq_1 : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R),
  p.totalDegree = p.support.sup fun s => s.sum fun x e => e
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftLeft_succ' : ∀ (m : ℤ) (n : ℕ), m <<< (n + 1) = 2 * m <<< n
-- Mathlib.Analysis.Complex.Trigonometric
Real.neg_one_lt_tanh : ∀ (x : ℝ), -1 < Real.tanh x
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Power.denote.match_3.eq_1 : ∀ (motive : Lean.Grind.CommRing.Power → Sort u_1) (x : Lean.Grind.CommRing.Var) (k : ℕ)
  (h_1 : (x : Lean.Grind.CommRing.Var) → (k : ℕ) → motive { x := x, k := k }),
  (match { x := x, k := k } with
    | { x := x, k := k } => h_1 x k) =
    h_1 x k
-- Mathlib.Data.Multiset.UnionInter
Multiset.inf_eq_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), s ⊓ t = s ∩ t
-- Lean.DocString.Add
/-- Checks that cannot be carried out during elaboration, typically because they require information
that is not yet available.
 -/
Lean.VersoDocResult.deferredChecks : Lean.VersoDocResult → Array Lean.Doc.DeferredCheck
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
/-- `R` is integrally closed iff all integral elements of its fraction field `K`
are also elements of `R`.  -/
isIntegrallyClosed_iff : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_4) [inst_1 : CommRing K] [inst_2 : Algebra R K] [IsFractionRing R K],
  IsIntegrallyClosed R ↔ ∀ {x : K}, IsIntegral R x → ∃ y, (algebraMap R K) y = x
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- A zero morphism `0 : X ⟶ Y` is an isomorphism if and only if
`X` and `Y` are zero objects.
 -/
CategoryTheory.Limits.isIsoZero_iff_source_target_isZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasZeroObject C] (X Y : C),
  CategoryTheory.IsIso 0 ↔ CategoryTheory.Limits.IsZero X ∧ CategoryTheory.Limits.IsZero Y
-- Mathlib.LinearAlgebra.Trace
LinearMap.trace_mul_cycle' : ∀ (R : Type u) [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f g h : M →ₗ[R] M), (LinearMap.trace R M) (f * (g * h)) = (LinearMap.trace R M) (h * (f * g))
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
Complex.polarCoord.eq_1 : Complex.polarCoord = Complex.equivRealProdCLM.toHomeomorph.transOpenPartialHomeomorph polarCoord
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- The functor mapping a profinite group to its underlying profinite space.  -/
ProfiniteGrp.instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap : CategoryTheory.HasForget₂ ProfiniteGrp.{u_1} Profinite
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.deleteEdges_le : ∀ {V : Type u_1} {G : SimpleGraph V} (s : Set (Sym2 V)), G.deleteEdges s ≤ G
-- Mathlib.Analysis.Normed.Group.Bounded
Filter.neg_cobounded : ∀ {E : Type u_2} [inst : SeminormedAddGroup E], -Bornology.cobounded E = Bornology.cobounded E
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.functorToPresheaves_obj_map : ∀ {P : TopCat → Prop} (X : Type (max u w)) {X_1 Y : (CompHausLike P)ᵒᵖ} (f : X_1 ⟶ Y),
  (CompHausLike.LocallyConstant.functorToPresheaves.obj X).map f =
    TypeCat.ofHom fun g => LocallyConstant.comap (TopCat.Hom.hom f.unop.hom) g
-- Mathlib.Data.Finsupp.Basic
Finsupp.sum_equivMapDomain : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_6} [inst : Zero M] [inst_1 : AddCommMonoid N] (f : α ≃ β)
  (l : α →₀ M) (g : β → M → N), (Finsupp.equivMapDomain f l).sum g = l.sum fun a m => g (f a) m
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.liftOrderHom.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {α : Type u_2}
  [inst_3 : PartialOrder α] (f : M → α) (h : ∀ (a b : M), ArchimedeanClass.mk a ≤ ArchimedeanClass.mk b → f a ≤ f b),
  ArchimedeanClass.liftOrderHom f h = { toFun := ArchimedeanClass.lift f ⋯, monotone' := ⋯ }
-- Lean.Data.Json.Printer
Lean.Json.instToFormat : Std.ToFormat Lean.Json
-- Mathlib.Analysis.Normed.Group.Constructions
MulOpposite.nnnorm_op : ∀ {E : Type u_2} [inst : SeminormedAddGroup E] (a : E), ‖MulOpposite.op a‖₊ = ‖a‖₊
-- Mathlib.NumberTheory.NumberField.CMField
/-- All the conjugations of a CM-field over its maximal real subfield are the same.
 -/
NumberField.IsCMField.isConj_eq_isConj : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [NumberField.IsCMField K] {φ ψ : K →+* ℂ}
  {σ τ : Gal(K/↥(NumberField.maximalRealSubfield K))},
  NumberField.ComplexEmbedding.IsConj φ σ → NumberField.ComplexEmbedding.IsConj ψ τ → σ = τ
-- Lean.Parser.Extra
Lean.Parser.withResetCache.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Fin.Fin2
Fin2.IsLT.mk : ∀ {m n : ℕ}, m < n → Fin2.IsLT m n
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.mkOfNatThm? : Lean.Meta.Grind.Arith.Cutsat.ToIntM (Option Lean.Expr)
-- Mathlib.CategoryTheory.Category.Quiv
/-- Construct a bundled `Quiv` from the underlying type and the typeclass.  -/
CategoryTheory.Quiv.of : (C : Type u) → [Quiver C] → CategoryTheory.Quiv
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- Any linear form on a topological vector space over a nontrivially normed field is continuous if
its kernel is closed.  -/
LinearMap.continuous_of_isClosed_ker : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] (l : E →ₗ[𝕜] 𝕜),
  IsClosed ↑l.ker → Continuous ⇑l
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.algebraPolynomial : (R : Type u_4) → [inst : CommSemiring R] → Algebra (Polynomial R) (LaurentPolynomial R)
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.le_iff_deriv : ∀ {f : Ordinal.{u} → Ordinal.{u}}, Order.IsNormal f → ∀ {a : Ordinal.{u}}, f a ≤ a ↔ ∃ o, Ordinal.deriv f o = a
-- Init.BinderPredicates
/-- The syntax category of binder predicates contains predicates like `> 0`, `∈ s`, etc.
(`: t` should not be a binder predicate because it would clash with the built-in syntax for ∀/∃.)
 -/
Lean.Parser.Category.binderPred : Lean.Parser.Category
-- Lean.Data.DeclarationRange
Lean.instDecidableEqDeclarationLocation : DecidableEq Lean.DeclarationLocation
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mem_sInf_arrows : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {s : Set (CategoryTheory.Subgroupoid C)} {c d : C} {p : c ⟶ d},
  p ∈ (sInf s).arrows c d ↔ ∀ S ∈ s, p ∈ S.arrows c d
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.getVert_length_takeUntil : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] {p : G.Walk v w} (h : u ∈ p.support),
  p.getVert (p.takeUntil u h).length = u
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.nnrpow_zero : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] {a : A},
  a ^ 0 = 0
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.mem_bot : ∀ (R : Type u_1) [inst : NonUnitalNonAssocRing R] {x : R}, x ∈ ⊥ ↔ x = 0
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Expand `⟪x - y, x - y⟫_ℝ`  -/
real_inner_sub_sub_self : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F),
  inner ℝ (x - y) (x - y) = inner ℝ x x - 2 * inner ℝ x y + inner ℝ y y
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Subalgebra.map_comap_eq : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (S : Subalgebra R B),
  Subalgebra.map f (Subalgebra.comap f S) = S ⊓ f.range
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go_denote_mem_prefix : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} {assign : α → Bool} {inv : Bool} (aig : Std.Sat.AIG α)
  (distance : ℕ) (input : aig.RefVec w) (curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr) (start : ℕ)
  (hstart : start < aig.decls.size),
  ⟦assign,
      { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go aig input distance curr hcurr s).aig,
        ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧
-- Init.Grind.Ring.Field
Lean.Grind.Field.zpow_add : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {a : α}, a ≠ 0 → ∀ (m n : ℤ), a ^ (m + n) = a ^ m * a ^ n
-- Lean.Meta.Sym.Arith.Types
/-- `CommRing` instance for `type`  -/
Lean.Meta.Sym.Arith.CommRing.commRingInst : Lean.Meta.Sym.Arith.CommRing → Lean.Expr
-- Mathlib.Data.Rat.Lemmas
Rat.den_dvd : ∀ (a b : ℤ), ↑(Rat.divInt a b).den ∣ b
-- Mathlib.RingTheory.Spectrum.Maximal.Basic
MaximalSpectrum.mk.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] (asIdeal asIdeal_1 : Ideal R) (e_asIdeal : asIdeal = asIdeal_1)
  (isMaximal : asIdeal.IsMaximal),
  { asIdeal := asIdeal, isMaximal := isMaximal } = { asIdeal := asIdeal_1, isMaximal := ⋯ }
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.IsFiniteMeasure.mk : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  μ Set.univ < ⊤ → MeasureTheory.IsFiniteMeasure μ
-- Lean.Data.Trie
_private.Lean.Data.Trie.0.Lean.Data.Trie.findPrefix.go : {α : Type} → String → Lean.Data.Trie α → ℕ → Array α
-- Mathlib.Algebra.Group.Defs
AddZero.ext_iff : ∀ {M : Type u_2} {x y : AddZero M}, x = y ↔ Zero.zero = Zero.zero ∧ Add.add = Add.add
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_apply : ∀ {α : Type u_2} {β : Type u_3} {C : β → Type u_7} [inst : (b : β) → SemilatticeInf (C b)]
  [inst_1 : (b : β) → OrderTop (C b)] (s : Finset α) (f : α → (b : β) → C b) (b : β), s.inf f b = s.inf fun a => f a b
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
MulOpposite.unop_list_prod : ∀ {M : Type u_4} [inst : Monoid M] (l : List Mᵐᵒᵖ), MulOpposite.unop l.prod = (List.map MulOpposite.unop l).reverse.prod
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Pullback a `CompleteAtomicBooleanAlgebra` along an injection.  -/
Function.Injective.completeAtomicBooleanAlgebra : {α : Type u} →
  {β : Type v} →
    [inst : Max α] →
      [inst_1 : Min α] →
        [inst_2 : LE α] →
          [inst_3 : LT α] →
            [inst_4 : SupSet α] →
              [inst_5 : InfSet α] →
                [inst_6 : Top α] →
                  [inst_7 : Bot α] →
                    [inst_8 : Compl α] →
                      [inst_9 : HImp α] →
                        [inst_10 : HNot α] →
                          [inst_11 : SDiff α] →
                            [inst_12 : CompleteAtomicBooleanAlgebra β] →
                              (f : α → β) →
                                Function.Injective f →
                                  (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) →
                                    (∀ {x y : α}, f x < f y ↔ x < y) →
                                      (∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) →
                                        (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) →
                                          (∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) →
                                            (∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) →
                                              f ⊤ = ⊤ →
                                                f ⊥ = ⊥ →
                                                  (∀ (a : α), f aᶜ = (f a)ᶜ) →
                                                    (∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) →
                                                      (∀ (a : α), f (￢a) = ￢f a) →
                                                        (∀ (a b : α), f (a \ b) = f a \ f b) →
                                                          CompleteAtomicBooleanAlgebra α
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.comap_equiv_eq_map_symm : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : N ≃* G) (K : Subgroup G),
  Subgroup.comap (↑f) K = Subgroup.map (↑f.symm) K
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
ContinuousMultilinearMap.changeOriginSeries_support : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [inst_3 : (i : ι) → NormedAddCommGroup (E i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_5 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) {k l : ℕ},
  k + l ≠ Fintype.card ι → f.toFormalMultilinearSeries.changeOriginSeries k l = 0
-- Mathlib.RingTheory.Regular.Free
Module.free_quotSMulTop_iff_free : ∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.FinitePresentation R M] {x : R},
  x ∈ ⊥.jacobson → IsSMulRegular M x → (Module.Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M) ↔ Module.Free R M)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.shiftFunctorZero_op_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ),
  (CategoryTheory.shiftFunctorZero Cᵒᵖ ℤ).hom.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C 0 0 ⋯).hom.app X)
      ((CategoryTheory.shiftFunctorZero C ℤ).inv.app (Opposite.unop X)).op
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset_image : ∀ {α : Type u} {β : Type v} {s : Set α} [inst : DecidableEq β] (f : α → β) (hs : s.Finite) (h : (f '' s).Finite),
  h.toFinset = Finset.image f hs.toFinset
-- Mathlib.Combinatorics.Quiver.Path.Vertices
/-- If a composition is `nil`, the left component must be `nil`
(proved via lengths, avoiding dependent pattern-matching).  -/
Quiver.Path.nil_of_comp_eq_nil_left : ∀ {V : Type u_1} [inst : Quiver V] {a b : V} {p : Quiver.Path a b} {q : Quiver.Path b a},
  p.comp q = Quiver.Path.nil → p.length = 0
-- Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
/-- The star algebra homomorphism underlying the instance of the continuous functional
calculus of a Hermitian matrix. This is an auxiliary definition and is not intended
for use outside of this file.  -/
Matrix.IsHermitian.cfcAux : {n : Type u_1} →
  {𝕜 : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : Fintype n] →
        [inst_2 : DecidableEq n] → {A : Matrix n n 𝕜} → A.IsHermitian → C(↑(spectrum ℝ A), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜
-- Mathlib.Data.Seq.Computation
Computation.exists_of_mem_bind : ∀ {α : Type u} {β : Type v} {s : Computation α} {f : α → Computation β} {b : β}, b ∈ s.bind f → ∃ a ∈ s, b ∈ f a
-- Mathlib.Algebra.Group.Defs
/-- Addition is commutative in a commutative additive magma.  -/
AddCommGroup.add_comm : ∀ {G : Type u} [self : AddCommGroup G] (a b : G), a + b = b + a
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
/-- `Z` is the cokernel of `P.complex.X 1 ⟶ P.complex.X 0` when `P : ProjectiveResolution Z`.  -/
CategoryTheory.ProjectiveResolution.isColimitCokernelCofork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {Z : C} → (P : CategoryTheory.ProjectiveResolution Z) → CategoryTheory.Limits.IsColimit P.cokernelCofork
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.ext_iff : ∀ {R : Type u} [inst : NonAssocSemiring R] {S T : Subsemiring R}, S = T ↔ ∀ (x : R), x ∈ S ↔ x ∈ T
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_insertIfNew : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k a : α} {v : β} {h₁ : a ∈ t.insertIfNew k v},
  Std.DTreeMap.Raw.Const.get (t.insertIfNew k v) a h₁ =
    if h₂ : cmp k a = Ordering.eq ∧ k ∉ t then v else Std.DTreeMap.Raw.Const.get t a ⋯
-- Init.Data.List.MinMaxOn
List.minOn?_id : ∀ {α : Type u_1} [inst : Min α] [inst_1 : LE α] [inst_2 : DecidableLE α] [Std.LawfulOrderLeftLeaningMin α]
  {xs : List α}, List.minOn? id xs = xs.min?
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- The unit of an adjunction between `F` and `G`  -/
CategoryTheory.Adjunction.CoreUnitCounit.unit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            CategoryTheory.Adjunction.CoreUnitCounit F G → (CategoryTheory.Functor.id C ⟶ F.comp G)
-- Init.Data.UInt.Lemmas
UInt64.mul_succ : ∀ {a b : UInt64}, a * (b + 1) = a * b + a
-- Mathlib.Order.Filter.Basic
/-- If `f : ι → Filter α` is directed, `α` is not empty, and `∀ i, f i ≠ ⊥`, then `iInf f ≠ ⊥`.
See also `iInf_neBot_of_directed'` for a version assuming `Nonempty ι` instead of `Nonempty α`.  -/
Filter.iInf_neBot_of_directed : ∀ {α : Type u} {ι : Sort x} {f : ι → Filter α} [hn : Nonempty α],
  Directed (fun x1 x2 => x1 ≥ x2) f → (∀ (i : ι), (f i).NeBot) → (iInf f).NeBot
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Real.sigmoid_lt_iff : ∀ {a b : ℝ}, a.sigmoid < b.sigmoid ↔ a < b
-- Mathlib.RingTheory.Smooth.Flat
Algebra.FormallySmooth.flat_of_algHom_of_isNoetherianRing : ∀ {R : Type u_1} {A : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing S] [inst_4 : Algebra R S] (f : S →ₐ[R] A),
  Function.Surjective ⇑f → ∀ [Module.Flat R S] [IsNoetherianRing S] [Algebra.FormallySmooth R A], Module.Flat R A
-- Mathlib.SetTheory.Ordinal.Notation
ONote.addAux.eq_1 : ∀ (e : ONote) (n : ℕ+), e.addAux n ONote.zero = e.oadd n 0
-- Mathlib.Probability.Independence.Integration
ProbabilityTheory.IndepFun.integral_mul_eq_mul_integral : ∀ {Ω : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → 𝕜},
  ProbabilityTheory.IndepFun X Y μ →
    MeasureTheory.AEStronglyMeasurable X μ →
      MeasureTheory.AEStronglyMeasurable Y μ → ∫ (x : Ω), (X * Y) x ∂μ = (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ
-- Lean.Elab.Util
Lean.Elab.syntaxNodeKindOfAttrParam : Lean.Name → Lean.Syntax → Lean.AttrM Lean.SyntaxNodeKind
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.lt_def : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Preorder Y] [inst_2 : Zero Y]
  {D₁ D₂ : Function.locallyFinsuppWithin U Y}, D₁ < D₂ ↔ ⇑D₁ < ⇑D₂
-- Init.Data.Fin.Fold
_private.Init.Data.Fin.Fold.0.Fin.foldrM.loop.eq_def : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (n : ℕ) (f : Fin n → α → m α) (a : { i // i ≤ n })
  (a_1 : α),
  Fin.foldrM.loop✝ n f a a_1 =
    match a, a_1 with
    | ⟨0, property⟩, x => pure x
    | ⟨i.succ, h⟩, x => f ⟨i, h⟩ x >>= Fin.foldrM.loop✝ n f ⟨i, ⋯⟩