mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim_ι_ι_inv_assoc : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfShape K C] (k : K) (j : J) {Z : C}
  (h : CategoryTheory.Limits.colimit (F.flip.comp CategoryTheory.Limits.colim) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.obj j) k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.Limits.colim) j)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim F).inv h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.flip.obj k) j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.flip.comp CategoryTheory.Limits.colim) k)
        h)
-- Lean.MetavarContext
/-- Assignment table for expression metavariables. -/
Lean.MetavarContext.eAssignment : Lean.MetavarContext → Lean.PersistentHashMap Lean.MVarId Lean.Expr
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.strFn : String → Lean.Parser.ParserFn
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.le_dist_iff_le_dist_coe_center : ∀ {z w : UpperHalfPlane} {r : ℝ}, r < dist z w ↔ w.im * Real.sinh r < dist ↑z ↑(w.center r)
-- Mathlib.Algebra.CharP.Frobenius
coe_iterateFrobenius_mul : ∀ (R : Type u_1) [inst : CommSemiring R] (p m n : ℕ) [inst_1 : ExpChar R p],
  ⇑(iterateFrobenius R p (m * n)) = (⇑(iterateFrobenius R p m))^[n]
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackShape.subsingleton_hom : ∀ {J : Type w}, Quiver.IsThin (CategoryTheory.Limits.WidePullbackShape J)
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Broadcast.inner : {α : Type} → Std.Broadcast α → Std.Bounded✝ α
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValue!_filter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited β] {f : α → β → Bool}
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      Std.Internal.List.getValue! k (List.filter (fun p => f p.fst p.snd) l) =
        ((Std.Internal.List.getValue? k l).pfilter fun v h => f (Std.Internal.List.getKey k l ⋯) v).get!
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.continuousAt_add_coe_top : ∀ (a : ℝ), ContinuousAt (fun p => p.1 + p.2) (↑a, ⊤)
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.toAddConstMapHom_apply : ∀ {G : Type u_1} [inst : Add G] {a : G} (self : AddConstEquiv G G a a),
  AddConstEquiv.toAddConstMapHom self = self.toAddConstMap
-- Mathlib.Order.BooleanAlgebra.Set
Set.compl_sdiff : ∀ {α : Type u_1} {s t : Set α}, (t \ s)ᶜ = s ∪ tᶜ
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.functorExt_inv_app : ∀ {J : CategoryTheory.Limits.MultispanShape} {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  {F G : CategoryTheory.Functor (CategoryTheory.Limits.WalkingMultispan J) C}
  (left :
    (i : J.L) →
      F.obj (CategoryTheory.Limits.WalkingMultispan.left i) ≅ G.obj (CategoryTheory.Limits.WalkingMultispan.left i))
  (right :
    (i : J.R) →
      F.obj (CategoryTheory.Limits.WalkingMultispan.right i) ≅ G.obj (CategoryTheory.Limits.WalkingMultispan.right i))
  (wl :
    autoParam
      (∀ (i : J.L),
        CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WalkingMultispan.Hom.fst i))
            (right (J.fst i)).hom =
          CategoryTheory.CategoryStruct.comp (left i).hom (G.map (CategoryTheory.Limits.WalkingMultispan.Hom.fst i)))
      CategoryTheory.Limits.WalkingMultispan.functorExt._auto_1)
  (wr :
    autoParam
      (∀ (i : J.L),
        CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WalkingMultispan.Hom.snd i))
            (right (J.snd i)).hom =
          CategoryTheory.CategoryStruct.comp (left i).hom (G.map (CategoryTheory.Limits.WalkingMultispan.Hom.snd i)))
      CategoryTheory.Limits.WalkingMultispan.functorExt._auto_3)
  (X : CategoryTheory.Limits.WalkingMultispan J),
  (CategoryTheory.Limits.WalkingMultispan.functorExt left right wl wr).inv.app X =
    (match X with
      | CategoryTheory.Limits.WalkingMultispan.left i => left i
      | CategoryTheory.Limits.WalkingMultispan.right i => right i).inv
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.excenter_restrict : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs →
    ∀ (S : AffineSubspace ℝ P) (hS : affineSpan ℝ (Set.range s.points) ≤ S),
      ↑((s.restrict S hS).excenter signs) = s.excenter signs
