mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- Applying a column-stochastic matrix to a vector preserves its sum.  -/
Matrix.sum_mulVec_of_mem_colStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R} {x : n → R},
  M ∈ Matrix.colStochastic R n → ∑ i, M.mulVec x i = ∑ i, x i
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.singleAddHom_apply : ∀ {ι : Type u} (β : ι → Type v) [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)] (i : ι) (b : β i),
  (DFinsupp.singleAddHom β i) b = fun₀ | i => b
-- Mathlib.Analysis.Normed.Group.Basic
coe_comp_nnnorm' : ∀ {E : Type u_5} [inst : SeminormedGroup E], NNReal.toReal ∘ nnnorm = norm
-- Init.Data.List.Basic
List.modifyTailIdx_succ_cons : ∀ {α : Type u} {f : List α → List α} {i : ℕ} {a : α} {l : List α},
  (a :: l).modifyTailIdx (i + 1) f = a :: l.modifyTailIdx i f
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_add : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] (f g : R → R) (a : A),
  autoParam (ContinuousOn f (quasispectrum R a)) _auto_382✝ →
    autoParam (f 0 = 0) _auto_384✝ →
      autoParam (ContinuousOn g (quasispectrum R a)) _auto_386✝ →
        autoParam (g 0 = 0) _auto_388✝ → cfcₙ (fun x => f x + g x) a = cfcₙ f a + cfcₙ g a
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
AlgebraicGeometry.UniversallyOpen.instIsStableUnderBaseChangeScheme : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.UniversallyOpen
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.sub_toSimpleFunc : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} (f g : ↥(MeasureTheory.Lp.simpleFunc E p μ)),
  ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc (f - g)) =ᵐ[μ]
    ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f) - ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc g)
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Broadcast.Consumer.promise : {α : Type} → Std.Broadcast.Consumer✝ α → IO.Promise Bool
-- Lean.MetavarContext
/-- Given a metavariable with type `e`, kind `kind` and free/meta variables `xs` in its local context `lctx`,
create the type for a new auxiliary metavariable. These auxiliary metavariables are created by `elimMVar`.

See "Gruesome details" section in the beginning of the file.

Note: It is assumed that `xs` is the result of calling `collectForwardDeps` on a subset of variables in `lctx`.
 -/
_private.Lean.MetavarContext.0.Lean.MetavarContext.MkBinding.mkAuxMVarType : Lean.LocalContext → Array Lean.Expr → Lean.MetavarKind → Lean.Expr → Bool → Lean.MetavarContext.MkBinding.M Lean.Expr
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.distribMulAction' : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {S : Type u_3} →
            [inst_3 : Monoid S] →
              [inst_4 : SMul S R] →
                [inst_5 : DistribMulAction S M] →
                  [IsScalarTower S R M] → (P : Submodule R M) → DistribMulAction S (M ⧸ P)
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_succEmb_Ioo : ∀ {n : ℕ} (i j : Fin n), Finset.map (Fin.succEmb n) (Finset.Ioo i j) = Finset.Ioo i.succ j.succ
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.parabolicEigenvalue.eq_1 : ∀ {K : Type u_1} [inst : Field K] (m : Matrix (Fin 2) (Fin 2) K), m.parabolicEigenvalue = m.trace / 2
-- Mathlib.Algebra.MvPolynomial.Equiv
Polynomial.toMvPolynomial_inj : ∀ {R : Type u_1} {σ : Type u_3} [inst : CommSemiring R] {i : σ} {p q : Polynomial R},
  (Polynomial.toMvPolynomial i) p = (Polynomial.toMvPolynomial i) q ↔ p = q
-- Mathlib.Order.Partition.Basic
Partition.exists_le_of_mem_le : ∀ {α : Type u_1} {s x : α} [inst : CompleteLattice α] {P Q : Partition s}, P ≤ Q → x ∈ P → ∃ y ∈ Q, x ≤ y
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Pons asinorum, oriented angle-at-point form.  -/
EuclideanGeometry.oangle_eq_oangle_of_dist_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, dist p₁ p₂ = dist p₁ p₃ → EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₂ p₃ p₁
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.BicategoricalCoherence.right'_iso : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (f g : a ⟶ b)
  [inst_1 : CategoryTheory.BicategoricalCoherence f g],
  CategoryTheory.BicategoricalCoherence.iso =
    CategoryTheory.BicategoricalCoherence.iso ≪≫ (CategoryTheory.Bicategory.rightUnitor g).symm
