mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Ray
/-- A vector is in the same ray as a nonnegative multiple of itself.  -/
SameRay.sameRay_nonneg_smul_right : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {S : Type u_5} [inst_5 : CommSemiring S] [inst_6 : PartialOrder S]
  [inst_7 : Algebra S R] [inst_8 : Module S M] [SMulPosMono S R] [IsScalarTower S R M] {a : S} (v : M),
  0 ≤ a → SameRay R v (a • v)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_right_mono₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀],
  1 ≤ a → Monotone fun x => a ^ x
-- Lean.Meta.Tactic.Grind.AC.Types
/-- Mapping from expressions/terms to their structure ids.
Recall that term may be the argument of different operators.  -/
Lean.Meta.Grind.AC.State.exprToOpIds : Lean.Meta.Grind.AC.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr (List ℕ)
-- Aesop.Forward.State
/-- Erase pattern substitutions with the given source.  -/
Aesop.ForwardState.erasePatSubsts : Aesop.PatSubstSource → Aesop.ForwardState → Aesop.ForwardState
-- Std.Http.Data.URI.Basic
Std.Http.instReprURI.repr : Std.Http.URI → ℕ → Std.Format
-- Mathlib.Dynamics.TopologicalEntropy.Semiconj
Dynamics.coverEntropyInf_image_le_of_uniformContinuousOn_invariant : ∀ {X : Type u_1} {Y : Type u_2} [inst : UniformSpace X] [inst_1 : UniformSpace Y] {S : X → X} {T : Y → Y} {φ : X → Y},
  Function.Semiconj φ S T →
    ∀ {F G : Set X},
      UniformContinuousOn φ G →
        F ⊆ G → Set.MapsTo S G G → Dynamics.coverEntropyInf T (φ '' F) ≤ Dynamics.coverEntropyInf S F
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
expNegInvGlue.contDiff_polynomial_eval_inv_mul : ∀ {n : ℕ∞} (p : Polynomial ℝ), ContDiff ℝ ↑n fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
-- Mathlib.Dynamics.Ergodic.Action.Basic
ErgodicVAdd.aeconst_of_forall_preimage_vadd_ae_eq : ∀ {G : Type u_1} {α : Type u_2} {inst : VAdd G α} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [self : ErgodicVAdd G α μ] {s : Set α},
  MeasurableSet s → (∀ (g : G), (fun x => g +ᵥ x) ⁻¹' s =ᵐ[μ] s) → Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.simpTraceToSimp : Lean.TSyntax `tactic → Lean.Elab.Tactic.TacticM (Lean.TSyntax `tactic)
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasLaw.integral_eq : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : Type u_3} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [SecondCountableTopology E] {mE : MeasurableSpace E} [OpensMeasurableSpace E]
  {μ : MeasureTheory.Measure E} {X : Ω → E}, ProbabilityTheory.HasLaw X μ P → ∫ (x : Ω), X x ∂P = ∫ (x : E), x ∂μ
-- Mathlib.NumberTheory.Harmonic.Bounds
harmonic_eq_sum_Icc : ∀ {n : ℕ}, harmonic n = ∑ i ∈ Finset.Icc 1 n, (↑i)⁻¹
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.supportAddSubgroup_eq_bot : ∀ {F : Type u_2} [inst : Field F] (P : RingPreordering F), P.supportAddSubgroup = ⊥
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
/-- **Alias** of `AlgebraicGeometry.Etale`.

---

