mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffWithinAt.nsmul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3} [inst_1 : TopologicalSpace H]
  {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5}
  [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G]
  {E' : Type u_6} [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7}
  [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace H' M] {s : Set M} {x : M} {g : M → G},
  ContMDiffWithinAt I' I n g s x → ∀ (m : ℕ), ContMDiffWithinAt I' I n (fun x => m • g x) s x
-- Mathlib.Data.NNReal.Defs
NNReal.instPosSMulStrictMono : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : MulAction ℝ α] [PosSMulStrictMono ℝ α], PosSMulStrictMono NNReal α
-- Lean.Elab.Tactic.Conv.Pattern
Lean.Elab.Tactic.Conv.matchPattern? : Lean.Meta.AbstractMVarsResult → Lean.Expr → Lean.MetaM (Option (Lean.Expr × Array Lean.Expr))
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.trivChange.eq_1 : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (i j : ι),
  Z.trivChange i j =
    { toFun := fun p => (p.1, Z.coordChange i j p.1 p.2), invFun := fun p => (p.1, Z.coordChange j i p.1 p.2),
      source := (Z.baseSet i ∩ Z.baseSet j) ×ˢ Set.univ, target := (Z.baseSet i ∩ Z.baseSet j) ×ˢ Set.univ,
      map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯, continuousOn_toFun := ⋯,
      continuousOn_invFun := ⋯, open_source := ⋯, open_target := ⋯ }
-- Std.Data.HashMap.Raw
/-- Creates a hash map from a list of mappings. If the same key appears multiple times, the last
occurrence takes precedence.  -/
Std.HashMap.Raw.ofArray : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → Array (α × β) → Std.HashMap.Raw α β
-- Std.Http.Protocol.H1
/-- Returns `true` when response status forbids framing headers entirely
(informational and `204` responses).
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.responseForbidsFramingHeaders : Std.Http.Status → Bool
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitIterator.toOption.eq_1 : ∀ {ρ : Type} {σ : String.Slice → Type} {pat : ρ} [inst : String.Slice.Pattern.ToForwardSearcher pat σ]
  {s : String.Slice} (currPos : s.Pos) (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s)),
  String.Slice.SplitIterator.toOption✝ (String.Slice.SplitIterator.operating currPos s_1) = some s_1
