mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.ModularForms.BoundedAtCusp
OnePoint.IsZeroAt.smul_iff : ∀ {c : OnePoint ℝ} {f : UpperHalfPlane → ℂ} {k : ℤ} {g : GL (Fin 2) ℝ},
  (g • c).IsZeroAt f k ↔ c.IsZeroAt (SlashAction.map k g f) k
-- Mathlib.RepresentationTheory.Continuous.TopRep
/-- the underlying type of an object in `TopRep k G`  -/
TopRep.V : {k : Type u} →
  {G : Type v} → [inst : Ring k] → [inst_1 : TopologicalSpace k] → [inst_2 : Monoid G] → TopRep k G → Type w
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.instIsHomologicalCompOfIsTriangulated : ∀ {C : Type u_1} {D : Type u_2} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.HasShift C ℤ] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.Limits.HasZeroObject D] [inst_4 : CategoryTheory.HasShift D ℤ]
  [inst_5 : CategoryTheory.Preadditive D] [inst_6 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive]
  [inst_7 : CategoryTheory.Pretriangulated D] [inst_8 : CategoryTheory.Category.{v_3, u_3} A]
  [inst_9 : CategoryTheory.Limits.HasZeroObject C] [inst_10 : CategoryTheory.Preadditive C]
  [inst_11 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_12 : CategoryTheory.Pretriangulated C]
  [inst_13 : CategoryTheory.Abelian A] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor D A)
  [inst_14 : L.CommShift ℤ] [L.IsTriangulated] [F.IsHomological], (L.comp F).IsHomological
-- Mathlib.Algebra.GroupWithZero.Basic
GroupWithZero.toDivisionMonoid : {G₀ : Type u_2} → [GroupWithZero G₀] → DivisionMonoid G₀
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the angle between three points is nonzero, the first and third points are not equal.  -/
EuclideanGeometry.left_ne_right_of_oangle_ne_zero : ∀ {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}, EuclideanGeometry.oangle p₁ p₂ p₃ ≠ 0 → p₁ ≠ p₃
-- Std.Time.Format.Modifier
/-- Exactly noon (12:00:00)
 -/
Std.Time.DayPeriod.noon : Std.Time.DayPeriod
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.card_smul_finset : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : Group α] [inst_2 : MulAction α β] (a : α)
  (s : Finset β), (a • s).card = s.card
-- Mathlib.Order.Filter.Pi
Filter.pi_inf_principal_univ_pi_neBot : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {s : (i : ι) → Set (α i)},
  (Filter.pi f ⊓ Filter.principal (Set.univ.pi s)).NeBot ↔ ∀ (i : ι), (f i ⊓ Filter.principal (s i)).NeBot
-- Mathlib.Tactic.FunProp.Theorems
/-- Collection of lambda theorems  -/
Mathlib.Meta.FunProp.LambdaTheorems : Type
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.ext_isBase : ∀ {α : Type u_1} {M₁ M₂ : Matroid α}, M₁.E = M₂.E → (∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B)) → M₁ = M₂
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instPow_1 : {α : Type u_1} → {β : Type u_2} → [Pow α β] → Pow α βᵒᵈ
-- Mathlib.Order.BooleanAlgebra.Basic
sup_compl_eq_top : ∀ {α : Type u} {x : α} [inst : BooleanAlgebra α], x ⊔ xᶜ = ⊤
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.restrictScalars_sup : ∀ (S : Type u_1) {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M] (s t : Submodule R M),
  Submodule.restrictScalars S (s ⊔ t) = Submodule.restrictScalars S s ⊔ Submodule.restrictScalars S t
