mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.PerfectPairing.Restrict
LinearMap.restrictScalarsField_apply_apply : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module L M] [inst_6 : Module L N] [inst_7 : Module K M]
  [inst_8 : Module K N] [inst_9 : IsScalarTower K L M] (p : M →ₗ[L] N →ₗ[L] L) {M' : Type u_5} {N' : Type u_6}
  [inst_10 : AddCommGroup M'] [inst_11 : AddCommGroup N'] [inst_12 : Module K M'] [inst_13 : Module K N']
  [inst_14 : IsScalarTower K L N] (i : M' →ₗ[K] M) (j : N' →ₗ[K] N)
  (hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap K L).range) (x : M') (y : N'),
  (algebraMap K L) (((i.restrictScalarsRange₂ j (Algebra.linearMap K L) ⋯ p hp) x) y) = (p (i x)) (j y)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.comp_toFun : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : AddMonoid C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] (g : B →ₜ+ C) (f : A →ₜ+ B)
  (x : A), (g.comp f) x = g (f x)
-- Mathlib.Data.Countable.Defs
not_countable_iff : ∀ {α : Sort u}, ¬Countable α ↔ Uncountable α
-- Mathlib.Order.Defs.PartialOrder
lt_iff_ge_iff_gt_iff_le : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, (a < b ↔ b ≤ a) ↔ (b < a ↔ a ≤ b)
-- Mathlib.GroupTheory.Index
AddSubgroup.index_dvd_of_le : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H ≤ K → K.index ∣ H.index
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_pow_natAbs : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a : E) (n : ℤ), ‖a ^ n.natAbs‖₊ = ‖a ^ n‖₊
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.mapCotangent.congr_simp : ∀ {R : Type u} [inst : CommRing R] {A : Type u_1} {B : Type u_2} [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (I₁ : Ideal A) (I₂ : Ideal B) (f f_1 : A →ₐ[R] B) (e_f : f = f_1)
  (h : I₁ ≤ Ideal.comap f I₂), I₁.mapCotangent I₂ f h = I₁.mapCotangent I₂ f_1 ⋯
-- Mathlib.CategoryTheory.Sites.Coverage
/-- Any sieve that contains a covering presieve for a coverage is a covering sieve for the associated
Grothendieck topology.
 -/
CategoryTheory.Coverage.mem_toGrothendieck_sieves_of_superset : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (K : CategoryTheory.Coverage C) {X : C}
  {S : CategoryTheory.Sieve X} {R : CategoryTheory.Presieve X},
  R ≤ S.arrows → R ∈ K.coverings X → S ∈ K.toGrothendieck X
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.instFullMonCatForget₂AddMonoidHomCarrierCarrier : (CategoryTheory.forget₂ AddGrpCat AddMonCat).Full
-- Mathlib.Data.Set.Sups
Set.subset_sups_self : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s : Set α}, s ⊆ s ⊻ s
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey!_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] [inst_4 : Inhabited α] {f : α → β → Option γ} {k : α} (h : m.WF),
  (Std.DHashMap.Raw.filterMap f m).getKey! k =
    ((m.getKey? k).pfilter fun x h' => (f x (Std.DHashMap.Raw.Const.get m x ⋯)).isSome).get!
-- Mathlib.Analysis.Convex.Basic
StarConvex.eq_1 : ∀ (𝕜 : Type u_4) {E : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] (x : E) (s : Set E),
  StarConvex 𝕜 x s = ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- carrier of the coalgebra  -/
CategoryTheory.Endofunctor.Coalgebra.V : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} → CategoryTheory.Endofunctor.Coalgebra F → C
-- Mathlib.RingTheory.Smooth.Pi
Ideal.Quotient.ring.congr_simp : ∀ {R : Type u} [inst : Ring R] (I : Ideal R) [inst_1 : I.IsTwoSided], Ideal.Quotient.ring I = Ideal.Quotient.ring I
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- Given two functions `f : ℝ → ℝ` and
`g : MultiseriesExpansion basis_tl → MultiseriesExpansion basis_tl'`, apply them to exponents and
coefficients of a multiseries.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.map : {basis_hd : ℝ → ℝ} →
  {basis_tl : Tactic.ComputeAsymptotics.Basis} →
    {basis_hd' : ℝ → ℝ} →
      {basis_tl' : Tactic.ComputeAsymptotics.Basis} →
        (ℝ → ℝ) →
          (Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl →
              Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl') →
            Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
              Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd' basis_tl'
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Slow.instDecidableEMem : {α : Type u_1} → {x : α} → [DecidableEq α] → {t : RBTree.RBNode α} → Decidable (RBTree.RBNode.EMem x t)
-- Mathlib.Algebra.CharP.Defs
/-- The exponential characteristic is unique.  -/
ExpChar.eq : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] {p q : ℕ}, ExpChar R p → ExpChar R q → p = q
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.coe_toSubmodule : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (L' : LieRinehartSubalgebra A L), ↑L'.toSubmodule = ↑L'
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- Given a measurable set `s`, then `μ (s ∩ closedBall x r) / μ (closedBall x r)` converges when
`r` tends to `0`, for almost every `x`. The limit is `1` for `x ∈ s` and `0` for `x ∉ s`.
This shows that almost every point of `s` is a Lebesgue density point for `s`.
A version for non-measurable sets holds, but it only gives the first conclusion,
see `ae_tendsto_measure_inter_div`.  -/
Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet : ∀ {β : Type u} [inst : MetricSpace β] [inst_1 : MeasurableSpace β] [BorelSpace β] [SecondCountableTopology β]
  [HasBesicovitchCovering β] (μ : MeasureTheory.Measure β) [MeasureTheory.IsLocallyFiniteMeasure μ] {s : Set β},
  MeasurableSet s →
    ∀ᵐ (x : β) ∂μ,
      Filter.Tendsto (fun r => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0))
        (nhds (s.indicator 1 x))
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey?_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = true → t.maxKey? = none
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.Agree'.brecOn : ∀ {F : PFunctor.{uA, uB}} {motive : (a : ℕ) → (a_1 a_2 : F.M) → PFunctor.M.Agree' a a_1 a_2 → Prop} {a : ℕ}
  {a_1 a_2 : F.M} (t : PFunctor.M.Agree' a a_1 a_2),
  (∀ (a : ℕ) (a_3 a_4 : F.M) (t : PFunctor.M.Agree' a a_3 a_4), PFunctor.M.Agree'.below t → motive a a_3 a_4 t) →
    motive a a_1 a_2 t
-- Mathlib.MeasureTheory.OuterMeasure.AE
/-- `f ≤ᵐ[μ] g` means `f` is eventually less than `g` along the a.e. filter,
i.e. `f ≤ g` away from a null set.

This is notation for `Filter.EventuallyLE (MeasureTheory.ae μ) f g`.  -/
MeasureTheory.«term_≤ᵐ[_]_» : Lean.TrailingParserDescr
-- Mathlib.Data.Sign.Defs
sign_apply : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Preorder α] [inst_2 : DecidableLT α] {a : α},
  SignType.sign a = if 0 < a then 1 else if a < 0 then -1 else 0
-- Mathlib.Probability.HasCondDistrib
ProbabilityTheory.HasCondDistrib.aemeasurable_snd : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {P : MeasureTheory.Measure Ω} {X : Ω → 𝓧} {Y : Ω → 𝓨} {κ : ProbabilityTheory.Kernel 𝓧 𝓨},
  ProbabilityTheory.HasCondDistrib Y X κ P → AEMeasurable Y P
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.PropertyIsLocal.and : ∀ {P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q) →
      RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] f => P f ∧ Q f
-- Mathlib.GroupTheory.Congruence.Basic
/-- Coercion from a congruence relation `c` on a monoid `M` to the submonoid of `M × M` whose
elements are `(x, y)` such that `x` is related to `y` by `c`.  -/
Con.toSubmonoid : {M : Type u_1} → [inst : MulOneClass M] → Coe (Con M) (Submonoid (M × M))
-- Lean.Meta.Sym.Offset
Lean.Meta.Sym.Offset.num.inj : ∀ {k k_1 : ℕ}, Lean.Meta.Sym.Offset.num k = Lean.Meta.Sym.Offset.num k_1 → k = k_1
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.instInfSet.eq_1 : ∀ (M : Type u_1) [inst : AddZeroClass M],
  SaturatedAddSubmonoid.instInfSet M =
    { sInf := fun f => { carrier := ⋂ s ∈ f, ↑s, add_mem' := ⋯, zero_mem' := ⋯, addSaturated := ⋯ } }
-- Mathlib.Data.Set.NAry
Set.image2_singleton_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {b : β},
  Set.image2 f s {b} = (fun a => f a b) '' s
-- Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
CategoryTheory.Functor.instLinearDerivedCategoryMapDerivedCategory : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] [inst_1 : CategoryTheory.Abelian C₁]
  [inst_2 : HasDerivedCategory C₁] {C₂ : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C₂]
  [inst_4 : CategoryTheory.Abelian C₂] [inst_5 : HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂)
  [inst_6 : F.Additive] [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F] (R : Type u_1) [inst_9 : Ring R]
  [inst_10 : CategoryTheory.Linear R C₁] [inst_11 : CategoryTheory.Linear R C₂] [CategoryTheory.Functor.Linear R F],
  CategoryTheory.Functor.Linear R F.mapDerivedCategory