-- Mathlib.Data.Set.Basic
/-- **Alias** of the forward direction of `Set.lt_iff_ssubset`. -/
LT.lt.ssubset : ∀ {α : Type u} {s t : Set α}, s ⊂ t → s ⊂ t
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracketWithin_def : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {V W : (x : M) → TangentSpace I x},
  VectorField.mlieBracketWithin I V W s = fun x₀ =>
    VectorField.mpullback I (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x₀))
      (VectorField.lieBracketWithin 𝕜
        (VectorField.mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x₀).symm) V (Set.range ↑I))
        (VectorField.mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x₀).symm) W (Set.range ↑I))
        (↑(extChartAt I x₀).symm ⁻¹' s ∩ Set.range ↑I))
      x₀
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instNatCast : {Γ : Type u_1} →
  {R : Type u_3} → [Zero Γ] → [inst : PartialOrder Γ] → [inst_1 : Zero R] → [NatCast R] → NatCast (HahnSeries Γ R)
-- Aesop.Forward.PremiseIndex
Aesop.PremiseIndex.mk.injEq : ∀ (toNat toNat_1 : ℕ), ({ toNat := toNat } = { toNat := toNat_1 }) = (toNat = toNat_1)
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.mk.sizeOf_spec : ∀ {M : Type u_9} {N : Type u_10} [inst : Mul M] [inst_1 : Mul N] [inst_2 : SizeOf M] [inst_3 : SizeOf N]
  (toEquiv : M ≃ N) (map_mul' : ∀ (x y : M), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y),
  sizeOf { toEquiv := toEquiv, map_mul' := map_mul' } = 1 + sizeOf toEquiv
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.lift_mk_fin : ∀ (n : ℕ), Cardinal.lift.{u_1, 0} (Cardinal.mk (Fin n)) = ↑n
-- Mathlib.MeasureTheory.Measure.Prod
AEMeasurable.lintegral_prod_right : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {f : α → β → ENNReal},
  AEMeasurable (Function.uncurry f) (μ.prod ν) → AEMeasurable (fun x => ∫⁻ (y : β), f x y ∂ν) μ
-- Std.Http.Data.URI.Basic
Std.Http.URI.Builder.mk.inj : ∀ {scheme : Option Std.Http.URI.Scheme} {userInfo : Option Std.Http.URI.UserInfo} {host : Option Std.Http.URI.Host}
  {port : Std.Http.URI.Port} {pathSegments : Array String} {query : Array (String × Option String)}
  {fragment : Option String} {scheme_1 : Option Std.Http.URI.Scheme} {userInfo_1 : Option Std.Http.URI.UserInfo}
  {host_1 : Option Std.Http.URI.Host} {port_1 : Std.Http.URI.Port} {pathSegments_1 : Array String}
  {query_1 : Array (String × Option String)} {fragment_1 : Option String},
  { scheme := scheme, userInfo := userInfo, host := host, port := port, pathSegments := pathSegments, query := query,
        fragment := fragment } =
      { scheme := scheme_1, userInfo := userInfo_1, host := host_1, port := port_1, pathSegments := pathSegments_1,
        query := query_1, fragment := fragment_1 } →
    scheme = scheme_1 ∧
      userInfo = userInfo_1 ∧
        host = host_1 ∧ port = port_1 ∧ pathSegments = pathSegments_1 ∧ query = query_1 ∧ fragment = fragment_1
-- Mathlib.Algebra.Group.Torsion
zsmul_right_inj : ∀ {G : Type u_2} [inst : AddGroup G] [IsAddTorsionFree G] {n : ℤ} {a b : G}, n ≠ 0 → (n • a = n • b ↔ a = b)
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.liftE_ιE_fromOpcycles_assoc : ∀ {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 l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) {A : C}
  (x : A ⟶ (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₂₃))
  (h :
    CategoryTheory.CategoryStruct.comp x ((X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) = 0)
  (hn₂ : n₁ + 1 = n₂) (h' : CategoryTheory.CategoryStruct.comp x (X.δ f₁ f₂₃ n₁ n₂ hn₂) = 0)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.liftE_ιE_fromOpcycles._auto_1) {Z : C}
  (h_1 : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₂₃) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.liftE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ x h hn₂ h' hn₁)
      (CategoryTheory.CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
        (CategoryTheory.CategoryStruct.comp (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁) h_1)) =
    CategoryTheory.CategoryStruct.comp x h_1
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.coe_copy_eq : ∀ {M : Type u_4} {N : Type u_5} {x : Mul M} {x_1 : Mul N} (f : M →ₙ* N) (f' : M → N) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.CategoryTheory.Functor.Functorial
/-- A functorial map preserves composition of morphisms.  -/
CategoryTheory.Functorial.map_comp : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : C → D} [self : CategoryTheory.Functorial F] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z},
  CategoryTheory.map F (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.map F f) (CategoryTheory.map F g)
-- Std.Time.DateTime.WallTime
/-- Subtracts a `Duration` from the given `WallTime`.
 -/
Std.Time.WallTime.subDuration : Std.Time.WallTime → Std.Time.Duration → Std.Time.WallTime
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- The diagram takes values in a small category equivalent to `FintypeCat`.  -/
LightDiagram'.diagram : LightDiagram' → CategoryTheory.Functor ℕᵒᵖ FintypeCat.Skeleton
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.forIn_filterMapM : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {o : Type u_1 → Type u_4} {α β β₂ γ : Type u_1} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Monad o] [LawfulMonad o] [inst_6 : MonadAttach n]
  [WeaklyLawfulMonadAttach n] [inst_8 : MonadLiftT m n] [LawfulMonadLiftT m n] [inst_10 : MonadLiftT n o]
  [LawfulMonadLiftT n o] [inst_12 : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_14 : Std.IteratorLoop α m o]
  [Std.LawfulIteratorLoop α m o] {it : Std.IterM m β} {f : β → n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)},
  forIn (Std.IterM.filterMapM f it) init g =
    forIn it init fun out acc => do
      let __do_lift ← liftM (f out)
      match __do_lift with
        | some c => g c acc
        | none => pure (ForInStep.yield acc)
-- Mathlib.LinearAlgebra.TensorProduct.Pi
/-- Internal implementation detail: we should make this `private`.  -/
TensorProduct.piScalarRightHomBil : (R : Type u_1) →
  [inst : CommSemiring R] →
    (S : Type u_2) →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          (N : Type u_3) →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                [inst_5 : Module S N] → [inst_6 : IsScalarTower R S N] → (ι : Type u_4) → N →ₗ[S] (ι → R) →ₗ[R] ι → N
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPInstantiateMVars : Lean.Options → Bool
-- Mathlib.Topology.Constructions
Topology.IsEmbedding.subtypeVal : ∀ {X : Type u} [inst : TopologicalSpace X] {p : X → Prop}, Topology.IsEmbedding Subtype.val
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.instAlgebraPolynomial : {R : Type r} → [inst : CommRing R] → {W' : WeierstrassCurve.Affine R} → Algebra (Polynomial R) W'.CoordinateRing
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agm_le_max : ∀ {x y : NNReal}, x.agm y ≤ max x y
-- Init.Data.Array.Range
_private.Init.Data.Array.Range.0.Array.range'.eq_1 : ∀ (start size step : ℕ), Array.range' start size step = Array.ofFn fun i => start + step * ↑i
-- Lean.Meta.Basic
Lean.Meta.Cache.mk : Lean.Meta.InferTypeCache →
  Lean.Meta.FunInfoCache →
    Lean.Meta.SynthInstanceCache → Lean.Meta.WhnfCache → Lean.Meta.DefEqCache → Lean.Meta.DefEqCache → Lean.Meta.Cache
-- Batteries.Recycling.RBTree.Basic
RBTree.RBSet.Slow.instDecidableMem : {α : Type u_1} → {cmp : α → α → Ordering} → {x : α} → {t : RBTree.RBSet α cmp} → Decidable (RBTree.RBSet.Mem x t)
-- Mathlib.Algebra.Homology.HomotopyFiber
/-- The isomorphism expressing the commutation between taking
the path object of a homological complex and applying an additive functor.  -/
HomologicalComplex.pathObject.mapHomologicalComplexObjIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {α : Type u_2} →
        {c : ComplexShape α} →
          (K : HomologicalComplex C c) →
            [inst_2 : DecidableRel c.Rel] →
              [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] →
                [inst_4 : K.HasPathObject] →
                  {D : Type u_3} →
                    [inst_5 : CategoryTheory.Category.{v_2, u_3} D] →
                      [inst_6 : CategoryTheory.Preadditive D] →
                        (H : CategoryTheory.Functor C D) →
                          [inst_7 : H.Additive] →
                            [inst_8 :
                                ∀ (i : α),
                                  CategoryTheory.Limits.HasBinaryBiproduct (((H.mapHomologicalComplex c).obj K).X i)
                                    (((H.mapHomologicalComplex c).obj K).X i)] →
                              [inst_9 : ((H.mapHomologicalComplex c).obj K).HasPathObject] →
                                [inst_10 :
                                    ∀ (i : α),
                                      CategoryTheory.Limits.HasBinaryBiproduct
                                        (((H.op.mapHomologicalComplex c.symm).obj K.op).X i)
                                        (((H.op.mapHomologicalComplex c.symm).obj K.op).X i)] →
                                  [HomologicalComplex.HasHomotopyCofiber
                                        (CategoryTheory.Limits.biprod.lift
                                          (CategoryTheory.CategoryStruct.id
                                            ((H.op.mapHomologicalComplex c.symm).obj K.op))
                                          (-CategoryTheory.CategoryStruct.id
                                              ((H.op.mapHomologicalComplex c.symm).obj K.op)))] →
                                    [HomologicalComplex.HasHomotopyCofiber
                                          ((H.op.mapHomologicalComplex c.symm).map
                                            (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K.op)
                                              (-CategoryTheory.CategoryStruct.id K.op)))] →
                                      [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.op.X i) (K.op.X i)] →
                                        (∀ (i : α), ∃ j, c.Rel i j) →
                                          ((H.mapHomologicalComplex c).obj K.pathObject ≅
                                            ((H.mapHomologicalComplex c).obj K).pathObject)
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_succ_eval : ∀ {S : Type u_1} [inst : Semiring S] (n : ℕ) (k : S),
  Polynomial.eval k (ascPochhammer S (n + 1)) = Polynomial.eval k (ascPochhammer S n) * (k + ↑n)
