mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.infEDist_vadd : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {M : Type u_2} [inst_1 : VAdd M α] [IsIsometricVAdd M α] (c : M) (x : α)
  (s : Set α), Metric.infEDist (c +ᵥ x) (c +ᵥ s) = Metric.infEDist x s
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv.shutdown : {β : Type} → Std.Http.Server.Connection.Recv✝ β
-- Mathlib.Logic.Function.Iterate
List.foldr_const : ∀ {α : Type u} {β : Type v} (f : β → β) (b : β) (l : List α), List.foldr (fun x => f) b l = f^[l.length] b
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.sum'_indep_iff : ∀ {α : Type u_1} {ι : Type u_2} {M : ι → Matroid α} {I : Set (ι × α)},
  (Matroid.sum' M).Indep I ↔ ∀ (i : ι), (M i).Indep (Prod.mk i ⁻¹' I)
-- Init.Data.UInt.Lemmas
UInt32.toUInt8_le : ∀ {a b : UInt32}, a.toUInt8 ≤ b.toUInt8 ↔ a % 256 ≤ b % 256
-- Init.Data.Nat.Lemmas
Nat.sub_add_comm : ∀ {n m k : ℕ}, k ≤ n → n + m - k = n - k + m
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.mem_supported : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  {s : Set M} {x : MonoidAlgebra S M}, x ∈ MonoidAlgebra.supported R S s ↔ ↑x.coeff.support ⊆ s
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.modify : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      [Hashable α] →
        [LawfulBEq α] → Std.DHashMap.Internal.Raw₀ α β → (a : α) → (β a → β a) → Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.nsmul_apply : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → AddMonoid (R i)] [inst_2 : ∀ (i : ι), AddSubmonoidClass (S i) (R i)]
  (x : RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕) (n : ℕ) (i : ι), (n • x) i = n • x i
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.num_one : ∀ {m : Type u_1} [inst : Fintype m] [inst_1 : DecidableEq m], Matrix.num 1 = 1
-- Init.Omega.Int
Lean.Omega.Int.lt_of_gt : ∀ {x y : ℤ}, x > y → y < x
-- Mathlib.Logic.Basic
eq_false_intro : ∀ {a : Prop}, ¬a → a = False
-- Mathlib.RingTheory.FreeCommRing
/-- If α has size at most 1 then the natural map from the free ring on `α` to the
free commutative ring on `α` is an isomorphism of rings.  -/
FreeRing.subsingletonEquivFreeCommRing : (α : Type u) → [Subsingleton α] → FreeRing α ≃+* FreeCommRing α
-- Mathlib.Combinatorics.Optimization.ValuedCSP
/-- Evaluation of a `Γ` term `t` for given solution `x`.  -/
ValuedCSP.Term.evalSolution : {D : Type u_1} →
  {C : Type u_2} →
    [inst : AddCommMonoid C] →
      [inst_1 : PartialOrder C] →
        [inst_2 : IsOrderedAddMonoid C] → {Γ : ValuedCSP D C} → {ι : Type u_3} → Γ.Term ι → (ι → D) → C
-- Lean.Elab.Do.InferControlInfo
Lean.Elab.Do.InferControlInfo.ofLetOrReassignArrow : Bool →
  Lean.TSyntax [`Lean.Parser.Term.doIdDecl, `Lean.Parser.Term.doPatDecl] → Lean.Elab.TermElabM Lean.Elab.Do.ControlInfo
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
/-- If we restrict the distribution of the trajectory up to time `c` to times `≤ b` we get
the trajectory up to time `b`.  -/
ProbabilityTheory.Kernel.partialTraj_map_frestrictLe₂ : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} {b c : ℕ}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (a : ℕ) (hbc : b ≤ c),
  (ProbabilityTheory.Kernel.partialTraj κ a c).map (Preorder.frestrictLe₂ hbc) =
    ProbabilityTheory.Kernel.partialTraj κ a b
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.addPosAssignment.eq_4 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned.addPosAssignment =
  Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {km : α}
  {hc : t.contains km = true}, t.maxKey?.get ⋯ = km → t.getKey km hc = km