-- Mathlib.Topology.UniformSpace.Ultra.Constructions
IsUltraUniformity.inf : ∀ {X : Type u_1} {u u' : UniformSpace X}, IsUltraUniformity X → IsUltraUniformity X → IsUltraUniformity X
-- Lean.Level
Lean.Level.PP.Result.maxNode.inj : ∀ {a a_1 : List Lean.Level.PP.Result}, Lean.Level.PP.Result.maxNode a = Lean.Level.PP.Result.maxNode a_1 → a = a_1
-- Mathlib.Control.LawfulFix
Part.Fix.mem_iff : ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
  b ∈ Part.fix (⇑f) a ↔ ∃ i, b ∈ Part.Fix.approx (⇑f) i a
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.size_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp}, t₁.Equiv t₂ → t₁.size = t₂.size
-- Mathlib.Probability.Kernel.Condexp
ProbabilityTheory.condExpKernel_singleton_ae_eq_cond : ∀ {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsFiniteMeasure μ]
  {s t : Set Ω} [inst_1 : StandardBorelSpace Ω],
  MeasurableSet s →
    MeasurableSet t →
      ∀ᵐ (ω : Ω) ∂μ.restrict s, ((ProbabilityTheory.condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t = μ[t | s]
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instNonUnitalSemiring : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : AddCommMonoid Γ] →
      [inst_1 : PartialOrder Γ] →
        [IsOrderedCancelAddMonoid Γ] → [inst : NonUnitalSemiring R] → NonUnitalSemiring (HahnSeries Γ R)
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.triangle_obj₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L),
  (CochainComplex.mappingCone.triangle φ).obj₂ = L
-- Init.Data.UInt.Lemmas
UInt32.size_dvd_usizeSize : UInt32.size ∣ USize.size
-- Mathlib.Computability.Primrec.List
Primrec.list_flatMap : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → List β} {g : α → β → List σ}, Primrec f → Primrec₂ g → Primrec fun a => List.flatMap (g a) (f a)
-- Mathlib.Topology.UniformSpace.Defs
isUniformEmbedding_iff : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] (f : α → β),
  IsUniformEmbedding f ↔ IsUniformInducing f ∧ Function.Injective f
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J]
  [inst_2 : SuccOrder J] {j : J} (hj : ¬IsMax j) (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {X : C}
  (τ : F.obj ⟨j, ⋯⟩ ⟶ X) (i : J) (hi : i ≤ j),
  CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso hj F τ i hi =
    CategoryTheory.SmallObject.SuccStruct.extendToSucc.objIso F X ⟨i, hi⟩
-- Std.Data.DTreeMap.Internal.Queries
/-- Folds the given function over the mappings in the tree in descending order.  -/
Std.DTreeMap.Internal.Impl.foldrM : {α : Type u} →
  {β : α → Type v} →
    {δ : Type w} →
      {m : Type w → Type u_1} → [Monad m] → ((a : α) → β a → δ → m δ) → δ → Std.DTreeMap.Internal.Impl α β → m δ
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.injective : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β),
  Function.Injective ⇑h
-- Mathlib.Tactic.MoveAdd
/-- `move_oper op [a]` repeatedly moves `a` to the far right hand side in applications of `op`.
Here the constant `op` refers to a binary associative commutative operation, and `a` is any term
(potentially with underscores).

If `a` contains underscores, they are filled in by unification with the first matching occurrence.
Subterms with different values for the underscores are not matched, unless you repeat `a`.

Currently, `move_oper` supports the operators `HAdd.hAdd` (`· + ·`), `HMul.hMul` (`· * ·`),
`And` (`· ∧ ·`), `Or` (`· ∨ ·`), `Max.max` and `Min.min`. To support more operations, add them to
`Mathlib.MoveAdd.moveOperSimpCtx`.

* `move_add [...]` uses addition as the operation: it abbreviates `move_oper HAdd.add [...]`.
* `move_mul [...]` uses multiplication as the operation: it abbreviates `move_oper HMul.mul [...]`.
* `move_oper op [← a]` moves the atoms matching `a` to the far left hand side instead of the right.
* `move_oper op [a, b, ← c, ← d, ...]` moves multiple atoms simultaneously, in the order indicated
  by the arguments: `c` will appear to the left of `d` and `a` will appear to the left of `b`.
 -/
