mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
/-- The cusp form submodule is linearly equivalent to the type of cusp forms.  -/
ModularForm.CuspForm.equivCuspFormSubmodule : (Γ : Subgroup (GL (Fin 2) ℝ)) → (k : ℤ) → [inst : Γ.HasDetOne] → CuspForm Γ k ≃ₗ[ℂ] ↥(ModularForm.cuspFormSubmodule Γ k)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.le_sup_left : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  [inst_2 : SemilatticeSup β] [inst_3 : ContinuousSup β] (f g : α →ₘ[μ] β), f ≤ f ⊔ g
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.AddConvolutionExistsAt.vadd_convolution : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} [inst : AddMonoid M] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid E'] [inst_4 : Module S E] [inst_5 : Module S E'] {F : Type u_10}
  [inst_6 : AddCommMonoid F] [inst_7 : Module S F] [inst_8 : TopologicalSpace F] [ContinuousConstSMul S F] [T2Space F]
  {c : S} {f : M → E} {g : M → E'} {x : M} (L : E →ₗ[S] E' →ₗ[S] F),
  DiscreteConvolution.AddConvolutionExistsAt L f g x →
    DiscreteConvolution.addConvolution L (c • f) g x = c • DiscreteConvolution.addConvolution L f g x
-- Lean.Level
/-- If result is true, then forall assignments `A` which assigns all parameters and metavariables occurring
in `l`, `l[A] != zero`  -/
Lean.Level.isNeverZero : Lean.Level → Bool
-- Std.Sync.Channel
/-- Return `true` if the channel is closed.
 -/
Std.CloseableChannel.Sync.isClosed : {α : Type} → Std.CloseableChannel.Sync α → BaseIO Bool
-- Lean.Elab.Tactic.Omega.OmegaM
Lean.Elab.Tactic.Omega.State.mk.inj : ∀ {atoms atoms_1 : Std.HashMap Lean.Expr ℕ}, { atoms := atoms } = { atoms := atoms_1 } → atoms = atoms_1
-- Aesop.Stats.Basic
Aesop.RuleStatsTotals : Type
-- Mathlib.Analysis.Analytic.Constructions
AnalyticAt.pi : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_9} [inst_3 : Fintype ι] {e : E} {Fm : ι → Type u_10}
  [inst_4 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (Fm i)] {f : (i : ι) → E → Fm i},
  (∀ (i : ι), AnalyticAt 𝕜 (f i) e) → AnalyticAt 𝕜 (fun x x_1 => f x_1 x) e
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Broadcast.Consumer : Type → Type
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
/-- An equivalence between the vertices of a simplicial set `X` and the
objects of `hoFunctor.obj X`.  -/
SSet.hoFunctor.unitHomEquiv : (X : SSet) →
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit SSet ⟶ X) ≃
    CategoryTheory.Functor ↑CategoryTheory.Cat.chosenTerminal ↑(SSet.hoFunctor.obj X)
-- Mathlib.Order.SuccPred.Basic
Order.lt_succ_iff_eq_or_lt_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α}, ¬IsMax b → (a < Order.succ b ↔ a = b ∨ a < b)
-- Mathlib.AlgebraicTopology.SimplicialNerve
/-- The simplicial thickening defines a functor from the category of linear orders to the category of
simplicial categories
 -/
CategoryTheory.SimplicialThickening.functor : {J K : Type u} →
  [inst : LinearOrder J] →
    [inst_1 : LinearOrder K] →
      (J →o K) →
        CategoryTheory.EnrichedFunctor SSet (CategoryTheory.SimplicialThickening J)
          (CategoryTheory.SimplicialThickening K)
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.tensorObj₃_ext : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ : CategoryTheory.GradedObject I C} [inst_3 : X₂.HasTensor X₃]
  [inst_4 : X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] {j : I} {A : C}
  (f g : CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) j ⟶ A)
  [H : X₁.HasGoodTensorTensor₂₃ X₂ X₃],
  (∀ (i₁ i₂ i₃ : I) (hi : i₁ + i₂ + i₃ = j),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi) f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi)
          g) →
    f = g
