mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Double
HomologicalComplex.mkHomFromDouble.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X₀ X₁ : C} {f : X₀ ⟶ X₁} {ι : Type u_2} {c : ComplexShape ι}
  {i₀ i₁ : ι} (hi₀₁ : c.Rel i₀ i₁) (h : i₀ ≠ i₁) {K : HomologicalComplex C c} (φ₀ φ₀_1 : X₀ ⟶ K.X i₀) (e_φ₀ : φ₀ = φ₀_1)
  (φ₁ φ₁_1 : X₁ ⟶ K.X i₁) (e_φ₁ : φ₁ = φ₁_1)
  (comm : CategoryTheory.CategoryStruct.comp φ₀ (K.d i₀ i₁) = CategoryTheory.CategoryStruct.comp f φ₁)
  (hφ : ∀ (k : ι), c.Rel i₁ k → CategoryTheory.CategoryStruct.comp φ₁ (K.d i₁ k) = 0),
  HomologicalComplex.mkHomFromDouble hi₀₁ h φ₀ φ₁ comm hφ = HomologicalComplex.mkHomFromDouble hi₀₁ h φ₀_1 φ₁_1 ⋯ ⋯
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.empty_eq : ∀ {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering}, RBTree.RBMap.empty = ∅
-- Mathlib.CategoryTheory.Sites.Pullback
CategoryTheory.Functor.sheafPullbackConstruction.instIsRightAdjointSheafSheafPushforwardContinuousOfHasWeakSheafify : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  (G : CategoryTheory.Functor C D) (A : Type u₁) [inst_2 : CategoryTheory.Category.{v₁, u₁} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [inst_3 : G.IsContinuous J K]
  [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasLeftKanExtension F] [CategoryTheory.HasWeakSheafify K A],
  (G.sheafPushforwardContinuous A J K).IsRightAdjoint
-- Init.Data.UInt.Bitwise
UInt32.toNat_or : ∀ (a b : UInt32), (a ||| b).toNat = a.toNat ||| b.toNat
-- Mathlib.Combinatorics.Hindman
/-- Constructor for `FS`. This is the preferred spelling over `FS.cons'`.  -/
Hindman.FS.cons : ∀ {M : Type u_1} [inst : AddSemigroup M] (a : Stream' M) (m : M), Hindman.FS a.tail m → a.head + m ∈ Hindman.FS a
-- Lean.Elab.MutualInductive
/-- Ensures that there are no conflicts among or between the type and constructor names defined in `elabs`.  -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.checkNoInductiveNameConflicts : Array Lean.Elab.Command.InductiveElabStep1 → optParam Bool false → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Algebra.Group.Subgroup.Basic
MonoidHom.liftOfRightInverse.eq_1 : ∀ {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [inst : Group G₁] [inst_1 : Group G₂] [inst_2 : Group G₃]
  (f : G₁ →* G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f),
  f.liftOfRightInverse f_inv hf =
    { toFun := fun g => f.liftOfRightInverseAux f_inv hf ↑g ⋯, invFun := fun φ => ⟨φ.comp f, ⋯⟩, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.Topology.Gluing
_private.Mathlib.Topology.Gluing.0.TopCat.GlueData.«term𝖣» : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
/-- The isomorphism `eA.functor ≅ F ⋙ e'.inverse` deduced from the
unit isomorphism of `e'` and the isomorphism `hF : eA.functor ⋙ e'.functor ≅ F`.  -/
AlgebraicTopology.DoldKan.Compatibility.υ : {A : Type u_1} →
  {A' : Type u_2} →
    {B' : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} A] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] →
            {eA : A ≌ A'} →
              {e' : A' ≌ B'} →
                {F : CategoryTheory.Functor A B'} → (eA.functor.comp e'.functor ≅ F) → (eA.functor ≅ F.comp e'.inverse)
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- A limit cone extended by an isomorphism is a limit cone.  -/
CategoryTheory.Limits.IsLimit.extendIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {s : CategoryTheory.Limits.Cone F} →
            {X : C} →
              (i : X ⟶ s.pt) →
                [CategoryTheory.IsIso i] → CategoryTheory.Limits.IsLimit s → CategoryTheory.Limits.IsLimit (s.extend i)
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.Finset.ProveEmptyOrConsResult.empty.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {s : Q(Finset «$α»)} {pf pf_1 : Q(«$s» = ∅)},
  Mathlib.Meta.Finset.ProveEmptyOrConsResult.empty pf = Mathlib.Meta.Finset.ProveEmptyOrConsResult.empty pf_1 →
    pf = pf_1
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mul_top : ∀ {R : Type u} [inst : Semiring R] (I : Ideal R) [I.IsTwoSided], I * ⊤ = I
-- Init.Data.Float.Model.Float32
Float32.Model.instBEq : BEq Float32.Model
-- Mathlib.Data.WSeq.Productive
/-- A weak sequence is *productive* if it never stalls forever - there are
always a finite number of `think`s between `cons` constructors.
The sequence itself is allowed to be infinite though.  -/
Stream'.WSeq.Productive : {α : Type u} → Stream'.WSeq α → Prop
-- Mathlib.Algebra.Star.CHSH
IsCHSHTuple.A₀_inv : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {A₀ A₁ B₀ B₁ : R}, IsCHSHTuple A₀ A₁ B₀ B₁ → A₀ ^ 2 = 1
-- Mathlib.Order.Hom.Lattice
SupHom.instPartialOrder.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : SemilatticeSup β],
  SupHom.instPartialOrder = PartialOrder.lift DFunLike.coe ⋯
-- Mathlib.Topology.Semicontinuity.Defs
lowerSemicontinuous_iff_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β},
  LowerSemicontinuous f ↔ ∀ (x : α) (y : β), (∃ᶠ (x' : α) in nhds x, f x' ≤ y) → f x ≤ y
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintLabelPart.mk.injEq : ∀ (value : String) (tooltip? : Option Lean.Lsp.InlayHintTooltip) (location? : Option Lean.Lsp.Location)
  (command? : Option Lean.Lsp.Command) (value_1 : String) (tooltip?_1 : Option Lean.Lsp.InlayHintTooltip)
  (location?_1 : Option Lean.Lsp.Location) (command?_1 : Option Lean.Lsp.Command),
  ({ value := value, tooltip? := tooltip?, location? := location?, command? := command? } =
      { value := value_1, tooltip? := tooltip?_1, location? := location?_1, command? := command?_1 }) =
    (value = value_1 ∧ tooltip? = tooltip?_1 ∧ location? = location?_1 ∧ command? = command?_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- An arbitrary choice of coequalizer cocone for a parallel pair `f` and `g`.
 -/
CategoryTheory.Limits.coequalizer.cofork : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (f g : X ⟶ Y) → [CategoryTheory.Limits.HasCoequalizer f g] → CategoryTheory.Limits.Cofork f g
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.trans : ∀ {α : Type u} {β : Type v} {m₁ m₂ m₃ : Std.HashMap.Raw α β}, m₁.Equiv m₂ → m₂.Equiv m₃ → m₁.Equiv m₃
-- Lean.Meta.Match.Match
Lean.Meta.Match.match.maxCounterExamples : Lean.Option ℕ
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
Complex.differentiableAt_exp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ] {x : ℂ},
  DifferentiableAt 𝕜 Complex.exp x
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsIntTangentAt.wbtw : ∀ {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₁ s₂ : EuclideanGeometry.Sphere P} {p : P},
  s₁.IsIntTangentAt s₂ p → Wbtw ℝ s₂.center s₁.center p
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_erase_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α}, (m.erase k).getKey! k = default
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.addConst.go.eq_def : ∀ (k : ℤ) (a : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.addConst.go k a =
    match a with
    | Lean.Grind.CommRing.Poly.num k' => Lean.Grind.CommRing.Poly.num (k' + k)
    | Lean.Grind.CommRing.Poly.add k' m p =>
      Lean.Grind.CommRing.Poly.add k' m (Lean.Grind.CommRing.Poly.addConst.go k p)
-- Mathlib.LinearAlgebra.Prod
LinearMap.inl_injective : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], Function.Injective ⇑(LinearMap.inl R M M₂)
-- Lean.Elab.Syntax
Lean.Elab.Term.ensureUnaryOutput : Lean.Term × ℕ → Lean.Term
-- Lean.Meta.SynthInstance
_private.Lean.Meta.SynthInstance.0.Lean.Meta.preprocess.norm : Lean.Expr → Array ℕ → Lean.Expr → Lean.Expr → ℕ → Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.tensorObj.instTensorObj.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : C} [inst_3 : CategoryTheory.GrpObj G]
  [inst_4 : CategoryTheory.GrpObj H],
  CategoryTheory.GrpObj.tensorObj.instTensorObj =
    { toMonObj := CategoryTheory.Mon.instMonObjTensorObj,
      inv := CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.GrpObj.inv CategoryTheory.GrpObj.inv,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiable_of_mdifferentiableOn_iUnion_of_isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {ι : Type u_11}
  {s : ι → Set M}, (∀ (i : ι), MDiff[s i] f) → (∀ (i : ι), IsOpen (s i)) → ⋃ i, s i = Set.univ → MDiff f
-- Mathlib.Analysis.Normed.Operator.Basic
/-- The norm of the identity is at most `1`. It is in fact `1`, except when the space is trivial
where it is `0`. It means that one cannot do better than an inequality in general.  -/
ContinuousLinearMap.norm_id_le : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : SeminormedAddCommGroup E] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 E], ‖ContinuousLinearMap.id 𝕜 E‖ ≤ 1
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasStrictFDerivAt.isEquivalent_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E},
  HasStrictFDerivAt f f' x →
    Topology.IsInducing ⇑f' → Asymptotics.IsEquivalent (nhds (x, x)) (fun p => f p.1 - f p.2) fun p => f' (p.1 - p.2)
-- Mathlib.Analysis.SpecificLimits.Basic
tendsto_add_mul_div_add_mul_atTop_nhds : ∀ {𝕜 : Type u_4} [inst : Semifield 𝕜] [inst_1 : CharZero 𝕜] [inst_2 : TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜]
  [IsTopologicalSemiring 𝕜] [ContinuousInv₀ 𝕜] (a b c : 𝕜) {d : 𝕜},
  d ≠ 0 → Filter.Tendsto (fun k => (a + c * ↑k) / (b + d * ↑k)) Filter.atTop (nhds (c / d))
-- Mathlib.Algebra.Category.Ring.FilteredColimits
SemiRingCat.FilteredColimits.semiringObj : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J SemiRingCat) →
      (j : J) →
        Semiring (((F.comp (CategoryTheory.forget₂ SemiRingCat MonCat)).comp (CategoryTheory.forget MonCat)).obj j)
-- Mathlib.Data.Set.Finite.List
List.finite_length_le : ∀ (α : Type u_1) [Finite α] (n : ℕ), {l | l.length ≤ n}.Finite
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.IsRkFinite.closure_eq_closure_of_subset_of_forall_insert : ∀ {α : Type u_1} {M : Matroid α} {X Y : Set α},
  M.IsRkFinite X → X ⊆ Y → (∀ e ∈ Y \ X, M.eRk (insert e X) ≤ M.eRk X) → M.closure X = M.closure Y
-- Mathlib.Order.TransfiniteIteration
transfiniteIterate_succ : ∀ {I : Type u} [inst : SupSet I] (φ : I → I) {J : Type w} [inst_1 : LinearOrder J] [inst_2 : SuccOrder J]
  [inst_3 : WellFoundedLT J] (i₀ : I) (j : J),
  ¬IsMax j → transfiniteIterate φ (Order.succ j) i₀ = φ (transfiniteIterate φ j i₀)
-- Batteries.Data.Vector.Lemmas
Vector.scanlM.eq_1 : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n : ℕ} [inst : Monad m] (f : β → α → m β) (init : β)
  (as : Vector α n), Vector.scanlM f init as = Vector.scanlM.loop f as init 0 ⋯ #v[]
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instLawfulEqOrdOrdinal : Std.LawfulEqOrd Std.Time.Millisecond.Ordinal
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.coe_lt_one : ∀ {α : Type u} [inst : One α] {a : α} [inst_1 : LT α], ↑a < 1 ↔ a < 1
-- Mathlib.RepresentationTheory.Submodule
/-- The natural order isomorphism between the two ways to represent invariant submodules.  -/
Representation.mapSubmodule : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring k] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] →
            [inst_3 : Module k V] →
              (ρ : Representation k G V) → ↥ρ.invtSubmodule ≃o Submodule (MonoidAlgebra k G) ρ.asModule
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.limit_zero_val : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteAddGrp.{max v u}) (j : J),
  ↑0 j = 0
