mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Sum.Order
OrderIso.sumCongr_trans : ∀ {α₁ : Type u_4} {α₂ : Type u_5} {β₁ : Type u_6} {β₂ : Type u_7} {γ₁ : Type u_8} {γ₂ : Type u_9} [inst : LE α₁]
  [inst_1 : LE α₂] [inst_2 : LE β₁] [inst_3 : LE β₂] [inst_4 : LE γ₁] [inst_5 : LE γ₂] (e₁ : α₁ ≃o β₁) (e₂ : α₂ ≃o β₂)
  (f₁ : β₁ ≃o γ₁) (f₂ : β₂ ≃o γ₂), (e₁.sumCongr e₂).trans (f₁.sumCongr f₂) = (e₁.trans f₁).sumCongr (e₂.trans f₂)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
MultipliableLocallyUniformlyOn.mono : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β] {t : Set β},
  MultipliableLocallyUniformlyOn f t → s ⊆ t → MultipliableLocallyUniformlyOn f s
-- Mathlib.Data.PNat.Defs
PNat.coe_eq_one_iff : ∀ {m : ℕ+}, ↑m = 1 ↔ m = 1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.TwoPowShiftTarget.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {w : ℕ} (n : ℕ) (lhs : aig.RefVec w)
  (rhs : aig.RefVec n) (pow n_1 : ℕ) (lhs_1 : aig.RefVec w) (rhs_1 : aig.RefVec n_1) (pow_1 : ℕ),
  ({ n := n, lhs := lhs, rhs := rhs, pow := pow } = { n := n_1, lhs := lhs_1, rhs := rhs_1, pow := pow_1 }) =
    (n = n_1 ∧ lhs = lhs_1 ∧ rhs ≍ rhs_1 ∧ pow = pow_1)
-- Init.Data.SInt.Lemmas
ISize.le_iff_toInt_le : ∀ {x y : ISize}, x ≤ y ↔ x.toInt ≤ y.toInt
-- Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
_private.Mathlib.MeasureTheory.VectorMeasure.BoundedVariation.0.BoundedVariationOn.measureAux.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : DenselyOrdered α] [inst_2 : TopologicalSpace α]
  [inst_3 : OrderTopology α] [inst_4 : SecondCountableTopology α] [inst_5 : CompactIccSpace α] [hα : MeasurableSpace α]
  [inst_6 : BorelSpace α] {E : Type u_2} [inst_7 : NormedAddCommGroup E] [inst_8 : CompleteSpace E] {f : α → E}
  (hf : BoundedVariationOn f Set.univ),
  BoundedVariationOn.measureAux✝ hf = if h : Nonempty α then (hf.stieltjesFunctionRightLim h.some).measure else 0
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.natCast.sizeOf_spec : ∀ (k : ℕ), sizeOf (Lean.Grind.CommRing.Expr.natCast k) = 1 + sizeOf k
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitePos_of_tendsto_top : ∀ {f : ℕ → ℝ}, Filter.Tendsto f Filter.atTop Filter.atTop → (Hyperreal.ofSeq f).InfinitePos
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicoequalizer.condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasMulticoequalizer I] (a : J.L)
  {Z : C} (h : CategoryTheory.Limits.multicoequalizer I ⟶ Z),
  CategoryTheory.CategoryStruct.comp (I.fst a)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I (J.fst a)) h) =
    CategoryTheory.CategoryStruct.comp (I.snd a)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I (J.snd a)) h)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The type of continuous monoid homomorphisms from `A` to `B`. -/
ContinuousMonoidHom.«term_→ₜ*_» : Lean.TrailingParserDescr
-- Init.Data.List.Find
/-- If `find? p` returns `some a` from `xs.flatten`, then `p a` holds, and
some list in `xs` contains `a`, and no earlier element of that list satisfies `p`.
Moreover, no earlier list in `xs` has an element satisfying `p`.
 -/
