mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Basis.Defs
/-- If `b` is a basis for `M` and `b'` a basis for `M'`, and the index types are equivalent,
`b.equiv b' e` is a linear equivalence `M ≃ₗ[R] M'`, mapping `b i` to `b' (e i)`.  -/
Module.Basis.equiv : {ι' : Type u_2} →
  {M' : Type u_7} →
    [inst : AddCommMonoid M'] →
      {ι : Type u_10} →
        {R : Type u_11} →
          {M : Type u_12} →
            [inst_1 : Semiring R] →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : Module R M] →
                  Module.Basis ι R M → [inst_4 : Module R M'] → Module.Basis ι' R M' → ι ≃ ι' → M ≃ₗ[R] M'
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
/-- The localization map of a submodule.  -/
Submodule.toLocalized₀ : {R : Type u_1} →
  {M : Type u_3} →
    {N : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] →
                (p : Submonoid R) →
                  (f : M →ₗ[R] N) →
                    [inst_5 : IsLocalizedModule p f] → (M' : Submodule R M) → ↥M' →ₗ[R] ↥(Submodule.localized₀ p f M')
-- Mathlib.AlgebraicGeometry.Scheme
/-- Copies a morphism with a different underlying map  -/
AlgebraicGeometry.Scheme.Hom.copyBase : {X Y : AlgebraicGeometry.Scheme} → (f : X.Hom Y) → (g : ↥X → ↥Y) → ⇑f = g → (X ⟶ Y)
-- Mathlib.Order.Filter.Prod
Filter.prod_map_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (F : Filter α) (G : Filter γ),
  Filter.map f F ×ˢ G = Filter.map (Prod.map f id) (F ×ˢ G)
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
/-- Postcompose an open partial homeomorphism with a homeomorphism.
We modify the source and target to have better definitional behavior.  -/
OpenPartialHomeomorph.transHomeomorph : {X : Type u_1} →
  {Y : Type u_3} →
    {Z : Type u_5} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : TopologicalSpace Z] → OpenPartialHomeomorph X Y → Y ≃ₜ Z → OpenPartialHomeomorph X Z
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
ContinuousLinearEquiv.compactConvergenceCLMCongrSL_symm_apply : ∀ {𝕜 : Type u_7} {𝕜₂ : Type u_8} {𝕜₃ : Type u_9} {𝕜₄ : Type u_10} {E : Type u_11} {F : Type u_12} {G : Type u_13}
  {H : Type u_14} [inst : AddCommGroup E] [inst_1 : AddCommGroup F] [inst_2 : AddCommGroup G] [inst_3 : AddCommGroup H]
  [inst_4 : NormedField 𝕜] [inst_5 : NormedField 𝕜₂] [inst_6 : NormedField 𝕜₃] [inst_7 : NormedField 𝕜₄]
  [inst_8 : Module 𝕜 E] [inst_9 : Module 𝕜₂ F] [inst_10 : Module 𝕜₃ G] [inst_11 : Module 𝕜₄ H]
  [inst_12 : TopologicalSpace E] [inst_13 : TopologicalSpace F] [inst_14 : TopologicalSpace G]
  [inst_15 : TopologicalSpace H] [inst_16 : IsTopologicalAddGroup G] [inst_17 : IsTopologicalAddGroup H]
  [inst_18 : ContinuousConstSMul 𝕜₃ G] [inst_19 : ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄}
  [inst_20 : RingHomInvPair σ₁₂ σ₂₁] [inst_21 : RingHomInvPair σ₂₁ σ₁₂] [inst_22 : RingHomInvPair σ₃₄ σ₄₃]
  [inst_23 : RingHomInvPair σ₄₃ σ₃₄] [inst_24 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [inst_25 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃]
  [inst_26 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_27 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄]
  [inst_28 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [inst_29 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] (e₁₂ : E ≃SL[σ₁₂] F)
  (e₄₃ : H ≃SL[σ₄₃] G) (φ : CompactConvergenceCLM σ₂₃ F G) (e : E), ⋯ = ⋯
-- Mathlib.Tactic.DepRewrite
_private.Mathlib.Tactic.DepRewrite.0.Mathlib.Tactic.DepRewrite.instEvalTermCastMode.evalTerm : Lean.Term → Lean.Elab.TermElabM (Mathlib.Tactic.DepRewrite.CastMode × Lean.Expr)
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Structure.fg_iff_finite : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] [L.IsRelational],
  FirstOrder.Language.Structure.FG L M ↔ Finite M
-- Std.Http.Data.URI.Basic
Std.Http.instReprRequestTarget.repr : Std.Http.RequestTarget → ℕ → Std.Format
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_sdiff_singleton_eq_closure : ∀ {α : Type u_2} {M : Matroid α} {X : Set α} {e : α}, e ∈ M.closure (X \ {e}) → M.closure (X \ {e}) = M.closure X
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.stabilizer_quotient : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), MulAction.stabilizer G ↑1 = H
-- Mathlib.Data.Set.Countable
Set.MapsTo.countable_of_injOn : ∀ {α : Type u} {β : Type v} {s : Set α} {t : Set β} {f : α → β},
  Set.MapsTo f s t → Set.InjOn f s → t.Countable → s.Countable
-- Mathlib.Topology.UniformSpace.CompareReals
AbsoluteValue.abs.congr_simp : ∀ {S : Type u_6} [inst : Ring S] [inst_1 : LinearOrder S] [inst_2 : IsStrictOrderedRing S],
  AbsoluteValue.abs = AbsoluteValue.abs
-- Mathlib.Tactic.Order.Graph.Tarjan
/-- The stack of visited vertices used in Tarjan's algorithm.  -/
Mathlib.Tactic.Order.Graph.TarjanState.stack : Mathlib.Tactic.Order.Graph.TarjanState → Array ℕ
-- Mathlib.Analysis.LocallyConvex.Montel
MontelSpace.heine_borel : ∀ {𝕜 : Type u_4} {E : Type u_5} {inst : SeminormedRing 𝕜} {inst_1 : Zero E} {inst_2 : SMul 𝕜 E}
  {inst_3 : TopologicalSpace E} [self : MontelSpace 𝕜 E] (s : Set E),
  IsClosed s → Bornology.IsVonNBounded 𝕜 s → IsCompact s
-- Mathlib.Algebra.GroupWithZero.ProdHom
WithZero.withZeroUnitsEquiv.eq_1 : ∀ {G : Type u_4} [inst : GroupWithZero G] [inst_1 : DecidablePred fun a => a = 0],
  WithZero.withZeroUnitsEquiv =
    { toFun := fun n => WithZero.recZeroCoe 0 Units.val n, invFun := fun a => if h : a = 0 then 0 else ↑(Units.mk0 a h),
      left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.card_edgeFinset_completeEquipartiteGraph : ∀ {r t : ℕ}, (SimpleGraph.completeEquipartiteGraph r t).edgeFinset.card = r.choose 2 * t ^ 2
-- Mathlib.Logic.Equiv.Set
Equiv.ofInjective_apply : ∀ {α : Sort u_3} {β : Type u_4} (f : α → β) (hf : Function.Injective f) (a : α), (Equiv.ofInjective f hf) a = ⟨f a, ⋯⟩
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_zero_eq_constantCoeff : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R], ⇑(MvPowerSeries.coeff 0) = ⇑MvPowerSeries.constantCoeff
-- Mathlib.Analysis.ODE.PicardLindelof
/-- When the radius is zero, a curve in `FunSpace` evaluated at `t₀` equals `x₀`.  -/
ODE.FunSpace.apply_of_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {L : NNReal}
  (α : ODE.FunSpace t₀ x₀ 0 L), α.toFun t₀ = x₀
-- Mathlib.FieldTheory.Cardinality
/-- There is a field structure on type if and only if its cardinality is a prime power.  -/
Field.nonempty_iff : ∀ {α : Type u}, Nonempty (Field α) ↔ IsPrimePow (Cardinal.mk α)
-- Mathlib.Algebra.Ring.Subring.Pointwise
Subring.mem_inv_pointwise_smul_iff : ∀ {M : Type u_1} {R : Type u_2} [inst : Group M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R] {a : M}
  {S : Subring R} {x : R}, x ∈ a⁻¹ • S ↔ a • x ∈ S
-- Mathlib.GroupTheory.Nilpotent
AddGroup.isNilpotent_iff : ∀ (G : Type u_2) [inst : AddGroup G], AddGroup.IsNilpotent G ↔ ∃ n, AddSubgroup.upperCentralSeries G n = ⊤
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.nodal.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} (s : Finset ι) (v : ι → R),
  Lagrange.nodal s v = ∏ i ∈ s, (Polynomial.X - Polynomial.C (v i))
-- Mathlib.CategoryTheory.Abelian.Exact
/-- If `(f, g)` is exact, then `Abelian.image.ι S.f` is a kernel of `S.g`.  -/
CategoryTheory.ShortComplex.Exact.isLimitImage : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {S : CategoryTheory.ShortComplex C} →
        S.Exact →
          CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Abelian.image.ι S.f) ⋯)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_finset_notMem : ∀ {α : Type u_1} (a : α), Measurable fun s => a ∉ s
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.isShared.sizeOf_spec : ∀ (x : Lean.IR.VarId), sizeOf (Lean.IR.Expr.isShared x) = 1 + sizeOf x
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.dmap.eq_2 : ∀ {α : Type u} {β : Type v} (a : α) (f : (a_1 : α) → some a = some a_1 → β),
  Std.Internal.List.Option.dmap✝ (some a) f = some (f a ⋯)
-- Mathlib.Order.Filter.ENNReal
NNReal.toReal_limsup : ∀ {ι : Type u_1} {f : Filter ι} {u : ι → NNReal}, Filter.limsup (fun i => ↑(u i)) f = ↑(Filter.limsup u f)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.tan_toReal : ∀ (θ : Real.Angle), Real.tan θ.toReal = θ.tan
-- Mathlib.Data.EReal.Basic
EReal.coe_pos : ∀ {x : ℝ}, 0 < ↑x ↔ 0 < x
-- Mathlib.Algebra.Group.Shrink
Shrink.instSub.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Sub α], Shrink.instSub = (equivShrink α).symm.sub
-- Mathlib.CategoryTheory.Limits.Shapes.SingleObj
CategoryTheory.Limits.SingleObj.colimitTypeRelEquivOrbitRelQuotient_symm_apply : ∀ {G : Type v} [inst : Group G] (J : CategoryTheory.Functor (CategoryTheory.SingleObj G) (Type u))
  (a : Quot ⇑(MulAction.orbitRel G (J.obj (CategoryTheory.SingleObj.star G)))),
  (CategoryTheory.Limits.SingleObj.colimitTypeRelEquivOrbitRelQuotient J).symm a =
    Quot.lift (fun x => Quot.mk J.ColimitTypeRel ⟨CategoryTheory.SingleObj.star G, x⟩) ⋯ a
