mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- For `Unique one`, the equivariant map from `one ↪ α` to `α`.  -/
MulActionHom.oneEmbeddingMap : {G : Type u_1} →
  {α : Type u_2} → [inst : Group G] → [inst_1 : MulAction G α] → {one : Type u_5} → [Unique one] → (one ↪ α) →ₑ[id] α
-- Batteries.Tactic.Lint.Frontend
/-- `low`: only print failing checks, print nothing on success.  -/
Batteries.Tactic.Lint.LintVerbosity.low : Batteries.Tactic.Lint.LintVerbosity
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.edist_eq_iSup : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → EDist (β i)] (f g : PiLp ⊤ β),
  edist f g = ⨆ i, edist (f.ofLp i) (g.ofLp i)
-- Mathlib.Order.Nat
/-- `Nat.find` is the minimum natural number satisfying a predicate `p`.  -/
Nat.isLeast_find : ∀ {p : ℕ → Prop} [inst : DecidablePred p] (hp : ∃ n, p n), IsLeast {n | p n} (Nat.find hp)
-- Mathlib.CategoryTheory.Sites.Subcanonical
/-- See also `map_yonedaEquiv'` for a more general version.  -/
CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X Y : C} {F : CategoryTheory.Sheaf J (Type (max v v'))}
  (f : (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).obj X ⟶ F) (g : Y ⟶ X),
  (CategoryTheory.ConcreteCategory.hom (F.obj.map g.op)) (J.uliftYonedaEquiv f) =
    (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op Y))) { down := g }
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Poly
-- Mathlib.Algebra.Ring.Periodic
Function.periodic_with_period_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : AddZeroClass α] (f : α → β), Function.Periodic f 0
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleIcc_to_cycleRange : ∀ {n : ℕ} {i j k : Fin n} (hij : i ≤ j) (kin : k ∈ Set.range ⇑(Fin.natAdd_castLEEmb ⋯)),
  (i.cycleIcc j) k =
    (Fin.natAdd_castLEEmb ⋯) (((j - i).castLT ⋯).cycleRange ((Fin.natAdd_castLEEmb ⋯).toEquivRange.symm ⟨k, kin⟩))
-- Batteries.Data.Nat.Lemmas
Nat.recAux_succ : ∀ {motive : ℕ → Sort u_1} (zero : motive 0) (succ : (n : ℕ) → motive n → motive (n + 1)) (n : ℕ),
  Nat.recAux zero succ (n + 1) = succ n (Nat.recAux zero succ n)
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.forget₂_addCommGrp_additive : ∀ {R : Type u} [inst : Ring R], (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).Additive
-- Mathlib.Topology.Order.LowerUpperTopology
/-- Left-closed right-infinite intervals $[a, ∞)$ are closed in the lower topology.  -/
Topology.IsLower.instClosedIciTopology : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLower α], ClosedIciTopology α
-- Mathlib.Data.FunLike.IsApply
FunLike.coe_pow : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Pow F M]
  [inst_2 : Pow β M] [IsPowApply M F α β] (f : F) (n : M), ⇑(f ^ n) = ⇑f ^ n
-- Init.Data.List.ToArray
Array.swap.eq_1 : ∀ {α : Type u} (xs : Array α) (i j : ℕ) (hi : i < xs.size) (hj : j < xs.size),
  xs.swap i j hi hj = (xs.set i xs[j] hi).set j xs[i] ⋯
-- Mathlib.Combinatorics.Matroid.Loop
/-- `M.IsNonloop e` means that `e` is an element of `M.E` but not a loop of `M`.  -/
Matroid.IsNonloop : {α : Type u_1} → Matroid α → α → Prop
-- Init.Data.String.Defs
/-- The proof that `offset` is valid for the string `s`.  -/
String.Pos.isValid : ∀ {s : String} (self : s.Pos), String.Pos.Raw.IsValid s self.offset
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
CategoryTheory.Over.conePost_obj_π_app : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) (i : J) (c : CategoryTheory.Limits.Cone F) (X : CategoryTheory.Over i),
  ((CategoryTheory.Over.conePost F i).obj c).π.app X = CategoryTheory.Over.homMk (c.π.app X.left) ⋯
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- Given a `CompSource` `cs`, `cs.flatten` maps an assumption index
to the number of copies of that assumption that appear in the history of `cs`.

