mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.PiLex
/-- `Colex (∀ i, α i)` is a linear order if the original order has well-founded `>`.  -/
Pi.Colex.linearOrder : {ι : Type u_1} →
  {β : ι → Type u_2} →
    [inst : LinearOrder ι] → [WellFoundedGT ι] → [(a : ι) → LinearOrder (β a)] → LinearOrder (Colex ((i : ι) → β i))
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.tfaeHaveIdLhs.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Geometry.Convex.ConvexSpace.AffineMap
Convexity.ConvexSpace.AffineMap.mk.congr_simp : ∀ {R : Type u_1} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R] {X : Type u_2}
  {Y : Type u_3} [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y] (toFun toFun_1 : X → Y)
  (e_toFun : toFun = toFun_1) (isAffineMap_toFun : Convexity.IsAffineMap R toFun),
  { toFun := toFun, isAffineMap_toFun := isAffineMap_toFun } = { toFun := toFun_1, isAffineMap_toFun := ⋯ }
-- Mathlib.Data.Int.Init
Int.pred_nat_succ : ∀ (n : ℕ), (↑n.succ).pred = ↑n
-- Mathlib.Topology.Homotopy.Product
/-- The product of homotopies h₁ and h₂.
This is `HomotopyRel.prod` specialized for path homotopies.  -/
Path.Homotopic.prodHomotopy : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        {a₁ a₂ : α} →
          {b₁ b₂ : β} →
            {p₁ p₁' : Path a₁ a₂} →
              {p₂ p₂' : Path b₁ b₂} → p₁.Homotopy p₁' → p₂.Homotopy p₂' → (p₁.prod p₂).Homotopy (p₁'.prod p₂')
-- Mathlib.Topology.Connected.PathConnected
/-- The preimage of a singleton in `ZerothHomotopy` is the path component of an element in the
equivalence class.  -/
ZerothHomotopy.preimage_singleton_eq_pathComponent : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X), ZerothHomotopy.mk ⁻¹' {ZerothHomotopy.mk x} = pathComponent x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.foldlM_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} {δ : Type w}
  {m : Type w → Type w'} [Std.TransCmp cmp] [inst : Monad m] [LawfulMonad m] {f : δ → α → β → m δ} {init : δ},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.TreeMap.Raw.foldlM f init t₁ = Std.TreeMap.Raw.foldlM f init t₂
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.imp_1eq_cert : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Bool
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.total.mapAux.d₁_mapMap : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂}
  (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂]
  [inst_4 : K.HasTotal c₁₂] [inst_5 : L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂),
  CategoryTheory.CategoryStruct.comp (K.d₁ c₁₂ i₁ i₂ i₁₂)
      (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂) =
    CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (L.d₁ c₁₂ i₁ i₂ i₁₂)
-- Mathlib.Order.BoundedOrder.Basic
BoundedOrder.instSubsingleton : ∀ {α : Type u} [inst : PartialOrder α], Subsingleton (BoundedOrder α)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_X_pow_mul : ∀ {R : Type u_1} [inst : Semiring R] (p : PowerSeries R) (n d : ℕ),
  (PowerSeries.coeff (d + n)) (PowerSeries.X ^ n * p) = (PowerSeries.coeff d) p
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_iInf_ne_zero : ∀ {G : Type u_1} [inst : AddGroup G] {L : AddSubgroup G} {ι : Type u_3} [_hι : Finite ι] {f : ι → AddSubgroup G},
  (∀ (i : ι), (f i).relIndex L ≠ 0) → (⨅ i, f i).relIndex L ≠ 0
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.coe_inf : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] (f g : CauSeq α abs),
  ↑(f ⊓ g) = ↑f ⊓ ↑g
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.comap_genWeightSpace_eq_of_injective : ∀ {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] {M₂ : Type u_5} [inst_8 : AddCommGroup M₂] [inst_9 : Module R M₂]
  [inst_10 : LieRingModule L M₂] [inst_11 : LieModule R L M₂] {χ : L → R} {f : M →ₗ⁅R,L⁆ M₂},
  Function.Injective ⇑f → LieSubmodule.comap f (LieModule.genWeightSpace M₂ χ) = LieModule.genWeightSpace M χ
