mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Galois.Examples
/-- The inclusion from the complement of the image of `f : X ⟶ Y` into `Y`.  -/
CategoryTheory.FintypeCat.Action.imageComplementIncl : (G : Type u) →
  [inst : Group G] →
    {X Y : Action FintypeCat G} → (f : X ⟶ Y) → CategoryTheory.FintypeCat.Action.imageComplement G f ⟶ Y
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The composition of `C^n` functions at points in domains is `C^n`.  -/
ContDiffWithinAt.comp_of_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E} {t : Set F} {g : F → G}
  {f : E → F} {y : F} (x : E),
  ContDiffWithinAt 𝕜 n g t y →
    ContDiffWithinAt 𝕜 n f s x → Set.MapsTo f s t → f x = y → ContDiffWithinAt 𝕜 n (g ∘ f) s x
-- Std.Http.Protocol.H1.Reader
/-- Checks if the connection should be kept alive for the next message.
 -/
Std.Http.Protocol.H1.Reader.shouldKeepAlive : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader dir → Bool
-- Mathlib.Algebra.Category.AlgCat.Symmetric
AlgCat.instSymmetricCategory : {R : Type u} → [inst : CommRing R] → CategoryTheory.SymmetricCategory (AlgCat R)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_eq_left_iff : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] [IsDomain k] [Module.IsTorsionFree k V1] {p₀ p₁ : P1} {c : k},
  (AffineMap.lineMap p₀ p₁) c = p₀ ↔ p₀ = p₁ ∨ c = 0
-- Mathlib.Logic.Function.Basic
Function.Bijective.comp_right : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β}, Function.Bijective f → Function.Bijective fun g => g ∘ f
-- Mathlib.RingTheory.Trace.Defs
Algebra.trace_comp_trace_of_basis : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type u_4}
  {κ : Type u_5} [Finite ι] [Finite κ] (b : Module.Basis ι R S) (c : Module.Basis κ S T),
  Algebra.trace R S ∘ₗ ↑R (Algebra.trace S T) = Algebra.trace R T
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.InternalCombinators.filterMap.eq_1 : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} (lift : ⦃α : Type w⦄ → m α → n α)
  [inst : Std.Iterator α m β] (f : β → Std.Iterators.PostconditionT n (Option γ)) (it : Std.IterM m β),
  Std.IterM.InternalCombinators.filterMap lift f it = { internalState := { inner := it } }
-- Init.Data.Option.Lemmas
Option.bind.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (x : α → Option β), none.bind x = none
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.«mcasesPat□_» : Lean.ParserDescr
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isNone_maxKey?_eq_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.maxKey?.isNone = t.isEmpty
-- Mathlib.Algebra.Category.Ring.Adjunctions
/-- If `n` is a singleton, `Hom(n, -)` is the identity in `CommRingCat`.  -/
CommRingCat.coyonedaUnique : {n : Type v} → [Unique n] → CommRingCat.coyoneda.obj (Opposite.op n) ≅ CategoryTheory.Functor.id CommRingCat
-- Mathlib.Probability.Kernel.Composition.MeasureComp
/-- Same as `add_comp` except that it uses `⇑κ + ⇑η` instead of `⇑(κ + η)` in order to have
a simp-normal form on the left of the equality.  -/
MeasureTheory.Measure.add_comp' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ η : ProbabilityTheory.Kernel α β}, μ.bind (⇑κ + ⇑η) = μ.bind ⇑κ + μ.bind ⇑η
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
/-- The set of sections associated to a presieve.  -/
AlgebraicGeometry.Scheme.AffineZariskiSite.sectionsOfPresieve : {X : AlgebraicGeometry.Scheme} →
  {U : X.AffineZariskiSite} → CategoryTheory.Presieve U → Set ↑(X.presheaf.obj (Opposite.op U.toOpens))
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.reflectionPerm_sq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι),
  P.reflectionPerm i ^ 2 = 1
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofFVarAliasInfo.sizeOf_spec : ∀ (i : Lean.Elab.FVarAliasInfo), sizeOf (Lean.Elab.Info.ofFVarAliasInfo i) = 1 + sizeOf i
-- Mathlib.Data.ENat.BigOperators
ENat.sum_iSup_of_monotone : ∀ {α : Type u_1} {ι : Type u_2} [inst : Preorder ι] [IsDirectedOrder ι] {s : Finset α} {f : α → ι → ℕ∞},
  (∀ (a : α), Monotone (f a)) → ∑ a ∈ s, iSup (f a) = ⨆ n, ∑ a ∈ s, f a n
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.symm_commRingEquiv : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N],
  AddMonoidAlgebra.commRingEquiv.symm = AddMonoidAlgebra.commRingEquiv
