mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.IndPredBelow
/-- Is `type` a motive nested in foralls and applications?  -/
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.isIH : Lean.Expr → Lean.Meta.IndPredBelow.Context✝ → Option ℕ
-- Lean.Elab.Tactic.RCases
/-- parenthesize the message if the precedence is above `tgt`  -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.RCasesPatt.instToMessageData.parenAbove : ℕ → ℕ → Lean.MessageData → Lean.MessageData
-- Mathlib.Algebra.Category.Ring.Basic
RingEquiv.toCommRingCatIso_inv : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S),
  e.toCommRingCatIso.inv = CommRingCat.ofHom ↑e.symm
-- Lean.Elab.PreDefinition.EqnsUtils
/-- Simplify `if-then-expression`s in the goal target.
If `useNewSemantics` is `true`, the flag `backward.split` is ignored.
 -/
Lean.Elab.Eqns.simpIf? : Lean.MVarId → optParam Bool false → Lean.MetaM (Option Lean.MVarId)
-- Mathlib.Analysis.Normed.Module.FiniteDimension
instSecondCountableTopologyContinuousLinearMapIdOfFiniteDimensional : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace 𝕜]
  [FiniteDimensional 𝕜 E] [SecondCountableTopology F], SecondCountableTopology (E →L[𝕜] F)
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
MulOpposite.nndist_unop : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] (x y : αᵐᵒᵖ),
  nndist (MulOpposite.unop x) (MulOpposite.unop y) = nndist x y
-- Mathlib.Tactic.Simproc.ExistsAndEq
/-- Triggers at goals of the form `∃ a, body` and checks if `body` allows a single value `a'`
for `a`. If so, replaces `a` with `a'` and removes quantifier.

It looks through nested quantifiers and conjunctions searching for a `a = a'`
or `a' = a` subexpression.  -/
ExistsAndEq.existsAndEq : Lean.Meta.Simp.Simproc
-- Mathlib.Order.Hom.Basic
OrderIso.symm_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β), e.symm.symm = e
-- Mathlib.Algebra.Group.Even
Multiplicative.instDecidablePredIsSquare : {α : Type u_2} → [inst : Add α] → [DecidablePred Even] → DecidablePred IsSquare
-- Mathlib.Data.Set.Insert
Set.subset_pair_iff : ∀ {α : Type u_1} {s : Set α} {a b : α}, s ⊆ {a, b} ↔ ∀ x ∈ s, x = a ∨ x = b
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph_max : ∀ (o₁ o₂ : Ordinal.{u_1}), Cardinal.aleph (max o₁ o₂) = max (Cardinal.aleph o₁) (Cardinal.aleph o₂)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.OplaxTrans.vComp_naturality_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.LaxFunctor B C} (η : CategoryTheory.Lax.OplaxTrans F G)
  (θ : CategoryTheory.Lax.OplaxTrans G H) (a : B),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (η.vCompApp θ a))
      (η.vCompNaturality θ (CategoryTheory.CategoryStruct.id a)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (η.vCompApp θ a)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (η.vCompApp θ a)).inv
        (CategoryTheory.Bicategory.whiskerLeft (η.vCompApp θ a) (H.mapId a)))
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- A morphism `k : W ⟶ X` satisfying `∀ j₁ j₂, k ≫ f j₁ = k ≫ f j₂` factors through the
wide equalizer of `f` via `wideEqualizer.lift : W ⟶ wideEqualizer f`.  -/
CategoryTheory.Limits.wideEqualizer.lift : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        {f : J → (X ⟶ Y)} →
          [inst_1 : CategoryTheory.Limits.HasWideEqualizer f] →
            [Nonempty J] →
              {W : C} →
                (k : W ⟶ X) →
                  (∀ (j₁ j₂ : J),
                      CategoryTheory.CategoryStruct.comp k (f j₁) = CategoryTheory.CategoryStruct.comp k (f j₂)) →
                    (W ⟶ CategoryTheory.Limits.wideEqualizer f)
-- Init.Data.UInt.Lemmas
UInt64.le_of_eq : ∀ {a b : UInt64}, a = b → a ≤ b
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
/-- The tensor algebra of the module `M` over the commutative semiring `R`.
 -/
TensorAlgebra : (R : Type u_1) →
  [inst : CommSemiring R] → (M : Type u_2) → [inst_1 : AddCommMonoid M] → [Module R M] → Type (max u_1 u_2)
