mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} {h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃} {Y : C}
  {φ φ' : Y ⟶ h.pullback},
  φ = φ' ↔
    CategoryTheory.CategoryStruct.comp φ h.p₁ = CategoryTheory.CategoryStruct.comp φ' h.p₁ ∧
      CategoryTheory.CategoryStruct.comp φ h.p₂ = CategoryTheory.CategoryStruct.comp φ' h.p₂ ∧
        CategoryTheory.CategoryStruct.comp φ h.p₃ = CategoryTheory.CategoryStruct.comp φ' h.p₃
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.norm_condExpL2_coe_le : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (hm : m ≤ m0) (f : ↥(MeasureTheory.Lp E 2 μ)), ‖↑((MeasureTheory.condExpL2 E 𝕜 hm) f)‖ ≤ ‖f‖
-- Lean.Meta.Diagnostics
Lean.Meta.DiagSummary : Type
-- Mathlib.Analysis.InnerProductSpace.Basic
isPosSemidef_inner : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E], (innerₗ E).IsPosSemidef
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.Num.add.match_1.splitter : (motive : Num → Num → Sort u_1) →
  (x x_1 : Num) →
    ((a : Num) → motive Num.zero a) →
      ((b : Num) → (b = Num.zero → False) → motive b Num.zero) →
        ((a b : PosNum) → motive (Num.pos a) (Num.pos b)) → motive x x_1
-- Mathlib.Algebra.Polynomial.Div
Polynomial.zero_modByMonic : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R), 0 %ₘ p = 0
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.if_eq_cond : ∀ {α : Sort u_1} {b : Bool} {x y : α}, (if b = true then x else y) = bif b then x else y
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.diagramIsoCospan_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C) (X : CategoryTheory.Limits.WalkingCospan),
  (CategoryTheory.Limits.diagramIsoCospan F).inv.app X = ((fun j => CategoryTheory.eqToIso ⋯) X).inv
-- Mathlib.RingTheory.Trace.Basic
/-- The trace of a nilpotent element is nilpotent.  -/
Algebra.isNilpotent_trace_of_isNilpotent : ∀ {R : Type u_7} {S : Type u_8} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S},
  IsNilpotent x → IsNilpotent ((Algebra.trace R S) x)
-- Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
arithGeom.eq_def : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] (a b u₀ : R) (x : ℕ),
  arithGeom a b u₀ x =
    match x with
    | 0 => u₀
    | n.succ => a * arithGeom a b u₀ n + b
-- Init.Data.List.Lemmas
List.append_left_inj : ∀ {α : Type u_1} {s₁ s₂ : List α} (t : List α), s₁ ++ t = s₂ ++ t ↔ s₁ = s₂
-- Lean.Environment
Lean.Kernel.Exception.typeExpected : Lean.Kernel.Environment → Lean.LocalContext → Lean.Expr → Lean.Kernel.Exception
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_of_get_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {v : β k} {w : k ∈ t}, t.get k w = v → k ∈ t
-- Mathlib.Analysis.Normed.Order.Lattice
norm_abs_sub_abs : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] (a b : α),
  ‖|a| - |b|‖ ≤ ‖a - b‖
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.trace_toEnd_genWeightSpaceChain_eq_zero : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [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] [inst_6 : LieModule R L M]
  {H : LieSubalgebra R L} (α χ : ↥H → R) (p q : ℤ) [inst_7 : H.IsCartanSubalgebra] [inst_8 : IsNoetherian R L],
  LieModule.genWeightSpace M (p • α + χ) = ⊥ →
    LieModule.genWeightSpace M (q • α + χ) = ⊥ →
      ∀ {x : ↥H},
        x ∈ LieAlgebra.corootSpace α →
          (LinearMap.trace R ↥(LieModule.genWeightSpaceChain M α χ p q))
              ((LieModule.toEnd R ↥H ↥(LieModule.genWeightSpaceChain M α χ p q)) x) =
            0