-- Init.Data.SInt.Bitwise
Int8.toISize_and : ∀ (a b : Int8), (a &&& b).toISize = a.toISize &&& b.toISize
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.mem_torsionBySet_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set R)
  (x : M), x ∈ Submodule.torsionBySet R M s ↔ ∀ (a : ↑s), ↑a • x = 0
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.module' : {S : Type u'} →
  {R : Type u} →
    {M : Type v} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          {module_M : Module R M} →
            (p : Submodule R M) →
              [inst_2 : Semiring S] → [inst_3 : SMul S R] → [inst_4 : Module S M] → [IsScalarTower S R M] → Module S ↥p
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.add.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α], Finset.add = { add := Finset.image₂ fun x1 x2 => x1 + x2 }
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.instAdd : {R : Type u} →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      {M₂ : Type w₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] →
                    [inst_6 : TopologicalSpace M₂] → [ContinuousAdd M₂] → Add (ContinuousMultilinearMap R M₁ M₂)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α},
      cmp k k' = Ordering.eq →
        List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
          k ∈ List.map Sigma.fst l → (t.insertMany l).getKey! k' = k
-- Mathlib.Logic.Equiv.Fintype
Equiv.Perm.viaFintypeEmbedding_apply_notMem_range : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] (e : Equiv.Perm α) (f : α ↪ β) {b : β},
  b ∉ Set.range ⇑f → (e.viaFintypeEmbedding f) b = b
-- Mathlib.Data.FinEnum
/-- An empty type has a trivial enumeration. Not registered as an instance, to make sure that there
aren't two definitionally differing instances around.  -/
FinEnum.ofIsEmpty : {α : Type u} → [IsEmpty α] → FinEnum α
-- Init.Data.UInt.Lemmas
UInt16.toNat_lt_usizeSize : ∀ (n : UInt16), n.toNat < USize.size
-- Mathlib.Order.JordanHolder
JordanHolderLattice.iso_trans : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {x y z : X × X},
  JordanHolderLattice.Iso x y → JordanHolderLattice.Iso y z → JordanHolderLattice.Iso x z
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Real.BohrMollerup.tendsto_logGammaSeq : ∀ {f : ℝ → ℝ} {x : ℝ},
  ConvexOn ℝ (Set.Ioi 0) f →
    (∀ {y : ℝ}, 0 < y → f (y + 1) = f y + Real.log y) →
      0 < x → Filter.Tendsto (Real.BohrMollerup.logGammaSeq x) Filter.atTop (nhds (f x - f 1))
-- Batteries.Data.Array.Scan
Array.getElem?_scanl : ∀ {β : Type u_1} {α : Type u_2} {a : β} {l : Array α} {i : ℕ} {f : β → α → β},
  (Array.scanl f a l)[i]? = if i ≤ l.size then some (Array.foldl f a (l.take i)) else none
-- Mathlib.NumberTheory.RamificationInertia.Inertia
/-- The inertia degree of `P : Ideal S` lying over `p : Ideal R` is the degree of the
extension `(S / P) : (R / p)`.

We do not assume `P` lies over `p` in the definition; we return `0` instead.

See `inertiaDeg'_algebraMap` for the common case where `f = algebraMap R S`
and there is an algebra structure `R / p → S / P`.

Note: This definition of inertia degree will eventually be replaced by `Ideal.inertiaDeg`.
 -/