-- Batteries.Data.List.Perm
List.Perm.diff_right : ∀ {α : Type u_1} {l₁ l₂ : List α} [inst : BEq α] [LawfulBEq α] (t : List α), l₁.Perm l₂ → (l₁.diff t).Perm (l₂.diff t)
-- Init.Data.List.Lemmas
/-- Reversing a flatten is the same as reversing the order of parts and reversing all parts.  -/
List.reverse_flatten : ∀ {α : Type u_1} {L : List (List α)}, L.flatten.reverse = (List.map List.reverse L).reverse.flatten
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
IsLocalFrameOn.generating : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {ι : Type u_7} {n : WithTop ℕ∞}
  {s : ι → (x : M) → V x} {u : Set M},
  IsLocalFrameOn I F n s u → ∀ {x : M}, x ∈ u → ⊤ ≤ Submodule.span 𝕜 (Set.range fun x_1 => s x_1 x)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instModuleCoeOfSMulMemClass : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            {R₀ : Type u_4} →
              [inst_1 : Semiring R₀] →
                [inst_2 : (i : ι) → AddCommMonoid (R i)] →
                  [inst_3 : (i : ι) → Module R₀ (R i)] →
                    [inst_4 : ∀ (i : ι), AddSubmonoidClass (S i) (R i)] →
                      [∀ (i : ι), SMulMemClass (S i) R₀ (R i)] →
                        Module R₀ (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Mathlib.Analysis.Normed.Operator.Banach
AntilipschitzWith.completeSpace_range_clm : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {σ : 𝕜 →+* 𝕜'} {σ' : 𝕜' →+* 𝕜}
  [inst_4 : RingHomInvPair σ σ'] {F : Type u_4} [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜' F]
  [CompleteSpace E] [CompleteSpace F] {f : E →SL[σ] F} {c : NNReal}, AntilipschitzWith c ⇑f → CompleteSpace ↥(↑f).range
-- Mathlib.Algebra.Polynomial.RuleOfSigns
/-- We can only lose, not gain, sign changes if we drop the leading coefficient.  -/
Polynomial.signVariations_eraseLead_le : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] (P : Polynomial R),
  P.eraseLead.signVariations ≤ P.signVariations
-- Mathlib.Order.Filter.Basic
Filter.mem_iSup : ∀ {α : Type u} {ι : Sort x} {x : Set α} {f : ι → Filter α}, x ∈ iSup f ↔ ∀ (i : ι), x ∈ f i
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm
/-- Given indexes `exitIdx` and `enterIdx` of exiting and entering variables in the `basic` and `free`
arrays, performs pivot operation, i.e. expresses one through the other and makes the free one basic
and vice versa.
 -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.doPivotOperation : {matType : ℕ → ℕ → Type} →
  [inst : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] →
    ℕ → ℕ → Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithmM matType Unit
-- Batteries.Data.Array.Scan
Array.back?_scanl : ∀ {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β} {as : Array α},
  (Array.scanl f init as).back? = some (Array.foldl f init as)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.intValuationDef.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R),
  v.intValuationDef r =
    if r = 0 then 0 else WithZero.exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors))