For example, suppose `cs` is produced by scaling assumption 2 by 5,
and adding to that the sum of assumptions 1 and 2.
`cs.flatten` maps `1 ↦ 1, 2 ↦ 6`.
 -/
Mathlib.Tactic.Linarith.CompSource.flatten : Mathlib.Tactic.Linarith.CompSource → Std.HashMap ℕ ℕ
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.eq_adjoint_iff_basis_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] {ι : Type u_5} (b : Module.Basis ι 𝕜 F)
  (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E),
  A = LinearMap.adjoint B ↔ ∀ (i : ι) (x : E), inner 𝕜 (A x) (b i) = inner 𝕜 x (B (b i))
-- Mathlib.Topology.LocallyClosed
/-- **Alias** of the reverse direction of `coborder_eq_univ_iff`. -/
IsClosed.coborder_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsClosed s → coborder s = Set.univ
-- Init.MetaTypes
/-- When `index` (default : `true`) is `false`, `simp` will only use the root symbol
to find candidate `simp` theorems. It approximates Lean 3 `simp` behavior.
 -/
Lean.Meta.DSimp.Config.index : Lean.Meta.DSimp.Config → Bool
-- Mathlib.Logic.Equiv.Sum
Equiv.sumCongr_apply : ∀ {α₁ : Type u_9} {α₂ : Type u_10} {β₁ : Type u_11} {β₂ : Type u_12} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (a : α₁ ⊕ β₁),
  (ea.sumCongr eb) a = Sum.map (⇑ea) (⇑eb) a
-- Lean.Data.Lsp.Basic
Lean.Lsp.instDecidableEqMarkupContent.decEq : (x x_1 : Lean.Lsp.MarkupContent) → Decidable (x = x_1)
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.Bool.not_beq_not : ∀ (a b : Bool), ((!a) == !b) = (a == b)
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.RightExtension.instIsClosedUnderIsomorphismsIsPointwiseRightKanExtensionAt : ∀ {C : Type u_1} {D : Type u_2} {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_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.RightExtension F),
  E.isPointwiseRightKanExtensionAt.IsClosedUnderIsomorphisms
-- Mathlib.Computability.RegularExpressions
_private.Mathlib.Computability.RegularExpressions.0.RegularExpression.deriv.match_1.eq_4 : ∀ {α : Type u_1} (motive : RegularExpression α → α → Sort u_2) (P Q : RegularExpression α) (a : α)
  (h_1 : (x : α) → motive RegularExpression.zero x) (h_2 : (x : α) → motive RegularExpression.epsilon x)
  (h_3 : (a₁ a₂ : α) → motive (RegularExpression.char a₁) a₂)
  (h_4 : (P Q : RegularExpression α) → (a : α) → motive (P.plus Q) a)
  (h_5 : (P Q : RegularExpression α) → (a : α) → motive (P.comp Q) a)
  (h_6 : (P : RegularExpression α) → (a : α) → motive P.star a),
  (match P.plus Q, a with
    | RegularExpression.zero, x => h_1 x
    | RegularExpression.epsilon, x => h_2 x
    | RegularExpression.char a₁, a₂ => h_3 a₁ a₂
    | P.plus Q, a => h_4 P Q a
    | P.comp Q, a => h_5 P Q a
    | P.star, a => h_6 P a) =
    h_4 P Q a
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitEpi.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (section_ : Y ⟶ X)
  (id :
    autoParam (CategoryTheory.CategoryStruct.comp section_ f = CategoryTheory.CategoryStruct.id Y)
      CategoryTheory.SplitEpi.id._autoParam)
  (section__1 : Y ⟶ X)
  (id_1 :
    autoParam (CategoryTheory.CategoryStruct.comp section__1 f = CategoryTheory.CategoryStruct.id Y)
      CategoryTheory.SplitEpi.id._autoParam),
  ({ section_ := section_, id := id } = { section_ := section__1, id := id_1 }) = (section_ = section__1)
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.Hom.ext_iff : ∀ {A B : GrpCat} {x y : A.Hom B}, x = y ↔ x.hom' = y.hom'
-- Lean.DocString.Markdown
_private.Lean.DocString.Markdown.0.Lean.Doc.quoteCode : String → String
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
CategoryTheory.WalkingIso.fromIso_map_zero_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (e : X ≅ Y)
  (f : CategoryTheory.WalkingIso.zero ⟶ CategoryTheory.WalkingIso.zero),
  (CategoryTheory.WalkingIso.fromIso e).map f = CategoryTheory.CategoryStruct.id X
