mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.lhom_ext'_iff : ∀ {R : Type u} [inst : Semiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f g : Polynomial R →ₗ[R] M}, f = g ↔ ∀ (n : ℕ), f ∘ₗ Polynomial.monomial n = g ∘ₗ Polynomial.monomial n
-- Qq.Macro
Qq.Impl.removeDollar : Lean.Name → Option Lean.Name
-- Mathlib.Algebra.Polynomial.Roots
/-- Non-constant polynomials have finite fibres, provided the coefficients are a domain.  -/
Polynomial.tendstoCofinite_of_natDegree_ne_zero : ∀ {R : Type} [inst : CommRing R] [IsDomain R] (p : Polynomial R),
  p.natDegree ≠ 0 → Filter.TendstoCofinite fun x => Polynomial.eval x p
-- Mathlib.Data.Ordmap.Invariants
Ordnode.toList_node : ∀ {α : Type u_1} (s : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α),
  (Ordnode.node s l x r).toList = l.toList ++ x :: r.toList
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addZ.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) (P Q : Fin 3 → R),
  W'.addZ P Q =
    -3 * P 0 ^ 2 * Q 0 * Q 2 + 3 * P 0 * Q 0 ^ 2 * P 2 + P 1 ^ 2 * Q 2 ^ 2 - Q 1 ^ 2 * P 2 ^ 2 +
                    W'.a₁ * P 0 * P 1 * Q 2 ^ 2 -
                  W'.a₁ * Q 0 * Q 1 * P 2 ^ 2 -
                W'.a₂ * P 0 ^ 2 * Q 2 ^ 2 +
              W'.a₂ * Q 0 ^ 2 * P 2 ^ 2 +
            W'.a₃ * P 1 * P 2 * Q 2 ^ 2 -
          W'.a₃ * Q 1 * P 2 ^ 2 * Q 2 -
        W'.a₄ * P 0 * P 2 * Q 2 ^ 2 +
      W'.a₄ * Q 0 * P 2 ^ 2 * Q 2
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKeyD_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Option γ}
  {k fallback : α} (h : (↑m).WF),
  (Std.DHashMap.Internal.Raw₀.filterMap f m).getKeyD k fallback =
    ((m.getKey? k).pfilter fun x h' => (f x (Std.DHashMap.Internal.Raw₀.Const.get m x ⋯)).isSome).getD fallback
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.mk : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] [toIsPrincipalIdealRing : IsPrincipalIdealRing R]
  [toIsLocalRing : IsLocalRing R], IsLocalRing.maximalIdeal R ≠ ⊥ → IsDiscreteValuationRing R
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.toContinuousMultilinearMap_injective : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N], Function.Injective ContinuousAlternatingMap.toContinuousMultilinearMap
-- Init.Data.SInt.Lemmas
Int8.toInt32_toISize : ∀ (n : Int8), n.toISize.toInt32 = n.toInt32
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.rpowIntegrand₁₂.eq_1 : ∀ (p t x : ℝ), p.rpowIntegrand₁₂ t x = t ^ (p - 1) * (t⁻¹ * x + t * (t + x)⁻¹ - 1)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.coe_singleton : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : T1Space α] (x : α), ↑{x} = {x}
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
WeierstrassCurve.ofJNe0Or1728_Δ : ∀ {R : Type u_1} [inst : CommRing R] (j : R), (WeierstrassCurve.ofJNe0Or1728 j).Δ = j ^ 2 * (j - 1728) ^ 9
-- Mathlib.Topology.Order.IntermediateValue
/-- A closed interval in a densely ordered conditionally complete linear order is preconnected.  -/
isPreconnected_Icc : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a b : α}, IsPreconnected (Set.Icc a b)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalRingHom.eq_of_eqOn_sdense : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] {F : Type u_1} [inst_1 : FunLike F R S]
  [inst_2 : NonUnitalNonAssocSemiring S] [NonUnitalRingHomClass F R S] {s : Set R},
  NonUnitalSubsemiring.closure s = ⊤ → ∀ {f g : F}, Set.EqOn (⇑f) (⇑g) s → f = g
-- Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
/-- The morphism `C⁺ : Spec R[x] → Spec R` is open.  -/
AlgebraicGeometry.Polynomial.isOpenMap_comap_C : ∀ {R : Type u_1} [inst : CommRing R], IsOpenMap (PrimeSpectrum.comap Polynomial.C)
-- Mathlib.Data.Set.Image
Set.image_preimage_subset : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set β), f '' f ⁻¹' s ⊆ s
-- Mathlib.Analysis.Normed.Ring.Units
nonunits.isClosed : ∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R], IsClosed (nonunits R)
-- Mathlib.Algebra.Category.HopfAlgCat.Monoidal
/-- The data needed to induce a `MonoidalCategory` structure via
`HopfAlgCat.instMonoidalCategoryStruct` and the forgetful functor to bialgebras.  -/
HopfAlgCat.MonoidalCategory.inducingFunctorData : (R : Type u) →
  [inst : CommRing R] → CategoryTheory.Monoidal.InducingFunctorData (CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R))
-- Init.Data.SInt.Basic
/-- Obtain the `BitVec` that contains the 2's complement representation of the `Int8`.
 -/
Int8.toBitVec : Int8 → BitVec 8
-- Lean.Meta.Tactic.Grind.SimpUtil
Lean.Meta.Grind.normalizeImp : Lean.Expr → Lean.Grind.Config → Lean.MetaM Lean.Expr
-- Mathlib.Order.Filter.AtTopBot.CompleteLattice
/-- If `f` is a monotone function with bounded range
and `g` tends to `atBot` along a nontrivial filter,
then the indexed infimum of `f ∘ g` is equal to the indexed infimum of `f`.

The assumption `BddBelow (range f)` can be omitted,
if the codomain of `f` is a conditionally complete linear order or a complete lattice, see below.
 -/
Monotone.ciInf_comp_tendsto_atBot : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder β] [inst_1 : ConditionallyCompleteLattice γ]
  {l : Filter α} [l.NeBot] {f : β → γ},
  Monotone f → BddBelow (Set.range f) → ∀ {g : α → β}, Filter.Tendsto g l Filter.atBot → ⨅ a, f (g a) = ⨅ b, f b
-- Lean.Elab.Tactic.SolveByElim
Lean.Elab.Tactic.SolveByElim.evalApplyAssumption : Lean.Elab.Tactic.Tactic
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_insertManyIfNewUnit_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} {ρ : Type w} [inst_2 : ForIn Id ρ α]
  [EquivBEq α] [LawfulHashable α], m.WF → ∀ {l : ρ} {k : α}, k ∈ m → k ∈ m.insertManyIfNewUnit l
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingSecond_succ_zero : ∀ (n : ℕ), n.succ.stirlingSecond 0 = 0
-- Mathlib.Analysis.Distribution.TestFunction
/-- Reformulation of the universal property of the topology on `𝓓^{n}(Ω, F)`, in the form of a
custom constructor for continuous linear maps `𝓓^{n}(Ω, F) →L[𝕜] V`, where `V` is an arbitrary
locally convex topological vector space. See also `mkCLM`.  -/
TestFunction.limitCLM : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_3} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace ℝ E] →
          {Ω : TopologicalSpace.Opens E} →
            {F : Type u_4} →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace ℝ F] →
                  [inst_5 : NormedSpace 𝕜 F] →
                    {n : ℕ∞} →
                      {V : Type u_6} →
                        [inst_6 : AddCommGroup V] →
                          [inst_7 : Module ℝ V] →
                            [t : TopologicalSpace V] →
                              [IsTopologicalAddGroup V] →
                                [ContinuousSMul ℝ V] →
                                  [LocallyConvexSpace ℝ V] →
                                    [inst_11 : Algebra ℝ 𝕜] →
                                      [inst_12 : IsScalarTower ℝ 𝕜 F] →
                                        [inst_13 : Module 𝕜 V] →
                                          [IsScalarTower ℝ 𝕜 V] →
                                            (toFun : TestFunction Ω F n → V) →
                                              (T :
                                                  (K : TopologicalSpace.Compacts E) →
                                                    ↑K ⊆ ↑Ω → ContDiffMapSupportedIn E F n K →L[𝕜] V) →
                                                (∀ (K : TopologicalSpace.Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω)
                                                    (f : ContDiffMapSupportedIn E F n K),
                                                    toFun (TestFunction.ofSupportedIn K_sub_Ω f) = (T K K_sub_Ω) f) →
                                                  TestFunction Ω F n →L[𝕜] V
