mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.MvPowerSeries.Basic
/-- The map between multivariate formal power series induced by a map on the coefficients.  -/
MvPowerSeries.map : {σ : Type u_1} →
  {R : Type u_2} →
    {S : Type u_3} → [inst : Semiring R] → [inst_1 : Semiring S] → (R →+* S) → MvPowerSeries σ R →+* MvPowerSeries σ S
-- Lean.Meta.Tactic.Grind.Types
/-- State for injective theorem support.  -/
Lean.Meta.Grind.Injective.State : Type
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.findSomeM?_pure : ∀ {α β : Type w} {γ : Type x} {m : Type x → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α Id β]
  [inst_2 : Std.IteratorLoop α Id m] [inst_3 : Std.IteratorLoop α Id Id] [LawfulMonad m] [Std.Iterators.Finite α Id]
  [Std.LawfulIteratorLoop α Id m] [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {f : β → Option γ},
  (it.findSomeM? fun x => pure (f x)) = pure (it.findSome? f)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isNonloop_iff_mem_compl_loops : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsNonloop e ↔ e ∈ M.E \ M.loops
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
/-- If a monoid `M` distributively continuously acts on `𝕜` and this action commutes with
multiplication on `𝕜`, then it acts on `WeakDual 𝕜 E`.  -/
WeakDual.instMulAction : {𝕜 : Type u_2} →
  {E : Type u_4} →
    [inst : CommSemiring 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [inst_2 : ContinuousAdd 𝕜] →
          [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
            [inst_4 : AddCommMonoid E] →
              [inst_5 : Module 𝕜 E] →
                [inst_6 : TopologicalSpace E] →
                  (M : Type u_6) →
                    [inst_7 : Monoid M] →
                      [inst_8 : DistribMulAction M 𝕜] →
                        [SMulCommClass 𝕜 M 𝕜] → [ContinuousConstSMul M 𝕜] → MulAction M (WeakDual 𝕜 E)
-- Mathlib.Combinatorics.SimpleGraph.Prod
/-- Box product of simple graphs. It relates `(a₁, b)` and `(a₂, b)` if `G` relates `a₁` and `a₂`,
and `(a, b₁)` and `(a, b₂)` if `H` relates `b₁` and `b₂`.  -/
SimpleGraph.«term_□_» : Lean.TrailingParserDescr
-- Init.Data.List.Pairwise
List.pairwise_middle : ∀ {α : Type u_1} {R : α → α → Prop},
  (∀ {x y : α}, R x y → R y x) →
    ∀ {a : α} {l₁ l₂ : List α}, List.Pairwise R (l₁ ++ a :: l₂) ↔ List.Pairwise R (a :: (l₁ ++ l₂))
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
Filter.EventuallyEq.lineDeriv_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f f₁ : E → F}
  {x v : E}, f₁ =ᶠ[nhds x] f → lineDeriv 𝕜 f₁ x v = lineDeriv 𝕜 f x v
-- Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
SSet.range_eq_iSup_sigma_ι : ∀ {ι : Type v} [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ι) (Type u)] {X : ι → SSet} {Y : SSet}
  [inst : CategoryTheory.Limits.HasCoproduct X] (f : ∐ X ⟶ Y),
  SSet.Subcomplex.range f =
    ⨆ i, SSet.Subcomplex.range (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι X i) f)
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.coe_mul : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : MulZeroClass R] [inst_4 : ContinuousMul R] (f g : ContinuousMapZero X R), ⇑(f * g) = ⇑f * ⇑g
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.X_pow_eq_monomial : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) [inst_1 : MulSemiringAction (Multiplicative ℕ) R],
  SkewPolynomial.X ^ n = (SkewPolynomial.monomial n) 1