-- Std.Data.HashSet.Lemmas
Std.HashSet.forIn_eq_forIn : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {δ : Type v} {m' : Type v → Type w} [inst : Monad m']
  [LawfulMonad m'] {f : α → δ → m' (ForInStep δ)} {init : δ}, forIn m init f = forIn m init f
-- Mathlib.GroupTheory.GroupAction.Defs
/-- The orbit of an element under an action.  -/
MulAction.orbit : (γ : Type u_2) → {α : Type u_3} → [SMul γ α] → α → Set α
-- Mathlib.Analysis.Normed.Group.Continuity
ContinuousAt.enorm : ∀ {E : Type u_7} [inst : TopologicalSpace E] [inst_1 : ContinuousENorm E] {X : Type u_8} [inst_2 : TopologicalSpace X]
  {f : X → E} {a : X}, ContinuousAt f a → ContinuousAt (fun x => ‖f x‖ₑ) a
-- Init.Data.Nat.Basic
Nat.instMax : Max ℕ
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.η_ε_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (X : C)
  [inst_3 : F.Monoidal],
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.η F).app X)
      ((CategoryTheory.Functor.LaxMonoidal.ε F).app X) =
    CategoryTheory.CategoryStruct.id ((F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit M)).obj X)
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec.eq_1 : ∀ (X : AlgebraicGeometry.Scheme),
  AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec X =
    CategoryTheory.NatIso.ofComponents (fun U => ⋯.isoSpec) ⋯