-- Mathlib.Algebra.Order.Monoid.Basic
/-- Pullback an `IsOrderedCancelMonoid` under an injective map.  -/
Function.Injective.isOrderedCancelMonoid : ∀ {α : Type u} {β : Type u_1} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedCancelMonoid α]
  [inst_3 : CommMonoid β] [inst_4 : Preorder β] (f : β → α),
  (∀ (x y : β), f (x * y) = f x * f y) → (∀ {x y : β}, f x ≤ f y ↔ x ≤ y) → IsOrderedCancelMonoid β
-- Mathlib.Data.Set.Subsingleton
Set.Subsingleton.inter_singleton : ∀ {α : Type u} {a : α} {s : Set α}, (s ∩ {a}).Subsingleton
-- Mathlib.NumberTheory.ModularForms.SlashActions
SlashAction.zero_slash : ∀ {β : Type u_1} {G : Type u_2} {α : Type u_3} {inst : Monoid G} {inst_1 : AddMonoid α} [self : SlashAction β G α]
  (k : β) (g : G), SlashAction.map k g 0 = 0
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
/-- If `φ : G ≃ₜ* G` then `mulEquivHaarChar φ` is the positive real factor by which
`φ` scales Haar measures on `G`.  -/
MeasureTheory.mulEquivHaarChar : {G : Type u_1} →
  [inst : Group G] →
    [inst_1 : TopologicalSpace G] →
      [inst_2 : MeasurableSpace G] →
        [BorelSpace G] → [IsTopologicalGroup G] → [LocallyCompactSpace G] → G ≃ₜ* G → NNReal
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
MeasureTheory.lintegral_mul_const'' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) {f : α → ENNReal},
  AEMeasurable f μ → ∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r
-- Mathlib.Topology.Connected.PathConnected
Pi.instPathConnectedSpace : ∀ {ι : Type u_3} {Z : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (Z i)] [∀ (i : ι), PathConnectedSpace (Z i)],
  PathConnectedSpace ((i : ι) → Z i)
-- Mathlib.Analysis.InnerProductSpace.JointEigenspace
/-- In finite dimensions, given a commuting family of symmetric linear operators, the inner
product space on which they act decomposes as an internal direct sum of joint eigenspaces.  -/
LinearMap.IsSymmetric.directSum_isInternal_of_pairwise_commute : ∀ {𝕜 : Type u_1} {E : Type u_2} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {T : n → Module.End 𝕜 E} [FiniteDimensional 𝕜 E] [inst_4 : DecidableEq (n → 𝕜)],
  (∀ (i : n), LinearMap.IsSymmetric (T i)) →
    Pairwise (Function.onFun Commute T) → DirectSum.IsInternal fun α => ⨅ j, (T j).eigenspace (α j)
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
/-- **Double counting** argument.

Considering `r` as a bipartite graph, the LHS is a lower bound on the number of edges while the RHS
is an upper bound.  -/
Finset.card_nsmul_le_card_nsmul' : ∀ {R : Type u_1} {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {s : Finset α} {t : Finset β} [inst : Semiring R]
  [inst_1 : PartialOrder R] [IsOrderedRing R] {m n : R} [inst_3 : (a : α) → (b : β) → Decidable (r a b)],
  (∀ b ∈ t, n ≤ ↑(Finset.bipartiteBelow r s b).card) →
    (∀ a ∈ s, ↑(Finset.bipartiteAbove r t a).card ≤ m) → t.card • n ≤ s.card • m