List.find?_flatten_eq_some_iff : ∀ {α : Type u_1} {xs : List (List α)} {p : α → Bool} {a : α},
  List.find? p xs.flatten = some a ↔
    p a = true ∧
      ∃ as ys zs bs, xs = as ++ (ys ++ a :: zs) :: bs ∧ (∀ l ∈ as, ∀ x ∈ l, (!p x) = true) ∧ ∀ x ∈ ys, (!p x) = true
-- Mathlib.Order.Basic
PUnit.le : ∀ (a b : PUnit.{u_5 + 1}), a ≤ b
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_eq_toBitVec : ∀ (a : ISize) (h : System.Platform.numBits = 64), a.toBitVec64 h = BitVec.cast h a.toBitVec
-- Mathlib.CategoryTheory.Limits.Creates
/-- The lifted cocone has an image isomorphic to the original cocone.  -/
CategoryTheory.liftedColimitMapsToOriginal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                [inst_3 : CategoryTheory.CreatesColimit K F] →
                  {c : CategoryTheory.Limits.Cocone (K.comp F)} →
                    (t : CategoryTheory.Limits.IsColimit c) → F.mapCocone (CategoryTheory.liftColimit t) ≅ c
-- Mathlib.GroupTheory.Focal
/-- Lemma: The focal subgroup is indeed a subgroup of H.  -/
AddSubgroup.focalAddSubgroup_le : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.focalAddSubgroup ≤ H
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.topEquiv_apply : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : ↥⊤),
  Submodule.topEquiv x = ↑x
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- The elliptic relator `ERₐ(a, b, c, d)` obtained by a change of variables in `ER(p, q, r, s)`
(see `IsEllipticNet.rel_eq` and `IsEllipticNet.atomRel_eq`). Note that this is defined in terms of
elliptic atoms, and hence should only be used when `a`, `b`, `c`, and `d` have the same parity.  -/
IsEllipticNet.atomRel : {R : Type u_1} → [CommRing R] → (ℤ → R) → ℤ → ℤ → ℤ → ℤ → R
-- Lean.Level
Lean.Level.succ.injEq : ∀ (a a_1 : Lean.Level), (a.succ = a_1.succ) = (a = a_1)
-- Mathlib.Analysis.Convex.EGauge
egauge_le_of_mem_smul : ∀ {𝕜 : Type u_1} [inst : NNNorm 𝕜] {E : Type u_2} [inst_1 : SMul 𝕜 E] {c : 𝕜} {s : Set E} {x : E},
  x ∈ c • s → egauge 𝕜 s x ≤ ‖c‖ₑ
-- Std.Data.DTreeMap.Basic
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Equiv.inner : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {m₁ m₂ : Std.DTreeMap α β cmp},
  m₁.Equiv m₂ → m₁.inner.Equiv m₂.inner
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.coequalizer.π_desc : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasCoequalizer f g] {W : C} (k : Y ⟶ W)
  (h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g)
      (CategoryTheory.Limits.coequalizer.desc k h) =
    k
