mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.getElem?_toList_eq : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α] {i : ℕ},
  r.toList[i]? = Option.filter (fun x => decide (x ≤ r.upper)) (Std.PRange.succMany? (i + 1) r.lower)
-- Lean.KeyedDeclsAttribute
/-- Builtin attribute name, if any (e.g., `builtin_term_elab)  -/
Lean.KeyedDeclsAttribute.Def.builtinName : {γ : Type} → Lean.KeyedDeclsAttribute.Def γ → Lean.Name
-- Mathlib.RepresentationTheory.Coinvariants
Representation.Coinvariants.map_comp : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {X : Type u_5} [inst : CommRing k] [inst_1 : Monoid G]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  [inst_6 : AddCommGroup X] [inst_7 : Module k X] {ρ : Representation k G V} {τ : Representation k G W}
  (υ : Representation k G X) (φ : ρ.IntertwiningMap τ) (ψ : τ.IntertwiningMap υ),
  Representation.Coinvariants.map τ υ ψ ∘ₗ Representation.Coinvariants.map ρ τ φ =
    Representation.Coinvariants.map ρ υ (ψ.comp φ)
-- Mathlib.Analysis.SpecificLimits.Normed
/-- The term norms of any convergent series are bounded by a constant.  -/
exists_norm_le_of_cauchySeq : ∀ {α : Type u_1} [inst : SeminormedAddCommGroup α] {f : ℕ → α},
  (CauchySeq fun n => ∑ k ∈ Finset.range n, f k) → ∃ C, ∀ (n : ℕ), ‖f n‖ ≤ C
-- Mathlib.RingTheory.WittVector.Basic
WittVector.mapFun.pow : ∀ {p : ℕ} {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Fact (Nat.Prime p)]
  (f : R →+* S) (x : WittVector p R) (n : ℕ), WittVector.mapFun (⇑f) (x ^ n) = WittVector.mapFun (⇑f) x ^ n
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Equivariant functions :
When `φ : M → N` is a function, and types `X` and `Y` are endowed with additive actions
of `M` and `N`, a function `f : X → Y` is `φ`-equivariant if `f (m +ᵥ x) = (φ m) +ᵥ (f x)`.  -/
AddActionHom : {M : Type u_8} →
  {N : Type u_9} → (M → N) → (X : Type u_10) → [VAdd M X] → (Y : Type u_11) → [VAdd N Y] → Type (max u_10 u_11)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.induce_singleton_eq_top : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V), SimpleGraph.induce {v} G = ⊤
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.coe_smul : ∀ {ι : Type u_1} {G : Type u_3} {k : Type u_5} {V : Type u_6} [inst : AddCommGroup V] [inst_1 : Ring k]
  [inst_2 : Module k V] [inst_3 : Group G] [inst_4 : DistribMulAction G V] [inst_5 : SMulCommClass G k V] (a : G)
  (b : AffineBasis ι k V), ⇑(a • b) = a • ⇑b
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsGEOfNat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ), t.IsGE 0 n
-- Mathlib.Topology.NhdsKer
nhdsKer_nhdsKer : ∀ {X : Type u_2} [inst : TopologicalSpace X] (s : Set X), nhdsKer (nhdsKer s) = nhdsKer s
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
_private.Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme.0.AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjIso_hom_ι : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjIso✝ I U).hom
      ((TopologicalSpace.Opens.map I.gluedTo.base).obj ↑U).ι =
    I.glueData.ι U
-- Mathlib.Algebra.Group.TypeTags.Finite
instInfiniteAdditive : ∀ {α : Type u} [h : Infinite α], Infinite (Additive α)
-- Mathlib.Algebra.Order.Floor.Semifield
Nat.floor_div_ofNat : ∀ {K : Type u_2} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [inst_3 : FloorSemiring K]
  (a : K) (n : ℕ) [inst_4 : n.AtLeastTwo], ⌊a / OfNat.ofNat n⌋₊ = ⌊a⌋₊ / OfNat.ofNat n
-- Init.Data.Iterators.Basic
/-- This theorem is used by a `decreasing_trivial` extension. It powers automatic termination proofs
with `IterM.finitelyManySteps`.
 -/
Std.IterM.TerminationMeasures.Finite.rel_of_skip : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {it it' : Std.IterM m β},
  it.IsPlausibleStep (Std.IterStep.skip it') → { it := it' }.Rel { it := it }
-- Mathlib.Topology.PartitionOfUnity
/-- A collection of bump functions `f i` is subordinate to a family of sets `U i` indexed by the
same type if for each `i` the closure of the support of `f i` is a subset of `U i`.  -/
BumpCovering.IsSubordinate : {ι : Type u} → {X : Type v} → [inst : TopologicalSpace X] → {s : Set X} → BumpCovering ι X s → (ι → Set X) → Prop
-- Mathlib.Algebra.Category.Grp.Basic
CategoryTheory.Iso.commGroupIsoToMulEquiv.eq_1 : ∀ {X Y : CommGrpCat} (i : X ≅ Y),
  i.commGroupIsoToMulEquiv = (CommGrpCat.Hom.hom i.hom).toMulEquiv (CommGrpCat.Hom.hom i.inv) ⋯ ⋯
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.fromOfGlobalSections_resLE : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {X : AlgebraicGeometry.Scheme} (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤)))
  (hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤) {r : A} {n : ℕ} (hn : 0 < n) (hr : r ∈ 𝒜 n),
  AlgebraicGeometry.Scheme.Hom.resLE (AlgebraicGeometry.Proj.fromOfGlobalSections 𝒜 f hf)
      (AlgebraicGeometry.Proj.basicOpen 𝒜 r) (X.basicOpen (f r)) ⋯ =
    AlgebraicGeometry.Proj.toBasicOpenOfGlobalSections 𝒜 f ⋯ hn hr
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.isSome_apply_of_mem_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α} (h : k ∈ Std.DHashMap.filterMap f m),
  (f (m.getKey k ⋯) (Std.DHashMap.Const.get m k ⋯)).isSome = true
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.utf8Size_assemble₂ : ∀ {w x : UInt8} {c : Char}, ByteArray.utf8DecodeChar?.assemble₂ w x = some c → c.utf8Size = 2
-- Mathlib.Data.FunLike.Basic
DFunLike.ext_iff : ∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] {f g : F}, f = g ↔ ∀ (x : α), f x = g x
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.cpow_ofReal_re : ∀ (x : ℂ) (y : ℝ), (x ^ ↑y).re = ‖x‖ ^ y * Real.cos (x.arg * y)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.balanceₘ.match_3.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (r : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (l : Std.DTreeMap.Internal.Impl α β) →
      ¬r.size > Std.DTreeMap.Internal.delta * l.size → l.size > Std.DTreeMap.Internal.delta * r.size → Sort u_3)
  (size : ℕ) (lk : α) (lv : β lk) (ll lr : Std.DTreeMap.Internal.Impl α β)
  (h : ¬r.size > Std.DTreeMap.Internal.delta * (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size)
  (h_1 : (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size > Std.DTreeMap.Internal.delta * r.size)
  (h_1_1 :
    (h : ¬r.size > Std.DTreeMap.Internal.delta * Std.DTreeMap.Internal.Impl.leaf.size) →
      (h_2 : Std.DTreeMap.Internal.Impl.leaf.size > Std.DTreeMap.Internal.delta * r.size) →
        motive Std.DTreeMap.Internal.Impl.leaf h h_2)
  (h_2 :
    (size : ℕ) →
      (lk : α) →
        (lv : β lk) →
          (ll lr : Std.DTreeMap.Internal.Impl α β) →
            (h : ¬r.size > Std.DTreeMap.Internal.delta * (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size) →
              (h_2 : (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size > Std.DTreeMap.Internal.delta * r.size) →
                motive (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr) h h_2),
  (match Std.DTreeMap.Internal.Impl.inner size lk lv ll lr, h, h_1 with
    | Std.DTreeMap.Internal.Impl.leaf, h, h_3 => h_1_1 h h_3
    | Std.DTreeMap.Internal.Impl.inner size lk lv ll lr, h, h_3 => h_2 size lk lv ll lr h h_3) =
    h_2 size lk lv ll lr h h_1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryCofan.IsColimit.inr_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y W : C} {s : CategoryTheory.Limits.BinaryCofan X Y}
  (h : CategoryTheory.Limits.IsColimit s) (f : X ⟶ W) (g : Y ⟶ W),
  CategoryTheory.CategoryStruct.comp s.inr (CategoryTheory.Limits.BinaryCofan.IsColimit.desc h f g) = g
-- Mathlib.Topology.Instances.Nat
Nat.instIsOrderBornology : IsOrderBornology ℕ
-- Mathlib.CategoryTheory.Action.Limits
Action.forget₂_preservesZeroMorphisms : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] {FV : V → V → Type u_3} {CV : V → Type u_4}
  [inst_3 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [inst_4 : CategoryTheory.ConcreteCategory V FV],
  (CategoryTheory.forget₂ (Action V G) V).PreservesZeroMorphisms
-- Aesop.Stats.Basic
Aesop.ForwardStateStats : Type
-- Std.Internal.UV.System
Std.Internal.UV.System.instReprRUsage.repr : Std.Internal.UV.System.RUsage → ℕ → Std.Format
-- Mathlib.Data.ENNReal.Operations
ENNReal.pow_le_pow_left : ∀ {a b : ENNReal} {n : ℕ}, a ≤ b → a ^ n ≤ b ^ n
-- Lean.Meta.Match.Basic
Lean.Meta.Match.CounterExample : Type
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.associatorNatIsoRight_hom_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) (d : B) (X : c ⟶ d),
  (CategoryTheory.Bicategory.associatorNatIsoRight f g d).hom.app X = (CategoryTheory.Bicategory.associator f g X).hom
-- Init.Data.Iterators.Basic
Std.Iterators.ProductivenessRelation.mk.inj : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {inst : Std.Iterator α m β}
  {Rel : Std.IterM m β → Std.IterM m β → Prop} {wf : WellFounded Rel}
  {subrelation : ∀ {it it' : Std.IterM m β}, it'.IsPlausibleSkipSuccessorOf it → Rel it' it}
  {Rel_1 : Std.IterM m β → Std.IterM m β → Prop} {wf_1 : WellFounded Rel_1}
  {subrelation_1 : ∀ {it it' : Std.IterM m β}, it'.IsPlausibleSkipSuccessorOf it → Rel_1 it' it},
  { Rel := Rel, wf := wf, subrelation := subrelation } = { Rel := Rel_1, wf := wf_1, subrelation := subrelation_1 } →
    Rel = Rel_1
-- Mathlib.Order.Preorder.Chain
IsChain.image_iso_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} [inst : LE α] [inst_1 : LE β] {φ : α ≃o β},
  IsChain (fun x1 x2 => x1 ≤ x2) (⇑φ '' s) ↔ IsChain (fun x1 x2 => x1 ≤ x2) s
-- Lean.PrettyPrinter.Delaborator.SubExpr
/-- The positioning scheme guarantees that there will be an infinite number of extra positions
which are never used by `Expr`s. The `HoleIterator` always points at the next such "hole".
We use these to attach additional `Elab.Info`.

Note: these positions are incompatible with `Lean.SubExpr.Pos.push` since the iterator
will eventually yield every child of every returned position.  -/
Lean.PrettyPrinter.Delaborator.SubExpr.nextExtraPos : {m : Type → Type} →
  [Monad m] → [MonadStateOf Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator m] → m Lean.SubExpr.Pos
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Finite
CategoryTheory.Limits.instHasFiniteProductsFunctor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {K : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] [CategoryTheory.Limits.HasFiniteProducts C],
  CategoryTheory.Limits.HasFiniteProducts (CategoryTheory.Functor K C)
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- `getFVarIdCandidates fv name lctx` takes an input an `FVarId`, a `Name` and a `LocalContext`.
It returns an array of guesses for a "best fit" `FVarId` in the given `LocalContext`.
The first entry of the array is the input `FVarId` `fv`, if it is present.
The next entry of the array is the `FVarId` with the given `Name`, if present.

Usually, the first entry of the returned array is "the best approximation" to `(fv, name)`.  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.getFVarIdCandidates : Lean.FVarId → Lean.Name → Lean.LocalContext → Array Lean.FVarId
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Given a cofork over `∐ I.left ⇉ ∐ I.right`, we may obtain a multicofork.  -/
CategoryTheory.Limits.Multicofork.ofSigmaCofork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      {I : CategoryTheory.Limits.MultispanIndex J C} →
        {c : CategoryTheory.Limits.Cofan I.left} →
          {hc : CategoryTheory.Limits.IsColimit c} →
            {d : CategoryTheory.Limits.Cofan I.right} →
              CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc) →
                CategoryTheory.Limits.Multicofork I
-- Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
/-- The finite module represented by an object of the type `FGModuleRepr R`, which is the quotient
of `Fin n → R` (i.e. `Rⁿ`) by the submodule `S` provided.  -/
FGModuleRepr.repr : {R : Type u} → [inst : Ring R] → FGModuleRepr R → Type u
-- Mathlib.MeasureTheory.MeasurableSpace.Pi
/-- Boxes formed by π-systems form a π-system.  -/
IsPiSystem.pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {C : (i : ι) → Set (Set (α i))},
  (∀ (i : ι), IsPiSystem (C i)) → IsPiSystem (Set.univ.pi '' Set.univ.pi C)
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.TriangleIndexData.mk.injEq : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {J : Type u_4} [inst : Zero I₂] {r : I₁ × I₂ × I₃ → J}
  {π : I₁ × I₃ → J} (p₁₂ : I₁ × I₂ → I₁) (hp₁₂ : ∀ (i : I₁ × I₂ × I₃), π (p₁₂ (i.1, i.2.1), i.2.2) = r i)
  (p₂₃ : I₂ × I₃ → I₃) (hp₂₃ : ∀ (i : I₁ × I₂ × I₃), π (i.1, p₂₃ i.2) = r i) (h₁ : ∀ (i₁ : I₁), p₁₂ (i₁, 0) = i₁)
  (h₃ : ∀ (i₃ : I₃), p₂₃ (0, i₃) = i₃) (p₁₂_1 : I₁ × I₂ → I₁)
  (hp₁₂_1 : ∀ (i : I₁ × I₂ × I₃), π (p₁₂_1 (i.1, i.2.1), i.2.2) = r i) (p₂₃_1 : I₂ × I₃ → I₃)
  (hp₂₃_1 : ∀ (i : I₁ × I₂ × I₃), π (i.1, p₂₃_1 i.2) = r i) (h₁_1 : ∀ (i₁ : I₁), p₁₂_1 (i₁, 0) = i₁)
  (h₃_1 : ∀ (i₃ : I₃), p₂₃_1 (0, i₃) = i₃),
  ({ p₁₂ := p₁₂, hp₁₂ := hp₁₂, p₂₃ := p₂₃, hp₂₃ := hp₂₃, h₁ := h₁, h₃ := h₃ } =
      { p₁₂ := p₁₂_1, hp₁₂ := hp₁₂_1, p₂₃ := p₂₃_1, hp₂₃ := hp₂₃_1, h₁ := h₁_1, h₃ := h₃_1 }) =
    (p₁₂ = p₁₂_1 ∧ p₂₃ = p₂₃_1)
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateAddSubgroup.one_le : ∀ {G : Type u_1} [inst : AddGroup G] {A : Set G} {K : ℝ}, IsApproximateAddSubgroup K A → 1 ≤ K
-- Mathlib.Algebra.Module.Congruence.Defs
VAddCon.instVAddQuotient.eq_1 : ∀ {S : Type u_2} (M : Type u_3) [inst : VAdd S M] (c : VAddCon S M),
  VAddCon.instVAddQuotient M c = { vadd := fun s => Quotient.map (fun x => s +ᵥ x) ⋯ }
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_mulMon_nc_go : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ) (m : Lean.Grind.CommRing.Mon)
  (p acc : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.mulMon_nc.go k m p acc) =
    ↑k * Lean.Grind.CommRing.Mon.denote ctx m * Lean.Grind.CommRing.Poly.denote ctx p +
      Lean.Grind.CommRing.Poly.denote ctx acc
-- Mathlib.NumberTheory.KummerDedekind
KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S} {I : Ideal R}
  [inst_3 : IsDomain R] [inst_4 : IsIntegrallyClosed R] [inst_5 : IsDedekindDomain S]
  [inst_6 : Module.IsTorsionFree R S] (hI : I.IsMaximal) (hI' : I ≠ ⊥)
  (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (hx' : IsIntegral R x),
  KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx' =
    KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx'
-- Mathlib.MeasureTheory.OuterMeasure.Defs
MeasureTheory.OuterMeasure.iUnion_nat : ∀ {α : Type u_2} (self : MeasureTheory.OuterMeasure α) (s : ℕ → Set α),
  Pairwise (Function.onFun Disjoint s) → self.measureOf (⋃ i, s i) ≤ ∑' (i : ℕ), self.measureOf (s i)
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.instIsCardinalFilteredCarrierObjPartOrdEmbIsCardinalFiltered : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ),
  CategoryTheory.IsCardinalFiltered (↑J.obj) κ
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.affineSpan_pair_altitudeFoot_eq_altitude : ∀ {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) (i : Fin (n + 1)),
  line[ℝ, s.altitudeFoot i, s.points i] = s.altitude i
-- Mathlib.RingTheory.PowerSeries.PiTopology
PowerSeries.WithPiTopology.tendsto_trunc_atTop : ∀ (R : Type u_1) [inst : TopologicalSpace R] [inst_1 : CommSemiring R] (f : PowerSeries R),
  Filter.Tendsto (fun d => ↑((PowerSeries.trunc d) f)) Filter.atTop (nhds f)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.orderIsoRpow_apply : ∀ (y : ℝ) (hy : 0 < y) (x : NNReal), (NNReal.orderIsoRpow y hy) x = x ^ y
-- Init.Data.String.Basic
String.Pos.ofToSlice_next_toSlice : ∀ {s : String} {pos : s.Pos} {h : pos.toSlice ≠ s.toSlice.endPos},
  String.Pos.ofToSlice (pos.toSlice.next h) = pos.next ⋯
-- Mathlib.Order.Hom.Bounded
BotHom.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : Bot α] [inst_1 : Bot β] (toFun : α → β) (map_bot' : toFun ⊥ = ⊥)
  (toFun_1 : α → β) (map_bot'_1 : toFun_1 ⊥ = ⊥),
  ({ toFun := toFun, map_bot' := map_bot' } = { toFun := toFun_1, map_bot' := map_bot'_1 }) = (toFun = toFun_1)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for signed shift right on `BitVec`.  -/
BitVec.reduceSShiftRight : Lean.Meta.Simp.DSimproc
-- Lean.Meta.Sym.AbstractS
/-- Similar to `mkForallFVars`, but uses the more efficient `abstractFVars` and `abstractFVarsRange`,
and makes the same assumption made by these functions.
 -/
Lean.Meta.Sym.mkForallFVarsS : Array Lean.Expr → Lean.Expr → Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.Data.Sum.Interval
Sum.Lex.Ico_inr_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : LocallyFiniteOrderTop α] [inst_5 : LocallyFiniteOrderBot β] (b₁ b₂ : β),
  Finset.Ico (Sum.inrₗ b₁) (Sum.inrₗ b₂) =
    Finset.map (Function.Embedding.inr.trans toLex.toEmbedding) (Finset.Ico b₁ b₂)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If the products `W ⨯ X` and `Y ⨯ Z` exist, then every pair of morphisms `f : W ⟶ Y` and
`g : X ⟶ Z` induces a morphism `prod.map f g : W ⨯ X ⟶ Y ⨯ Z`.  -/
CategoryTheory.Limits.prod.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      [inst_1 : CategoryTheory.Limits.HasBinaryProduct W X] →
        [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z] → (W ⟶ Y) → (X ⟶ Z) → (W ⨯ X ⟶ Y ⨯ Z)
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.toRange_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)} (p : F' ⟶ F)
  {Z : CategoryTheory.Functor C (Type w)} (h : F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.toRange p)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.range p).ι h) =
    CategoryTheory.CategoryStruct.comp p h
-- Mathlib.Algebra.Lie.Basic
/-- The Lie bracket as a biadditive map.

Usually one will have coefficients and `LieModule.toEnd` will be more useful.  -/
LieRingModule.toEnd : (L : Type v) → (M : Type w) → [inst : LieRing L] → [inst_1 : AddCommGroup M] → [LieRingModule L M] → L →+ M →+ M
-- Init.Data.SInt.Lemmas
Int32.toNatClampNeg_sub_of_le : ∀ {a b : Int32}, 0 ≤ b → b ≤ a → (a - b).toNatClampNeg = a.toNatClampNeg - b.toNatClampNeg
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.Step.lift : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} {β : Type v} [inst : AddGroup β] {f : α → β},
  FreeAddGroup.Red.Step L₁ L₂ → FreeAddGroup.Lift.aux f L₁ = FreeAddGroup.Lift.aux f L₂
-- Batteries.Control.Lemmas
ReaderT.run_tryCatch : ∀ {ε : Type u_1} {m : Type u_2 → Type u_3} {ρ α : Type u_2} [inst : MonadExceptOf ε m] (body : ReaderT ρ m α)
  (handler : ε → ReaderT ρ m α) (ctx : ρ),
  (tryCatch body handler).run ctx = tryCatch (body.run ctx) fun x => (handler x).run ctx
-- Mathlib.Order.Directed
DirectedOn.pi : ∀ {ι : Type u_5} {α : ι → Type u_6} {r : (i : ι) → α i → α i → Prop} {d : (i : ι) → Set (α i)},
  (∀ (i : ι), DirectedOn (r i) (d i)) → DirectedOn (fun x y => ∀ (i : ι), r i (x i) (y i)) (Set.univ.pi d)
-- Mathlib.Geometry.Convex.Cone.Basic
/-- The image of a convex cone under an `R`-linear map is a convex cone.  -/
ConvexCone.map : {R : Type u_2} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : Semiring R] →
        [inst_1 : PartialOrder R] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R M] → [inst_5 : Module R N] → (M →ₗ[R] N) → ConvexCone R M → ConvexCone R N
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthSup_sup : ∀ {u v : ℕ → ENNReal}, ExpGrowth.expGrowthSup (u ⊔ v) = max (ExpGrowth.expGrowthSup u) (ExpGrowth.expGrowthSup v)
-- Lean.Elab.InfoTree.Main
Lean.Elab.ContextInfo.toPPContext : Lean.Elab.ContextInfo → Lean.LocalContext → Lean.PPContext
-- Mathlib.Geometry.Convex.Cone.Basic
Submodule.coe_toConvexCone : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (C : Submodule R M), ↑C.toConvexCone = ↑C
-- Mathlib.Data.Set.Subsingleton
Set.Nontrivial.choose_snd_mem : ∀ {α : Type u} {s : Set α} (hs : s.Nontrivial), hs.choose.2 ∈ s
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.adjoin.powerBasis_dim : ∀ {K : Type u} [inst : Field K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] {x : L} (hx : IsIntegral K x),
  (IntermediateField.adjoin.powerBasis hx).dim = (minpoly K x).natDegree
-- Mathlib.CategoryTheory.Category.PartialFun
typeToPartialFunIsoPartialFunToPointed_inv_app_toFun : ∀ (X : Type u_1) (a : (typeToPointed.obj X).X), (typeToPartialFunIsoPartialFunToPointed.inv.app X).toFun a = a
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
/-- `DomMulAct.mk` as a homeomorphism.  -/
DomMulAct.mkHomeomorph : {M : Type u_1} → [inst : TopologicalSpace M] → M ≃ₜ Mᵈᵐᵃ
-- Mathlib.Algebra.Group.Hom.Instances
/-- Composition of monoid morphisms (`MonoidHom.comp`) as a monoid morphism.

Note that unlike `MonoidHom.comp_hom'` this requires commutativity of `N`.  -/
MonoidHom.compHom : {M : Type uM} →
  {N : Type uN} →
    {P : Type uP} →
      [inst : MulOneClass M] → [inst_1 : CommMonoid N] → [inst_2 : CommMonoid P] → (N →* P) →* (M →* N) →* M →* P
-- Init.Data.SInt.Basic
/-- Obtains the `Int32` that is 2's complement equivalent to the `UInt32`.  -/
UInt32.toInt32 : UInt32 → Int32
-- Init.Data.Vector.Lemmas
Vector.pop_eq_of_push_eq : ∀ {α : Type u_1} {n : ℕ} {a b : α} {xs ys : Vector α n}, xs.push a = ys.push b → xs = ys
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.descFZero.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Y Z : C} (f : Z ⟶ Y) (I : CategoryTheory.InjectiveResolution Y)
  (J : CategoryTheory.InjectiveResolution Z),
  CategoryTheory.InjectiveResolution.descFZero f I J =
    CategoryTheory.Injective.factorThru (CategoryTheory.CategoryStruct.comp f (I.ι.f 0)) (J.ι.f 0)
-- Init.Data.BitVec.Lemmas
BitVec.getElem?_eq : ∀ {w : ℕ} (l : BitVec w) (i : ℕ), l[i]? = if h : i < w then some l[i] else none
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.mapA.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (as : List α) → motive (a :: as)) → motive x