-- Mathlib.RepresentationTheory.Equiv
Representation.diagonalOneEquivLeftRegular.eq_1 : ∀ (k : Type u) [inst : Semiring k] (G : Type v) [inst_1 : Monoid G],
  Representation.diagonalOneEquivLeftRegular k G =
    Representation.Equiv.mk (MonoidAlgebra.mapDomainLinearEquiv k k (Equiv.funUnique (Fin 1) G)) ⋯
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Homotopy.extend.hom_eq : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {K L : HomologicalComplex C c} (e : c.Embedding c')
  (φ : (i j : ι) → K.X i ⟶ L.X j) {i' j' : ι'} {i j : ι} (hi : e.f i = i') (hj : e.f j = j'),
  Homotopy.extend.hom e φ i' j' =
    CategoryTheory.CategoryStruct.comp (K.extendXIso e hi).hom
      (CategoryTheory.CategoryStruct.comp (φ i j) (L.extendXIso e hj).inv)
-- Mathlib.Order.Circular
/-- **Alias** of `sbtw_asymm`. -/
SBtw.sbtw.not_sbtw : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → ¬sbtw c b a
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.sum_obj_map : ∀ {I : Type w₀} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₀}
  {D : J → Type u₁} [inst_1 : (j : J) → CategoryTheory.Category.{v₁, u₁} (D j)] (X : (i : I) → C i)
  {x x_1 : (j : J) → D j} (f : x ⟶ x_1) (s : I ⊕ J),
  ((CategoryTheory.Pi.sum C).obj X).map f s =
    match s with
    | Sum.inl i => CategoryTheory.CategoryStruct.id (X i)
    | Sum.inr j => f j
-- Mathlib.Data.Nat.Digits.Lemmas
_private.Mathlib.Data.Nat.Digits.Lemmas.0.List.alternatingSum.match_1.eq_1 : ∀ {G : Type u_1} (motive : List G → Sort u_2) (h_1 : Unit → motive []) (h_2 : (g : G) → motive [g])
  (h_3 : (g h : G) → (t : List G) → motive (g :: h :: t)),
  (match [] with
    | [] => h_1 ()
    | [g] => h_2 g
    | g :: h :: t => h_3 g h t) =
    h_1 ()
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateSubgroup.sq_covBySMul : ∀ {G : Type u_1} [inst : Group G] {K : ℝ} {A : Set G}, IsApproximateSubgroup K A → CovBySMul G K (A ^ 2) A
-- Lean.Server.CodeActions.Basic
Lean.Server.LazyCodeAction.mk.injEq : ∀ (eager : Lean.Lsp.CodeAction) (lazy? : Option (IO Lean.Lsp.CodeAction)) (eager_1 : Lean.Lsp.CodeAction)
  (lazy?_1 : Option (IO Lean.Lsp.CodeAction)),
  ({ eager := eager, lazy? := lazy? } = { eager := eager_1, lazy? := lazy?_1 }) = (eager = eager_1 ∧ lazy? = lazy?_1)
-- Mathlib.LinearAlgebra.TensorProduct.Associator
/-- This special case is useful for describing the interplay between `dualTensorHomEquiv` and
composition of linear maps.

E.g., composition of linear maps gives a map `(M → N) ⊗ (N → P) → (M → P)`, and applying
`dual_tensor_hom_equiv.symm` to the three hom-modules gives a map
`(M.dual ⊗ N) ⊗ (N.dual ⊗ P) → (M.dual ⊗ P)`, which agrees with the application of `contractRight`
on `N ⊗ N.dual` after the suitable rebracketing.
 -/
TensorProduct.tensorTensorTensorAssoc : (R : Type u_1) →
  [inst : CommSemiring R] →
    (M : Type u_5) →
      (N : Type u_6) →
        (P : Type u_7) →
          (Q : Type u_8) →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : AddCommMonoid N] →
                [inst_3 : AddCommMonoid P] →
                  [inst_4 : AddCommMonoid Q] →
                    [inst_5 : Module R M] →
                      [inst_6 : Module R N] →
                        [inst_7 : Module R Q] →
                          [inst_8 : Module R P] →
                            TensorProduct R (TensorProduct R M N) (TensorProduct R P Q) ≃ₗ[R]
                              TensorProduct R (TensorProduct R M (TensorProduct R N P)) Q
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.PosDef.anisotropic : ∀ {M : Type u_4} {N : Type u_5} {R₂ : Type u} [inst : CommSemiring R₂] [inst_1 : AddCommMonoid M] [inst_2 : Module R₂ M]
  [inst_3 : PartialOrder N] [inst_4 : AddCommMonoid N] [inst_5 : Module R₂ N] {Q : QuadraticMap R₂ M N},
  Q.PosDef → Q.Anisotropic
