mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- Given an affinely independent family of points, suppose that an affine combination lies in
the span of two points given as affine combinations, and suppose that, for two indices, the
coefficients in the first point in the span are zero and those in the second point in the span
have the same sign. Then the coefficients in the combination lying in the span have the same
sign.  -/
sign_eq_of_affineCombination_mem_affineSpan_pair : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup V] [inst_4 : Module k V] [inst_5 : AddTorsor V P] {ι : Type u_4} {p : ι → P},
  AffineIndependent k p →
    ∀ {w w₁ w₂ : ι → k} {s : Finset ι},
      ∑ i ∈ s, w i = 1 →
        ∑ i ∈ s, w₁ i = 1 →
          ∑ i ∈ s, w₂ i = 1 →
            (Finset.affineCombination k s p) w ∈
                line[k, (Finset.affineCombination k s p) w₁, (Finset.affineCombination k s p) w₂] →
              ∀ {i j : ι},
                i ∈ s →
                  j ∈ s →
                    w₁ i = 0 →
                      w₁ j = 0 → SignType.sign (w₂ i) = SignType.sign (w₂ j) → SignType.sign (w i) = SignType.sign (w j)
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset_eq_empty : ∀ {α : Type u} {s : Set α} {h : s.Finite}, h.toFinset = ∅ ↔ s = ∅
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_add_le_iff_left : ∀ {R : Type u} [inst : Semiring R] {n : ℕ} (p q : Polynomial R),
  q.natDegree ≤ n → ((p + q).natDegree ≤ n ↔ p.natDegree ≤ n)
-- Mathlib.Analysis.Complex.Poisson
/-- Companion theorem to the Poisson Integral Formula: Lower estimate for the real part of the
Herglotz-Riesz kernel.
 -/
le_re_herglotzRieszKernel : ∀ {R : ℝ} {w c z : ℂ},
  z ∈ Metric.sphere c R →
    w ∈ Metric.ball c R → (R - ‖w - c‖) / (R + ‖w - c‖) ≤ ((z - c + (w - c)) / (z - c - (w - c))).re
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.le_mul_ediam_image : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f → ∀ (s : Set α), Metric.ediam s ≤ ↑K * Metric.ediam (f '' s)
-- Mathlib.Order.RelIso.Basic
RelIso.symm_apply_eq : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) {x : β} {y : α},
  e.symm x = y ↔ x = e y
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.disjUnion_boxes : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.TaggedPrepartition I} (h : Disjoint π₁.iUnion π₂.iUnion),
  (π₁.disjUnion π₂ h).boxes = π₁.boxes ∪ π₂.boxes
-- Mathlib.Tactic.NormNum.PowMod
Mathlib.Meta.NormNum.IsNatPowModT.mk : ∀ {p : Prop} {a b m c : ℕ}, (p → (a.pow b).mod m = c) → Mathlib.Meta.NormNum.IsNatPowModT p a b m c
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.natCast_eq_iff : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (x y : ℕ),
  ↑x = ↑y ↔ ↑x = ↑y
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.ppEqcs : optParam Bool true → Lean.Meta.Grind.M✝ Unit
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.hlup : Primrec fun p => Nat.Partrec.Code.lup✝ p.1 p.2.1 p.2.2
-- Mathlib.Algebra.Star.Subalgebra
StarAlgEquiv.ofInjective_apply : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : Semiring B] [inst_6 : Algebra R B] [inst_7 : StarRing B]
  [inst_8 : StarModule R B] (f : A →⋆ₐ[R] B) (hf : Function.Injective ⇑f) (a : A),
  (StarAlgEquiv.ofInjective f hf) a = f.rangeRestrict a
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.List.mapA.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- If a function admits a finite power series expansion bounded by `n`, then it is equal to
the `m`th partial sums of this power series at every point of the disk for `n ≤ m`.  -/
HasFiniteFPowerSeriesOnBall.eq_partialSum : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ},
  HasFiniteFPowerSeriesOnBall f p x n r → ∀ y ∈ Metric.eball 0 r, ∀ (m : ℕ), n ≤ m → f (x + y) = p.partialSum m y
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.superpose_cert : ℤ →
  Lean.Grind.CommRing.Mon →
    Lean.Grind.CommRing.Poly → ℤ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Bool
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrable.neg : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {f : X → E},
  MeasureTheory.LocallyIntegrable f μ → MeasureTheory.LocallyIntegrable (-f) μ