-- Mathlib.Topology.Algebra.Ring.Basic
/-- Construct an absolute value on a semiring `T` from an absolute value on a semiring `R`
and an injective ring homomorphism `f : T →+* R`  -/
AbsoluteValue.comp : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : Semiring T] →
        [inst_1 : Semiring R] →
          [inst_2 : Semiring S] →
            [inst_3 : PartialOrder S] → AbsoluteValue R S → {f : T →+* R} → Function.Injective ⇑f → AbsoluteValue T S
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- The target of a 1-simplex in a path is identified with the target vertex.  -/
SSet.Truncated.Path₁.arrow_tgt : ∀ {X : SSet.Truncated 1} {n : ℕ} (self : X.Path₁ n) (i : Fin n),
  (CategoryTheory.ConcreteCategory.hom
        (X.map
          (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 0) SSet.Truncated.Path₁._proof_1
              SSet.Truncated.Path₁._proof_5).op))
      (self.arrow i) =
    self.vertex i.succ
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roo_eq_if : ∀ {m n : ℕ}, (m<...n).toList = if m + 1 < n then (m + 1) :: ((m + 1)<...n).toList else []
-- Mathlib.RingTheory.LocalProperties.Submodule
Module.subsingleton_of_localization_maximal : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5) [inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_4 : (P : Ideal R) → [inst_4 : P.IsMaximal] → Module R (Mₚ P)]
  (f : (P : Ideal R) → [inst_5 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [∀ (P : Ideal R) [inst_5 : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)],
  (∀ (P : Ideal R) [inst : P.IsMaximal], Subsingleton (Mₚ P)) → Subsingleton M
-- Mathlib.Topology.Constructions
induced_to_pi : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {X : Type u_9} (f : X → (i : ι) → A i),
  TopologicalSpace.induced f Pi.topologicalSpace = ⨅ i, TopologicalSpace.induced (fun x => f x i) inferInstance
-- Init.Data.SInt.Basic
/-- Converts a word-sized signed integer to an 8-bit signed integer by truncating its bitvector representation.

This function is overridden at runtime with an efficient implementation.
 -/
ISize.toInt8 : ISize → Int8
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.HasImages.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasImage f) → CategoryTheory.Limits.HasImages C
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.Tendsto.div_const : ∀ {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a b : ENNReal},
  Filter.Tendsto m f (nhds a) → a ≠ 0 ∨ b ≠ 0 → Filter.Tendsto (fun x => m x / b) f (nhds (a / b))
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- Stalk of the structure sheaf at a prime p as localization of R  -/
AlgebraicGeometry.StructureSheaf.IsLocalization.to_stalk : ∀ (R : Type u) [inst : CommRing R] (p : PrimeSpectrum R),
  IsLocalization.AtPrime (↑((AlgebraicGeometry.Spec.structureSheaf R).presheaf.stalk p)) p.asIdeal
-- Init.Prelude
/-- Is this syntax a `node` with kind `k`?  -/
Lean.Syntax.isNodeOf : Lean.Syntax → Lean.SyntaxNodeKind → ℕ → Bool
-- Mathlib.FieldTheory.IsSepClosed
IsSepClosed.algebraMap_bijective : ∀ (k : Type u) [inst : Field k] (K : Type v) [inst_1 : Field K] [IsSepClosed k] [inst_3 : Algebra k K]
  [Algebra.IsSeparable k K], Function.Bijective ⇑(algebraMap k K)
-- Init.Sym.Lemmas
Lean.Sym.Fin.eq_eq_true : ∀ {n : ℕ} (a b : Fin n), decide (a = b) = true → (a = b) = True
-- Mathlib.Order.SuccPred.Limit
Order.isSuccPrelimitRecOn_of_isSuccPrelimit : ∀ {α : Type u_1} {b : α} {motive : α → Sort u_2} [inst : PartialOrder α] [inst_1 : SuccOrder α]
  (succ : (a : α) → ¬IsMax a → motive (Order.succ a)) (isSuccPrelimit : (a : α) → Order.IsSuccPrelimit a → motive a)
  (hb : Order.IsSuccPrelimit b), Order.isSuccPrelimitRecOn b succ isSuccPrelimit = isSuccPrelimit b hb
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
/-- The inverse function is continuous on `f '' s`.
Use properties of `OpenPartialHomeomorph` instead.  -/
ApproximatesLinearOn.inverse_continuousOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E ≃L[𝕜] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f (↑f') s c)
  (hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹), ContinuousOn (↑(hf.toPartialEquiv hc).symm) (f '' s)
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.withAppFn : {α : Type} →
  {m : Type → Type} → [Monad m] → [MonadReaderOf Lean.SubExpr m] → [MonadWithReaderOf Lean.SubExpr m] → m α → m α
-- Mathlib.Topology.Semicontinuity.Defs
/-- A relation `r : α → β → Prop` is semicontinuous at `x : α`, if whenever `r x y`
is true, it is also true for all `x'` sufficiently close to `x`.

This notion generalizes lower and upper semicontinuity of functions, as well as
lower and upper hemicontinuity of set-valued correspondences.  -/
SemicontinuousAt : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → (α → β → Prop) → α → Prop
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.OplaxMonoidal.δ_of_cartesianMonoidalCategory : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] (X Y : C),
  CategoryTheory.Functor.OplaxMonoidal.δ F X Y = CategoryTheory.CartesianMonoidalCategory.prodComparison F X Y
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.recoverHereWithKeeping : Array Lean.Syntax → ℕ → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.hasMap_comp : ∀ {I : Type u_1} {J : Type u_2} {K : Type u_3} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  (X : CategoryTheory.GradedObject I C) (p : I → J) [inst_1 : X.HasMap p] (q : J → K) (r : I → K),
  (∀ (i : I), q (p i) = r i) → ∀ [(X.mapObj p).HasMap q], X.HasMap r
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
/-- If `‖v‖^n * ‖f v‖` is integrable, then the Fourier transform of `f` is `C^n`.  -/
Real.contDiff_fourier : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V] [inst_6 : BorelSpace V]
  {f : V → E} {N : ℕ∞},
  (∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (fun v => ‖v‖ ^ n * ‖f v‖) MeasureTheory.volume) →
    ContDiff ℝ (↑N) (FourierTransform.fourier f)
