mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Real.sphere_eq_pair : ∀ (x : ℝ) {r : ℝ}, 0 ≤ r → Metric.sphere x r = {x - r, x + r}
-- Mathlib.CategoryTheory.Triangulated.Generators
CategoryTheory.ObjectProperty.triangEnvelope.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C), P.triangEnvelope = ⨆ n, P.triangEnvelopeIter n
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
mdifferentiableWithinAt_iff' : ∀ {𝕜 : 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'] (f : M → M') (s : Set M) (x : M),
  MDiffAt[s] f x ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I)
        (↑(extChartAt I x) x)
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
AddSubsemigroup.instIsAddCommutative_closure : ∀ (M : Type u_1) [inst : AddSemigroup M] {S : Type u_2} [inst_1 : SetLike S M] [inst_2 : AddMemClass S M] (s : S)
  [IsAddCommutative ↥s], IsAddCommutative ↥(AddSubsemigroup.closure ↑s)
-- Mathlib.Order.BourbakiWitt
NonemptyChain.Nonempty' : ∀ {α : Type u_4} [inst : LE α] (self : NonemptyChain α), self.carrier.Nonempty
-- Std.Internal.Parsec.ByteArray
/-- Parse a string by matching its UTF-8 bytes, returns the string on success.
 -/
Std.Internal.Parsec.ByteArray.pstring : String → Std.Internal.Parsec.ByteArray.Parser String
-- Init.Data.SInt.Lemmas
ISize.toInt64_ne_neg_one : ∀ (a : ISize), a ≠ -1 → a.toInt64 ≠ -1
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.pow' : ∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] {S : Type u_17} [inst_1 : NormedRing S] [NormMulClass S]
  {c : ℝ} {l : Filter α} [NormOneClass S] {f : α → R} {g : α → S},
  Asymptotics.IsBigOWith c l f g →
    ∀ (n : ℕ), Asymptotics.IsBigOWith (Nat.casesOn n ‖1‖ fun n => c ^ (n + 1)) l (fun x => f x ^ n) fun x => g x ^ n
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.Context.subExpr : Lean.PrettyPrinter.Delaborator.Context → Lean.SubExpr
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
SemiSimplexCategory.homEquiv_id : ∀ (a : SemiSimplexCategory),
  SemiSimplexCategory.homEquiv (CategoryTheory.CategoryStruct.id a) = RelEmbedding.refl fun x1 x2 => x1 ≤ x2
-- Lean.Language.Lean.Types
Lean.Language.Lean.CommandElaboratingSnapshot.mk : Lean.Language.Snapshot →
  Lean.Language.SnapshotTask Lean.Language.DynamicSnapshot →
    Lean.Language.SnapshotTask Lean.Language.Lean.CommandResultSnapshot →
      Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf →
        Lean.Language.SnapshotTask Lean.Language.SnapshotTree → Lean.Language.Lean.CommandElaboratingSnapshot
-- Mathlib.Geometry.Manifold.Notation
/-- `tangentMap[s] f` elaborates to `tangentMapWithin I J f s`,
trying to determine `I` and `J` from the local context.  -/
Manifold.«termTangentMap[_]__» : Lean.ParserDescr
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.IsSymmetric.rename : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] {φ : MvPolynomial σ R},
  φ.IsSymmetric → ∀ (e : σ ≃ τ), ((MvPolynomial.rename ⇑e) φ).IsSymmetric
-- Lean.Meta.Basic
/-- Key for the function information cache.
 -/
Lean.Meta.InfoCacheKey : Type
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.exists_isPathGraph3Compl_of_not_isCompleteMultipartite : ∀ {α : Type u} {G : SimpleGraph α}, ¬G.IsCompleteMultipartite → ∃ v w₁ w₂, G.IsPathGraph3Compl v w₁ w₂
-- Init.Core
Exists.of_psigma_prop : ∀ {α : Sort u} {p : α → Prop} (a : (x : α) ×' p x), ∃ x, p x
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Wequiv.ind : ∀ {F : Type u → Type v} [q : QPF F] (a : (QPF.P F).A) (f f' : (QPF.P F).B a → (QPF.P F).W),
  (∀ (x : (QPF.P F).B a), QPF.Wequiv (f x) (f' x)) → QPF.Wequiv (WType.mk a f) (WType.mk a f')
-- Mathlib.Algebra.Order.ToIntervalMod
_private.Mathlib.Algebra.Order.ToIntervalMod.0.toIxxMod_antisymm : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {a b c : α},
  toIcoMod hp a b ≤ toIocMod hp a c →
    toIcoMod hp a c ≤ toIocMod hp a b → b ≡ a [PMOD p] ∨ c ≡ b [PMOD p] ∨ a ≡ c [PMOD p]
-- Mathlib.CategoryTheory.Limits.MonoCoprod
/-- The binary cofan `binaryCofanSum c c₁ c₂ hc₁ hc₂` is colimit.  -/
CategoryTheory.Limits.MonoCoprod.isColimitBinaryCofanSum : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {I₁ : Type u_2} →
      {I₂ : Type u_3} →
        {X : I₁ ⊕ I₂ → C} →
          (c : CategoryTheory.Limits.Cofan X) →
            (c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl)) →
              (c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)) →
                CategoryTheory.Limits.IsColimit c →
                  (hc₁ : CategoryTheory.Limits.IsColimit c₁) →
                    (hc₂ : CategoryTheory.Limits.IsColimit c₂) →
                      CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.MonoCoprod.binaryCofanSum c c₁ c₂ hc₁ hc₂)