-- Mathlib.RingTheory.TensorProduct.Maps
LinearMap.tensorProduct.eq_1 : ∀ (R : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid N]
  [inst_6 : Module R N],
  LinearMap.tensorProduct R A M N =
    TensorProduct.AlgebraTensorModule.lift
      { toFun := fun a => a • LinearMap.baseChangeHom R A M N, map_add' := ⋯, map_smul' := ⋯ }
-- Lean.Elab.InfoTree.Main
Lean.Elab.assignInfoHoleId : {m : Type → Type} → [Monad m] → [Lean.Elab.MonadInfoTree m] → Lean.MVarId → Lean.Elab.InfoTree → m Unit
-- Lean.Elab.Calc
_private.Lean.Elab.Calc.0.Lean.Elab.Term.getRelUniv : Lean.Expr → Lean.MetaM Lean.Level
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.Functor.mapDifferentialObject_obj_d : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (D : Type u')
  [inst_4 : CategoryTheory.Category.{v', u'} D] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D]
  [inst_6 : CategoryTheory.HasShift D S] (F : CategoryTheory.Functor C D)
  (η : (CategoryTheory.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1))
  (hF : ∀ (c c' : C), F.map 0 = 0) (X : CategoryTheory.DifferentialObject S C),
  ((CategoryTheory.Functor.mapDifferentialObject D F η hF).obj X).d =
    CategoryTheory.CategoryStruct.comp (F.map X.d) (η.app X.obj)
-- Mathlib.RingTheory.Perfection
ModP.preVal_mk : ∀ {K : Type u₁} [inst : Field K] {v : Valuation K NNReal} {O : Type u₂} [inst_1 : CommRing O] [inst_2 : Algebra O K],
  v.Integers O →
    ∀ {p : ℕ} {x : O},
      (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0 →
        ModP.preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) x) = v ((algebraMap O K) x)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.updateCell.match_5.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (l : Std.DTreeMap.Internal.Impl α β) → l.Balanced → Sort u_3)
  (hl : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (h_1 : (hl : Std.DTreeMap.Internal.Impl.leaf.Balanced) → motive Std.DTreeMap.Internal.Impl.leaf hl)
  (h_2 :
    (sz : ℕ) →
      (ky : α) →
        (y : β ky) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (hl : (Std.DTreeMap.Internal.Impl.inner sz ky y l r).Balanced) →
              motive (Std.DTreeMap.Internal.Impl.inner sz ky y l r) hl),
  (match Std.DTreeMap.Internal.Impl.leaf, hl with
    | Std.DTreeMap.Internal.Impl.leaf, hl => h_1 hl
    | Std.DTreeMap.Internal.Impl.inner sz ky y l r, hl => h_2 sz ky y l r hl) =
    h_1 hl
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.IsHermitian.star_eq : ∀ {α : Type u_1} {n : Type u_4} {A : Matrix n n α} [inst : Star α], A.IsHermitian → star A = A
-- Mathlib.Algebra.Order.GroupWithZero.Basic
lt_mul_of_one_lt_left : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Zero α] {a b : α} [inst_2 : Preorder α] [MulPosStrictMono α],
  0 < b → 1 < a → b < a * b
-- Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
AlgebraicGeometry.sourceLocalClosure.instIsStableUnderBaseChangeScheme : ∀ {W P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [W.IsStableUnderBaseChange]
  [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving W] [P.IsStableUnderBaseChange],
  (AlgebraicGeometry.sourceLocalClosure W P).IsStableUnderBaseChange
-- Mathlib.Algebra.Module.Congruence.Defs
SMulCon.mk.inj : ∀ {S : Type u_2} {M : Type u_3} {inst : SMul S M} {toSetoid : Setoid M}
  {smul : ∀ (s : S) {x y : M}, toSetoid x y → toSetoid (s • x) (s • y)} {toSetoid_1 : Setoid M}
  {smul_1 : ∀ (s : S) {x y : M}, toSetoid_1 x y → toSetoid_1 (s • x) (s • y)},
  { toSetoid := toSetoid, smul := smul } = { toSetoid := toSetoid_1, smul := smul_1 } → toSetoid = toSetoid_1
-- Mathlib.Data.Set.NAry
Set.image2_empty_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {t : Set β}, Set.image2 f ∅ t = ∅
-- Mathlib.FieldTheory.Normal.Closure
isNormalClosure_normalClosure : ∀ (F : Type u_1) (K : Type u_2) (L : Type u_3) [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra F K] [inst_4 : Algebra F L] [ne : Nonempty (K →ₐ[F] L)] [h : Normal F L],
  IsNormalClosure F K ↥(IntermediateField.normalClosure F K L)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
/-- The left and right shift of cochains commute only up to a sign.  -/
CochainComplex.HomComplex.Cochain.leftShift_rightShift_eq_negOnePow_rightShift_leftShift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' n'' : ℤ) (hn' : n' + a = n)
  (hn'' : n + a = n''),
  (γ.rightShift a n' hn').leftShift a n hn' = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.instMonoHomObjOverForget : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {f : CategoryTheory.MonoOver X},
  CategoryTheory.Mono ((CategoryTheory.MonoOver.forget X).obj f).hom
-- Mathlib.Order.Filter.SmallSets
Filter.comap_smallSets : ∀ {α : Type u_1} {β : Type u_2} (l : Filter β) (f : α → Set β),
  Filter.comap f l.smallSets = l.lift' (Set.preimage f ∘ Set.powerset)
-- Mathlib.Topology.Neighborhoods
Filter.HasBasis.nhds_interior : ∀ {X : Type u} [inst : TopologicalSpace X] {ι : Sort v} {x : X} {p : ι → Prop} {s : ι → Set X},
  (nhds x).HasBasis p s → (nhds x).HasBasis p fun x => interior (s x)
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Continuous.mulExpNegMulSq : ∀ {ε : ℝ} {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℝ},
  Continuous f → Continuous fun x => ε.mulExpNegMulSq (f x)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
ContinuousInv₀.measurableInv : ∀ {γ : Type u_3} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [BorelSpace γ] [inst_3 : GroupWithZero γ]
  [T1Space γ] [ContinuousInv₀ γ], MeasurableInv γ
-- Mathlib.Data.List.TakeWhile
List.dropWhile_eq_nil_iff : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.dropWhile p l = [] ↔ ∀ x ∈ l, p x = true
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
/-- Any surjective, flat morphism locally of finite presentation is an effective epimorphism.
In particular, étale surjections satisfy this.  -/
AlgebraicGeometry.Scheme.instEffectiveEpiOfLocallyOfFinitePresentationOfSurjectiveOfFlat : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyOfFinitePresentation f]
  [AlgebraicGeometry.Surjective f] [AlgebraicGeometry.Flat f], CategoryTheory.EffectiveEpi f
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.coe_neg : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Neg Y] (f : LocallyConstant X Y), ⇑(-f) = -⇑f
-- Lean.Elab.App
Lean.Elab.Term.ElabAppArgs.Context.mk.injEq : ∀ (ellipsis explicit resultIsOutParamSupport : Bool) (numImplicitParams : ℕ)
  (ellipsis_1 explicit_1 resultIsOutParamSupport_1 : Bool) (numImplicitParams_1 : ℕ),
  ({ ellipsis := ellipsis, explicit := explicit, resultIsOutParamSupport := resultIsOutParamSupport,
        numImplicitParams := numImplicitParams } =
      { ellipsis := ellipsis_1, explicit := explicit_1, resultIsOutParamSupport := resultIsOutParamSupport_1,
        numImplicitParams := numImplicitParams_1 }) =
    (ellipsis = ellipsis_1 ∧
      explicit = explicit_1 ∧
        resultIsOutParamSupport = resultIsOutParamSupport_1 ∧ numImplicitParams = numImplicitParams_1)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.mk.inj : ∀ {L : FirstOrder.Language} {M : Type w} {inst : L.Structure M} {carrier : Set M}
  {fun_mem : ∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f carrier} {carrier_1 : Set M}
  {fun_mem_1 : ∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f carrier_1},
  { carrier := carrier, fun_mem := fun_mem } = { carrier := carrier_1, fun_mem := fun_mem_1 } → carrier = carrier_1
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.isLocallyFaithful : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D)
  [CategoryTheory.Functor.IsDenseSubsite J K G], G.IsLocallyFaithful K
