mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Summable.map_iff_of_leftInverse : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L : SummationFilter β} [inst_2 : AddCommMonoid γ] [inst_3 : TopologicalSpace γ] {G : Type u_4} {G' : Type u_5}
  [inst_4 : FunLike G α γ] [AddMonoidHomClass G α γ] [inst_6 : FunLike G' γ α] [AddMonoidHomClass G' γ α] (g : G)
  (g' : G'), Continuous ⇑g → Continuous ⇑g' → Function.LeftInverse ⇑g' ⇑g → (Summable (⇑g ∘ f) L ↔ Summable f L)
-- Mathlib.Algebra.Group.Shrink
Shrink.instAddCommGroup.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : AddCommGroup α],
  Shrink.instAddCommGroup = (equivShrink α).symm.addCommGroup
-- Init.Data.Array.Subarray
/-- The ending index of the region of interest (exclusive).  -/
Std.Slice.Internal.SubarrayData.stop : {α : Type u} → Std.Slice.Internal.SubarrayData α → ℕ
-- Mathlib.Topology.Category.UniformSpace
CpltSepUniformSpace.instInhabited : Inhabited CpltSepUniformSpace
-- Init.Data.Slice.List.Lemmas
List.toList_mkSlice_rco : ∀ {α : Type u_1} {xs : List α} {lo hi : ℕ},
  Std.Slice.toList (Std.Rco.Sliceable.mkSlice xs lo...hi) = List.drop lo (List.take hi xs)
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovary_inv`. -/
Monovary.of_inv : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α]
  [inst_3 : CommGroup β] [inst_4 : PartialOrder β] [IsOrderedMonoid β] {f : ι → α} {g : ι → β},
  Monovary f⁻¹ g⁻¹ → Monovary f g
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_apply : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] (d : n → α) (i j : n),
  Matrix.diagonal d i j = if i = j then d i else 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.insertMany_cons : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} {l : List (α × β)} {k : α}
  {v : β}, Std.DTreeMap.Const.insertMany t ((k, v) :: l) = Std.DTreeMap.Const.insertMany (t.insert k v) l
-- Mathlib.LinearAlgebra.Pi
/-- The projections from a family of modules are linear maps.

Note: this definition would be called `Pi.evalLinearMap` if we followed the pattern established by
`Pi.evalAddHom`, `Pi.evalMonoidHom`, `Pi.evalRingHom`, ...  -/
LinearMap.proj : {R : Type u} →
  {ι : Type x} →
    [inst : Semiring R] →
      {φ : ι → Type i} →
        [inst_1 : (i : ι) → AddCommMonoid (φ i)] →
          [inst_2 : (i : ι) → Module R (φ i)] → (i : ι) → ((i : ι) → φ i) →ₗ[R] φ i
-- Mathlib.AlgebraicGeometry.Over
/-- Given `X.Over S`, this is the bundled object of `Over S`.  -/
AlgebraicGeometry.Scheme.asOver : (X S : AlgebraicGeometry.Scheme) → [X.Over S] → CategoryTheory.Over S
-- Mathlib.Topology.SmallInductiveDimension
instHasSmallInductiveDimensionLTOfIsEmpty : ∀ {X : Type u_1} [inst : TopologicalSpace X] (n : ℕ) [IsEmpty X], HasSmallInductiveDimensionLT X n
-- Mathlib.Analysis.Normed.Lp.lpSpace
Memℓp.star_mem : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)]
  [inst_1 : (i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] {f : (i : α) → E i},
  Memℓp f p → Memℓp (star f) p
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftLeft_succ : ∀ (m : ℤ) (n : ℕ), m <<< (n + 1) = m <<< n * 2
-- Mathlib.Analysis.Calculus.ContDiff.Bounds
norm_iteratedFDerivWithin_clm_apply : ∀ {𝕜 : 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] {G : Type uG}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F →L[𝕜] G} {g : E → F} {s : Set E} {x : E}
  {N : WithTop ℕ∞} {n : ℕ},
  ContDiffOn 𝕜 N f s →
    ContDiffOn 𝕜 N g s →
      UniqueDiffOn 𝕜 s →
        x ∈ s →
          ↑n ≤ N →
            ‖iteratedFDerivWithin 𝕜 n (fun y => (f y) (g y)) s x‖ ≤
              ∑ i ∈ Finset.range (n + 1),
                ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
-- Mathlib.Analysis.Calculus.Deriv.Pow
hasDerivAt_pow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] (n : ℕ) (x : 𝕜), HasDerivAt (fun x => x ^ n) (↑n * x ^ (n - 1)) x
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
/-- **Gram-Schmidt Orthonormalization**:
`gramSchmidtNormed` applied to a linearly independent set of vectors produces an orthonormal
system of vectors.  -/
InnerProductSpace.gramSchmidtNormed_orthonormal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] {f : ι → E},
  LinearIndependent 𝕜 f → Orthonormal 𝕜 (InnerProductSpace.gramSchmidtNormed 𝕜 f)
-- Mathlib.ModelTheory.Syntax
/-- Sends a term with extra variables to a term with constants.  -/
FirstOrder.Language.Term.varsToConstants : {L : FirstOrder.Language} → {α : Type u'} → {γ : Type u_1} → L.Term (γ ⊕ α) → (L.withConstants γ).Term α
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic absolute value on `K` defined as `b` raised to negative `v`-adic
valuation, for some `b` in `ℝ≥0`  -/
IsDedekindDomain.HeightOneSpectrum.adicAbv : {R : Type u_1} →
  [inst : CommRing R] →
    [IsDedekindDomain R] →
      {K : Type u_2} →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [IsFractionRing R K] → IsDedekindDomain.HeightOneSpectrum R → {b : NNReal} → 1 < b → AbsoluteValue K ℝ
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_9.eq_2 : ∀ (motive : Std.Tactic.BVDecide.BVBinOp → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVBinOp.and)
  (h_2 : Unit → motive Std.Tactic.BVDecide.BVBinOp.or) (h_3 : Unit → motive Std.Tactic.BVDecide.BVBinOp.xor)
  (h_4 : Unit → motive Std.Tactic.BVDecide.BVBinOp.add) (h_5 : Unit → motive Std.Tactic.BVDecide.BVBinOp.mul)
  (h_6 : Unit → motive Std.Tactic.BVDecide.BVBinOp.udiv) (h_7 : Unit → motive Std.Tactic.BVDecide.BVBinOp.umod),
  (match Std.Tactic.BVDecide.BVBinOp.or with
    | Std.Tactic.BVDecide.BVBinOp.and => h_1 ()
    | Std.Tactic.BVDecide.BVBinOp.or => h_2 ()
    | Std.Tactic.BVDecide.BVBinOp.xor => h_3 ()
    | Std.Tactic.BVDecide.BVBinOp.add => h_4 ()
    | Std.Tactic.BVDecide.BVBinOp.mul => h_5 ()
    | Std.Tactic.BVDecide.BVBinOp.udiv => h_6 ()
    | Std.Tactic.BVDecide.BVBinOp.umod => h_7 ()) =
    h_2 ()
-- Mathlib.RingTheory.Etale.StandardEtale
Algebra.instIsStandardEtaleRing : ∀ {R : Type u_1} [inst : CommRing R] (P : StandardEtalePair R), Algebra.IsStandardEtale R P.Ring
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.foldlM_list_const_inv : ∀ {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {ps : Std.Do.PostShape} [inst : Monad m]
  [inst_1 : Std.Do.WPMonad m ps] {xs : List α} {init : β} {f : β → α → m β} {inv : Std.Do.PostCond β ps},
  (∀ (hd : α) (b : β), ⦃inv.1 b⦄ f b hd ⦃(fun b' => inv.1 b', inv.2)⦄) → ⦃inv.1 init⦄ List.foldlM f init xs ⦃inv⦄
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_eq_isSome_get? : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α},
  m.contains a = (m.get? a).isSome
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- Rotation by π is negation.  -/
Orientation.rotation_pi : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)), o.rotation ↑Real.pi = LinearIsometryEquiv.neg ℝ
-- Mathlib.Algebra.Ring.Prod
RingHom.instRingHomSurjectiveProdFst : ∀ (R : Type u_6) (S : Type u_7) [inst : Semiring R] [inst_1 : Semiring S], RingHomSurjective (RingHom.fst R S)
-- Mathlib.Algebra.Ring.Subsemiring.Defs
RingHom.domRestrict_apply : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {σR : Type u_1}
  [inst_2 : SetLike σR R] [inst_3 : SubsemiringClass σR R] (f : R →+* S) {s : σR} (x : ↥s), (f.domRestrict s) x = f ↑x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getKey!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, t₁.Equiv t₂ → t₁.getKey! k = t₂.getKey! k
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Mon C),
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A) =
    CategoryTheory.MonObj.one
-- Mathlib.Algebra.Lie.Matrix
Matrix.instLieRingModuleForall : {R : Type u} →
  [inst : CommRing R] →
    {n : Type w} → [inst_1 : DecidableEq n] → [inst_2 : Fintype n] → LieRingModule (Matrix n n R) (n → R)
-- Mathlib.Topology.Constructions
/-- **Alias** of `IsOpenMap.domRestrict`. -/
IsOpenMap.restrict : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsOpenMap f → ∀ {s : Set X}, IsOpen s → IsOpenMap (s.domRestrict f)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Multiplicative.toAdd.eq_1 : ∀ {α : Type u}, Multiplicative.toAdd = Multiplicative.ofAdd.symm
-- Batteries.Tactic.Lint.Simp
/-- The thing to replace  -/
Batteries.Tactic.Lint.SimpTheoremInfo.lhs : Batteries.Tactic.Lint.SimpTheoremInfo → Lean.Expr
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_filter_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {f : (a : α) → β a → Bool},
  m.WF → ((Std.DHashMap.Raw.filter f m).isEmpty = true ↔ ∀ (k : α) (h : k ∈ m), f k (m.get k h) = false)
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.BinaryInput_invert_rhs : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} (input : aig.BinaryInput)
  (linv rinv : Bool),
  (input.invert linv rinv).rhs = { gate := input.rhs.gate, invert := rinv ^^ input.rhs.invert, hgate := ⋯ }
-- Lean.Elab.Term.TermElabM
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.elabImplicitLambda.loop : Lean.Syntax → Bool → Lean.Expr → Array Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- A subset closed under the scalar action inherits that action.  -/
SetLike.smul' : {S : Type u'} →
  {M : Type v} →
    {N : Type u_1} →
      {α : Type u_2} →
        [inst : SetLike S α] →
          [inst_1 : SMul M N] →
            [inst_2 : SMul M α] →
              [inst_3 : Monoid N] →
                [inst_4 : MulAction N α] → [SMulMemClass S N α] → [IsScalarTower M N α] → (s : S) → SMul M ↥s
-- Mathlib.Topology.Maps.Strict.Basic
/-- A homeomorphism is a strict map.  -/
IsHomeomorph.isStrictMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f → Topology.IsStrictMap f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.hasPullback_of_right_factors_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Z : C} (f : X ⟶ Z) (i : Z ⟶ W) [CategoryTheory.Mono i],
  CategoryTheory.Limits.HasPullback i (CategoryTheory.CategoryStruct.comp f i)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.coe_tanPartialHomeomorph : ↑Real.tanPartialHomeomorph = Real.tan
-- Mathlib.Analysis.Subadditive
/-- The limit of a bounded-below subadditive sequence. The fact that the sequence indeed tends to
this limit is given in `Subadditive.tendsto_lim`  -/
Subadditive.lim : {u : ℕ → ℝ} → Subadditive u → ℝ
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Walk.reachable : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), G.Reachable u v
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_pow_mul_eq_add_pow : ∀ {n : ℕ} {R : Type u_3} [inst : CommSemiring R] (a b : R), ∑ s, a ^ s.card * b ^ (n - s.card) = (a + b) ^ n
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.eq_or_eq_neg_of_xRep_eq_xRep : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} {P Q : W.Point}, P.xRep = Q.xRep → P = Q ∨ P = -Q
-- Lean.Util.LeanOptions
Lean.LeanOptions.mk.sizeOf_spec : ∀ (values : Lean.NameMap Lean.LeanOptionValue), sizeOf { values := values } = 1 + sizeOf values
-- Mathlib.CategoryTheory.Limits.Opposites
/-- The limit of `F.unop` is the unopposite of `colimit F`.  -/
CategoryTheory.Limits.limitUnopIsoUnopColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) →
          [inst_2 : CategoryTheory.Limits.HasColimit F] →
            CategoryTheory.Limits.limit F.unop ≅ Opposite.unop (CategoryTheory.Limits.colimit F)
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Prequotient.of : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {F : CategoryTheory.Functor J RingCat} → (j : J) → ↑(F.obj j) → RingCat.Colimits.Prequotient F
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.instSupBotHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : Max β] [inst_3 : Bot β],
  SupBotHomClass (SupBotHom α β) α β
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insert.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (v : β k) (hr_1 : Std.DTreeMap.Internal.Impl.leaf.Balanced),
  Std.DTreeMap.Internal.Impl.insert k v Std.DTreeMap.Internal.Impl.leaf hr_1 =
    { impl := Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf,
      balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
/-- If a number is Liouville with exponent `p`, then it is Liouville with any smaller exponent.  -/
LiouvilleWith.mono : ∀ {p q x : ℝ}, LiouvilleWith p x → q ≤ p → LiouvilleWith q x
-- Mathlib.Logic.Equiv.Prod
Equiv.pprodCongr_apply : ∀ {α : Sort u_1} {β : Sort u_4} {γ : Sort u_7} {δ : Sort u_8} (e₁ : α ≃ β) (e₂ : γ ≃ δ) (x : α ×' γ),
  (e₁.pprodCongr e₂) x = ⟨e₁ x.fst, e₂ x.snd⟩
-- Mathlib.Order.SuccPred.WithBot
WithBot.succ_le_succ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] [inst_2 : SuccOrder α] {x y : WithBot α},
  x ≤ y → x.succ ≤ y.succ
-- Mathlib.Topology.Algebra.Module.LocallyConvex
LocallyConvexSpace.iInf : ∀ {ι : Sort u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {ts' : ι → TopologicalSpace E}, (∀ (i : ι), LocallyConvexSpace 𝕜 E) → LocallyConvexSpace 𝕜 E
-- Mathlib.AlgebraicTopology.CechNerve
/-- The Čech conerve associated to an arrow.  -/
CategoryTheory.Arrow.cechConerve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (f : CategoryTheory.Arrow C) →
      [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] →
        CategoryTheory.CosimplicialObject C
-- Mathlib.GroupTheory.Perm.MaximalSubgroups
MulAction.IsBlock.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s : Set α} [Finite α]
  [MulAction.IsMultiplyPretransitive M α (s.ncard + 1)] {G : Subgroup M},
  MulAction.stabilizer M s ≤ G → ∀ {B : Set α}, ¬B ⊆ s → ¬B ⊆ sᶜ → MulAction.IsBlock (↥G) B → sᶜ ⊆ B
-- Std.Time.Date.Unit.Day
Std.Time.Day.instOfNatOrdinal : {n : ℕ} → OfNat Std.Time.Day.Ordinal n
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- **Alias** of `Metric.eball_ofReal`.

---

Balls defined using the distance or the edistance coincide  -/
Metric.emetric_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.eball x (ENNReal.ofReal ε) = Metric.ball x ε
-- Mathlib.Data.Stream.Init
Stream'.corec_eq : ∀ {α : Type u} {β : Type v} (f : α → β) (g : α → α) (a : α),
  Stream'.corec f g a = Stream'.cons (f a) (Stream'.corec f g (g a))
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.opNNNorm_le_iff : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  {f : E →SL[σ₁₂] F} {C : NNReal}, ‖f‖₊ ≤ C ↔ ∀ (x : E), ‖f x‖₊ ≤ C * ‖x‖₊
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensorLeftTensor.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  CategoryTheory.MonoidalCategory.tensorLeftTensor X Y =
    CategoryTheory.NatIso.ofComponents (CategoryTheory.MonoidalCategoryStruct.associator X Y) ⋯
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.vanishingIdeal_isIrreducible : ∀ {R : Type u} [inst : CommSemiring R], PrimeSpectrum.vanishingIdeal '' {s | IsIrreducible s} = {P | P.IsPrime}
-- Lean.Data.Name
/-- Return `true` if `n` contains a string part `s` that satisfies `f`.

Examples:
```
#eval (`foo.bla).anyS (·.startsWith "fo") -- true
#eval (`foo.bla).anyS (·.startsWith "boo") -- false
```
 -/
Lean.Name.anyS : Lean.Name → (String → Bool) → Bool
-- Lean.Elab.InfoTree.Types
Lean.Elab.MonadInfoTree.mk : {m : Type → Type} →
  m Lean.Elab.InfoState → ((Lean.Elab.InfoState → Lean.Elab.InfoState) → m Unit) → Lean.Elab.MonadInfoTree m
-- Mathlib.RingTheory.Valuation.Basic
Valuation.isEquiv_iff_val_lt_one : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : LinearOrderedCommGroupWithZero Γ'₀] {v : Valuation K Γ₀} {v' : Valuation K Γ'₀},
  v.IsEquiv v' ↔ ∀ {x : K}, v x < 1 ↔ v' x < 1
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.projectMapAux.eq_3 : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v', u'} D] [inst_1 : CategoryTheory.MonoidalCategory D]
  (f : C → D) (X Y Z : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.FreeMonoidalCategory.projectMapAux f (CategoryTheory.FreeMonoidalCategory.Hom.α_inv X Y Z) =
    (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.FreeMonoidalCategory.projectObj f X)
        (CategoryTheory.FreeMonoidalCategory.projectObj f Y) (CategoryTheory.FreeMonoidalCategory.projectObj f Z)).inv
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.epsilon_pos : ∀ (o : Ordinal.{u_1}), 0 < o.epsilon
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instGroup.eq_1 : ∀ {α : Type u_1} {l : Filter α} {G : Type u_6} [inst : Group G],
  Filter.Germ.instGroup = { toDivInvMonoid := Filter.Germ.instDivInvMonoid, inv_mul_cancel := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.Hom.group.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G X : C}
  [inst_2 : CategoryTheory.GrpObj G],
  CategoryTheory.Hom.group =
    { toMonoid := CategoryTheory.Hom.monoid,
      inv := fun f => CategoryTheory.CategoryStruct.comp f CategoryTheory.GrpObj.inv, div := DivInvMonoid.div',
      zpow := zpowRec, div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯ }
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.Measure.dirac.isProbabilityMeasure : ∀ {α : Type u_1} [inst : MeasurableSpace α] {x : α}, MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.dirac x)
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.mulVecLin_add : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_4} {n : Type u_5} [inst_1 : Fintype n] (M N : Matrix m n R),
  (M + N).mulVecLin = M.mulVecLin + N.mulVecLin
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.empty_mul : ∀ {α : Type u} {n' : Type uₙ} {o' : Type uₒ} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n']
  (A : Matrix (Fin 0) n' α) (B : Matrix n' o' α), A * B = Matrix.of ![]
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.mul_splits_in_splittingField_of_mul : ∀ {F : Type u_1} [inst : Field F] {p₁ q₁ p₂ q₂ : Polynomial F},
  q₁ ≠ 0 →
    q₂ ≠ 0 →
      (Polynomial.map (algebraMap F q₁.SplittingField) p₁).Splits →
        (Polynomial.map (algebraMap F q₂.SplittingField) p₂).Splits →
          (Polynomial.map (algebraMap F (q₁ * q₂).SplittingField) (p₁ * p₂)).Splits
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atTop_of_mul_le_const : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelMonoid M] {l : Filter α}
  {f g : α → M},
  (∃ C, ∀ (x : α), g x ≤ C) → Filter.Tendsto (fun x => f x * g x) l Filter.atTop → Filter.Tendsto f l Filter.atTop
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.mul_apply : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A]
  [inst_5 : NonUnitalNonAssocSemiring B] [inst_6 : Module R B] [inst_7 : SMulCommClass R B B]
  [inst_8 : IsScalarTower R B B] (a₁ a₂ : A) (b₁ b₂ : B),
  (Algebra.TensorProduct.mul (a₁ ⊗ₜ[R] b₁)) (a₂ ⊗ₜ[R] b₂) = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.subset_add_right : ∀ {α : Type u_2} [inst : AddZeroClass α] {s : Set α} (t : Set α), 0 ∈ s → t ⊆ s + t
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.IsHamiltonian.exists_isHamiltonianCycle : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} [inst_1 : Fintype α] [Nontrivial α],
  G.IsHamiltonian → ∀ (v : α), ∃ p, p.IsHamiltonianCycle
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop.0.Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastCpopLayer.go : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len w : ℕ} {assign : α → Bool} (aig : Std.Sat.AIG α)
  (iterNum : ℕ) (oldLayer : aig.RefVec (len * w)) (newLayer : aig.RefVec (iterNum * w)) (oldLayerBv : BitVec (len * w))
  (hold' : 2 * (iterNum - 1) < len),
  (∀ (idx : ℕ) (hidx : idx < len * w),
      ⟦assign, { aig := aig, ref := oldLayer.get idx hidx }⟧ = oldLayerBv.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < iterNum * w),
        ⟦assign, { aig := aig, ref := newLayer.get idx hidx }⟧ = (oldLayerBv.cpopLayer 0#(0 * w) ⋯).getLsbD idx) →
      ∀ (idx : ℕ) (hidx : idx < (len + 1) / 2 * w),
        ⟦assign,
            { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer.go iterNum oldLayer newLayer hold' ⋯).aig,
              ref :=
                (Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer.go iterNum oldLayer newLayer hold' ⋯).vec.get idx
                  hidx }⟧ =
          (oldLayerBv.cpopLayer 0#(0 * w) ⋯).getLsbD idx
-- Mathlib.RingTheory.Extension.Cotangent.BaseChange
Algebra.Extension.H1Cotangent.equiv.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P₁ : Algebra.Extension R S} {P₂ : Algebra.Extension R S} (f₁ : P₁.Hom P₂) (f₂ : P₂.Hom P₁),
  Algebra.Extension.H1Cotangent.equiv f₁ f₂ =
    { toLinearMap := Algebra.Extension.H1Cotangent.map f₁, invFun := ⇑(Algebra.Extension.H1Cotangent.map f₂),
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.p_opcyclesMap_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology] (φ : S₁ ⟶ S₂)
  {Z : C} (h : S₂.opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp S₁.pOpcycles
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ) h) =
    CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.CategoryStruct.comp S₂.pOpcycles h)
-- Mathlib.Analysis.Analytic.Basic
/-- Given a function `f : E → F`, we say that `f` is analytic on a set `s` if it is analytic around
every point of `s`.  -/
AnalyticOnNhd : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [NormedSpace 𝕜 E] → [inst_3 : NormedAddCommGroup F] → [NormedSpace 𝕜 F] → (E → F) → Set E → Prop