-- Init.SizeOf
Lean.Syntax.node.sizeOf_spec : ∀ (info : Lean.SourceInfo) (kind : Lean.SyntaxNodeKind) (args : Array Lean.Syntax),
  sizeOf (Lean.Syntax.node info kind args) = 1 + sizeOf info + sizeOf kind + sizeOf args
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetric.add : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T S : E →ₗ[𝕜] E}, T.IsSymmetric → S.IsSymmetric → (T + S).IsSymmetric
-- Mathlib.Order.Category.DistLat
DistLat.coe_of : ∀ (X : Type u) [inst : DistribLattice X], ↑(DistLat.of X) = X
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.orderEmbeddingN_apply : ∀ (X : SSet) (x : X.N), X.orderEmbeddingN x = x.subcomplex
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.set.match_1.splitter : {α : Type u_1} →
  (motive : List α → ℕ → α → Sort u_2) →
    (x : List α) →
      (x_1 : ℕ) →
        (x_2 : α) →
          ((head : α) → (as : List α) → (b : α) → motive (head :: as) 0 b) →
            ((a : α) → (as : List α) → (n : ℕ) → (b : α) → motive (a :: as) n.succ b) →
              ((x : ℕ) → (x_3 : α) → motive [] x x_3) → motive x x_1 x_2
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_empty' : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M], ∅.sum = fun x => 0
-- Mathlib.GroupTheory.Torsion
AddCommGroup.le_comap_torsion : ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommGroup G] [inst_1 : AddCommGroup H] (f : G →+ H),
  AddCommGroup.torsion G ≤ AddSubgroup.comap f (AddCommGroup.torsion H)
-- Mathlib.Algebra.Group.TypeTags.Basic
ofMul_one : ∀ {α : Type u} [inst : One α], Additive.ofMul 1 = 0
-- Mathlib.Algebra.Group.Finsupp
Finsupp.support_neg : ∀ {ι : Type u_1} {G : Type u_6} [inst : AddGroup G] (f : ι →₀ G), (-f).support = f.support
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.map_id : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (z : N), (f.map ⋯ f) z = z
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.instIsCancelVAddSubtypeMem : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : VAdd R M] [inst_1 : SetLike S M] [hS : VAddMemClass S R M] (s : S)
  [IsCancelVAdd R M], IsCancelVAdd R ↥s
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.coe.eq_1 : ∀ {α : Type u}, WithZero.coe = some
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (toPrelaxFunctorStruct : CategoryTheory.PrelaxFunctorStruct B C) →
          autoParam
              (∀ {a b : B} (f : a ⟶ b),
                toPrelaxFunctorStruct.map₂ (CategoryTheory.CategoryStruct.id f) =
                  CategoryTheory.CategoryStruct.id (toPrelaxFunctorStruct.map f))
              CategoryTheory.PrelaxFunctor.map₂_id._autoParam →
            autoParam
                (∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
                  toPrelaxFunctorStruct.map₂ (CategoryTheory.CategoryStruct.comp η θ) =
                    CategoryTheory.CategoryStruct.comp (toPrelaxFunctorStruct.map₂ η) (toPrelaxFunctorStruct.map₂ θ))
                CategoryTheory.PrelaxFunctor.map₂_comp._autoParam →
              CategoryTheory.PrelaxFunctor B C
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
/-- We can define `esymm σ R n` as a sum over explicit monomials  -/
MvPolynomial.esymm_eq_sum_monomial : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] (n : ℕ),
  MvPolynomial.esymm σ R n = ∑ t ∈ Finset.powersetCard n Finset.univ, (MvPolynomial.monomial (∑ i ∈ t, fun₀ | i => 1)) 1
