mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}, ∅.WF
-- Mathlib.Algebra.BigOperators.Finprod
finsum_eq_indicator_apply : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (s : Set α) (f : α → M) (a : α),
  ∑ᶠ (_ : a ∈ s), f a = s.indicator f a
-- Lean.Elab.Binders
Lean.Elab.Term.LetIdDeclView.binders : Lean.Elab.Term.LetIdDeclView → Array Lean.Syntax
-- Mathlib.Topology.Semicontinuity.Basic
/-- The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with
`[ContinuousAdd]`. The primed version of the lemma uses an explicit continuity assumption on
addition, for application to `EReal`.  -/
UpperSemicontinuousOn.add : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_5} [inst_1 : AddCommMonoid γ]
  [inst_2 : LinearOrder γ] [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ]
  {f g : α → γ}, UpperSemicontinuousOn f s → UpperSemicontinuousOn g s → UpperSemicontinuousOn (fun z => f z + g z) s
-- Init.Data.SInt.Lemmas
Int64.ofIntLE_eq_ofIntTruncate : ∀ {x : ℤ} {h₁ : Int64.minValue.toInt ≤ x} {h₂ : x ≤ Int64.maxValue.toInt}, Int64.ofIntLE x h₁ h₂ = Int64.ofIntClamp x
-- Mathlib.Data.Seq.Basic
Stream'.Seq.update_cons_succ : ∀ {α : Type u} (hd : α) (tl : Stream'.Seq α) (f : α → α) (n : ℕ),
  (Stream'.Seq.cons hd tl).update (n + 1) f = Stream'.Seq.cons hd (tl.update n f)
-- Mathlib.Tactic.Explode.Datatypes
/-- A type of this expression as a `MessageData`. Make sure to use `addMessageContext`.  -/
Mathlib.Explode.Entry.type : Mathlib.Explode.Entry → Lean.MessageData
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs.0.EisensteinSeries.denom_aux : ∀ (A B : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane),
  ↑(↑(A * B) 1 0) *
      UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) B)) ↑z =
    ↑(↑A 1 0) * ↑(↑B).det +
      ↑(↑B 1 0) *
        UpperHalfPlane.denom
          (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) A) *
            Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) B))
          ↑z
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Fact.mk.sizeOf_spec : ∀ (coeffs : Lean.Omega.Coeffs) (constraint : Lean.Omega.Constraint)
  (justification : Lean.Elab.Tactic.Omega.Justification constraint coeffs),
  sizeOf { coeffs := coeffs, constraint := constraint, justification := justification } =
    1 + sizeOf coeffs + sizeOf constraint + sizeOf justification
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_sub_const_uIcc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => x - a) '' Set.uIcc b c = Set.uIcc (b - a) (c - a)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.natDegree_Φ_pos : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [Nontrivial R] {n : ℤ}, n ≠ 0 → 0 < (W.Φ n).natDegree
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.HomotopyCategory.homMk_comp_homMk_assoc : ∀ {V : SSet.Truncated 2}
  {x₀ x₁ x₂ : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })}
  {e₀₁ : SSet.Truncated.Edge x₀ x₁} {e₁₂ : SSet.Truncated.Edge x₁ x₂} {e₀₂ : SSet.Truncated.Edge x₀ x₂}
  (h : e₀₁.CompStruct e₁₂ e₀₂) {Z : V.HomotopyCategory} (h : SSet.Truncated.HomotopyCategory.mk x₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.Truncated.HomotopyCategory.homMk e₀₁)
      (CategoryTheory.CategoryStruct.comp (SSet.Truncated.HomotopyCategory.homMk e₁₂) h) =
    CategoryTheory.CategoryStruct.comp (SSet.Truncated.HomotopyCategory.homMk e₀₂) h
