mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- `G.degree v` is the number of vertices adjacent to `v`.  -/
SimpleGraph.degree : {V : Type u_1} → (G : SimpleGraph V) → (v : V) → [Fintype ↑(G.neighborSet v)] → ℕ
-- Lean.Server.FileWorker.InlayHints
Lean.Server.FileWorker.InlayHintState.init : Lean.Server.FileWorker.InlayHintState
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
/-- The projection `enrichedHom V F₁ F₂ ⟶ F₁.obj j ⟶[V] F₂.obj j` in the category `V`
for any `j : J` when `F₁` and `F₂` are functors `J ⥤ C` and `C` is a `V`-enriched category.  -/
CategoryTheory.Enriched.FunctorCategory.enrichedHomπ : (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₂] →
                    (j : J) → CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂ ⟶ F₁.obj j ⟶[V] F₂.obj j
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.del : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.FVarId →
    Lean.Compiler.LCNF.Code pu →
      autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_19 → Lean.Compiler.LCNF.Code pu
-- Mathlib.Algebra.MvPolynomial.Coeff
/-- The formula for the `d`th coefficient of `(X 0 + X 1) ^ n`.  -/
MvPolynomial.coeff_add_pow : ∀ {R : Type u_1} [inst : CommSemiring R] (d : Fin 2 →₀ ℕ) (n : ℕ),
  MvPolynomial.coeff d ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ n) =
    ↑(if (d 0, d 1) ∈ Finset.HasAntidiagonal.antidiagonal n then n.choose (d 0) else 0)
-- Mathlib.Data.Matrix.Mul
Matrix.smul_eq_mul_diagonal : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : CommSemiring α] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (M : Matrix m n α) (a : α), a • M = M * Matrix.diagonal fun x => a
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.image_mono : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] {U V : X.Opens},
  U ≤ V → (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U ≤ (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj V
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
LineDifferentiableAt.hasLineDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {x v : E},
  LineDifferentiableAt 𝕜 f x v → HasLineDerivAt 𝕜 f (lineDeriv 𝕜 f x v) x v
-- Mathlib.LinearAlgebra.Vandermonde
/-- The formula for the determinant of a projective Vandermonde matrix.  -/
Matrix.det_projVandermonde : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (v w : Fin n → R),
  (Matrix.projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_continuous : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω],
  Continuous fun μ => μ.toWeakDualBCNN
-- Mathlib.Data.List.Permutation
Fin.mk.hinj : ∀ {n val : ℕ} {isLt : val < n} {n_1 val_1 : ℕ} {isLt_1 : val_1 < n_1},
  n = n_1 → ⟨val, isLt⟩ ≍ ⟨val_1, isLt_1⟩ → n = n_1 ∧ val = val_1
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.sum_comp'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R S : C}
  {J : Type u_1} (s : Finset J) (f : J → (P ⟶ Q)) (g : J → (Q ⟶ R)) (h : R ⟶ S) {Z : C} (h_1 : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp (∑ j ∈ s, CategoryTheory.CategoryStruct.comp (f j) (g j))
      (CategoryTheory.CategoryStruct.comp h h_1) =
    CategoryTheory.CategoryStruct.comp
      (∑ j ∈ s, CategoryTheory.CategoryStruct.comp (f j) (CategoryTheory.CategoryStruct.comp (g j) h)) h_1
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.distribMulAction : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} →
      [inst : Monoid S] → [inst_1 : Semiring R] → [DistribMulAction S R] → DistribMulAction S (AddMonoidAlgebra R M)
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- If `L/K` is finite and normal, then `spectralNorm K L = invariantExtension K L`.  -/
spectralNorm_eq_invariantExtension : ∀ (K : Type u_2) [inst : NormedField K] (L : Type u_3) [inst_1 : Field L] [inst_2 : Algebra K L]
  [h_fin : FiniteDimensional K L] [hn : Normal K L] [hu : IsUltrametricDist K],
  spectralNorm K L = ⇑(IsUltrametricDist.invariantExtension K L)
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.copy_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {s : (X : C) → Set (CategoryTheory.Sieve X)} {h : J.sieves = s}, J.copy s h = J
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.nextCoeff_mul_C : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {a : R} [NoZeroDivisors R],
  (p * Polynomial.C a).nextCoeff = p.nextCoeff * a
-- Lean.Elab.DeclModifiers
/-- Whether a declaration is default, partial or nonrec.  -/
Lean.Elab.RecKind : Type
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  (↑m).WF →
    ∀ {l : List α} {k k' : α},
      (k == k') = true →
        m.contains k = false →
          List.Pairwise (fun a b => (a == b) = false) l →
            k ∈ l → (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).getKey! k' = k
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.ι₀_desc_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F K : HomologicalComplex C c} [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder]
  (φ₀ φ₁ : K ⟶ F) (h : Homotopy φ₀ φ₁) {Z : HomologicalComplex C c} (h_1 : F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.ι₀ K)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.desc φ₀ φ₁ h) h_1) =
    CategoryTheory.CategoryStruct.comp φ₀ h_1
-- Mathlib.Order.LiminfLimsup
Filter.limsSup_principal_eq_csSup : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α},
  BddAbove s → s.Nonempty → (Filter.principal s).limsSup = sSup s
