mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient
/-- `Submodule.liftQ` as a `ContinuousLinearMap`.  -/
Submodule.liftQL : {R : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring R₂] →
        {σ : R →+* R₂} →
          {M : Type u_3} →
            {M₂ : Type u_4} →
              [inst_2 : TopologicalSpace M] →
                [inst_3 : AddCommGroup M] →
                  [inst_4 : Module R M] →
                    [inst_5 : TopologicalSpace M₂] →
                      [inst_6 : AddCommGroup M₂] →
                        [inst_7 : Module R₂ M₂] →
                          (S : Submodule R M) → (f : M →SL[σ] M₂) → S ≤ (↑f).ker → M ⧸ S →SL[σ] M₂
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
SSet.Augmented.StandardSimplex.nonempty_extraDegeneracy_stdSimplex : ∀ (Δ : SimplexCategory),
  Nonempty (CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy (SSet.Augmented.stdSimplex.obj Δ))
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.inner_sub_left : ∀ {A : Type u_1} {E : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ A] [inst_4 : Module ℂ E] [inst_5 : PartialOrder A] [inst_6 : SMul A E] [inst_7 : Norm A]
  [inst_8 : Norm E] [inst_9 : CStarModule A E] [StarModule ℂ A] {x y z : E},
  inner A (x - y) z = inner A x z - inner A y z
-- Mathlib.MeasureTheory.Function.Jacobian
MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv_aux1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure],
  MeasurableSet s →
    (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
      ∀ {ε : NNReal}, 0 < ε → μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑ε * μ s
-- Init.Data.Nat.Basic
Nat.sub_self_add : ∀ (n m : ℕ), n - (n + m) = 0
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- Given a short complex `S` such that `S.HasHomology`, this is the canonical
homology data for `S` whose `left.K`, `left/right.H` and `right.Q` fields are
respectively `S.cycles`, `S.homology` and `S.opcycles`.  -/
CategoryTheory.ShortComplex.HomologyData.canonical : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [S.HasHomology] → S.HomologyData
-- Mathlib.Algebra.Group.Hom.Defs
/-- `AddMonoidHomClass F M N` states that `F` is a type of `AddZero`-preserving
homomorphisms.

You should also extend this typeclass when you extend `AddMonoidHom`.
 -/
AddMonoidHomClass : (F : Type u_10) →
  (M : outParam (Type u_11)) → (N : outParam (Type u_12)) → [AddZero M] → [AddZero N] → [FunLike F M N] → Prop
-- Mathlib.Order.Defs.PartialOrder
Decidable.lt_or_eq_of_le : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α} [DecidableLE α], a ≤ b → a < b ∨ a = b
-- Mathlib.Topology.MetricSpace.Gluing
Metric.toGlueL.eq_1 : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : Nonempty Z] [inst_1 : MetricSpace Z] [inst_2 : MetricSpace X]
  [inst_3 : MetricSpace Y] {Φ : Z → X} {Ψ : Z → Y} (hΦ : Isometry Φ) (hΨ : Isometry Ψ) (x : X),
  Metric.toGlueL hΦ hΨ x = Quotient.mk'' (Sum.inl x)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.penultimate_mem_dropLast_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, ¬p.Nil → p.penultimate ∈ p.support.dropLast
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.instDecidableRelAdjMulCayleyOfFintypeOfDecidableEqOfDecidablePredMemSet : {M : Type u_1} →
  (s : Set M) →
    [inst : Mul M] →
      [Fintype M] → [DecidableEq M] → [DecidablePred fun x => x ∈ s] → DecidableRel (SimpleGraph.mulCayley s).Adj
-- Init.Data.List.OfFn
List.ofFn_getElem : ∀ {α : Type u_1} {xs : List α}, (List.ofFn fun i => xs[↑i]) = xs
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
/-- Right `wrap` cancellation theorem of the form
```
toInt a = a' → toInt b = i.wrap b' → toInt (a ⊞ b) = i.wrap (a' ⊞ b')
```
 -/