-- Mathlib.RingTheory.Extension.Cotangent.Basic
/-- The cotangent complex given by a presentation `R[X] → S` (i.e. a closed embedding `S ↪ Aⁿ`).  -/
Algebra.Extension.cotangentComplex : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (P : Algebra.Extension R S) → P.Cotangent →ₗ[S] P.CotangentSpace
-- Mathlib.GroupTheory.GroupAction.Hom
FaithfulSMul.of_injective : ∀ {M' : Type u_1} {X : Type u_5} [inst : SMul M' X] {Y : Type u_6} [inst_1 : SMul M' Y] {F : Type u_8}
  [inst_2 : FunLike F X Y] [FaithfulSMul M' X] [MulActionHomClass F M' X Y] (f : F),
  Function.Injective ⇑f → FaithfulSMul M' Y
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
/-- Effective **Szemerédi Regularity Lemma**: For any sufficiently large graph, there is an
`ε`-uniform equipartition of bounded size (where the bound does not depend on the graph).  -/
szemeredi_regularity : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (G : SimpleGraph α) [inst_2 : DecidableRel G.Adj] {ε : ℝ}
  {l : ℕ},
  0 < ε →
    l ≤ Fintype.card α →
      ∃ P, P.IsEquipartition ∧ l ≤ P.parts.card ∧ P.parts.card ≤ SzemerediRegularity.bound ε l ∧ P.IsUniform G ε
-- Mathlib.Algebra.GroupWithZero.ProdHom
MonoidWithZeroHom.fst_apply_coe : ∀ {G₀ : Type u_1} {H₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀] (x : G₀ˣ × H₀ˣ),
  (MonoidWithZeroHom.fst G₀ H₀) ↑x = ↑x.1
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.natCast_toProd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] (n : ℕ), (↑n).toProd = ↑n
-- Init.Data.Vector.Lemmas
Vector.finIdxOf?_mk : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {xs : Array α} (h : xs.size = n) (x : α),
  (Vector.mk xs h).finIdxOf? x = Option.map (Fin.cast h) (xs.finIdxOf? x)
-- Mathlib.Data.Finset.Sum
/-- Given a finset of elements `α ⊕ β`, extract all the elements of the form `β`. This
forms a quasi-inverse to `disjSum`, in that it recovers its right input.

See also `List.partitionMap`.
 -/
Finset.toRight : {α : Type u_1} → {β : Type u_2} → Finset (α ⊕ β) → Finset β
-- Mathlib.CategoryTheory.Comma.CatCommSq
CategoryTheory.Arrow.catCommSq : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        [inst : CategoryTheory.Category.{u_5, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{u_6, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{u_7, u_3} D₁] →
              [inst_3 : CategoryTheory.Category.{u_8, u_4} D₂] →
                (T : CategoryTheory.Functor C₁ C₂) →
                  (L : CategoryTheory.Functor C₁ D₁) →
                    (R : CategoryTheory.Functor C₂ D₂) →
                      (B : CategoryTheory.Functor D₁ D₂) →
                        [CategoryTheory.CatCommSq T L R B] →
                          CategoryTheory.CatCommSq T.mapArrow L.mapArrow R.mapArrow B.mapArrow
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.Mk₁.map.eq_3 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) (isLt isLt_1 : 1 < 2)
  (x_3 : ⟨1, isLt⟩ ≤ ⟨1, isLt_1⟩),
  CategoryTheory.ComposableArrows.Mk₁.map f ⟨1, isLt⟩ ⟨1, isLt_1⟩ x_3 =
    CategoryTheory.CategoryStruct.id (CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ ⟨1, isLt⟩)
-- Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
HomologicalComplex.homology.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K K_1 : HomologicalComplex C c) (e_K : K = K_1) (i i_1 : ι) (e_i : i = i_1)
  [inst_2 : K.HasHomology i], K.homology i = K_1.homology i_1
-- Mathlib.Order.Bounds.Basic
DirectedOn.le_of_minimal : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a b : α},
  DirectedOn (fun x y => y ≤ x) s → Minimal (fun x => x ∈ s) a → b ∈ s → a ≤ b
-- Mathlib.Algebra.Order.Sub.Basic
/-- A `CanonicallyOrderedAddCommMonoid` with ordered subtraction and order-reflecting addition is
cancellative. This is not an instance as it would form a typeclass loop.

See note [reducible non-instances].  -/
CanonicallyOrderedAddCommMonoid.toAddCancelCommMonoid : (α : Type u_1) →
  [inst : AddCommMonoid α] →
    [inst_1 : PartialOrder α] → [inst_2 : Sub α] → [OrderedSub α] → [AddLeftReflectLE α] → AddCancelCommMonoid α
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.LiesOver.mk : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {φ : L →+* ℂ} {ψ : K →+* ℂ},
  φ.comp (algebraMap K L) = ψ → NumberField.ComplexEmbedding.LiesOver φ ψ