-- Mathlib.Data.Nat.Log
Nat.clog.go.eq_2 : ∀ (n a fuel : ℕ),
  Nat.clog.go n a fuel.succ =
    if n ≤ a then (a / n, 0)
    else
      match Nat.clog.go n (a * a) fuel with
      | (q, e) => if q < a then (q, 2 * e + 1) else (q / a, 2 * e)
-- Mathlib.Topology.LocallyClosed
/-- **Alias** of the reverse direction of `coborder_eq_compl_frontier_iff`. -/
IsOpen.coborder_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsOpen s → coborder s = (frontier s)ᶜ
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.map_coe : ∀ {X Y : TopCat} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑Y),
  ↑((TopologicalSpace.Opens.map f).obj U) = ⇑(CategoryTheory.ConcreteCategory.hom f) ⁻¹' ↑U
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Entry.entry.inj : ∀ {α : Type u} {β : Type v} {σ : Type w} {key : α} {val : β} {key_1 : α} {val_1 : β},
  Lean.PersistentHashMap.Entry.entry key val = Lean.PersistentHashMap.Entry.entry key_1 val_1 →
    key = key_1 ∧ val = val_1
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.tsupport_extend_zero : ∀ {α : Type u_2} {α' : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace α']
  [inst_2 : Zero β] {f : α → β} [T2Space α'],
  HasCompactSupport f →
    ∀ {g : α → α'}, Continuous g → Function.Injective g → tsupport (Function.extend g f 0) = g '' tsupport f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, k ∈ t₂ → (t₁ \ t₂).getKeyD k fallback = fallback
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.range_eq_top_iff : ∀ {X Y : SSet} (f : X ⟶ Y), SSet.Subcomplex.range f = ⊤ ↔ CategoryTheory.Epi f
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgEquiv.trdeg_eq : ∀ {R : Type u_2} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {A' : Type v}
  [inst_3 : CommRing A'] [inst_4 : Algebra R A'] (e : A ≃ₐ[R] A'), Algebra.trdeg R A = Algebra.trdeg R A'
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop_f : ∀ {R : CommRingCat} {ι : Type u_1} (s : ι → ↑R) (hs : Ideal.span (Set.range s) = ⊤) (i : ι),
  (AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop s hs).f i =
    AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away (s i))))
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.eval_smul : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [inst_12 : IsOrderedAddMonoid R] [inst_13 : Archimedean R] (k : K) (x : M), f.eval (k • x) = k • f.eval x
-- Mathlib.Algebra.Order.ToIntervalMod
left_le_toIcoMod : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), a ≤ toIcoMod hp a b
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.copy_eq : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B] (f : A →⋆ₐ[R] B) (f' : A → B)
  (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.Data.Nat.Sqrt
Nat.sqrt_eq_zero : ∀ {n : ℕ}, n.sqrt = 0 ↔ n = 0
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- A purely inseparable extension has inseparable degree equal to degree.  -/
IsPurelyInseparable.insepDegree_eq : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [IsPurelyInseparable F E],
  Field.insepDegree F E = Module.rank F E
-- Mathlib.Order.CompleteLattice.Defs
OrderDual.supSet.eq_1 : ∀ (α : Type u_8) [h : InfSet α], OrderDual.supSet α = { sSup := fun s => sInf s }
-- Mathlib.Algebra.Polynomial.Div
Polynomial.modByMonic_one : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R), p %ₘ 1 = 0
-- Mathlib.Order.Atoms
IsAtom.disjoint_of_ne : ∀ {α : Type u_2} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α}, IsAtom a → IsAtom b → a ≠ b → Disjoint a b
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.isPrime_iff_of_isPrincipalIdealRing : ∀ {α : Type u} [inst : CommSemiring α] [IsPrincipalIdealRing α] {P : Ideal α},
  P ≠ ⊥ → (P.IsPrime ↔ ∃ p, Prime p ∧ P = Ideal.span {p})
-- Std.Data.Internal.List.Associative
Std.Internal.List.le_minKey! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {k : α},
        (compare k (Std.Internal.List.minKey! l)).isLE = true ↔
          ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k k').isLE = true
-- Mathlib.Order.Std
Std.LawfulOrderCmp.compareOfLessAndEq : ∀ (α : Type u_1) [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] [inst_4 : DecidableEq α]
  [inst_5 : DecidableLT α], Std.LawfulOrderCmp fun a b => compareOfLessAndEq a b
