mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Tower
/-- The `R`-algebra morphism `A → End (M)` corresponding to the representation of the algebra `A`
on the `B`-module `M`.

This is a stronger version of `DistribSMul.toLinearMap`, and could also have been
called `Algebra.toModuleEnd`.

The typeclasses correspond to the situation where the types act on each other as
```
R ----→ B
| ⟍     |
|   ⟍   |
↓     ↘ ↓
A ----→ M
```
where the diagram commutes, the action by `R` commutes with everything, and the action by `A` and
`B` on `M` commute.

Typically this is most useful with `B = R` as `Algebra.lsmul R R A : A →ₐ[R] Module.End R M`.
However this can be used to get the fact that left-multiplication by `A` is right `A`-linear, and
vice versa, as
```lean
example : A →ₐ[R] Module.End Aᵐᵒᵖ A := Algebra.lsmul R Aᵐᵒᵖ A
example : Aᵐᵒᵖ →ₐ[R] Module.End A A := Algebra.lsmul R A A
```
respectively; though `LinearMap.mulLeft` and `LinearMap.mulRight` can also be used here.
 -/
Algebra.lsmul : (R : Type u) →
  {A : Type w} →
    (B : Type u₁) →
      (M : Type v₁) →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] →
                  [inst_5 : AddCommMonoid M] →
                    [inst_6 : Module R M] →
                      [inst_7 : Module A M] →
                        [inst_8 : Module B M] →
                          [IsScalarTower R A M] →
                            [inst_10 : IsScalarTower R B M] → [SMulCommClass A B M] → A →ₐ[R] Module.End B M
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.coweightHom_injective : ∀ {ι : 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),
  Function.Injective ⇑(RootPairing.Hom.coweightHom P)
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
WeakDual.CharacterSpace.instFunLike : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [inst_2 : ContinuousAdd 𝕜] →
          [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
            [inst_4 : NonUnitalNonAssocSemiring A] →
              [inst_5 : TopologicalSpace A] → [inst_6 : Module 𝕜 A] → FunLike (↑(WeakDual.characterSpace 𝕜 A)) A 𝕜
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_sub : ∀ {n : Type u_3} {R : Type u_6} [inst : Fintype n] [inst_1 : AddCommGroup R] (A B : Matrix n n R),
  (A - B).trace = A.trace - B.trace
-- Mathlib.CategoryTheory.Filtered.Grothendieck
CategoryTheory.instIsFilteredOrEmptyGrothendieckOfαCategoryObjCat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat)
  [CategoryTheory.IsFilteredOrEmpty C] [∀ (c : C), CategoryTheory.IsFilteredOrEmpty ↑(F.obj c)],
  CategoryTheory.IsFilteredOrEmpty (CategoryTheory.Grothendieck F)
-- Mathlib.Algebra.Group.Action.Defs
Function.Injective.vaddCommClass : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [inst : VAdd M α] [inst_1 : VAdd N α] [inst_2 : VAdd M β]
  [inst_3 : VAdd N β] [VAddCommClass M N β] {f : α → β},
  Function.Injective f →
    (∀ (c : M) (x : α), f (c +ᵥ x) = c +ᵥ f x) → (∀ (c : N) (x : α), f (c +ᵥ x) = c +ᵥ f x) → VAddCommClass M N α
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- Any three points in a cospherical set are affinely independent.  -/
EuclideanGeometry.Cospherical.affineIndependent_of_mem_of_ne : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : Set P},
  EuclideanGeometry.Cospherical s →
    ∀ {p₁ p₂ p₃ : P}, p₁ ∈ s → p₂ ∈ s → p₃ ∈ s → p₁ ≠ p₂ → p₁ ≠ p₃ → p₂ ≠ p₃ → AffineIndependent ℝ ![p₁, p₂, p₃]
-- Aesop.Rule.Name
Aesop.instToJsonPhaseName : Lean.ToJson Aesop.PhaseName
-- Std.Data.String.ToInt
_private.Std.Data.String.ToInt.0.String.Slice.isInt.eq_1 : ∀ (s : String.Slice),
  s.isInt =
    match s.dropPrefix? '-' with
    | some rest => rest.isNat
    | none => s.isNat