-- Init.Data.String.Defs
String.Pos.le_refl : ∀ {s : String} (p : s.Pos), p ≤ p
-- Init.Data.UInt.Lemmas
UInt8.mod_one : ∀ {a : UInt8}, a % 1 = 0
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardDistinctFactors_pos : ∀ {n : ℕ}, 0 < ArithmeticFunction.cardDistinctFactors n ↔ 1 < n
-- Mathlib.Data.Ineq
Mathlib.Ineq.lt : Mathlib.Ineq
-- Mathlib.Order.Height
Set.encard_le_chainHeight_of_isChain : ∀ {α : Type u_1} {r : α → α → Prop} (s t : Set α), t ⊆ s → IsChain r t → t.encard ≤ s.chainHeight r
-- Lean.Meta.RecursorInfo
Lean.Meta.getMajorPos? : Lean.Environment → Lean.Name → Option ℕ
-- Mathlib.Data.Set.Lattice
Set.sUnion_subset : ∀ {α : Type u_1} {S : Set (Set α)} {t : Set α}, (∀ t' ∈ S, t' ⊆ t) → ⋃₀ S ⊆ t
-- Init.Data.UInt.Lemmas
UInt16.toUInt32_inj : ∀ {a b : UInt16}, a.toUInt32 = b.toUInt32 ↔ a = b
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.sigmaIsoSigma_inv_apply : ∀ {ι : Type v} (α : ι → TopCat) (i : ι) (x : ↑(α i)),
  (CategoryTheory.ConcreteCategory.hom (TopCat.sigmaIsoSigma α).inv) ⟨i, x⟩ =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Sigma.ι α i)) x
-- Mathlib.Topology.Order.Filter
Filter.Tendsto.nhds_atTop : ∀ {α : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : PartialOrder X] [OrderTopology X] [NoMaxOrder X]
  {f : α → X} {l : Filter α}, Filter.Tendsto f l Filter.atTop → Filter.Tendsto (nhds ∘ f) l (nhds Filter.atTop)
-- Init.Data.Vector.Lex
Vector.instTotalLeOfAsymmLt : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] [Std.Asymm fun x1 x2 => x1 < x2], Std.Total fun x1 x2 => x1 ≤ x2
-- Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
/-- Universally open satisfies fpqc descent.  -/
AlgebraicGeometry.descendsAlong_universallyOpen_surjective_inf_flat_inf_quasicompact : CategoryTheory.MorphismProperty.DescendsAlong (@AlgebraicGeometry.UniversallyOpen)
  (@AlgebraicGeometry.Surjective ⊓ @AlgebraicGeometry.Flat ⊓ @AlgebraicGeometry.QuasiCompact)
-- Mathlib.Data.Set.Pairwise.Chain
IsChain.pairwise_sUnion : ∀ {α : Type u_1} {c : Set (Set α)} {r : α → α → Prop},
  IsChain (fun x1 x2 => x1 ⊆ x2) c → ((⋃₀ c).Pairwise r ↔ ∀ s ∈ c, s.Pairwise r)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.injective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Embedding M N), Function.Injective ⇑f
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
MvPolynomial.universalFactorizationMap_freeMonic : ∀ (R : Type u_1) [inst : CommRing R] (n m k : ℕ) (hn : n = m + k),
  Polynomial.map (↑(MvPolynomial.universalFactorizationMap R n m k hn)) (Polynomial.freeMonic R n) =
    Polynomial.map
        (algebraMap (MvPolynomial (Fin m) R) (TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R)))
        (Polynomial.freeMonic R m) *
      Polynomial.map (↑Algebra.TensorProduct.includeRight) (Polynomial.freeMonic R k)
