mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.FiberBundle.Trivialization
/-- A fiberwise inverse to `e'`. The function `F → E x` that induces a local inverse
`B × F → TotalSpace F E` of `e'` on `e'.baseSet`. It takes on junk values chosen using
`Classical.arbitrary` outside `e'.baseSet`.  -/
Bundle.Trivialization.symm : {B : Type u_1} →
  {F : Type u_2} →
    {E : B → Type u_3} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] →
            [∀ (x : B), Nonempty (E x)] → Bundle.Trivialization F Bundle.TotalSpace.proj → (b : B) → F → E b
-- Mathlib.Order.Interval.Finset.Defs
Subtype.instLocallyFiniteOrderTop : {α : Type u_1} →
  [inst : Preorder α] →
    (p : α → Prop) → [DecidablePred p] → [LocallyFiniteOrderTop α] → LocallyFiniteOrderTop (Subtype p)
-- Mathlib.Order.RelSeries
RelSeries.mk.sizeOf_spec : ∀ {α : Type u_1} {r : SetRel α α} [inst : SizeOf α] [inst_1 : (a : α × α) → SizeOf (r a)] (length : ℕ)
  (toFun : Fin (length + 1) → α) (step : ∀ (i : Fin length), (toFun i.castSucc, toFun i.succ) ∈ r),
  sizeOf { length := length, toFun := toFun, step := step } = 1 + sizeOf length
