mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Options
Lean.OptionDeprecation.since : Lean.OptionDeprecation → String
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
/-- **Alias** of `Left.nsmul_neg`. -/
nsmul_neg : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddLeftMono M] {a : M} {n : ℕ}, a < 0 → n ≠ 0 → n • a < 0
-- Mathlib.Logic.Relation
Relation.le_onFun_map : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} (f : α → β), r ≤ Function.onFun (Relation.Map r f f) f
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.genWeightSpace_ne_bot' : ∀ {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] (self : LieModule.Weight R L M), LieModule.genWeightSpace M self.toFun ≠ ⊥
-- Lean.Meta.Sym.Pattern
Lean.Meta.Sym.Pattern.varTypes : Lean.Meta.Sym.Pattern → Array Lean.Expr
-- Mathlib.FieldTheory.AlgebraicClosure
/-- If `i` is an `F`-algebra homomorphism from `E` to `K`, then the preimage of
`algebraicClosure F K` under the map `i` is equal to `algebraicClosure F E`.  -/
algebraicClosure.comap_eq_of_algHom : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra F K] (i : E →ₐ[F] K),
  IntermediateField.comap i (algebraicClosure F K) = algebraicClosure F E
-- Mathlib.Order.SetDissipate
Set.iInter_dissipate : ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : Preorder α], ⋂ x, Set.dissipate s x = ⋂ x, s x
-- Mathlib.Order.CompleteLattice.Basic
iInf_emptyset : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α}, ⨅ x ∈ ∅, f x = ⊤
-- Mathlib.MeasureTheory.Group.AEStabilizer
MulAction.stabilizer_le_aestabilizer : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {x : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : MeasureTheory.SMulInvariantMeasure G α μ] (s : Set α),
  MulAction.stabilizer G s ≤ MulAction.aestabilizer G μ s
-- Lean.Meta.Match.MatcherApp.Transform
/-- Given a `MatcherApp`, replaces the motive with one that is inferred from the actual types of the
alternatives.

For example, given
```
(match (motive := Nat → Unit → ?) n with
 0 => 1
 _ => true) ()
```
(for any `?`; the motive’s result type be ignored) will give this type
```
(match n with
 | 0 => Nat
 | _ => Bool)
```

The given `MatcherApp` must not use a splitter in `matcherName`.
The resulting expression *will* use the splitter corresponding to `matcherName` (this is necessary
for the construction).

Internally, this needs to reduce the matcher in a given branch; this is done using
`Split.simpMatchTarget`.
 -/
Lean.Meta.MatcherApp.inferMatchType : Lean.Meta.MatcherApp → Lean.MetaM Lean.Meta.MatcherApp
-- Mathlib.Analysis.Convex.Basic
Convex.is_linear_preimage : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] {s : Set F},
  Convex 𝕜 s → ∀ {f : E → F}, IsLinearMap 𝕜 f → Convex 𝕜 (f ⁻¹' s)
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalTerm.instDataValue : Lean.Elab.ConfigEval.EvalTerm Lean.DataValue
-- Mathlib.Dynamics.Minimal
/-- An action of an additive monoid `M` on a topological space is called *minimal* if the `M`-orbit
of every point `x : α` is dense.  -/
AddAction.IsMinimal : (M : Type u_1) → (α : Type u_2) → [inst : AddMonoid M] → [TopologicalSpace α] → [AddAction M α] → Prop
-- Init.Data.Vector.Lemmas
Vector.swap_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} (h : xs.size = n) {i j : ℕ} (hi : i < n) (hj : j < n),
  (Vector.mk xs h).swap i j hi hj = Vector.mk (xs.swap i j ⋯ ⋯) ⋯