-- Mathlib.Order.UpperLower.Relative
isRelUpperSet_true_iff_isUpperSet : ∀ {α : Type u_1} {s : Set α} [inst : LE α], (IsRelUpperSet s fun x => True) ↔ IsUpperSet s
-- Mathlib.Data.Nat.Cast.Basic
nsmul_eq_mul' : ∀ {α : Type u_1} [inst : NonAssocSemiring α] (a : α) (n : ℕ), n • a = a * ↑n
-- Batteries.Data.List.Lemmas
List.length_insertP : ∀ {α : Type u_1} (p : α → Bool) (a : α) (l : List α), (List.insertP p a l).length = l.length + 1
-- Mathlib.Data.Set.Card
Set.infinite_iff_infinite_of_encard_eq_encard : ∀ {α : Type u_1} {s t : Set α}, s.encard = t.encard → (s.Infinite ↔ t.Infinite)
-- Mathlib.Analysis.InnerProductSpace.Spectrum
LinearMap.IsSymmetric.eigenvalues_eq_eigenvalues_iff : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} {E' : Type u_3} [inst_4 : NormedAddCommGroup E']
  [inst_5 : InnerProductSpace 𝕜 E'] [inst_6 : FiniteDimensional 𝕜 E'] {T' : E' →ₗ[𝕜] E'} (hT : T.IsSymmetric)
  (hn : Module.finrank 𝕜 E = n) (hT' : T'.IsSymmetric) (hn' : Module.finrank 𝕜 E' = n),
  hT.eigenvalues hn = hT'.eigenvalues hn' ↔ T.charpoly = T'.charpoly
-- Init.Data.Iterators.Basic
Std.Iter.toIterM_comp_toIter : ∀ {α β : Type w}, Std.Iter.toIterM ∘ Std.IterM.toIter = id
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.addAndFinalizeInductiveDecl : Lean.Elab.Command.AddAndFinalizeContext✝ → Lean.Elab.TermElabM Lean.Elab.Command.FinalizeContext✝
-- Mathlib.Algebra.GroupWithZero.Basic
/-- A structure that has zero and pow is reduced if it has no nonzero nilpotent elements.  -/
IsReduced : (R : Type u_5) → [Zero R] → [Pow R ℕ] → Prop
-- Mathlib.Tactic.Order.Graph.Tarjan
/-- `id[v]` is the index of the vertex `v` in the DFS traversal.  -/
Mathlib.Tactic.Order.Graph.TarjanState.id : Mathlib.Tactic.Order.Graph.TarjanState → Std.HashMap ℕ ℕ
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.setValue.eq_1 : ∀ {α : Sort u_1} {β : Sort u_2} (f : α ↪ β) (a : α) (b : β) [inst : (a' : α) → Decidable (a' = a)]
  [inst_1 : (a' : α) → Decidable (f a' = b)],
  f.setValue a b = { toFun := fun a' => if a' = a then b else if f a' = b then f a else f a', inj' := ⋯ }
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.instAddCommMonoid : {R : Type u_1} →
  {E₁ : Type u_2} →
    {E₂ : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid E₁] →
          [inst_2 : PartialOrder E₁] →
            [inst_3 : AddCommMonoid E₂] →
              [inst_4 : PartialOrder E₂] →
                [inst_5 : Module R E₁] → [inst_6 : Module R E₂] → [IsOrderedAddMonoid E₂] → AddCommMonoid (E₁ →ₚ[R] E₂)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constGetEntryGT!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.getEntryGT! t₁ k = Std.DTreeMap.Raw.Const.getEntryGT! t₂ k
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.eq_zero_iff_forall_coroot'_eq_zero : ∀ {ι : 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) [P.IsRootSystem]
  {x : M}, x = 0 ↔ ∀ (i : ι), (P.coroot' i) x = 0
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.brecOn_1.eq : ∀ {motive_1 : Lean.Elab.Tactic.RCases.RCasesPatt → Sort u} {motive_2 : List Lean.Elab.Tactic.RCases.RCasesPatt → Sort u}
  (t : List Lean.Elab.Tactic.RCases.RCasesPatt) (F_1 : (t : Lean.Elab.Tactic.RCases.RCasesPatt) → t.below → motive_1 t)
  (F_2 : (t : List Lean.Elab.Tactic.RCases.RCasesPatt) → Lean.Elab.Tactic.RCases.RCasesPatt.below_1 t → motive_2 t),
  Lean.Elab.Tactic.RCases.RCasesPatt.brecOn_1 t F_1 F_2 =
    F_2 t (Lean.Elab.Tactic.RCases.RCasesPatt.brecOn_1.go t F_1 F_2).2
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.flattenList.match_1.splitter : {n : ℕ} →
  (motive : List (BitVec n) → Sort u_1) →
    (xs : List (BitVec n)) →
      (Unit → motive []) → ((x : BitVec n) → (rest : List (BitVec n)) → motive (x :: rest)) → motive xs
-- Mathlib.Order.BoundedOrder.Basic
Prod.instTop.eq_1 : ∀ (α : Type u) (β : Type v) [inst : Top α] [inst_1 : Top β], Prod.instTop α β = { top := (⊤, ⊤) }
-- Mathlib.RingTheory.Congruence.Defs
RingCon.hasZSMul : {R : Type u_1} → [inst : AddGroup R] → [inst_1 : Mul R] → (c : RingCon R) → SMul ℤ c.Quotient
-- Mathlib.Tactic.Attr.Register
/-- "Simp attribute for lemmas about `RCLike`"  -/
Parser.Attr.rclike_simps : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Matrix.Kronecker
/-- The Kronecker tensor product. This is just a shorthand for `kroneckerMap (⊗ₜ)`.
Prefer the notation `⊗ₖₜ` rather than this definition.  -/
Kronecker.«term_⊗ₖₜ[_]_» : Lean.TrailingParserDescr
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.UnsatProof.cooper.sizeOf_spec : ∀ (c₁ c₂ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr) (c₃ : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.UnsatProof.cooper c₁ c₂ c₃) = 1 + sizeOf c₁ + sizeOf c₂ + sizeOf c₃
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `strictMonoOn_comp_ofDual_iff`. -/
StrictAntiOn.dual_left : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictAntiOn f s → StrictMonoOn (f ∘ ⇑OrderDual.ofDual) s
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.gluing_f : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (x x_1 : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).f x x_1 =
    CategoryTheory.Limits.pullback.fst
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f x) f) g) (𝒰.f x))
      (𝒰.f x_1)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