-- Mathlib.Data.Multiset.Defs
/-- Defines a size for a multiset by referring to the size of the underlying list.

This has to be defined before the definition of `Finset`, otherwise its automatically generated
`SizeOf` instance will be wrong.
 -/
Multiset.sizeOf : {α : Type u_1} → [SizeOf α] → Multiset α → ℕ
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.comp_hom' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} {M N K : Bimod A B} (f : M ⟶ N) (g : N ⟶ K),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
/-- If `f : E → F` is injective and `E` is finite-dimensional,
`f` has a continuous left inverse.  -/
ContinuousLinearMap.HasLeftInverse.of_injective_of_finiteDimensional : ∀ {𝕜 : Type u_7} [inst : NontriviallyNormedField 𝕜] {E : Type u_8} {F : Type u_9} [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [inst_6 : TopologicalSpace F] [inst_7 : AddCommGroup F] [inst_8 : Module 𝕜 F] [IsTopologicalAddGroup F]
  [ContinuousSMul 𝕜 F] [T2Space F] {f : E →L[𝕜] F} [CompleteSpace 𝕜] [FiniteDimensional 𝕜 F],
  Function.Injective ⇑f → f.HasLeftInverse
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic valuation of `1 : R` equals 1.  -/
IsDedekindDomain.HeightOneSpectrum.intValuation.map_one' : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R),
  v.intValuationDef 1 = 1
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- A measurable set `s` is a *fundamental domain* for an additive action of an additive group `G`
on a measurable space `α` with respect to a measure `μ` if the sets `g +ᵥ s`, `g : G`, are pairwise
a.e. disjoint and cover the whole space.  -/
MeasureTheory.IsAddFundamentalDomain : (G : Type u_1) →
  {α : Type u_2} →
    [Zero G] →
      [VAdd G α] →
        [inst : MeasurableSpace α] →
          Set α → autoParam (MeasureTheory.Measure α) MeasureTheory.IsAddFundamentalDomain._auto_1 → Prop
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
/-- The atoms in a countably generated measurable space.

Some of those sets may be empty, but the nonempty ones are the atoms of the measurable space.
See `measurableAtom_eq_countablyGeneratedAtom_natGeneratingSequence`.  -/
MeasurableSpace.countablyGeneratedAtom : (α : Type u_3) → [inst : MeasurableSpace α] → [MeasurableSpace.CountablyGenerated α] → (ℕ → Prop) → Set α
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
UniqueFactorizationMonoid.exists_prime_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [UniqueFactorizationMonoid α], (∃ p, Prime p) ↔ ∃ x, x ≠ 0 ∧ ¬IsUnit x
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.norm_natCast : ∀ {d : ℤ} (n : ℕ), (↑n).norm = ↑n * ↑n
-- Std.Time.DateTime.WallTime
Std.Time.WallTime.instOfNat : {n : ℕ} → OfNat Std.Time.WallTime n
-- Mathlib.Data.List.Nodup
List.Nodup.of_append_right : ∀ {α : Type u} {l₁ l₂ : List α}, (l₁ ++ l₂).Nodup → l₂.Nodup
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeGroupBasis.reindex_apply : ∀ {ι : Type u_1} {ι' : Type u_2} {G : Type u_3} [inst : Group G] (b : FreeGroupBasis ι G) (e : ι ≃ ι') (x : ι'),
  (b.reindex e) x = b (e.symm x)
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.preimage_min : ∀ {X Y : SSet} (A B : X.Subcomplex) (p : Y ⟶ X), (A ⊓ B).preimage p = A.preimage p ⊓ B.preimage p
-- Mathlib.GroupTheory.Complement
/-- `S` and `T` are complements if `(*) : S × T → G` is a bijection.
This notion generalizes left transversals, right transversals, and complementary subgroups.

If `S` and `T` are `SetLike`s such as `Subgroup`s, see `isComplement_iff_bijective` for a
more ergonomic way to unfold.
 -/
Subgroup.IsComplement : {G : Type u_1} → [Group G] → Set G → Set G → Prop
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.pullback.lift_snd_assoc : ∀ {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [inst : CompHausLike.HasExplicitPullback f g]
  {Z : CompHausLike P} (a : Z ⟶ X) (b : Z ⟶ Y)
  (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) {Z_1 : CompHausLike P}
  (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.lift f g a b w)
      (CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.snd f g) h) =
    CategoryTheory.CategoryStruct.comp b h
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.add_nonempty : ∀ {α : Type u_2} [inst : Add α] {s t : Set α}, (s + t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Init.Grind.AC
Lean.Grind.AC.Seq : Type
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.shrinkFunctorHomEquiv_apply_coe : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X}
  [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  (t : (CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F) (Y : C) (f : Y ⟶ X) (hf : S.arrows f),
  ↑(CategoryTheory.Presieve.shrinkFunctorHomEquiv t) f hf =
    (CategoryTheory.ConcreteCategory.hom (t.app (Opposite.op Y))) ⟨CategoryTheory.shrinkYonedaObjObjEquiv.symm f, ⋯⟩
-- Mathlib.Algebra.GCDMonoid.Basic
subsingleton_gcdMonoid_of_unique_units : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [Subsingleton αˣ], Subsingleton (GCDMonoid α)
-- Mathlib.RepresentationTheory.Coinvariants
/-- Given a `G`-representation `(V, ρ)` and a type `α`, this is the map `(α →₀ V)_G →ₗ (α →₀ V_G)`
sending `⟦single a v⟧ ↦ single a ⟦v⟧`.  -/
Representation.coinvariantsToFinsupp : {k : Type u_6} →
  {G : Type u_7} →
    {V : Type u_8} →
      [inst : CommRing k] →
        [inst_1 : Group G] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Module k V] →
              (ρ : Representation k G V) → (α : Type u_9) → (ρ.finsupp α).Coinvariants →ₗ[k] α →₀ ρ.Coinvariants
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- A complex differentiable function `f : ℂ → E` is continuously differentiable at every point.  -/
Differentiable.contDiff : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E},
  Differentiable ℂ f → ∀ {n : WithTop ℕ∞}, ContDiff ℂ n f
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.exists_finset_support : ∀ {α : Type u} (x : FreeCommRing α), ∃ s, x.IsSupported ↑s
-- Mathlib.Order.SuccPred.LinearLocallyFinite
/-- `toZ` defines an `OrderIso` between `ι` and its range.  -/
orderIsoRangeToZOfLinearSuccPredArch : {ι : Type u_1} →
  [inst : LinearOrder ι] →
    [inst_1 : SuccOrder ι] →
      [inst_2 : PredOrder ι] → [inst_3 : IsSuccArchimedean ι] → [hι : Nonempty ι] → ι ≃o ↑(Set.range (toZ hι.some))
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
inv_lt' : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a b : α} [MulRightStrictMono α],
  a⁻¹ < b ↔ b⁻¹ < a
-- Mathlib.Order.CompleteLattice.Basic
le_iInf_comp : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {ι' : Sort u_8} (f : ι' → α) (g : ι → ι'),
  ⨅ y, f y ≤ ⨅ x, f (g x)
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.MatchEqnsExtState.eqns : Lean.Meta.Match.MatchEqnsExtState → Lean.PHashSet Lean.Name
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.X.eq_1 : ∀ {R : Type u} [inst : Semiring R], Polynomial.X = (Polynomial.monomial 1) 1
-- Mathlib.Condensed.Light.TopCatAdjunction
_private.Mathlib.Condensed.Light.TopCatAdjunction.0.LightCondSet.coinducingCoprod.eq_1 : ∀ (X : LightCondSet) (fst : LightProfinite) (i : X.obj.obj (Opposite.op fst)) (s : ↑⟨fst, i⟩.fst.toTop),
  LightCondSet.coinducingCoprod✝ X ⟨⟨fst, i⟩, s⟩ =
    (CategoryTheory.ConcreteCategory.hom (X.obj.map (CompHausLike.const (LightProfinite.of PUnit.{u + 1}) s).op)) i
-- Mathlib.Logic.Basic
instSubsingletonSubtype_mathlib : ∀ {α : Sort u_1} [Subsingleton α] (p : α → Prop), Subsingleton (Subtype p)
-- Mathlib.Order.MinMax
instLawfulOrderInf_mathlib : ∀ {α : Type u} [inst : LinearOrder α], Std.LawfulOrderInf α
-- Mathlib.Topology.Path
/-- A useful special case of `Continuous.path_extend`.  -/
Path.continuous_extend : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), Continuous ⇑γ.extend
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- Any morphism from a terminal object is split mono.  -/
CategoryTheory.Limits.terminal.isSplitMono_from : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y : C} [inst_1 : CategoryTheory.Limits.HasTerminal C]
  (f : ⊤_ C ⟶ Y), CategoryTheory.IsSplitMono f
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.mkRat_pos : ∀ {a : ℤ}, 0 < a → ∀ {b : ℕ}, b ≠ 0 → 0 < mkRat a b
-- Aesop.Search.Expansion
Aesop.runSafeRule : {Q : Type} →
  [inst : Aesop.Queue Q] → Aesop.GoalRef → Aesop.IndexMatchResult Aesop.SafeRule → Aesop.SearchM Q Aesop.SafeRuleResult
-- Lean.Util.Recognizers
Lean.Expr.app4? : Lean.Expr → Lean.Name → Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr)
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.State : Type
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.nonneg_inner_and_areaForm_eq_zero_iff_sameRay : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), 0 ≤ inner ℝ x y ∧ (o.areaForm x) y = 0 ↔ SameRay ℝ x y
-- Mathlib.Algebra.Group.Indicator
Set.mulIndicator_inv : ∀ {α : Type u_1} {G : Type u_6} [inst : Group G] (s : Set α) (f : α → G),
  (s.mulIndicator fun a => (f a)⁻¹) = fun a => (s.mulIndicator f a)⁻¹
