mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Dimension.Basic
/-- Two linearly equivalent vector spaces have the same dimension, a version with different
universes.  -/
LinearEquiv.lift_rank_eq : ∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M ≃ₗ[R] M'),
  Cardinal.lift.{v', v} (Module.rank R M) = Cardinal.lift.{v, v'} (Module.rank R M')
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
/-- The set of differentiability points of a continuous function depending on a parameter taking
values in a complete space is Borel-measurable.  -/
measurableSet_of_differentiableAt_with_param : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [LocallyCompactSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] {α : Type u_4} [inst_6 : TopologicalSpace α] {f : α → E → F} [inst_7 : MeasurableSpace α]
  [OpensMeasurableSpace α] [inst_9 : MeasurableSpace E] [OpensMeasurableSpace E] [CompleteSpace F],
  Continuous (Function.uncurry f) → MeasurableSet {p | DifferentiableAt 𝕜 (f p.1) p.2}
-- Mathlib.Data.Finset.Sups
Finset.subset_infs_self : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {s : Finset α}, s ⊆ s ⊼ s
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
/-- Continuous star algebra homomorphisms from `C(s, 𝕜)` into a star `𝕜`-algebra `A` which agree
at `X : 𝕜[X]` (interpreted as a continuous map) are, in fact, equal.  -/
ContinuousMap.starAlgHom_ext_map_X : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : RCLike 𝕜] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra 𝕜 A]
  [inst_4 : TopologicalSpace A] [T2Space A] {s : Set 𝕜} [CompactSpace ↑s] {φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A},
  Continuous ⇑φ →
    Continuous ⇑ψ →
      φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) =
          ψ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) →
        φ = ψ
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.mk : {A : Type u_7} →
  {B : Type u_8} →
    [inst : AddMonoid A] →
      [inst_1 : AddMonoid B] →
        [inst_2 : TopologicalSpace A] →
          [inst_3 : TopologicalSpace B] →
            (toAddMonoidHom : A →+ B) →
              autoParam (Continuous (↑toAddMonoidHom).toFun) ContinuousMap.continuous_toFun._autoParam → A →ₜ+ B
-- Mathlib.Data.Multiset.MapFold
Multiset.Nodup.map : ∀ {α : Type u_1} {β : Type v} {f : α → β} {s : Multiset α}, Function.Injective f → s.Nodup → (Multiset.map f s).Nodup
-- Mathlib.Data.Rat.Cast.Lemmas
NNRat.Nonneg.coe_ofScientific : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K] (m : ℕ) (s : Bool) (e : ℕ),
  ↑(OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
/-- The type of morphisms in `DescentDataAsCoalgebra`.  -/
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F :
        CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
          (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} → F.DescentDataAsCoalgebra f → F.DescentDataAsCoalgebra f → Type (max t v')
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.lTensor_refl : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) (N : Type u_8) [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N],
  LinearEquiv.lTensor M (LinearEquiv.refl R N) = LinearEquiv.refl R (TensorProduct R M N)
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.mem_centralizer_iff_commutator_eq_one' : ∀ {G : Type u_1} [inst : Group G] {g : G} {s : Set G}, g ∈ Subgroup.centralizer s ↔ ∀ h ∈ s, ⁅g, h⁆ = 1
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- A version of `ιMulti_span_fixedDegree_of_span_eq_top` that works in the exterior power.  -/
exteriorPower.ιMulti_span_of_span : ∀ (R : Type u) [inst : CommRing R] (n : ℕ) (M : Type u_1) [inst_1 : AddCommGroup M] [inst_2 : Module R M] {s : Set M},
  Submodule.span R s = ⊤ → Submodule.span R (⇑(exteriorPower.ιMulti R n) '' {a | Set.range a ⊆ s}) = ⊤
-- Mathlib.RingTheory.Adjoin.Field
AlgEquiv.coe_adjoinSingletonEquivAdjoinRootMinpoly_symm : ∀ (F : Type u_1) [inst : Field F] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra F R] (x : R),
  ⇑(AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly F x).symm = ⇑(AdjoinRoot.Minpoly.toAdjoin F x)
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
ContinuousMap.Homotopy.affine.congr_simp : ∀ {X : Type u_1} {E : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : IsTopologicalAddGroup E] [inst_4 : Module ℝ E] [inst_5 : ContinuousSMul ℝ E] (f g : C(X, E)),
  ContinuousMap.Homotopy.affine f g = ContinuousMap.Homotopy.affine f g
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.instStarMul : StarMul Complex.UnitDisc
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasLimit F],
  CategoryTheory.Limits.limit F = (CategoryTheory.Limits.limit.cone F).pt