-- Mathlib.Topology.UniformSpace.Basic
/-- A uniform space with the discrete uniformity has the discrete topology.  -/
discreteTopology_of_discrete_uniformity : ∀ {α : Type ua} [hα : UniformSpace α], uniformity α = Filter.principal SetRel.id → DiscreteTopology α
-- Mathlib.RingTheory.Kaehler.TensorProduct
/-- (Implementation). `B = S ⊗[R] A`-module structure on `S ⊗[R] Ω[A⁄R]`.  -/
KaehlerDifferential.moduleBaseChange' : (R : Type u_1) →
  (S : Type u_2) →
    (A : Type u_3) →
      (B : Type u_4) →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : CommRing A] →
                [inst_4 : CommRing B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      [inst_7 : Algebra A B] →
                        [inst_8 : Algebra S B] →
                          [inst_9 : IsScalarTower R A B] →
                            [inst_10 : IsScalarTower R S B] →
                              [Algebra.IsPushout R S A B] → Module B (TensorProduct R S Ω[A⁄R])
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.Skeleton.ext : ∀ (X Y : FintypeCat.Skeleton), X.len = Y.len → X = Y
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Etale.etale_appLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.Etale f] {U : Y.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {V : X.Opens},
      AlgebraicGeometry.IsAffineOpen V →
        ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).Etale
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A non-unital subalgebra of a non-unital normed ring is also a non-unital normed ring, with the
restriction of the norm.  -/
NonUnitalSubalgebra.nonUnitalNormedRing : {𝕜 : Type u_5} →
  [inst : CommRing 𝕜] →
    {E : Type u_6} →
      [inst_1 : NonUnitalNormedRing E] → [inst_2 : Module 𝕜 E] → (s : NonUnitalSubalgebra 𝕜 E) → NonUnitalNormedRing ↥s
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.llr_smul_nnreal_same : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [μ.HaveLebesgueDecomposition ν],
  μ.AbsolutelyContinuous ν → ∀ (c : NNReal), c ≠ 0 → MeasureTheory.llr (c • μ) (c • ν) =ᵐ[μ] MeasureTheory.llr μ ν
-- Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
HasDerivAt.clog : ∀ {f : ℂ → ℂ} {f' x : ℂ},
  HasDerivAt f f' x → f x ∈ Complex.slitPlane → HasDerivAt (fun t => Complex.log (f t)) (f' / f x) x
-- Mathlib.Algebra.Group.Basic
zero_eq_neg : ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a : α}, 0 = -a ↔ a = 0
-- Mathlib.Data.Matrix.Mul
Matrix.mulVec_vecMul : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : NonUnitalCommSemiring α] [inst_1 : Fintype n]
  [inst_2 : Fintype o] (A : Matrix m n α) (B : Matrix o n α) (x : o → α),
  A.mulVec (Matrix.vecMul x B) = (A * B.transpose).mulVec x
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.range_prod_map : ∀ {W X Y Z : TopCat} (f : W ⟶ Y) (g : X ⟶ Z),
  Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.map f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.fst) ⁻¹'
        Set.range ⇑(CategoryTheory.ConcreteCategory.hom f) ∩
      ⇑(CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.snd) ⁻¹'
        Set.range ⇑(CategoryTheory.ConcreteCategory.hom g)
-- Mathlib.Algebra.BigOperators.Finsupp.Fin
finTwoArrowEquiv'_apply : ∀ (M : Type u_1) [inst : Zero M] (a : Fin 2 →₀ M), (finTwoArrowEquiv' M) a = (a 0, a 1)
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.coe_mul : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  (x y : ↥S), ↑(x * y) = ↑x * ↑y
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ ∪ t₂).getKey? k = t₂.getKey? k
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
CurveIntegrable.zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {γ : Path a b},
  CurveIntegrable 0 γ