-- Mathlib.Topology.CWComplex.Classical.Graph
/-- The 1-skeleton of a CW complex as a graph.  -/
Topology.CWComplex.OneSkeletonGraph : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    (C : Set X) →
      [inst_1 : Topology.CWComplex C] → Graph (Topology.RelCWComplex.cell C 0) (Topology.RelCWComplex.cell C 1)
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.primeSpectrumOrderEquiv_apply_coe_carrier : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (a : (PrimeSpectrum ↥A)ᵒᵈ),
  ↑↑(A.primeSpectrumOrderEquiv a) =
    {x | ∃ a_1 ∈ A, ∃ a_2, (∃ (x : a_2 ∈ A), ⟨a_2, ⋯⟩ ∉ (OrderDual.ofDual a).asIdeal) ∧ x = a_1 * a_2⁻¹}
-- Mathlib.Topology.Algebra.Valued.NormedValued
Valued.toNormedField.norm_lt_one_iff : ∀ {L : Type u_1} [inst : Field L] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀]
  [hv : Valued.v.RankOne] {x : L}, ‖x‖ < 1 ↔ Valued.v x < 1
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.opcyclesMap_comp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j')
  (g' : j' ⟶ k') {i'' j'' k'' : ι} (f'' : i'' ⟶ j'') (g'' : j'' ⟶ k'')
  (α : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g')
  (α' : CategoryTheory.ComposableArrows.mk₂ f' g' ⟶ CategoryTheory.ComposableArrows.mk₂ f'' g'')
  (α'' : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f'' g'') (n : ℤ),
  autoParam (CategoryTheory.CategoryStruct.comp α α' = α'')
      CategoryTheory.Abelian.SpectralObject.opcyclesMap_comp._auto_1 →
    CategoryTheory.CategoryStruct.comp (X.opcyclesMap f g f' g' α n) (X.opcyclesMap f' g' f'' g'' α' n) =
      X.opcyclesMap f g f'' g'' α'' n
-- Mathlib.Algebra.Group.Basic
sub_nsmul_nsmul_add : ∀ {M : Type u_4} [inst : AddMonoid M] {m n : ℕ} (a : M), m ≤ n → (n - m) • a + m • a = n • a
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Constructor for `ComposableArrows C 1`.  -/
CategoryTheory.ComposableArrows.mk₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → {X₀ X₁ : C} → (X₀ ⟶ X₁) → CategoryTheory.ComposableArrows C 1
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.queryMap : Std.DHashMap Lean.Name fun x => Lean.Name × Array (Lean.MacroM (Lean.TSyntax `term))
-- Mathlib.Topology.LocallyClosed
subset_coborder : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, s ⊆ coborder s
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
CompactCoherentification.continuousOn_rng_of_isCompact : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {f : X → CompactCoherentification Y} {K : Set X},
  IsCompact K → (ContinuousOn f K ↔ ContinuousOn (⇑(CompactCoherentification.mk Y).symm ∘ f) K)
-- Mathlib.Algebra.Order.Module.Defs
/-- Do not use this. Use `le_of_smul_le_smul_right` instead.  -/
SMulPosReflectLE.le_of_smul_le_smul_right : ∀ {α : Type u_1} {β : Type u_2} {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero β}
  [self : SMulPosReflectLE α β] ⦃b : β⦄, 0 < b → ∀ ⦃a₁ a₂ : α⦄, a₁ • b ≤ a₂ • b → a₁ ≤ a₂
-- Mathlib.FieldTheory.PrimitiveElement
AlgHom.card_of_splits : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [inst_3 : FiniteDimensional F E] [Algebra.IsSeparable F E] (L : Type u_3) [inst_5 : Field L] [inst_6 : Algebra F L],
  (∀ (x : E), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) → Fintype.card (E →ₐ[F] L) = Module.finrank F E
-- Mathlib.Analysis.Calculus.Deriv.Abs
contDiffAt_abs : ∀ {n : ℕ∞} {x : ℝ}, x ≠ 0 → ContDiffAt ℝ (↑n) (fun x => |x|) x
-- Mathlib.Geometry.Euclidean.Incenter
/-- An excenter is equidistant to any two of its touchpoints.  -/
Affine.Simplex.ExcenterExists.dist_excenter_eq_dist_excenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs →
    ∀ (i₁ i₂ : Fin (n + 1)),
      dist (s.excenter signs) (s.touchpoint signs i₁) = dist (s.excenter signs) (s.touchpoint signs i₂)
-- Mathlib.Topology.Algebra.AffineSubspace
AffineSubspace.instIsTopologicalAddTorsorSubtypeMemSubmoduleDirection : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] [IsTopologicalAddTorsor P]
  {s : AffineSubspace R P} [inst_7 : Nonempty ↥s], IsTopologicalAddTorsor ↥s
-- Mathlib.Algebra.Ring.Subring.MulOpposite
/-- Bijection between `MulOpposite` of a subring `S` and its opposite.  -/
Subring.mopRingEquivOp : {R : Type u_2} → [inst : NonAssocRing R] → (S : Subring R) → (↥S)ᵐᵒᵖ ≃+* ↥S.op
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.expand_eval : ∀ {R : Type u} [inst : CommSemiring R] (p : ℕ) (P : Polynomial R) (r : R),
  Polynomial.eval r ((Polynomial.expand R p) P) = Polynomial.eval (r ^ p) P
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.compl_nonempty_of_mk_lt_mk : ∀ {α : Type u} {S : Set α}, Cardinal.mk ↑S < Cardinal.mk α → Sᶜ.Nonempty
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.instSFiniteOfSigmaFinite : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ],
  MeasureTheory.SFinite μ
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- Given maps `f`, `g` from a manifold into a field `𝕜` and `𝕜`-vector space `V`, respectively, the
formula for the `mfderiv` (differential) of their scalar multiplication `f • g`.

Mathematically speaking the formula is `d(f • g) = f • dg + df ⊗ g`, i.e.
`mfderiv% (f • g) x = f x • mfderiv% g x + toSpanSingleton 𝕜 (g x) ∘L mfderiv% f x`,
but this doesn't typecheck because `mfderiv% (f • g) x` and `mfderiv% g x` take values in different
tangent spaces -- respectively the tangent spaces to `V` at `(f • g) x` and `g x`. Of course, both
these tangent spaces can be canonically identified with `V`.

This lemma phrases the formula using the equiv `NormedSpace.fromTangentSpace`, which provides this
canonical identification. (It would also be possible to phrase the formula without this equiv,
instead using casting and definitional abuse.)  -/
_private.Mathlib.Geometry.Manifold.MFDeriv.NormedSpace.0.fromTangentSpace_mfderiv_smul : ∀ {𝕜 : 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] {x : M} {V : Type u_18} [inst_6 : NormedAddCommGroup V]
  [inst_7 : NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V},
  MDiffAt f x →
    MDiffAt g x →
      ↑(NormedSpace.fromTangentSpace ((f • g) x)) ∘SL mfderiv% (f • g) x =
        f x • ↑(NormedSpace.fromTangentSpace (g x)) ∘SL mfderiv% g x +
          ContinuousLinearMap.toSpanSingleton 𝕜 (g x) ∘SL ↑(NormedSpace.fromTangentSpace (f x)) ∘SL mfderiv% f x
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.Equivalent.prod : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} {P : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M₁] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N₁] [inst_4 : AddCommMonoid N₂]
  [inst_5 : AddCommMonoid P] [inst_6 : Module R M₁] [inst_7 : Module R M₂] [inst_8 : Module R N₁] [inst_9 : Module R N₂]
  [inst_10 : Module R P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} {Q₁' : QuadraticMap R N₁ P}
  {Q₂' : QuadraticMap R N₂ P}, Q₁.Equivalent Q₁' → Q₂.Equivalent Q₂' → (Q₁.prod Q₂).Equivalent (Q₁'.prod Q₂')
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffAt.differentiableAt_one : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E}, ContDiffAt 𝕜 1 f x → DifferentiableAt 𝕜 f x
-- Mathlib.NumberTheory.Transcendental.Liouville.Residual
/-- **Alias** of `setOfPred_liouville_eq_iInter_iUnion`. -/
setOf_liouville_eq_iInter_iUnion : {x | Liouville x} = ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), Metric.ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}
-- Mathlib.LinearAlgebra.Dimension.Basic
LinearIndepOn.encard_le_toENat_rank : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R]
  {ι : Type u_1} {v : ι → M} {s : Set ι}, LinearIndepOn R v s → s.encard ≤ Cardinal.toENat (Module.rank R M)
-- Mathlib.Topology.Separation.Hausdorff
lim_eq_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] {f : Filter X} [f.NeBot],
  (∃ x, f ≤ nhds x) → ∀ {x : X}, f.lim = x ↔ f ≤ nhds x
-- Init.Data.Array.Nat
Array.sum_append_nat : ∀ {as₁ as₂ : Array ℕ}, (as₁ ++ as₂).sum = as₁.sum + as₂.sum
-- Mathlib.Data.Sym.Basic
Sym.coe_nil : ∀ {α : Type u_1}, ↑Sym.nil = 0
-- Aesop.Tree.Data
Aesop.NormalizationState.normal.inj : ∀ {postGoal : Lean.MVarId} {postState : Lean.Meta.SavedState}
  {script : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep))} {postGoal_1 : Lean.MVarId}
  {postState_1 : Lean.Meta.SavedState}
  {script_1 : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep))},
  Aesop.NormalizationState.normal postGoal postState script =
      Aesop.NormalizationState.normal postGoal_1 postState_1 script_1 →
    postGoal = postGoal_1 ∧ postState = postState_1 ∧ script = script_1
-- Mathlib.RingTheory.DedekindDomain.Factorization
LinearMap.restrict.eq_1 : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  (f : M →ₛₗ[σ₁₂] M₂) {p : Submodule R M} {q : Submodule R₂ M₂} (hf : ∀ x ∈ p, f x ∈ q),
  f.restrict hf = LinearMap.codRestrict q (f.domRestrict p) ⋯
-- Mathlib.Topology.Order.OrderClosed
/-- For any `a`, the set `[a, +∞)` is closed.  -/
ClosedIciTopology.isClosed_Ici : ∀ {α : Type u_1} {inst : TopologicalSpace α} {inst_1 : Preorder α} [self : ClosedIciTopology α] (a : α),
  IsClosed (Set.Ici a)
-- Init.Data.List.Lemmas
List.insert_of_mem : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, a ∈ l → List.insert a l = l
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.diff₀ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} (h₁ : m₁.WF)
  (h₂ : m₂.WF), (↑(Std.DHashMap.Internal.Raw₀.diff ⟨m₁, ⋯⟩ ⟨m₂, ⋯⟩)).WF
-- Init.Grind.Module.Basic
Lean.Grind.AddCommGroup.neg_zero : ∀ {M : Type u} [inst : Lean.Grind.AddCommGroup M], -0 = 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.two_mul_arctan_sub_pi : ∀ {x : ℝ}, x < -1 → 2 * Real.arctan x = Real.arctan (2 * x / (1 - x ^ 2)) - Real.pi
-- Mathlib.Data.Complex.Basic
Complex.I_mul_I : Complex.I * Complex.I = -1
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.AdicCauchySequence.map_zero : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_3} [inst_3 : AddCommGroup N] [inst_4 : Module R N], AdicCompletion.AdicCauchySequence.map I 0 = 0
-- Init.System.IO
/-- Reads the entire contents of the UTF-8-encoded file at the given path as a `String`.

An exception is thrown if the contents of the file are not valid UTF-8. This is in addition to
exceptions that may always be thrown as a result of failing to read files.
 -/
IO.FS.readFile : System.FilePath → IO String
-- Std.Http.Internal.ChunkedBuffer
/-- Build from an array of ByteArrays directly.
 -/
Std.Http.Internal.ChunkedBuffer.ofArray : Array ByteArray → Std.Http.Internal.ChunkedBuffer
-- Init.Core
/-- `break s` means that `break` was called, meaning that we should exit
from the containing loop  -/
DoResultSBC.break : {α σ : Type u} → σ → DoResultSBC α σ
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
/-- **Alias** of the forward direction of `Matrix.isHyperbolic_neg_iff`. -/
Matrix.IsHyperbolic.of_neg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Preorder R] {m : Matrix (Fin 2) (Fin 2) R},
  (-m).IsHyperbolic → m.IsHyperbolic
-- Mathlib.NumberTheory.Pell
/-- The proof that `a` is a solution to the Pell equation `x^2 - d*y^2 = 1`  -/
Pell.Solution₁.prop : ∀ {d : ℤ} (a : Pell.Solution₁ d), a.x ^ 2 - d * a.y ^ 2 = 1
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
ContDiffWithinAt.log : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E}
  {n : WithTop ℕ∞}, ContDiffWithinAt ℝ n f s x → f x ≠ 0 → ContDiffWithinAt ℝ n (fun x => Real.log (f x)) s x
-- Init.Data.Fin.Lemmas
Fin.sub_ofNat : ∀ {n : ℕ} [inst : NeZero n] (x : Fin n) (y : ℕ), x - Fin.ofNat n y = Fin.ofNat n (n - y % n + ↑x)
-- Init.Data.List.Count
List.count_filter : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {p : α → Bool} {a : α} {l : List α},
  p a = true → List.count a (List.filter p l) = List.count a l
-- Init.Data.List.Monadic
List.zipWithM'_nil_left : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {l : List β} [inst : Monad m]
  {f : α → β → m γ}, List.zipWithM' f [] l = pure []
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.le_join_of_le_left : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q R : l},
  Lean.Order.PartialOrder.rel P Q → Lean.Order.PartialOrder.rel P (Lean.Order.join Q R)
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.val_qsmul : ∀ {R : Type u_1} [inst : Field R] [inst_1 : StarRing R] (q : ℚ) (x : ↥(selfAdjoint R)), ↑(q • x) = q • ↑x
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.instVAddOfVAddAssocClass.eq_1 : ∀ {R : Type u_1} {M : Type u_3} {X : Type u_4} [inst : AddMonoid M] {S : AddSubmonoid M}
  [inst_1 : AddOreLocalization.AddOreSet S] [inst_2 : AddAction M X] [inst_3 : VAdd R X] [inst_4 : VAdd R M]
  [inst_5 : VAddAssocClass R M X] [inst_6 : VAddAssocClass R M M],
  AddOreLocalization.instVAddOfVAddAssocClass = { vadd := AddOreLocalization.hvadd }
-- Mathlib.Analysis.RCLike.Basic
RCLike.imCLM_apply : ∀ {K : Type u_1} [inst : RCLike K], ⇑RCLike.imCLM = ⇑RCLike.im
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv.congr_simp : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p p_1 : α} (e_p : p = p_1) (hp : 0 < p) (a a_1 : α),
  a = a_1 → ∀ (b b_1 : α), b = b_1 → toIocDiv hp a b = toIocDiv ⋯ a_1 b_1
-- Mathlib.RingTheory.IntegralClosure.Algebra.Defs
Algebra.IsIntegral.isIntegral : ∀ {R : Type u_1} {A : Type u_3} {inst : CommRing R} {inst_1 : Ring A} {inst_2 : Algebra R A}
  [self : Algebra.IsIntegral R A] (x : A), IsIntegral R x
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueNum_compl : ∀ {α : Type u_3} {G : SimpleGraph α}, Gᶜ.cliqueNum = G.indepNum
-- Lean.DocString.Types
Lean.Doc.Part.brecOn.go : {i : Type u} →
  {b : Type v} →
    {p : Type w} →
      {motive_1 : Lean.Doc.Part i b p → Sort u_1} →
        {motive_2 : Array (Lean.Doc.Part i b p) → Sort u_1} →
          {motive_3 : List (Lean.Doc.Part i b p) → Sort u_1} →
            (t : Lean.Doc.Part i b p) →
              ((t : Lean.Doc.Part i b p) → t.below → motive_1 t) →
                ((t : Array (Lean.Doc.Part i b p)) → Lean.Doc.Part.below_1 t → motive_2 t) →
                  ((t : List (Lean.Doc.Part i b p)) → Lean.Doc.Part.below_2 t → motive_3 t) → motive_1 t ×' t.below
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.whiskerRight.inj : ∀ {e : Lean.Expr} {isoLift? : Option Mathlib.Tactic.BicategoryLike.IsoLift} {f g : Mathlib.Tactic.BicategoryLike.Mor₁}
  {η : Mathlib.Tactic.BicategoryLike.Mor₂} {h : Mathlib.Tactic.BicategoryLike.Mor₁} {e_1 : Lean.Expr}
  {isoLift?_1 : Option Mathlib.Tactic.BicategoryLike.IsoLift} {f_1 g_1 : Mathlib.Tactic.BicategoryLike.Mor₁}
  {η_1 : Mathlib.Tactic.BicategoryLike.Mor₂} {h_1 : Mathlib.Tactic.BicategoryLike.Mor₁},
  Mathlib.Tactic.BicategoryLike.Mor₂.whiskerRight e isoLift? f g η h =
      Mathlib.Tactic.BicategoryLike.Mor₂.whiskerRight e_1 isoLift?_1 f_1 g_1 η_1 h_1 →
    e = e_1 ∧ isoLift? = isoLift?_1 ∧ f = f_1 ∧ g = g_1 ∧ η = η_1 ∧ h = h_1
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_X_add_C : ∀ {R : Type u} [Nontrivial R] [inst : Semiring R] (a : R), (Polynomial.X + Polynomial.C a).degree = 1
-- Mathlib.Algebra.Lie.Classical
/-- The split-signature diagonal matrix.  -/
LieAlgebra.Orthogonal.S : (l : Type u_4) → (R : Type u₂) → [DecidableEq l] → [CommRing R] → Matrix (l ⊕ l) (l ⊕ l) R
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.Slice.intercalate.match_1.eq_2 : ∀ (motive : List String.Slice → Sort u_1) (a : String.Slice) (as : List String.Slice) (h_1 : Unit → motive [])
  (h_2 : (a : String.Slice) → (as : List String.Slice) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Mathlib.Topology.Algebra.Module.Basic
/-- The topological closure of a closed submodule `s` is equal to `s`.  -/
IsClosed.submodule_topologicalClosure_eq : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : ContinuousConstSMul R M] [inst_5 : ContinuousAdd M] {s : Submodule R M},
  IsClosed ↑s → s.topologicalClosure = s
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
/-- The composition of two pullback functors on sheaves of modules identifies
to the pullback for the composition.  -/
SheafOfModules.pullbackComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {D' : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} D'] →
            {J : CategoryTheory.GrothendieckTopology C} →
              {K : CategoryTheory.GrothendieckTopology D} →
                {F : CategoryTheory.Functor C D} →
                  {S : CategoryTheory.Sheaf J RingCat} →
                    {R : CategoryTheory.Sheaf K RingCat} →
                      [inst_3 : F.IsContinuous J K] →
                        (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) →
                          [inst_4 : (SheafOfModules.pushforward φ).IsRightAdjoint] →
                            {K' : CategoryTheory.GrothendieckTopology D'} →
                              {G : CategoryTheory.Functor D D'} →
                                {R' : CategoryTheory.Sheaf K' RingCat} →
                                  [inst_5 : G.IsContinuous K K'] →
                                    [inst_6 : (F.comp G).IsContinuous J K'] →
                                      (ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K K').obj R') →
                                        [inst_7 : (SheafOfModules.pushforward ψ).IsRightAdjoint] →
                                          (SheafOfModules.pullback φ).comp (SheafOfModules.pullback ψ) ≅
                                            SheafOfModules.pullback
                                              (CategoryTheory.CategoryStruct.comp φ
                                                ((F.sheafPushforwardContinuous RingCat J K).map ψ))
-- Mathlib.FieldTheory.SeparableDegree
Polynomial.natSepDegree_smul_nonzero : ∀ {F : Type u} [inst : Field F] (f : Polynomial F) {x : F}, x ≠ 0 → (x • f).natSepDegree = f.natSepDegree
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.mk_zpow : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Group γ] [inst_3 : IsTopologicalGroup γ] (f : α → γ) (hf : MeasureTheory.AEStronglyMeasurable f μ) (n : ℤ),
  MeasureTheory.AEEqFun.mk f hf ^ n = MeasureTheory.AEEqFun.mk (f ^ n) ⋯