-- Lean.LocalContext
Lean.LocalContext.erase : Lean.LocalContext → Lean.FVarId → Lean.LocalContext
-- Qq.Macro
Qq.Impl.makeDefEq : Lean.Expr → Lean.Expr → Lean.MetaM (Option Lean.LocalContext)
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
SeminormFamily.basisSets_mem : ∀ {R : Type u_1} {E : Type u_6} {ι : Type u_9} [inst : SeminormedRing R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  (p : SeminormFamily R E ι) (i : Finset ι) {r : ℝ}, 0 < r → (i.sup p).ball 0 r ∈ p.basisSets
-- Init.Data.BitVec.Lemmas
BitVec.msb_intMin : ∀ {w : ℕ}, (BitVec.intMin w).msb = decide (0 < w)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.FiniteAtFilter.inf_ae_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α},
  μ.FiniteAtFilter (f ⊓ MeasureTheory.ae μ) ↔ μ.FiniteAtFilter f
-- Batteries.Control.ForInStep.Lemmas
ForInStep.bindList_append : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] (f : α → β → m (ForInStep β))
  (s : ForInStep β) (l₁ l₂ : List α),
  ForInStep.bindList f (l₁ ++ l₂) s = do
    let x ← ForInStep.bindList f l₁ s
    ForInStep.bindList f l₂ x