Lean.Meta.Grind.Arith.Cutsat.ToIntThms.c_wr? : Lean.Meta.Grind.Arith.Cutsat.ToIntThms → Option Lean.Expr
-- Mathlib.RingTheory.Trace.Basic
trace_eq_sum_embeddings : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (E : Type u_7)
  [inst_3 : Field E] [inst_4 : Algebra K E] [IsAlgClosed E] [inst_6 : FiniteDimensional K L] [Algebra.IsSeparable K L]
  {x : L}, (algebraMap K E) ((Algebra.trace K L) x) = ∑ σ, σ x
-- Mathlib.Order.RelClasses
/-- A well-founded relation. Not to be confused with `IsWellOrder`.  -/
IsWellFounded : (α : Type u) → (α → α → Prop) → Prop
-- Mathlib.RepresentationTheory.Tannaka
TannakaDuality.FiniteGroup.leftRegular_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (s t : G) (f : G → k),
  (TannakaDuality.FiniteGroup.leftRegular s) f t = f (s⁻¹ * t)
-- Init.Data.Iterators.Combinators.Monadic.Take
Std.Iterators.Types.Take.instIterator : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} → [Monad m] → [inst : Std.Iterator α m β] → Std.Iterator (Std.Iterators.Types.Take α m) m β
-- Lean.Meta.Tactic.Util
Lean.Meta.appendTag : Lean.Name → Lean.Name → Lean.Name
-- Mathlib.Analysis.Convex.Extreme
extremePoints_singleton : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {x : E}, Set.extremePoints 𝕜 {x} = {x}
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_eq_blsub : ∀ (o : Ordinal.{u}) (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}),
  (o.bsup fun a ha => Order.succ (f a ha)) = o.blsub f
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.neg_add_eq_iff_eq_add : ∀ {α : Type u} [inst : SubtractionMonoid α] {a b c : α}, IsAddUnit a → (-a + b = c ↔ b = a + c)
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeffHom_apply : ∀ {R : Type u} [inst : Semiring R] [inst_1 : NoZeroDivisors R] (p : Polynomial R),
  Polynomial.leadingCoeffHom p = p.leadingCoeff
-- Mathlib.Data.Set.Lattice
Set.iUnion₂_subset : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} {t : Set α},
  (∀ (i : ι) (j : κ i), s i j ⊆ t) → ⋃ i, ⋃ j, s i j ⊆ t
-- Lean.ScopedEnvExtension
Lean.SimpleScopedEnvExtension.Descr.mk.injEq : ∀ {α σ : Type} (name : autoParam Lean.Name Lean.SimpleScopedEnvExtension.Descr.name._autoParam) (addEntry : σ → α → σ)
  (initial : σ) (finalizeImport : σ → σ) (exportEntry? : Lean.Environment → α → Lean.OLeanEntries (Option α))
  (name_1 : autoParam Lean.Name Lean.SimpleScopedEnvExtension.Descr.name._autoParam) (addEntry_1 : σ → α → σ)
  (initial_1 : σ) (finalizeImport_1 : σ → σ) (exportEntry?_1 : Lean.Environment → α → Lean.OLeanEntries (Option α)),
  ({ name := name, addEntry := addEntry, initial := initial, finalizeImport := finalizeImport,
        exportEntry? := exportEntry? } =
      { name := name_1, addEntry := addEntry_1, initial := initial_1, finalizeImport := finalizeImport_1,
        exportEntry? := exportEntry?_1 }) =
    (name = name_1 ∧
      addEntry = addEntry_1 ∧ initial = initial_1 ∧ finalizeImport = finalizeImport_1 ∧ exportEntry? = exportEntry?_1)