-- Init.Core
id_def : ∀ {α : Sort u} (a : α), id a = a
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.of_semiconj : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β} {ga : α → α} {gb : β → β},
  MeasureTheory.MeasurePreserving f μa μb →
    MeasureTheory.MeasurePreserving ga μa μa →
      Function.Semiconj f ga gb → Measurable gb → MeasureTheory.MeasurePreserving gb μb μb
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.zero_ne_top : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R], 0 ≠ ⊤
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.ιMulti_family_mul_of_not_disjoint : ∀ (R : Type u1) [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {m n : ℕ}
  {I : Type u_1} [inst_3 : LinearOrder I] (v : I → M) (s : ↑(Set.powersetCard I m)) (t : ↑(Set.powersetCard I n)),
  ¬Disjoint ↑s ↑t → ExteriorAlgebra.ιMulti_family R m v s * ExteriorAlgebra.ιMulti_family R n v t = 0
-- Init.Data.Nat.Lemmas
Nat.le_of_pred_lt : ∀ {n : ℕ} {m : ℕ}, m.pred < n → m ≤ n
-- Mathlib.Computability.NFA
DFA.toNFA_accept : ∀ {α : Type u} {σ : Type v} (M : DFA α σ), M.toNFA.accept = M.accept
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.dualAnnihilator_sup_eq : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (U V : Submodule R M), (U ⊔ V).dualAnnihilator = U.dualAnnihilator ⊓ V.dualAnnihilator
-- Mathlib.NumberTheory.Padics.WithVal
Padic.coe_withValRingEquiv : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)],
  ⇑Padic.withValRingEquiv = UniformSpace.Completion.extension (Rat.cast ∘ ⇑(WithVal.equiv (Rat.padicValuation p)))
-- Lean.Data.Lsp.Ipc
_private.Lean.Data.Lsp.Ipc.0.Lean.Lsp.Ipc.expandModuleHierarchyImports.go : ℕ → Lean.Lsp.LeanImport → Std.TreeSet String compare → Lean.Lsp.Ipc.IpcM (Lean.Lsp.Ipc.ModuleHierarchy × ℕ)
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- An n-ary version of `Set.add_subset_add`.  -/
Set.multiset_sum_subset_multiset_sum : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] (t : Multiset ι) (f₁ f₂ : ι → Set α),
  (∀ i ∈ t, f₁ i ⊆ f₂ i) → (Multiset.map f₁ t).sum ⊆ (Multiset.map f₂ t).sum
-- Mathlib.CategoryTheory.Category.Pointed
/-- The identity morphism of `X : Pointed`.  -/
Pointed.Hom.id : (X : Pointed) → X.Hom X
-- Mathlib.ModelTheory.Semantics
/-- List.foldr on BoundedFormula.imp gives a big "And" of input conditions.  -/
FirstOrder.Language.BoundedFormula.realize_foldr_imp : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {k : ℕ} (l : List (L.BoundedFormula α k))
  (f : L.BoundedFormula α k) (v : α → M) (xs : Fin k → M),
  (List.foldr FirstOrder.Language.BoundedFormula.imp f l).Realize v xs = ((∀ i ∈ l, i.Realize v xs) → f.Realize v xs)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_filterMap! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Std.TransOrd α] {f : α → β → Option γ} {k : α} (h : t.WF)
  {h' : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filterMap! f t) = true},
  Std.DTreeMap.Internal.Impl.Const.get (Std.DTreeMap.Internal.Impl.filterMap! f t) k h' =
    (f (t.getKey k ⋯) (Std.DTreeMap.Internal.Impl.Const.get t k ⋯)).get ⋯
-- Mathlib.GroupTheory.Coxeter.Matrix
CoxeterMatrix.isSymm : ∀ {B : Type u_1} (self : CoxeterMatrix B), self.M.IsSymm
-- Mathlib.Algebra.Order.Archimedean.Basic
OrderDual.instMulArchimedean : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : PartialOrder G] [IsOrderedMonoid G] [MulArchimedean G],
  MulArchimedean Gᵒᵈ
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_nat : Cardinal.mk ℕ = Cardinal.aleph0
-- Mathlib.Algebra.Lie.Ideal
/-- Transfer the `LieModule` instance from the coercion `LieIdeal → LieSubalgebra`.  -/
LieIdeal.lieModule : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : LieAlgebra R L] [LieModule R L M] (I : LieIdeal R L),
  LieModule R (↥I) M
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
/-- Homomorphic image of an integral algebra is an integral algebra.  -/
Algebra.IsIntegral.of_surjective : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_5} {B : Type u_6} [inst_1 : Ring A] [inst_2 : Ring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [Algebra.IsIntegral R A] (f : A →ₐ[R] B),
  Function.Surjective ⇑f → Algebra.IsIntegral R B
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.toContinuousLinearMap_comp : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  [inst_10 : AddCommGroup U] [inst_11 : Module R U] [inst_12 : TopologicalSpace U] [inst_13 : IsTopologicalAddGroup U]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} {π₃ : ContRepresentation R G U}
  (f : ContIntertwiningMap π₂ π₃) (g : ContIntertwiningMap π₁ π₂),
  (f.comp g).toContinuousLinearMap = f.toContinuousLinearMap ∘SL g.toContinuousLinearMap