-- Mathlib.SetTheory.Ordinal.Notation
ONote.zero_lt_one : 0 < 1
-- Lean.Meta.Eqns
/-- These options affect the generation of equational theorems in a significant way. For these, their
value at definition time, not realization time, should matter.

This is implemented by storing their values at definition time (when non-default) in an environment
extension, and restoring them when the equations are lazily realized.
 -/
Lean.Meta.eqnAffectingOptions : Array (Lean.Option Bool)
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.Receiver.recv : {α : Type} → Std.Bounded.Receiver✝ α → BaseIO (Task (Option α))
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.LHom.realize_onFormula : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'}
  [inst_1 : L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (ψ : L.Formula α) {v : α → M},
  (φ.onFormula ψ).Realize v ↔ ψ.Realize v
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.coherenceComp.inj : ∀ {e : Lean.Expr} {f g h i : Mathlib.Tactic.BicategoryLike.Mor₁} {α : Mathlib.Tactic.BicategoryLike.CoherenceHom}
  {η θ : Mathlib.Tactic.BicategoryLike.Mor₂Iso} {e_1 : Lean.Expr} {f_1 g_1 h_1 i_1 : Mathlib.Tactic.BicategoryLike.Mor₁}
  {α_1 : Mathlib.Tactic.BicategoryLike.CoherenceHom} {η_1 θ_1 : Mathlib.Tactic.BicategoryLike.Mor₂Iso},
  Mathlib.Tactic.BicategoryLike.Mor₂Iso.coherenceComp e f g h i α η θ =
      Mathlib.Tactic.BicategoryLike.Mor₂Iso.coherenceComp e_1 f_1 g_1 h_1 i_1 α_1 η_1 θ_1 →
    e = e_1 ∧ f = f_1 ∧ g = g_1 ∧ h = h_1 ∧ i = i_1 ∧ α = α_1 ∧ η = η_1 ∧ θ = θ_1
-- Init.Data.Fin.Lemmas
Fin.lastCases_castSucc : ∀ {n : ℕ} {motive : Fin (n + 1) → Sort u_1} {last : motive (Fin.last n)} {cast : (i : Fin n) → motive i.castSucc}
  (i : Fin n), Fin.lastCases last cast i.castSucc = cast i
-- Init.Core
PSum.nonemptyLeft : ∀ {α : Sort u_1} {β : Sort u_2} [h : Nonempty α], Nonempty (α ⊕' β)
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.mk_eq_top_of_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.IsIso f],
  CategoryTheory.Subobject.mk f = ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackProdFstIsoProd_inv_snd_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct Y Z] [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Z]
  [inst_3 : CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.prod.fst],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdFstIsoProd f Z).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f CategoryTheory.Limits.prod.fst)
        CategoryTheory.Limits.prod.snd) =
    CategoryTheory.Limits.prod.snd
-- Init.Data.String.Subslice
String.Slice.Subslice.instToString : {s : String.Slice} → ToString s.Subslice
-- Mathlib.SetTheory.Cardinal.Basic
/-- **Alias** of `Cardinal.mk_sdiff_add_mk`. -/
Cardinal.mk_diff_add_mk : ∀ {α : Type u} {S T : Set α}, T ⊆ S → Cardinal.mk ↑(S \ T) + Cardinal.mk ↑T = Cardinal.mk ↑S
-- Std.Data.ByteSlice
/-- Computes the size of the byte slice.
 -/