-- Mathlib.Order.Lattice
instDistribLatticeOfLinearOrder : {α : Type u} → [LinearOrder α] → DistribLattice α
-- Mathlib.Topology.Algebra.Module.Equiv
MulOpposite.opContinuousLinearEquiv_symm_apply : ∀ (R : Type u_1) [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] (a : Mᵐᵒᵖ), (MulOpposite.opContinuousLinearEquiv R).symm a = MulOpposite.unop a
-- Mathlib.Algebra.Ring.Invertible
IsAddUnit.mul_right : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] {x : R}, IsAddUnit x → ∀ (y : R), IsAddUnit (x * y)
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.LeanSemanticToken.mk.injEq : ∀ (stx : Lean.Syntax) (type : Lean.Lsp.SemanticTokenType) (priority : ℕ) (stx_1 : Lean.Syntax)
  (type_1 : Lean.Lsp.SemanticTokenType) (priority_1 : ℕ),
  ({ stx := stx, type := type, priority := priority } = { stx := stx_1, type := type_1, priority := priority_1 }) =
    (stx = stx_1 ∧ type = type_1 ∧ priority = priority_1)
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_two_add_inv_two : 2⁻¹ + 2⁻¹ = 1
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.op_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : Cᵒᵖ} (f : X ⟶ Y), F.op.map f = (F.map f.unop).op
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.map_b₈ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {A : Type v} [inst_1 : CommRing A] (f : R →+* A),
  (W.map f).b₈ = f W.b₈
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- If `c ∉ {0, ∞}` and `m₁ d ≤ c * m₂ d` for `d < ε` for some `ε > 0`
(we use `≤ᶠ[𝓝[≥] 0]` to state this), then `mkMetric m₁ hm₁ ≤ c • mkMetric m₂ hm₂`.  -/
MeasureTheory.Measure.mkMetric_mono_smul : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X]
  {m₁ m₂ : ENNReal → ENNReal} {c : ENNReal},
  c ≠ ⊤ →
    c ≠ 0 →
      m₁ ≤ᶠ[nhdsWithin 0 (Set.Ici 0)] c • m₂ → MeasureTheory.Measure.mkMetric m₁ ≤ c • MeasureTheory.Measure.mkMetric m₂
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
/-- The Weierstrass curve in projective coordinates base changed to an algebra `S` over `R`.  -/
WeierstrassCurve.Projective.baseChange : {R : Type r} →
  [inst : CommRing R] →
    WeierstrassCurve.Projective R → (S : Type s) → [inst_1 : CommRing S] → [Algebra R S] → WeierstrassCurve.Projective S
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
CategoryTheory.Free.embedding_obj : ∀ (R : Type u_1) [inst : CommRing R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C] (X : C),
  (CategoryTheory.Free.embedding R C).obj X = X
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleRange_zero : ∀ (n : ℕ) [inst : NeZero n], Fin.cycleRange 0 = 1
-- Mathlib.Data.Seq.Basic
Stream'.Seq.ofList_toList : ∀ {α : Type u} (s : Stream'.Seq α) (h : s.Terminates), ↑(s.toList h) = s
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
Pi.conditionallyCompleteLattice : {ι : Type u_5} →
  {α : ι → Type u_6} → [(i : ι) → ConditionallyCompleteLattice (α i)] → ConditionallyCompleteLattice ((i : ι) → α i)
-- Mathlib.Probability.Process.LocalProperty
_private.Mathlib.Probability.Process.LocalProperty.0.ProbabilityTheory.le_mkStrictMonoAux : ∀ (x : ℕ → ℕ) (n : ℕ), x n ≤ ProbabilityTheory.mkStrictMonoAux✝ x n
-- Mathlib.Algebra.Group.ULift
ULift.smul_down : ∀ {α : Type u} {β : Type v} [inst : SMul β α] (a : ULift.{w, u} α) (b : β), (b • a).down = b • a.down
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.Tendsto.eventually_ge_atTop : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] {f : α → β} {l : Filter α},
  Filter.Tendsto f l Filter.atTop → ∀ (c : β), ∀ᶠ (x : α) in l, c ≤ f x
-- Mathlib.GroupTheory.QuotientGroup.Basic
MonoidHom.domRestrictHomKerEquiv_symm_coe_apply : ∀ {G : Type u} [inst : Group G] (A : Type u_1) [inst_1 : CommGroup A] (H : Subgroup G) [inst_2 : H.Normal]
  (f : G ⧸ H →* A) (g : G), ↑((MonoidHom.domRestrictHomKerEquiv A H).symm f) g = f ↑g
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.polynomialY.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R),
  W'.polynomialY = (MvPolynomial.pderiv 1) W'.polynomial
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableSet_preimage_up : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set (ULift.{u_6, u_1} α)},
  MeasurableSet (ULift.up ⁻¹' s) ↔ MeasurableSet s
-- Init.Data.String.Lemmas.Iterate
String.Slice.Pos.Splits.mem_toList_right_iff : ∀ {s : String.Slice} {pos : s.Pos} {t u : String} {c : Char},
  pos.Splits t u → (c ∈ u.toList ↔ ∃ pos', ∃ (_ : pos ≤ pos') (h : pos' ≠ s.endPos), pos'.get h = c)
-- Std.Data.DTreeMap.Raw.Basic
/-- Returns `true` if there is a mapping for the given key `a` or a key that is equal to `a` according
to the comparator `cmp`. There is also a `Prop`-valued version
of this: `a ∈ t` is equivalent to `t.contains a = true`.

Observe that this is different behavior than for lists: for lists, `∈` uses `=` and `contains` uses
`==` for equality checks, while for tree maps, both use the given comparator `cmp`.
 -/
Std.DTreeMap.Raw.contains : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → Bool
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.map_add : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : DistribMulAction M A] {B : Type u_5} [inst_4 : AddMonoid B] [inst_5 : DistribMulAction N B] (f : A →ₑ+[φ] B)
  (x y : A), f (x + y) = f x + f y
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
VectorFourier.fourierSMulRight_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) (f : V → E) (v : V) (w : W),
  (VectorFourier.fourierSMulRight L f v) w = -(2 * ↑Real.pi * Complex.I) • (L v) w • f v
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β},
  k ∉ m₁ → Std.ExtDHashMap.Const.getD (m₁ \ m₂) k fallback = fallback
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_diff_le_size_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], (m₁ \ m₂).size ≤ m₁.size
-- Lean.Meta.Match.MatcherInfo
/-- Information about the structure of a matcher declaration
 -/