-- Std.Async.System
Std.Async.System.instDecidableEqGroupId.decEq : (x x_1 : Std.Async.System.GroupId) → Decidable (x = x_1)
-- Mathlib.Geometry.Euclidean.Inversion.Basic
EuclideanGeometry.inversion.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (c : P) (R : ℝ) (x : P),
  EuclideanGeometry.inversion c R x = (R / dist x c) ^ 2 • (x -ᵥ c) +ᵥ c
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasFDerivAt.sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {f' g' : E →L[𝕜] F} {x : E}, HasFDerivAt f f' x → HasFDerivAt g g' x → HasFDerivAt (f - g) (f' - g') x
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.lapply_comp_lsingle_of_ne : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (a a' : α), a ≠ a' → Finsupp.lapply a ∘ₗ Finsupp.lsingle a' = 0
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
NumberField.sign_discr : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  (NumberField.discr K).sign = (-1) ^ NumberField.InfinitePlace.nrComplexPlaces K
-- Mathlib.CategoryTheory.Subobject.NoetherianObject
CategoryTheory.instContainsZeroIsNoetherianObjectOfHasZeroObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C],
  CategoryTheory.isNoetherianObject.ContainsZero
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
/-- Return `some c` if `e` is a `Char.ofNat`-application that encodes the character `c`.  -/
Lean.Char.fromExpr? : Lean.Expr → Lean.Meta.SimpM (Option Char)
-- Mathlib.Analysis.Distribution.DerivNotation
/-- `∂_{v} f` is the line derivative of `f` in direction `v`. The meaning of this notation is
type-dependent.  -/
LineDeriv.«term∂_{_}» : Lean.ParserDescr
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
VonNeumannAlgebra.ext_iff : ∀ {H : Type u} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : CompleteSpace H]
  {S T : VonNeumannAlgebra H}, S = T ↔ ∀ (x : H →L[ℂ] H), x ∈ S ↔ x ∈ T
-- Mathlib.CategoryTheory.Grothendieck
/-- A morphism in the Grothendieck category `F : C ⥤ Cat` consists of
`base : X.base ⟶ Y.base` and `f.fiber : (Functor.ofCatHom (F.map base)).obj X.fiber ⟶ Y.fiber`.
 -/
CategoryTheory.Grothendieck.Hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      CategoryTheory.Grothendieck F → CategoryTheory.Grothendieck F → Type (max v v₂)
-- Mathlib.Order.UpperLower.Principal
UpperSet.map_Ioi : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) (a : α),
  (UpperSet.map f) (UpperSet.Ioi a) = UpperSet.Ioi (f a)
-- Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.hom_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y} (H : CategoryTheory.SimplicialObject.Homotopy f g) (p q : ℕ),
  p + 1 ≠ q → CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.hom H p q = 0
-- Mathlib.Algebra.Lie.Cochain
/-- The coboundary operator taking degree 2 cochains to a space containing degree 3 cochains.  -/
LieModule.Cohomology.d₂₃ : (R : Type u_1) →
  [inst : CommRing R] →
    (L : Type u_2) →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          (M : Type u_3) →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [LieModule R L M] → ↥(LieModule.Cohomology.twoCochain R L M) →ₗ[R] L →ₗ[R] L →ₗ[R] L →ₗ[R] M
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instFromJsonPosition.fromJson : Lean.Json → Except String Lean.Lsp.Position
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
Valued.integer.norm_irreducible_lt_one : ∀ {K : Type u_1} [inst : NontriviallyNormedField K] [inst_1 : IsUltrametricDist K] {ϖ : ↥(Valued.integer K)},
  Irreducible ϖ → ‖ϖ‖ < 1
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_nsmul : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : AddMonoid α] [inst_1 : StarAddMonoid α] (c : ℕ) (M : Matrix m n α),
  (c • M).conjTranspose = c • M.conjTranspose
-- Mathlib.Geometry.Convex.Cone.Basic
Submodule.toConvexCone_bot : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M], ⊥.toConvexCone = 0
-- Mathlib.Data.Stream.Init
Stream'.head_iterate : ∀ {α : Type u} (f : α → α) (a : α), (Stream'.iterate f a).head = a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- To check equality of two natural transformations of functors to a `CategoricalPullback`, it
suffices to do so after whiskering with the projections.  -/
CategoryTheory.Limits.CategoricalPullback.natTrans_ext : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  {J K : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)} {α β : J ⟶ K},
  CategoryTheory.Functor.whiskerRight α (CategoryTheory.Limits.CategoricalPullback.π₁ F G) =
      CategoryTheory.Functor.whiskerRight β (CategoryTheory.Limits.CategoricalPullback.π₁ F G) →
    CategoryTheory.Functor.whiskerRight α (CategoryTheory.Limits.CategoricalPullback.π₂ F G) =
        CategoryTheory.Functor.whiskerRight β (CategoryTheory.Limits.CategoricalPullback.π₂ F G) →
      α = β