-- Mathlib.SetTheory.Cardinal.Defs
/-- A cardinal lifted to the zero universe equals itself.  -/
Cardinal.lift_uzero : ∀ (a : Cardinal.{u}), Cardinal.lift.{0, u} a = a
-- Mathlib.Algebra.Polynomial.Div
Polynomial.neg_modByMonic : ∀ {R : Type u} [inst : CommRing R] (p q : Polynomial R), -p %ₘ q = -(p %ₘ q)
-- Mathlib.Topology.Algebra.Module.Complement
ContinuousLinearMap.ofIsTopCompl_eq_add : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} {F : Type u_3} [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : TopologicalSpace F] [inst_6 : AddCommGroup F]
  [inst_7 : Module R F] [inst_8 : ContinuousAdd F] {p q : Submodule R E} (h : Submodule.IsTopCompl p q) (φ : ↥p →L[R] F)
  (ψ : ↥q →L[R] F), ContinuousLinearMap.ofIsTopCompl h φ ψ = φ ∘SL p.projectionOntoL q h + ψ ∘SL q.projectionOntoL p ⋯
-- Lean.Elab.Do.ForwardSyntax
Lean.Elab.Do.ForwardArg.mk.injEq : ∀ (binders : Array (Lean.TSyntax `Lean.Parser.Term.funBinder)) (body : Lean.DoSeq)
  (binders_1 : Array (Lean.TSyntax `Lean.Parser.Term.funBinder)) (body_1 : Lean.DoSeq),
  ({ binders := binders, body := body } = { binders := binders_1, body := body_1 }) =
    (binders = binders_1 ∧ body = body_1)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.filter_sub : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddGroup (β i)] (p : ι → Prop) [inst_1 : DecidablePred p]
  (f g : Π₀ (i : ι), β i), DFinsupp.filter p (f - g) = DFinsupp.filter p f - DFinsupp.filter p g
-- Mathlib.CategoryTheory.Countable
CategoryTheory.CountableCategory.instLocallySmallObjAsType : ∀ (α : Type u) [inst : CategoryTheory.Category.{v, u} α] [inst_1 : CategoryTheory.CountableCategory α],
  CategoryTheory.LocallySmall.{0, v, 0} (CategoryTheory.CountableCategory.ObjAsType α)
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
HomologicalComplex.g_shortComplexTruncLEX₃ToTruncGE_assoc : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C] [inst_1 : CategoryTheory.Abelian C]
  (K : HomologicalComplex C c) {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} [inst_2 : e₁.IsTruncLE]
  [inst_3 : e₂.IsTruncGE] (ac : e₁.AreComplementary e₂) {Z : HomologicalComplex C c} (h : K.truncGE e₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.shortComplexTruncLE e₁).g
      (CategoryTheory.CategoryStruct.comp (K.shortComplexTruncLEX₃ToTruncGE ac) h) =
    CategoryTheory.CategoryStruct.comp (K.πTruncGE e₂) h
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_diff_le_size_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  (m₁ \ m₂).size ≤ m₁.size
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- (Implementation) The map from `Spec(𝒪ₓ/I)` to `X`. See `IdealSheafData.subschemeι` instead.  -/
AlgebraicGeometry.Scheme.IdealSheafData.gluedTo : {X : AlgebraicGeometry.Scheme} → (I : X.IdealSheafData) → I.glueData.glued ⟶ X
-- Mathlib.Order.Hom.WithTopBot
InfHom.withBot_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β]
  [inst_2 : SemilatticeInf γ] (f : InfHom β γ) (g : InfHom α β), (f.comp g).withBot = f.withBot.comp g.withBot
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int32.reduceDiv : Lean.Meta.Simp.DSimproc
-- Lean.Environment
/-- Checks whether `modifyState (asyncDecl := declName)` may be called on an async environment
extension; see `AsyncMode.async` for details.
 -/
Lean.EnvExtension.asyncMayModify : {σ : Type} →
  (ext : Lean.EnvExtension σ) → Lean.Environment → Lean.Name → optParam Lean.EnvExtension.AsyncMode ext.asyncMode → Bool