-- Lean.Data.JsonRpc
/-- In JSON-RPC, each request from the client editor to the language server comes with a
request id so that the corresponding response can be identified or cancelled.  -/
Lean.JsonRpc.RequestID : Type
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.isZero_of_subsingleton : ∀ {R : Type u} [inst : Semiring R] (M : SemimoduleCat R) [Subsingleton ↑M], CategoryTheory.Limits.IsZero M
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsCyclotomicExtension.neZero' : ∀ (n : ℕ) [NeZero n] (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [IsCyclotomicExtension {n} A B] [IsDomain B], NeZero ↑n
-- Mathlib.FieldTheory.Minpoly.MinpolyDiv
coeff_minpolyDiv : ∀ (R : Type u_2) {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (x : S) (i : ℕ),
  (minpolyDiv R x).coeff i = (algebraMap R S) ((minpoly R x).coeff (i + 1)) + (minpolyDiv R x).coeff (i + 1) * x
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.cocone_pt : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct fun j => X.obj { as := j }],
  (CategoryTheory.Limits.Sigma.cocone X).pt = ∐ fun j => X.obj { as := j }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k a : α} {v : β k},
  (t.insertIfNew k v).get? a = if h : cmp k a = Ordering.eq ∧ k ∉ t then some (cast ⋯ v) else t.get? a
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_mul_real : ∀ {r : ℝ}, 0 < r → ∀ (x : ℂ), (x * ↑r).arg = x.arg
-- Mathlib.RingTheory.Polynomial.Opposites
Polynomial.support_opRingEquiv : ∀ {R : Type u_1} [inst : Semiring R] (p : (Polynomial R)ᵐᵒᵖ),
  ((Polynomial.opRingEquiv R) p).support = (MulOpposite.unop p).support