/-- The map `M.sections → N.sections` induced by a morphism `M ⟶ N` of sheaves of modules.  -/
SheafOfModules.sectionsMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} → {M N : SheafOfModules R} → (M ⟶ N) → M.sections → N.sections
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.iSup_genWeightSpaceOf_eq_top : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [LieModule.IsTriangularizable R L M] (x : L),
  ⨆ φ, LieModule.genWeightSpaceOf M φ x = ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- `HasBiproduct F` expresses the mere existence of a bicone which is
simultaneously a limit and a colimit of the diagram `F`.  -/
CategoryTheory.Limits.HasBiproduct : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] → [CategoryTheory.Limits.HasZeroMorphisms C] → (J → C) → Prop
-- Lean.Expr
/-- A mapping from free variable identifiers to values of type `α`.
This is a persistent data structure implemented using `Std.TreeMap`.  -/
Lean.FVarIdMap : Type → Type
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey?_eq_none_iff_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {l : List ((a : α) × β a)},
  Std.Internal.List.maxKey? l = none ↔ l.isEmpty = true
-- Mathlib.Order.Hom.WithTopBot
/-- Adjoins a `⊤` to the domain and codomain of an `InfHom`.  -/
InfHom.withTop : {α : Type u_1} →
  {β : Type u_2} →
    [inst : SemilatticeInf α] → [inst_1 : SemilatticeInf β] → InfHom α β → InfTopHom (WithTop α) (WithTop β)
-- Init.Data.Array.Basic
/-- Checks whether `a` is an element of `as`, using `==` to compare elements.

`Array.contains` is a synonym that takes the array before the element.

For verification purposes, `Array.elem` is simplified to `Array.contains`.

Example:
* `Array.elem 3 #[1, 4, 2, 3, 3, 7] = true`
* `Array.elem 5 #[1, 4, 2, 3, 3, 7] = false`
 -/