-- Init.Data.SInt.Lemmas
ISize.toInt_maxValue_add_one : ISize.maxValue.toInt + 1 = 2 ^ (System.Platform.numBits - 1)
-- Mathlib.Data.Finset.Union
Finset.disjiUnion_singleton_eq_self : ∀ {α : Type u_1} (s : Finset α), s.disjiUnion singleton ⋯ = s
-- Init.Data.String.Slice
String.Slice.RevSplitIterator.instIteratorOfPure : {ρ : Type} →
  {ρ_1 : ρ} →
    {σ : String.Slice → Type} →
      [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
        [inst : String.Slice.Pattern.ToBackwardSearcher ρ_1 σ] →
          {m : Type → Type u_1} →
            {s : String.Slice} → [Pure m] → Std.Iterator (String.Slice.RevSplitIterator ρ_1 s) m String.Slice
-- Mathlib.Data.Nat.Log
Nat.log_div_mul_self : ∀ (b n : ℕ), Nat.log b (n / b * b) = Nat.log b n
-- Mathlib.Data.Finset.Slice
Set.Sized.mono : ∀ {α : Type u_1} {A B : Set (Finset α)} {r : ℕ}, A ⊆ B → Set.Sized r B → Set.Sized r A
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.HasEval.mul_left : ∀ {σ : Type u_1} {S : Type u_3} [inst : CommRing S] [inst_1 : TopologicalSpace S] [IsLinearTopology S S] (c : σ → S)
  {x : σ → S}, MvPowerSeries.HasEval x → MvPowerSeries.HasEval (c * x)
-- Mathlib.Order.Interval.Set.UnorderedInterval
Antitone.mapsTo_uIcc : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Lattice β] {f : α → β} {a b : α},
  Antitone f → Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_of_add_lt_of_nonneg_left : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftMono α] {a b c : α}, a + b < c → 0 ≤ b → a < c
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.exists_eq_mul : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedField β] {u v : α → β} {l : Filter α},
  Asymptotics.IsEquivalent l u v → ∃ φ, ∃ (_ : Filter.Tendsto φ l (nhds 1)), u =ᶠ[l] φ * v
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.liftMagma_apply_apply : ∀ (R : Type u_1) {A : Type u_4} {M : Type u_7} [inst : Semiring R] [inst_1 : Mul M]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : Module R A] [inst_4 : IsScalarTower R A A]
  [inst_5 : SMulCommClass R A A] (f : M →ₙ* A) (a : MonoidAlgebra R M),
  ((MonoidAlgebra.liftMagma R) f) a =
    (↑((Finsupp.liftAddHom fun x => (smulAddHom R A).flip (f x)).comp MonoidAlgebra.coeffAddEquiv.toAddMonoidHom)).toFun
      a
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_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] (L : CategoryTheory.Functor C D)
  (R : CategoryTheory.Functor E D),
  (CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence L R).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        CategoryTheory.Iso.refl
          (((CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor L R).comp
                (CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R)).obj
            x))
      ⋯
-- Mathlib.FieldTheory.NormalizedTrace
/-- Normalized trace defined purely in terms of the degree and the next coefficient of the minimal
polynomial. Could be an alternative definition but it is harder to work with linearity.  -/
Algebra.normalizedTrace_minpoly : ∀ (F : Type u_1) {K : Type u_2} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] [inst_3 : CharZero F]
  [inst_4 : Algebra.IsIntegral F K] (a : K),
  (Algebra.normalizedTrace F K) a = (↑(minpoly F a).natDegree)⁻¹ • -(minpoly F a).nextCoeff
-- Mathlib.NumberTheory.LucasLehmer
/-- `q` is the minimum factor of `mersenne p`, so `M p = 0` in `X q`.  -/
LucasLehmer.mersenne_coe_X : ∀ (p : ℕ), ↑(mersenne p) = 0
-- Std.Time.DateTime.Timestamp
_private.Std.Time.DateTime.Timestamp.0.Std.Time.Timestamp.mk.injEq : ∀ (val val_1 : Std.Time.Duration), ({ val := val } = { val := val_1 }) = (val = val_1)
-- Mathlib.RingTheory.TensorProduct.Basic
LinearMap.liftBaseChange_tmul : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} (A : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : Module A N] [inst_8 : IsScalarTower R A N] (l : M →ₗ[R] N) (x : A) (y : M),
  (LinearMap.liftBaseChange A l) (x ⊗ₜ[R] y) = x • l y
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.genWrapper : Lean.Name → Option Lean.Expr → Lean.Expr → Lean.Elab.TermElabM Lean.Name
-- Mathlib.GroupTheory.Nilpotent
/-- The nilpotency class of a nilpotent `G` is equal to the smallest `n` for which an
ascending central series reaches `G` in its `n`-th term.  -/
AddSubgroup.least_ascending_central_series_length_eq_nilpotencyClass : ∀ {G : Type u_1} [inst : AddGroup G] [hG : AddGroup.IsNilpotent G], Nat.find ⋯ = AddGroup.nilpotencyClass G
-- Mathlib.Topology.Category.UniformSpace
CpltSepUniformSpace.hasForgetToUniformSpace : CategoryTheory.HasForget₂ CpltSepUniformSpace UniformSpaceCat
-- Mathlib.Order.Closure
LowerAdjoint.eq_of_le : ∀ {α : Type u_1} {β : Type u_4} [inst : SetLike α β] [inst_1 : PartialOrder α] (l : LowerAdjoint SetLike.coe)
  {s : Set β} {S : α}, s ⊆ ↑S → S ≤ l.toFun s → l.toFun s = S