-- Mathlib.Data.Nat.Cast.Field
Nat.cast_div_charZero : ∀ {K : Type u_1} [inst : DivisionSemiring K] {m n : ℕ} [CharZero K], n ∣ m → ↑(m / n) = ↑m / ↑n
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
/-- The domain of evaluation of `MvPowerSeries`, as an ideal  -/
MvPowerSeries.hasEvalIdeal : {σ : Type u_1} →
  {S : Type u_3} →
    [inst : CommRing S] → [inst_1 : TopologicalSpace S] → [IsTopologicalRing S] → [IsLinearTopology S S] → Ideal (σ → S)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.WalkingPair.ofNat : ℕ → CategoryTheory.Limits.WalkingPair
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {c : ℕ},
  Std.DHashMap.Internal.Raw.WFImp ↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity c)
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.Graph.in₂₀_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {c : γ},
  (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₂ c) (Sum3.in₀ a) ↔ ∃ b, (a, b, c) ∈ t
-- Mathlib.Data.EReal.Operations
EReal.add_lt_add : ∀ {x y z t : EReal}, x < y → z < t → x + z < y + t
-- Mathlib.Algebra.Homology.QuasiIso
HomotopyEquiv.quasiIsoAt_hom : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} {K L : HomologicalComplex C c} (e : HomotopyEquiv K L) (n : ι) [inst_2 : K.HasHomology n]
  [inst_3 : L.HasHomology n], QuasiIsoAt e.hom n
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.toEquiv_inj : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  {e₁ e₂ : A ≃ₐc[R] B}, e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
IsLocalDiffeomorph.preimage_interior : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H' N] {n : WithTop ℕ∞},
  n ≠ 0 → ∀ {f : M → N}, IsLocalDiffeomorph I I' n f → f ⁻¹' ModelWithCorners.interior N = ModelWithCorners.interior M
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernel.desc.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f] {W : C} (k k_1 : Y ⟶ W) (e_k : k = k_1)
  (h : CategoryTheory.CategoryStruct.comp f k = 0),
  CategoryTheory.Limits.cokernel.desc f k h = CategoryTheory.Limits.cokernel.desc f k_1 ⋯
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.setIntegral_dirac' : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [hE : CompleteSpace E]
  {mα : MeasurableSpace α} {f : α → E},
  MeasureTheory.StronglyMeasurable f →
    ∀ (a : α) {s : Set α},
      MeasurableSet s →
        ∀ [inst_2 : Decidable (a ∈ s)], ∫ (x : α) in s, f x ∂MeasureTheory.Measure.dirac a = if a ∈ s then f a else 0
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive],
  CategoryTheory.NatTrans.rightDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.id F) =
    CategoryTheory.CategoryStruct.id F.rightDerivedToHomotopyCategory
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_set_pi_of_surjective : ∀ {M : Type u_5} {ι : Type u_6} {π : ι → Type u_7} [inst : (i : ι) → SMul M (π i)] (c : M) (I : Set ι)
  (s : (i : ι) → Set (π i)), (∀ i ∉ I, Function.Surjective fun x => c • x) → c • I.pi s = I.pi (c • s)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
ContinuousLinearMap.coeFn_compLp : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {𝕜 : Type u_6} {𝕜' : Type u_7}
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' F] {σ : 𝕜 →+* 𝕜'} [inst_6 : RingHomIsometric σ] (L : E →SL[σ] F)
  (f : ↥(MeasureTheory.Lp E p μ)), ∀ᵐ (a : α) ∂μ, ↑↑(L.compLp f) a = L (↑↑f a)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