-- Aesop.Tree.Data
Aesop.Goal.setAddedInIteration : Aesop.Iteration → Aesop.Goal → Aesop.Goal
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of the reverse direction of `SimpleGraph.Walk.isTrail_map_iff_of_injective`. -/
SimpleGraph.Walk.IsTrail.map : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u v : V} {p : G.Walk u v},
  Function.Injective ⇑f → p.IsTrail → (SimpleGraph.Walk.map f p).IsTrail
-- Mathlib.Combinatorics.Configuration
/-- If a nondegenerate configuration has a unique line through any two points, and if `|P| = |L|`,
then there is a unique point on any two lines.  -/
Configuration.HasLines.hasPoints : {P : Type u_1} →
  {L : Type u_2} →
    [inst : Membership P L] →
      [Configuration.HasLines P L] →
        [inst_2 : Fintype P] → [inst_3 : Fintype L] → Fintype.card P = Fintype.card L → Configuration.HasPoints P L
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.rotateL.fun_cases_unfolding : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (rk : α) (rv : β rk)
  (rr : Std.DTreeMap.Internal.Impl α β)
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Prop),
  (∀ (rl : Std.DTreeMap.Internal.Impl α β),
      rl.size < Std.DTreeMap.Internal.ratio * rr.size →
        motive rl (Std.DTreeMap.Internal.Impl.singleL k v l rk rv rl rr)) →
    (¬Std.DTreeMap.Internal.Impl.leaf.size < Std.DTreeMap.Internal.ratio * rr.size →
        motive Std.DTreeMap.Internal.Impl.leaf
          (Std.DTreeMap.Internal.Impl.singleL k v l rk rv Std.DTreeMap.Internal.Impl.leaf rr)) →
      (∀ (ls : ℕ) (lk : α) (lv : β lk) (ll lr : Std.DTreeMap.Internal.Impl α β),
          ¬(Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).size < Std.DTreeMap.Internal.ratio * rr.size →
            motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)
              (Std.DTreeMap.Internal.Impl.doubleL k v l rk rv lk lv ll lr rr)) →
        ∀ (rl : Std.DTreeMap.Internal.Impl α β), motive rl (Std.DTreeMap.Internal.Impl.rotateL k v l rk rv rl rr)