-- Mathlib.LinearAlgebra.Matrix.Notation
/-- Updating a row then removing it is the same as removing it.  -/
Matrix.submatrix_updateRow_succAbove : ∀ {α : Type u} {m : ℕ} {n' : Type uₙ} {o' : Type uₒ} (A : Matrix (Fin m.succ) n' α) (v : n' → α) (f : o' → n')
  (i : Fin m.succ), (A.updateRow i v).submatrix i.succAbove f = A.submatrix i.succAbove f
-- Init.Data.Array.Lemmas
Array.toList_modify : ∀ {α : Type u_1} {xs : Array α} {f : α → α} {i : ℕ}, (xs.modify i f).toList = xs.toList.modify i f
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.MapTarget.chainable : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {len : ℕ}
  (self : Std.Sat.AIG.RefVec.MapTarget aig len), Std.Sat.AIG.RefVec.LawfulMapOperator α self.func
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- The angle at the apex of an isosceles triangle is `π` minus twice a base angle, oriented
angle-at-point form.  -/
EuclideanGeometry.oangle_eq_pi_sub_two_zsmul_oangle_of_dist_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  p₂ ≠ p₃ →
    dist p₁ p₂ = dist p₁ p₃ → EuclideanGeometry.oangle p₃ p₁ p₂ = ↑Real.pi - 2 • EuclideanGeometry.oangle p₁ p₂ p₃
-- Mathlib.Order.Filter.CardinalInter
Filter.CardinalGenerateSets.superset : ∀ {α : Type u} {c : Cardinal.{u}} {g : Set (Set α)} {s t : Set α},
  Filter.CardinalGenerateSets g s → s ⊆ t → Filter.CardinalGenerateSets g t
-- Mathlib.Logic.Equiv.Fintype
Function.Embedding.toEquivRange_symm_apply_self : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] (f : α ↪ β) (a : α),
  f.toEquivRange.symm ⟨f a, ⋯⟩ = a
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `M` and `N` are linearly disjoint, if one of `M` and `N` is flat,
if any two elements of `↥(M ⊓ N)` are commutative, then the rank of `↥(M ⊓ N)` is at most one.  -/
Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N →
    Module.Flat R ↥M ∨ Module.Flat R ↥N → (∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n) → Module.rank R ↥(M ⊓ N) ≤ 1
-- Mathlib.Order.RelSeries
RelSeries.last_snoc' : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (newLast : α) (rel : (p.last, newLast) ∈ r),
  (p.snoc newLast rel).toFun (Fin.last (p.length + 1)) = newLast
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.closure_sUnion : ∀ {K : Type u} [inst : DivisionRing K] (s : Set (Set K)), Subfield.closure (⋃₀ s) = ⨆ t ∈ s, Subfield.closure t
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GLPos.coe_neg_GL : ∀ {n : Type u} {R : Type v} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing R] [inst_3 : LinearOrder R]
  [inst_4 : IsStrictOrderedRing R] [inst_5 : Fact (Even (Fintype.card n))] (g : ↥(Matrix.GLPos n R)), ↑(-g) = -↑g
-- Mathlib.Combinatorics.Enumerative.Composition
composition_card : ∀ (n : ℕ), Fintype.card (Composition n) = 2 ^ (n - 1)
-- Mathlib.Data.TypeVec
TypeVec.const.eq_1 : ∀ {β : Type u_1} (x : β) (n : ℕ) (α : TypeVec.{u_2} n.succ) (a : Fin2 n),
  TypeVec.const x α a.fs =
    match (motive := (x : ℕ) → (x_1 : TypeVec.{u_2} x) → (x_2 : Fin2 x) → x_1 x_2 → TypeVec.repeat x β x_2) n.succ, α,
      a.fs with
    | n.succ, α, a.fs => TypeVec.const x α.drop a
    | n.succ, x_1, Fin2.fz => fun x_2 => x