-- Mathlib.SetTheory.Cardinal.Free
Cardinal.mk_freeAddGroup : ∀ (α : Type u) [Nonempty α], Cardinal.mk (FreeAddGroup α) = max (Cardinal.mk α) Cardinal.aleph0
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- A graph homomorphism is a map on vertex sets that respects adjacency relations.

The notation `G →g G'` represents the type of graph homomorphisms.  -/
SimpleGraph.«term_→g_» : Lean.TrailingParserDescr
-- Mathlib.Util.CountHeartbeats
/-- `#count_heartbeats in cmd` counts the heartbeats used in the enclosed command `cmd`.
Use `#count_heartbeats` to count the heartbeats in *all* the following declarations.

This is most useful for setting sufficient but reasonable limits via `set_option maxHeartbeats`
for long-running declarations.

If you do so, please resist the temptation to set the limit as low as possible.
As the `simp` set and other features of the library evolve,
other contributors will find that their (likely unrelated) changes
have pushed the declaration over the limit.
`count_heartbeats in` will automatically suggest a `set_option maxHeartbeats` via "Try this:"
using the least number of the form `2^k * 200000` that suffices.

Note that the internal heartbeat counter accessible via `IO.getNumHeartbeats`
has granularity 1000 times finer than the limits set by `set_option maxHeartbeats`.
As this is intended as a user command, we divide by 1000.