Ideal.inertiaDeg' : {R : Type u} → [inst : CommRing R] → {S : Type v} → [inst_1 : CommRing S] → [Algebra R S] → Ideal R → Ideal S → ℕ
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.IterM.toArray_flatMapAfterM : ∀ {α α₂ β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α m β] [inst_5 : Std.Iterator α₂ m γ] [Std.Iterators.Finite α m]
  [Std.Iterators.Finite α₂ m] {f : β → m (Std.IterM m γ)} {it₁ : Std.IterM m β} {it₂ : Option (Std.IterM m γ)},
  (Std.IterM.flatMapAfterM f it₁ it₂).toArray =
    match it₂ with
    | none =>
      Array.flatten <$>
        (Std.IterM.mapM
            (fun b => do
              let __do_lift ← f b
              __do_lift.toArray)
            it₁).toArray
    | some it₂ => do
      let __do_lift ← it₂.toArray
      let __do_lift_1 ←
        Array.flatten <$>
            (Std.IterM.mapM
                (fun b => do
                  let __do_lift ← f b
                  __do_lift.toArray)
                it₁).toArray
      pure (__do_lift ++ __do_lift_1)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.mk₅_surjective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.ComposableArrows C 5),
  ∃ X₀ X₁ X₂ X₃ X₄ X₅ f₀ f₁ f₂ f₃ f₄, X = CategoryTheory.ComposableArrows.mk₅ f₀ f₁ f₂ f₃ f₄
-- Mathlib.CategoryTheory.Sites.Plus
/-- Lift a morphism `P ⟶ Q` to `P⁺ ⟶ Q` when `Q` is a sheaf.  -/
CategoryTheory.GrothendieckTopology.plusLift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          [inst_2 :
              ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
            [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
              {P Q : CategoryTheory.Functor Cᵒᵖ D} → (P ⟶ Q) → CategoryTheory.Presheaf.IsSheaf J Q → (J.plusObj P ⟶ Q)
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.op_comp_isSheaf_of_isSheaf_type : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C)
  {K : CategoryTheory.GrothendieckTopology D} [F.IsContinuous J K] {G : CategoryTheory.Functor Dᵒᵖ (Type u_1)},
  CategoryTheory.Presieve.IsSheaf K G → CategoryTheory.Presieve.IsSheaf J (F.op.comp G)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- **Alias** of `Submodule.orthogonalProjectionOnto_apply_of_mem_orthogonal`.

---

The orthogonal projection onto `K` of an element of `Kᗮ` is zero.  -/
Submodule.orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] {v : E}, v ∈ Kᗮ → K.orthogonalProjectionOnto v = 0
-- Init.Data.String.Pattern.Basic
/-- A strict forward pattern is one which never drops an empty prefix.

This condition ensures that the default searcher derived from the forward pattern is a finite
iterator.
 -/
String.Slice.Pattern.StrictForwardPattern : {ρ : Type} → (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → Prop
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- Constructor for `SSet.Edge.CompStruct` which takes as an input a term in the
definitionally equal type `SSet.Truncated.Edge.CompStruct` for the `2`-truncation of
the simplicial set. (This definition is made to contain abuse of defeq in
other definitions.)  -/
SSet.Edge.CompStruct.ofTruncated : {X : SSet} →
  {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} →
    {e₀₁ : SSet.Edge x₀ x₁} →
      {e₁₂ : SSet.Edge x₁ x₂} →
        {e₀₂ : SSet.Edge x₀ x₂} → e₀₁.toTruncated.CompStruct e₁₂.toTruncated e₀₂.toTruncated → e₀₁.CompStruct e₁₂ e₀₂
-- Lean.Parser.Term
Lean.Parser.Term.matchExprElseAlt.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Pos.revSkip?_bool_eq_none_iff : ∀ {p : Char → Bool} {s : String} {pos : s.Pos},
  pos.revSkip? p = none ↔ ∀ (h : pos ≠ s.startPos), p ((pos.prev h).get ⋯) = false
-- Mathlib.Data.Finset.Lattice.Fold
Finset.le_sup_of_le : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α} {a : α}
  {b : β}, b ∈ s → a ≤ f b → a ≤ s.sup f
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the forward direction of `lowerHemicontinuousAt_iff_frequently`. -/
LowerHemicontinuousAt.frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α},
  LowerHemicontinuousAt f x → ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, f x' ⊆ t) → f x ⊆ t