-- Init.Data.String.Substring
Substring.prev : Substring.Raw → String.Pos.Raw → String.Pos.Raw
-- Mathlib.GroupTheory.Sylow
/-- A generalisation of **Sylow's first theorem**. If `p ^ n` divides
the cardinality of `G`, then there is a subgroup of cardinality `p ^ n`  -/
Sylow.exists_subgroup_card_pow_prime : ∀ {G : Type u} [inst : Group G] [Finite G] (p : ℕ) {n : ℕ} [Fact (Nat.Prime p)],
  p ^ n ∣ Nat.card G → ∃ K, Nat.card ↥K = p ^ n
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.omega0_opow_mul_nat_lt : ∀ {a b : Ordinal.{u_1}}, a < b → ∀ (n : ℕ), Ordinal.omega0 ^ a * ↑n < Ordinal.omega0 ^ b
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.mk.inj : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} {val val_1 : X}, { val := val } = { val := val_1 } → val = val_1
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_smul : ∀ {n : Type u_3} {R : Type u_7} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : SMulZeroClass R α]
  (r : R) (d : n → α), Matrix.diagonal (r • d) = r • Matrix.diagonal d
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.inter_of_right : ∀ {α : Type u} {s : Set α}, s.Finite → ∀ (t : Set α), (t ∩ s).Finite
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_inter!_of_contains_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        Std.DTreeMap.Internal.Impl.contains k m₂ = true →
          Std.DTreeMap.Internal.Impl.Const.getD (m₁.inter! m₂) k fallback =
            Std.DTreeMap.Internal.Impl.Const.getD m₁ k fallback
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coe_sum : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddCommMonoid β]
  [inst_3 : ContinuousAdd β] {ι : Type u_3} (s : Finset ι) (f : ι → C(α, β)), ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Prod
CliffordAlgebra.toProd_one_tmul_ι : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] (Q₁ : QuadraticForm R M₁)
  (Q₂ : QuadraticForm R M₂) (m₂ : M₂),
  (CliffordAlgebra.toProd Q₁ Q₂) (1 ᵍ⊗ₜ[R] (CliffordAlgebra.ι Q₂) m₂) =
    (CliffordAlgebra.ι (QuadraticMap.prod Q₁ Q₂)) (0, m₂)
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.below.constModify : ∀ {α : Type u} [inst : Ord α] {motive : {β : α → Type v} → (a : Std.DTreeMap.Internal.Impl α β) → a.WF → Prop}
  {x : Type v} {t : Std.DTreeMap.Internal.Impl α fun x_1 => x} {k : α} {f : x → x} (a : t.WF),
  Std.DTreeMap.Internal.Impl.WF.below a → motive t a → Std.DTreeMap.Internal.Impl.WF.below ⋯