-- Mathlib.Data.String.Lemmas
String.congr_append : ∀ (a b : String), a ++ b = String.ofList (a.toList ++ b.toList)
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_atBot_atBot : ∀ {α : Type u_3} {β : Type u_4} [Nonempty α] [inst : Preorder α] [IsCodirectedOrder α] {f : α → β}
  [inst_2 : Preorder β], Filter.Tendsto f Filter.atBot Filter.atBot ↔ ∀ (b : β), ∃ i, ∀ a ≤ i, f a ≤ b
-- Mathlib.Data.Complex.Basic
Complex.ofReal_comp_mul : ∀ {α : Type u_1} (f g : α → ℝ), Complex.ofReal ∘ (f * g) = Complex.ofReal ∘ f * Complex.ofReal ∘ g
-- Lean.Data.JsonRpc
Lean.JsonRpc.ResponseError.id : {α : Type u} → Lean.JsonRpc.ResponseError α → Lean.JsonRpc.RequestID
-- Mathlib.Order.InitialSeg
InitialSeg.instRelHomClass : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, RelHomClass (InitialSeg r s) r s
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.ClassifyResult.commRing.inj : ∀ {id id_1 : ℕ},
  Lean.Meta.Sym.Arith.ClassifyResult.commRing id = Lean.Meta.Sym.Arith.ClassifyResult.commRing id_1 → id = id_1
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.map_inv : ∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : Aˣ),
  (spectrum 𝕜 ↑a)⁻¹ = spectrum 𝕜 ↑a⁻¹
-- Aesop.Search.Expansion.Simp
Aesop.SimpResult.solved.injEq : ∀ (usedTheorems usedTheorems_1 : Lean.Meta.Simp.UsedSimps),
  (Aesop.SimpResult.solved usedTheorems = Aesop.SimpResult.solved usedTheorems_1) = (usedTheorems = usedTheorems_1)
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
/-- The quotient functor from the category of bifibrant objects to its
homotopy category.  -/
HomotopicalAlgebra.BifibrantObject.toHoCat : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      CategoryTheory.Functor (HomotopicalAlgebra.BifibrantObject C) (HomotopicalAlgebra.BifibrantObject.HoCat C)
-- Mathlib.NumberTheory.ModularForms.Petersson
UpperHalfPlane.petersson_norm_symm : ∀ (k : ℤ) (f f' : UpperHalfPlane → ℂ) (τ : UpperHalfPlane),
  ‖UpperHalfPlane.petersson k f' f τ‖ = ‖UpperHalfPlane.petersson k f f' τ‖
-- Mathlib.SetTheory.Ordinal.Univ
/-- The ordinal `univ.{u, v}` is the order type of `Ordinal.{u}` or `Cardinal.{u}`, as an element of
`Ordinal.{v}` (when `u < v`).  -/
Ordinal.univ : Ordinal.{max (u + 1) v}
-- Mathlib.Data.Finmap
Finmap.mem_toFinmap : ∀ {α : Type u} {β : α → Type v} {a : α} {s : AList β}, a ∈ s.toFinmap ↔ a ∈ s
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.IsBilimit.total : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J : Type u_1}
  [inst_2 : Fintype J] {f : J → C} {b : CategoryTheory.Limits.Bicone f} (i : b.IsBilimit),
  ∑ j, CategoryTheory.CategoryStruct.comp (b.π j) (b.ι j) = CategoryTheory.CategoryStruct.id b.pt
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.SymbolPriorityEntry.declName : Lean.Meta.Grind.SymbolPriorityEntry → Lean.Name
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mopMopEquivalenceInverseMonoidal_δ_unmop_unmop : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  (CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.MonoidalOpposite.mopMopEquivalence C).inverse X
          Y).unmop.unmop =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Mathlib.Algebra.BigOperators.Finprod
finprod_eq_mulIndicator_apply : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (s : Set α) (f : α → M) (a : α),
  ∏ᶠ (_ : a ∈ s), f a = s.mulIndicator f a
-- Init.Data.List.Nat.Sublist
List.suffix_iff_getElem : ∀ {α : Type u_1} {l₁ l₂ : List α},
  l₁ <:+ l₂ ↔ ∃ (x : l₁.length ≤ l₂.length), ∀ (i : ℕ) (x_1 : i < l₁.length), l₂[i + l₂.length - l₁.length] = l₁[i]
