mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
/-- Fold a bilinear map along the generators of a term of the clifford algebra, with the rule
given by `foldl Q f hf n (ι Q m * x) = f m (foldl Q f hf n x)`.

For example, `foldl f hf n (r • ι R u + ι R v * ι R w) = r • f u n + f v (f w n)`.  -/
CliffordAlgebra.foldl : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : AddCommGroup N] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] →
                (Q : QuadraticForm R M) →
                  (f : M →ₗ[R] N →ₗ[R] N) →
                    (∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x) → N →ₗ[R] CliffordAlgebra Q →ₗ[R] N
-- Mathlib.Topology.Sheaves.Stalks
/-- Stalks are functorial with respect to morphisms of presheaves over a fixed `X`.  -/
TopCat.Presheaf.stalkFunctor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasColimits C] → {X : TopCat} → ↑X → CategoryTheory.Functor (TopCat.Presheaf C X) C
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblZ_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R) (u : R),
  W'.dblZ (u • P) = u ^ 4 * W'.dblZ P
-- Mathlib.RingTheory.TensorProduct.Maps
Subalgebra.tmul_mem_baseChange : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : CommSemiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {C : Subalgebra R A} {x : A},
  x ∈ C → ∀ (b : B), b ⊗ₜ[R] x ∈ Subalgebra.baseChange B C
-- Init.NotationExtra
unexpandEqRec : Lean.PrettyPrinter.Unexpander
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.fixedPoints_ne_univ_of_faithfulSMul : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [inst_2 : DecidableEq α] [Nontrivial G]
  [FaithfulSMul G α] {n : ℕ}, 0 < n → n < Nat.card α → MulAction.fixedPoints G ↑(Set.powersetCard α n) ≠ Set.univ
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatchAt.le : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {startPos endPos : s.Pos}, String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos endPos → startPos ≤ endPos
-- Mathlib.Algebra.Category.CommAlgCat.Monoidal
CommAlgCat.binaryCofan_inl : ∀ {R : Type u} [inst : CommRing R] (A B : CommAlgCat R),
  (A.binaryCofan B).inl = CommAlgCat.ofHom Algebra.TensorProduct.includeLeft
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- Taking sub-families preserves uniform equicontinuity.  -/
UniformEquicontinuous.comp : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β]
  {F : ι → β → α}, UniformEquicontinuous F → ∀ (u : κ → ι), UniformEquicontinuous (F ∘ u)
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
thickenedIndicator_le_one : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) (x : α),
  (thickenedIndicator δ_pos E) x ≤ 1
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- Eta-expanded form of `meromorphicNFAt_comp_add_const_iff_meromorphicNFAt`

---

`MeromorphicNFAt` is invariant under translation.  -/
meromorphicNFAt_fun_comp_add_const_iff_meromorphicNFAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x c : 𝕜} {f : 𝕜 → E}, MeromorphicNFAt (fun x => f (x + c)) x ↔ MeromorphicNFAt f (x + c)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.notMem_of_notMem_closure : ∀ {R : Type u} [inst : NonAssocSemiring R] {s : Set R} {P : R}, P ∉ Subsemiring.closure s → P ∉ s
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- If a Hahn series $f$ is in the range, then any truncation of $f$ is also in the range.  -/
HahnEmbedding.IsPartial.truncLT_mem_range : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R}
  {f : M →ₗ.[K] Lex (HahnSeries (FiniteArchimedeanClass M) R)},
  HahnEmbedding.IsPartial seed f →
    ∀ (x : ↥f.domain) (c : FiniteArchimedeanClass M),
      toLex ((HahnSeries.truncLTLinearMap K c) (ofLex (↑f x))) ∈ f.toFun.range
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- **Alias** of `MonoidAlgebra.mapRingEquiv`.

---

Isomorphic rings have isomorphic monoid algebras.  -/
MonoidAlgebra.mapRangeRingEquiv : {R : Type u_3} →
  {S : Type u_4} →
    (M : Type u_6) →
      [inst : Semiring R] →
        [inst_1 : Semiring S] → [inst_2 : Monoid M] → R ≃+* S → MonoidAlgebra R M ≃+* MonoidAlgebra S M
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.core.inj : ∀ {e e_1 : Lean.Expr},
  Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.core e = Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.core e_1 → e = e_1
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.infty_coeFn_natCast : ∀ {I : Type u_5} {B : I → Type u_6} [inst : (i : I) → NormedRing (B i)] [inst_1 : ∀ (i : I), NormOneClass (B i)]
  (n : ℕ), ↑↑n = ↑n