/-- Lebesgue dominated convergence theorem for series.  -/
MeasureTheory.VectorMeasure.hasSum_integral_of_dominated_convergence : ∀ {ι : Type u_1} {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] {μ : MeasureTheory.VectorMeasure X F}
  {B : E →L[ℝ] F →L[ℝ] G} [Countable ι] {F_1 : ι → X → E} {f : X → E} (bound : ι → X → ℝ),
  (∀ (n : ι), MeasureTheory.AEStronglyMeasurable (F_1 n) μ.variation) →
    (∀ (n : ι), ∀ᵐ (a : X) ∂μ.variation, ‖F_1 n a‖ ≤ bound n a) →
      (∀ᵐ (a : X) ∂μ.variation, Summable fun n => bound n a) →
        MeasureTheory.Integrable (fun a => ∑' (n : ι), bound n a) μ.variation →
          (∀ᵐ (a : X) ∂μ.variation, HasSum (fun n => F_1 n a) (f a)) →
            HasSum (fun n => ∫ᵛ (a : X), F_1 n a ∂[B; μ]) ∫ᵛ (a : X), f a ∂[B; μ]
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
AlgebraicGeometry.Scheme.Hom.singleton_mem_fppfPrecoverage : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Flat f] [AlgebraicGeometry.Surjective f]
  [AlgebraicGeometry.LocallyOfFinitePresentation f],
  CategoryTheory.Presieve.singleton f ∈ AlgebraicGeometry.Scheme.fppfPrecoverage.coverings Y
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.max?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp], t₁.Equiv t₂ → t₁.max? = t₂.max?
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the angle between two vectors is `π / 2`, the second vector is nonzero.  -/
Orientation.right_ne_zero_of_oangle_eq_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) → y ≠ 0
-- Init.Prelude
/-- `a⁻¹` computes the inverse of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `⁻¹` in identifiers is `inv`. -/
Inv.inv : {α : Type u} → [self : Inv α] → α → α
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.eq_normN_cert.eq_1 : ∀ (lhs rhs : Lean.Grind.Linarith.Expr), Lean.Grind.Linarith.eq_normN_cert lhs rhs = (lhs.toPolyN == rhs.toPolyN)
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
deriv_riemannZeta_eq_neg_inv_sub_sq_mul_add : ∀ {s : ℂ}, s ≠ 1 → deriv riemannZeta s = -(s - 1)⁻¹ ^ 2 * riemannZeta₁ s + (s - 1)⁻¹ * deriv riemannZeta₁ s
-- Mathlib.Analysis.Calculus.Gradient.Basic
inner_gradient_left : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {x y : F}, inner 𝕜 (gradient f x) y = (fderiv 𝕜 f x) y
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
/-- The canonical linear map `M →ₗ[R] CliffordAlgebra Q`.  -/
CliffordAlgebra.ι : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (Q : QuadraticForm R M) → M →ₗ[R] CliffordAlgebra Q
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Wequiv.below : {F : Type u → Type v} →
  [q : QPF F] →
    {motive : (a a_1 : (QPF.P F).W) → QPF.Wequiv a a_1 → Prop} → {a a_1 : (QPF.P F).W} → QPF.Wequiv a a_1 → Prop
-- Mathlib.RingTheory.PowerSeries.Ideal
/-- If `R` is noetherian then so is `R⟦X⟧`.  -/
PowerSeries.instIsNoetherianRing : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R], IsNoetherianRing (PowerSeries R)
-- Mathlib.Algebra.Lie.Weights.Linear
LieModule.Weight.instCoeLinearMap : (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] →
                      [LieModule.LinearWeights R L M] → CoeOut (LieModule.Weight R L M) (L →ₗ[R] R)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.extendIsoEquiv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cone F} {X : C} (i : X ⟶ s.pt)
  [inst_2 : CategoryTheory.IsIso i],
  CategoryTheory.Limits.IsLimit.extendIsoEquiv i =
    equivOfSubsingletonOfSubsingleton (CategoryTheory.Limits.IsLimit.extendIso i)
      (CategoryTheory.Limits.IsLimit.ofExtendIso i)
-- Mathlib.Condensed.Discrete.Colimit
/-- To presheaves on `Profinite` whose restrictions to finite sets are isomorphic have isomorphic left
Kan extensions.
 -/
Condensed.lanPresheafExt : {F G : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} →
  (FintypeCat.toProfinite.op.comp F ≅ FintypeCat.toProfinite.op.comp G) →
    (Condensed.lanPresheaf F ≅ Condensed.lanPresheaf G)