-- Mathlib.Data.Finset.Dedup
List.toFinset_val : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.toFinset.val = ↑l.dedup
-- Mathlib.Topology.UniformSpace.Ascoli
/-- Let `X` be a topological space, `𝔖` a family of compact subsets of `X`, `α` a uniform space,
and `F : ι → (X → α)` a family which is equicontinuous on each `K ∈ 𝔖`. Then, the uniform
structures of uniform convergence on `𝔖` and pointwise convergence on `⋃₀ 𝔖` induce the same
uniform structure on `ι`.

In particular, pointwise convergence and compact convergence coincide on an equicontinuous
subset of `X → α`.

This is a version of `EquicontinuousOn.comap_uniformOnFun_eq` stated in terms of `IsUniformInducing`
for convenience.  -/
EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi' : ∀ {ι : Type u_1} {X : Type u_2} {α : Type u_3} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α}
  [inst_2 : UniformSpace ι] {𝔖 : Set (Set X)},
  (∀ K ∈ 𝔖, IsCompact K) →
    (∀ K ∈ 𝔖, EquicontinuousOn F K) →
      (IsUniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsUniformInducing ((⋃₀ 𝔖).domRestrict ∘ F))
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.final_iff_isIso_colimit_pre : ∀ {C : Type v} [inst : CategoryTheory.Category.{v, v} C] {D : Type v} [inst_1 : CategoryTheory.Category.{v, v} D]
  (F : CategoryTheory.Functor C D),
  F.Final ↔ ∀ (G : CategoryTheory.Functor D (Type v)), CategoryTheory.IsIso (CategoryTheory.Limits.colimit.pre G F)
-- Mathlib.Algebra.BigOperators.Pi
Pi.multiset_prod_apply : ∀ {α : Type u_7} {M : α → Type u_8} [inst : (a : α) → CommMonoid (M a)] (a : α) (s : Multiset ((a : α) → M a)),
  s.prod a = (Multiset.map (fun f => f a) s).prod
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss.0.Polynomial.Chebyshev.sum_exp : ∀ {n : ℕ} {k : ℤ},
  n ≠ 0 →
    ¬2 * ↑n ∣ k →
      ∑ i ∈ Finset.range n, Complex.exp (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑Real.pi) * Complex.I) =
        Complex.exp (↑k / (2 * ↑n) * ↑Real.pi * Complex.I) / (Complex.exp (↑k / ↑n * ↑Real.pi * Complex.I) - 1) *
          ((-1) ^ k - 1)
-- Mathlib.Order.KrullDimension
Order.coheight_ne_zero : ∀ {α : Type u_1} [inst : Preorder α] {x : α}, Order.coheight x ≠ 0 ↔ ¬IsMax x
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.not_ite_beq' : ∀ {w : ℕ} {a b : BitVec (w + 1)} {c : Bool}, ((~~~bif c then b else a) == a) = (c && ~~~b == a)
-- Mathlib.Analysis.Normed.Group.Pointwise
sub_ball : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) (x : E),
  s - Metric.ball x δ = -x +ᵥ Metric.thickening δ s
-- Mathlib.Algebra.CubicDiscriminant
Cubic.monic_of_d_eq_one' : { a := 0, b := 0, c := 0, d := 1 }.toPoly.Monic
-- Mathlib.Algebra.Quaternion
Quaternion.instSMul : {S : Type u_1} → {R : Type u_3} → [inst : CommRing R] → [SMul S R] → SMul S (Quaternion R)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.symm_bijective : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂], Function.Bijective AlgEquiv.symm
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.mul_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} (X : C)
  [self : CategoryTheory.MonObj X],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X)
      CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X X).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.MonObj.mul) CategoryTheory.MonObj.mul)
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.equivPair.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (M i)] (i : ι),
  Monoid.CoprodI.Word.equivPair i =
    { toFun := fun w => ↑(Monoid.CoprodI.Word.equivPairAux✝ i w), invFun := Monoid.CoprodI.Word.rcons, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.coe_neg : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommGroup R]
  (s : HahnSeries.SummableFamily Γ R α), ⇑(-s) = -⇑s
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.union_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp}, t₁.union t₂ = t₁ ∪ t₂
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.getElem_toArray_eq : ∀ {α : Type u} {r : Std.Rci α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxi.IsAlwaysFinite α] {i : ℕ} {h : i < r.toArray.size},
  r.toArray[i] = (Std.PRange.succMany? i r.lower).get ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