-- Mathlib.Algebra.Group.Prod
AddEquiv.prodProdProdComm.eq_1 : ∀ (M : Type u_3) (N : Type u_4) [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (M' : Type u_6) (N' : Type u_7)
  [inst_2 : AddZeroClass N'] [inst_3 : AddZeroClass M'],
  AddEquiv.prodProdProdComm M N M' N' =
    { toFun := fun mnmn => ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2),
      invFun := fun mmnn => ((mmnn.1.1, mmnn.2.1), mmnn.1.2, mmnn.2.2), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Eq
Std.Tactic.BVDecide.BVPred.mkEq : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {w : ℕ} → (aig : Std.Sat.AIG α) → aig.BinaryRefVec w → Std.Sat.AIG.Entrypoint α
-- Mathlib.Util.Notation3
Mathlib.Notation3.MatchState.mk.inj : ∀ {vars : Std.HashMap Lean.Name (Lean.SubExpr × Lean.LocalContext × Lean.LocalInstances)}
  {scopeState : Option (Array (Lean.TSyntax `Batteries.ExtendedBinder.extBinderParenthesized))}
  {foldState : Std.HashMap Lean.Name (Array Lean.Term)}
  {vars_1 : Std.HashMap Lean.Name (Lean.SubExpr × Lean.LocalContext × Lean.LocalInstances)}
  {scopeState_1 : Option (Array (Lean.TSyntax `Batteries.ExtendedBinder.extBinderParenthesized))}
  {foldState_1 : Std.HashMap Lean.Name (Array Lean.Term)},
  { vars := vars, scopeState := scopeState, foldState := foldState } =
      { vars := vars_1, scopeState := scopeState_1, foldState := foldState_1 } →
    vars = vars_1 ∧ scopeState = scopeState_1 ∧ foldState = foldState_1
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.cyclesMapIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} (iso : K ≅ L) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i], (HomologicalComplex.cyclesMapIso iso i).hom = HomologicalComplex.cyclesMap iso.hom i
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.nonsingular_iff : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R),
  W'.Nonsingular P ↔
    W'.Equation P ∧
      (W'.a₁ * P 1 * P 2 - (3 * P 0 ^ 2 + 2 * W'.a₂ * P 0 * P 2 ^ 2 + W'.a₄ * P 2 ^ 4) ≠ 0 ∨
        2 * P 1 + W'.a₁ * P 0 * P 2 + W'.a₃ * P 2 ^ 3 ≠ 0 ∨
          W'.a₁ * P 0 * P 1 + 3 * W'.a₃ * P 1 * P 2 ^ 2 -
              (2 * W'.a₂ * P 0 ^ 2 * P 2 + 4 * W'.a₄ * P 0 * P 2 ^ 3 + 6 * W'.a₆ * P 2 ^ 5) ≠
            0)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.tendsto_translation_number₀ : ∀ (f : CircleDeg1Lift), Filter.Tendsto (fun n => (f ^ n) 0 / ↑n) Filter.atTop (nhds f.translationNumber)
-- Mathlib.Data.Analysis.Filter
CFilter.mk.injEq : ∀ {α : Type u_1} {σ : Type u_2} [inst : PartialOrder α] (f : σ → α) (pt : σ) (inf : σ → σ → σ)
  (inf_le_left : ∀ (a b : σ), f (inf a b) ≤ f a) (inf_le_right : ∀ (a b : σ), f (inf a b) ≤ f b) (f_1 : σ → α)
  (pt_1 : σ) (inf_1 : σ → σ → σ) (inf_le_left_1 : ∀ (a b : σ), f_1 (inf_1 a b) ≤ f_1 a)
  (inf_le_right_1 : ∀ (a b : σ), f_1 (inf_1 a b) ≤ f_1 b),
  ({ f := f, pt := pt, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right } =
      { f := f_1, pt := pt_1, inf := inf_1, inf_le_left := inf_le_left_1, inf_le_right := inf_le_right_1 }) =
    (f = f_1 ∧ pt = pt_1 ∧ inf = inf_1)
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- `F` is oplax monoidal given a counit morphism `η : F.obj (𝟙_ C) ⟶ 𝟙_ D` and a tensorator
`δ : F (- ⊗ -) ⟶ F - ⊗ F -` as a natural transformation between bifunctors, satisfying the
relevant compatibilities.
 -/
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (η :
                  F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶
                    CategoryTheory.MonoidalCategoryStruct.tensorUnit D) →
                (δ :
                    CategoryTheory.MonoidalCategory.curriedTensorPost F ⟶
                      CategoryTheory.MonoidalCategory.curriedTensorPre F) →
                  CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap δ =
                      CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap δ →
                    CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.leftMapₗ F =
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.topMapₗ F)
                          (CategoryTheory.CategoryStruct.comp
                            (δ.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                            (CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.bottomMapₗ η)) →
                      CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.leftMapᵣ F =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.topMapᵣ F)
                            (CategoryTheory.CategoryStruct.comp
                              (((CategoryTheory.flipFunctor C C D).map δ).app
                                (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                              (CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.bottomMapᵣ η)) →
                        F.OplaxMonoidal
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.shortComplexTruncLE_shortExact : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K : CochainComplex C ℤ) (n : ℤ), (K.shortComplexTruncLE n).ShortExact
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.ofFinitary_indep : ∀ {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅)
  (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I))
  (indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I)
  (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E),
  (IndepMatroid.ofFinitary E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).Indep = Indep
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_congr : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} {s t : Set α},
  s =ᵐ[μ] t → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in t, f x ∂μ