The optional `approximately` keyword rounds down the heartbeats to the nearest thousand.
This helps make the tests more stable to small changes in heartbeats.
To use this functionality, use `#count_heartbeats approximately in cmd`.
 -/
Mathlib.CountHeartbeats.«command#count_heartbeatsApproximatelyIn__» : Lean.ParserDescr
-- Mathlib.ModelTheory.Order
/-- The relation symbol representing `≤`.  -/
FirstOrder.Language.IsOrdered.leSymb : {L : FirstOrder.Language} → [self : L.IsOrdered] → L.Relations 2
-- Lean.MetavarContext
Lean.MetavarContext.UnivMVarParamResult.expr : Lean.MetavarContext.UnivMVarParamResult → Lean.Expr
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
/-- The composition of the derivative of `extChartAt` with the derivative of the inverse of
`extChartAt` gives the identity.
Version where the basepoint belongs to `(extChartAt I x).source`.  -/
mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm' : ∀ {𝕜 : 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] [IsManifold I 1 M] {x y : M},
  y ∈ (extChartAt I x).source →
    mfderiv% ↑(extChartAt I x) y ∘SL mfderiv[Set.range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y) =
      ContinuousLinearMap.id 𝕜 (TangentSpace (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x) y))
-- Mathlib.Data.Real.Basic
Real.mk_const : ∀ {x : ℚ}, Real.mk (CauSeq.const abs x) = ↑x
-- Batteries.Data.List.Lemmas
List.IsChain.cons_of_imp_of_imp : ∀ {α : Type u_1} {R S : α → α → Prop} {a : α} {l : List α} {b : α},
  (∀ ⦃a b : α⦄, R a b → S a b) → (∀ ⦃c : α⦄, R a c → S b c) → List.IsChain R (a :: l) → List.IsChain S (b :: l)
-- Init.Grind.Norm
Lean.Grind.eq_false_eq : ∀ (p : Prop), (p = False) = ¬p
-- Init.Data.Int.LemmasAux
Int.neg_nonpos_iff : ∀ (i : ℤ), -i ≤ 0 ↔ 0 ≤ i