-- Mathlib.Data.Matrix.Basis
Matrix.single_mul_apply_same : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq l] [inst_1 : DecidableEq m]
  [inst_2 : Fintype m] [inst_3 : NonUnitalNonAssocSemiring α] (c : α) (i : l) (j : m) (b : n) (M : Matrix m n α),
  (Matrix.single i j c * M) i b = c * M j b
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- The universal property of left Kan extensions characterizes the functor
corepresented by `F ⊛ G`.  -/
CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            (F G : CategoryTheory.Functor C V) →
              [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G] →
                (((CategoryTheory.Functor.whiskeringLeft (C × C) C V).obj
                          (CategoryTheory.MonoidalCategory.tensor C)).comp
                      (CategoryTheory.coyoneda.obj
                        (Opposite.op (CategoryTheory.MonoidalCategory.externalProduct F G)))).CorepresentableBy
                  (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G)
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.tendsto_atTop_of_leadingCoeff_nonneg : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜)
  [OrderTopology 𝕜],
  0 < P.degree → 0 ≤ P.leadingCoeff → Filter.Tendsto (fun x => Polynomial.eval x P) Filter.atTop Filter.atTop
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
CategoryTheory.Adjunction.ofCat_toCat : ∀ {C D : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v, u} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G),
  CategoryTheory.Adjunction.ofCat adj.toCat = adj
-- Init.Data.Option.Lemmas
Option.isSome_max : ∀ {α : Type u_1} [inst : Max α] {o o' : Option α}, (o ⊔ o').isSome = (o.isSome || o'.isSome)
-- Init.Data.Array.Lemmas
Array.exists_mem_push : ∀ {α : Type u_1} {p : α → Prop} {a : α} {xs : Array α},
  (∃ x, ∃ (_ : x ∈ xs.push a), p x) ↔ p a ∨ ∃ x, ∃ (_ : x ∈ xs), p x
-- Mathlib.Algebra.Algebra.NonUnitalHom
/-- The prod of two morphisms is a morphism.  -/
NonUnitalAlgHom.prod : {R : Type u} →
  [inst : Monoid R] →
    {A : Type v} →
      {B : Type w} →
        {C : Type w₁} →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : DistribMulAction R A] →
              [inst_3 : NonUnitalNonAssocSemiring B] →
                [inst_4 : NonUnitalNonAssocSemiring C] →
                  [inst_5 : DistribMulAction R B] →
                    [inst_6 : DistribMulAction R C] → (A →ₙₐ[R] B) → (A →ₙₐ[R] C) → A →ₙₐ[R] B × C
-- Lean.Elab.InfoTree.Types
Lean.Elab.CommandContextInfo.ngen : Lean.Elab.CommandContextInfo → Lean.NameGenerator
-- Mathlib.RingTheory.Regular.RegularSequence
Ideal.ofList_cons_smul : ∀ {R : Type u_7} [inst : CommSemiring R] (r : R) (rs : List R) {M : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (N : Submodule R M), Ideal.ofList (r :: rs) • N = r • N ⊔ Ideal.ofList rs • N
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.factor_dvd_of_natDegree_ne_zero : ∀ {K : Type v} [inst : Field K] {f : Polynomial K}, f.natDegree ≠ 0 → f.factor ∣ f
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  (S : J.MayerVietorisSquare),
  S.shortComplex.X₃ =
    (CategoryTheory.presheafToSheaf J AddCommGrpCat).obj ((CategoryTheory.yoneda.obj S.X₄).comp AddCommGrpCat.free)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.instSMul : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          {𝒜 : ι → σ} →
            (x : Submonoid A) →
              {α : Type u_4} →
                [inst_2 : SMul α A] →
                  [IsScalarTower α A A] → [SMulMemClass σ α A] → SMul α (HomogeneousLocalization 𝒜 x)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- Slight reformulation of `MeasureTheory.AECover.integral_tendsto_of_countably_generated`.  -/
MeasureTheory.AECover.integral_eq_of_tendsto : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [l.NeBot] [l.IsCountablyGenerated] {φ : ι → Set α},
  MeasureTheory.AECover μ l φ →
    ∀ {f : α → E} (I : E),
      MeasureTheory.Integrable f μ →
        Filter.Tendsto (fun n => ∫ (x : α) in φ n, f x ∂μ) l (nhds I) → ∫ (x : α), f x ∂μ = I
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.card_opow_eq_of_omega0_le_right : ∀ {a b : Ordinal.{u_1}}, 1 < a → Ordinal.omega0 ≤ b → (a ^ b).card = max a.card b.card
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- Formal operation of negation on special linear group on even cardinality `n` given by negating
each element.  -/
Matrix.SpecialLinearGroup.instNeg : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {R : Type v} → [inst_2 : CommRing R] → [Fact (Even (Fintype.card n))] → Neg (Matrix.SpecialLinearGroup n R)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.coprod.inl_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.fst X Y) h) =
    h
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.toTrivial_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.Bimon C),
  A.toTrivial.hom = CategoryTheory.ComonObj.counit