-- Mathlib.CategoryTheory.Comma.Over.StrictInitial
CategoryTheory.underEquivOfIsTerminal_inverse : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X),
  (CategoryTheory.underEquivOfIsTerminal.{w, v_1, u_1} X h).inverse =
    CategoryTheory.Functor.fromPUnit (CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.id X))
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_le_rpow_of_exponent_le : ∀ {x : NNReal} {y z : ℝ}, 1 ≤ x → y ≤ z → x ^ y ≤ x ^ z
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂Hom_zero'_apply : ∀ {R : Type u} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₂] (f : R →+* S₂)
  (p : MvPolynomial σ R), (MvPolynomial.eval₂Hom f fun x => 0) p = f (MvPolynomial.constantCoeff p)
-- Mathlib.Algebra.BigOperators.Finprod
finsum_dmem : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {s : Set α} [inst_1 : DecidablePred fun x => x ∈ s]
  (f : (a : α) → a ∈ s → M), ∑ᶠ (a : α) (h : a ∈ s), f a h = ∑ᶠ (a : α) (_ : a ∈ s), if h' : a ∈ s then f a h' else 0
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.prodInverse_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (S : CategoryTheory.Functor C D) (S' : CategoryTheory.Functor C' D')
  (T : D) (T' : D') {X Y : CategoryTheory.CostructuredArrow S T × CategoryTheory.CostructuredArrow S' T'} (η : X ⟶ Y),
  (CategoryTheory.CostructuredArrow.prodInverse S S' T T').map η =
    CategoryTheory.CostructuredArrow.homMk (η.1.left, η.2.left) ⋯
-- Init.Meta.Defs
Lean.Meta.instReprTransparencyMode : Repr Lean.Meta.TransparencyMode
-- Mathlib.Order.GaloisConnection.Basic
GaloisCoinsertion.isGLB_of_l_image : ∀ {α : Type u} {β : Type v} {u : α → β} {l : β → α} [inst : Preorder α] [inst_1 : Preorder β]
  (gi : GaloisCoinsertion l u) {s : Set β} {a : α}, IsGLB (l '' s) a → IsGLB s (u a)
-- Mathlib.RingTheory.Jacobson.Ideal
/-- An ideal `I` of `R` is equal to its Jacobson radical if and only if
the Jacobson radical of the quotient ring `R/I` is the zero ideal  -/
Ideal.jacobson_eq_iff_jacobson_quotient_eq_bot : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R}, I.jacobson = I ↔ ⊥.jacobson = ⊥
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.preEquivalence.functor_obj_right_as : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e)
  (g : CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.pre F G e) f),
  ((CategoryTheory.CostructuredArrow.preEquivalence.functor F f).obj g).right.as = PUnit.unit
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_uIcc_cast : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a b : Fin n),
  ∑ i ∈ Finset.uIcc (Fin.cast h a) (Fin.cast h b), f i = ∑ i ∈ Finset.uIcc a b, f (Fin.cast h i)
-- Mathlib.NumberTheory.Pell
/-- If there is a fundamental solution, it is unique.  -/
Pell.IsFundamental.subsingleton : ∀ {d : ℤ} {a b : Pell.Solution₁ d}, Pell.IsFundamental a → Pell.IsFundamental b → a = b
-- Init.Data.Format.Basic
Std.Format.align.sizeOf_spec : ∀ (force : Bool), sizeOf (Std.Format.align force) = 1 + sizeOf force
-- Mathlib.Order.RelIso.Basic
RelIso.trans_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f₁ : r ≃r s)
  (f₂ : s ≃r t) (a : α), (f₁.trans f₂) a = f₂ (f₁ a)
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
ModuleCat.FilteredColimits.M.mk_map : ∀ {R : Type u} [inst : Ring R] {J : Type v} [inst_1 : CategoryTheory.SmallCategory J]
  [inst_2 : CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCat R)) {j k : J} (f : j ⟶ k)
  (x : ↑(F.obj j)),
  ModuleCat.FilteredColimits.M.mk F ⟨k, (CategoryTheory.ConcreteCategory.hom (F.map f)) x⟩ =
    ModuleCat.FilteredColimits.M.mk F ⟨j, x⟩
-- Mathlib.Order.Basic
forall_gt_imp_ge_iff_le_of_dense : ∀ {α : Type u_2} [inst : LinearOrder α] [DenselyOrdered α] {a₁ a₂ : α}, (∀ (a : α), a₂ < a → a₁ ≤ a) ↔ a₁ ≤ a₂