-- Lean.Elab.ConfigEval.DeriveEvalExpr
/-- Creates an `EvalExpr` instance that uses `Meta.evalExpr` to compile and evaluate the expression.  -/
Lean.Elab.ConfigEval.deriveEvalExprUsingMetaEval : Option (Lean.TSyntax `Lean.Parser.Command.visibility) →
  Lean.TSyntax `Lean.Parser.Term.attrKind → Lean.Syntax → Lean.Syntax → Lean.Expr → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsUniversal.brecOn : ∀ {L : FirstOrder.Language} {α : Type u'} {motive : {n : ℕ} → (a : L.BoundedFormula α n) → a.IsUniversal → Prop} {n : ℕ}
  {a : L.BoundedFormula α n} (t : a.IsUniversal),
  (∀ {n : ℕ} (a : L.BoundedFormula α n) (t : a.IsUniversal),
      FirstOrder.Language.BoundedFormula.IsUniversal.below t → motive a t) →
    motive a t
-- Mathlib.Order.Comparable
CompRel.of_gt : ∀ {α : Type u_1} {a b : α} [inst : Preorder α], b < a → CompRel (fun x1 x2 => x1 ≤ x2) a b
-- Mathlib.Data.Matrix.Basic
AddMonoidHom.mapMatrix_smul : ∀ {m : Type u_2} {n : Type u_3} {A : Type u_10} {α : Type u_11} {β : Type u_12} [inst : Monoid A]
  [inst_1 : AddZeroClass α] [inst_2 : AddMonoid β] [inst_3 : DistribMulAction A β] (a : A) (f : α →+ β),
  (a • f).mapMatrix = a • f.mapMatrix
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example : Type
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.instAddZeroClass : {R : Type u_2} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [inst_2 : AddCommMonoid M] → [inst_3 : Module R M] → AddZeroClass (ConvexCone R M)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α},
  k ∈ Std.ExtDHashMap.filterMap f m ↔ ∃ (h : k ∈ m), (f k (m.get k h)).isSome = true
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.mker_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoidHom.mker (AddMonoidHom.inl M N) = ⊥
-- Mathlib.Geometry.Convex.ConvexSpace.AffineMap
/-- The type of (bundled) affine maps between two convex spaces.  -/
Convexity.ConvexSpace.AffineMap : (R : Type u_1) →
  [inst : PartialOrder R] →
    [inst_1 : Semiring R] →
      [inst_2 : IsStrictOrderedRing R] →
        (X : Type u_2) → (Y : Type u_3) → [Convexity.ConvexSpace R X] → [Convexity.ConvexSpace R Y] → Type (max u_2 u_3)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to0.instInhabitedΛ' : {Γ : Type u_1} →
  {Λ : Type u_2} →
    [Inhabited Λ] → {σ : Type u_3} → [Inhabited σ] → (M : Λ → Turing.TM1.Stmt Γ Λ σ) → Inhabited (Turing.TM1to0.Λ' M)
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
SSet.Truncated.instCategoryHomotopyCategory₂ : {A : SSet.Truncated 2} → [A.Quasicategory₂] → CategoryTheory.Category.{u_1, u_1} A.HomotopyCategory₂
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.distinguished_iff_of_isZero₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  (T : CategoryTheory.Pretriangulated.Triangle C),
  CategoryTheory.Limits.IsZero T.obj₃ →
    (T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ CategoryTheory.IsIso T.mor₁)
-- Mathlib.Algebra.Polynomial.Div
Polynomial.X_dvd_sub_C : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R}, Polynomial.X ∣ p - Polynomial.C (p.coeff 0)
-- Mathlib.Topology.DiscreteSubset
IsDiscrete.image_of_isOpenMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
  IsDiscrete s → IsOpenMap f → Function.Injective f → IsDiscrete (f '' s)
-- Mathlib.AlgebraicGeometry.Geometrically.Connected
AlgebraicGeometry.instSurjectiveOfGeometricallyConnected : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.GeometricallyConnected f],
  AlgebraicGeometry.Surjective f
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.symmetry'_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (P Q : C) {Z : C} (h : P ⊞ Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst) h) =
    h
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.deg_zero : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} (x : Submonoid A) [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι]
  [inst_5 : GradedRing 𝒜], HomogeneousLocalization.NumDenSameDeg.deg 0 = 0
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans_obj_V : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (α : F ⟶ G)
  (V : CategoryTheory.Endofunctor.Coalgebra F),
  ((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans α).obj V).V = V.V