-- Init.Data.Repr
Sum.repr : {α : Type u_1} → {β : Type u_2} → [Repr α] → [Repr β] → α ⊕ β → ℕ → Std.Format
-- Mathlib.Algebra.Group.Semiconj.Basic
SemiconjBy.inv_symm_left_iff : ∀ {G : Type u_1} [inst : Group G] {a x y : G}, SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
AlgebraicGeometry.Smooth.exists_isStandardSmooth : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Smooth f] (x : ↥X),
  ∃ U,
    ∃ (_ : AlgebraicGeometry.IsAffineOpen U),
      ∃ V,
        ∃ (_ : AlgebraicGeometry.IsAffineOpen V) (_ : x ∈ V) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).IsStandardSmooth
-- Mathlib.Data.Multiset.MapFold
Multiset.foldr_add : ∀ {α : Type u_1} {β : Type v} (f : α → β → β) [inst : LeftCommutative f] (b : β) (s t : Multiset α),
  Multiset.foldr f b (s + t) = Multiset.foldr f (Multiset.foldr f b t) s
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- A version of `QuadraticMap.associated_isSymm` for general targets
(using `flip` because `IsSymm` does not apply here).  -/
QuadraticMap.associated_flip : ∀ (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : CommSemiring S] [inst_6 : Algebra S R]
  [inst_7 : Module S N] [inst_8 : IsScalarTower S R N] [inst_9 : Invertible 2] (Q : QuadraticMap R M N),
  LinearMap.flip ((QuadraticMap.associatedHom S) Q) = (QuadraticMap.associatedHom S) Q
-- Init.Data.UInt.Lemmas
UInt8.ne_of_toBitVec_ne : ∀ {a b : UInt8}, a.toBitVec ≠ b.toBitVec → a ≠ b
-- Mathlib.Data.List.OfFn
List.find?_ofFn_eq_some : ∀ {α : Type u} {n : ℕ} {f : Fin n → α} {p : α → Bool} {b : α},
  List.find? p (List.ofFn f) = some b ↔ p b = true ∧ ∃ i, f i = b ∧ ∀ j < i, ¬p (f j) = true
-- Aesop.Script.Check
Aesop.checkRenderedScriptIfEnabled : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq → Lean.Meta.SavedState → Lean.MVarId → Bool → Lean.MetaM Unit
-- Init.Data.String.Iterate
String.Slice.PosIterator.mk : {s : String.Slice} → s.Pos → s.PosIterator
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.card_support_binomial : ∀ {R : Type u} [inst : Semiring R] {k m : ℕ},
  k ≠ m →
    ∀ {x y : R},
      x ≠ 0 → y ≠ 0 → (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m).support.card = 2
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.trunc_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J]
  [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] [inst_5 : WellFoundedLT J] {j : J} (iter : Φ.Iteration j)
  {j' : J} (hj' : j' ≤ j), (iter.trunc hj').F = CategoryTheory.SmallObject.restrictionLE iter.F hj'
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {a : α} [inst : Inhabited α], ∅.getKey! a = default
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasNegAssignment : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Bool
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Negating the orientation negates the value of `oangle`.  -/
Orientation.oangle_neg_orientation_eq_neg : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), (-o).oangle x y = -o.oangle x y
-- Mathlib.Data.Multiset.Filter
Multiset.filter_add : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s t : Multiset α),
  Multiset.filter p (s + t) = Multiset.filter p s + Multiset.filter p t
-- Mathlib.Order.Cover
CovBy.image : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a b : α} (f : α ↪o β),
  a ⋖ b → (Set.range ⇑f).OrdConnected → f a ⋖ f b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.hp₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
  (h : CategoryTheory.Limits.ChosenPullback f₁ f₂), CategoryTheory.CategoryStruct.comp h.p₂ f₂ = h.p