-- Mathlib.RepresentationTheory.Equiv
Representation.leftRegularTensorTrivialIsoFree.eq_1 : ∀ {G : Type v} [inst : Monoid G] {k : Type u} [inst_1 : CommSemiring k] (α : Type w'),
  Representation.leftRegularTensorTrivialIsoFree α =
    Representation.Equiv.mk
      (((((TensorProduct.congr (MonoidAlgebra.coeffLinearEquiv k) (MonoidAlgebra.coeffLinearEquiv k)).trans
                    (finsuppTensorFinsupp' k G α)).trans
                (Finsupp.domLCongr (Equiv.prodComm G α))).trans
            (Finsupp.curryLinearEquiv k)).trans
        (Finsupp.mapRange.linearEquiv (MonoidAlgebra.coeffLinearEquiv k).symm))
      ⋯
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.maxValueSealed : Int64
-- Mathlib.Analysis.Complex.UpperHalfPlane.Measure
UpperHalfPlane.measurable_coe : Measurable UpperHalfPlane.coe
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Lean.commandDeclare_sint_simprocs_ : Lean.ParserDescr
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.tr_supports : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} (enc : Γ → List.Vector Bool n) (dec : List.Vector Bool n → Γ)
  (M : Λ → Turing.TM1.Stmt Γ Λ σ) [inst : Fintype Γ] [inst_1 : Inhabited Λ] {S : Finset Λ},
  Turing.TM1.Supports M S → Turing.TM1.Supports (Turing.TM1to1.tr enc dec M) (Turing.TM1to1.trSupp M S)
-- Mathlib.RingTheory.Derivation.Lie
Derivation.instLieModule : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A],
  LieModule R (Derivation R A A) A
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Iso.sumComm_comp_sumCongr : ∀ {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W}
  {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G ≃g G') (g : H ≃g H'),
  SimpleGraph.Iso.sumComm.comp (f.sumCongr g) = (g.sumCongr f).comp SimpleGraph.Iso.sumComm
-- Mathlib.FieldTheory.NormalizedTrace
Algebra.normalizedTrace_eq_of_finiteDimensional_apply : ∀ (F : Type u_1) {K : Type u_2} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] [inst_3 : CharZero F]
  [inst_4 : Algebra.IsIntegral F K] [FiniteDimensional F K] (a : K),
  (Algebra.normalizedTrace F K) a = (↑(Module.finrank F K))⁻¹ • (Algebra.trace F K) a
-- Mathlib.RingTheory.Kaehler.Basic
/-- `Ω[S⁄R]` is isomorphic to `S` copies of `S` with kernel `KaehlerDifferential.kerTotal`.  -/
KaehlerDifferential.quotKerTotalEquiv : (R : Type u) →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → ((S →₀ S) ⧸ KaehlerDifferential.kerTotal R S) ≃ₗ[S] Ω[S⁄R]
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Truncated.skAdj.coreflective : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (n : ℕ) →
      [inst_1 :
          ∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
            (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F] →
        [∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
              (SimplexCategory.Truncated.inclusion n).op.HasPointwiseLeftKanExtension F] →
          CategoryTheory.Coreflective (CategoryTheory.SimplicialObject.Truncated.sk n)
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_zero_right : ∀ (n : ℕ), n.choose 0 = 1
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.mk_eq_mk_iff : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y X' Y' : T} (f : X ⟶ Y) (f' : X' ⟶ Y'),
  CategoryTheory.Arrow.mk f = CategoryTheory.Arrow.mk f' ↔
    ∃ (hX : X = X') (hY : Y = Y'),
      f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hX)
          (CategoryTheory.CategoryStruct.comp f' (CategoryTheory.eqToHom ⋯))
-- Mathlib.Topology.Compactification.StoneCech
ultrafilter_compact : ∀ {α : Type u}, CompactSpace (Ultrafilter α)
-- Mathlib.Data.Sigma.Interval
Sigma.Ioo_mk_mk : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (α i)]
  [inst_2 : (i : ι) → LocallyFiniteOrder (α i)] (i : ι) (a b : α i),
  Finset.Ioo ⟨i, a⟩ ⟨i, b⟩ = Finset.map (Function.Embedding.sigmaMk i) (Finset.Ioo a b)
-- Mathlib.Data.PNat.Factors
PrimeMultiset.prod_add : ∀ (u v : PrimeMultiset), (u + v).prod = u.prod * v.prod
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.fold_eq_foldM : ∀ {α β : Type w} {γ : Type x} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_2 : Std.IteratorLoop α Id Id] {f : γ → β → γ} {init : γ} {it : Std.Iter β},
  Std.Iter.fold f init it = (Std.Iter.foldM (fun x1 x2 => pure (f x1 x2)) init it).run