-- Init.Data.Int.Order
Int.sub_lt_sub_right : ∀ {a b : ℤ}, a < b → ∀ (c : ℤ), a - c < b - c
-- Lean.Parser.Command
/-- `open Foo in tacs` (the tactic) acts like `open Foo` at command level,
but it opens a namespace only within the tactics `tacs`.  -/
Lean.Parser.Tactic.open : Lean.Parser.Parser
-- Mathlib.Combinatorics.Additive.DoublingConst
/-- The doubling constant `σ[A, B]` of two finsets `A` and `B` in a group is `|A + B| / |A|`.  -/
Combinatorics.Additive.«termσ[_,_]» : Lean.ParserDescr
-- Mathlib.RingTheory.FractionalIdeal.Extended
FractionalIdeal.extendedHom_injective : ∀ (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A]
  [inst_2 : CommRing B] [inst_3 : IsDomain B] [inst_4 : Algebra A B] [inst_5 : Module.IsTorsionFree A B]
  [inst_6 : Field K] [inst_7 : Field L] [inst_8 : Algebra A K] [inst_9 : Algebra B L] [inst_10 : IsFractionRing A K]
  [inst_11 : IsFractionRing B L] [inst_12 : Algebra K L] [inst_13 : Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsDedekindDomain A] [IsDedekindDomain B],
  Function.Injective fun I => (FractionalIdeal.extendedHom L B) I
-- Mathlib.Algebra.Free
FreeSemigroup.instMonad : Monad FreeSemigroup
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- Pythagorean theorem, subtracting vectors, vector angle form.  -/
InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq' : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  InnerProductGeometry.angle x y = Real.pi / 2 → ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
-- Mathlib.Algebra.Module.Presentation.Tensor
_private.Mathlib.Algebra.Module.Presentation.Tensor.0.Module.Relations.Solution.tensor.match_1.eq_1 : ∀ {A : Type u_5} [inst : CommRing A] {relations₁ : Module.Relations A} {relations₂ : Module.Relations A}
  (motive : (relations₁.tensor relations₂).G → Sort u_6) (g₁ : relations₁.G) (g₂ : relations₂.G)
  (h_1 : (g₁ : relations₁.G) → (g₂ : relations₂.G) → motive (g₁, g₂)),
  (match (g₁, g₂) with
    | (g₁, g₂) => h_1 g₁ g₂) =
    h_1 g₁ g₂