-- Mathlib.Order.Preorder.Chain
IsChain.total : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {x y : α} [Std.Refl r], IsChain r s → x ∈ s → y ∈ s → r x y ∨ r y x
-- Lean.Parser.Do
Lean.Parser.Term.doIfLet.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.LiminfLimsup
Filter.bliminf_sup_le_and_aux_left : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α},
  Filter.bliminf u f p ≤ Filter.bliminf u f fun x => p x ∧ q x
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
measurable_enorm : ∀ {ε : Type u_5} [inst : MeasurableSpace ε] [inst_1 : TopologicalSpace ε] [inst_2 : ContinuousENorm ε]
  [OpensMeasurableSpace ε], Measurable enorm
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv'.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  (A : CategoryTheory.Functor C ℰ) (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) (E : ℰ),
  CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv' A P E =
    {
      toFun := fun f =>
        {
          app := fun x =>
            TypeCat.ofHom fun x_1 =>
              { down := f.app (CategoryTheory.CostructuredArrow.mk (CategoryTheory.uliftYonedaEquiv.symm x_1)) },
          naturality := ⋯ },
      invFun := fun g =>
        { app := fun y => (CategoryTheory.uliftYonedaEquiv (CategoryTheory.CategoryStruct.comp y.hom g)).down,
          naturality := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.hom_ext_iff : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y Z : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] {f g : Z ⟶ X ⊞ Y},
  f = g ↔
    CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst =
        CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.fst ∧
      CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd =
        CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.snd
-- Init.Data.List.Erase
List.getLast_eraseP_mem : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} (h : List.eraseP p xs ≠ []), (List.eraseP p xs).getLast h ∈ xs
-- Mathlib.Algebra.Category.Grp.Colimits
AddCommGrpCat.Colimits.colimitCocone_pt : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat)
  [inst_1 : DecidableEq J] [inst_2 : Small.{w, max w u} (AddCommGrpCat.Colimits.Quot F)],
  (AddCommGrpCat.Colimits.colimitCocone F).pt = AddCommGrpCat.of (Shrink.{w, max u w} (AddCommGrpCat.Colimits.Quot F))
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} {I : Ideal A}
  (H : g.IsWeierstrassFactorizationAt f h I) [inst_1 : IsAdicComplete I A] (x : PowerSeries A ⧸ Ideal.span {g}),
  H.algEquivQuotient.symm x = (Ideal.Quotient.mk (Ideal.span {f})) (⋯.mod' ((Ideal.quotientEquivAlgOfEq A ⋯) x))
-- Mathlib.CategoryTheory.Equivalence.Symmetry
CategoryTheory.Equivalence.symmEquiv_counitIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (D : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D],
  (CategoryTheory.Equivalence.symmEquiv C D).counitIso =
    CategoryTheory.NatIso.ofComponents (fun e => (CategoryTheory.Iso.refl (Opposite.unop e)).op) ⋯
-- Init.Data.BitVec.Lemmas
BitVec.sub_eq_self : ∀ {x : BitVec 1}, -x = x
-- Mathlib.Analysis.Normed.Ring.Basic
NormedRing.mk : {α : Type u_5} →
  [toNorm : Norm α] →
    [toRing : Ring α] →
      [toMetricSpace : MetricSpace α] →
        (∀ (x y : α), dist x y = ‖-x + y‖) → (∀ (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖) → NormedRing α
-- Mathlib.Data.Seq.Computation
/-- `c₁ <|> c₂` calculates `c₁` and `c₂` simultaneously, returning
the first one that gives a result.  -/
Computation.orElse : {α : Type u} → Computation α → (Unit → Computation α) → Computation α
-- Mathlib.Algebra.Ring.SumsOfSquares
isSumSq_iff : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [inst_2 : Zero R] (a : R),
  IsSumSq a ↔ a = 0 ∨ ∃ a_1 s, IsSumSq s ∧ a = a_1 * a_1 + s
-- Mathlib.Algebra.Group.End
Equiv.mul_swap_eq_swap_mul : ∀ {α : Type u_4} [inst : DecidableEq α] (f : Equiv.Perm α) (x y : α), f * Equiv.swap x y = Equiv.swap (f x) (f y) * f
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.ofComponents.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (app : (X : C) → F.obj X ≅ G.obj X)
  (naturality :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.CategoryStruct.comp (F.map f) (app Y).hom =
        CategoryTheory.CategoryStruct.comp (app X).hom (G.map f)),
  CategoryTheory.NatIso.ofComponents app naturality =
    { hom := { app := fun X => (app X).hom, naturality := ⋯ }, inv := { app := fun X => (app X).inv, naturality := ⋯ },
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.Analysis.Convex.BetweenList
List.sbtw_cons : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] {p : P} {l : List P},
  List.Sbtw R (p :: l) ↔ List.Pairwise (Sbtw R p) l ∧ List.Sbtw R l ∧ l ≠ [p]
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_rw₁ : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f f' : α → β},
  f =ᵐ[μ] f' → ∀ (g : β → ENNReal), ∫⁻ (a : α), g (f a) ∂μ = ∫⁻ (a : α), g (f' a) ∂μ
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Format a `RefinedDiscrTree.LazyEntry`.  -/
Lean.Meta.RefinedDiscrTree.LazyEntry.format : Lean.Meta.RefinedDiscrTree.LazyEntry → Std.Format
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanIleanInfoParams.mk.sizeOf_spec : ∀ (version : ℕ) (references : Lean.Lsp.ModuleRefs) (decls : Lean.Lsp.Decls),
  sizeOf { version := version, references := references, decls := decls } =
    1 + sizeOf version + sizeOf references + sizeOf decls
-- Mathlib.Order.RelSeries
LTSeries.map_toFun : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (p : LTSeries α) (f : α → β)
  (hf : StrictMono f) (a : Fin (p.length + 1)), (p.map f hf).toFun a = f (p.toFun a)
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigOWith_of_div_tendsto_nhds : ∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {C : ℝ} {a : 𝕜} {f g : α → 𝕜} {l : Filter α},
  Filter.Tendsto (fun x => g x / f x) l (nhds a) → 0 < C → C⁻¹ < ‖a‖ → Asymptotics.IsBigOWith C l f g
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instMonadBacktrackSavedStateGrindM : Lean.MonadBacktrack Lean.Meta.Grind.SavedState Lean.Meta.Grind.GrindM
-- Mathlib.Data.Fin.Tuple.Basic
Fin.update_insertNth : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (x y : α p) (f : (i : Fin n) → α (p.succAbove i)),
  Function.update (p.insertNth x f) p y = p.insertNth y f
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
SeminormFamily.comp_smul_nnreal : ∀ {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι : Type u_9} [inst : NormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : NormedField 𝕜₂] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂] (q : SeminormFamily 𝕜₂ F ι) (c : NNReal)
  (f : E →ₛₗ[σ₁₂] F), c • q.comp f = (c • q).comp f
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.lt_rpow_iff_log_lt : ∀ {x y z : ℝ}, 0 < x → 0 < y → (x < y ^ z ↔ Real.log x < z * Real.log y)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.powerBifunctor_map_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X Y : Type tᵒᵖ}
  (f : X ⟶ Y) (x : CategoryTheory.Limits.FormalCoproduct C),
  (CategoryTheory.Limits.FormalCoproduct.powerBifunctor.map f).app x =
    x.mapPower ⇑(CategoryTheory.ConcreteCategory.hom f.unop)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