-- Mathlib.Algebra.Group.End
Equiv.zsmul_addLeft : ∀ {α : Type u_4} [inst : AddGroup α] (a : α) (n : ℤ), Equiv.addLeft a ^ n = Equiv.addLeft (n • a)
-- Lean.Elab.Term.TermElabM
/-- Field `suffix?` is for producing better error messages because `x.y` may be a field access or a hierarchical/composite name.
`ref` is the syntax object representing the field. `fullRef` includes the LHS.  -/
Lean.Elab.Term.LVal.fieldName : Lean.Syntax → String → List Lean.Level → Option Lean.Name → Lean.Syntax → Lean.Elab.Term.LVal
-- Mathlib.Data.Countable.Defs
countable_iff_exists_surjective : ∀ {α : Sort u} [Nonempty α], Countable α ↔ ∃ f, Function.Surjective f
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The `vectorSpan` of the empty set is `⊥`.  -/
vectorSpan_empty : ∀ (k : Type u_1) {V : Type u_2} (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P], vectorSpan k ∅ = ⊥
-- Mathlib.Algebra.Order.Nonneg.Module
Nonneg.instIsStrictOrderedModule : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : PartialOrder M] [inst_4 : SMulWithZero R M] [hM : IsStrictOrderedModule R M],
  IsStrictOrderedModule { c // 0 ≤ c } M
-- Qq.Match
Qq.Impl.mkIsDefEqCore : (decls : List Qq.Impl.PatVarDecl) →
  Q(Lean.Expr) →
    Q(Lean.Expr) →
      List Qq.Impl.PatVarDecl →
        Lean.MetaM
          (have a := Qq.Impl.mkIsDefEqType decls;
          Q(Lean.MetaM «$a»))
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.ι_mapBifunctorLeftUnitor_hom_apply : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C)
  (e : F.obj X ≅ CategoryTheory.Functor.id D)
  [inst_5 : ∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
  (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D)
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj
          Y).HasMap
      p]
  (j : J),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p ((CategoryTheory.GradedObject.single₀ I).obj X) Y 0 j j ⋯)
      ((CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).hom j) =
    CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).hom).app (Y j))
      (e.hom.app (Y j))