-- Mathlib.Algebra.Category.Grp.Images
/-- the inclusion of `image f` into the target  -/
AddCommGrpCat.image.ι : {G H : AddCommGrpCat} → (f : G ⟶ H) → AddCommGrpCat.image f ⟶ H
-- Std.Data.ExtDHashMap.Lemmas
/-- Simpler variant of `get!_filter` when `LawfulBEq` is available.  -/
Std.ExtDHashMap.Const.get!_filter' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : LawfulBEq α]
  [inst_1 : Inhabited β] {f : α → β → Bool} {k : α},
  Std.ExtDHashMap.Const.get! (Std.ExtDHashMap.filter f m) k =
    (Option.filter (f k) (Std.ExtDHashMap.Const.get? m k)).get!
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rco_eq_singleton_iff : ∀ {k m n : ℕ}, (m...n).toList = [k] ↔ n = m + 1 ∧ m = k
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.of_forall_mem_unit_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [LawfulBEq α] {m₁ m₂ : Std.DHashMap α fun x => Unit},
  (∀ (k : α), k ∈ m₁ ↔ k ∈ m₂) → m₁.Equiv m₂
-- Mathlib.CategoryTheory.Shift.Twist
CategoryTheory.TwistShiftData.shift_z_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type w} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (t : CategoryTheory.TwistShiftData C A) (a b c : A) (X : C),
  (CategoryTheory.shiftFunctor C c).map ((↑(t.z a b)).app X) =
    (↑(t.z a b)).app ((CategoryTheory.shiftFunctor C c).obj X)
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
IsLocalFrameOn.coeff_apply_of_mem : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {ι : Type u_7} {s : ι → (x : M) → V x}
  {u : Set M} {n : WithTop ℕ∞} {x : M} (hs : IsLocalFrameOn I F n s u) (hx : x ∈ u) (t : (x : M) → V x) (i : ι),
  (hs.coeff i x) (t x) = ((hs.toBasisAt hx).repr (t x)) i
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
ruzsaSzemerediNumber_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : Fintype α]
  [inst_3 : Fintype β] (f : α ↪ β), ruzsaSzemerediNumber α ≤ ruzsaSzemerediNumber β
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integrableOn_exp_mul_complex_Iic : ∀ {a : ℂ},
  0 < a.re → ∀ (c : ℝ), MeasureTheory.IntegrableOn (fun x => Complex.exp (a * ↑x)) (Set.Iic c) MeasureTheory.volume
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
/-- An element of a product algebra is integral iff each component is integral.  -/
IsIntegral.pair_iff : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Ring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {x : A × B}, IsIntegral R x ↔ IsIntegral R x.1 ∧ IsIntegral R x.2
-- Mathlib.GroupTheory.Coprod.Basic
/-- Coproduct of two monoids or groups.  -/
Monoid.Coprod.«term_∗_» : Lean.TrailingParserDescr
-- Init.Data.Array.Lemmas
Array.set_append : ∀ {α : Type u_1} {xs ys : Array α} {i : ℕ} {x : α} (h : i < (xs ++ ys).size),
  (xs ++ ys).set i x h = if h' : i < xs.size then xs.set i x h' ++ ys else xs ++ ys.set (i - xs.size) x ⋯
-- Lean.Widget.TaggedText
_private.Lean.Widget.TaggedText.0.Lean.Widget.TaggedText.TaggedState.out : Lean.Widget.TaggedText.TaggedState✝ → Lean.Widget.TaggedText (ℕ × ℕ)
-- Init.Data.Range.Polymorphic.Basic
Std.Rxc.size_eq_zero_iff_not_le : ∀ {α : Type u} [inst : LE α] [inst_1 : Std.PRange.UpwardEnumerable α] [inst_2 : Std.Rxc.HasSize α]
  [Std.Rxc.LawfulHasSize α] {lo hi : α}, Std.Rxc.HasSize.size lo hi = 0 ↔ ¬lo ≤ hi
-- Mathlib.Algebra.Group.Subsemigroup.Membership
/-- A dependent version of `Subsemigroup.iSup_induction`.  -/
Subsemigroup.iSup_induction' : ∀ {ι : Sort u_1} {M : Type u_2} [inst : Mul M] (S : ι → Subsemigroup M) {C : (x : M) → x ∈ ⨆ i, S i → Prop},
  (∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯) →
    (∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯) →
      ∀ {x₁ : M} (hx₁ : x₁ ∈ ⨆ i, S i), C x₁ hx₁
-- Mathlib.GroupTheory.Exponent
Monoid.exponent_min : ∀ {G : Type u} [inst : Monoid G] (m : ℕ), 0 < m → m < Monoid.exponent G → ∃ g, g ^ m ≠ 1
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.WPath.inhabited : {n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) →
    (x : P.last.W) → {i : Fin2 n} → [I : Inhabited (P.drop.B x.head i)] → Inhabited (P.WPath x i)
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
le_or_le_of_mul_le_mul : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Mul α] [MulLeftStrictMono α] [MulRightStrictMono α] {a₁ a₂ b₁ b₂ : α},
  a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioi_inj : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ioi a = Set.Ioi b ↔ a = b