-- Mathlib.Topology.Compactness.CountablyCompact
Subtype.isSeqCompact_iff : ∀ {E : Type u_2} [inst : TopologicalSpace E] {p : E → Prop} {A : Set { x // p x }},
  IsSeqCompact A ↔ IsSeqCompact (Subtype.val '' A)
-- Mathlib.Order.CompleteLattice.Basic
le_iInf_iff : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {f : ι → α} {a : α}, a ≤ iInf f ↔ ∀ (i : ι), a ≤ f i
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.exists_isIntegral : ∀ (R : Type u_1) [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] [inst_3 : IsDomain R]
  [ValuationRing R] [IsFractionRing R K] (W : WeierstrassCurve K), ∃ C, WeierstrassCurve.IsIntegral R (C • W)
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.linearIndepOn_root : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (self : P.Base),
  LinearIndepOn R ⇑P.root ↑self.support
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
Std.IterM.uLift.eq_1 : ∀ {α β : Type u} {m : Type u → Type u'} (it : Std.IterM m β) (n : Type (max u v) → Type v')
  [lift : MonadLiftT m (Std.Iterators.ULiftT n)], it.uLift n = { internalState := { inner := it } }
-- Mathlib.Topology.Semicontinuity.Defs
/-- A function `f : α → Set β` has an open cgraph if the set of all `x` such that `x.2 ∈ f x.1`
is open in `α × β`.  -/
HasOpenCGraph : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → [TopologicalSpace β] → (α → Set β) → Prop
-- Mathlib.NumberTheory.RamificationInertia.Basic
/-- Let `V` be a vector space over `K = Frac(R)`, `S / R` a ring extension
and `V'` a module over `S`. If `b`, in the intersection `V''` of `V` and `V'`,
is linear independent over `S` in `V'`, then it is linear independent over `R` in `V`.

The statement we prove is actually slightly more general:
* it suffices that the inclusion `algebraMap R S : R → S` is nontrivial
* the function `f' : V'' → V'` doesn't need to be injective
 -/
Ideal.FinrankQuotientMap.linearIndependent_of_nontrivial : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (K : Type u_1)
  [inst_3 : Field K] [inst_4 : Algebra R K] {V : Type u_3} {V' : Type u_4} {V'' : Type u_5} [inst_5 : AddCommGroup V]
  [inst_6 : Module R V] [inst_7 : Module K V] [IsScalarTower R K V] [inst_9 : AddCommGroup V'] [inst_10 : Module R V']
  [inst_11 : Module S V'] [IsScalarTower R S V'] [inst_13 : AddCommGroup V''] [inst_14 : Module R V'']
  [hRK : IsFractionRing R K] [IsDedekindDomain R],
  RingHom.ker (algebraMap R S) ≠ ⊤ →
    ∀ (F : V'' →ₗ[R] V),
      Function.Injective ⇑F →
        ∀ (f' : V'' →ₗ[R] V') {ι : Type u_6} {b : ι → V''}, LinearIndependent S (⇑f' ∘ b) → LinearIndependent K (⇑F ∘ b)
-- Mathlib.Topology.Order.IsLUB
isGLB_iff_of_subset_of_subset_closure : ∀ {α : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIciTopology α] {s t : Set α},
  s ⊆ t → t ⊆ closure s → ∀ {x : α}, IsGLB s x ↔ IsGLB t x
-- Mathlib.Combinatorics.Matroid.Loop
/-- A 'loop' is a member of the closure of the empty set  -/
Matroid.IsLoop : {α : Type u_1} → Matroid α → α → Prop
-- Mathlib.Order.Interval.Set.Fin
Fin.image_natAdd_Ioc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.natAdd m '' Set.Ioc i j = Set.Ioc (Fin.natAdd m i) (Fin.natAdd m j)
-- Mathlib.Algebra.FreeAlgebra
/-- Given a function from `X` to an `R`-algebra `A`, `lift_fun` provides a lift of `f` to a function
from `Pre R X` to `A`. This is mainly used in the construction of `FreeAlgebra.lift`.  -/
FreeAlgebra.liftFun : (R : Type u_1) →
  (X : Type u_2) →
    [inst : CommSemiring R] → {A : Type u_3} → [inst_1 : Semiring A] → [Algebra R A] → (X → A) → FreeAlgebra.Pre R X → A
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwiseDisjoint_insert : ∀ {α : Type u_1} {ι : Type u_4} [inst : PartialOrder α] [inst_1 : OrderBot α] {s : Set ι} {f : ι → α} {i : ι},
  (insert i s).PairwiseDisjoint f ↔ s.PairwiseDisjoint f ∧ ∀ j ∈ s, i ≠ j → Disjoint (f i) (f j)
-- Mathlib.Data.Part
Part.instSub.eq_1 : ∀ {α : Type u_1} [inst : Sub α], Part.instSub = { sub := fun a b => (fun x1 x2 => x1 - x2) <$> a <*> b }
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.num_le : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [IsLocalization S P] (I : FractionalIdeal S P), ↑I.num ≤ I
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `not_isMulTorsion_of_isMulTorsionFree`.

---

A nontrivial torsion-free abelian group is not torsion.  -/
not_isTorsion_of_isMulTorsionFree : ∀ {G : Type u_1} [inst : CommGroup G] [Nontrivial G] [IsMulTorsionFree G], ¬IsMulTorsion G
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
Vector.iterFromIdxM.eq_1 : ∀ {α : Type w} {n : ℕ} (xs : Vector α n) (m : Type w → Type w') (pos : ℕ) [inst : Pure m],
  xs.iterFromIdxM m pos = xs.toArray.iterFromIdxM m pos
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- `s ↦ (s - 1) * L χ s` is an entire function when `χ` is a trivial Dirichlet character.  -/
DirichletCharacter.differentiable_LFunctionTrivChar₁ : ∀ (n : ℕ) [inst : NeZero n], Differentiable ℂ (DirichletCharacter.LFunctionTrivChar₁ n)
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofCustomInfo.injEq : ∀ (i i_1 : Lean.Elab.CustomInfo), (Lean.Elab.Info.ofCustomInfo i = Lean.Elab.Info.ofCustomInfo i_1) = (i = i_1)
-- Mathlib.Algebra.PresentedMonoid.Basic
/-- `of` is the canonical map from `α` to a presented monoid with generators `x : α`. The term `x`
is mapped to the equivalence class of the image of `x` in `FreeMonoid α`.  -/
PresentedMonoid.of : {α : Type u_1} → (rels : FreeMonoid α → FreeMonoid α → Prop) → α → PresentedMonoid rels
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthInfTopHom.eq_1 : LinearGrowth.linearGrowthInfTopHom =
  { toFun := LinearGrowth.linearGrowthInf, map_inf' := ⋯, map_top' := LinearGrowth.linearGrowthInf_top }
-- Batteries.Data.List.Basic
/-- Auxiliary for `findIdxNth`: `findIdxNth.go p l n acc = findIdxNth p l n + acc`.  -/
List.findIdxNth.go : {α : Type u_1} → (α → Bool) → List α → ℕ → ℕ → ℕ
-- Mathlib.Data.WSeq.Defs
/-- Like take, but does not wait for a result. Calculates `n` steps of
computation and returns the sequence computed so far  -/
Stream'.WSeq.collect : {α : Type u} → Stream'.WSeq α → ℕ → List α
-- Mathlib.LinearAlgebra.Isomorphisms
LinearMap.quotientInfToSupQuotient.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p p' : Submodule R M),
  LinearMap.quotientInfToSupQuotient p p' =
    (Submodule.comap p.subtype (p ⊓ p')).liftQ (LinearMap.subToSupQuotient p p') ⋯
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.all_toList : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] {p : α → β → Bool},
  m.WF → (m.toList.all fun x => p x.1 x.2) = m.all p
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_unitIso_inv_app_right_app : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {L L' : CategoryTheory.Functor C D} (iso₁ : L ≅ L') (F : CategoryTheory.Functor C H)
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L))
  (X_1 : D),
  ((CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁ iso₁ F).unitIso.inv.app X).right.app X_1 =
    CategoryTheory.CategoryStruct.id (X.right.obj X_1)
-- Mathlib.Logic.Function.Basic
Function.LeftInverse.rightInverse : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α}, Function.LeftInverse g f → Function.RightInverse f g
-- Mathlib.CategoryTheory.Adjunction.CompositionIso
CategoryTheory.Adjunction.leftAdjointCompIso_hom : ∀ {C₀ : Type u_1} {C₁ : Type u_2} {C₂ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₀]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₁] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₂]
  {F₀₁ : CategoryTheory.Functor C₀ C₁} {F₁₂ : CategoryTheory.Functor C₁ C₂} {F₀₂ : CategoryTheory.Functor C₀ C₂}
  {G₁₀ : CategoryTheory.Functor C₁ C₀} {G₂₁ : CategoryTheory.Functor C₂ C₁} {G₂₀ : CategoryTheory.Functor C₂ C₀}
  (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₂ : F₁₂ ⊣ G₂₁) (adj₀₂ : F₀₂ ⊣ G₂₀) (e₀₁₂ : G₂₁.comp G₁₀ ≅ G₂₀),
  (adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂).hom = adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ e₀₁₂.inv