Mathlib.MoveAdd.moveOperTac : Lean.ParserDescr
-- Mathlib.Algebra.GCDMonoid.Basic
normalize_zero : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α], normalize 0 = 0
-- Mathlib.CategoryTheory.Sites.Whiskering
CategoryTheory.instFullSheafFunctorOppositeCompSheafComposeSheafToPresheafOfFaithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {B : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C)
  (F : CategoryTheory.Functor A B) [inst_3 : J.HasSheafCompose F] [F.Faithful] [F.Full],
  ((CategoryTheory.sheafCompose J F).comp (CategoryTheory.sheafToPresheaf J B)).Full
-- Mathlib.Algebra.GroupWithZero.Units.Basic
zpow_sub₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → ∀ (m n : ℤ), a ^ (m - n) = a ^ m / a ^ n
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_eq_some_get!_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β],
  t.WF → ∀ {a : α}, t.contains a = true → Std.DTreeMap.Raw.Const.get? t a = some (Std.DTreeMap.Raw.Const.get! t a)
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- The 2-simplices in a 2-truncated simplicial set `V` generate a hom relation on the free
category on the underlying refl quiver of `V`.  -/
SSet.OneTruncation₂.HoRel₂ : (V : SSet.Truncated 2) → HomRel (CategoryTheory.Cat.FreeRefl (SSet.OneTruncation₂ V))
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.inrX_π_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder] (i : ι)
  {Z : C} (h : K.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.inrX K i)
      (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.cylinder.π K).f i) h) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Limits.biprod.desc (CategoryTheory.CategoryStruct.id K) (CategoryTheory.CategoryStruct.id K)).f
        i)
      h
-- Mathlib.Data.Nat.Factorization.Defs
/-- For nonzero `a` and `b`, the power of `p` in `a * b` is the sum of the powers in `a` and `b`  -/
Nat.factorization_mul : ∀ {a b : ℕ}, a ≠ 0 → b ≠ 0 → (a * b).factorization = a.factorization + b.factorization
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.get? (t.minD fallback) = some (t.minD fallback)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- If `G` is fully faithful, then `post F G S : (F, S) ⥤ (F ⋙ G, G(S))` is an equivalence.  -/
CategoryTheory.CostructuredArrow.isEquivalence_post : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (S : C) (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) [G.Full] [G.Faithful], (CategoryTheory.CostructuredArrow.post F G S).IsEquivalence
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ihom_ev_app_hom : ∀ {k : Type u} [inst : CommRing k] {G : Type v} [inst_1 : Group G] (A B : Rep.{u, u, v} k G),
  (Rep.Hom.hom ((CategoryTheory.ihom.ev A).app B)).toLinearMap =
    (TensorProduct.uncurry (RingHom.id k) (↑A) (↑A →ₗ[k] ↑B) ↑B) LinearMap.id.flip
-- Mathlib.GroupTheory.Perm.Support
/-- The support of a permutation is invariant  -/
Equiv.Perm.isInvariant_of_support_le : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {c : Equiv.Perm α} {s : Finset α},
  c.support ⊆ s → ∀ (x : α), c x ∈ s ↔ x ∈ s
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.ne_zero_iff_nequiv_zero : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (f : PadicSeq p), CauSeq.Completion.mk f ≠ 0 ↔ ¬f ≈ 0
-- Mathlib.MeasureTheory.Covering.Differentiation
VitaliFamily.limRatioMeas.congr_simp : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v v_1 : VitaliFamily μ),
  v = v_1 →
    ∀ [inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α] [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ]
      {ρ ρ_1 : MeasureTheory.Measure α} (e_ρ : ρ = ρ_1) [inst_4 : MeasureTheory.IsLocallyFiniteMeasure ρ]
      (hρ : ρ.AbsolutelyContinuous μ) (a a_1 : α), a = a_1 → v.limRatioMeas hρ a = v_1.limRatioMeas ⋯ a_1
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsPrenex.induction_on_all_not : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {P : {n : ℕ} → L.BoundedFormula α n → Prop}
  {φ : L.BoundedFormula α n},
  φ.IsPrenex →
    (∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ) →
      (∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P ψ.all) →
        (∀ {m : ℕ} {ψ : L.BoundedFormula α m}, P ψ → P ψ.not) → P φ