-- Mathlib.LinearAlgebra.Dimension.RankNullity
Submodule.rank_sup_add_rank_inf_eq : ∀ {R : Type u_1} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [HasRankNullity.{u, u_1} R] (s t : Submodule R M),
  Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) = Module.rank R ↥s + Module.rank R ↥t
-- Mathlib.Order.PartialSups
comp_partialSups : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β]
  [inst_2 : Preorder ι] [inst_3 : LocallyFiniteOrderBot ι] {F : Type u_4} [inst_4 : FunLike F α β] [SupHomClass F α β]
  (f : ι → α) (g : F), ⇑(partialSups (⇑g ∘ f)) = ⇑g ∘ ⇑(partialSups f)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isSome_getElem?_toArray_ric_eq : ∀ {n i : ℕ}, ((*...=n).toArray[i]?.isSome = true) = (i ≤ n)
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- The underlying value of a bundled eigenvalue.  -/
Module.End.UnifEigenvalues.val : {R : Type v} →
  {M : Type w} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (f : Module.End R M) → (k : ℕ∞) → f.UnifEigenvalues k → R
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorLeftUnitor_naturality : ∀ {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 Y' : CategoryTheory.GradedObject J D} (φ : Y ⟶ Y')
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj
          Y).HasMap
      p]
  [inst_7 :
    (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj
          Y').HasMap
      p],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.mapBifunctorMapMap F p
        (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj X)) φ)
      (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y').hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).hom φ
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.addConst_neg_left : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : DecidableEq G] (A B : Finset G), (-A).addConst B = A.subConst B
-- Mathlib.Algebra.MonoidAlgebra.Division
AddMonoidAlgebra.coeff_divOf : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] [inst_2 : IsCancelAdd G] (g : G)
  (x : AddMonoidAlgebra k G) (g' : G), (x.divOf g).coeff g' = x.coeff (g + g')
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.toList_map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} (m : Std.DHashMap.Internal.Raw₀ α β) {f : (a : α) → β a → γ a},
  (↑(Std.DHashMap.Internal.Raw₀.map f m)).toList.Perm (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) (↑m).toList)
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `1` and `*` is a left cancel monoid, if it admits an injective map that
preserves `1` and `*` to a left cancel monoid. See note [reducible non-instances].  -/
Function.Injective.leftCancelMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₁] →
      [inst_1 : One M₁] →
        [inst_2 : Pow M₁ ℕ] →
          [inst_3 : LeftCancelMonoid M₂] →
            (f : M₁ → M₂) →
              Function.Injective f →
                f 1 = 1 →
                  (∀ (x y : M₁), f (x * y) = f x * f y) →
                    (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) → LeftCancelMonoid M₁
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.IsColimit.fac_apply : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes}
  (hc : c.IsColimit) (c' : F.CoconeTypes) (j : J) (x : F.obj j), hc.desc c' (c.ι j x) = c'.ι j x
-- Lean.Parser.Do
Lean.Parser.doElemParser : optParam ℕ 0 → Lean.Parser.Parser
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.toList_filter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {f : (a : α) → β a → Bool},
  t.WF → (Std.DTreeMap.Internal.Impl.filter! f t).toList = List.filter (fun p => f p.fst p.snd) t.toList
-- Mathlib.Analysis.Calculus.Deriv.Shift
/-- Translation in the domain does not change the derivative.  -/
HasDerivAt.comp_sub_const : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} (x a : 𝕜),
  HasDerivAt f f' (x - a) → HasDerivAt (fun x => f (x - a)) f' x
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.zero_associator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N P : C}
  [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N] [inst_4 : CategoryTheory.AddMonObj P],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
        (CategoryTheory.MonoidalCategoryStruct.tensorHom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
            (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero
              CategoryTheory.AddMonObj.zero))
          CategoryTheory.AddMonObj.zero))
      (CategoryTheory.MonoidalCategoryStruct.associator M N P).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
          (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero
            CategoryTheory.AddMonObj.zero)))
-- Mathlib.NumberTheory.Height.NumberField
/-- This is the familiar definition of the logarithmic height on a number field.  -/
NumberField.logHeight₁_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : K),
  Height.logHeight₁ x = ∑ v, ↑v.mult * (v x).posLog + ∑ᶠ (v : NumberField.FinitePlace K), (v x).posLog