Lean.Meta.Match.MatcherInfo : Type
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.coe_mk : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ P₂) (e' : V₁ ≃ₗ[k] V₂)
  (h : ∀ (p : P₁) (v : V₁), e (v +ᵥ p) = e' v +ᵥ e p), ⇑{ toEquiv := e, linear := e', map_vadd' := h } = ⇑e
-- Mathlib.GroupTheory.Subsemigroup.Center
/-- The center of an additive magma is commutative and associative.  -/
AddSubsemigroup.center.addCommSemigroup : {M : Type u_1} → [inst : Add M] → AddCommSemigroup ↥(AddSubsemigroup.center M)
-- Mathlib.LinearAlgebra.Orientation
/-- Given a basis, any orientation equals the orientation given by that basis or its negation.  -/
Module.Basis.orientation_eq_or_eq_neg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_3} [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  (e : Module.Basis ι R M) (x : Orientation R M ι), x = e.orientation ∨ x = -e.orientation
-- Mathlib.Data.Fin.Tuple.Sort
Equiv.Perm.monotone_iff : ∀ {n : ℕ} (σ : Equiv.Perm (Fin n)), Monotone ⇑σ ↔ σ = 1
-- Mathlib.Data.Set.FiniteExhaustion
Set.FiniteExhaustion.iUnion_eq : ∀ {α : Type u_1} {s : Set α} (K : s.FiniteExhaustion), ⋃ n, K n = s
-- Init.Data.UInt.Lemmas
UInt64.toNat_add : ∀ (a b : UInt64), (a + b).toNat = (a.toNat + b.toNat) % 2 ^ 64
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_left_idem : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), s ∪ (s ∪ t) = s ∪ t
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.replicateCol.eq_1 : ∀ {m : Type u_2} {α : Type v} (ι : Type u_6) (w : m → α), Matrix.replicateCol ι w = Matrix.of fun x x_1 => w x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  m.WF →
    ∀ {l : List α} {k k' : α},
      (k == k') = true →
        k ∉ m →
          List.Pairwise (fun a b => (a == b) = false) l →
            k ∈ l → (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l).getKey! k' = k
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.isUniformInducing : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} [inst_2 : Fact (1 ≤ p)], IsUniformInducing Subtype.val
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
CategoryTheory.JointlyReflectIsomorphisms.exactAt_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{v_2, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  CategoryTheory.JointlyReflectIsomorphisms F →
    ∀ [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
      [inst_3 : (i : I) → CategoryTheory.Limits.HasZeroMorphisms (D i)]
      [inst_4 : ∀ (i : I), (F i).PreservesZeroMorphisms] [CategoryTheory.CategoryWithHomology C]
      [∀ (i : I), (F i).PreservesHomology] [CategoryTheory.Limits.HasZeroObject C] {α : Type u_4} {c : ComplexShape α}
      (K : HomologicalComplex C c) (a : α), K.ExactAt a ↔ ∀ (i : I), (((F i).mapHomologicalComplex c).obj K).ExactAt a
-- Mathlib.Algebra.Homology.Homotopy
/-- An auxiliary construction for `mkInductive`.
 -/
Homotopy.mkInductiveAux₂ : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {P Q : ChainComplex V ℕ} →
        (e : P ⟶ Q) →
          (zero : P.X 0 ⟶ Q.X 1) →
            e.f 0 = CategoryTheory.CategoryStruct.comp zero (Q.d 1 0) →
              (one : P.X 1 ⟶ Q.X 2) →
                e.f 1 =
                    CategoryTheory.CategoryStruct.comp (P.d 1 0) zero +
                      CategoryTheory.CategoryStruct.comp one (Q.d 2 1) →
                  ((n : ℕ) →
                      (p :
                          (f : P.X n ⟶ Q.X (n + 1)) ×'
                            (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
                              e.f (n + 1) =
                                CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f +
                                  CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) →
                        (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
                          e.f (n + 2) =
                            CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst +
                              CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2))) →
                    (n : ℕ) →
                      (f : HomologicalComplex.xNext P n ⟶ Q.X n) ×'
                        (f' : P.X n ⟶ HomologicalComplex.xPrev Q n) ×'
                          e.f n =
                            CategoryTheory.CategoryStruct.comp (HomologicalComplex.dFrom P n) f +
                              CategoryTheory.CategoryStruct.comp f' (HomologicalComplex.dTo Q n)
-- Mathlib.Topology.Sion
_private.Mathlib.Topology.Sion.0.Sion.setOfPred_sublevelLeft_subset.eq_1 : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} [inst : LinearOrder β] (X : Set E) (Y : Set F) (f : E → F → β)
  [inst_1 : AddCommGroup F] [inst_2 : Module ℝ F] (b b' : β) (y y' : ↑Y),
  Sion.setOfPred_sublevelLeft_subset✝ X Y f b b' y y' = {z | Sion.sublevelLeft✝ X f b ↑z ⊆ Sion.sublevelLeft✝ X f b' ↑y}
-- Mathlib.CategoryTheory.Join.Basic
/-- Characterizing `mapPair` on left morphisms.  -/
CategoryTheory.Join.mapPairLeft : {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] →
            {E' : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] →
                (Fₗ : CategoryTheory.Functor C E) →
                  (Fᵣ : CategoryTheory.Functor D E') →
                    (CategoryTheory.Join.inclLeft C D).comp (CategoryTheory.Join.mapPair Fₗ Fᵣ) ≅
                      Fₗ.comp (CategoryTheory.Join.inclLeft E E')
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.Std.Iter.toArray_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β) (out : β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Init.Data.Range.Polymorphic.UInt
UInt32.instHasSize : Std.Rxc.HasSize UInt32
-- Mathlib.Topology.MetricSpace.Holder
HolderOnWith.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y]
  [inst_2 : PseudoEMetricSpace Z] {s : Set X} {Cg rg : NNReal} {g : Y → Z} {t : Set Y},
  HolderOnWith Cg rg g t →
    ∀ {Cf rf : NNReal} {f : X → Y},
      HolderOnWith Cf rf f s → Set.MapsTo f s t → HolderOnWith (Cg * Cf ^ ↑rg) (rg * rf) (g ∘ f) s
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isPrincipal_add_mul_of_isPrincipal_add`. -/
Ordinal.principal_add_mul_of_principal_add : ∀ (a : Ordinal.{u}) {b : Ordinal.{u}},
  b ≠ 1 → Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) b → Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) (a * b)
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.eraseMiddle.eq_1 : ∀ {n : ℕ} (c : OrderedFinpartition (n + 1)) (hc : Set.range (c.emb 0) ≠ {0}),
  c.eraseMiddle hc =
    { length := c.length, partSize := Function.update c.partSize (c.index 0) (c.partSize (c.index 0) - 1),
      partSize_pos := ⋯,
      emb := fun i j =>
        if h : i = c.index 0 then (c.emb i (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb i (Fin.cast ⋯ j)).pred ⋯,
      emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.HasZeroObject.to_zero_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C] {X : C}
  {f g : X ⟶ 0}, f = g ↔ True
-- Mathlib.Analysis.Normed.Operator.Prod
/-- `ContinuousLinearMap.prodMap` as a continuous linear map.  -/
ContinuousLinearMap.prodMapL : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    (M₁ : Type u_5) →
      (M₂ : Type u_6) →
        (M₃ : Type u_7) →
          (M₄ : Type u_8) →
            [inst_1 : SeminormedAddCommGroup M₁] →
              [inst_2 : NormedSpace 𝕜 M₁] →
                [inst_3 : SeminormedAddCommGroup M₂] →
                  [inst_4 : NormedSpace 𝕜 M₂] →
                    [inst_5 : SeminormedAddCommGroup M₃] →
                      [inst_6 : NormedSpace 𝕜 M₃] →
                        [inst_7 : SeminormedAddCommGroup M₄] →
                          [inst_8 : NormedSpace 𝕜 M₄] → (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.getPatternsVarsEx : Array Lean.Syntax → Lean.Elab.TermElabM (Array Lean.Elab.Term.Do.Var)
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.insert_Ioc_left_eq_Ioc_sub_one_of_not_isMin : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Sub α]
  [PredSubOrder α] {a b : α}, a ≤ b → ¬IsMin a → insert a (Finset.Ioc a b) = Finset.Ioc (a - 1) b
-- Mathlib.Order.Disjoint
Disjoint.mono_left : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b c : α}, a ≤ b → Disjoint b c → Disjoint a c
-- Mathlib.Data.NNReal.Defs
NNReal.coe_ne_zero : ∀ {r : NNReal}, ↑r ≠ 0 ↔ r ≠ 0
-- Mathlib.NumberTheory.Height.NumberField
/-- **Alias** of `NumberField.finite_setOfPred_prod_infinitePlace_iSup_le`. -/
NumberField.finite_setOf_prod_infinitePlace_iSup_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {n : ℕ},
  n ≠ 0 → ∀ (B : ℝ), {x | ∏ v, (⨆ i, v (![↑x, ↑n] i)) ^ v.mult ≤ B}.Finite
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
/-- The Haar measure equals the Lebesgue measure on `ℝ^ι`.  -/
MeasureTheory.addHaarMeasure_eq_volume_pi : ∀ (ι : Type u_1) [inst : Fintype ι],
  MeasureTheory.Measure.addHaarMeasure (TopologicalSpace.PositiveCompacts.piIcc01 ι) = MeasureTheory.volume
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.neighborFinset_bot : ∀ {V : Type u_1} (v : V) [inst : Fintype ↑(⊥.neighborSet v)], ⊥.neighborFinset v = ∅
-- Mathlib.GroupTheory.MonoidLocalization.Order
AddLocalization.lt : {α : Type u_1} →
  [inst : AddCommMonoid α] →
    [inst_1 : PartialOrder α] → [IsOrderedCancelAddMonoid α] → {s : AddSubmonoid α} → LT (AddLocalization s)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instSeminormedAddCommGroup : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : SeminormedAddCommGroup β] → SeminormedAddCommGroup (BoundedContinuousFunction α β)
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.below.prec : ∀ {motive : (a : ℕ → ℕ) → Nat.Primrec a → Prop} {f g : ℕ → ℕ} (a : Nat.Primrec f) (a_1 : Nat.Primrec g),
  Nat.Primrec.below a → motive f a → Nat.Primrec.below a_1 → motive g a_1 → Nat.Primrec.below ⋯
-- Mathlib.RingTheory.Nullstellensatz
MvPolynomial.eq_vanishingIdeal_singleton_of_isMaximal : ∀ {k : Type u_1} (K : Type u_2) [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Type u_3}
  [IsAlgClosed K] [Finite σ] {I : Ideal (MvPolynomial σ k)}, I.IsMaximal → ∃ x, I = MvPolynomial.vanishingIdeal k {x}
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.insertListIfNewUnit.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (hd : α) → (tl : List α) → motive (hd :: tl)),
  (match [] with
    | [] => h_1 ()
    | hd :: tl => h_2 hd tl) =
    h_1 ()
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rcc_eq_push : ∀ {m n : ℕ}, m ≤ n → (m...=n).toArray = (m...n).toArray.push n
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.AdicCauchySequence.instSub : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u_4) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Sub (AdicCompletion.AdicCauchySequence I M)
-- Batteries.Data.String.Lemmas
String.Pos.Raw.extract.go₁_add_right_cancel : ∀ (s : List Char) (i b e n : ℕ),
  String.Pos.Raw.extract.go₁ s { byteIdx := i + n } { byteIdx := b + n } { byteIdx := e + n } =
    String.Pos.Raw.extract.go₁ s { byteIdx := i } { byteIdx := b } { byteIdx := e }
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, panicking if no such pair exists.
 -/
Std.DTreeMap.getEntryLE! : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited (Sigma β)] → Std.DTreeMap α β cmp → α → (a : α) × β a
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
/-- `riemannZeta₁ s` is the completion of `(s-1) * riemannZeta s` at `s = 1`.  -/
riemannZeta₁ : ℂ → ℂ
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsIsoAppTruncGEπOfIsGE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (n : ℤ) [t.IsGE X n],
  CategoryTheory.IsIso ((t.truncGEπ n).app X)