-- Mathlib.Algebra.Group.UniqueProds.Basic
Additive.instUniqueSumsOfUniqueProds : ∀ {M : Type u_1} [inst : Mul M] [UniqueProds M], UniqueSums (Additive M)
-- Mathlib.Computability.Ackermann
ack_mono_left : ∀ (n : ℕ), Monotone fun m => ack m n
-- Mathlib.Order.WellFoundedSet
Set.IsPWO.image_of_monotoneOn : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α},
  s.IsPWO → ∀ {f : α → β}, MonotoneOn f s → (f '' s).IsPWO
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The negative of a `C^n` function on a domain is `C^n`.  -/
ContDiffOn.neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {s : Set E} {f : E → F}, ContDiffOn 𝕜 n f s → ContDiffOn 𝕜 n (fun x => -f x) s
-- Init.Data.String.Basic
/-- Given a position in `s` that is at most `p₀`, obtain the corresponding position in `s.sliceTo p₀`.  -/
String.Slice.Pos.sliceTo : {s : String.Slice} → (p₀ pos : s.Pos) → pos ≤ p₀ → (s.sliceTo p₀).Pos
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.instDecidableEq : {α : Type u_1} → [DecidableEq α] → DecidableEq (FreeGroup α)
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.pellZd.eq_1 : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), Pell.pellZd a1 n = { re := ↑(Pell.xn a1 n), im := ↑(Pell.yn a1 n) }
-- Mathlib.NumberTheory.LSeries.HurwitzZeta
HurwitzZeta.sinZeta_eq : ∀ (a : UnitAddCircle) (s : ℂ),
  HurwitzZeta.sinZeta a s = (HurwitzZeta.expZeta a s - HurwitzZeta.expZeta (-a) s) / (2 * Complex.I)
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The L-series of the arithmetic function `ζ` equals the Riemann Zeta Function on its
domain of convergence `1 < re s`.  -/
ArithmeticFunction.LSeriesHasSum_zeta : ∀ {s : ℂ}, 1 < s.re → LSeriesHasSum (fun n => ↑(ArithmeticFunction.zeta n)) s (riemannZeta s)
-- Std.Internal.UV.System
Std.Internal.UV.System.instReprCPUTimes.repr : Std.Internal.UV.System.CPUTimes → ℕ → Std.Format
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.isSt_ofSeq_iff_tendsto : ∀ {f : ℕ → ℝ} {r : ℝ}, (Hyperreal.ofSeq f).IsSt r ↔ Filter.Tendsto f (↑(Filter.hyperfilter ℕ)) (nhds r)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.oproj.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {i : ℕ} {var : Lean.FVarId}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_7} {i_1 : ℕ}
  {var_1 : Lean.FVarId} {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_7},
  Lean.Compiler.LCNF.LetValue.oproj i var h = Lean.Compiler.LCNF.LetValue.oproj i_1 var_1 h_1 → i = i_1 ∧ var = var_1
-- Mathlib.Analysis.Calculus.ContDiff.WithLp
contDiffWithinAt_piLp_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_3 : Fintype ι]
  (p : ENNReal) [inst_4 : Fact (1 ≤ p)] {n : WithTop ℕ∞} {i : ι} {t : Set (PiLp p E)} {y : PiLp p E},
  ContDiffWithinAt 𝕜 n (fun f => f.ofLp i) t y
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.mem_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {S : Submonoid N} {f : F} {x : M}, x ∈ Submonoid.comap f S ↔ f x ∈ S
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.mod_add_div' : ∀ {R : Type u} [inst : EuclideanDomain R] (m k : R), m % k + m / k * k = m
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.toLinearEquiv_symm_to_linearMap : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (A : SpecialLinearGroup R V), ↑(SpecialLinearGroup.toLinearEquiv A).symm = ↑↑A⁻¹
-- Mathlib.MeasureTheory.OuterMeasure.Defs
MeasureTheory.OuterMeasure.mono : ∀ {α : Type u_2} (self : MeasureTheory.OuterMeasure α) {s₁ s₂ : Set α}, s₁ ⊆ s₂ → self.measureOf s₁ ≤ self.measureOf s₂