-- Mathlib.Algebra.GroupWithZero.ULift
ULift.commMonoidWithZero : {α : Type u} → [CommMonoidWithZero α] → CommMonoidWithZero (ULift.{u_1, u} α)
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.isOpen_iff : ∀ {s : Set Ordinal.{u}}, IsOpen s ↔ ∀ o ∈ s, Order.IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s
-- Lean.Elab.Tactic.Omega.Core
/-- Helper function for adding an equality of the form `const + Coeffs.dot coeffs atoms = 0`
to a `Problem`.

(This is only used while initializing a `Problem`. During elimination we use `addConstraint`.)
 -/
Lean.Elab.Tactic.Omega.Problem.addEquality : Lean.Elab.Tactic.Omega.Problem →
  ℤ → Lean.Omega.Coeffs → Option Lean.Elab.Tactic.Omega.Proof → Lean.Elab.Tactic.Omega.Problem
-- Mathlib.Analysis.ConstantSpeed
has_unit_speed_naturalParameterization : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) {s : Set α},
  LocallyBoundedVariationOn f s →
    ∀ {a : α}, a ∈ s → HasUnitSpeedOn (naturalParameterization f s a) (variationOnFromTo f s a '' s)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.cpow_ofReal : ∀ (x : ℂ) (y : ℝ), x ^ ↑y = ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * Complex.I)
-- Mathlib.GroupTheory.Subgroup.Center
ConjClasses.mk_bijOn : ∀ (G : Type u_2) [inst : Group G], Set.BijOn ConjClasses.mk (↑(Subgroup.center G)) (ConjClasses.noncenter G)ᶜ
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- A multiseries `ms` is `Sorted` when the exponents at each of its levels are sorted.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted : {basis_hd : ℝ → ℝ} →
  {basis_tl : Tactic.ComputeAsymptotics.Basis} →
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl → Prop
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.rel.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (W : ℤ → R) (p q r s : ℤ),
  IsEllipticNet.rel W p q r s =
    W (p + q + s) * W (p - q) * W (r + s) * W r - W (p + r + s) * W (p - r) * W (q + s) * W q +
      W (q + r + s) * W (q - r) * W (p + s) * W p
-- Mathlib.ModelTheory.Algebra.Ring.Basic
/-- The constant `1` in the `Language.ring.Structure` is the same as the constant given by the
`One` instance  -/
FirstOrder.Ring.CompatibleRing.funMap_one : ∀ {R : Type u_2} {inst : Add R} {inst_1 : Mul R} {inst_2 : Neg R} {inst_3 : One R} {inst_4 : Zero R}
  [self : FirstOrder.Ring.CompatibleRing R] (x : Fin 0 → R),
  FirstOrder.Language.Structure.funMap FirstOrder.Ring.oneFunc x = 1
-- Mathlib.Topology.Order.WithTop
WithBot.continuousOn_unbotD : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] (d : ι),
  ContinuousOn (WithBot.unbotD d) {a | a ≠ ⊥}
-- Std.Data.Iterators.Lemmas.Producers.Slice
Std.Slice.count_iter_eq_size : ∀ {γ : Type u_1} {α β : Type u_2} [inst : Std.ToIterator (Std.Slice γ) Id α β] [inst_1 : Std.Iterator α Id β]
  {s : Std.Slice γ} [Std.Iterators.Finite α Id] [inst_3 : Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id]
  [inst_5 : Std.Slice.SliceSize γ] [Std.Slice.LawfulSliceSize γ], s.iter.length = s.size
-- Std.Data.ByteSlice
instSliceableByteSliceNat_5 : Std.Roi.Sliceable ByteSlice ℕ ByteSlice
-- Mathlib.Geometry.Manifold.IntegralCurve.Basic
IsMIntegralCurve.isMIntegralCurveOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x}, IsMIntegralCurve γ v → ∀ (s : Set ℝ), IsMIntegralCurveOn γ v s
-- Std.Sat.AIG.Lemmas
/-- The AIG produced by `AIG.mkConst` agrees with the input AIG on all indices that are valid for both.
 -/