-- Init.Data.Fin.Bitwise
Fin.or_val_of_uInt16Size : ∀ (a b : Fin UInt16.size), ↑(a ||| b) = ↑a ||| ↑b
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
/-- `t.toFun` tends to `𝓝 0` when `t.coef = 0`.  -/
Tactic.ComputeAsymptotics.Monomial.tendsto_zero_of_coef_zero : ∀ {coef : ℝ} {exps : Tactic.ComputeAsymptotics.UnitMonomial} (basis : Tactic.ComputeAsymptotics.Basis),
  coef = 0 →
    have t := { coef := coef, unit := exps };
    Filter.Tendsto (t.toFun basis) Filter.atTop (nhds 0)
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.Hom.Simps.hom.eq_1 : ∀ (X Y : AddCommGrpCat) (f : X.Hom Y), AddCommGrpCat.Hom.Simps.hom X Y f = f.hom
-- Mathlib.Algebra.Group.Defs
DivisionCommMonoid.toCommMonoid : {G : Type u} → [self : DivisionCommMonoid G] → CommMonoid G
-- Mathlib.Order.CompleteLattice.Chain
_private.Mathlib.Order.CompleteLattice.Chain.0.chainClosure_succ_total : ∀ {α : Type u_1} {r : α → α → Prop} {c₁ c₂ : Set α},
  ChainClosure r c₁ → ChainClosure r c₂ → c₁ ⊆ c₂ → c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂
-- Mathlib.Data.Sym.Basic
/-- The canonical map to `Multiset α` that forgets that `s` has length `n`  -/
Sym.toMultiset : {α : Type u_1} → {n : ℕ} → Sym α n → Multiset α
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Inhabited α]
  {k fallback : α} {f : Option β → Option β},
  (t.alter k f).getKeyD k fallback = if (f t[k]?).isSome = true then k else fallback
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- `MonoOver.lift` commutes with composition of functors.  -/
CategoryTheory.MonoOver.liftComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {X Z : C} →
          {Y : D} →
            (F : CategoryTheory.Functor (CategoryTheory.Over X) (CategoryTheory.Over Y)) →
              (G : CategoryTheory.Functor (CategoryTheory.Over Y) (CategoryTheory.Over Z)) →
                (h₁ :
                    ∀ (f : CategoryTheory.MonoOver X),
                      CategoryTheory.Mono (F.obj ((CategoryTheory.MonoOver.forget X).obj f)).hom) →
                  (h₂ :
                      ∀ (f : CategoryTheory.MonoOver Y),
                        CategoryTheory.Mono (G.obj ((CategoryTheory.MonoOver.forget Y).obj f)).hom) →
                    (CategoryTheory.MonoOver.lift F h₁).comp (CategoryTheory.MonoOver.lift G h₂) ≅
                      CategoryTheory.MonoOver.lift (F.comp G) ⋯
-- Mathlib.Topology.NhdsWithin
nhdsWithin_le_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α} {x : α}, nhdsWithin x s ≤ nhdsWithin x t ↔ t ∈ nhdsWithin x s
-- Mathlib.MeasureTheory.Measure.Comap
MeasureTheory.Measure.comap_smul : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β}
  {μ : MeasureTheory.Measure β} (c : ENNReal),
  MeasureTheory.Measure.comap f (c • μ) = c • MeasureTheory.Measure.comap f μ