-- Init.Data.BitVec.Lemmas
BitVec.neg_mul_comm : ∀ {w : ℕ} (x y : BitVec w), -x * y = x * -y
-- Mathlib.Algebra.Star.Unitary
Unitary.coe_star : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {U : ↥(unitary R)}, ↑(star U) = star ↑U
-- Init.Data.Float.Model.Float32
/-- Computes `m * 10^e`.  -/
Float32.Model.ofScientific : ℕ → ℤ → Float32.Model
-- Mathlib.Analysis.LocallyConvex.AbsConvex
absConvexHull_univ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜], (absConvexHull 𝕜) Set.univ = Set.univ
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.instSubsingletonHomCompDiscreteNormalMonoidalObject : ∀ {C : Type u} (x y : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C),
  Subsingleton (x ⟶ y)
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.Trace.messages.sizeOf_spec : sizeOf Lean.Lsp.Trace.messages = 1
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
/-- The single functor `C ⥤ DerivedCategory C` which sends `X : C` to the
single cochain complex with `X` sitting in degree `n : ℤ`.  -/
DerivedCategory.singleFunctor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] → ℤ → CategoryTheory.Functor C (DerivedCategory C)
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.ofProp_forall : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {α : Type u_1} {Φ : α → Prop},
  (Lean.Order.iInf fun x => Lean.Order.CompleteLattice.ofProp (Φ x)) =
    Lean.Order.CompleteLattice.ofProp (∀ (x : α), Φ x)