A morphism of schemes `f : X ⟶ Y` is étale if for each affine `U ⊆ Y` and
`V ⊆ f ⁻¹' U`, The induced map `Γ(Y, U) ⟶ Γ(X, V)` is étale.  -/
AlgebraicGeometry.IsEtale : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
affineSpan_eq_top_iff_nonempty_of_subsingleton : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P} [Subsingleton P], affineSpan k s = ⊤ ↔ s.Nonempty
-- Mathlib.Analysis.Normed.Affine.AddTorsor
dist_right_lineMap : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜),
  dist p₂ ((AffineMap.lineMap p₁ p₂) c) = ‖1 - c‖ * dist p₁ p₂
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
complEDS₂_one : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), complEDS₂ b c d 1 = b
-- Mathlib.Logic.Embedding.Basic
/-- `Sigma.mk` as a `Function.Embedding`.  -/
Function.Embedding.sigmaMk : {α : Type u_1} → {β : α → Type u_3} → (a : α) → β a ↪ (x : α) × β x
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.isClosedEmbedding_toContinuousMap : ∀ {X : Type u_1} {R : Type u_3} [inst : Zero X] [inst_1 : Zero R] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace R] [T1Space R], Topology.IsClosedEmbedding toContinuousMap
-- Mathlib.GroupTheory.Congruence.Opposite
AddCon.orderIsoOp.eq_1 : ∀ {M : Type u_1} [inst : Add M],
  AddCon.orderIsoOp = { toFun := AddCon.op, invFun := AddCon.unop, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.curryFinFinset_symm_apply_piecewise_const : ∀ {𝕜 : Type u} {n : ℕ} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] {k l : ℕ} {s : Finset (Fin n)}
  (hk : s.card = k) (hl : sᶜ.card = l) (f : G [×k]→L[𝕜] G [×l]→L[𝕜] G') (x y : G),
  ((ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl).symm f) (s.piecewise (fun x_1 => x) fun x => y) =
    (f fun x_1 => x) fun x => y
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
CategoryTheory.Limits.instIsIsoTerminalComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Limits.HasTerminal C]
  [inst_3 : CategoryTheory.Limits.HasTerminal D]
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G],
  CategoryTheory.IsIso (CategoryTheory.Limits.terminalComparison G)
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.exists_lt_mul_omega0' : ∀ {o : Ordinal.{u_1}} ⦃a : Ordinal.{u_1}⦄, a < o * Ordinal.omega0 → ∃ i, a < o * ↑i + o
-- Init.Data.SInt.Lemmas
Int32.toInt16_ofInt : ∀ {n : ℤ}, (Int32.ofInt n).toInt16 = Int16.ofInt n
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- If `f` is integrable on intervals `Ioc (a i) (b i)`,
where `a i` tends to -∞ and `b i` tends to ∞, and
`∫ x in a i .. b i, ‖f x‖ ∂μ` converges to `I : ℝ` along a filter `l`,
then `f` is integrable on the interval (-∞, ∞)  -/
MeasureTheory.integrable_of_intervalIntegral_norm_tendsto : ∀ {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.NeBot] [l.IsCountablyGenerated]
  [inst : NormedAddCommGroup E] {a b : ι → ℝ} {f : ℝ → E} (I : ℝ),
  (∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) (b i)) μ) →
    Filter.Tendsto a l Filter.atBot →
      Filter.Tendsto b l Filter.atTop →
        Filter.Tendsto (fun i => ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ) l (nhds I) → MeasureTheory.Integrable f μ
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.map : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R},
  f.Splits → ∀ {S : Type u_2} [inst_1 : Semiring S] (i : R →+* S), (Polynomial.map i f).Splits
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ}, (Std.TreeMap.Raw.map f t).isEmpty = t.isEmpty
-- Mathlib.CategoryTheory.MorphismProperty.Descent
/-- `P` codescends along `Q` if whenever `Q` holds for `Z ⟶ X`,
`P` holds for `X ⟶ X ∐[Z] Y` implies `P` holds for `Z ⟶ Y`.  -/
CategoryTheory.MorphismProperty.CodescendsAlong : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.RingTheory.Ideal.CotangentBaseChange
Ideal.tensorCotangentHom_tmul : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] (I : Ideal S) (t : T) (x : ↥I),
  (Ideal.tensorCotangentHom R T I) (t ⊗ₜ[R] I.toCotangent x) =
    t • (Ideal.map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent ⟨1 ⊗ₜ[R] ↑x, ⋯⟩
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
/-- Any action is `0`-preprimitive.  -/
AddAction.is_zero_preprimitive : ∀ (M : Type u_1) (α : Type u_2) [inst : AddGroup M] [inst_1 : AddAction M α], AddAction.IsMultiplyPreprimitive M α 0
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
/-- The component of an ideal sheaf at an affine open.  -/
AlgebraicGeometry.Scheme.IdealSheafData.ideal : {X : AlgebraicGeometry.Scheme} → X.IdealSheafData → (U : ↑X.affineOpens) → Ideal ↑(X.presheaf.obj (Opposite.op ↑U))
-- Mathlib.Data.Num.ZNum
ZNum.neg_zero : -0 = 0
-- Mathlib.GroupTheory.Index
AddSubgroup.finiteIndex_iInf : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_3} [Finite ι] {f : ι → AddSubgroup G},
  (∀ (i : ι), (f i).FiniteIndex) → (⨅ i, f i).FiniteIndex