-- Aesop.RuleTac.Basic
Aesop.RuleApplication.successProbability? : Aesop.RuleApplication → Option Aesop.Percent
-- Aesop.Script.UScriptToSScript
Aesop.Script.StepTree.toMessageData : Aesop.Script.StepTree → Lean.MessageData
-- Mathlib.Order.Interval.Finset.Nat
Nat.range_succ_eq_Iic : ∀ (n : ℕ), Finset.range (n + 1) = Finset.Iic n
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.IndGroupInst.toMessageData : Lean.Elab.Structural.IndGroupInst → Lean.MessageData
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.all_one_of_le_one_le_of_prod_eq_one : ∀ {M : Type u_3} [inst : CommMonoid M] [inst_1 : PartialOrder M] [IsOrderedMonoid M] {l : List M},
  (∀ x ∈ l, 1 ≤ x) → l.prod = 1 → ∀ {x : M}, x ∈ l → x = 1
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.enorm_integral_le_lintegral_enorm : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f : X → E} {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G},
  ‖∫ᵛ (a : X), f a ∂[B; μ]‖ₑ ≤ ‖B‖ₑ * ∫⁻ (a : X), ‖f a‖ₑ ∂μ.variation
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.zero_left : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, MeasureTheory.Measure.MutuallySingular 0 μ
-- Mathlib.LinearAlgebra.Basis.VectorSpace
Module.Basis.extendLe_subset : ∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s t : Set V}
  (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ Submodule.span K t),
  Set.range ⇑(Module.Basis.extendLe hs hst ht) ⊆ t
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.isoMk_inv_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S}
  (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j))
  (h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k))
  (w₀ :
    autoParam (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i)
      CategoryTheory.PreOneHypercover.isoMk._auto_1)
  (w₁₁ :
    autoParam
      (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k).hom (F.p₁ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₁ k) (h₀ i).hom)
      CategoryTheory.PreOneHypercover.isoMk._auto_3)
  (w₁₂ :
    autoParam
      (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k).hom (F.p₂ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₂ k) (h₀ j).hom)
      CategoryTheory.PreOneHypercover.isoMk._auto_5)
  (a : F.I₀), (CategoryTheory.PreOneHypercover.isoMk s₀ h₀ s₁ h₁ w₀ w₁₁ w₁₂).inv.s₀ a = s₀.symm a
-- Lean.HeadIndex
Lean.HeadIndex.lam.sizeOf_spec : sizeOf Lean.HeadIndex.lam = 1
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_eq_some_minKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} {he : l.isEmpty = false},
  Std.Internal.List.minKey? l = some (Std.Internal.List.minKey l he)
-- Mathlib.Algebra.Order.AddTorsor
IsOrderedVAdd.vadd_le_vadd_right : ∀ {G : Type u_3} {P : Type u_4} {inst : LE G} {inst_1 : LE P} {inst_2 : VAdd G P} [self : IsOrderedVAdd G P] (c d : G),
  c ≤ d → ∀ (a : P), c +ᵥ a ≤ d +ᵥ a