nnnorm_apply_le_nnnorm_cfcₙ : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) ⦃x : 𝕜⦄,
  x ∈ quasispectrum 𝕜 a →
    autoParam (ContinuousOn f (quasispectrum 𝕜 a)) nnnorm_apply_le_nnnorm_cfcₙ._auto_1 →
      autoParam (f 0 = 0) nnnorm_apply_le_nnnorm_cfcₙ._auto_3 →
        autoParam (p a) nnnorm_apply_le_nnnorm_cfcₙ._auto_5 → ‖f x‖₊ ≤ ‖cfcₙ f a‖₊
-- Std.Sync.Broadcast
/-- A multi-subscriber broadcast that delivers each message to all current subscribers.
Supports only bounded buffering and an asynchronous API; to switch into
synchronous mode use `Broadcast.sync`.

Unlike `Std.Channel`, each message is received by **every** subscriber instead of just one.
Subscribers only receive messages sent after they have subscribed (unless otherwise specified).
 -/
Std.Broadcast : Type → Type
-- Mathlib.Algebra.Ring.Int.Parity
Int.two_mul_ediv_two_of_odd : ∀ {n : ℤ}, Odd n → 2 * (n / 2) = n - 1
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.ι_map : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : β → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] [inst_2 : CategoryTheory.Limits.HasCoproduct g]
  (p : (b : β) → f b ⟶ g b) (b : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) (CategoryTheory.Limits.Sigma.map p) =
    CategoryTheory.CategoryStruct.comp (p b) (CategoryTheory.Limits.Sigma.ι g b)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.getLast_darts_eq_lastDart : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : p.darts ≠ []), p.darts.getLast hnil = p.lastDart ⋯
-- Mathlib.MeasureTheory.VectorMeasure.Integral
/-- Eta-expanded form of `MeasureTheory.VectorMeasure.Integrable.smul` -/
MeasureTheory.VectorMeasure.Integrable.fun_smul : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {f : X → E} {μ : MeasureTheory.VectorMeasure X F} {𝕜 : Type u_8}
  [inst_2 : NormedAddCommGroup 𝕜] [inst_3 : SMulZeroClass 𝕜 E] [IsBoundedSMul 𝕜 E] (c : 𝕜),
  μ.Integrable f → μ.Integrable fun i => c • f i
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.nsmul : {α : Type u_1} → [inst : AddMonoid α] → [inst_1 : Preorder α] → [AddLeftMono α] → SMul ℕ { x // 0 ≤ x }
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
CategoryTheory.Abelian.Pseudoelement.pseudoApply_mk' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q)
  (a : CategoryTheory.Over P),
  CategoryTheory.Abelian.Pseudoelement.pseudoApply f ⟦a⟧ =
    ⟦CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp a.hom f)⟧