-- Mathlib.LinearAlgebra.Dual.Defs
Module.evalEquiv_apply : ∀ (R : Type u_3) (M : Type u_4) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.IsReflexive R M] (m : M), (Module.evalEquiv R M) m = (Module.Dual.eval R M) m
-- Init.Data.UInt.Bitwise
UInt32.shiftRight_zero : ∀ {a : UInt32}, a >>> 0 = a
-- Mathlib.MeasureTheory.Measure.GiryMonad
Measurable.smul_measure : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → ENNReal},
  Measurable f → ∀ (μ : MeasureTheory.Measure β), Measurable fun x => f x • μ
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.summable_measure_toReal : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [hμ : MeasureTheory.IsFiniteMeasure μ]
  {f : ℕ → Set α},
  (∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Function.onFun Disjoint f) → Summable fun x => μ.real (f x)
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.hsum_orderTop_of_le : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  {s : HahnSeries.SummableFamily Γ R α} {g : Γ} {a : α},
  ↑g = (s a).orderTop →
    (∀ (b : α), ∀ g' ∈ (s b).support, g ≤ g') → (∀ (b : α), b ≠ a → (s b).coeff g = 0) → s.hsum.orderTop = ↑g
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.adicAbv_def`. -/
NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] {x : K},
  (NumberField.HeightOneSpectrum.adicAbv K v) x =
    ↑((WithZeroMulInt.toNNReal ⋯) ((IsDedekindDomain.HeightOneSpectrum.valuation K v) x))
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.mem_ker_mkLinearMap_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Submonoid R}
  {m : M}, m ∈ (LocalizedModule.mkLinearMap S M).ker ↔ ∃ r ∈ S, r • m = 0
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.enriched_id_comp_assoc : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₁]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] {Z : V}
  (h : CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor
          (CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Enriched.FunctorCategory.enrichedId V F₁)
          (CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedComp V F₁ F₁ F₂) h)) =
    h
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.mul_upcrossingsBefore_le : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {ω : Ω},
  a ≤ f N ω →
    a < b →
      (b - a) * ↑(MeasureTheory.upcrossingsBefore a b f N ω) ≤
        ∑ k ∈ Finset.range N, MeasureTheory.upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_of_core_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Bool
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.inr_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
      (CategoryTheory.kernelCokernelCompSequence.π f g) =
    CategoryTheory.Limits.cokernel.π (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.lowerCentralSeries_pi_le : ∀ {η : Type u_2} {Gs : η → Type u_3} [inst : (i : η) → AddGroup (Gs i)] (Ss : (i : η) → AddSubgroup (Gs i)) (n : ℕ),
  (AddSubgroup.pi Set.univ Ss).lowerCentralSeries n ≤ AddSubgroup.pi Set.univ fun i => (Ss i).lowerCentralSeries n
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
MvQPF.Cofix.corec'.eq_1 : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u}
  (g : β → F (α ::: (MvQPF.Cofix F α ⊕ β))) (x : β),
  MvQPF.Cofix.corec' g x =
    MvQPF.Cofix.corec (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ MvQPF.Cofix.dest) g) (Sum.inr x)
-- Mathlib.Probability.Distributions.SetBernoulli
ProbabilityTheory.IsSetBernoulli.ae_subset : ∀ {ι : Type u_1} {Ω : Type u_2} {m : MeasurableSpace Ω} {X : Ω → Set ι} {u : Set ι} {p : ↑unitInterval}
  {P : MeasureTheory.Measure Ω} [Countable ι], ProbabilityTheory.IsSetBernoulli X u p P → ∀ᵐ (ω : Ω) ∂P, X ω ⊆ u
-- Mathlib.SetTheory.Ordinal.Exponential
_private.Mathlib.SetTheory.Ordinal.Exponential.0.Ordinal.opow_of_ne_zero : ∀ {a b : Ordinal.{u_1}}, a ≠ 0 → a ^ b = Ordinal.limitRecOn b 1 (fun x x_1 => x_1 * a) fun o x f => ⨆ x, f ↑x ⋯
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.neg_apply : ∀ {A : Type u_2} {ι : Type u_3} {E : ι → Type u_4} (x : WithCStarModule A ((i : ι) → E i)) (i : ι)
  [inst : (i : ι) → AddCommGroup (E i)], (-x) i = -x i
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
SimpleGraph.degMatrix_mulVec_apply : ∀ {V : Type u_1} {R : Type u_2} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj]
  [inst_2 : DecidableEq V] [inst_3 : NonAssocSemiring R] (v : V) (vec : V → R),
  (SimpleGraph.degMatrix R G).mulVec vec v = ↑(G.degree v) * vec v
-- Mathlib.Analysis.InnerProductSpace.NormDet
LinearMap.normDet_eq_zero_iff_rank_range_ne : ∀ {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U]
  [inst_2 : InnerProductSpace 𝕜 U] [inst_3 : FiniteDimensional 𝕜 U] [inst_4 : NormedAddCommGroup V]
  [inst_5 : InnerProductSpace 𝕜 V] {f : U →ₗ[𝕜] V}, f.normDet = 0 ↔ Module.finrank 𝕜 ↥f.range ≠ Module.finrank 𝕜 U
-- Mathlib.LinearAlgebra.Basis.Exact
LinearMap.linearProjOfIsCompl_comp_bijective_of_exact : ∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup K] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R K] [inst_6 : Module R P]
  {f : K →ₗ[R] M} {g : M →ₗ[R] P},
  Function.Exact ⇑f ⇑g →
    Function.Injective ⇑f →
      ∀ {q : Submodule R M} {E : Type u_8} [inst_7 : AddCommGroup E] [inst_8 : Module R E] {i : E →ₗ[R] M}
        (hi : Function.Injective ⇑i) (h : IsCompl i.range q),
        Disjoint g.ker q → Submodule.map g q = ⊤ → Function.Bijective ⇑(LinearMap.linearProjOfIsCompl q i hi h ∘ₗ f)
-- Lean.Elab.App
/-- Return the successful candidates. Recall we have Syntax `choice` nodes and overloaded symbols when we open multiple namespaces.  -/
_private.Lean.Elab.App.0.Lean.Elab.Term.getSuccesses : Array (Lean.Elab.Term.TermElabResult Lean.Expr) → Lean.Elab.TermElabM (Array (Lean.Elab.Term.TermElabResult Lean.Expr))
-- Mathlib.RingTheory.FilteredAlgebra.Basic
IsRingFiltration.toGradedMonoid : ∀ {ι : Type u_1} {R : Type u_2} {σ : Type u_3} {inst : AddMonoid ι} {inst_1 : PartialOrder ι} {inst_2 : Preorder σ}
  {inst_3 : Semiring R} {inst_4 : SetLike σ R} {F : ι → σ} {F_lt : outParam (ι → σ)} [self : IsRingFiltration F F_lt],
  SetLike.GradedMonoid F
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
/-- Any object at the top left of a pullback square is
isomorphic to the pullback provided by the `HasLimit` API.  -/
CategoryTheory.IsPullback.isoPullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P X Y Z : C} →
      {fst : P ⟶ X} →
        {snd : P ⟶ Y} →
          {f : X ⟶ Z} →
            {g : Y ⟶ Z} →
              CategoryTheory.IsPullback fst snd f g →
                [inst_1 : CategoryTheory.Limits.HasPullback f g] → P ≅ CategoryTheory.Limits.pullback f g
-- Mathlib.Algebra.Order.Star.Basic
star_lt_iff : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {x y : R}, star x < y ↔ x < star y
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.min?_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Min α] [inst_2 : LE α] [Std.LawfulOrderCmp cmp] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α]
  [Std.LawfulEqCmp cmp], t.keys.min? = t.minKey?
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.HasRightHomology.hasCokernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [S.HasRightHomology], CategoryTheory.Limits.HasCokernel S.f
-- Mathlib.Algebra.Category.ModuleCat.AB
instIsGrothendieckAbelianModuleCat : ∀ (R : Type u) [inst : Ring R], CategoryTheory.IsGrothendieckAbelian.{u, u, u + 1} (ModuleCat R)
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
/-- An alternative formulation of the sheaf condition
(which we prove equivalent to the usual one below as
`isSheaf_iff_isSheafPairwiseIntersections`).

A presheaf is a sheaf if `F` sends the cone `(Pairwise.cocone U).op` to a limit cone.
(Recall `Pairwise.cocone U` has cone point `iSup U`, mapping down to the `U i` and the `U i ⊓ U j`.)
 -/
TopCat.Presheaf.IsSheafPairwiseIntersections : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {X : TopCat} → TopCat.Presheaf C X → Prop
-- Mathlib.ModelTheory.Syntax
/-- A sentence indicating that a structure has `n` distinct elements.  -/
FirstOrder.Language.Sentence.cardGe : (L : FirstOrder.Language) → ℕ → L.Sentence
-- Mathlib.Topology.Baire.Lemmas
/-- A finite set is Baire.  -/
baire_of_finite : ∀ {X : Type u_1} [inst : TopologicalSpace X] [Finite X], BaireSpace X
-- Mathlib.Topology.Homotopy.Lifting
IsAddQuotientCoveringMap.monodromyPerm_injective : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E] (hp : IsAddQuotientCoveringMap p G) {x : X} [SimplyConnectedSpace E],
  Function.Injective ⇑(⋯.monodromyPerm x)
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.mem_infPrepartition_comm : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.TaggedPrepartition I},
  J ∈ π₁.infPrepartition π₂.toPrepartition ↔ J ∈ π₂.infPrepartition π₁.toPrepartition
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.mem_nonDegenerate_iff_strictMono : ∀ {n d : ℕ} (s : (SSet.stdSimplex.obj { len := n }).obj (Opposite.op { len := d })),
  s ∈ (SSet.stdSimplex.obj { len := n }).nonDegenerate d ↔ StrictMono ⇑s
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafReflectorSheafToPresheaf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] [inst_2 : CategoryTheory.HasSheafify J A],
  CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.reflector (CategoryTheory.sheafToPresheaf J A))
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.top_prod_top : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S], ⊤.prod ⊤ = ⊤
-- Mathlib.RingTheory.AdjoinRoot
/-- Promote `AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot` to an `AlgEquiv`.  -/
AdjoinRoot.quotEquivQuotMap : {R : Type u_1} →
  [inst : CommRing R] →
    (f : Polynomial R) →
      (I : Ideal R) →
        (AdjoinRoot f ⧸ Ideal.map (AdjoinRoot.of f) I) ≃ₐ[R]
          Polynomial (R ⧸ I) ⧸ Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f}
-- Init.Data.Vector.Basic
/-- Returns `true` with the monad if `p` returns `true` for all elements of the vector.  -/
Vector.allM : {m : Type → Type u_1} → {α : Type u_2} → {n : ℕ} → [Monad m] → (α → m Bool) → Vector α n → m Bool
-- Init.Data.ByteArray.Lemmas
ByteArray.getElem_set!_self : ∀ (data : ByteArray) (i : ℕ) (v : UInt8) (h : i < data.size), (data.set! i v)[i] = v
-- Mathlib.Order.Filter.Bases.Basic
/-- **Alias** of the reverse direction of `Filter.disjoint_principal_principal`. -/
Disjoint.filter_principal : ∀ {α : Type u_1} {s t : Set α}, Disjoint s t → Disjoint (Filter.principal s) (Filter.principal t)
-- Mathlib.Algebra.Group.Center
Set.neg_mem_addCenter : ∀ {M : Type u_1} [inst : SubtractionMonoid M] {a : M}, a ∈ Set.addCenter M → -a ∈ Set.addCenter M
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
AnalyticOnNhd.re_ofReal : ∀ {f : ℂ → ℂ} {s : Set ℝ}, AnalyticOnNhd ℂ f (Complex.ofReal '' s) → AnalyticOnNhd ℝ (fun x => (f ↑x).re) s
-- Mathlib.Data.Finset.NAry
Finset.le_inf'_image₂ : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α}
  {t : Finset β} [inst_1 : SemilatticeInf δ] {g : γ → δ} {a : δ} (h : (Finset.image₂ f s t).Nonempty),
  a ≤ (Finset.image₂ f s t).inf' h g ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.Const.ofArray : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {a : Array (α × β)},
  (Std.DHashMap.Raw.Const.ofArray a).WF
-- Mathlib.RingTheory.Ideal.Maps
Ideal.mem_map_of_mem : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  {I : Ideal R} {x : R}, x ∈ I → f x ∈ Ideal.map f I
-- Mathlib.Order.Heyting.Hom
HeytingHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β] {f g : HeytingHom α β},
  (∀ (a : α), f a = g a) → f = g
-- Mathlib.Topology.Algebra.Constructions
Units.continuous_embedProduct : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Monoid M], Continuous ⇑(Units.embedProduct M)
-- Init.Data.Array.Lemmas
Array.forall_mem_singleton : ∀ {α : Type u_1} {p : α → Prop} {a : α}, (∀ x ∈ #[a], p x) ↔ p a
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_unitIso_hom_app_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat))
  (ι : Type u_1) [inst_1 : Unique ι] {X S : C} (f : X ⟶ S) (X_1 : F.DescentDataAsCoalgebra fun x => f) (i : ι),
  ((CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence F ι f).unitIso.hom.app X_1).hom i =
    CategoryTheory.eqToHom ⋯
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.ShrinkHoms.equivalence_inverse : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C],
  (CategoryTheory.ShrinkHoms.equivalence C).inverse = CategoryTheory.ShrinkHoms.inverse C
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- The dimension theorem: if `v` and `v'` are two bases, their index types
have the same cardinalities.  -/
mk_eq_mk_of_basis : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type w}
  {ι' : Type w'} [InvariantBasisNumber R] (v : Module.Basis ι R M) (v' : Module.Basis ι' R M),
  Cardinal.lift.{w', w} (Cardinal.mk ι) = Cardinal.lift.{w, w'} (Cardinal.mk ι')
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.δ_leftShift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' m' : ℤ) (hn' : n + a = n')
  (m : ℤ) (hm' : m + a = m'),
  CochainComplex.HomComplex.δ n' m' (γ.leftShift a n' hn') =
    a.negOnePow • (CochainComplex.HomComplex.δ n m γ).leftShift a m' hm'