-- Std.Data.TreeMap.AdditionalOperations
/-- Updates the values of the map by applying the given function to all mappings.  -/
Std.TreeMap.map : {α : Type u} →
  {β : Type v} → {γ : Type w} → {cmp : α → α → Ordering} → (α → β → γ) → Std.TreeMap α β cmp → Std.TreeMap α γ cmp
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_left_le_size_union : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α], (↑m₁).WF → (↑m₂).WF → (↑m₁).size ≤ (↑(m₁.union m₂)).size
-- Init.Data.Int.Order
Int.le_add_of_neg_add_le_right : ∀ {a b c : ℤ}, -c + a ≤ b → a ≤ b + c
-- Init.Data.List.Attach
List.getLast?_attach : ∀ {α : Type u_1} {xs : List α}, xs.attach.getLast? = xs.getLast?.pbind fun a h => some ⟨a, ⋯⟩
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.ofSliceTo_ne_endPos : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos},
  p ≠ (s.sliceTo p₀).endPos → String.Slice.Pos.ofSliceTo p ≠ s.endPos
-- Init.Data.Array.Basic
Array.foldrM.fold : {α : Type u} →
  {β : Type v} →
    {m : Type v → Type w} → [Monad m] → (α → β → m β) → (as : Array α) → ℕ → (i : ℕ) → i ≤ as.size → β → m β
-- Init.Data.SInt.Basic
/-- Converts a 64-bit signed integer to a 16-bit signed integer by truncating its bitvector
representation.

This function is overridden at runtime with an efficient implementation.
 -/
Int64.toInt16 : Int64 → Int16
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.coe_coe : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj), ↑e.toPartialEquiv = ↑e
-- Init.Prelude
instMonadWithReaderOfReaderT : {ρ : Type u} → {m : Type u → Type v} → MonadWithReaderOf ρ (ReaderT ρ m)
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_range_mul_prod_Ico : ∀ {M : Type u_3} [inst : CommMonoid M] (f : ℕ → M) {m n : ℕ},
  m ≤ n → (∏ k ∈ Finset.range m, f k) * ∏ k ∈ Finset.Ico m n, f k = ∏ k ∈ Finset.range n, f k
-- Lean.Elab.Do.Basic
/-- The raw `Name` of a `mut` variable, as found in the local context.  -/
Lean.Elab.Do.MutVar.getId : Lean.Elab.Do.MutVar → Lean.Name
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso_hom_app_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (X : CategoryTheory.Functor C (CategoryTheory.Comon D)) (X_1 : C),
  ((CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso.hom.app X).app X_1).hom =
    CategoryTheory.CategoryStruct.id (X.obj X_1).X