-- Lean.LibrarySuggestions.Basic
_private.Lean.LibrarySuggestions.Basic.0.Lean.Expr.FoldRelevantConstantsImpl.State : Type
-- Mathlib.Data.Int.Bitwise
Int.bit_zero : Int.bit false 0 = 0
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∩ m₂).contains k = (m₁.contains k && m₂.contains k)
-- Mathlib.RingTheory.FreeRing
FreeRing.lift_comp_of : ∀ {α : Type u} {R : Type v} [inst : Ring R] (f : FreeRing α →+* R), FreeRing.lift (⇑f ∘ FreeRing.of) = f
-- Init.Data.UInt.Lemmas
instLawfulIdentityUInt64HAddOfNat : Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0
-- Mathlib.Order.Basic
Sum.elim_le_elim_iff : ∀ {β : Type u_3} {α₁ : Type u_5} {α₂ : Type u_6} [inst : LE β] {u₁ v₁ : α₁ → β} {u₂ v₂ : α₂ → β},
  Sum.elim u₁ u₂ ≤ Sum.elim v₁ v₂ ↔ u₁ ≤ v₁ ∧ u₂ ≤ v₂
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.const_s' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : C),
  (CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.const X).s' =
    CategoryTheory.CategoryStruct.id (CategoryTheory.SimplicialObject.Augmented.const.obj X).right
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.zero.sizeOf_spec : sizeOf Nat.Partrec.Code.zero = 1
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton : ∀ {n : ℕ} {K : Type u} [inst : Field K] [inst_1 : CharZero K] [hn : NeZero n] {ζ : K}
  [hcycl : IsCyclotomicExtension {n} ℚ K], IsPrimitiveRoot ζ n → IsIntegralClosure ↥ℤ[ζ] ℤ K
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.length_toList : ∀ {α : Type u} {r : Std.Rco α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxo.HasSize α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_6 : Std.Rxo.IsAlwaysFinite α] [Std.Rxo.LawfulHasSize α], r.toList.length = r.size
-- Mathlib.Tactic.Linter.FlexibleLinter
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.instReprStained : Repr Mathlib.Linter.Flexible.Stained✝
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.ReflPrefunctor.comp_map : ∀ {U : Type u_1} [inst : CategoryTheory.ReflQuiver U] {V : Type u_2} [inst_1 : CategoryTheory.ReflQuiver V]
  {W : Type u_3} [inst_2 : CategoryTheory.ReflQuiver W] (F : U ⥤rq V) (G : V ⥤rq W) {X Y : U} (f : X ⟶ Y),
  (F ⋙rq G).map f = G.map (F.map f)
-- Mathlib.Tactic.Linter.UnusedInstancesInType
/-- Gathers instance hypotheses in the type of `decl` that are unused in the remainder of the type and
whose types satisfy `p`. (Does not consider the body of the declaration.) Collects them into an
`Array Parameter`, and if (and only if) this array is nonempty, feeds it to `logOnUnused`.

Since `logOnUnused` will only be run if its argument is nonempty, it is allowed to be expensive.

Note that `p` is non-monadic, and may encounter loose bvars in its argument. This is a performance
optimization. However, the `Parameter`s are created in a telescope, and their fields will *not*
have loose bound variables.
 -/
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Lean.ConstantVal.onUnusedInstancesWhere : Lean.ConstantVal →
  (Lean.Expr → Bool) →
    (Array Mathlib.Linter.UnusedInstancesInType.Parameter✝ → Lean.Elab.TermElabM Unit) → Lean.Elab.TermElabM Unit
-- Mathlib.Geometry.Manifold.Riemannian.Basic
/-- Any neighborhood of `x` contains all the points which are close enough to `x` for the
Riemannian distance, `ℝ≥0∞` version.  -/
setOfPred_riemannianEDist_lt_subset_nhds' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : Bundle.RiemannianBundle fun x => TangentSpace I x] [inst_6 : IsManifold I 1 M]
  [IsContinuousRiemannianBundle E fun x => TangentSpace I x] [RegularSpace M] {x : M} {s : Set M},
  s ∈ nhds x → ∃ c > 0, {y | Manifold.riemannianEDist I x y < c} ⊆ s
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unmop_tensorUnit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit Cᴹᵒᵖ).unmop = CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.one_scaleRoots : ∀ {R : Type u_1} [inst : Semiring R] (r : R), Polynomial.scaleRoots 1 r = 1
-- Mathlib.Order.Basic
le_imp_le_iff_lt_imp_lt : ∀ {α : Type u_2} {β : Type u_5} [inst : LinearOrder α] [inst_1 : LinearOrder β] {a b : α} {c d : β},
  a ≤ b → c ≤ d ↔ d < c → b < a
-- Std.Time.Time.Unit.Basic
/-- Converts a `Nanosecond.Offset` to a `Millisecond.Offset`.
 -/
Std.Time.Nanosecond.Offset.toMilliseconds : Std.Time.Nanosecond.Offset → Std.Time.Millisecond.Offset
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.contains_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.isEmpty = true → t.contains a = false
-- Mathlib.Order.CompleteBooleanAlgebra
CompleteBooleanAlgebra.toBooleanAlgebra : {α : Type u_1} → [self : CompleteBooleanAlgebra α] → BooleanAlgebra α
-- Mathlib.CategoryTheory.Limits.Preorder
/-- The point of a cocone is an upper bound.  -/
Preorder.coconePt_mem_upperBounds : ∀ {C : Type u} [inst : Preorder C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} J]
  (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cocone F), c.pt ∈ upperBounds (Set.range F.obj)