-- Mathlib.Tactic.Simproc.Factors
/-- Given `n` and `a` (in expressions `en` and `ea`) corresponding to literal numerals
(in `enl` and `eal`), returns `(l, ⊢ factorsHelper n a l)`.  -/
_private.Mathlib.Tactic.Simproc.Factors.0.Mathlib.Meta.Simproc.evalPrimeFactorsListAux : {en enl ea eal : Q(ℕ)} →
  Q(Mathlib.Meta.NormNum.IsNat «$en» «$enl») →
    Q(Mathlib.Meta.NormNum.IsNat «$ea» «$eal») →
      Lean.MetaM ((l : Q(List ℕ)) × Q(Mathlib.Meta.Simproc.FactorsHelper «$en» «$ea» «$l»))
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.singleton_prod_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (x : α) (y : β),
  {x} ×ˢ {y} = {(x, y)}
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.isColocal_of_isIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.IsIso f], P.isColocal f
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer.eq_def : ∀ (S : Type u) [inst : Semiring S] (x : ℕ),
  ascPochhammer S x =
    match x with
    | 0 => 1
    | n.succ => Polynomial.X * (ascPochhammer S n).comp (Polynomial.X + 1)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Homeomorph.setCongr.congr_simp : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X} (h : s = t), Homeomorph.setCongr h = Homeomorph.setCongr h
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- A weighted homogeneous polynomial of degree `n` is zero if no monomial has weight `n`.  -/
MvPolynomial.IsWeightedHomogeneous.eq_zero_of_no_monomials : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {φ : MvPolynomial σ R}
  {n : M} {w : σ → M}, MvPolynomial.IsWeightedHomogeneous w φ n → (∀ (d : σ →₀ ℕ), (Finsupp.weight w) d ≠ n) → φ = 0
-- Mathlib.Tactic.CategoryTheory.Elementwise
/-- List of simp lemmas to apply to the elementwise theorem.  -/
Mathlib.Tactic.Elementwise.elementwiseThms : List Lean.Name
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- If `f : M → N` is a submultiplicative function, `f (x * y) ≤ f x * f y` and `g i`, `i ∈ s`, is a
nonempty finite family of elements of `M`, then `f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)`.  -/
Finset.le_prod_nonempty_of_submultiplicative : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : CommMonoid M] [inst_1 : CommMonoid N] [inst_2 : Preorder N]
  [IsOrderedMonoid N] (f : M → N),
  (∀ (x y : M), f (x * y) ≤ f x * f y) →
    ∀ {s : Finset ι}, s.Nonempty → ∀ (g : ι → M), f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
AddLECancellable.lt_tsub_iff_left_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, AddLECancellable c → c ≤ b → (a < b - c ↔ c + a < b)
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
mdifferentiableWithinAt_extChartAt_symm : ∀ {𝕜 : 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] [IsManifold I 1 M] {x : M} {z : E},
  z ∈ (extChartAt I x).target → MDiffAt[Set.range ↑I] ↑(extChartAt I x).symm z
-- Init.Data.Vector.Extract
Vector.extract_set : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j k : ℕ} (h : k < n) {a : α},
  (xs.set k a h).extract i j =
    if x : k < i then xs.extract i j else if x_1 : k < min j n then (xs.extract i j).set (k - i) a ⋯ else xs.extract i j
-- Std.Async.Signal
Std.Async.Signal.sigcont.sizeOf_spec : sizeOf Std.Async.Signal.sigcont = 1
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars
ContinuousLinearMap.toContinuousAddMonoidHom_restrictScalars : ∀ {A : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {R : Type u_4} [inst : Semiring A] [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid M₁] [inst_3 : Module A M₁] [inst_4 : Module R M₁] [inst_5 : TopologicalSpace M₁]
  [inst_6 : AddCommMonoid M₂] [inst_7 : Module A M₂] [inst_8 : Module R M₂] [inst_9 : TopologicalSpace M₂]
  [inst_10 : LinearMap.CompatibleSMul M₁ M₂ R A] (f : M₁ →L[A] M₂), ↑(ContinuousLinearMap.restrictScalars R f) = ↑f
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonLeanIleanInfoParams.toJson : Lean.Lsp.LeanIleanInfoParams → Lean.Json
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.cons_cons_iff : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} (p : α × Bool), FreeGroup.Red (p :: L₁) (p :: L₂) ↔ FreeGroup.Red L₁ L₂
-- Mathlib.Analysis.Convex.Basic
MonotoneOn.convex_lt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {s : Set E} {f : E → β}, MonotoneOn f s → Convex 𝕜 s → ∀ (r : β), Convex 𝕜 {x | x ∈ s ∧ f x < r}
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.FirstByte : Type
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.iSup_le_lsub : ∀ {ι : Type u_3} (f : ι → Ordinal.{max u_4 u_3}), iSup f ≤ Ordinal.lsub f
-- Mathlib.Data.Num.Bitwise
/-- The `head` of a `NzsNum` is the Boolean value of its LSB.  -/
NzsNum.head : NzsNum → Bool
-- Mathlib.RingTheory.PowerBasis
IsIntegral.mem_span_pow : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] [Nontrivial R] {x y : S},
  IsIntegral R x → (∃ f, y = (Polynomial.aeval x) f) → y ∈ Submodule.span R (Set.range fun i => x ^ ↑i)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.opensRange_ι : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens), AlgebraicGeometry.Scheme.Hom.opensRange U.ι = U