-- Mathlib.Order.RelIso.Basic
RelIso.eq_iff_eq : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) {a b : α}, f a = f b ↔ a = b
-- Mathlib.Algebra.Group.Fin.Tuple
Fin.insertNth_sub : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} [inst : (j : Fin (n + 1)) → Sub (α j)] (i : Fin (n + 1)) (x y : α i)
  (p q : (j : Fin n) → α (i.succAbove j)), i.insertNth (x - y) (p - q) = i.insertNth x p - i.insertNth y q
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instantiateRangeArgs : {pu : Lean.Compiler.LCNF.Purity} → Lean.Expr → ℕ → ℕ → Array (Lean.Compiler.LCNF.Arg pu) → Lean.Expr
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
SpectrumRestricts.starAlgHom_injective : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Semifield S] [inst_6 : StarRing S]
  [inst_7 : MetricSpace S] [inst_8 : IsTopologicalSemiring S] [inst_9 : ContinuousStar S] [inst_10 : Ring A]
  [inst_11 : StarRing A] [inst_12 : Algebra S A] [inst_13 : Algebra R S] [inst_14 : Algebra R A]
  [inst_15 : IsScalarTower R S A] [inst_16 : StarModule R S] [inst_17 : ContinuousSMul R S] {a : A}
  {φ : C(↑(spectrum S a), S) →⋆ₐ[S] A},
  Function.Injective ⇑φ →
    ∀ {f : C(S, R)} (h : SpectrumRestricts a ⇑f),
      Function.Injective ⇑(algebraMap R S) → Function.Injective ⇑(SpectrumRestricts.starAlgHom φ h)
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.toContinuousLinearMap_zero : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W}, ContIntertwiningMap.toContinuousLinearMap 0 = 0
-- Mathlib.Algebra.Quaternion
Quaternion.imK_ratCast : ∀ {R : Type u_1} [inst : Field R] (q : ℚ), (↑q).imK = 0
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.homeomorphAddCircle_symm_apply_mk : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] (p q : 𝕜) [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [inst_4 : OrderTopology 𝕜] (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜),
  (AddCircle.homeomorphAddCircle p q hp hq).symm ↑x = ↑(x * (q⁻¹ * p))
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.coe_zero : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β], ⇑0 = 0
-- Init.Grind.Module.Envelope
_private.Init.Grind.Module.Envelope.0.Lean.Grind.IntModule.OfNatModule.rel : {α : Type u} →
  [inst : Lean.Grind.NatModule α] →
    Equivalence (Lean.Grind.IntModule.OfNatModule.r α) →
      Lean.Grind.IntModule.OfNatModule.Q α → Lean.Grind.IntModule.OfNatModule.Q α → Prop
-- Mathlib.Algebra.Module.FinitePresentation
Module.finitePresentation_iff_finite : ∀ (R : Type u_1) (M : Type u_2) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherianRing R],
  Module.FinitePresentation R M ↔ Module.Finite R M
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.ofMagma_apply : ∀ (R : Type u_8) (M : Type u_9) [inst : Semiring R] [inst_1 : Add M] (a : Multiplicative M),
  (AddMonoidAlgebra.ofMagma R M) a = AddMonoidAlgebra.single (Multiplicative.toAdd a) 1
-- Mathlib.Algebra.Order.Monoid.Lex
OrderAddMonoidHom.fst_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddMonoid β]
  [inst_3 : Preorder β] (self : α × β), (OrderAddMonoidHom.fst α β) self = self.1
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.homQuotientZSMulOfHom_comp : ∀ {A B : Type u} [inst : AddCommGroup A] [inst_1 : AddCommGroup B] (f : A →+ B) (g : B →+ A) (n : ℤ),
  QuotientAddGroup.homQuotientZSMulOfHom (f.comp g) n =
    (QuotientAddGroup.homQuotientZSMulOfHom f n).comp (QuotientAddGroup.homQuotientZSMulOfHom g n)
-- Mathlib.Order.Filter.Bases.Basic
/-- A filter basis `B` on a type `α` is a nonempty collection of sets of `α`
such that the intersection of two elements of this collection contains some element
of the collection.  -/
FilterBasis : Type u_6 → Type u_6
-- Init.Data.List.MinMax
List.le_max_of_mem : ∀ {α : Type u_1} [inst : Max α] [inst_1 : LE α] [Std.IsLinearOrder α] [Std.LawfulOrderMax α] {l : List α} {a : α}
  (ha : a ∈ l), a ≤ l.max ⋯
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.algEquivOfIso_apply : ∀ {R : Type u} [inst : CommRing R] {A B : CommAlgCat R} (i : A ≅ B) (a : ↑A),
  (CommAlgCat.algEquivOfIso i) a = (CategoryTheory.ConcreteCategory.hom i.hom) a
-- Init.Control.Lawful.Basic
bind_pure_unit : ∀ {m : Type u_1 → Type u_2} [inst : Monad m] [LawfulMonad m] {x : m PUnit.{u_1 + 1}},
  (do
      x
      pure PUnit.unit) =
    x
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- If a vector space has a finite basis, then its dimension (seen as a cardinal) is equal to the
cardinality of the basis.  -/
rank_eq_card_basis : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {ι : Type w} [inst_4 : Fintype ι] (h : Module.Basis ι R M), Module.rank R M = ↑(Fintype.card ι)
-- Mathlib.Algebra.Group.Basic
div_ne_one : ∀ {G : Type u_3} [inst : Group G] {a b : G}, a / b ≠ 1 ↔ a ≠ b
-- Mathlib.Data.ENat.Basic
ENat.instUniqueUnits : Unique ℕ∞ˣ