-- Init.Data.List.MinMax
List.le_min_iff : ∀ {α : Type u_1} [inst : Min α] [inst_1 : LE α] [Std.LawfulOrderInf α] {l : List α} (hl : l ≠ []) {x : α},
  x ≤ l.min hl ↔ ∀ b ∈ l, x ≤ b
-- Mathlib.Data.Complex.Basic
Complex.ofReal_inj : ∀ {z w : ℝ}, ↑z = ↑w ↔ z = w
-- Mathlib.Dynamics.FixedPoints.Basic
Function.fixedPoints_symm : ∀ {α : Type u_1} {e : Equiv.Perm α}, Function.fixedPoints ⇑(Equiv.symm e) = Function.fixedPoints ⇑e
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
ModuleCat.Derivation.d_add : ∀ {A B : CommRingCat} {M : ModuleCat ↑B} {f : A ⟶ B} (D : M.Derivation f) (b b' : ↑B), D.d (b + b') = D.d b + D.d b'
-- Mathlib.Topology.Algebra.MulAction
continuousSMul_sInf : ∀ {M : Type u_2} {X : Type u_3} [inst : TopologicalSpace M] [inst_1 : SMul M X] {ts : Set (TopologicalSpace X)},
  (∀ t ∈ ts, ContinuousSMul M X) → ContinuousSMul M X
-- Lean.Parser.Do
Lean.Parser.Term.doLet.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.ODE.ExistUnique
/-- A version of `ODE_solution_unique_of_mem_Icc` for uniqueness in an open interval.  -/
ODE_solution_unique_of_mem_Ioo : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal}
  {f g : ℝ → E} {a b t₀ : ℝ},
  (∀ t ∈ Set.Ioo a b, LipschitzOnWith K (v t) (s t)) →
    t₀ ∈ Set.Ioo a b →
      (∀ t ∈ Set.Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t) →
        (∀ t ∈ Set.Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t) → f t₀ = g t₀ → Set.EqOn f g (Set.Ioo a b)
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENatAux_eq_top : ∀ {a : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a → a.toENatAux = ⊤
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.Gamma0_mem : ∀ {N : ℕ} {A : Matrix.SpecialLinearGroup (Fin 2) ℤ}, A ∈ CongruenceSubgroup.Gamma0 N ↔ ↑(↑A 1 0) = 0
-- Mathlib.Tactic.NormNum.DivMod
/-- Given a result for evaluating `a b` in `ℤ`, evaluate `a % b`.  -/
_private.Mathlib.Tactic.NormNum.DivMod.0.Mathlib.Meta.NormNum.evalIntMod.go : (a na : Q(ℤ)) →
  ℤ →
    Q(Mathlib.Meta.NormNum.IsInt «$a» «$na») →
      (b : Q(ℤ)) → Mathlib.Meta.NormNum.Result b → Option (Mathlib.Meta.NormNum.Result q(«$a» % «$b»))
-- Mathlib.Order.Interval.Set.Fin
Fin.image_addNat_Ici : ∀ {n : ℕ} (m : ℕ) (i : Fin n), (fun x => x.addNat m) '' Set.Ici i = Set.Ici (i.addNat m)
-- Mathlib.NumberTheory.Pell
Pell.Solution₁.instCoeZsqrtd : {d : ℤ} → Coe (Pell.Solution₁ d) (ℤ√d)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.piFunctor_obj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] (X : C)
  {X_1 Y : Type wᵒᵖ} (f : X_1 ⟶ Y),
  (CategoryTheory.Limits.piFunctor.obj X).map f =
    CategoryTheory.Limits.Pi.map' ⇑(CategoryTheory.ConcreteCategory.hom f.unop) fun x =>
      CategoryTheory.CategoryStruct.id X
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
DirichletCharacter.LFunctionTrivChar.congr_simp : ∀ (N N_1 : ℕ) (e_N : N = N_1) [inst : NeZero N] (s s_1 : ℂ),
  s = s_1 → DirichletCharacter.LFunctionTrivChar N s = DirichletCharacter.LFunctionTrivChar N_1 s_1
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realSpace K),
  ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis x =
    ↑NumberField.mixedEmbedding.fundamentalCone.expMap
      ((NumberField.mixedEmbedding.fundamentalCone.completeBasis K).equivFun.symm x)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertMany_empty_list_cons : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {k : α} {v : β} {tl : List (α × β)},
  ↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty ((k, v) :: tl) ⋯) =
    ↑(Std.DTreeMap.Internal.Impl.Const.insertMany
        (Std.DTreeMap.Internal.Impl.insert k v Std.DTreeMap.Internal.Impl.empty ⋯).impl tl ⋯)