-- Std.Internal.Do.WP.Basic
Std.Internal.Do.WP.wpTrans_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {Prog : Type u} {Value : Type v} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Std.Internal.Do.WP Prog Value Pred EPred] (x : Prog),
  (Std.Internal.Do.WP.wpTrans x).apply = Std.Internal.Do.wp x
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.leadingCoeff_taylor : ∀ {R : Type u_1} [inst : Semiring R] (r : R) (f : Polynomial R), ((Polynomial.taylor r) f).leadingCoeff = f.leadingCoeff
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.isNonConstFun : Lean.Expr → Lean.MetaM Bool
-- Mathlib.CategoryTheory.Shift.SingleFunctorsLift
CategoryTheory.SingleFunctors.map_lift_shiftIso_hom_app_assoc : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{u_7, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_6, u_2} D] [inst_2 : CategoryTheory.Category.{u_5, u_3} E] {A : Type u_4}
  [inst_3 : AddMonoid A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : CategoryTheory.HasShift E A]
  (F : CategoryTheory.SingleFunctors C E A) (G : CategoryTheory.Functor D E) [inst_6 : G.CommShift A] [inst_7 : G.Full]
  [inst_8 : G.Faithful] (Φ : A → CategoryTheory.Functor C D) (hΦ : (a : A) → (Φ a).comp G ≅ F.functor a) (n a a' : A)
  (h : n + a = a') (X : C) {Z : E} (h_1 : G.obj ((Φ a).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map (((F.lift G Φ hΦ).shiftIso n a a' h).hom.app X)) h_1 =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso G n).hom.app ((Φ a').obj X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor E n).map ((hΦ a').hom.app X))
        (CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' h).hom.app X)
          (CategoryTheory.CategoryStruct.comp ((hΦ a).inv.app X) h_1)))
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.subgraphOfAdj.congr_simp : ∀ {V : Type u} (G : SimpleGraph V) {v v_1 : V} (e_v : v = v_1) {w w_1 : V} (e_w : w = w_1) (hvw : G.Adj v w),
  G.subgraphOfAdj hvw = G.subgraphOfAdj ⋯
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- Constructs a morphism to the product given its two components.
 -/
CategoryTheory.CartesianMonoidalCategory.lift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {T X Y : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.eq_of_mem_uIoc_of_mem_uIoc' : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, b ∈ Set.uIoc a c → c ∈ Set.uIoc a b → b = c
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.Error.other.sizeOf_spec : ∀ (s : String), sizeOf (Std.Internal.Parsec.Error.other s) = 1 + sizeOf s