mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Preadditive.LeftExact
/-- A functor between preadditive categories preserves all equalizers if it preserves all kernels.
 -/
CategoryTheory.Functor.preservesEqualizers_of_preservesKernels : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [F.PreservesZeroMorphisms] [CategoryTheory.Limits.HasBinaryBiproducts C]
  [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F],
  CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair F
-- Lake.Util.Casing
/-- Converts a snake case, kebab case, or lower camel case `Name` to upper camel case.  -/
Lake.toUpperCamelCase : Lean.Name → Lean.Name
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.hasseDeriv_zero : ∀ {R : Type u_1} [inst : Semiring R] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module R V],
  LaurentSeries.hasseDeriv R 0 = LinearMap.id
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- the structural isomorphism `F.obj fst ≅ G.obj snd`  -/
CategoryTheory.Limits.CategoricalPullback.iso : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                (self : CategoryTheory.Limits.CategoricalPullback F G) → F.obj self.fst ≅ G.obj self.snd
-- Mathlib.Tactic.Conv
/-- The command `#whnfR e` evaluates `e` to Weak Head Normal Form with Reducible transparency,
that is, it uses `whnf` but only unfolding reducible definitions.
 -/
Mathlib.Tactic.Conv.«command#whnfR_» : Lean.ParserDescr
-- Batteries.Tactic.PrintPrefix
/-- Include internal declarations (names starting with `_`, `match_` or `proof_`)
 -/
Batteries.Tactic.PrintPrefixConfig.internals : Batteries.Tactic.PrintPrefixConfig → Bool
-- Init.Data.Option.Basic
/-- A monadic case analysis function for `Option`.

Given a fallback computation for `none` and a monadic operation to apply to the contents of `some`,
`Option.elimM` checks which constructor a given `Option` consists of, and uses the appropriate
argument.

`Option.elimM` can also be seen as a combination of `Option.mapM` and `Option.getDM`. It is a
monadic analogue of `Option.elim`.
 -/
Option.elimM : {m : Type u_1 → Type u_2} → {α β : Type u_1} → [Monad m] → m (Option α) → m β → (α → m β) → m β
-- Lean.Parser.Command
Lean.Parser.Command.omit.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.DirectSum.Internal
/-- Build a `DirectSum.GSemiring` instance for a collection of additive submonoids.  -/
SetLike.gsemiring : {ι : Type u_1} →
  {σ : Type u_2} →
    {R : Type u_4} →
      [inst : AddMonoid ι] →
        [inst_1 : Semiring R] →
          [inst_2 : SetLike σ R] →
            [inst_3 : AddSubmonoidClass σ R] →
              (A : ι → σ) → [SetLike.GradedMonoid A] → DirectSum.GSemiring fun i => ↥(A i)
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.vars_add_of_disjoint : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p q : MvPolynomial σ R} [inst_1 : DecidableEq σ],
  Disjoint p.vars q.vars → (p + q).vars = p.vars ∪ q.vars