-- Mathlib.CategoryTheory.Generator.StrongGenerator
CategoryTheory.ObjectProperty.IsStrongGenerator.mk_of_exists_extremalEpi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C},
  (∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, CategoryTheory.ExtremalEpi p) → P.IsStrongGenerator
-- Mathlib.Analysis.LocallyConvex.AbsConvexOpen
gaugeSeminormFamily.congr_simp : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] [inst_4 : Module ℝ E] [inst_5 : IsScalarTower ℝ 𝕜 E] [inst_6 : ContinuousSMul ℝ E]
  (a a_1 : AbsConvexOpenSets 𝕜 E), a = a_1 → gaugeSeminormFamily 𝕜 E a = gaugeSeminormFamily 𝕜 E a_1
-- Mathlib.Topology.Algebra.Monoid
Subsemigroup.separatelyContinuousMul : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Semigroup M] [SeparatelyContinuousMul M] (S : Subsemigroup M),
  SeparatelyContinuousMul ↥S
-- Lean.Elab.DeclModifiers
Lean.Elab.instInhabitedModifiers : Inhabited Lean.Elab.Modifiers
-- Mathlib.Order.Interval.Set.Defs
Set.Ici.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (b : α), Set.Ici b = {x | b ≤ x}
-- Mathlib.FieldTheory.RatFunc.Basic
/-- `RatFunc.num` is the numerator of a rational function,
normalized such that the denominator is monic.  -/
RatFunc.num : {K : Type u} → [inst : Field K] → RatFunc K → Polynomial K
-- Mathlib.Analysis.Normed.Group.Basic
dist_indicator : ∀ {α : Type u_2} {E : Type u_5} [inst : SeminormedAddGroup E] (s t : Set α) (f : α → E) (x : α),
  dist (s.indicator f x) (t.indicator f x) = ‖(symmDiff s t).indicator f x‖
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveTermGoal.mk : Lean.Widget.InteractiveGoalCore →
  Lean.Lsp.Range → Lean.Server.WithRpcRef Lean.Elab.TermInfo → Lean.Widget.InteractiveTermGoal
-- Mathlib.RingTheory.LaurentSeries
/-- Since extracting coefficients is uniformly continuous, every Cauchy filter in
`K⸨X⸩` gives rise to a Cauchy filter in `K` for every `d : ℤ`, and such Cauchy filter
in `K` converges to a principal filter  -/
LaurentSeries.Cauchy.coeff : {K : Type u_2} → [inst : Field K] → {ℱ : Filter (LaurentSeries K)} → Cauchy ℱ → ℤ → K
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
HasProd.mul_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a b : α}
  [ContinuousMul α] {s : Set β}, HasProd (f ∘ Subtype.val) a → HasProd (f ∘ Subtype.val) b → HasProd f (a * b)
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Pythagorean theorem, if-and-only-if vector inner product form.  -/
norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F),
  ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ inner ℝ x y = 0
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteS.eq_7 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (a b : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.Expr.denoteS ctx (a.sub b) = 0
-- Mathlib.Data.Part
Part.map_id' : ∀ {α : Type u_1} {f : α → α}, (∀ (x : α), f x = x) → ∀ (o : Part α), Part.map f o = o
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.finitaryExtensive : ∀ {P : TopCat → Prop} [CompHausLike.HasExplicitFiniteCoproducts P],
  (∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B),
      Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f) → CompHausLike.HasExplicitPullback f g) →
    CategoryTheory.FinitaryExtensive (CompHausLike P)
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
QuadraticModuleCat.hom_hom_associator : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Invertible 2] {M N K : QuadraticModuleCat R},
  QuadraticModuleCat.Hom.toIsometry (CategoryTheory.MonoidalCategoryStruct.associator M N K).hom =
    (M.form.tensorAssoc N.form K.form).toIsometry
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.exs.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} (φ : L.BoundedFormula α 0), φ.exs = φ
-- Mathlib.Analysis.Normed.Module.Ball.Action
ne_neg_of_mem_sphere : ∀ (𝕜 : Type u_1) {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
  [CharZero 𝕜] {r : ℝ}, r ≠ 0 → ∀ (x : ↑(Metric.sphere 0 r)), x ≠ -x
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
AddChar.zmodChar_apply' : ∀ {C : Type v} [inst : CommMonoid C] {n : ℕ} [inst_1 : NeZero n] {ζ : C} (hζ : ζ ^ n = 1) (a : ℕ),
  (AddChar.zmodChar n hζ) ↑a = ζ ^ a
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.instMin : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Min α] → [inst_1 : Top α] → [inst_2 : SemilatticeInf β] → [inst_3 : OrderTop β] → Min (InfTopHom α β)
-- Std.Tactic.Do.Syntax
/-- `mreplace` is like `replace`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
  mintro HP HPQ
  mreplace HPQ : Q := by mspecialize HPQ HP; mexact HPQ
  mexact HPQ