-- Init.Data.OfScientific
instOfNatFloat32 : {n : ℕ} → OfNat Float32 n
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.instIsInvInvariantForallVolumeOfMeasurableInvOfSigmaFinite : ∀ {ι : Type u_1} [inst : Fintype ι] {G : ι → Type u_4} [inst_1 : (i : ι) → Group (G i)]
  [inst_2 : (i : ι) → MeasureTheory.MeasureSpace (G i)] [∀ (i : ι), MeasurableInv (G i)]
  [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] [∀ (i : ι), MeasureTheory.volume.IsInvInvariant],
  MeasureTheory.volume.IsInvInvariant
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arctan`.  -/
Orientation.oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V},
  o.oangle x y = ↑(Real.pi / 2) → o.oangle x (x + y) = ↑(Real.arctan (‖y‖ / ‖x‖))
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.coe_support_ofIdealTop : ∀ {X : AlgebraicGeometry.Scheme} (I : Ideal ↑(X.presheaf.obj (Opposite.op ⊤))),
  ↑(AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop I).support = X.zeroLocus ↑I
-- Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Algebra.Generators.localizationAway.eq_1 : ∀ {R : Type u} (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [inst_3 : IsLocalization.Away r S],
  Algebra.Generators.localizationAway S r =
    { val := fun x => IsLocalization.Away.invSelf r,
      σ' := fun s =>
        MvPolynomial.C (IsLocalization.Away.sec r s).1 * MvPolynomial.X () ^ (IsLocalization.Away.sec r s).2,
      aeval_val_σ' := ⋯, algebraMap_eq := ⋯ }
-- Mathlib.Analysis.InnerProductSpace.PiL2
DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv.congr_simp : ∀ {ι : Type u_7} {𝕜 : Type u_8} [inst : RCLike 𝕜] {E : Type u_9} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : FiniteDimensional 𝕜 E] {n : ℕ}
  (hn : Module.finrank 𝕜 E = n) [inst_5 : DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : DirectSum.IsInternal V)
  (hV' : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ),
  DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv hn hV hV' =
    DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv hn hV hV'
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.coeff_of_lt_order_toNat : ∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R}, ∀ n < φ.order.toNat, (PowerSeries.coeff n) φ = 0
-- Mathlib.FieldTheory.KrullTopology
/-- Given a field extension `L/K`, `galBasis K L` is the filter basis on `Gal(L/K)` whose sets
are `Gal(L/E)` for intermediate fields `E` with `E/K` finite dimensional.  -/
galBasis : (K : Type u_1) → (L : Type u_2) → [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → FilterBasis Gal(L/K)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.ext_contains_unit : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {m₁ m₂ : Std.ExtHashMap α Unit},
  (∀ (k : α), m₁.contains k = m₂.contains k) → m₁ = m₂
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.parseToken : String → Lean.PrettyPrinter.FormatterM Lean.Parser.ParserState
-- Mathlib.CategoryTheory.Monoidal.Closed.Enrichment
CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_eHomWhiskerLeft : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.MonoidalClosed C] (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂),
  CategoryTheory.eHomWhiskerLeft C X g = (CategoryTheory.ihom X).map g
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
IsCyclotomicExtension.zeta_isRoot : ∀ (n : ℕ) [inst : NeZero n] (A : Type w) (B : Type z) [inst_1 : CommRing A] [inst_2 : CommRing B] [inst_3 : Algebra A B]
  [inst_4 : IsCyclotomicExtension {n} A B] [IsDomain B] [NeZero ↑n],
  (Polynomial.cyclotomic n B).IsRoot (IsCyclotomicExtension.zeta n A B)
-- Std.Time.Date.Unit.Month
/-- The ordinal value representing the month of May.
 -/
Std.Time.Month.Ordinal.may : Std.Time.Month.Ordinal
-- Init.Data.Int.DivMod.Lemmas
Int.mul_sub_fmod_self_left : ∀ (a b c : ℤ), (a * b - c).fmod a = (-c).fmod a
-- Lean.Meta.InferType
/-- Visit a bvar `e := .bvar vidx`, assuming `offset < e.looseBVarRange`.
 -/
_private.Lean.Meta.InferType.0.Lean.Expr.instantiateBetaRevRange.visitBVar : ℕ → ℕ → Array Lean.Expr → ℕ → ℕ → Lean.Expr
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SavedState.mk.inj : ∀ {«meta» : Lean.Meta.SavedState} {«elab» : Lean.Elab.Term.State} {meta_1 : Lean.Meta.SavedState}
  {elab_1 : Lean.Elab.Term.State},
  { «meta» := «meta», «elab» := «elab» } = { «meta» := meta_1, «elab» := elab_1 } → «meta» = meta_1 ∧ «elab» = elab_1
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.apriori_edist_iterate_efixedPoint_le : ∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α} [inst_1 : CompleteSpace α] (hf : ContractingWith K f)
  {x : α} (hx : edist x (f x) ≠ ⊤) (n : ℕ),
  edist (f^[n] x) (ContractingWith.efixedPoint f hf x hx) ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)