-- Mathlib.Computability.TuringMachine.Tape
/-- A `ListBlank Γ` is a quotient of `List Γ` by extension by blanks at the end. This is used to
represent half-tapes of a Turing machine, so that we can pretend that the list continues
infinitely with blanks.  -/
Turing.ListBlank : (Γ : Type u_1) → [Inhabited Γ] → Type u_1
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.isFintype : (self : FinBddDistLat) → Fintype ↑self.toDistLat
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.List.forIn'_eq_foldlM.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.yield b))
  (h_2 : (b : β) → motive (ForInStep.done b)),
  (match ForInStep.yield b with
    | ForInStep.yield b => h_1 b
    | ForInStep.done b => h_2 b) =
    h_1 b
-- Std.Time.Time.Unit.Basic
/-- Converts a `Second.Offset` to a `Millisecond.Offset`.
 -/
Std.Time.Millisecond.Offset.ofSeconds : Std.Time.Second.Offset → Std.Time.Millisecond.Offset
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.nnrpow_one : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] (a : A),
  autoParam (0 ≤ a) CFC.nnrpow_one._auto_1 → a ^ 1 = a
-- Init.Data.Array.Lemmas
Array.foldr_filterMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : β → γ → γ} {xs : Array α} {init : γ},
  Array.foldr g init (Array.filterMap f xs) =
    Array.foldr
      (fun x y =>
        match f x with
        | some b => g b y
        | none => y)
      init xs
-- Init.Data.UInt.Bitwise
UInt8.ofFin_xor : ∀ (a b : Fin UInt8.size), UInt8.ofFin (a ^^^ b) = UInt8.ofFin a ^^^ UInt8.ofFin b
-- Mathlib.Data.Multiset.Defs
/-- `Nodup s` means that `s` has no duplicates, i.e. the multiplicity of
any element is at most 1.  -/
Multiset.Nodup : {α : Type u_1} → Multiset α → Prop
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.ofLinearEquiv_symm : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (l : A₁ ≃ₗ[R] A₂) (map_one : l 1 = 1)
  (map_mul : ∀ (x y : A₁), l (x * y) = l x * l y),
  (AlgEquiv.ofLinearEquiv l map_one map_mul).symm = AlgEquiv.ofLinearEquiv l.symm ⋯ ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
/-- The pullback `X ×[W] Y` is initial, if `W` is the coproduct of `X` and `Y`.  -/
CategoryTheory.Limits.IsInitial.ofBinaryCoproductDisjointOfIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [CategoryTheory.Limits.BinaryCoproductDisjoint X Y] →
        {Z : C} →
          {f : X ⟶ Z} →
            {g : Y ⟶ Z} →
              [inst_2 : CategoryTheory.Limits.HasPullback f g] →
                CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk f g) →
                  CategoryTheory.Limits.IsInitial (CategoryTheory.Limits.pullback f g)
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
SSet.instAdditiveFunctorChainComplexNatChainComplexFunctor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C], (SSet.chainComplexFunctor C).Additive
-- Mathlib.Data.Finset.SDiff
/-- See also `Finset.sdiff_inter_right_comm`.  -/
Finset.inter_sdiff_assoc : ∀ {α : Type u_1} [inst : DecidableEq α] (s t u : Finset α), (s ∩ t) \ u = s ∩ (t \ u)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKeyD_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.maxKeyD fallback ∈ t
-- Mathlib.Order.SymmDiff
ofDual_symmDiff : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b : αᵒᵈ),
  OrderDual.ofDual (symmDiff a b) = bihimp (OrderDual.ofDual a) (OrderDual.ofDual b)