-- Mathlib.Order.Hom.Basic
/-- The underlying function of an `OrderHom` is monotone.  -/
OrderHom.monotone' : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] (self : α →o β), Monotone self.toFun
-- Mathlib.MeasureTheory.Integral.DivergenceTheorem
/-- **Divergence theorem** for functions on the plane along rectangles. It is formulated in terms of
two functions `f g : ℝ × ℝ → E` and an integral over `Icc a b = [a.1, b.1] × [a.2, b.2]`, where
`a b : ℝ × ℝ`, `a ≤ b`. When thinking of `f` and `g` as the two coordinates of a single function
`F : ℝ × ℝ → E × E` and when `E = ℝ`, this is the usual statement that the integral of the
divergence of `F` inside the rectangle equals the integral of the normal derivative of `F` along the
boundary.

See also `MeasureTheory.integral2_divergence_prod_of_hasFDerivAt_off_countable` for a
version that does not assume `a ≤ b` and uses iterated interval integral instead of the integral
over `Icc a b`.  -/
MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivAt_off_countable_of_le : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f g : ℝ × ℝ → E)
  (f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E) (a b : ℝ × ℝ),
  a ≤ b →
    ∀ (s : Set (ℝ × ℝ)),
      s.Countable →
        ContinuousOn f (Set.Icc a b) →
          ContinuousOn g (Set.Icc a b) →
            (∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x) →
              (∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x) →
                MeasureTheory.IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) MeasureTheory.volume →
                  ∫ (x : ℝ × ℝ) in Set.Icc a b, (f' x) (1, 0) + (g' x) (0, 1) =
                    (((∫ (x : ℝ) in a.1..b.1, g (x, b.2)) - ∫ (x : ℝ) in a.1..b.1, g (x, a.2)) +
                        ∫ (y : ℝ) in a.2..b.2, f (b.1, y)) -
                      ∫ (y : ℝ) in a.2..b.2, f (a.1, y)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isSome_minKey?_iff_isEmpty_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → (t.minKey?.isSome = true ↔ t.isEmpty = false)
-- Mathlib.Data.Real.Basic
Real.decidableLT : (a b : ℝ) → Decidable (a < b)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- The natural isomorphism between the diagrams attached to `data : F.PreOneHypercoverDenseData X`
that are induced by isomorphisms in `C₀ᵒᵖ ⥤ A`.  -/
CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanMapIso : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {A : Type u'} →
            [inst_2 : CategoryTheory.Category.{v', u'} A] →
              {X : C} →
                (data : F.PreOneHypercoverDenseData X) →
                  {P Q : CategoryTheory.Functor C₀ᵒᵖ A} →
                    (P ≅ Q) → ((data.multicospanIndex P).multicospan ≅ (data.multicospanIndex Q).multicospan)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.filter_eq_self_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {f : α → Bool}, Std.ExtHashSet.filter f m = m ↔ ∀ (k : α) (h : k ∈ m), f (m.get k h) = true
-- Mathlib.Analysis.LConvolution
/-- Convolution is commutative when the group is commutative.  -/
MeasureTheory.lconvolution_comm : ∀ {G : Type u_1} {mG : MeasurableSpace G} [inst : AddCommGroup G] [MeasurableAdd₂ G] [MeasurableNeg G]
  {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] [μ.IsNegInvariant] {f g : G → ENNReal},
  MeasureTheory.lconvolution f g μ = MeasureTheory.lconvolution g f μ
-- Mathlib.Logic.Function.Defs
Function.map_comp_prod : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} (f : ι → α) (g : ι → β) {γ : Type u_4} {δ : Type u_5} (h : α → γ)
  (k : β → δ), Prod.map h k ∘ Function.prod f g = Function.prod (h ∘ f) (k ∘ g)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.smulFDeriv.eq_1 : ∀ (g : GL (Fin 2) ℝ) (z : ℂ),
  UpperHalfPlane.smulFDeriv g z =
    ↑↑(UpperHalfPlane.σ g) ∘SL
      ContinuousLinearMap.restrictScalars ℝ
        (ContinuousLinearMap.toSpanSingleton ℂ (↑↑(Matrix.GeneralLinearGroup.det g) / UpperHalfPlane.denom g z ^ 2))