_private.Mathlib.CategoryTheory.Limits.Shapes.Reflexive.0.CategoryTheory.Limits.reflexivePair.match_3.eq_1 : ∀ (motive : (X Y : CategoryTheory.Limits.WalkingReflexivePair) → (X ⟶ Y) → Sort u_1)
  (x : CategoryTheory.Limits.WalkingReflexivePair)
  (h_1 :
    (x : CategoryTheory.Limits.WalkingReflexivePair) → motive x x (CategoryTheory.Limits.WalkingReflexivePair.Hom.id x))
  (h_2 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero
        CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
  (h_3 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero
        CategoryTheory.Limits.WalkingReflexivePair.Hom.right)
  (h_4 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.zero CategoryTheory.Limits.WalkingReflexivePair.one
        CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion)
  (h_5 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.one
        CategoryTheory.Limits.WalkingReflexivePair.Hom.rightCompReflexion)
  (h_6 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.one
        CategoryTheory.Limits.WalkingReflexivePair.Hom.leftCompReflexion),
  (match x, x, CategoryTheory.Limits.WalkingReflexivePair.Hom.id x with
    | x, .(x), CategoryTheory.Limits.WalkingReflexivePair.Hom.id .(x) => h_1 x
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.zero),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.left => h_2 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.zero),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.right => h_3 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.zero), .(CategoryTheory.Limits.WalkingReflexivePair.one),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion => h_4 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.one),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.rightCompReflexion => h_5 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.one),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.leftCompReflexion => h_6 ()) =
    h_1 x
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin_zero_of_notMem_closure : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜}, x ∉ closure s → derivWithin f s x = 0
-- Std.Http.Data.Request
/-- Sets the request target/URI for the request being built
 -/
Std.Http.Request.Builder.uri! : Std.Http.Request.Builder → String → Std.Http.Request.Builder
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegral.zsmul : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B] {x : B},
  IsIntegral R x → ∀ (n : ℤ), IsIntegral R (n • x)
-- Lean.Meta.Tactic.Grind.Proof
/-- Constructs a congruence proof for `lhs` and `rhs` using `congr`, `congrFun`, and `congrArg`.
This function assumes `isCongrDefaultProofTarget` returned `true`.
 -/
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.mkCongrDefaultProof : Lean.Expr → Lean.Expr → Bool → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.Algebra.LinearRecurrence
/-- Coefficients of the linear recurrence  -/
LinearRecurrence.coeffs : {R : Type u_1} → [inst : CommSemiring R] → (self : LinearRecurrence R) → Fin self.order → R
-- Mathlib.Algebra.Category.Grp.FilteredColimits
/-- The colimit of `F ⋙ forget₂ CommGrpCat GrpCat` in the category `GrpCat`.
In the following, we will show that this has the structure of a _commutative_ group.
 -/
CommGrpCat.FilteredColimits.G : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] → [CategoryTheory.IsFiltered J] → CategoryTheory.Functor J CommGrpCat → GrpCat
-- Lean.Meta.Tactic.Grind.EMatch
/-- Matches pattern `p` with term `e` with respect to choice `c`.
We traverse the equivalence class of `e` looking for applications compatible with `p`.
For each candidate application, we match the arguments and may update `c`s assignments and constraints.
We add the updated choices to the choice stack.
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.processMatch : Lean.Meta.Grind.EMatch.Choice →
  Option Lean.Meta.Grind.GenPatternInfo → Lean.Expr → Lean.Expr → Lean.Meta.Grind.EMatch.M Unit