-- Init.Data.SInt.Bitwise
ISize.and_zero : ∀ {a : ISize}, a &&& 0 = 0
-- Mathlib.Algebra.Group.Basic
div_left_injective : ∀ {G : Type u_3} [inst : Group G] {b : G}, Function.Injective fun a => a / b
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.hom_zero : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R}, ModuleCat.Hom.hom 0 = 0
-- Init.Data.Array.Lemmas
Array.isEqv_eq : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs ys : Array α},
  ((xs.isEqv ys fun x1 x2 => x1 == x2) = true) = (xs = ys)
-- Init.Data.Option.Basic
Option.getD_some : ∀ {α : Type u_1} {a b : α}, (some a).getD b = a
-- Init.Control.StateRef
instMonadFinallyStateRefT' : {m : Type → Type} → {ω σ : Type} → [MonadFinally m] → MonadFinally (StateRefT' ω σ m)
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.HeapNode.rankTR.go.match_1.splitter : {α : Type u_1} →
  (motive : Batteries.BinomialHeap.Imp.HeapNode α → ℕ → Sort u_2) →
    (x : Batteries.BinomialHeap.Imp.HeapNode α) →
      (x_1 : ℕ) →
        ((r : ℕ) → motive Batteries.BinomialHeap.Imp.HeapNode.nil r) →
          ((a : α) →
              (child s : Batteries.BinomialHeap.Imp.HeapNode α) →
                (r : ℕ) → motive (Batteries.BinomialHeap.Imp.HeapNode.node a child s) r) →
            motive x x_1
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.RightHomologyMapData.homologyMap_comm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) h₂.homologyIso.hom =
    CategoryTheory.CategoryStruct.comp h₁.homologyIso.hom γ.φH
-- Init.System.IO
IO.FS.SystemTime.mk.injEq : ∀ (sec : ℤ) (nsec : UInt32) (sec_1 : ℤ) (nsec_1 : UInt32),
  ({ sec := sec, nsec := nsec } = { sec := sec_1, nsec := nsec_1 }) = (sec = sec_1 ∧ nsec = nsec_1)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.dropUntil_copy : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v w v' w' : V} (p : G.Walk v w) (hv : v = v') (hw : w = w')
  (h : u ∈ (p.copy hv hw).support), (p.copy hv hw).dropUntil u h = (p.dropUntil u ⋯).copy ⋯ hw
-- Mathlib.Algebra.Group.Pi.Lemmas
Function.update_zero : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Zero (f i)] [inst_1 : DecidableEq I] (i : I),
  Function.update 0 i 0 = 0
-- Mathlib.Order.BoundedOrder.Basic
ULift.instOrderBot.eq_1 : ∀ {α : Type u} [inst : LE α] [inst_1 : OrderBot α], ULift.instOrderBot = OrderBot.lift ULift.down ⋯ ⋯
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
GenContFract.IntFractPair.inhabited : {K : Type u_1} → [Inhabited K] → Inhabited (GenContFract.IntFractPair K)
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.isUnit_jacobian_of_linearIndependent_of_span_eq_top : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ) [inst_3 : Finite σ],
  (LinearIndependent S fun j i => (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv (P.map i)) (P.relation j))) →
    Submodule.span S
          (Set.range fun j i => (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv (P.map i)) (P.relation j))) =
        ⊤ →
      IsUnit P.jacobian
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.foldr_eq_foldr_toArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {δ : Type w}
  {f : (a : α) → β a → δ → δ} {init : δ},
  Std.DTreeMap.Raw.foldr f init t = Array.foldr (fun a b => f a.fst a.snd b) init t.toArray
-- Mathlib.AlgebraicGeometry.Group.Affine
/-- `Spec` as a functor from `R`-algebras to schemes over `Spec R` is braided.