-- Mathlib.RingTheory.Noetherian.Orzech
/-- Any surjective endomorphism of a Noetherian module is bijective.  -/
IsNoetherian.bijective_of_surjective_endomorphism : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherian R M]
  (f : M →ₗ[R] M), Function.Surjective ⇑f → Function.Bijective ⇑f
-- Mathlib.Analysis.Calculus.Deriv.Mul
Differentiable.finsetProd : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {ι : Type u_2} {𝔸' : Type u_3} [inst_1 : NormedCommRing 𝔸']
  [inst_2 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, Differentiable 𝕜 (f i)) → Differentiable 𝕜 (∏ i ∈ u, f i)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
UniformCauchySeqOn.div : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {s : Set β},
  UniformCauchySeqOn f l s → UniformCauchySeqOn f' l s → UniformCauchySeqOn (f / f') l s
-- Mathlib.Geometry.Euclidean.Projection
/-- Subtracting the `orthogonalProjection` from `p` produces a result
in the orthogonal direction.  -/
EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] (p : P),
  p -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p) ∈ s.directionᗮ
-- Lean.Widget.UserWidget
/-- Save the data of a panel widget which will be displayed whenever the text cursor is on `stx`.

`hash` must be as in `WidgetInstance.ofHash`.

For panel widgets, the Lean infoview appends additional fields to the `props` object:
see https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/userWidget.tsx#L145.  -/
Lean.Widget.savePanelWidgetInfo : UInt64 → StateM Lean.Server.RpcObjectStore Lean.Json → Lean.Syntax → Lean.CoreM Unit
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_inter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_contains : Std.DTreeMap.Internal.Impl.contains k (m₁.inter m₂ ⋯) = true},
  (m₁.inter m₂ ⋯).getKey k h_contains = m₁.getKey k ⋯
-- Mathlib.Algebra.GCDMonoid.Basic
normalize_eq_normalize_iff_associated : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] {a b : α},
  normalize a = normalize b ↔ Associated a b
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
/-- This is a slightly more convenient method to verify that a fork is a weak limit cone. It
only asks for a proof of facts that carry any mathematical content  -/
CategoryTheory.Limits.Fork.IsWeakLimit.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} →
      {f g : X ⟶ Y} →
        (t : CategoryTheory.Limits.Fork f g) →
          (lift : (s : CategoryTheory.Limits.Fork f g) → s.pt ⟶ t.pt) →
            (∀ (s : CategoryTheory.Limits.Fork f g), CategoryTheory.CategoryStruct.comp (lift s) t.ι = s.ι) →
              CategoryTheory.Limits.IsWeakLimit t
-- Mathlib.Algebra.Module.Equiv.Basic
/-- Ring equivalence between additive group endomorphisms of an `AddCommGroup` `A` and
`ℤ`-module endomorphisms of `A.`  -/
addMonoidEndRingEquivInt : (A : Type u_9) → [inst : AddCommGroup A] → AddMonoid.End A ≃+* Module.End ℤ A
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.unop_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : F ⟶ G) (X : C),
  (CategoryTheory.NatTrans.unop α).app X = (α.app (Opposite.op X)).unop
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.instAddMonoidWithOne : {σ : Type u_1} → {R : Type u_2} → [Semiring R] → AddMonoidWithOne (MvPowerSeries σ R)
-- Mathlib.LinearAlgebra.Basis.Flag
Module.Basis.flag_covBy : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {n : ℕ}
  (b : Module.Basis (Fin n) K V) (i : Fin n), b.flag i.castSucc ⋖ b.flag i.succ
-- Mathlib.Topology.Compactness.SigmaCompact
/-- Countable unions of σ-compact sets are σ-compact.  -/
isSigmaCompact_biUnion : ∀ {X : Type u_1} {ι : Type u_3} [inst : TopologicalSpace X] {s : Set ι} {S : ι → Set X},
  s.Countable → (∀ i ∈ s, IsSigmaCompact (S i)) → IsSigmaCompact (⋃ i ∈ s, S i)