Array.elem : {α : Type u} → [BEq α] → α → Array α → Bool
-- Mathlib.CategoryTheory.GradedObject
/-- The isomorphism of `J`-graded objects `X.mapObj p ≅ Y.mapObj p` induced by an
isomorphism `X ≅ Y` of graded objects and a map `p : I → J`.  -/
CategoryTheory.GradedObject.mapIso : {I : Type u_1} →
  {J : Type u_2} →
    {C : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_4} C] →
        {X Y : CategoryTheory.GradedObject I C} →
          (X ≅ Y) → (p : I → J) → [inst_1 : X.HasMap p] → [inst_2 : Y.HasMap p] → X.mapObj p ≅ Y.mapObj p
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.diff_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ m₃ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF), m₃.WF → m₁.Equiv m₂ → (m₁.diff m₃ ⋯).Equiv (m₂.diff m₃ ⋯)
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
Mathlib.Tactic.BicategoryCoherence.liftHom₂Id : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      (f : a ⟶ b) →
        [inst_1 : Mathlib.Tactic.BicategoryCoherence.LiftHom f] →
          Mathlib.Tactic.BicategoryCoherence.LiftHom₂ (CategoryTheory.CategoryStruct.id f)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.lift_sInf : ∀ (s : Set Cardinal.{v}), Cardinal.lift.{u, v} (sInf s) = sInf (Cardinal.lift.{u, v} '' s)
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- **Alias** of the reverse direction of `summable_norm_iff`.

---