-- Init.Data.List.Attach
List.head_pmap : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β} {xs : List α} (H : ∀ a ∈ xs, P a)
  (h : List.pmap f xs H ≠ []), (List.pmap f xs H).head h = f (xs.head ⋯) ⋯
-- Mathlib.GroupTheory.Submonoid.Center
/-- The center of a monoid acts commutatively on that monoid.  -/
Submonoid.center.smulCommClass_right : ∀ {M : Type u_1} [inst : Monoid M], SMulCommClass M (↥(Submonoid.center M)) M
-- Mathlib.Analysis.Normed.Module.Extr
/-- If `f : α → E` is a function such that `norm ∘ f` has a maximum along a filter `l` at a point
`c`, then the function `fun x => ‖f x + f c‖` has a maximum along `l` at `c`.  -/
IsMaxFilter.norm_add_self : ∀ {α : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {f : α → E} {l : Filter α} {c : α},
  IsMaxFilter (norm ∘ f) l c → IsMaxFilter (fun x => ‖f x + f c‖) l c
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_op_iff_unop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] (Q : CategoryTheory.ObjectProperty Cᵒᵖ),
  Q.IsClosedUnderLimitsOfShape Jᵒᵖ ↔ Q.unop.IsClosedUnderColimitsOfShape J
-- Mathlib.CategoryTheory.Galois.Decomposition
/-- Any connected object admits a hom from a Galois object.  -/
CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_connected : ∀ {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], ∃ A x, CategoryTheory.PreGaloisCategory.IsGalois A
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPMVars : Lean.Options → Bool
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.lTensor_zero : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P], LinearMap.lTensor M 0 = 0
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Option γ} {k : α},
  (Std.ExtTreeMap.filterMap f t).getKey? k = (t.getKey? k).pfilter fun x h' => (f x t[x]).isSome
-- Mathlib.Topology.ExtremallyDisconnected
ExtremallyDisconnected.mk : ∀ {X : Type u} [inst : TopologicalSpace X], (∀ (U : Set X), IsOpen U → IsOpen (closure U)) → ExtremallyDisconnected X
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.simpAttrNameToSimprocAttrName : Lean.Name → Lean.Name
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
spectralAlgNorm_one : ∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsUltrametricDist K] [h_alg : Algebra.IsAlgebraic K L], (spectralAlgNorm K L) 1 = 1
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- To show that `F` preserves the colimit of `K`, we may assume that `K` has a colimit.  -/
CategoryTheory.Limits.PreservesColimit.mk' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D},
  (CategoryTheory.Limits.HasColimit K → CategoryTheory.Limits.PreservesColimit K F) →
    CategoryTheory.Limits.PreservesColimit K F
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
IsStationary.nonempty : ∀ {α : Type v} {s : Set α} [inst : LinearOrder α], IsStationary s → s.Nonempty
-- Mathlib.Topology.Homeomorph.Lemmas
Topology.IsCoinducing.connectedComponentsHomeomorph_symm_mk_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  (hf : Topology.IsCoinducing f) (hf' : ∀ (y : Y), IsConnected (f ⁻¹' {y})) (x : X),
  (hf.connectedComponentsHomeomorph hf').symm (ConnectedComponents.mk (f x)) = ConnectedComponents.mk x
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.root_add_nsmul_mem_range_iff_le_chainTopCoeff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  LinearIndependent R ![P.root i, P.root j] →
    ∀ {n : ℕ}, P.root j + n • P.root i ∈ Set.range ⇑P.root ↔ n ≤ RootPairing.chainTopCoeff i j
-- Mathlib.Analysis.Calculus.Deriv.ZPow
iter_deriv_pow : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (n : ℕ) (x : 𝕜) (k : ℕ),
  deriv^[k] (fun x => x ^ n) x = (∏ i ∈ Finset.range k, (↑n - ↑i)) * x ^ (n - k)
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat),
  (CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence F).functor =
    CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor F