-- Std.Data.HashMap.RawLemmas
/-- Simpler variant of `getElem!_filter` when `LawfulBEq` is available.  -/
Std.HashMap.Raw.getElem!_filter' : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [LawfulBEq α]
  [inst_3 : Inhabited β] {f : α → β → Bool} {k : α},
  m.WF → (Std.HashMap.Raw.filter f m)[k]! = (Option.filter (f k) m[k]?).get!
-- Init.Data.String.Lemmas.FindPos
String.posLE_toSlice : ∀ {s : String} {p : String.Pos.Raw}, s.toSlice.posLE p = (s.posLE p).toSlice
-- Mathlib.CategoryTheory.GlueData
/-- For each `i : J`, an object `U i`  -/
CategoryTheory.GlueData.U : {C : Type u₁} → [inst : CategoryTheory.Category.{v, u₁} C] → (self : CategoryTheory.GlueData C) → self.J → C
-- Mathlib.Analysis.Calculus.Conformal.NormedSpace
conformal_const_smul : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] [inst_1 : NormedSpace ℝ X] {c : ℝ}, c ≠ 0 → Conformal fun x => c • x
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Spec.map.hcongr_3 : ∀ (R R' : CommRingCat),
  R = R' →
    ∀ (S S' : CommRingCat),
      S = S' → ∀ (f : R ⟶ S) (f' : R' ⟶ S'), f ≍ f' → AlgebraicGeometry.Spec.map f ≍ AlgebraicGeometry.Spec.map f'
-- Init.Data.Array.Lemmas
Array.contains_eq_mem : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {xs : Array α}, xs.contains a = decide (a ∈ xs)
-- Init.Data.Slice.Array.Lemmas
_private.Init.Data.Slice.Array.Lemmas.0.Array.toSubarray.eq_1 : ∀ {α : Type u} (as : Array α) (start stop : ℕ),
  as.toSubarray start stop =
    if h₂ : stop ≤ as.size then
      if h₁ : start ≤ stop then
        {
          internalRepresentation :=
            { array := as, start := start, stop := stop, start_le_stop := h₁, stop_le_array_size := h₂ } }
      else
        {
          internalRepresentation :=
            { array := as, start := stop, stop := stop, start_le_stop := ⋯, stop_le_array_size := h₂ } }
    else
      if h₁ : start ≤ as.size then
        {
          internalRepresentation :=
            { array := as, start := start, stop := as.size, start_le_stop := h₁, stop_le_array_size := ⋯ } }
      else
        {
          internalRepresentation :=
            { array := as, start := as.size, stop := as.size, start_le_stop := ⋯, stop_le_array_size := ⋯ } }
-- Mathlib.Control.Monad.Writer
WriterT.run_tryCatch : ∀ {α ω : Type u} {M : Type u → Type u_2} {ε : Type u_1} [inst : MonadExceptOf ε M] (cmd : WriterT ω M α)
  (c : ε → WriterT ω M α), (tryCatch cmd c).run = tryCatch cmd.run fun e => (c e).run
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
ContDiffPointwiseHolderAt.continuousLinearMap_comp : ∀ {E : Type u_1} {F : Type u_2} {G : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {k : ℕ} {α : ↑unitInterval} {f : E → F} {a : E},
  ContDiffPointwiseHolderAt k α f a → ∀ (g : F →L[ℝ] G), ContDiffPointwiseHolderAt k α (⇑g ∘ f) a
-- Mathlib.Order.Filter.Prod
Filter.prod_inf : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g₁ g₂ : Filter β}, f ×ˢ (g₁ ⊓ g₂) = f ×ˢ g₁ ⊓ f ×ˢ g₂
-- Init.Data.Int.Lemmas
Int.add_neg_eq_sub : ∀ {a b : ℤ}, a + -b = a - b
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey!_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {v : β}, (t.insertIfNew k v).maxKey! = t.maxKey?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey?_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (Std.DTreeMap.Raw.Const.alter t k f).getKey? k =
        if (f (Std.DTreeMap.Raw.Const.get? t k)).isSome = true then some k else none