-- Lean.Meta.Tactic.Grind.Types
/-- `ematch  -/
Lean.Meta.Grind.NewRawFact.ematchDiagSource : Lean.Meta.Grind.NewRawFact → Lean.Meta.Grind.EMatchDiagSource
-- Mathlib.Order.FixedPoints
OrderHom.map_gfp_comp : ∀ {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : β →o α) (g : α →o β),
  f (OrderHom.gfp (g.comp f)) = OrderHom.gfp (f.comp g)
-- Mathlib.Data.ENNReal.Basic
ENNReal.toNNReal_eq_one_iff : ∀ (x : ENNReal), x.toNNReal = 1 ↔ x = 1
-- Std.Data.DHashMap.Basic
Std.DHashMap.instUnion : {α : Type u} → {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Union (Std.DHashMap α β)
-- Mathlib.Algebra.RingQuot
/-- Given an arbitrary relation `r` on a ring, we strengthen it to a relation `Rel r`,
such that the equivalence relation generated by `Rel r` has `x ~ y` if and only if
`x - y` is in the ideal generated by elements `a - b` such that `r a b`.
 -/
RingQuot.Rel : {R : Type uR} → [Semiring R] → (R → R → Prop) → R → R → Prop
-- Mathlib.RingTheory.Spectrum.Prime.Basic
/-- In a Noetherian integral domain which is not a field, every non-zero ideal contains a non-zero
product of prime ideals; in a field, the whole ring is a non-zero ideal containing only 0 as
product or prime ideals ([samuel1967, § 3.3, Lemma 3])  -/
PrimeSpectrum.exists_primeSpectrum_prod_le_and_ne_bot_of_domain : ∀ {A : Type u} [inst : CommRing A] [IsDomain A] [IsNoetherianRing A],
  ¬IsField A →
    ∀ {I : Ideal A},
      I ≠ ⊥ → ∃ Z, (Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I ∧ (Multiset.map PrimeSpectrum.asIdeal Z).prod ≠ ⊥
-- Mathlib.LinearAlgebra.Matrix.Rank
LinearIndependent.rank_matrix : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : Field R] [inst_2 : Fintype m]
  {M : Matrix m n R}, LinearIndependent R M.row → M.rank = Fintype.card m
-- Init.Data.Float.Model.Float
/-- Returns `true` if the float is positive or negative infinity.
 -/
Float.Model.isInf : Float.Model → Bool
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.XIsoOfEq_inv_comp_XIsoOfEq_inv : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι}
  (h₂₁ : p₂ = p₁) (h₃₂ : p₃ = p₂),
  CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₂₁).inv (K.XIsoOfEq h₃₂).inv = (K.XIsoOfEq ⋯).hom
-- Mathlib.Data.Countable.Defs
not_surjective_countable_uncountable : ∀ {α : Sort u} {β : Sort v} [Countable α] [Uncountable β] (f : α → β), ¬Function.Surjective f
-- Mathlib.Algebra.Order.Group.Multiset
/-- `Multiset.replicate` as an `AddMonoidHom`.  -/
Multiset.replicateAddMonoidHom : {α : Type u_1} → α → ℕ →+ Multiset α
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendBit.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (start : ℕ) (x : aig.RefVec w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendBit aig { start := start, x := x } =
    {
      aig :=
        (Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract aig { w := w, vec := x, start := start }).aig
            { w := 1,
              vec :=
                (Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract aig { w := w, vec := x, start := start }).vec }).aig,
      vec :=
        (Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract aig { w := w, vec := x, start := start }).aig
            { w := 1,
              vec :=
                (Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract aig { w := w, vec := x, start := start }).vec }).vec }
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_diff_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ \ t₂).get? k = none
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.mul_star : ∀ {d x y : ℤ}, { re := x, im := y } * star { re := x, im := y } = ↑x * ↑x - ↑d * ↑y * ↑y
-- Mathlib.Topology.Bases
/-- The image of a topological basis under an open quotient map is a topological basis.  -/
TopologicalSpace.IsTopologicalBasis.isQuotientMap : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_2} [inst_1 : TopologicalSpace Y] {π : X → Y} {V : Set (Set X)},
  TopologicalSpace.IsTopologicalBasis V →
    Topology.IsQuotientMap π → IsOpenMap π → TopologicalSpace.IsTopologicalBasis (Set.image π '' V)
-- Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Submonoid.IsLocalizationMap.map_zero : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoidWithZero N]
  {F : Type u_4} [inst_2 : FunLike F M N] [MulHomClass F M N] {f : F}, S.IsLocalizationMap ⇑f → f 0 = 0
-- Mathlib.NumberTheory.LSeries.RiemannZeta
/-- Riemann zeta functional equation, formulated for `Λ`: for any complex `s` we have
`Λ (1 - s) = Λ s`.  -/
completedRiemannZeta_one_sub : ∀ (s : ℂ), completedRiemannZeta (1 - s) = completedRiemannZeta s
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, (m.erase k).size = if k ∈ m then m.size - 1 else m.size
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Cell.getEntry?.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : Option ((a : α) × β a) → Sort u_3) →
      (x : Option ((a : α) × β a)) → (Unit → motive none) → ((p : (a : α) × β a) → motive (some p)) → motive x
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- The `Aut F` action on the fiber of a connected object is transitive.  -/
CategoryTheory.PreGaloisCategory.FiberFunctor.isPretransitive_of_isConnected : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C)
  [CategoryTheory.PreGaloisCategory.IsConnected X], MulAction.IsPretransitive (CategoryTheory.Aut F) (F.obj X).obj
-- Mathlib.Topology.Algebra.Group.Defs
/-- If a function converges to a value in an additive topological group, then its
negation converges to the negation of this value.  -/
Filter.Tendsto.neg : ∀ {G : Type u_1} {α : Type u_2} [inst : TopologicalSpace G] [inst_1 : Neg G] [ContinuousNeg G] {f : α → G}
  {l : Filter α} {y : G}, Filter.Tendsto f l (nhds y) → Filter.Tendsto (fun x => -f x) l (nhds (-y))
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.instNeg : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) → (M : Type u_4) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Neg (AdicCompletion I M)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.app_one_eq_ι_comp_left : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (s : CategoryTheory.Limits.Fork f g),
  s.π.app CategoryTheory.Limits.WalkingParallelPair.one = CategoryTheory.CategoryStruct.comp s.ι f
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
EReal.tendsto_exp_nhds_zero_nhds_one : Filter.Tendsto EReal.exp (nhds 0) (nhds 1)
-- Mathlib.Algebra.Ring.Defs
mul_add_one : ∀ {α : Type u} [inst : Add α] [inst_1 : MulOneClass α] [LeftDistribClass α] (a b : α), a * (b + 1) = a * b + a
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.zoom_zoomed₁ : ∀ {α : Type u_1} {cut : α → Ordering} {t : RBTree.RBNode α} {path : RBTree.RBNode.Path α} {t' : RBTree.RBNode α}
  {path' : RBTree.RBNode.Path α},
  RBTree.RBNode.zoom cut t path = (t', path') → RBTree.RBNode.OnRoot (fun x => cut x = Ordering.eq) t'
-- Mathlib.Algebra.Group.Equiv.Opposite
AddEquiv.unop.eq_1 : ∀ {α : Type u_3} {β : Type u_4} [inst : Add α] [inst_1 : Add β], AddEquiv.unop = AddEquiv.op.symm
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k k' : α},
      cmp k k' = Ordering.eq →
        ∀ {v : β} [inst : Inhabited β],
          List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l → (k, v) ∈ l → (t.insertMany l)[k']! = v
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorRightUnitor_inv_naturality_assoc : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) {Y : C}
  (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
  [inst_5 : ∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
  (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X X' : CategoryTheory.GradedObject J D) (φ : X ⟶ X')
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj
          ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
      p]
  [inst_7 :
    (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X').obj
          ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
      p]
  {Z : CategoryTheory.GradedObject J D}
  (h : CategoryTheory.GradedObject.mapBifunctorMapObj F p X' ((CategoryTheory.GradedObject.single₀ I).obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp φ
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X').inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GradedObject.mapBifunctorMapMap F p φ
          (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj Y)))
        h)
-- Mathlib.Data.Set.Piecewise
Set.piecewise_mem_pi : ∀ {α : Type u_1} (s : Set α) [inst : (j : α) → Decidable (j ∈ s)] {δ : α → Type u_8} {t : Set α}
  {t' : (i : α) → Set (δ i)} {f g : (i : α) → δ i}, f ∈ t.pi t' → g ∈ t.pi t' → s.piecewise f g ∈ t.pi t'
-- Mathlib.Algebra.Group.Equiv.Defs
/-- See Note [custom simps projection]  -/
MulEquiv.Simps.symm_apply : {M : Type u_4} → {N : Type u_5} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → N → M
-- Lean.Meta.Tactic.Grind.Proof
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.isEqProof : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Algebra.Divisibility.Basic
/-- **Alias** of `dvd_of_eq`. -/
Eq.dvd : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, a = b → a ∣ b
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
MultipliableLocallyUniformly.multipliableLocallyUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  MultipliableLocallyUniformly f → MultipliableLocallyUniformlyOn f s
-- Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition
CategoryTheory.ObjectProperty.instIsStableUnderTransfiniteCompositionOfShapeIsLocal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (J : Type w)
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J],
  P.isLocal.IsStableUnderTransfiniteCompositionOfShape J
-- Mathlib.CategoryTheory.Sites.JointlySurjective
/-- The jointly surjective precoverage in the category of types has the jointly surjective
families as coverings.  -/
CategoryTheory.Types.jointlySurjectivePrecoverage : CategoryTheory.Precoverage (Type u)
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.limsup_const_mul_of_nonneg_of_ne_top : ∀ {α : Type u_3} {f : Filter α} {u : α → EReal} [f.NeBot] {c : EReal},
  0 ≤ c → c ≠ ⊤ → Filter.limsup (fun x => c * u x) f = c * Filter.limsup u f
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.compRight_id : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (B : LinearMap.BilinForm R M), B.compRight LinearMap.id = B
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
ProbabilityTheory.Kernel.instIsMarkovKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (a b : ℕ),
  ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.Kernel.partialTraj κ a b)
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.Strictness.positive : {u : Lean.Level} →
  {α : Q(Type u)} →
    {zα : Q(Zero «$α»)} →
      {e : Q(«$α»)} → {pα : Q(PartialOrder «$α»)} → Q(0 < «$e») → Mathlib.Meta.Positivity.Strictness zα e (some pα)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
CategoryTheory.IsMonHom.Normal.exists_comp_eq_conj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {G H : C} {inst_2 : CategoryTheory.GrpObj G} {inst_3 : CategoryTheory.GrpObj H} (φ : H ⟶ G)
  [self : CategoryTheory.IsMonHom.Normal φ],
  ∃ ψ,
    CategoryTheory.CategoryStruct.comp ψ φ =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G φ)
        (CategoryTheory.GrpObj.conj G)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.not_gt_of_le : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {a b : α},
  Std.PRange.UpwardEnumerable.LE a b → ¬Std.PRange.UpwardEnumerable.LT b a
-- Mathlib.RingTheory.Localization.Defs
/-- Injectivity of a map descends to the map induced on localizations.  -/
IsLocalization.map_injective_of_injective : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
  (Q : Type u_4) [inst_5 : CommSemiring Q] [inst_6 : Algebra P Q],
  Function.Injective ⇑g →
    ∀ [inst_7 : IsLocalization (Submonoid.map g M) Q], Function.Injective ⇑(IsLocalization.map Q g ⋯)
-- Batteries.Data.Array.Scan
Array.scanl_eq_scanl_toList : ∀ {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β} {as : Array α},
  Array.scanl f init as = (List.scanl f init as.toList).toArray
-- Mathlib.Algebra.Torsor.Basic
Equiv.left_vsub_pointReflection : ∀ {G : Type u_3} {P : Type u_4} [inst : AddGroup G] [T : AddTorsor G P] (x y : P),
  x -ᵥ (Equiv.pointReflection x) y = y -ᵥ x
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.dual : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u →
    GaloisConnection (⇑OrderDual.toDual ∘ u ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ l ∘ ⇑OrderDual.ofDual)
-- Init.Data.Fin.Fold
/-- Inner loop for `Fin.foldl`. `Fin.foldl.loop n f x i = f (f (f x i) ...) (n-1)`.  -/
Fin.foldl.loop : {α : Sort u_1} → (n : ℕ) → (α → Fin n → α) → α → ℕ → α
-- Mathlib.RingTheory.Ideal.Operations
Ideal.top_mul : ∀ {R : Type u} [inst : Semiring R] (I : Ideal R), ⊤ * I = I
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Remove an initial segment of the set that satisfies the predicate `p`.
`p` is required to be antitone, that is, `x < y → p y → p x`.

```
dropWhile (fun x ↦ x < 4) {1, 2, 3, 4, 5} = {4, 5}
dropWhile (fun x ↦ x > 4) {1, 2, 3, 4, 5} = precondition violation
```  -/
Ordnode.dropWhile : {α : Type u_1} → (p : α → Prop) → [DecidablePred p] → Ordnode α → Ordnode α
-- Init.Data.Fin.Lemmas
Fin.is_le : ∀ {n : ℕ} (i : Fin (n + 1)), ↑i ≤ n
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.insertMany.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {ρ : Type w} [inst_1 : ForIn Id ρ ((a : α) × β a)]
  (t : Std.DTreeMap.Internal.Impl α β) (l l_1 : ρ), l = l_1 → ∀ (h : t.Balanced), t.insertMany l h = t.insertMany l_1 h
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.fintypePowers.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] {a : M} [inst_1 : Fintype M],
  Submonoid.fintypePowers =
    {
      elems :=
        { val := Multiset.pmap Subtype.mk (Finset.filter (Membership.mem (Submonoid.powers a)) Finset.univ).val ⋯,
          nodup := ⋯ },
      complete := ⋯ }
-- Mathlib.CategoryTheory.Abelian.Preradical.Basic
CategoryTheory.Abelian.Preradical.instIsIsoAppιObjROfIsIdempotent : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.Abelian.Preradical C) [Φ.IsIdempotent]
  (X : C), CategoryTheory.IsIso (Φ.ι.app (Φ.r.obj X))
-- Mathlib.Analysis.Distribution.TestFunction
/-- The canonical LF topology on `𝓓^{n}(Ω, F)`. This makes `𝓓^{n}(Ω, F)` the inductive
limit of the `𝓓^{n}_{K}(E, F)`s **in the category of locally convex topological vector spaces**
(over ℝ). See `TestFunction.continuous_iff_continuous_comp` for the corresponding universal
property.

More concretely, this is defined as the infimum of *all* locally convex topologies which are
coarser than the "original topology" `TestFunction.originalTop`, which corresponds to taking
the inductive limit in the category of topological spaces.  -/
TestFunction.topologicalSpace : {E : Type u_3} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      (Ω : TopologicalSpace.Opens E) →
        (F : Type u_4) →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] → (n : ℕ∞) → TopologicalSpace (TestFunction Ω F n)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableOn_iff_integrable_of_support_subset : ∀ {α : Type u_1} {mα : MeasurableSpace α} {s : Set α} {μ : MeasureTheory.Measure α} {ε' : Type u_7}
  [inst : TopologicalSpace ε'] [inst_1 : ENormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε'] {f : α → ε'},
  Function.support f ⊆ s → (MeasureTheory.IntegrableOn f s μ ↔ MeasureTheory.Integrable f μ)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.smul_testAgainstNN_apply : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] (c : NNReal)
  (μ : MeasureTheory.FiniteMeasure Ω) (f : BoundedContinuousFunction Ω NNReal),
  (c • μ).testAgainstNN f = c • μ.testAgainstNN f
-- Init.Core
iff_of_false : ∀ {a b : Prop}, ¬a → ¬b → (a ↔ b)
-- Mathlib.Order.Fin.Basic
Fin.succAbove_le_succAbove_iff : ∀ {n : ℕ} {p : Fin (n + 1)} {i j : Fin n}, p.succAbove i ≤ p.succAbove j ↔ i ≤ j
-- Mathlib.CategoryTheory.Subterminal
/-- An object `A` is subterminal iff for any `Z`, there is at most one morphism `Z ⟶ A`.  -/
CategoryTheory.IsSubterminal : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → Prop
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
/-- A modification `Γ` between lax natural transformations `η` and `θ` (between lax functors)
consists of a family of 2-morphisms `Γ.app a : η.app a ⟶ θ.app a`, which satisfies the equation
`(app a ▷ G.map f) ≫ θ.naturality f = η.naturality f ≫ (F.map f ◁ app b)`
for each 1-morphism `f : a ⟶ b`.
 -/
CategoryTheory.Lax.LaxTrans.Modification : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} → (F ⟶ G) → (F ⟶ G) → Type (max u₁ w₂)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_eq_one_of_unique : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] [Nonempty α] [Subsingleton α], Ordinal.type r = 1
-- Mathlib.Control.LawfulFix
LawfulFix.toFix : {α : Type u_3} → {inst : OmegaCompletePartialOrder α} → [self : LawfulFix α] → Fix α
-- Mathlib.Analysis.Analytic.Constructions
AnalyticAt.add : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {x : E},
  AnalyticAt 𝕜 f x → AnalyticAt 𝕜 g x → AnalyticAt 𝕜 (f + g) x
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.functor_obj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C] (X Y : C),
  (CategoryTheory.Limits.prod.functor.obj X).obj Y = (X ⨯ Y)
-- Aesop.Builder.Unfold
Aesop.RuleBuilder.checkUnfoldableConst : Lean.Name → Lean.MetaM (Option Lean.Name)
-- Mathlib.Data.ZMod.Basic
ZMod.coe_intCast : ∀ {n : ℕ} (a : ℤ), (↑a).cast = a % ↑n
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.eq_zero_of_not_le' : ∀ {𝕜 : Type u_7} {α : Type u_8} [inst : Zero 𝕜] [inst_1 : LE α] (self : IncidenceAlgebra 𝕜 α) ⦃a b : α⦄,
  ¬a ≤ b → self.toFun a b = 0
-- Mathlib.Topology.UnitInterval
unitInterval.mul_le_left : ∀ {x y : ↑unitInterval}, x * y ≤ x