-- Mathlib.FieldTheory.IntermediateField.ExtendRight
IntermediateField.extendRight.algebraMap_mem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : IntermediateField K L)
  (M : Type u_3) [inst_3 : Field M] [inst_4 : Algebra K M] [inst_5 : Algebra L M] [inst_6 : IsScalarTower K L M]
  {S : Type u_5} [inst_7 : CommRing S] [inst_8 : Algebra S ↥F] [inst_9 : Algebra S M] [IsScalarTower S (↥F) M] (s : S),
  (algebraMap S M) s ∈ F.extendRight M
-- Mathlib.Analysis.Complex.Trigonometric
Real.tanh.eq_1 : ∀ (x : ℝ), Real.tanh x = (Complex.tanh ↑x).re
-- Std.Net.Addr
Std.Net.IPv4Addr.mk.sizeOf_spec : ∀ (octets : Vector UInt8 4), sizeOf { octets := octets } = 1 + sizeOf octets
-- Mathlib.Algebra.Group.Action.Hom
/-- A monoid homomorphism between two additive monoids M and N can be equivalently
specified by an additive action of M on N that is compatible with the addition on N.  -/
addMonoidHomEquivAddActionVAddAssocClass : (M : Type u_4) →
  (N : Type u_5) → [inst : AddMonoid M] → [inst_1 : AddMonoid N] → (M →+ N) ≃ { _inst // VAddAssocClass M N N }
-- Lean.Server.GoTo
Lean.Server.instFromJsonGoToKind : Lean.FromJson Lean.Server.GoToKind
-- Init.Control.Reader
instMonadControlReaderT : {m : Type u_1 → Type u_2} → {ρ : Type u_1} → MonadControl m (ReaderT ρ m)
-- Mathlib.Data.Holor
HolorIndex.take.eq_1 : ∀ {ds₂ : List ℕ} (x : List ℕ) (x_1 : HolorIndex (x ++ ds₂)), x_1.take = ⟨List.take x.length ↑x_1, ⋯⟩
-- Mathlib.Topology.Order
instTopologicalSpacePEmpty : TopologicalSpace PEmpty.{u_1 + 1}
-- Init.Data.Ord.Basic
Ordering.instDecidableExistsOfDecidablePred : {p : Ordering → Prop} → [DecidablePred p] → Decidable (∃ o, p o)
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- In finite dimensions over a non-discrete complete normed field, the canonical identification
(in terms of a basis) with `𝕜^n` (endowed with the product topology) is continuous.
This is the key fact which makes all linear maps from a T2 finite-dimensional TVS over such a field
continuous (see `LinearMap.continuous_of_finiteDimensional`), which in turn implies that all
norms are equivalent in finite dimensions.  -/
continuous_equivFun_basis : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [CompleteSpace 𝕜] [T2Space E]
  {ι : Type u_1} [inst_7 : Finite ι] (ξ : Module.Basis ι 𝕜 E), Continuous ⇑ξ.equivFun
-- Init.Data.Rat.Lemmas
Rat.intCast_sub : ∀ (a b : ℤ), ↑(a - b) = ↑a - ↑b
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- **Alias** of `MonoidAlgebra.coeff_mapAlgHom`. -/
MonoidAlgebra.mapRangeAlgHom_apply : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Monoid M] (f : A →ₐ[R] B)
  (x : MonoidAlgebra A M) (m : M), ((MonoidAlgebra.mapAlgHom M f) x).coeff m = f (x.coeff m)