Std.Sat.AIG.mkConst_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (val : Bool) (idx : ℕ)
  {h : idx < aig.decls.size},
  have this := ⋯;
  (aig.mkConst val).aig.decls[idx] = aig.decls[idx]
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cos_three_mul : ∀ (x : ℂ), Complex.cos (3 * x) = 4 * Complex.cos x ^ 3 - 3 * Complex.cos x
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_radical_of_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  Function.Surjective ⇑f → ∀ {I : Ideal R}, RingHom.ker f ≤ I → Ideal.map f I.radical = (Ideal.map f I).radical
-- Mathlib.LinearAlgebra.Dual.Lemmas
LinearMap.dualMap_surjective_of_injective : ∀ {K : Type u_3} {V₁ : Type u_4} {V₂ : Type u_5} [inst : Field K] [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {f : V₁ →ₗ[K] V₂},
  Function.Injective ⇑f → Function.Surjective ⇑f.dualMap
-- Lean.Data.Lsp.Internal
/-- End character of the range of this location.  -/
Lean.Lsp.RefInfo.Location.endPosCharacter : Lean.Lsp.RefInfo.Location → ℕ
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.identEq.formatter : Lean.Name → Lean.PrettyPrinter.Formatter
-- Mathlib.AlgebraicTopology.ModelCategory.Over
HomotopicalAlgebra.weakEquivalences_over_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C)
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C],
  HomotopicalAlgebra.weakEquivalences (CategoryTheory.Over S) = (HomotopicalAlgebra.weakEquivalences C).over
-- Mathlib.Algebra.Order.Floor.Div
/-- Typeclass for division rounded down. For each `a > 0`, this asserts the existence of a right
adjoint to the map `b ↦ a • b : β → β`.  -/
FloorDiv : (α : Type u_2) →
  (β : Type u_3) →
    [AddCommMonoid α] →
      [PartialOrder α] → [inst : AddCommMonoid β] → [PartialOrder β] → [SMulZeroClass α β] → Type (max u_2 u_3)
-- Mathlib.Tactic.NormNum.Basic
/-- The `norm_num` extension which identifies expressions of the form `a + b`,
such that `norm_num` successfully recognises both `a` and `b`.  -/
Mathlib.Meta.NormNum.evalAdd : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.CategoryTheory.Subfunctor.Subobject
CategoryTheory.Subfunctor.equivalenceMonoOver_functor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w))
  {A B : CategoryTheory.Subfunctor F} (f : A ⟶ B),
  (CategoryTheory.Subfunctor.equivalenceMonoOver F).functor.map f =
    CategoryTheory.MonoOver.homMk (CategoryTheory.Subfunctor.homOfLe ⋯) ⋯
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.continuousOn_log : ContinuousOn Real.log {0}ᶜ
-- Mathlib.LinearAlgebra.Projectivization.Independence
/-- A family of points in a projective space is independent if and only if the representative
vectors determined by the family are linearly independent.  -/
Projectivization.independent_iff : ∀ {ι : Type u_1} {K : Type u_2} {V : Type u_3} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {f : ι → Projectivization K V}, Projectivization.Independent f ↔ LinearIndependent K (Projectivization.rep ∘ f)
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.WSeq.drop.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Geometry.Manifold.ContMDiffMap
ContMDiffMap.coeFn_mk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {H' : Type u_5} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞} (f : M → M')
  (hf : ContMDiff I I' n f), ⇑⟨f, hf⟩ = f
-- Mathlib.Algebra.GroupWithZero.Basic
inv_mul_cancel_right₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {b : G₀}, b ≠ 0 → ∀ (a : G₀), a * b⁻¹ * b = a
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- `3α + β` is long.  -/
RootPairing.EmbeddedG2.threeShortAddLongRoot_longRoot : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.EmbeddedG2] (B : P.InvariantForm),
  (B.form (RootPairing.EmbeddedG2.threeShortAddLongRoot P)) (RootPairing.EmbeddedG2.threeShortAddLongRoot P) =
    (B.form (RootPairing.EmbeddedG2.longRoot P)) (RootPairing.EmbeddedG2.longRoot P)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for unsigned division of `BitVec`s.  -/