-- Mathlib.Algebra.Order.GroupWithZero.Basic
div_le_comm₀ : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀},
  0 < b → 0 < c → (a / b ≤ c ↔ a / c ≤ b)
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.CongrInfo.congrTheorem.injEq : ∀ (thm thm_1 : Lean.Meta.CongrTheorem),
  (Lean.Meta.Sym.CongrInfo.congrTheorem thm = Lean.Meta.Sym.CongrInfo.congrTheorem thm_1) = (thm = thm_1)
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.top_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Top α] [inst_2 : SemilatticeInf β] [inst_3 : OrderTop β]
  (a : α), ⊤ a = ⊤
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.equation_some : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (a b : R),
  W'.Equation ![a, b, 1] ↔ W'.toAffine.Equation a b
-- Mathlib.Topology.DenseEmbedding
IsDenseInducing.toIsInducing : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β},
  IsDenseInducing i → Topology.IsInducing i
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.rightUnshift_rightShift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n' + a = n),
  (γ.rightShift a n' hn').rightUnshift n hn' = γ
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- Adding a point to a set with a finite-dimensional span increases the dimension by at most
one.  -/
finrank_vectorSpan_insert_le_set : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : Set P) (p : P),
  Module.finrank k ↥(vectorSpan k (insert p s)) ≤ Module.finrank k ↥(vectorSpan k s) + 1
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.opProductIsoCoproduct_inv_comp_lift : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C}
  [inst_1 : CategoryTheory.Limits.HasProduct Z] {X : C} (π : (a : α) → X ⟶ Z a),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProductIsoCoproduct Z).inv
      (CategoryTheory.Limits.Pi.lift π).op =
    CategoryTheory.Limits.Sigma.desc fun a => (π a).op
-- Mathlib.LinearAlgebra.Matrix.Action
Matrix.instModuleForall : {n : Type u_1} →
  {R : Type u_2} → [inst : Fintype n] → [inst_1 : DecidableEq n] → [inst_2 : Semiring R] → Module (Matrix n n R) (n → R)
-- Mathlib.Analysis.Complex.Circle
Circle.instDistribMulAction : {M : Type u_3} → [inst : AddMonoid M] → [DistribMulAction ℂ M] → DistribMulAction Circle M
-- ProofWidgets.Presentation.Expr
ProofWidgets.GetExprPresentationParams.mk.sizeOf_spec : ∀ (expr : Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx) (name : Lean.Name),
  sizeOf { expr := expr, name := name } = 1 + sizeOf expr + sizeOf name
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_ne_zero : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ) [IsDomain R] [NeZero 2], Polynomial.Chebyshev.T R n ≠ 0
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonPlainGoal : Lean.ToJson Lean.Lsp.PlainGoal
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Stream.toList.eq_1 : ∀ {α : Type u_1} (t : RBTree.RBNode.Stream α), t.toList = RBTree.RBNode.Stream.foldr (fun x1 x2 => x1 :: x2) t []
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Delaborates a function application of the form `f ... x (fun _ : Unit => y)`.  -/
Lean.PrettyPrinter.Delaborator.delabLazyBinop : ℕ →
  (Lean.Term → Lean.Term → Lean.PrettyPrinter.Delaborator.DelabM Lean.Term) →
    Lean.PrettyPrinter.Delaborator.DelabM Lean.Term
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.rawIdentNoAntiquot.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Compactness.Compact
noncompact_univ : ∀ (X : Type u_2) [inst : TopologicalSpace X] [NoncompactSpace X], ¬IsCompact Set.univ
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.toList_eq_match_roi : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [inst_3 : Std.Rxi.IsAlwaysFinite α],
  r.toList =
    match Std.PRange.least? with
    | none => []
    | some init => init :: init<...*.toList
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioi_subset_Ioc_union_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ioi a ⊆ Set.Ioc a b ∪ Set.Ici b
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.locallyCompactSpace_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α],
  LocallyCompactSpace (TopologicalSpace.NonemptyCompacts α) ↔ LocallyCompactSpace α
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.findSomeM?.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (x : Option β) (h_1 : (b : β) → motive (some b))
  (h_2 : (x : Option β) → motive x),
  (∀ (b : β), x = some b → False) →
    (match x with
      | some b => h_1 b
      | x => h_2 x) =
      h_2 x
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.coe_mk' : ∀ {ι : Type u_1} (l u : ι → ℝ), ↑(BoxIntegral.Box.mk' l u) = Set.univ.pi fun i => Set.Ioc (l i) (u i)
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.nhds_zero_eq_of_basis : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  (𝔖 : Set (Set E)) {ι : Type u_6} {p : ι → Prop} {b : ι → Set F},
  (nhds 0).HasBasis p b → nhds 0 = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), Filter.principal {f | Set.MapsTo (⇑f) s (b i)}