-- Mathlib.Data.Set.Piecewise
Set.piecewise_insert : ∀ {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f g : (i : α) → δ i) [inst : (j : α) → Decidable (j ∈ s)]
  [inst_1 : DecidableEq α] (j : α) [inst_2 : (i : α) → Decidable (i ∈ insert j s)],
  (insert j s).piecewise f g = Function.update (s.piecewise f g) j (f j)
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.of_injective : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B), Function.Injective ⇑HNNExtension.of
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.addCommGroup : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {I : ModelWithCorners 𝕜 E H} →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    {G : Type u_10} →
                                      [inst_9 : AddCommGroup G] →
                                        [inst_10 : TopologicalSpace G] →
                                          [inst_11 : ChartedSpace H' G] →
                                            [LieAddGroup I' n G] → AddCommGroup (ContMDiffMap I I' N G n)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_erase_self : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, (m.erase k).getKey? k = none
-- Mathlib.Order.PrimeIdeal
Order.Ideal.IsPrime.compl_filter : ∀ {P : Type u_1} {inst : Preorder P} {I : Order.Ideal P} [self : I.IsPrime], Order.IsPFilter (↑I)ᶜ
-- Mathlib.RingTheory.Finiteness.Basic
Module.Finite.of_restrictScalars_finite : ∀ (R : Type u_6) (A : Type u_7) (M : Type u_8) [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : Module A M] [inst_5 : SMul R A] [IsScalarTower R A M] [hM : Module.Finite R M],
  Module.Finite A M
-- Mathlib.LinearAlgebra.Complex.Module
Complex.coe_realPart : ∀ (z : ℂ), ↑(realPart z) = ↑z.re
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.forkOfIsColimit_ι_map_inj_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} A]
  {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X}
  (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'}
  (hd : CategoryTheory.Limits.IsColimit d) (F : CategoryTheory.Functor Cᵒᵖ A) (i : E.I₀) {Z : A}
  (h : F.obj (Opposite.op (E.X i)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (E.forkOfIsColimit hc hd F).ι
      (CategoryTheory.CategoryStruct.comp (F.map (c.inj i).op) h) =
    CategoryTheory.CategoryStruct.comp (F.map (E.f i).op) h
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
/-- Given trivializations `e₁`, `e₂` in the atlas for vector bundles `E₁`, `E₂` over a base `B`,
the induced trivialization for the continuous `σ`-semilinear maps from `E₁` to `E₂`,
whose base set is `e₁.baseSet ∩ e₂.baseSet`.  -/
Bundle.Trivialization.continuousAlternatingMap : (𝕜 : Type u_1) →
  (ι : Type u_2) →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : Fintype ι] →
        {B : Type u_3} →
          [inst_2 : TopologicalSpace B] →
            {F₁ : Type u_4} →
              [inst_3 : NormedAddCommGroup F₁] →
                [inst_4 : NormedSpace 𝕜 F₁] →
                  {E₁ : B → Type u_5} →
                    [inst_5 : (x : B) → AddCommGroup (E₁ x)] →
                      [inst_6 : (x : B) → Module 𝕜 (E₁ x)] →
                        [inst_7 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] →
                          [inst_8 : (x : B) → TopologicalSpace (E₁ x)] →
                            [inst_9 : FiberBundle F₁ E₁] →
                              [inst_10 : VectorBundle 𝕜 F₁ E₁] →
                                {F₂ : Type u_6} →
                                  [inst_11 : NormedAddCommGroup F₂] →
                                    [inst_12 : NormedSpace 𝕜 F₂] →
                                      {E₂ : B → Type u_7} →
                                        [inst_13 : (x : B) → AddCommGroup (E₂ x)] →
                                          [inst_14 : (x : B) → Module 𝕜 (E₂ x)] →
                                            [inst_15 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] →
                                              [inst_16 : (x : B) → TopologicalSpace (E₂ x)] →
                                                [inst_17 : FiberBundle F₂ E₂] →
                                                  [inst_18 : VectorBundle 𝕜 F₂ E₂] →
                                                    [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] →
                                                      [inst_20 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] →
                                                        (e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) →
                                                          (e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj) →
                                                            [he₁ : MemTrivializationAtlas e₁] →
                                                              [he₂ : MemTrivializationAtlas e₂] →
                                                                Bundle.Trivialization (F₁ [⋀^ι]→L[𝕜] F₂)
                                                                  Bundle.TotalSpace.proj
-- Mathlib.Analysis.Meromorphic.Order
/-- The set where a meromorphic function has infinite order is clopen in its domain of meromorphy.
 -/
MeromorphicOn.isClopen_setOfPred_meromorphicOrderAt_eq_top : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜}, MeromorphicOn f U → IsClopen {u | meromorphicOrderAt f ↑u = ⊤}
-- Mathlib.Tactic.Simps.NotationClass
/-- Find arguments for a notation class  -/
Simps.defaultfindArgs : Simps.findArgType
-- Lean.Util.Sorry
Lean.Expr.hasSyntheticSorry : Lean.Expr → Bool
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapShortComplexH2_τ₁ : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u_1, u, u} k H}
  {B : Rep.{u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B),
  (groupCohomology.mapShortComplexH2 f φ).τ₁ = groupCohomology.cochainsMap₁ f φ
-- Mathlib.NumberTheory.RamificationInertia.Basic
/-- Since the inclusion `(P^(i + 1) / P^e) ⊂ (P^i / P^e)` has a kernel isomorphic to `P / S`,
`[P^i / P^e : R / p] = [P^(i+1) / P^e : R / p] + [P / S : R / p]`  -/
Ideal.rank_pow_quot_aux : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  [hfp : NeZero (p.ramificationIdx' P)] [IsDedekindDomain S] [p.IsMaximal] [P.IsPrime],
  P ≠ ⊥ →
    ∀ {i : ℕ},
      i < p.ramificationIdx' P →
        Module.rank (R ⧸ p) ↥(Ideal.map (Ideal.Quotient.mk (P ^ p.ramificationIdx' P)) (P ^ i)) =
          Module.rank (R ⧸ p) (S ⧸ P) +
            Module.rank (R ⧸ p) ↥(Ideal.map (Ideal.Quotient.mk (P ^ p.ramificationIdx' P)) (P ^ (i + 1)))
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_monomial_le : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (a : R), ((Polynomial.monomial n) a).degree ≤ ↑n
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.succ?_rotate : ∀ {n : ℕ} {x : BitVec n}, Std.PRange.succ? (BitVec.Signed.rotate✝ x) = BitVec.Signed.rotate✝ <$> Std.PRange.succ? x
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.apply_firstDiff_ne : ∀ {E : ℕ → Type u_1} {x y : (n : ℕ) → E n}, x ≠ y → x (PiNat.firstDiff x y) ≠ y (PiNat.firstDiff x y)
-- Mathlib.Algebra.Group.Equiv.Basic
/-- The isomorphism `(M₁ →* N) ≃* (M₂ →* N)` obtained by postcomposition with
a multiplicative equivalence `e : M₁ ≃* M₂`.  -/
MulEquiv.monoidHomCongrLeft : {M₁ : Type u_5} →
  {M₂ : Type u_6} →
    {N : Type u_8} →
      [inst : MulOneClass M₁] → [inst_1 : MulOneClass M₂] → [inst_2 : CommMonoid N] → M₁ ≃* M₂ → (M₁ →* N) ≃* (M₂ →* N)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.id_right_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented C)
  (X_1 : SimplexCategory),
  (CategoryTheory.CategoryStruct.id X).right.app X_1 = CategoryTheory.CategoryStruct.id (X.right.obj X_1)
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (mid : C) (ι : X ⟶ mid) (π : mid ⟶ Y)
  (ι_π : autoParam (CategoryTheory.CategoryStruct.comp ι π = f) CategoryTheory.Factorisation.ι_π._autoParam) (mid_1 : C)
  (ι_1 : X ⟶ mid_1) (π_1 : mid_1 ⟶ Y)
  (ι_π_1 : autoParam (CategoryTheory.CategoryStruct.comp ι_1 π_1 = f) CategoryTheory.Factorisation.ι_π._autoParam),
  ({ mid := mid, ι := ι, π := π, ι_π := ι_π } = { mid := mid_1, ι := ι_1, π := π_1, ι_π := ι_π_1 }) =
    (mid = mid_1 ∧ ι ≍ ι_1 ∧ π ≍ π_1)
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
/-- See also `continuousAt_cpow_const` for a version that assumes `z ≠ 0` but makes no
assumptions about `w`.  -/
Complex.continuousAt_cpow_const_of_re_pos : ∀ {z w : ℂ}, 0 ≤ z.re ∨ z.im ≠ 0 → 0 < w.re → ContinuousAt (fun x => x ^ w) z
-- Mathlib.MeasureTheory.Measure.Tight
MeasureTheory.IsTightMeasureSet.subset : ∀ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S T : Set (MeasureTheory.Measure 𝓧)} [inst : TopologicalSpace 𝓧],
  MeasureTheory.IsTightMeasureSet T → S ⊆ T → MeasureTheory.IsTightMeasureSet S
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
_private.Mathlib.CategoryTheory.Limits.Shapes.Reflexive.0.CategoryTheory.Limits.reflexivePair.match_1.eq_1 : ∀ (motive : CategoryTheory.Limits.WalkingReflexivePair → Sort u_1)
  (h_1 : Unit → motive CategoryTheory.Limits.WalkingReflexivePair.zero)
  (h_2 : Unit → motive CategoryTheory.Limits.WalkingReflexivePair.one),
  (match CategoryTheory.Limits.WalkingReflexivePair.zero with
    | CategoryTheory.Limits.WalkingReflexivePair.zero => h_1 ()
    | CategoryTheory.Limits.WalkingReflexivePair.one => h_2 ()) =
    h_1 ()
-- Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver
CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] {X Y : CategoryTheory.LocallyDiscrete Cᵒᵖ} (f : X ⟶ Y)
  (X_1 : CategoryTheory.Sheaf (J.over (Opposite.unop X.as)) A) {X_2 Y_1 : (CategoryTheory.Over (Opposite.unop Y.as))ᵒᵖ}
  (f_1 : X_2 ⟶ Y_1),
  (((J.pseudofunctorOver A).map f).toFunctor.obj X_1).obj.map f_1 =
    X_1.obj.map ((CategoryTheory.Over.map f.as.unop).map f_1.unop).op
-- Lean.Parser.Basic
Lean.Parser.symbolInfo : String → Lean.Parser.ParserInfo
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
Multiset.Nat.antidiagonalTuple_zero_succ : ∀ (n : ℕ), Multiset.Nat.antidiagonalTuple 0 n.succ = 0
-- Mathlib.Analysis.SpecificLimits.Basic
tendsto_pow_atTop_atTop_of_one_lt : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [Archimedean α]
  {r : α}, 1 < r → Filter.Tendsto (fun n => r ^ n) Filter.atTop Filter.atTop
-- Mathlib.Data.Nat.Nth
Nat.image_nth_Iio_card : ∀ {p : ℕ → Prop} (hf : (Set.ofPred p).Finite), Nat.nth p '' Set.Iio hf.toFinset.card = Set.ofPred p
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.nonneg_total : ∀ {d : ℕ} (a : ℤ√↑d), a.Nonneg ∨ (-a).Nonneg
-- Mathlib.Algebra.Order.Star.Prod
Prod.instStarOrderedRing : ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalSemiring α] [inst_1 : NonUnitalSemiring β] [inst_2 : PartialOrder α]
  [inst_3 : PartialOrder β] [inst_4 : StarRing α] [inst_5 : StarRing β] [StarOrderedRing α] [StarOrderedRing β],
  StarOrderedRing (α × β)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toContinuousAddMonoidHom_injective : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂],
  Function.Injective ContinuousAddMonoidHom.toContinuousAddMonoidHom
-- Mathlib.Combinatorics.Additive.DoublingConst
/-- If `A` has small doubling, then it has small difference, with the constant squared.

This is a consequence of the Ruzsa triangle inequality.  -/
Finset.divConst_le_mulConst_sq : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A : Finset G}, A.divConst A ≤ A.mulConst A ^ 2
-- Init.Data.List.Lemmas
List.flatMap_singleton : ∀ {α : Type u_1} {β : Type u_2} (f : α → List β) (x : α), List.flatMap f [x] = f x
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
Module.finrank_of_isPerfPair : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R N] (p : M →ₗ[R] N →ₗ[R] R) [p.IsPerfPair] [Module.Finite R M]
  [Module.Free R M], Module.finrank R M = Module.finrank R N
-- Mathlib.RingTheory.MvPowerSeries.Derivative
MvPowerSeries.pderiv_invOf : ∀ {σ : Type u_1} {R : Type u_2} {i : σ} [inst : CommRing R] (f : MvPowerSeries σ R) [inst_1 : Invertible f],
  (MvPowerSeries.pderiv R i) ⅟f = -⅟f ^ 2 * (MvPowerSeries.pderiv R i) f
-- Mathlib.LinearAlgebra.AffineSpace.Matrix
/-- A change of basis formula for barycentric coordinates.

See also `AffineBasis.toMatrix_inv_vecMul_toMatrix`.  -/
AffineBasis.toMatrix_vecMul_coords : ∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) [inst_4 : Fintype ι] (b₂ : AffineBasis ι k P) (x : P),
  Matrix.vecMul (b₂.coords x) (b.toMatrix ⇑b₂) = b.coords x
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin_deg : ∀ (l : ℕ) (pq : ℤ × Fin l), (CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin l).deg pq = pq.1 + ↑↑pq.2
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p} ℚ K] (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime]
  [hP₂ : P.LiesOver (Ideal.span {↑p})], P.ramificationIdx ℤ = p - 1