ByteSlice.size : ByteSlice → ℕ
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.Edge.map_snd : ∀ {X Y : SSet.Truncated 2}
  {x x' : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (e₁ : SSet.Truncated.Edge x x')
  {y y' : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (e₂ : SSet.Truncated.Edge y y'), (e₁.tensor e₂).map (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y) = e₂
-- Init.Data.Float.Model.Float32
Float32.Model.instLE : LE Float32.Model
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp_neg : ∀ {𝔸 : Type u_1} [inst : NormedDivisionRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (x : 𝔸),
  NormedSpace.exp (-x) = (NormedSpace.exp x)⁻¹
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
ModuleCat.Derivation.d_map : ∀ {A B : CommRingCat} {M : ModuleCat ↑B} {f : A ⟶ B} (D : M.Derivation f) (a : ↑A),
  D.d ((CategoryTheory.ConcreteCategory.hom f) a) = 0
-- Mathlib.Order.CompactlyGenerated.Basic
CompleteLattice.isCompactElement_finsetSup : ∀ {α : Type u_3} {β : Type u_4} [inst : CompleteLattice α] {f : β → α} (s : Finset β),
  (∀ x ∈ s, IsCompactElement (f x)) → IsCompactElement (s.sup f)
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.Functor.map_comp_heq' : ∀ {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} {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z},
  (∀ (X : C), F.obj X = G.obj X) →
    (∀ {X Y : C} (f : X ⟶ Y), F.map f ≍ G.map f) →
      F.map (CategoryTheory.CategoryStruct.comp f g) ≍ G.map (CategoryTheory.CategoryStruct.comp f g)
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.Slice.positions.eq_1 : ∀ (s : String.Slice), s.positions = String.Slice.positionsFrom s.startPos
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.ret.injEq : ∀ (x x_1 : Lean.IR.Arg), (Lean.IR.FnBody.ret x = Lean.IR.FnBody.ret x_1) = (x = x_1)
-- Batteries.Tactic.Lint.Basic
/-- `test` defines a test to perform on every declaration. It should never fail. Returning `none`
signifies a passing test. Returning `some msg` reports a failing test with error `msg`.  -/
Batteries.Tactic.Lint.Linter.test : Batteries.Tactic.Lint.Linter → Lean.Name → Lean.MetaM (Option Lean.MessageData)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.lt_norm_expr : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsPreorder α] [Lean.Grind.OrderedRing α] (ctx : Lean.Grind.CommRing.Context α)
  (lhs rhs lhs' rhs' : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.norm_cnstr_cert lhs rhs lhs' rhs' = true →
    (Lean.Grind.CommRing.Expr.denote ctx lhs < Lean.Grind.CommRing.Expr.denote ctx rhs) =
      (Lean.Grind.CommRing.Expr.denote ctx lhs' < Lean.Grind.CommRing.Expr.denote ctx rhs')
-- Mathlib.Order.Filter.Ultrafilter.Defs
/-- **Alias** of the forward direction of `Ultrafilter.frequently_iff_eventually`. -/
Filter.Frequently.eventually : ∀ {α : Type u} {f : Ultrafilter α} {p : α → Prop}, (∃ᶠ (x : α) in ↑f, p x) → ∀ᶠ (x : α) in ↑f, p x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.mem_toArray_iff_get?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [LawfulBEq α] {k : α}
  {v : β}, (k, v) ∈ Std.DHashMap.Const.toArray m ↔ Std.DHashMap.Const.get? m k = some v
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.Functor.Braided.instComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                {E : Type u₃} →
                  [inst_6 : CategoryTheory.Category.{v₃, u₃} E] →
                    [inst_7 : CategoryTheory.MonoidalCategory E] →
                      [inst_8 : CategoryTheory.BraidedCategory E] →
                        (F : CategoryTheory.Functor C D) →
                          (G : CategoryTheory.Functor D E) → [F.Braided] → [G.Braided] → (F.comp G).Braided
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.optimalGHDist_mem_candidatesB : ∀ (X : Type u) (Y : Type v) [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X]
  [inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y],
  GromovHausdorff.optimalGHDist✝ X Y ∈ GromovHausdorff.candidatesB✝ X Y
-- Batteries.Data.List.Lemmas
List.mem_idxsOf_iff_getElem_sub_pos : ∀ {α : Type u_1} {xs : List α} {x : α} {s i : ℕ} [inst : BEq α],
  i ∈ List.idxsOf x xs s ↔ s ≤ i ∧ ∃ (hix : i - s < xs.length), (xs[i - s] == x) = true
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.findSome?.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match some b with
    | some b => h_1 b
    | none => h_2 ()) =
    h_1 b