-- Mathlib.Algebra.Category.Grp.FilteredColimits
GrpCat.FilteredColimits.G.mk_eq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J GrpCat) (x y : (j : J) × ↑(F.obj j)),
  (∃ k f g,
      (CategoryTheory.ConcreteCategory.hom (F.map f)) x.snd = (CategoryTheory.ConcreteCategory.hom (F.map g)) y.snd) →
    GrpCat.FilteredColimits.G.mk F x = GrpCat.FilteredColimits.G.mk F y
-- Mathlib.Probability.Kernel.Condexp
MeasureTheory.AEStronglyMeasurable.integral_condExpKernel : ∀ {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] [inst_2 : NormedAddCommGroup F] {f : Ω → F}
  [inst_3 : NormedSpace ℝ F],
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable (fun ω => ∫ (y : Ω), f y ∂(ProbabilityTheory.condExpKernel μ m) ω) μ
-- Mathlib.GroupTheory.Congruence.Defs
/-- Given types with additions `M, N` and an additive congruence relation `c` on `N`,
an addition-preserving map `f : M → N` induces an additive congruence relation on `f`'s domain
defined by '`x ≈ y` iff `f(x)` is related to `f(y)` by `c`.'  -/
AddCon.comap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Add M] → [inst_1 : Add N] → (f : M → N) → (∀ (x y : M), f (x + y) = f x + f y) → AddCon N → AddCon M
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
WeakDual.CharacterSpace.equivAlgHom.congr_simp : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : CompleteSpace A]
  [inst_3 : NormedAlgebra 𝕜 A], WeakDual.CharacterSpace.equivAlgHom = WeakDual.CharacterSpace.equivAlgHom
-- Mathlib.CategoryTheory.Limits.Final.ParallelPair
CategoryTheory.Limits.parallelPair_initial_mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f g : X ⟶ Y),
  (∀ (Z : C), Nonempty (X ⟶ Z)) →
    (∀ ⦃Z : C⦄ (i j : X ⟶ Z),
        ∃ a, i = CategoryTheory.CategoryStruct.comp f a ∧ j = CategoryTheory.CategoryStruct.comp g a) →
      (CategoryTheory.Limits.parallelPair f g).Initial
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.mk.inj : ∀ {X : Type u_7} {Y : Type u_8} {inst : TopologicalSpace X} {inst_1 : TopologicalSpace Y}
  {toPartialEquiv : PartialEquiv X Y} {continuousOn_toFun : ContinuousOn (↑toPartialEquiv) toPartialEquiv.source}
  {continuousOn_invFun : ContinuousOn toPartialEquiv.invFun toPartialEquiv.target} {toPartialEquiv_1 : PartialEquiv X Y}
  {continuousOn_toFun_1 : ContinuousOn (↑toPartialEquiv_1) toPartialEquiv_1.source}
  {continuousOn_invFun_1 : ContinuousOn toPartialEquiv_1.invFun toPartialEquiv_1.target},
  { toPartialEquiv := toPartialEquiv, continuousOn_toFun := continuousOn_toFun,
        continuousOn_invFun := continuousOn_invFun } =
      { toPartialEquiv := toPartialEquiv_1, continuousOn_toFun := continuousOn_toFun_1,
        continuousOn_invFun := continuousOn_invFun_1 } →
    toPartialEquiv = toPartialEquiv_1
-- Init.Data.Nat.Fold
Eq.congr_simp : ∀ {α : Sort u_1} (a a_1 : α), a = a_1 → ∀ (a_2 a_3 : α), a_2 = a_3 → (a = a_2) = (a_1 = a_3)
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Functor.sum_map_inl : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C D)
  {a a' : A} (f : a ⟶ a'),
  (F.sum G).map ((CategoryTheory.Sum.inl_ A C).map f) = (CategoryTheory.Sum.inl_ B D).map (F.map f)