-- Mathlib.Analysis.Calculus.MeanValue
/-- The mean value theorem on a convex set in dimension 1: if the derivative of a function is
bounded by `C` on `s`, then the function is `C`-Lipschitz on `s`.
Version with `deriv` and `LipschitzOnWith`.  -/
Convex.lipschitzOnWith_of_nnnorm_deriv_le : ∀ {𝕜 : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] {f : 𝕜 → G}
  {s : Set 𝕜} {C : NNReal},
  (∀ x ∈ s, DifferentiableAt 𝕜 f x) → (∀ x ∈ s, ‖deriv f x‖₊ ≤ C) → Convex ℝ s → LipschitzOnWith C f s
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
/-- The property of reflecting pullbacks expressed in terms of binary fans.  -/
CategoryTheory.Limits.isLimitOfIsLimitPullbackConeMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {W X Y Z : C} →
            {f : X ⟶ Z} →
              {g : Y ⟶ Z} →
                {h : W ⟶ X} →
                  {k : W ⟶ Y} →
                    (comm : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g) →
                      [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan f g) G] →
                        CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (G.map h) (G.map k) ⋯) →
                          CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk h k comm)
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
GenContFract.IntFractPair.of.eq_1 : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] (v : K),
  GenContFract.IntFractPair.of v = { b := ⌊v⌋, fr := Int.fract v }
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLT?.go.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option α) (size : ℕ) (k' : α) (v : β k')
  (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getKeyLT?.go k best (Std.DTreeMap.Internal.Impl.inner size k' v l r) =
    match compare k k' with
    | Ordering.gt => Std.DTreeMap.Internal.Impl.getKeyLT?.go k (some k') r
    | x => Std.DTreeMap.Internal.Impl.getKeyLT?.go k best l
-- Mathlib.Algebra.Field.Subfield.Defs
SubfieldClass.coe_nnratCast : ∀ {K : Type u} [inst : DivisionRing K] {S : Type u_1} [inst_1 : SetLike S K] [h : SubfieldClass S K] (s : S) (q : ℚ≥0),
  ↑↑q = ↑q
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
MeasureTheory.integrableOn_fun_norm_addHaar : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] {F : Type u_2}
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [Nontrivial E] (μ : MeasureTheory.Measure E)
  [FiniteDimensional ℝ E] [BorelSpace E] [μ.IsAddHaarMeasure] {f : ℝ → F} {r : ℝ},
  MeasureTheory.IntegrableOn (fun x => f ‖x‖) (Metric.ball 0 r) μ ↔
    MeasureTheory.IntegrableOn (fun y => y ^ (Module.finrank ℝ E - 1) • f y) (Set.Ioo 0 r) MeasureTheory.volume
-- Mathlib.Algebra.Group.Prod
Prod.instMonoid : {M : Type u_3} → {N : Type u_4} → [Monoid M] → [Monoid N] → Monoid (M × N)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpParams.mk.injEq : ∀ (toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams)
  (toWorkDoneProgressParams : Lean.Lsp.WorkDoneProgressParams) (context? : Option Lean.Lsp.SignatureHelpContext)
  (toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams)
  (toWorkDoneProgressParams_1 : Lean.Lsp.WorkDoneProgressParams) (context?_1 : Option Lean.Lsp.SignatureHelpContext),
  ({ toTextDocumentPositionParams := toTextDocumentPositionParams, toWorkDoneProgressParams := toWorkDoneProgressParams,
        context? := context? } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1,
        toWorkDoneProgressParams := toWorkDoneProgressParams_1, context? := context?_1 }) =
    (toTextDocumentPositionParams = toTextDocumentPositionParams_1 ∧
      toWorkDoneProgressParams = toWorkDoneProgressParams_1 ∧ context? = context?_1)
-- Mathlib.Order.Antisymmetrization
Relation.SymmGen.of_symmGen_of_antisymmRel : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α],
  Relation.SymmGen (fun x1 x2 => x1 ≤ x2) a b →
    AntisymmRel (fun x1 x2 => x1 ≤ x2) b c → Relation.SymmGen (fun x1 x2 => x1 ≤ x2) a c