-- Mathlib.Dynamics.Flow
/-- A flow `ψ` is called a *factor* of `ϕ` if there exists a semiconjugacy from `ϕ` to `ψ`.  -/
Flow.IsFactorOf : {τ : Type u_1} →
  {α : Type u_2} →
    [inst : TopologicalSpace τ] →
      [inst_1 : TopologicalSpace α] →
        [inst_2 : AddMonoid τ] → {β : Type u_3} → [inst_3 : TopologicalSpace β] → Flow τ β → Flow τ α → Prop
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.instBiprod : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P Q : C}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct P Q]
  [CategoryTheory.Injective P] [CategoryTheory.Injective Q], CategoryTheory.Injective (P ⊞ Q)
-- Mathlib.Data.Multiset.Defs
Multiset.mem_attach : ∀ {α : Type u_1} (s : Multiset α) (x : { x // x ∈ s }), x ∈ s.attach
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_map_left_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor T D) (Y : D) (X : T)
  {X_1 Y_1 : CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.proj F Y) X} (g : X_1 ⟶ Y_1),
  ((CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor F Y X).map g).left.left = g.left.left
-- Mathlib.Data.Matrix.Basic
AlgHom.mapMatrix_id : ∀ {m : Type u_2} {R : Type u_7} {α : Type u_11} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : CommSemiring R]
  [inst_3 : Semiring α] [inst_4 : Algebra R α], (AlgHom.id R α).mapMatrix = AlgHom.id R (Matrix m m α)
-- Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict
Preorder.measurable_restrictLe₂ : ∀ {α : Type u_1} [inst : Preorder α] {X : α → Type u_2} [inst_1 : (a : α) → MeasurableSpace (X a)] {a b : α}
  (hab : a ≤ b), Measurable (Preorder.restrictLe₂ hab)
-- Init.Data.Iterators.Internal.LawfulMonadLiftFunction
Std.Internal.instLawfulMonadLiftFunctionOfLawfulMonadLiftBindFunctionBindOfLawfulMonad : ∀ {m : Type u → Type v} {n : Type u → Type w} [inst : Monad m] [inst_1 : Monad n] {lift : ⦃α : Type u⦄ → m α → n α}
  [Std.Internal.LawfulMonadLiftBindFunction fun x x_1 f x_2 => lift x_2 >>= f] [LawfulMonad n],
  Std.Internal.LawfulMonadLiftFunction lift
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.map_algebraMap_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : CommRing S] [inst_4 : Module S M] [inst_5 : Algebra R S] [IsScalarTower R S M],
  IsAdicComplete (Ideal.map (algebraMap R S) I) M ↔ IsAdicComplete I M
-- Mathlib.Topology.MetricSpace.CantorScheme
/-- From a `β`-scheme on `α` `A`, we define a partial function from `(ℕ → β)` to `α`
which sends each infinite sequence `x` to an element of the intersection along the
branch corresponding to `x`, if it exists.
We call this the map induced by the scheme.  -/
CantorScheme.inducedMap : {β : Type u_1} → {α : Type u_2} → (List β → Set α) → (s : Set (ℕ → β)) × (↑s → α)
-- Mathlib.Tactic.Abel
/-- Raw form: the representation `abel` uses internally.  -/
Mathlib.Tactic.Abel.AbelMode.raw : Mathlib.Tactic.Abel.AbelMode
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.map_neg_atTop : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G],
  Filter.map Neg.neg Filter.atTop = Filter.atBot
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.preEquivalence_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e),
  (CategoryTheory.CostructuredArrow.preEquivalence F f).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        CategoryTheory.CostructuredArrow.isoMk
          (CategoryTheory.Iso.refl
            (((CategoryTheory.CostructuredArrow.preEquivalence.inverse F f).comp
                    (CategoryTheory.CostructuredArrow.preEquivalence.functor F f)).obj
                x).left)
          ⋯)
      ⋯
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.map_le_iff_le_comap : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {K : AddSubgroup G}
  {H : AddSubgroup N}, AddSubgroup.map f K ≤ H ↔ K ≤ AddSubgroup.comap f H
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeAddGroupBasis.instIsFreeAddGroupFreeAddGroup : ∀ (X : Type u_5), IsFreeAddGroup (FreeAddGroup X)
-- Mathlib.Order.Sublocale
Nucleus.coe_toSublocale : ∀ {X : Type u_1} [inst : Order.Frame X] (n : Nucleus X), ↑n.toSublocale = Set.range ⇑n
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.RotateLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateLeft.go_get : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (distance : ℕ)
  (input : aig.RefVec w) (curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr) (idx : ℕ) (hidx1 : idx < w),
  curr ≤ idx →
    (Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateLeft.go input distance curr hcurr s).get idx hidx1 =
      if hidx3 : idx < distance % w then input.get (w - distance % w + idx) ⋯ else input.get (idx - distance % w) ⋯