The monoidal data is copied from `Functor.Braided.ofChosenFiniteProducts` so that `ε`, `η` are
definitionally `𝟙 (Spec R)` and `μ`, `δ` are definitionally `pullbackSpecIso`.  -/
AlgebraicGeometry.braidedAlgSpec : {R : CommRingCat} → (AlgebraicGeometry.algSpec R).Braided
-- Mathlib.Algebra.Regular.Opposite
/-- **Alias** of the reverse direction of `isRegular_unop`. -/
IsRegular.unop : ∀ {R : Type u_1} [inst : Mul R] {a : Rᵐᵒᵖ}, IsRegular a → IsRegular (MulOpposite.unop a)
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCochain.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {G : CategoryTheory.Functor Cᵒᵖ GrpCat} {I : Type w'}
  {U : I → C} {ev : (i j : I) → ⦃T : C⦄ → (T ⟶ U i) → (T ⟶ U j) → ↑(G.obj (Opposite.op T))}
  {ev_precomp :
    autoParam
      (∀ (i j : I) ⦃T T' : C⦄ (φ : T ⟶ T') (a : T' ⟶ U i) (b : T' ⟶ U j),
        (CategoryTheory.ConcreteCategory.hom (G.map φ.op)) (ev i j a b) =
          ev i j (CategoryTheory.CategoryStruct.comp φ a) (CategoryTheory.CategoryStruct.comp φ b))
      CategoryTheory.PresheafOfGroups.OneCochain.ev_precomp._autoParam}
  {ev_1 : (i j : I) → ⦃T : C⦄ → (T ⟶ U i) → (T ⟶ U j) → ↑(G.obj (Opposite.op T))}
  {ev_precomp_1 :
    autoParam
      (∀ (i j : I) ⦃T T' : C⦄ (φ : T ⟶ T') (a : T' ⟶ U i) (b : T' ⟶ U j),
        (CategoryTheory.ConcreteCategory.hom (G.map φ.op)) (ev_1 i j a b) =
          ev_1 i j (CategoryTheory.CategoryStruct.comp φ a) (CategoryTheory.CategoryStruct.comp φ b))
      CategoryTheory.PresheafOfGroups.OneCochain.ev_precomp._autoParam},
  { ev := ev, ev_precomp := ev_precomp } = { ev := ev_1, ev_precomp := ev_precomp_1 } → ev = ev_1
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.mk_map_eq_iff_of_mono : ∀ {X : SSet} {n m : ℕ} (x : X.obj (Opposite.op { len := n })) (f : { len := m } ⟶ { len := n }) [CategoryTheory.Mono f],
  { dim := m, simplex := (CategoryTheory.ConcreteCategory.hom (X.map f.op)) x } = { dim := n, simplex := x } ↔
    CategoryTheory.IsIso f
-- Mathlib.Data.FunLike.IsApply
/-- `IsNatCastApply F α` states for all `n : ℕ` and `x : α`, `(n : F) x = n • x`.  -/
IsNatCastApply : (F : Type u_1) → (α : outParam (Type u_2)) → [FunLike F α α] → [NatCast F] → [SMul ℕ α] → Prop
-- Mathlib.CategoryTheory.Functor.Trifunctor
CategoryTheory.bifunctorComp₂₃_map_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {X₁ Y₁ : C₁} (φ : X₁ ⟶ Y₁) (X₂ : C₂) (X₃ : C₃),
  (((CategoryTheory.bifunctorComp₂₃ F G₂₃).map φ).app X₂).app X₃ = (F.map φ).app ((G₂₃.obj X₂).obj X₃)
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_inv_app_app : ∀ {X Y : AlgebraicGeometry.Scheme} {U : X.Opens} {f g : X ⟶ Y} (hf : f = g) [inst : AlgebraicGeometry.IsOpenImmersion f]
  [inst_1 : AlgebraicGeometry.IsOpenImmersion g] (M : Y.Modules),
  AlgebraicGeometry.Scheme.Modules.Hom.app ((AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr hf).inv.app M) U =
    M.presheaf.map (CategoryTheory.eqToHom ⋯).op
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Profinite.NobelingProof.Products.span_nil_eq_top : ∀ {I : Type u_1} [inst : LinearOrder I],
  Submodule.span ℤ (Profinite.NobelingProof.Products.eval {fun x => false} '' {Profinite.NobelingProof.Products.nil}) =
    ⊤
-- Lean.Server.Requests
Lean.Server.SerializedLspResponse.response? : Lean.Server.SerializedLspResponse → Option Lean.Json
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_eq_none_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.minKey? = none ↔ t = ∅
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
/-- A simply connected space is one whose fundamental groupoid is equivalent to `Discrete Unit`  -/
SimplyConnectedSpace : (X : Type u_3) → [TopologicalSpace X] → Prop
-- Lean.Meta.ForEachExpr
_private.Lean.Meta.ForEachExpr.0.Lean.Meta.visitForall.visit : {m : Type → Type u_1} →
  [Monad m] → [MonadControlT Lean.MetaM m] → (Lean.Expr → m Unit) → Array Lean.Expr → Lean.Expr → m Unit