-- Mathlib.Topology.EMetricSpace.Diam
Metric.ediam_pos_iff : ∀ {X : Type u_2} {s : Set X} [inst : EMetricSpace X], 0 < Metric.ediam s ↔ s.Nontrivial
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplexHomeomorphUnitInterval_symm_apply_coe : ∀ (x : ↑(Set.Icc 0 1)), ↑(stdSimplexHomeomorphUnitInterval.symm x) = ![1 - ↑x, ↑x]
-- Std.Data.TreeMap.Raw.Basic
/-- Transforms a list of keys into a tree map.  -/
Std.TreeMap.Raw.unitOfList : {α : Type u} →
  List α → (cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw.unitOfList._auto_1) → Std.TreeMap.Raw α Unit cmp
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
/-- Some chosen `EffectiveEpiStruct` associated to an effective epi.  -/
CategoryTheory.EffectiveEpi.getStruct : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} → (f : Y ⟶ X) → [CategoryTheory.EffectiveEpi f] → CategoryTheory.EffectiveEpiStruct f
-- Mathlib.FieldTheory.Minpoly.Field
/-- If `B/K` is a nontrivial algebra over a field, and `x` is an element of `K`,
then the minimal polynomial of `algebraMap K B x` is `X - C x`.  -/
minpoly.eq_X_sub_C : ∀ {A : Type u_1} (B : Type u_2) [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] [Nontrivial B] (a : A),
  minpoly A ((algebraMap A B) a) = Polynomial.X - Polynomial.C a
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_lt_one_iff_of_nonneg : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : LinearOrder M₀] [PosMulStrictMono M₀] {a : M₀} {n : ℕ}
  [ZeroLEOneClass M₀], 0 ≤ a → n ≠ 0 → (a ^ n < 1 ↔ a < 1)
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_toNNReal_eq_toReal : ∀ (z : ENNReal), ↑z.toNNReal = z.toReal
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.dsimp : Lean.Expr → Lean.Meta.SimpM Lean.Expr
-- Mathlib.Topology.Algebra.UniformMulAction
/-- A multiplicative action such that for all `c`,
the map `fun x ↦ c • x` is uniformly continuous.  -/
UniformContinuousConstSMul : (M : Type v) → (X : Type x) → [UniformSpace X] → [SMul M X] → Prop
-- Mathlib.Geometry.Convex.Cone.Pointed
/-- The cone hull of a set `s` is the smallest pointed cone that contains `s`.

Pointed cones being defined as submodules over nonnegative scalars, this is implemented as
the submodule span of `s` w.r.t. nonnegative scalars.  -/
PointedCone.hull : (R : Type u_1) →
  {E : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsOrderedRing R] → [inst_3 : AddCommMonoid E] → [inst_4 : Module R E] → Set E → PointedCone R E
-- Batteries.Data.List.Basic
/-- Ternary version of `List.zipWith`.  -/
List.zipWith₃ : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → {δ : Type u_4} → (α → β → γ → δ) → List α → List β → List γ → List δ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, k ∈ t.insert k v
-- Mathlib.Combinatorics.Quiver.Symmetric
_private.Mathlib.Combinatorics.Quiver.Symmetric.0.Quiver.Symmetrify.lift.match_1.splitter : {V : Type u_2} →
  [inst : Quiver V] →
    {X Y : Quiver.Symmetrify V} →
      (motive : (X ⟶ Y) → Sort u_3) →
        (x : X ⟶ Y) → ((g : X ⟶ Y) → motive (Sum.inl g)) → ((g : Y ⟶ X) → motive (Sum.inr g)) → motive x
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.isInvalidContinuationByte_eq_false_of_assemble₄_eq_some_right : ∀ {w x y z : UInt8} {c : Char},
  ByteArray.utf8DecodeChar?.assemble₄ w x y z = some c → ByteArray.utf8DecodeChar?.isInvalidContinuationByte z = false
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_ofList : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α},
  k ∈ Std.HashMap.ofList l ↔ (List.map Prod.fst l).contains k = true