-- Mathlib.Data.List.Forall2
List.rel_reverse : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop},
  Relator.LiftFun (List.Forall₂ R) (List.Forall₂ R) List.reverse List.reverse
-- Lean.Parser.Types
_private.Lean.Parser.Types.0.Lean.Parser.SyntaxStack.mk.inj : ∀ {raw : Array Lean.Syntax} {drop : ℕ} {raw_1 : Array Lean.Syntax} {drop_1 : ℕ},
  { raw := raw, drop := drop } = { raw := raw_1, drop := drop_1 } → raw = raw_1 ∧ drop = drop_1
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.PreservesEpimorphisms.ofRetract : ∀ {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} (r : CategoryTheory.Retract G F) [F.PreservesEpimorphisms], G.PreservesEpimorphisms
-- Mathlib.Topology.Semicontinuity.Basic
/-- The sublevel sets of a lower semicontinuous function on a compact set are compact.  -/
LowerSemicontinuousOn.isCompact_inter_preimage_Iic : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_4} [inst_1 : LinearOrder γ] {f : α → γ},
  LowerSemicontinuousOn f s → IsCompact s → ∀ (c : γ), IsCompact (s ∩ f ⁻¹' Set.Iic c)
-- Mathlib.Data.Set.Monotone
strictMonoOn_insert_iff_of_forall_ge : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α},
  (∀ x ∈ s, a ≤ x) → (StrictMonoOn f (insert a s) ↔ (∀ b ∈ s, a < b → f a < f b) ∧ StrictMonoOn f s)
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.one.inj : ∀ {name name_1 : Lean.TSyntax `Lean.binderIdent},
  Lean.Parser.Tactic.MCasesPat.one name = Lean.Parser.Tactic.MCasesPat.one name_1 → name = name_1
-- Mathlib.Topology.Category.CompHaus.Basic
topToCompHaus_obj : ∀ (X : TopCat), ↑(topToCompHaus.obj X).toTop = StoneCech ↑X
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.instMax : {G : Type u_1} → [inst : AddGroup G] → Max (FiniteIndexNormalAddSubgroup G)
-- Std.Http.Protocol.H1.Message
Std.Http.Protocol.H1.instEncodeV11Head : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Internal.Encode Std.Http.Version.v11 (Std.Http.Protocol.H1.Message.Head dir)
-- Mathlib.Control.Bifunctor
Function.bicompr.lawfulBifunctor : ∀ {F : Type u₀ → Type u₁ → Type u₂} [inst : Bifunctor F] (G : Type u₂ → Type u_1) [inst_1 : Functor G] [LawfulFunctor G]
  [LawfulBifunctor F], LawfulBifunctor (Function.bicompr G F)
-- Mathlib.RingTheory.GradedAlgebra.Basic
DirectSum.decomposeAlgEquiv_symm_apply : ∀ {ι : Type u_1} {R : Type u_2} {A : Type u_3} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : CommSemiring R]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (𝒜 : ι → Submodule R A) [inst_5 : GradedAlgebra 𝒜]
  (a : DirectSum ι fun i => ↥(𝒜 i)), (DirectSum.decomposeAlgEquiv 𝒜).symm a = (DirectSum.decompose 𝒜).symm a
-- Lean.Elab.Term.TermElabM
/-- Return true if `stx` is a lambda abstraction containing a `{}` or `[]` binder annotation.
Example: `fun {α} (a : α) => a`  -/
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.isLambdaWithImplicit : Lean.Syntax → Bool
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- A variant of `RightHomotopy.compRight` useful for dealing with homotopy equivalences.  -/
CategoryTheory.Arrow.RightHomotopy.compRightId : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v : CategoryTheory.Arrow V} →
        {f : u ⟶ u} →
          CategoryTheory.Arrow.RightHomotopy f (CategoryTheory.CategoryStruct.id u) →
            (g : u ⟶ v) → CategoryTheory.Arrow.RightHomotopy (CategoryTheory.CategoryStruct.comp f g) g
-- Mathlib.MeasureTheory.Integral.TorusIntegral
/-- The integral over a generalized torus with center `c ∈ ℂⁿ` and radius `R ∈ ℝⁿ`, defined
as the `•`-product of the derivative of `torusMap` and `f (torusMap c R θ)`  -/
«term∯_InT(_,_),_» : Lean.ParserDescr
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedArg : {a : Lean.Compiler.LCNF.Purity} → Inhabited (Lean.Compiler.LCNF.Arg a)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulEquiv.subsemigroupCongr.eq_1 : ∀ {M : Type u_1} [inst : Mul M] {S T : Subsemigroup M} (h : S = T),
  MulEquiv.subsemigroupCongr h = { toEquiv := Equiv.setCongr ⋯, map_mul' := ⋯ }
-- Init.Data.Vector.Lemmas
Vector.prod_toArray : ∀ {α : Type u_1} {n : ℕ} [inst : Mul α] [inst_1 : One α] {xs : Vector α n}, xs.toArray.prod = xs.prod
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
returning `none` if no such pair exists.
 -/
Std.DTreeMap.getEntryGT? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → Option ((a : α) × β a)
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.measurePreserving_div_left : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : DivisionMonoid G] [MeasurableMul G] [MeasurableInv G]
  (μ : MeasureTheory.Measure G) [μ.IsInvInvariant] [μ.IsMulLeftInvariant] (g : G),
  MeasureTheory.MeasurePreserving (fun t => g / t) μ μ
-- Mathlib.NumberTheory.ModularForms.Derivative
/-- The `SL(2, ℤ)` case of `normalizedDerivOfComplex_slash`, where the determinant factor is `1`.  -/
Derivative.normalizedDerivOfComplex_SL_slash : ∀ {k : ℤ} {F : UpperHalfPlane → ℂ},
  MDiff F →
    ∀ {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ},
      Derivative.normalizedDerivOfComplex (SlashAction.map k γ F) =
        SlashAction.map (k + 2) γ (Derivative.normalizedDerivOfComplex F) - fun z =>
          ↑k * (2 * ↑Real.pi * Complex.I)⁻¹ *
              (↑(↑γ 1 0) /
                UpperHalfPlane.denom
                  (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z) *
            SlashAction.map k γ F z
-- Lean.Parser.Extra
/-- The parser `char` parses a character literal, such as `'a'` or `'\n'`. Character literals can
contain C-style escapes like `\n`, `\"`, `\x00` or `\u2665`, as well as literal unicode characters
like `∈`, but must evaluate to a single unicode codepoint, so `'♥'` is allowed but `'❤️'` is not
(since it is two codepoints but one grapheme cluster).

This parser has arity 1: it produces a `charLitKind` node containing an atom with the raw
literal (including the quote marks and without interpreting the escapes).
You can use `TSyntax.getChar` to decode the string from the resulting syntax object.  -/
Lean.Parser.charLit : Lean.Parser.Parser
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.biprod_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {Y : C} {n : ℕ} {X₁ X₂ : C} {α β : CategoryTheory.Abelian.Ext (X₁ ⊞ X₂) Y n},
  (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.inl).comp α ⋯ =
      (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.inl).comp β ⋯ →
    (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.inr).comp α ⋯ =
        (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.inr).comp β ⋯ →
      α = β
-- Mathlib.Algebra.GroupWithZero.Subgroup
AddSubgroup.mem_inv_pointwise_smul_iff : ∀ {G : Type u_2} {A : Type u_4} [inst : Group G] [inst_1 : AddGroup A] [inst_2 : DistribMulAction G A]
  {S : AddSubgroup A} {a : G} {x : A}, x ∈ a⁻¹ • S ↔ a • x ∈ S
-- Lean.Parser.Term
Lean.Parser.Term.letrec.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.zero_le : ∀ {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α), 0 ≤ μ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_insert_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, (t.insert k v).size ≤ t.size + 1
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iInter_inv : ∀ {α : Type u_2} {ι : Sort u_5} [inst : Inv α] (s : ι → Set α), (⋂ i, s i)⁻¹ = ⋂ i, (s i)⁻¹
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_sigmaDesc_shrinkYoneda_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {S : C} {ι : Type u_2} [inst_2 : Small.{w, u_2} ι] {X : ι → C}
  (f : (i : ι) → X i ⟶ S),
  CategoryTheory.Sieve.ofArrows X f ∈ J S ↔
    CategoryTheory.Presheaf.IsLocallySurjective J
      (CategoryTheory.Limits.Sigma.desc fun i => CategoryTheory.shrinkYoneda.{w, v, u}.map (f i))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
/-- Given
```
Y₃ - i₃ -> X₃
|          |
g₂         f₂
∨          ∨
Y₂ - i₂ -> X₂
|          |
g₁         f₁
∨          ∨
Y₁ - i₁ -> X₁
```
The top square is a pullback if the bottom square and the big square are.
 -/
CategoryTheory.Limits.topSquareIsPullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ Y₁ : C} →
      {f₁ : X₂ ⟶ X₁} →
        {f₂ : X₃ ⟶ X₂} →
          {i₁ : Y₁ ⟶ X₁} →
            {t₁ : CategoryTheory.Limits.PullbackCone i₁ f₁} →
              {i₂ : t₁.pt ⟶ X₂} →
                (t₂ : CategoryTheory.Limits.PullbackCone i₂ f₂) →
                  (hi₂ : i₂ = t₁.snd) →
                    CategoryTheory.Limits.IsLimit t₁ →
                      CategoryTheory.Limits.IsLimit (t₁.pasteVert t₂ hi₂) → CategoryTheory.Limits.IsLimit t₂