-- Mathlib.Algebra.Order.SuccPred
Order.sub_one_wcovBy : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Sub α] [inst_2 : One α] [PredSubOrder α] (x : α), x - 1 ⩿ x
-- Mathlib.Topology.Algebra.Group.Torsor
Homeomorph.constVSub_apply : ∀ {V : Type u_1} {P : Type u_2} [inst : AddGroup V] [inst_1 : TopologicalSpace V] [inst_2 : AddTorsor V P]
  [inst_3 : TopologicalSpace P] [inst_4 : IsTopologicalAddTorsor P] (p x : P), (Homeomorph.constVSub p) x = p -ᵥ x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_filterMap : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  [inst : Std.TransOrd α] [inst_1 : Std.LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k fallback : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl.getKeyD k fallback =
    ((t.getKey? k).pfilter fun x h' => (f x (t.get x ⋯)).isSome).getD fallback
-- Mathlib.RingTheory.IsTensorProduct
Algebra.IsPushout.cancelBaseChange_symm_tmul : ∀ (R : Type u_1) (S : Type v₃) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (A : Type u_8)
  (B : Type u_9) [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [inst_11 : Algebra.IsPushout R S A B] (M : Type u_10) [inst_12 : AddCommGroup M] [inst_13 : Module R M]
  [inst_14 : Module A M] [inst_15 : IsScalarTower R A M] (s : S) (m : M),
  (Algebra.IsPushout.cancelBaseChange R S A B M).symm (s ⊗ₜ[R] m) = (algebraMap S B) s ⊗ₜ[A] m
-- Mathlib.RingTheory.Kaehler.TensorProduct
KaehlerDifferential.tensorKaehlerEquiv_left_inv : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [inst_11 : Algebra.IsPushout R S A B],
  ↑S (KaehlerDifferential.derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ
      LinearMap.liftBaseChange S (↑R (KaehlerDifferential.map R S A B)) =
    LinearMap.id
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens),
  (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj ((TopologicalSpace.Opens.map f.base).obj U) =
    AlgebraicGeometry.Scheme.Hom.opensRange f ⊓ U
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.AEStronglyMeasurable.comp_snd_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {X : Type u_4} [inst_2 : TopologicalSpace X] [MeasureTheory.SFinite ν] {f : β → X},
  μ ≠ 0 → (MeasureTheory.AEStronglyMeasurable (fun x => f x.2) (μ.prod ν) ↔ MeasureTheory.AEStronglyMeasurable f ν)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.ProofMode.start_entails : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs} {φ : Prop} [Std.Do.SPred.Tactic.PropAsSPredTautology φ P], (⊢ₛ P) → φ
-- Mathlib.Data.Setoid.Partition
IndexedPartition.proj_fiber : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (x : hs.Quotient),
  hs.proj ⁻¹' {x} = s (hs.equivQuotient.symm x)
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
/-- The tensor product of `ι →₀ R` and `N` is linearly equivalent to `ι →₀ N`  -/
TensorProduct.finsuppScalarLeft : (R : Type u_1) →
  [inst : CommSemiring R] →
    (N : Type u_4) →
      [inst_1 : AddCommMonoid N] →
        [inst_2 : Module R N] → (ι : Type u_5) → [DecidableEq ι] → TensorProduct R (ι →₀ R) N ≃ₗ[R] ι →₀ N
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.point_logSizeBallSeq_zero : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T]
  (hJ : J.Nonempty), (PairReduction.logSizeBallSeq J hJ a c 0).point = Exists.choose hJ
-- Lean.Meta.MethodSpecs
_private.Lean.Meta.MethodSpecs.0.Lean.MethodSpecTheorem.mk : Lean.Name → List Lean.Name → Lean.Expr → Lean.MethodSpecTheorem✝
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxi.Iterator.instIteratorLoop.loop.wf.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  {n : Type u → Type w} [inst_2 : Monad n] (γ : Type u) (Pl : α → γ → ForInStep γ → Prop)
  (wf : Std.IteratorLoop.WellFounded (Std.Rxi.Iterator α) Id Pl) (LargeEnough : α → Prop)
  (hl : ∀ (a b : α), Std.PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b) (acc : γ) (next : α)
  (h : LargeEnough next) (f : (out : α) → LargeEnough out → (c : γ) → n { s // Pl out c s }),
  Std.Rxi.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl acc next h f = do
    let __do_lift ← f next h acc
    match __do_lift with
      | ⟨ForInStep.yield acc', property⟩ =>
        match hs : Std.PRange.succ? next with
        | some next' => Std.Rxi.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl acc' next' ⋯ f
        | none => pure acc'
      | ⟨ForInStep.done acc', property⟩ => pure acc'
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.tendsto_cocompact : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [ProperSpace E] (f : SchwartzMap E F), Filter.Tendsto (⇑f) (Filter.cocompact E) (nhds 0)
-- Mathlib.Algebra.Ring.NegOnePow
Int.abs_negOnePow : ∀ (n : ℤ), |↑n.negOnePow| = 1
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.mk.eq_1 : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] {v : ι → E} (hon : Orthonormal 𝕜 v)
  (hsp : ⊤ ≤ Submodule.span 𝕜 (Set.range v)), OrthonormalBasis.mk hon hsp = (Module.Basis.mk ⋯ hsp).toOrthonormalBasis ⋯
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintKind.parameter : Lean.Elab.InlayHintKind
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
/-- The fundamental cone is a cone in the mixed space, i.e. a subset fixed by multiplication by
a nonzero real number, see `smul_mem_of_mem`, that is also a fundamental domain for the action
of `(𝓞 K)ˣ` modulo torsion, see `exists_unit_smul_mem` and `torsion_smul_mem_of_mem`.  -/
NumberField.mixedEmbedding.fundamentalCone : (K : Type u_1) → [inst : Field K] → [NumberField K] → Set (NumberField.mixedEmbedding.mixedSpace K)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the angle between two vectors is `-π / 2`, the vectors are not equal.  -/
Orientation.ne_of_oangle_eq_neg_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(-Real.pi / 2) → x ≠ y
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
/-- Given a map `f : M ⟶ N` between sheaves of modules over `R`, this is the restriction
to the map `M.over X ⟶ N.over X` between sheaves of modules over `R.over X`.  -/
SheafOfModules.Hom.over : {D : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} D] →
    {K : CategoryTheory.GrothendieckTopology D} →
      {R : CategoryTheory.Sheaf K RingCat} → {M N : SheafOfModules R} → (M ⟶ N) → (X : D) → M.over X ⟶ N.over X
-- Mathlib.Analysis.Convex.Function
ConcaveOn.comp_strictConvexOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid α] [inst_4 : PartialOrder α] [inst_5 : AddCommMonoid β]
  [inst_6 : PartialOrder β] [inst_7 : SMul 𝕜 E] [inst_8 : SMul 𝕜 α] [inst_9 : SMul 𝕜 β] {s : Set E} {f : E → β}
  {g : β → α}, ConcaveOn 𝕜 (f '' s) g → StrictConvexOn 𝕜 s f → StrictAntiOn g (f '' s) → StrictConcaveOn 𝕜 s (g ∘ f)
-- Mathlib.Algebra.Order.Group.Synonym
ofColex_mul : ∀ {α : Type u_1} [inst : Mul α] (a b : Colex α), ofColex (a * b) = ofColex a * ofColex b
-- Lean.Meta.Match.MatchPatternAttr
Lean.hasMatchPatternAttribute : Lean.Environment → Lean.Name → Bool
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.stabilizer_vadd_eq_right : ∀ {G : Type u_1} {β : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G β] {α : Type u_4} [inst_2 : AddGroup α]
  [inst_3 : AddAction α β] [VAddCommClass G α β] (a : α) (b : β),
  AddAction.stabilizer G (a +ᵥ b) = AddAction.stabilizer G b
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
TopCat.Presheaf.restrictOpen.congr_simp : ∀ {X : TopCat} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  {F : TopCat.Presheaf C X} {V : TopologicalSpace.Opens ↑X} (x x_1 : CategoryTheory.ToType (F.obj (Opposite.op V))),
  x = x_1 →
    ∀ (U : TopologicalSpace.Opens ↑X) (e : U ≤ V),
      TopCat.Presheaf.restrictOpen x U e = TopCat.Presheaf.restrictOpen x_1 U e
-- Mathlib.Analysis.Calculus.FDeriv.Const
fderiv_natCast : ∀ {𝕜 : 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 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : NatCast F] (n : ℕ), fderiv 𝕜 ↑n = 0
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.minDegree_bot_eq_zero : ∀ {V : Type u_1} [inst : Fintype V], ⊥.minDegree = 0
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_filter_gt_of_eq : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α → Ordering} [Std.Internal.IsStrictCut compare k]
  {sz : ℕ} {k' : α} {v' : β k'} {l r : Std.DTreeMap.Internal.Impl α β},
  k k' = Ordering.eq →
    (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).Ordered →
      List.filter (fun x => k x.fst == Ordering.gt) (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).toListModel =
        l.toListModel
-- Mathlib.Data.ENat.Basic
ENat.map_add : ∀ {β : Type u_2} {F : Type u_3} [inst : Add β] [inst_1 : FunLike F ℕ β] [AddHomClass F ℕ β] (f : F) (a b : ℕ∞),
  ENat.map (⇑f) (a + b) = ENat.map (⇑f) a + ENat.map (⇑f) b
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isSome_maxKey?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, (t.insert k v).maxKey?.isSome = true
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.mkD_eq_self : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : C(α, β)},
  ContinuousMap.mkD (⇑f) g = f
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.le_extensionProductIter : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] (n : ℕ), P ≤ P.extensionProductIter n
-- Init.Data.Order.Ord
Std.TransCmp.gt_of_gt_of_eq : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a b c : α},
  cmp a b = Ordering.gt → cmp b c = Ordering.eq → cmp a c = Ordering.gt
-- Std.Data.ExtDTreeMap.Basic
/-- Implementation detail of the tree map  -/
Std.ExtDTreeMap.inner : {α : Type u} →
  {β : α → Type v} →
    {cmp : autoParam (α → α → Ordering) Std.ExtDTreeMap._auto_1} →
      Std.ExtDTreeMap α β cmp → Quotient (Std.DTreeMap.isSetoid α β cmp)
-- Mathlib.Data.Fintype.Basic
PSigma.fintypePropLeft : {α : Prop} → {β : α → Type u_4} → [Decidable α] → [(a : α) → Fintype (β a)] → Fintype ((a : α) ×' β a)
-- Mathlib.RingTheory.Extension.Basic
/-- The identity map `P.ker.Cotangent → P.Cotangent` into the type synonym.  -/
Algebra.Extension.Cotangent.of : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → {P : Algebra.Extension R S} → P.ker.Cotangent → P.Cotangent
-- Mathlib.CategoryTheory.Limits.Types.Colimits
/-- The category of types has all colimits.  -/
CategoryTheory.Limits.Types.hasColimitsOfSize : ∀ [UnivLE.{v, u}], CategoryTheory.Limits.HasColimitsOfSize.{w, v, u, u + 1} (Type u)