-- Mathlib.CategoryTheory.Equivalence
/-- Powers of an auto-equivalence.  Use `(^)` instead.  -/
CategoryTheory.Equivalence.pow : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → (C ≌ C) → ℤ → (C ≌ C)
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
CategoryTheory.Limits.PullbackCone.toPullbackObj_coe_fst : ∀ {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} (c : CategoryTheory.Limits.PullbackCone f g) (x : c.pt),
  (↑(c.toPullbackObj x)).1 = (CategoryTheory.ConcreteCategory.hom c.fst) x
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] [inst_2 : Inhabited α]
  {l : List α} {k k' : α},
  (k == k') = true → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.ExtHashSet.ofList l).get! k' = k
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of the reverse direction of `SimpleGraph.Walk.isTrail_mapLe`. -/
SimpleGraph.Walk.IsTrail.mapLe : ∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v},
  p.IsTrail → (SimpleGraph.Walk.mapLe h p).IsTrail
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β}
  {x_2 : NonAssocSemiring γ} {g₁ g₂ : β →+* γ} {f : α →+* β}, Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.Analysis.Calculus.Deriv.Slope
/-- The derivative within a set of an antitone function is nonpositive.  -/
AntitoneOn.derivWithin_nonpos : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [OrderTopology 𝕜] {g : 𝕜 → 𝕜}, AntitoneOn g s → derivWithin g s x ≤ 0
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} [inst_3 : Inhabited (β k')],
      List.Pairwise (fun a b => (a.fst == b.fst) = false) l → ⟨k, v⟩ ∈ l → (↑(m.insertMany l)).get! k' = cast ⋯ v
-- Mathlib.Topology.Algebra.Support
tsupport_subset_comp : ∀ {X : Type u_1} {α : Type u_2} {β : Type u_4} [inst : Zero α] [inst_1 : TopologicalSpace X] [inst_2 : Zero β]
  {g : α → β}, (∀ {x : α}, g x = 0 → x = 0) → ∀ (f : X → α), tsupport f ⊆ tsupport (g ∘ f)
-- Mathlib.CategoryTheory.Comma.Basic
/-- Composing the `leftOp` of `opFunctor L R` with `snd L.op R.op` is naturally isomorphic
to `fst L R`.  -/
CategoryTheory.Comma.opFunctorCompSnd : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            (L : CategoryTheory.Functor A T) →
              (R : CategoryTheory.Functor B T) →
                (CategoryTheory.Comma.opFunctor L R).leftOp.comp (CategoryTheory.Comma.snd R.op L.op) ≅
                  (CategoryTheory.Comma.fst L R).op
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.instFaithfulComonadFunctorComonadToFunctor : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C], (CategoryTheory.comonadToFunctor C).Faithful
-- Init.Data.Rat.Basic
Rat.instPowInt : Pow ℚ ℤ
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.instInhabitedCompSource.default : Mathlib.Tactic.Linarith.CompSource
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.reflectsMonomorphisms_of_preserves_of_reflects : ∀ {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] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [G.PreservesMonomorphisms] [(F.comp G).ReflectsMonomorphisms],
  F.ReflectsMonomorphisms
-- Std.Data.DTreeMap.Raw.Lemmas
/-- Simpler variant of `getD_filter` when `LawfulEqCmp` is available.  -/
Std.DTreeMap.Raw.Const.getD_filter' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → Bool} {k : α} {fallback : β},
  t.WF →
    Std.DTreeMap.Raw.Const.getD (Std.DTreeMap.Raw.filter f t) k fallback =
      (Option.filter (f k) (Std.DTreeMap.Raw.Const.get? t k)).getD fallback
-- Mathlib.Order.WithBot
WithTop.none_eq_top : ∀ {α : Type u_1}, none = ⊤
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.IsPositive.re_inner_nonneg_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →L[𝕜] E}, T.IsPositive → ∀ (x : E), 0 ≤ RCLike.re (inner 𝕜 (T x) x)
-- Mathlib.Order.Circular
/-- Strict betweenness for circular orders. `sbtw a b c` states that `b` is strictly between `a`
and `c` (in that order).  -/
SBtw.sbtw : {α : Type u_1} → [self : SBtw α] → α → α → α → Prop
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.Modification.ext : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {x y : CategoryTheory.Oplax.OplaxTrans.Modification η θ},
  x.app = y.app → x = y
-- Init.Control.ExceptCps
ExceptCpsT.run_bind_throw : ∀ {m : Type u_1 → Type u_2} {ε α β : Type u_1} [inst : Monad m] (e : ε) (f : α → ExceptCpsT ε m β),
  (throw e >>= f).run = (throw e).run
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.instCancelCommMonoidLocalization.eq_1 : ∀ {M : Type u_3} [inst : CancelCommMonoid M] (S : Submonoid M),
  Submonoid.LocalizationMap.instCancelCommMonoidLocalization S = (Localization.monoidOf S).cancelCommMonoid