-- Lean.Declaration
Lean.Declaration.inductDecl.injEq : ∀ (lparams : List Lean.Name) (nparams : ℕ) (types : List Lean.InductiveType) (isUnsafe : Bool)
  (lparams_1 : List Lean.Name) (nparams_1 : ℕ) (types_1 : List Lean.InductiveType) (isUnsafe_1 : Bool),
  (Lean.Declaration.inductDecl lparams nparams types isUnsafe =
      Lean.Declaration.inductDecl lparams_1 nparams_1 types_1 isUnsafe_1) =
    (lparams = lparams_1 ∧ nparams = nparams_1 ∧ types = types_1 ∧ isUnsafe = isUnsafe_1)
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_sub_mul_right : ∀ {α : Type u} [inst : CommRing α] (x y z : α), Ideal.span {x - z * y, y} = Ideal.span {x, y}
-- Mathlib.Analysis.Quaternion
Quaternion.nnnorm_coe : ∀ (a : ℝ), ‖↑a‖₊ = ‖a‖₊
-- Mathlib.Data.Complex.Basic
Complex.conj_eq_iff_re : ∀ {z : ℂ}, (starRingEnd ℂ) z = z ↔ ↑z.re = z
-- Mathlib.Data.List.Lookmap
List.lookmap_cons_some : ∀ {α : Type u_1} (f : α → Option α) {a b : α} (l : List α), f a = some b → List.lookmap f (a :: l) = b :: l