-- Mathlib.NumberTheory.FunctionField
/-- **Alias** of `RatFunc.InftyValuation.map_one'`. -/
FunctionField.InftyValuation.map_one' : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)], RatFunc.inftyValuationDef F 1 = 1
-- Init.Data.Prod
Prod.fst_swap : ∀ {α : Type u_1} {β : Type u_2} {p : α × β}, p.swap.1 = p.2
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.adjoinRootAlgEquiv_symm_apply_eq_mk : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) (a : S), h.adjoinRootAlgEquiv.symm a = (AdjoinRoot.mk f) (h.repr a)
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
prodIsoPullback_inv_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasTerminal C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryProduct X Y],
  CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).inv CategoryTheory.Limits.prod.fst =
    CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)
-- Mathlib.SetTheory.Cardinal.NatCard
Finite.one_lt_card : ∀ {α : Type u_1} [Finite α] [h : Nontrivial α], 1 < Nat.card α
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_const_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} {f : 𝕜 → F},
  0 < n → ∀ (c : F), iteratedDerivWithin n (fun z => c - f z) s x = iteratedDerivWithin n (fun z => -f z) s x
-- Std.Time.Zoned.Database
/-- Gets the local zone rules, accounting for platform differences.
In windows it uses the current `icu.h` in Windows SDK. If it's linux or macos then it will use the `tzdata`
files.
 -/
Std.Time.Database.defaultGetLocalZoneRules : IO Std.Time.TimeZone.ZoneRules
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.iUnion_top : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι}, ⊤.iUnion = ↑I
-- Mathlib.Analysis.Complex.UnitDisc.Basic
/-- Conjugate point of the unit disc.  -/
Complex.UnitClosedDisc.instStar : Star Complex.UnitClosedDisc
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
/-- Given `c = lineMap a b r`, `a < c`, the point `(c, f c)` is non-strictly above the
segment `[(a, f a), (b, f b)]` if and only if `slope f a b ≤ slope f a c`.  -/
lineMap_le_map_iff_slope_le_slope_left : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup E]
  [inst_3 : PartialOrder E] [IsOrderedAddMonoid E] [inst_5 : Module k E] [IsStrictOrderedModule k E]
  [PosSMulReflectLE k E] {f : k → E} {a b r : k},
  0 < r * (b - a) →
    ((AffineMap.lineMap (f a) (f b)) r ≤ f ((AffineMap.lineMap a b) r) ↔
      slope f a b ≤ slope f a ((AffineMap.lineMap a b) r))
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
/-- Shows `prodToProdTop` is an isomorphism, whose inverse is precisely the product
of the induced left and right projections.
 -/
FundamentalGroupoidFunctor.prodIso : (A : TopCat) →
  (B : TopCat) →
    CategoryTheory.Grpd.of
        (↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj A) ×
          ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj B)) ≅
      FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of (↑A × ↑B))
-- Mathlib.Algebra.Group.Hom.Defs
/-- Composition of monoid morphisms as a monoid morphism.  -/
MonoidHom.comp : {M : Type u_4} →
  {N : Type u_5} →
    {P : Type u_6} → [inst : MulOne M] → [inst_1 : MulOne N] → [inst_2 : MulOne P] → (N →* P) → (M →* N) → M →* P
-- Init.Core
/-- Iff can now be used to do substitutions in a calculation  -/
Iff.subst : ∀ {a b : Prop} {p : Prop → Prop}, (a ↔ b) → p a → p b
-- Mathlib.Algebra.Order.Ring.Defs
IsStrictOrderedRing.toIsOrderedRing : ∀ {R : Type u} [inst : Semiring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R], IsOrderedRing R
-- Mathlib.Analysis.Convex.Topology
convex_closed_sInter : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] {S : Set (Set E)},
  (∀ s ∈ S, Convex 𝕜 s ∧ IsClosed s) → Convex 𝕜 (⋂₀ S) ∧ IsClosed (⋂₀ S)
-- Mathlib.Data.String.Lemmas
String.leftpad_suffix : ∀ (n : ℕ) (c : Char) (s : String), s.IsSuffix (String.leftpad n c s)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_lt_mul_of_le_of_lt : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a b : M₀} [ZeroLEOneClass M₀] [MulPosMono M₀],
  1 ≤ a → 1 < b → 1 < a * b
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l →
        ∀ {h' : k' ∈ Std.DTreeMap.Const.ofList l cmp}, (Std.DTreeMap.Const.ofList l cmp).getKey k' h' = k