In a finite-dimensional vector space over `ℝ`, the series `∑ x, ‖f x‖` is unconditionally
summable if and only if the series `∑ x, f x` is unconditionally summable. One implication holds in
any complete normed space, while the other holds only in finite-dimensional spaces.  -/
Summable.norm : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  {f : α → E}, Summable f → Summable fun x => ‖f x‖
-- Mathlib.Tactic.ClickSuggestions.ApplyAt
/-- The structure for `apply at` lemmas stored in the `RefinedDiscrTree`.  -/
Mathlib.Tactic.ClickSuggestions.ApplyAtLemma : Type
-- Mathlib.RingTheory.Derivation.Basic
Derivation.coe_zero : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M], ⇑0 = 0
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.ReflexiveRelation.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {R X : C} {p₁ p₂ : R ⟶ X}
  {toJointlyMono₂ : CategoryTheory.JointlyMono₂ p₁ p₂} {r : X ⟶ R}
  {reflexivity₁ :
    autoParam (CategoryTheory.CategoryStruct.comp r p₁ = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.ReflexiveRelation.reflexivity₁._autoParam}
  {reflexivity₂ :
    autoParam (CategoryTheory.CategoryStruct.comp r p₂ = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.ReflexiveRelation.reflexivity₂._autoParam}
  {toJointlyMono₂_1 : CategoryTheory.JointlyMono₂ p₁ p₂} {r_1 : X ⟶ R}
  {reflexivity₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp r_1 p₁ = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.ReflexiveRelation.reflexivity₁._autoParam}
  {reflexivity₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp r_1 p₂ = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.ReflexiveRelation.reflexivity₂._autoParam},
  { toJointlyMono₂ := toJointlyMono₂, r := r, reflexivity₁ := reflexivity₁, reflexivity₂ := reflexivity₂ } =
      { toJointlyMono₂ := toJointlyMono₂_1, r := r_1, reflexivity₁ := reflexivity₁_1, reflexivity₂ := reflexivity₂_1 } →
    r = r_1
-- Mathlib.Tactic.ProdAssoc
Lean.Expr.instReprProdTree.repr : Lean.Expr.ProdTree → ℕ → Std.Format
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileEvent.type : Lean.Lsp.FileEvent → Lean.Lsp.FileChangeType
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- Suppose all distances from `p₁` and `p₂` to the points of a
simplex are equal, and that `p₁` and `p₂` lie in the affine span of
`p` with the vertices of that simplex.  Then `p₁` and `p₂` are equal
or reflections of each other in the affine span of the vertices of the
simplex.  -/
EuclideanGeometry.eq_or_eq_reflection_of_dist_eq : ∀ {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 : ℕ} {s : Affine.Simplex ℝ P n} {p p₁ p₂ : P} {r : ℝ},
  p₁ ∈ affineSpan ℝ (insert p (Set.range s.points)) →
    p₂ ∈ affineSpan ℝ (insert p (Set.range s.points)) →
      (∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r) →
        (∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r) →
          p₁ = p₂ ∨ p₁ = (EuclideanGeometry.reflection (affineSpan ℝ (Set.range s.points))) p₂
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
/-- `ReflectsFilteredColimitsOfSize.{w', w} F` means that whenever the image of a filtered cocone
under `F` is a colimit cocone, the original cocone was already a colimit.  -/
CategoryTheory.Limits.ReflectsFilteredColimitsOfSize : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.fin0_apply_norm : ∀ {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] (f : G [×0]→L[𝕜] G')
  {x : Fin 0 → G}, ‖f x‖ = ‖f‖
-- Mathlib.Control.ULiftable
ULiftable.mk : {f : outParam (Type u₀ → Type u₁)} →
  {g : Type v₀ → Type v₁} → ({α : Type u₀} → {β : Type v₀} → α ≃ β → f α ≃ g β) → ULiftable f g
-- Mathlib.Data.Rel
SetRel.inv_eq_self : ∀ {α : Type u_1} (R : SetRel α α) [R.IsSymm], R.inv = R
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.image_toSnowflaking_eball : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoEMetricSpace X] (x : X) (r : ENNReal),
  ⇑Metric.Snowflaking.toSnowflaking '' Metric.eball x r = Metric.eball (Metric.Snowflaking.toSnowflaking x) (r ^ α)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExProdNat.mul.injEq : ∀ {x e b : Q(ℕ)} (a : Mathlib.Tactic.Ring.Common.ExBaseNat x) (a_1 : Mathlib.Tactic.Ring.Common.ExProdNat e)
  (a_2 : Mathlib.Tactic.Ring.Common.ExProdNat b) (a_3 : Mathlib.Tactic.Ring.Common.ExBaseNat x)
  (a_4 : Mathlib.Tactic.Ring.Common.ExProdNat e) (a_5 : Mathlib.Tactic.Ring.Common.ExProdNat b),
  (Mathlib.Tactic.Ring.Common.ExProdNat.mul a a_1 a_2 = Mathlib.Tactic.Ring.Common.ExProdNat.mul a_3 a_4 a_5) =
    (a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5)
-- Mathlib.Data.Finset.NAry
Finset.image₂_union_inter_subset_union : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s s' : Finset α}
  {t t' : Finset β} [inst_1 : DecidableEq α] [inst_2 : DecidableEq β],
  Finset.image₂ f (s ∪ s') (t ∩ t') ⊆ Finset.image₂ f s t ∪ Finset.image₂ f s' t'
-- Mathlib.Order.SuccPred.LinearLocallyFinite
/-- If the order has neither bot nor top, `toZ` defines an `OrderIso` between `ι` and `ℤ`.  -/
orderIsoIntOfLinearSuccPredArch : {ι : Type u_1} →
  [inst : LinearOrder ι] →
    [inst_1 : SuccOrder ι] →
      [PredOrder ι] → [IsSuccArchimedean ι] → [NoMaxOrder ι] → [NoMinOrder ι] → [hι : Nonempty ι] → ι ≃o ℤ
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.instBEqPolyCnstr.beq_spec_2 : ∀ (x x_1 : Nat.Internal.Linear.PolyCnstr),
  (∀ (a : Bool) (a_1 a_2 : Nat.Internal.Linear.Poly) (b : Bool) (b_1 b_2 : Nat.Internal.Linear.Poly),
      x = { eq := a, lhs := a_1, rhs := a_2 } → x_1 = { eq := b, lhs := b_1, rhs := b_2 } → False) →
    (x == x_1) = false
-- Mathlib.Algebra.Homology.ComplexShapeSigns
/-- The symmetry bijection `(π c₂ c₁ c₁₂ ⁻¹' {j}) ≃ (π c₁ c₂ c₁₂ ⁻¹' {j})`.  -/
ComplexShape.symmetryEquiv : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₁₂ : Type u_4} →
      (c₁ : ComplexShape I₁) →
        (c₂ : ComplexShape I₂) →
          (c₁₂ : ComplexShape I₁₂) →
            [inst : TotalComplexShape c₁ c₂ c₁₂] →
              [inst_1 : TotalComplexShape c₂ c₁ c₁₂] →
                [TotalComplexShapeSymmetry c₁ c₂ c₁₂] → (j : I₁₂) → ↑(c₂.π c₁ c₁₂ ⁻¹' {j}) ≃ ↑(c₁.π c₂ c₁₂ ⁻¹' {j})
-- Mathlib.Logic.Basic
/-- On a goal of the form of `x ↔ y`, also try to simplify `y ↔ x`.

If simplifying `y ↔ x` gives `y' ↔ x'` then this simproc returns `x' ↔ y'` (so that the use of
commutativity is transparent), otherwise it returns the result of simplifying `y ↔ x` unmodified.
 -/
iffComm : Lean.Meta.Simp.Simproc
-- Mathlib.Combinatorics.Graph.Subgraph
/-- `H ≤c G` (`Graph.IsClosedSubgraph`) is a union of components of `G`.  -/
Graph.«term_≤c_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- Forward direction of Vitali's convergence theorem: if `f` is a sequence of uniformly integrable
functions that converge in measure to some function `g` in a finite measure space, then `f`
converge in Lp to `g`.  -/
MeasureTheory.tendsto_Lp_finite_of_tendstoInMeasure : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {p : ENNReal} {f : ℕ → α → β} {g : α → β} [MeasureTheory.IsFiniteMeasure μ],
  1 ≤ p →
    p ≠ ⊤ →
      (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
        MeasureTheory.MemLp g p μ →
          MeasureTheory.UnifIntegrable f p μ →
            MeasureTheory.TendstoInMeasure μ f Filter.atTop g →
              Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0)
-- Lean.Elab.DeclModifiers
/-- Converts optional visibility syntax to a `Visibility` value.  -/
Lean.Elab.elabVisibility : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadError m] →
      [Lean.MonadEnv m] →
        [Lean.MonadOptions m] →
          [Lean.MonadLog m] →
            [Lean.AddMessageContext m] → Option (Lean.TSyntax `Lean.Parser.Command.visibility) → m Lean.Elab.Visibility
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_closedBall_mul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (x : E) {r : ℝ},
  0 ≤ r →
    ∀ {s : ℝ},
      0 ≤ s → μ (Metric.closedBall x (r * s)) = ENNReal.ofReal (r ^ Module.finrank ℝ E) * μ (Metric.closedBall 0 s)
-- Init.Data.Array.Zip
_private.Init.Data.Array.Zip.0.List.getElem?_zipWithAll.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (a? : Option α) (b? : Option β)
  (h_1 : Unit → motive none none) (h_2 : (a? : Option α) → (b? : Option β) → motive a? b?),
  (a? = none → b? = none → False) →
    (match a?, b? with
      | none, none => h_1 ()
      | a?, b? => h_2 a? b?) =
      h_2 a? b?
-- Std.Time.DateTime
/-- Add `Nanosecond.Offset` to a `DateTime`.
 -/
Std.Time.DateTime.addNanoseconds : Std.Time.DateTime → Std.Time.Nanosecond.Offset → Std.Time.DateTime
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_mul_eq_add_arg_iff : ∀ {x y : ℂ}, x ≠ 0 → y ≠ 0 → ((x * y).arg = x.arg + y.arg ↔ x.arg + y.arg ∈ Set.Ioc (-Real.pi) Real.pi)
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.equiv_apply : ∀ {ι' : Type u_2} {M' : Type u_7} [inst : AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12}
  [inst_1 : Semiring R] [inst_2 : AddCommMonoid M] [inst_3 : Module R M] (b : Module.Basis ι R M) [inst_4 : Module R M']
  (i : ι) (b' : Module.Basis ι' R M') (e : ι ≃ ι'), (b.equiv b' e) (b i) = b' (e i)
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.lie_h_e_smul : ∀ (R : Type u_1) {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {h e f : L},
  IsSl2Triple h e f → ⁅h, e⁆ = 2 • e
-- Mathlib.Algebra.Group.Nat.Even
Nat.two_not_dvd_two_mul_add_one : ∀ (n : ℕ), ¬2 ∣ 2 * n + 1
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.endsWith_string_eq_endsWith_toSlice : ∀ {pat : String} {s : String.Slice}, s.endsWith pat = s.endsWith pat.toSlice