-- Init.Data.Int.Pow
Int.pow_zero : ∀ (m : ℤ), m ^ 0 = 1
-- Mathlib.Algebra.BigOperators.Associated
Associates.prod_le_prod : ∀ {M : Type u_2} [inst : CommMonoid M] {p q : Multiset (Associates M)}, p ≤ q → p.prod ≤ q.prod
-- Mathlib.RingTheory.WittVector.Defs
WittVector.sub_coeff : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (x y : WittVector p R) (n : ℕ),
  (x - y).coeff n = WittVector.peval (WittVector.wittSub p n) ![x.coeff, y.coeff]
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.toAddMonoidHom_eq_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M ≃+ N), f.toAddMonoidHom = ↑f
-- Mathlib.RingTheory.Idempotents
orthogonalIdempotents_iff : ∀ {R : Type u_1} [inst : Semiring R] {I : Type u_3} (e : I → R),
  OrthogonalIdempotents e ↔ (∀ (i : I), IsIdempotentElem (e i)) ∧ Pairwise fun x1 x2 => e x1 * e x2 = 0
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.instToJsonSuggestionStyle : Lean.ToJson Lean.Meta.Tactic.TryThis.SuggestionStyle
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.descFunLift.eq_3 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat)
  (s : CategoryTheory.Limits.Cocone F), CommRingCat.Colimits.descFunLift F s CommRingCat.Colimits.Prequotient.one = 1
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
EisensteinSeries.tsum_symmetricIco_tsum_eq_S_act : ∀ (z : UpperHalfPlane),
  ∑'[SummationFilter.symmetricIco ℤ] (n : ℤ), ∑' (m : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2 =
    (↑z ^ 2)⁻¹ * EisensteinSeries.G2 (ModularGroup.S • z)
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.adjMatrix_mulVec_const_apply : ∀ {α : Type u_1} {V : Type u_2} {G : SimpleGraph V} [inst : DecidableRel G.Adj] [inst_1 : Fintype V]
  [inst_2 : NonAssocSemiring α] {a : α} {v : V},
  (SimpleGraph.adjMatrix α G).mulVec (Function.const V a) v = ↑(G.degree v) * a
-- Init.Prelude
/-- Gets the word size of the current platform. The word size may be 64 or 32 bits.

This function is opaque because there is no guarantee at compile time that the target will have the
same word size as the host. It also helps avoid having type checking be architecture-dependent.

Lean only works on 64 and 32 bit systems. This fact is visible in the return type.
 -/
System.Platform.getNumBits : Unit → { n // n = 32 ∨ n = 64 }
-- Mathlib.CategoryTheory.Yoneda
/-- Coyoneda's lemma as a bijection `(uliftCoyoneda.{w}.obj X ⟶ F) ≃ F.obj (op X)`
for any presheaf of type `F : Cᵒᵖ ⥤ Type (max w v₁)` for some
auxiliary universe `w`.  -/
CategoryTheory.uliftCoyonedaEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : Cᵒᵖ} →
      {F : CategoryTheory.Functor C (Type (max w v₁))} →
        (CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ F) ≃ F.obj (Opposite.unop X)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instAdd : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → [inst_2 : Add β] → [ContinuousAdd β] → Add C(α, β)
-- Mathlib.Control.Random
Random.instBoundedRandomInt : {m : Type → Type u_1} → [Monad m] → BoundedRandom m ℤ
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.trans.eq_1 : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ f₂ : C(X, Y)}
  (F : f₀.Homotopy f₁) (G : f₁.Homotopy f₂),
  F.trans G =
    { toFun := fun x => if ↑x.1 ≤ 1 / 2 then (F.extend (2 * ↑x.1)) x.2 else (G.extend (2 * ↑x.1 - 1)) x.2,
      continuous_toFun := ⋯, map_zero_left := ⋯, map_one_left := ⋯ }
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderConjugate.eq_1 : ∀ (p q : ENNReal), p.HolderConjugate q = p.HolderTriple q 1
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
AbsolutelyContinuousOnInterval.tendsto_volume_restrict_totalLengthFilter_disjWithin_nhds_zero : ∀ (a b : ℝ),
  Filter.Tendsto
    (fun E => (MeasureTheory.volume.restrict (Set.uIoc a b)) (⋃ i ∈ Finset.range E.1, Set.uIoc (E.2 i).1 (E.2 i).2))
    (AbsolutelyContinuousOnInterval.totalLengthFilter ⊓
      Filter.principal (AbsolutelyContinuousOnInterval.disjWithin a b))
    (nhds 0)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_neg : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : InvolutiveNeg α] (s : Finset α), ↑(-s) = -↑s