```
 -/
Lean.Parser.Tactic.mreplaceError : Lean.ParserDescr
-- Mathlib.MeasureTheory.Measure.Lebesgue.Complex
Complex.volume_preserving_equiv_real_prod : MeasureTheory.MeasurePreserving (⇑Complex.measurableEquivRealProd) MeasureTheory.volume MeasureTheory.volume
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Functor.mapCommMon_obj_mon_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.Functor C D) [inst_6 : F.LaxBraided] (A : CategoryTheory.CommMon C),
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F A.X A.X)
      (F.map CategoryTheory.MonObj.mul)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.relMap_sumInr : ∀ {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} {S : Type u_3} [inst : L₁.Structure S] [inst_1 : L₂.Structure S]
  {n : ℕ} (R : L₂.Relations n),
  FirstOrder.Language.Structure.RelMap (Sum.inr R) = FirstOrder.Language.Structure.RelMap R
-- Init.Data.BitVec.Bitblast
BitVec.aandRec.eq_1 : ∀ {w : ℕ} (x y : BitVec w) (s : ℕ) (hs : s < w), x.aandRec y s hs = (y[s] && x.uppcRec s hs)
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientAt.hasDerivAt' : ∀ {g : ℝ → ℝ} {g' u : ℝ}, HasGradientAt g g' u → HasDerivAt g g' u
-- Mathlib.Algebra.Category.Ring.Constructions
/-- The limit cone of the tensor product `A ⊗[ℤ] B` in `CommRingCat`.  -/
CommRingCat.coproductColimitCocone : (A B : CommRingCat) → CategoryTheory.Limits.ColimitCocone (CategoryTheory.Limits.pair A B)
-- Mathlib.Topology.Order.DenselyOrdered
frontier_Iic' : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α},
  (Set.Ioi a).Nonempty → frontier (Set.Iic a) = {a}
-- Batteries.Control.Nondet.Basic
/-- Find the first alternative in a nondeterministic value, as a monadic value.
 -/
Nondet.head : {σ : Type} → {m : Type → Type} → [AlternativeMonad m] → [inst : Lean.MonadBacktrack σ m] → {α : Type} → Nondet m α → m α
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.union_insert_right_equiv_insert_union : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {p : (a : α) × β a}, (m₁ ∪ m₂.insert p.fst p.snd).Equiv ((m₁ ∪ m₂).insert p.fst p.snd)
-- Mathlib.Data.Finsupp.Basic
Finsupp.uncurry_curry : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α × β →₀ M), f.curry.uncurry = f
-- Mathlib.Algebra.GroupWithZero.Shrink
instSemigroupWithZeroShrink : {α : Type u_2} → [inst : Small.{v, u_2} α] → [SemigroupWithZero α] → SemigroupWithZero (Shrink.{v, u_2} α)
-- Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
HomotopicalAlgebra.bijective_leftHomotopyClassToHom_iff_bijective_rightHomotopyClassToHom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {H : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} H] (L : CategoryTheory.Functor C H)
  [inst_3 : L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)] (X Y : C) [HomotopicalAlgebra.IsCofibrant X]
  [HomotopicalAlgebra.IsFibrant Y],
  Function.Bijective (HomotopicalAlgebra.leftHomotopyClassToHom L) ↔
    Function.Bijective (HomotopicalAlgebra.rightHomotopyClassToHom L)
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.instPreservesColimitsOfShapeπ₃ : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasColimitsOfShape J C],
  CategoryTheory.Limits.PreservesColimitsOfShape J CategoryTheory.ShortComplex.π₃
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.IsLoop.eRk_eq : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsLoop e → M.eRk {e} = 0
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `strictAnti_toDual_comp_iff`. -/
StrictMono.dual_right : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  StrictMono f → StrictAnti (⇑OrderDual.toDual ∘ f)
-- Lean.Meta.Sym.Simp.SimpM
/-- Like `mkRflResult` with `done := false`.  -/
Lean.Meta.Sym.Simp.mkRflResultCD : Bool → Lean.Meta.Sym.Simp.Result
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.eqToHom_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {X Y : CategoryTheory.StructuredArrow S T} (h : X = Y),
  CategoryTheory.StructuredArrow.Hom.right (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom ⋯
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentChange.delete.inj : ∀ {a a_1 : Lean.Lsp.DeleteFile}, Lean.Lsp.DocumentChange.delete a = Lean.Lsp.DocumentChange.delete a_1 → a = a_1
-- Mathlib.Data.Stream.Init
Stream'.mem_iff_exists_get_eq : ∀ {α : Type u} {s : Stream' α} {a : α}, a ∈ s ↔ ∃ n, a = s.get n
-- Mathlib.Data.ZMod.IntUnitsPower
/-- This is an indirect way of saying that `ℤˣ` has a power operation by `ZMod 2`.  -/
instModuleZModOfNatNatAdditiveUnitsInt : Module (ZMod 2) (Additive ℤˣ)
-- Lean.Data.Json.Basic
Lean.JsonNumber.toFloat : Lean.JsonNumber → Float
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.root_sub_zsmul_mem_range_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  LinearIndependent R ![P.root i, P.root j] →
    ∀ {z : ℤ},
      P.root j - z • P.root i ∈ Set.range ⇑P.root ↔
        z ∈ Set.Icc (-↑(RootPairing.chainTopCoeff i j)) ↑(RootPairing.chainBotCoeff i j)
-- Mathlib.Algebra.Order.Ring.Pow
/-- Bernoulli's inequality for `b / a`, written after multiplication by the denominators.  -/
Commute.pow_add_mul_le_add_pow_of_sq_nonneg : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] {a b : R},
  Commute a b →
    0 ≤ a → 0 ≤ b ^ 2 → 0 ≤ (a + b) ^ 2 → 0 ≤ 2 * a + b → ∀ (n : ℕ), a ^ n + ↑n * a ^ (n - 1) * b ≤ (a + b) ^ n
-- Mathlib.MeasureTheory.Function.Holder
ContinuousLinearMap.holderₗ_apply_apply : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {m : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) (p q r : ENNReal) [hpqr : p.HolderTriple q r] [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedAddCommGroup G]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G)
  (m_1 : ↥(MeasureTheory.Lp E p μ)) (g : ↥(MeasureTheory.Lp F q μ)),
  ((ContinuousLinearMap.holderₗ μ p q r B) m_1) g = ContinuousLinearMap.holder r B m_1 g
-- Init.Data.BitVec.Lemmas
/-- The sign extension is a bitwise not, followed by a zero extend, followed by another bitwise not
when `msb = true`. The double bitwise not ensures that the high bits are '1',
and the lower bits are preserved.  -/
BitVec.signExtend_eq_not_setWidth_not_of_msb_true : ∀ {w : ℕ} {x : BitVec w} {v : ℕ}, x.msb = true → BitVec.signExtend v x = ~~~BitVec.setWidth v (~~~x)
-- Mathlib.FieldTheory.RatFunc.Valuation
RatFunc.CompletionAtInfty.instField : (F : Type u_1) → [inst : Field F] → [inst_1 : DecidableEq (RatFunc F)] → Field (RatFunc.CompletionAtInfty F)
-- Mathlib.Analysis.SpecialFunctions.Arcosh
Real.add_sqrt_self_sq_sub_one_inv : ∀ {x : ℝ}, 1 ≤ x → (x + √(x ^ 2 - 1))⁻¹ = x - √(x ^ 2 - 1)
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.constantCoeff_invOfUnit : ∀ {σ : Type u_1} {R : Type u_2} [inst : Ring R] (φ : MvPowerSeries σ R) (u : Rˣ),
  MvPowerSeries.constantCoeff (φ.invOfUnit u) = ↑u⁻¹
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.elabFlatInductiveViews : Array Lean.Expr → Array Lean.Elab.Command.InductiveElabStep1 → Lean.Elab.TermElabM Unit
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
/-- The constructed cone is a limit.  -/
TopCat.pullbackConeIsLimit : {X Y Z : TopCat} → (f : X ⟶ Z) → (g : Y ⟶ Z) → CategoryTheory.Limits.IsLimit (TopCat.pullbackCone f g)
-- Mathlib.Algebra.Group.Subgroup.Even
/-- In an abelian group `G`, `Subgroup.square G` is the subgroup of squares in `G`.
 -/
Subgroup.square : (G : Type u_1) → [inst : CommGroup G] → Subgroup G
-- Mathlib.Computability.TuringMachine.Computable
Turing.TM2ComputableInPolyTime.mk : {α β αΓ βΓ : Type} →
  {ea : α → List αΓ} →
    {eb : β → List βΓ} →
      {f : α → β} →
        (toTM2ComputableAux : Turing.TM2ComputableAux αΓ βΓ) →
          (time : Polynomial ℕ) →
            ((a : α) →
                Turing.TM2OutputsInTime toTM2ComputableAux.tm (List.map toTM2ComputableAux.inputAlphabet.invFun (ea a))
                  (some (List.map toTM2ComputableAux.outputAlphabet.invFun (eb (f a))))
                  (Polynomial.eval (ea a).length time)) →
              Turing.TM2ComputableInPolyTime ea eb f
-- Mathlib.Algebra.Group.Action.Defs
/-- `SMul` version of `one_mul_eq_id`  -/
one_smul_eq_id : ∀ (M : Type u_1) {α : Type u_5} [inst : Monoid M] [inst_1 : MulAction M α], (fun x => 1 • x) = id
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_add_one : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R),
  Int.fract (a + 1) = Int.fract a
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- A finite rank torsion-free module has positive `finrank` iff it has a nonzero element.  -/
Module.finrank_pos_iff_exists_ne_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Finite R M] [IsDomain R] [Module.IsTorsionFree R M], 0 < Module.finrank R M ↔ ∃ x, x ≠ 0
-- Mathlib.NumberTheory.EulerProduct.Basic
/-- The *Euler Product* for completely multiplicative functions.

If `f : ℕ →*₀ F`, where `F` is a complete normed field and `‖f ·‖` is summable, then
`∏' p : Nat.Primes, (1 - f p)⁻¹ = ∑' n, f n`.
This version is stated in the form of convergence of finite partial products.  -/
EulerProduct.eulerProduct_completely_multiplicative : ∀ {F : Type u_1} [inst : NormedField F] [CompleteSpace F] {f : ℕ →*₀ F},
  (Summable fun x => ‖f x‖) →
    Filter.Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - f p)⁻¹) Filter.atTop (nhds (∑' (n : ℕ), f n))
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrix₂_comp : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {M₁' : Type u_8} {n : Type u_11} {m : Type u_12} {n' : Type u_13}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : Fintype n] [inst_6 : Fintype m] [inst_7 : DecidableEq m] [inst_8 : DecidableEq n]
  (b₁ : Module.Basis n R M₁) (b₂ : Module.Basis m R M₂) [inst_9 : AddCommMonoid M₁'] [inst_10 : Module R M₁']
  (b₁' : Module.Basis n' R M₁') [inst_11 : Fintype n'] [inst_12 : DecidableEq n'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R)
  (f : M₁' →ₗ[R] M₁),
  (LinearMap.toMatrix₂ b₁' b₂) (B ∘ₗ f) = ((LinearMap.toMatrix b₁' b₁) f).transpose * (LinearMap.toMatrix₂ b₁ b₂) B
-- Std.Tactic.BVDecide.LRAT.Internal.PosFin
Std.Tactic.BVDecide.LRAT.Internal.instDecidableEqPosFin : {n : ℕ} → DecidableEq (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.ι_mapBifunctor₁₂BifunctorDesc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r}
  {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂}
  {X₃ : CategoryTheory.GradedObject I₃ C₃}
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
              (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
          X₃).HasMap
      ρ₁₂.q]
  [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] {j : J} {A : C₄}
  (f :
    (i₁ : I₁) → (i₂ : I₂) → (i₃ : I₃) → r (i₁, i₂, i₃) = j → ((G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶ A))
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorDesc f) =
    f i₁ i₂ i₃ h
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_ofSurjective : ∀ {R : Type u_1} {R₂ : Type u_2} {E₂ : Type u_6} {F : Type u_9} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E₂] [inst_5 : Module R₂ E₂] [inst_6 : NormedAddCommGroup F] [inst_7 : Module R F]
  (f : F →ₛₗᵢ[σ₁₂] E₂) (hfr : Function.Surjective ⇑f), ⇑(LinearIsometryEquiv.ofSurjective f hfr) = ⇑f