-- Std.Internal.UV.System
Std.Internal.UV.System.CPUInfo.mk : String → UInt64 → Std.Internal.UV.System.CPUTimes → Std.Internal.UV.System.CPUInfo
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLT?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α),
  Std.DTreeMap.Internal.Impl.getKeyLT? k = Std.DTreeMap.Internal.Impl.getKeyLT?.go k none
-- Mathlib.Order.Filter.Basic
Filter.instInhabited : {α : Type u} → Inhabited (Filter α)
-- Mathlib.Analysis.Normed.Group.Uniform
antilipschitzWith_neg_iff : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {K : NNReal}
  {f : α → E}, AntilipschitzWith K (-f) ↔ AntilipschitzWith K f
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderivWithin_fst : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {s : Set (M × M')} {x : M × M'},
  UniqueMDiffAt[s] x → mfderiv[s] Prod.fst x = ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)
-- Init.Core
/-- A setoid's equivalence relation is transitive.  -/
Setoid.trans : ∀ {α : Sort u} [inst : Setoid α] {a b c : α}, a ≈ b → b ≈ c → a ≈ c
-- Init.Data.BitVec.Bitblast
/-- Recurrence lemma: truncating to `i+1` bits and then zero extending to `w`
equals truncating upto `i` bits `[0..i-1]`, and then adding the `i`th bit of `x`.
 -/
BitVec.setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow : ∀ {w : ℕ} (x : BitVec w) (i : ℕ),
  BitVec.setWidth w (BitVec.setWidth (i + 1) x) = BitVec.setWidth w (BitVec.setWidth i x) + (x &&& BitVec.twoPow w i)
-- Mathlib.Data.NNReal.Defs
NNReal.instInhabited : Inhabited NNReal
-- Mathlib.Algebra.Group.Basic
mul_right_iterate : ∀ {M : Type u_4} [inst : Monoid M] (a : M) (n : ℕ), (fun x => x * a)^[n] = fun x => x * a ^ n
-- Init.Data.Format.Basic
Std.Format.instAppend : Append Std.Format
-- Init.Data.Float.Model.Unpacked.Sign
Float.Model.UnpackedFloat.instBEqSign : BEq Float.Model.UnpackedFloat.Sign
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsClosedSubgraph.inc_congr : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β},
  x ∈ H.vertexSet → H.IsClosedSubgraph G → (H.Inc e x ↔ G.Inc e x)
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkYonedaEquiv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X Y : C}
  {P : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : CategoryTheory.shrinkYoneda.{w, v, u}.obj X ⟶ P) (g : Y ⟶ X),
  (CategoryTheory.ConcreteCategory.hom (P.map g.op)) (CategoryTheory.shrinkYonedaEquiv f) =
    CategoryTheory.shrinkYonedaEquiv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkYoneda.{w, v, u}.map g) f)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.getKey! t.minKey! = t.minKey!
-- Mathlib.RingTheory.Morita.Matrix
fromModuleCatToModuleCatLinearEquiv.eq_1 : ∀ (R : Type u) {ι : Type v} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (M : Type u_1)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (i : ι),
  fromModuleCatToModuleCatLinearEquiv R M i =
    { toFun := fun x => ∑ i_1, ↑x i_1, map_add' := ⋯, map_smul' := ⋯, invFun := fun x => ⟨Pi.single i x, ⋯⟩,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Data.FunLike.IsApply
IsOneApplyEqSelf.mk : ∀ {F : Type u_1} {α : outParam (Type u_2)} [inst : FunLike F α α] [inst_1 : One F],
  (∀ (x : α), 1 x = x) → IsOneApplyEqSelf F α
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.instZeroOfNontrivialSubtypeMemLieSubmoduleGenWeightSpaceOfNatForall : {R : Type u_2} →
  {L : Type u_3} →
    {M : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [inst_6 : LieModule R L M] →
                    [inst_7 : LieRing.IsNilpotent L] →
                      [Nontrivial ↥(LieModule.genWeightSpace M 0)] → Zero (LieModule.Weight R L M)