-- Mathlib.Algebra.Polynomial.GroupRingAction
Polynomial.smul_eval_smul : ∀ {M : Type u_1} [inst : Monoid M] (S : Type u_3) [inst_1 : CommSemiring S] [inst_2 : MulSemiringAction M S] (m : M)
  (f : Polynomial S) (x : S), Polynomial.eval (m • x) (m • f) = m • Polynomial.eval x f
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.mapMUnsafe.map : {α : Type u} →
  {β : Type v} → {m : Type v → Type w} → [Monad m] → (α → m β) → USize → USize → Array NonScalar → m (Array PNonScalar)
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.Functor.rightUnitor_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C), F.rightUnitor.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Init.Core
Inter.mk : {α : Type u} → (α → α → α) → Inter α
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Finset.hasProd_iff_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : CommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalGroup α] {f : β → α}
  {a : α} (s : Finset β), HasProd f a ↔ HasProd (fun x => f ↑x) (a / ∏ i ∈ s, f i)
-- Mathlib.Tactic.Simproc.ExistsAndEq
/-- Type for storing the chosen branch at `And` nodes.  -/
ExistsAndEq.GoTo : Type
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.LoogleResult.success.inj : ∀ {a a_1 : Array LeanSearchClient.SearchResult},
  LeanSearchClient.LoogleResult.success a = LeanSearchClient.LoogleResult.success a_1 → a = a_1
-- Mathlib.LinearAlgebra.FreeModule.ModN
ModN.instModuleZMod : {G : Type u_1} → [inst : AddCommGroup G] → {n : ℕ} → Module (ZMod n) (ModN G n)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_le_size_insertMany!_list : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {l : List ((a : α) × β a)}, t.size ≤ (↑(t.insertMany! l)).size
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.absNorm_algebraMap : ∀ (R : Type u_1) [inst : CommRing R] [IsDomain R] (S : Type u_3) [inst_2 : CommRing S] [IsDomain S]
  [IsIntegrallyClosed R] [IsIntegrallyClosed S] [inst_6 : Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S]
  [inst_9 : IsDedekindDomain R] [inst_10 : IsDedekindDomain S] [inst_11 : Module.Free ℤ R] [inst_12 : Module.Free ℤ S]
  [Module.Finite ℤ S] (I : Ideal R) [Module.Finite ℤ R],
  Ideal.absNorm (Ideal.map (algebraMap R S) I) = Ideal.absNorm I ^ Module.finrank R S
-- Init.Data.Array.Lemmas
Array.pop_append : ∀ {α : Type u_1} {xs ys : Array α}, (xs ++ ys).pop = if ys.isEmpty = true then xs.pop else xs ++ ys.pop