-- Init.Data.Ord.Basic
compareOfLessAndEq_eq_gt : ∀ {α : Type u} [inst : LT α] [inst_1 : LE α] [inst_2 : DecidableLT α] [inst_3 : DecidableEq α],
  (∀ {x y : α}, x ≤ y → y ≤ x → x = y) →
    (∀ (x y : α), x ≤ y ∨ y ≤ x) →
      (∀ {x y : α}, ¬x ≤ y ↔ y < x) → ∀ (x y : α), compareOfLessAndEq x y = Ordering.gt ↔ y < x
-- Init.Data.SInt.Lemmas
ISize.toNat_toUSize_of_le : ∀ {x : ISize}, 0 ≤ x → x.toUSize.toNat = x.toNatClampNeg
-- Mathlib.Algebra.Group.UniqueProds.Basic
_private.Mathlib.Algebra.Group.UniqueProds.Basic.0.Prod.upAddHom : (G : Type u) → (H : Type v) → [inst : Add G] → [inst_1 : Add H] → G × H →ₙ+ (b : Bool) → I✝ G H b
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.continuousAt_add_bot_coe : ∀ (a : ℝ), ContinuousAt (fun p => p.1 + p.2) (⊥, ↑a)
-- Mathlib.Algebra.Algebra.Opposite
AlgHom.toLinearMap_toOpposite : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), Commute (f x) (f y)),
  (f.toOpposite hf).toLinearMap = ↑(MulOpposite.opLinearEquiv R) ∘ₗ f.toLinearMap
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.LHom.setOfPred_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 α),
  Set.ofPred (φ.onFormula ψ).Realize = Set.ofPred ψ.Realize
-- Init.Data.Option.Lemmas
Option.max_eq_some_iff : ∀ {α : Type u_1} [inst : Max α] {o o' : Option α} {a : α},
  o ⊔ o' = some a ↔ o = some a ∧ o' = none ∨ o = none ∧ o' = some a ∨ ∃ b c, o = some b ∧ o' = some c ∧ b ⊔ c = a
-- Aesop.Tree.ExtractScript
Aesop.ExtractScriptM.State : Type
-- Init.Data.Ord.Basic
Ordering.isGE_gt : Ordering.gt.isGE = true
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
NNRealRMK.le_rieszMeasure_of_tsupport_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal)
  [inst_1 : T2Space X] [inst_2 : LocallyCompactSpace X] [inst_3 : MeasurableSpace X] [inst_4 : BorelSpace X]
  {f : CompactlySupportedContinuousMap X NNReal},
  (∀ (x : X), f x ≤ 1) → ∀ {V : Set X}, tsupport ⇑f ⊆ V → ↑(Λ f) ≤ (NNRealRMK.rieszMeasure Λ) V
-- Init.Grind.Module.Basic
Lean.Grind.AddCommGroup.sub_eq_iff : ∀ {M : Type u} [inst : Lean.Grind.AddCommGroup M] {a b c : M}, a - b = c ↔ a = c + b
-- Mathlib.Data.Set.Image
Set.forall_mem_range : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α} {p : α → Prop}, (∀ a ∈ Set.range f, p a) ↔ ∀ (i : ι), p (f i)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_filter_eq_size_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.size = t.size ↔
    ∀ (a : α) (h : Std.DTreeMap.Internal.Impl.contains a t = true), f a (t.get a h) = true
-- Mathlib.Topology.Algebra.Group.Basic
continuousAt_inv_iff : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [ContinuousInv G]
  [inst_3 : TopologicalSpace α] {f : α → G} {x : α}, ContinuousAt f⁻¹ x ↔ ContinuousAt f x
-- Mathlib.SetTheory.Lists
Lists.Equiv.refl : ∀ {α : Type u_1} (l : Lists α), l.Equiv l
-- Init.Data.Array.MinMax
Array.isSome_min?_of_mem : ∀ {α : Type u_1} {xs : Array α} [inst : Min α] {a : α}, a ∈ xs → xs.min?.isSome = true