-- Mathlib.Data.EReal.Inv
EReal.div_le_div_right_of_nonpos : ∀ {a b c : EReal}, c ≤ 0 → a ≤ b → b / c ≤ a / c
-- Mathlib.Tactic.CancelDenoms.Core
/-- Helper lemma to chain together a `simp` proof and the result of `mkProdPrf`.  -/
Mathlib.Tactic.CancelDenoms.derive_trans : ∀ {α : Type u_1} [inst : Mul α] {a b c d : α}, a = b → c * b = d → c * a = d
-- Mathlib.RingTheory.FormalGroup.Basic
_private.Mathlib.RingTheory.FormalGroup.Basic.0.termY₁ : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
IsLocalDiffeomorphAt.localInverse_mem_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (hf : IsLocalDiffeomorphAt I J n f x), f x ∈ hf.localInverse.source
-- Mathlib.Order.Heyting.Basic
GeneralizedCoheytingAlgebra.toOrderBot : {α : Type u_4} → [self : GeneralizedCoheytingAlgebra α] → OrderBot α
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.boundedBy_caratheodory : ∀ {α : Type u_1} {m : Set α → ENNReal} {s : Set α}, (∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t) → MeasurableSet s
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- The object of `smoothSheaf IM I M N` for the open set `U` in `M` is
`C^∞⟮IM, (unop U : Opens M); I, N⟯`, the `(IM, I)`-smooth functions from `U` to `N`.  This is not
just a "moral" equality but a literal and definitional equality!  -/
smoothSheaf.obj_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) {M : Type u} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (N : Type u)
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H N] (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ),
  (smoothSheaf IM I M N).presheaf.obj U = ContMDiffMap IM I (↥(Opposite.unop U)) N ↑⊤
-- Mathlib.Data.TypeVec
/-- retain only a `n-length` prefix of the argument  -/
TypeVec.drop : {n : ℕ} → TypeVec.{u} (n + 1) → TypeVec.{u} n
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
CompleteLattice.MulticoequalizerDiagram.multispanIndex_left : ∀ {T : Type u} [inst : CompleteLattice T] {ι : Type u_1} {x : T} {u : ι → T} {v : ι → ι → T}
  (d : CompleteLattice.MulticoequalizerDiagram x u v) (x_1 : (CategoryTheory.Limits.MultispanShape.prod ι).L),
  d.multispanIndex.left x_1 =
    match x_1 with
    | (i, j) => v i j
-- Std.Async.Signal
Std.Async.Signal.sigurg.sizeOf_spec : sizeOf Std.Async.Signal.sigurg = 1
-- Mathlib.Topology.ContinuousOn
Continuous.preimage_mem_nhdsSet : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Continuous f → ∀ {s u : Set β}, u ∈ nhdsSet s → f ⁻¹' u ∈ nhdsSet (f ⁻¹' s)
-- Mathlib.CategoryTheory.Core
CategoryTheory.Functor.coreId_inv_app_iso_inv : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : CategoryTheory.Core C),
  ((CategoryTheory.Functor.coreId C).inv.app X).iso.inv = CategoryTheory.CategoryStruct.id X.of
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.unop : C ⥤ D` creates limits of shape `Jᵒᵖ`, then `F : Cᵒᵖ ⥤ Dᵒᵖ` creates colimits
of shape `J`.  -/
CategoryTheory.Limits.createsColimitsOfShapeOfUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (J : Type w) →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) →
              [CategoryTheory.CreatesLimitsOfShape Jᵒᵖ F.unop] → CategoryTheory.CreatesColimitsOfShape J F