-- Mathlib.Data.W.Constructions
/-- The isomorphism from lists to the `WType` construction of lists  -/
WType.ofList : (γ : Type u) → List γ → WType (WType.Listβ γ)
-- Lean.DocString.Parser
/-- Records that the parser is presently parsing a list.
 -/
Lean.Doc.Parser.InList : Type
-- Mathlib.Logic.Encodable.Basic
_private.Mathlib.Logic.Encodable.Basic.0.Encodable.encodeSigma.match_1.splitter : {α : Type u_1} →
  {γ : α → Type u_2} → (motive : Sigma γ → Sort u_3) → (x : Sigma γ) → ((a : α) → (b : γ a) → motive ⟨a, b⟩) → motive x
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_min : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {he : t ≠ ∅}
  {hc : t.min he ∈ t}, t.get (t.min he) hc = t.min he
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.top_adj : ∀ {V : Type u} {G : SimpleGraph V} {a b : V}, ⊤.Adj a b ↔ G.Adj a b
-- Mathlib.Data.Set.Basic
Set.univ.nonempty : ∀ {α : Type u} [Nonempty α], Nonempty ↑Set.univ
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- **Alias** of `smul_apply`. -/
SlashInvariantForm.smul_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : SMul M β} {inst_2 : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α), (r • f) x = r • f x
-- Lean.Elab.MutualDef
Lean.Elab.DefViewElabHeader.toDefViewElabHeaderData : Lean.Elab.DefViewElabHeader → Lean.Elab.DefViewElabHeaderData
-- Mathlib.Algebra.Group.Semiconj.Defs
/-- Any element semiconjugates `0` to `0`.  -/
AddSemiconjBy.zero_right : ∀ {M : Type u_2} [inst : AddZeroClass M] (a : M), AddSemiconjBy a 0 0
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd_finset_def : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset β} {a : α},
  a +ᵥ s = Finset.image (fun x => a +ᵥ x) s
-- Mathlib.Algebra.Module.LinearMap.Polynomial
/-- Let `L` and `M` be finite free modules over `R`,
and let `φ : L →ₗ[R] Module.End R M` be a linear family of endomorphisms,
and denote `n := nilRank φ`.

An element `x : L` is *nil-regular* with respect to `φ`
if the `n`-th coefficient of the characteristic polynomial of `φ x` is non-zero.  -/
LinearMap.IsNilRegular : {R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup L] →
          [inst_2 : Module R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                (L →ₗ[R] Module.End R M) →
                  [Module.Free R M] → [Module.Finite R M] → [Module.Finite R L] → [Module.Free R L] → L → Prop