BitVec.reduceUDiv : Lean.Meta.Simp.DSimproc
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.id_s₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {i j : E.I₀}
  (a : E.I₁ i j), (CategoryTheory.PreOneHypercover.Hom.id E).s₁ a = a
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.IsPositive.isSymmetric : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →L[𝕜] E}, T.IsPositive → (↑T).IsSymmetric
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.zpow_neg_natCast : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  (A : Matrix n' n' R) (n : ℕ), A ^ (-↑n) = (A ^ n)⁻¹
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.CertificateOracle.mk : (List Mathlib.Tactic.Linarith.Comp → ℕ → Lean.MetaM (Std.HashMap ℕ ℕ)) → Mathlib.Tactic.Linarith.CertificateOracle
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isColimitCoconeOfConeLeftOp_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cone F.leftOp} (hc : CategoryTheory.Limits.IsLimit c)
  (s : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.isColimitCoconeOfConeLeftOp F hc).desc s =
    (hc.lift (CategoryTheory.Limits.coneLeftOpOfCocone s)).op
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_comp_add_div : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b c : ℝ} (f : ℝ → E),
  c ≠ 0 → ∀ (d : ℝ), ∫ (x : ℝ) in a..b, f (d + x / c) = c • ∫ (x : ℝ) in d + a / c..d + b / c, f x
-- Mathlib.Analysis.Normed.Group.Constructions
Additive.seminormedCommGroup : {E : Type u_2} → [SeminormedCommGroup E] → SeminormedAddCommGroup (Additive E)
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.coassoc_left_assoc : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {M' : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid M']
  [inst_6 : Module R M'] [inst_7 : Coalgebra R M] (f : M →ₗ[R] M') (g : N →ₗ[R] M),
  ↑(TensorProduct.assoc R M M M') ∘ₗ TensorProduct.map CoalgebraStruct.comul f ∘ₗ CoalgebraStruct.comul ∘ₗ g =
    TensorProduct.map LinearMap.id (TensorProduct.map LinearMap.id f) ∘ₗ
      TensorProduct.map LinearMap.id CoalgebraStruct.comul ∘ₗ CoalgebraStruct.comul ∘ₗ g
-- Std.Time.Format.DateFormat
Std.Time.DayPeriodSymbols.mk.sizeOf_spec : ∀ (am pm noon midnight : String),
  sizeOf { am := am, pm := pm, noon := noon, midnight := midnight } =
    1 + sizeOf am + sizeOf pm + sizeOf noon + sizeOf midnight
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- In a separable pseudometric space, for any ε > 0 there exists a countable collection of
disjoint Borel measurable subsets of diameter at most ε that cover the whole space.  -/
MeasureTheory.SeparableSpace.exists_measurable_partition_diam_le : ∀ (Ω : Type u_1) [inst : PseudoMetricSpace Ω] [inst_1 : MeasurableSpace Ω] [OpensMeasurableSpace Ω]
  [TopologicalSpace.SeparableSpace Ω] {ε : ℝ},
  0 < ε →
    ∃ As,
      (∀ (n : ℕ), MeasurableSet (As n)) ∧
        (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧
          (∀ (n : ℕ), Metric.diam (As n) ≤ ε) ∧ ⋃ n, As n = Set.univ ∧ Pairwise fun n m => Disjoint (As n) (As m)
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalSubstEqs : Lean.Elab.Tactic.Tactic
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instIsStableUnderPrecompHomRel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  CategoryTheory.HomRel.IsStableUnderPrecomp (HomotopicalAlgebra.CofibrantObject.homRel C)
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instModuleReal : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → Module ℝ (ModularForm Γ k)