-- Mathlib.Data.List.Pairwise
List.Pairwise.rel_getLast_of_rel_getLast_getLast : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α} {a : α},
  List.Pairwise R l → ∀ (ha : a ∈ l), R (l.getLast ⋯) (l.getLast ⋯) → R a (l.getLast ⋯)
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_iff_of_equivalence : ∀ {C : Type u_1} {D : Type u_2} {D' : Type u_3} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} D']
  [inst_3 : CategoryTheory.Category.{v_4, u_4} H] (L : CategoryTheory.Functor C D) (L' : CategoryTheory.Functor C D')
  (F : CategoryTheory.Functor C H) (E : D ≌ D') (eL : L.comp E.functor ≅ L') (Y : D) (Y' : D')
  (e : E.functor.obj Y ≅ Y'), L.HasPointwiseLeftKanExtensionAt F Y ↔ L'.HasPointwiseLeftKanExtensionAt F Y'
-- Init.Data.List.Impl
/-- Auxiliary for `take`: `take.go l xs n acc = acc.toList ++ take n xs`,
unless `n ≥ xs.length` in which case it returns `l`.  -/
_private.Init.Data.List.Impl.0.List.takeTR.go : {α : Type u_1} → List α → List α → ℕ → Array α → List α
-- Mathlib.Analysis.Normed.Ring.Basic
Finset.nnnorm_prod_le : ∀ {ι : Type u_4} {α : Type u_5} [inst : NormedCommRing α] [NormOneClass α] (s : Finset ι) (f : ι → α),
  ‖∏ i ∈ s, f i‖₊ ≤ ∏ i ∈ s, ‖f i‖₊
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
not_linearIndependent_iffₒₛ : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : LinearOrder R] [CanonicallyOrderedAdd R] [AddRightReflectLE R] [IsCancelAdd M],
  ¬LinearIndependent R v ↔ ∃ s t f, Disjoint s t ∧ ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i ∧ ∃ i ∈ s, 0 < f i
-- ProofWidgets.Cancellable
/-- Transforms a request handler returning `β`
into one that returns immediately with a `RequestId`.

The ID uniquely identifies the running request:
its results can be retrieved using `checkRequest`,
and it can be cancelled using `cancelRequest`.  -/
ProofWidgets.mkCancellable : {β : Type} →
  {α : Sort u_1} →
    [Lean.Server.RpcEncodable β] →
      (α → Lean.Server.RequestM (Lean.Server.RequestTask β)) →
        α → Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.RequestId)
-- Mathlib.Algebra.Prime.Defs
Prime.dvd_or_dvd : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p : M}, Prime p → ∀ {a b : M}, p ∣ a * b → p ∣ a ∨ p ∣ b
-- Mathlib.Data.Fin.Tuple.Basic
Fin.snoc_rev : ∀ {α : Sort u_3} {n : ℕ} (a : α) (f : Fin n → α) (i : Fin (n + 1)), Fin.snoc f a i.rev = Fin.cons a (f ∘ Fin.rev) i
-- Init.Data.String.Termination
String.Slice.Pos.Down.mk.injEq : ∀ {s : String.Slice} (inner inner_1 : s.Pos), ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.bind : ∀ {n : ℕ} {f : List.Vector ℕ n →. ℕ} {g : List.Vector ℕ (n + 1) →. ℕ},
  Nat.Partrec' f → Nat.Partrec' g → Nat.Partrec' fun v => (f v).bind fun a => g (a ::ᵥ v)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.toContinuousMap_toContinuousMonoidHom : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] {F : Type u_7} [inst_4 : FunLike F A B] [inst_5 : MonoidHomClass F A B]
  [inst_6 : ContinuousMapClass F A B] (f : F), ↑↑f = ↑f
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.proj_comp_of_subset : ∀ {I : Type u} (J K : I → Prop) [inst : (i : I) → Decidable (J i)] [inst_1 : (i : I) → Decidable (K i)],
  (∀ (i : I), J i → K i) →
    Profinite.NobelingProof.Proj J ∘ Profinite.NobelingProof.Proj K = Profinite.NobelingProof.Proj J
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.dist_self_center : ∀ (z : UpperHalfPlane) (r : ℝ), dist ↑z ↑(z.center r) = z.im * (Real.cosh r - 1)
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.add_left_cancel : ∀ {M : Type u_1} [inst : AddMonoid M] {a b c : M}, IsAddUnit a → a + b = a + c → b = c
-- Mathlib.Analysis.Normed.Algebra.Unitization
/-- The natural equivalence between `Unitization 𝕜 A` and `𝕜 × A` as a uniform equivalence.  -/
Unitization.uniformEquivProd : {𝕜 : Type u_1} →
  {A : Type u_2} → [inst : NontriviallyNormedField 𝕜] → [inst_1 : NonUnitalNormedRing A] → Unitization 𝕜 A ≃ᵤ 𝕜 × A