-- Mathlib.AlgebraicGeometry.Over
/-- `X.Over S` is the typeclass containing the data of a structure morphism `X ↘ S : X ⟶ S`.
 -/
AlgebraicGeometry.Scheme.Over : AlgebraicGeometry.Scheme → AlgebraicGeometry.Scheme → Type u
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
AlgHom.ext_of_eq_adjoin : ∀ {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] {S : Subalgebra R A} {s : Set A} (hS : S = Algebra.adjoin R s)
  ⦃φ₁ φ₂ : ↥S →ₐ[R] B⦄, (∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩) → φ₁ = φ₂
-- Init.Data.Option.Lemmas
Option.filter_bind : ∀ {α : Type u_1} {β : Type u_2} {x : Option α} {p : β → Bool} {f : α → Option β},
  Option.filter p (x.bind f) = (Option.filter (fun a => Option.any p (f a)) x).bind f
-- Init.Data.UInt.Bitwise
USize.not_xor : ∀ {a b : USize}, ~~~a ^^^ b = ~~~(a ^^^ b)
-- Mathlib.Analysis.Seminorm
Seminorm.neg_mem_closedBall_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) {r : ℝ} {x : E}, -x ∈ p.closedBall 0 r ↔ x ∈ p.closedBall 0 r
-- Aesop.Index.Forward
/-- Maps expressions `T` to all tuples `(r, i)` where `r : ForwardRule`,
`i : PremiseIndex` and the `i`-th argument of the type of `r.expr` (counting
from zero) likely unifies with `T`.  -/
Aesop.ForwardIndex.tree : Aesop.ForwardIndex → Lean.Meta.DiscrTree (Aesop.ForwardRule × Aesop.PremiseIndex)
-- Lean.Elab.PreDefinition.EqnsUtils
/-- Apply `whnfR` to lhs, return `none` if `lhs` was not modified  -/
Lean.Elab.Eqns.whnfReducibleLHS? : Lean.MVarId → Lean.MetaM (Option Lean.MVarId)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.isPullback_lift_id : ∀ {X U Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : U ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion g]
  (H : Set.range ⇑f ⊆ Set.range ⇑g),
  CategoryTheory.IsPullback (AlgebraicGeometry.IsOpenImmersion.lift g f H) (CategoryTheory.CategoryStruct.id X) g f