-- Lean.Environment
_private.Lean.Environment.0.Lean.readModuleDataPartsOfMod.unsafe_impl_8 : Lean.ModuleData × Lean.CompactedRegion →
  Lean.ModuleData × Lean.CompactedRegion → System.FilePath → IO (Lean.ModuleData × Lean.CompactedRegion)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.map_apply : ∀ {ι : Type u_1} {𝓕 : Filter ι} {G : ι → Type u_9} {H : ι → Type u_10} {C : (i : ι) → Set (G i)}
  {D : (i : ι) → Set (H i)} (φ : (i : ι) → G i → H i) (hφ : ∀ᶠ (i : ι) in 𝓕, Set.MapsTo (φ i) (C i) (D i))
  (x : RestrictedProduct (fun i => G i) (fun i => C i) 𝓕) (j : ι), (RestrictedProduct.map φ hφ x) j = φ j (x j)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.unop_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F.op), c.unop.pt = Opposite.unop c.pt
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.mem_positive : ∀ (R : Type u_1) (E : Type u_2) [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : PartialOrder E] [inst_5 : IsOrderedAddMonoid E] [inst_6 : Module R E]
  [inst_7 : PosSMulMono R E] {x : E}, x ∈ PointedCone.positive R E ↔ 0 ≤ x
-- Mathlib.Algebra.Category.AlgCat.Monoidal
AlgCat.hom_hom_rightUnitor : ∀ {R : Type u} [inst : CommRing R] {M : AlgCat R},
  AlgCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom =
    ↑(Algebra.TensorProduct.rid (↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (AlgCat R))) R ↑M)
-- Mathlib.RingTheory.Smooth.Basic
/-- Smooth is stable under composition.  -/
Algebra.Smooth.comp : ∀ (R : Type u_4) [inst : CommRing R] (A : Type u_5) (B : Type u_6) [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B] [Algebra.Smooth R A]
  [Algebra.Smooth A B], Algebra.Smooth R B
-- Mathlib.Data.List.Nodup
List.rel_nodup : ∀ {α : Type u} {β : Type v} {r : α → β → Prop},
  Relator.BiUnique r → Relator.LiftFun (List.Forall₂ r) (fun x1 x2 => x1 ↔ x2) List.Nodup List.Nodup
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_mono : ∀ {r₁ r₂ : ℝ}, r₁ ≤ r₂ → r₁.toNNReal ≤ r₂.toNNReal
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkCoyoneda_obj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X : Cᵒᵖ}
  {Y Y' : C} (g : Y ⟶ Y') (f : (CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X).obj Y),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X).map g)) f =
    CategoryTheory.shrinkCoyonedaObjObjEquiv.symm
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkCoyonedaObjObjEquiv f) g)
-- Init.GrindInstances.Ring.UInt
UInt32.intCast_ofNat : ∀ (x : ℕ), ↑(OfNat.ofNat x) = OfNat.ofNat x
-- Mathlib.Algebra.Order.Floor.Div
zero_ceilDiv : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [inst_4 : SMulZeroClass α β] [inst_5 : CeilDiv α β] (a : α), 0 ⌈/⌉ a = 0
-- Mathlib.Topology.Closure
/-- Complement to a singleton is dense if and only if the singleton is not an open set.  -/
dense_compl_singleton_iff_not_open : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X}, Dense {x}ᶜ ↔ ¬IsOpen {x}
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_image : ∀ (R : Type uR) {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (s : Set A),
  Algebra.adjoin R (⇑f '' s) = Subalgebra.map f (Algebra.adjoin R s)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_inf : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (S T : AddSubmonoid M) (f : F),
  Function.Injective ⇑f → AddSubmonoid.map f (S ⊓ T) = AddSubmonoid.map f S ⊓ AddSubmonoid.map f T
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous
at `b`, then the derivative of `u ↦ ∫ x in a..u, f x` at `b` equals `f b`.  -/
intervalIntegral.deriv_integral_right : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
      ContinuousAt f b → deriv (fun u => ∫ (x : ℝ) in a..u, f x) b = f b
-- Mathlib.Analysis.Analytic.Basic
AnalyticWithinAt.congr_of_eventuallyEq : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {s : Set E}
  {x : E}, AnalyticWithinAt 𝕜 f s x → g =ᶠ[nhdsWithin x s] f → g x = f x → AnalyticWithinAt 𝕜 g s x
-- Init.Meta
/-- `simp_all!` is shorthand for `simp_all` with `autoUnfold := true`.
This will unfold applications of functions defined by pattern matching, when one of the patterns applies.
This can be used to partially evaluate many definitions.  -/
Lean.Parser.Tactic.simpAllAutoUnfold : Lean.ParserDescr