-- Init.System.IO
IO.AccessRight.mk.inj : ∀ {read write execution read_1 write_1 execution_1 : Bool},
  { read := read, write := write, execution := execution } =
      { read := read_1, write := write_1, execution := execution_1 } →
    read = read_1 ∧ write = write_1 ∧ execution = execution_1
-- Mathlib.MeasureTheory.Constructions.Pi
MeasurableSpace.comap.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (m : MeasurableSpace β),
  MeasurableSpace.comap f m =
    { MeasurableSet' := fun s => ∃ s', MeasurableSet s' ∧ f ⁻¹' s' = s, measurableSet_empty := ⋯,
      measurableSet_compl := ⋯, measurableSet_iUnion := ⋯ }
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey_eq_minKeyD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} {he : l.isEmpty = false} {fallback : α},
  Std.Internal.List.minKey l he = Std.Internal.List.minKeyD l fallback
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.nullMeasurableSet_empty : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, MeasureTheory.NullMeasurableSet ∅ μ
-- Init.Data.Float.Float
/-- Checks whether a floating-point number is finite, that is, whether it is normal, subnormal, or zero,
but not infinite or `NaN`.

This function has a logical model in terms of `Float.Model`. It is compiled to the C operator `isfinite`.
 -/
Float.isFinite : Float → Bool
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiringClass.noZeroDivisors : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : SetLike S R]
  [inst_2 : NonUnitalSubsemiringClass S R] (s : S) [NoZeroDivisors R], NoZeroDivisors ↥s
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- Naturality of the oplax functoriality constraint, on the right.  -/
CategoryTheory.OplaxFunctor.mapComp_naturality_right_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.OplaxFunctor B C) {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g')
  {Z : self.obj a ⟶ self.obj c} (h : CategoryTheory.CategoryStruct.comp (self.map f) (self.map g') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η))
      (CategoryTheory.CategoryStruct.comp (self.mapComp f g') h) =
    CategoryTheory.CategoryStruct.comp (self.mapComp f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.map₂ η)) h)
-- Init.Data.UInt.Lemmas
UInt8.ofBitVec_uInt64ToBitVec : ∀ (n : UInt64), { toBitVec := BitVec.setWidth 8 n.toBitVec } = n.toUInt8
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs.0.Tactic.ComputeAsymptotics.MultiseriesExpansion.lt_iff_lt : ∀ {basis : Tactic.ComputeAsymptotics.Basis} {exp1 exp2 : ℝ}
  {coef1 coef2 : Tactic.ComputeAsymptotics.MultiseriesExpansion basis}, (exp1, coef1) < (exp2, coef2) ↔ exp1 < exp2
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.sec.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (z : N), f.sec z = Classical.choose ⋯
-- Batteries.Data.Fin.Coding
/-- Decode `Quotient s` from `Fin m` where `s` is a decidable setoid on `Fin n`.  -/
Fin.decodeQuotient : {n : ℕ} →
  (s : Setoid (Fin n)) → [inst : DecidableRel ⇑s] → Fin (Fin.countP fun i => decide (Fin.getRepr s i = i)) → Quotient s
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- A Dirichlet character of modulus `≠ 1` maps `0` to `0`.  -/
DirichletCharacter.map_zero' : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n), n ≠ 1 → χ 0 = 0
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The adjunction between the cofree and forgetful constructions for Eilenberg-Moore coalgebras
for a comonad.
 -/
CategoryTheory.Comonad.adj : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → (G : CategoryTheory.Comonad C) → G.forget ⊣ G.cofree
-- Mathlib.GroupTheory.Nilpotent
/-- Products of nilpotent groups are nilpotent.  -/
Group.isNilpotent_prod : ∀ {G₁ : Type u_2} {G₂ : Type u_3} [inst : Group G₁] [inst_1 : Group G₂] [Group.IsNilpotent G₁] [Group.IsNilpotent G₂],
  Group.IsNilpotent (G₁ × G₂)
-- Mathlib.GroupTheory.Congruence.Hom
/-- The uniqueness part of the universal property for quotients of monoids.  -/
Con.lift_unique : ∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] {c : Con M} {f : M →* P}
  (H : c ≤ Con.ker f) (g : c.Quotient →* P), g.comp c.mk' = f → g = c.lift f H
-- Mathlib.Analysis.Normed.Module.RCLike.Basic
/-- `LinearMap.bound_of_ball_bound` is a version of this over arbitrary nontrivially normed fields.
It produces a less precise bound so we keep both versions.  -/
LinearMap.bound_of_ball_bound' : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {r : ℝ},
  0 < r → ∀ (c : ℝ) (f : E →ₗ[𝕜] 𝕜), (∀ z ∈ Metric.closedBall 0 r, ‖f z‖ ≤ c) → ∀ (z : E), ‖f z‖ ≤ c / r * ‖z‖
-- Mathlib.Algebra.Group.Hom.Basic
ZeroHom.coe_sub : ∀ {M : Type u_8} {N : Type u_9} [inst : Zero M] [inst_1 : SubtractionMonoid N] (f g : ZeroHom M N), ⇑(f - g) = ⇑f - ⇑g