mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.HashMap.Basic
/-- Looks up an element in the map with key `a`. Returns `b₀` if the element is not found.
```
def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.findD "one" 0 = 1
hashMap.findD "three" 0 = 0
```
 -/
Batteries.HashMap.findD : {α : Type u_1} → {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α β → α → β → β
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_1.congr_eq_1 : ∀ {n : ℕ}
  (motive : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1)
  (x : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty)
  (h_3 :
    (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
      (b : Bool) → motive (Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b)))
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit),
  x = Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth →
    (match x with
      | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth => h_1 ()
      | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty => h_2 ()
      | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b) => h_3 l b
      | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit => h_4 ()) ≍
      h_1 ()
-- Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
ContinuousLinearMapWOT.instStarModuleId : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F], StarModule 𝕜 (F →WOT[𝕜] F)
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.fromSpecResidueField.eq_1 : ∀ (X : AlgebraicGeometry.Scheme) (x : ↥X),
  X.fromSpecResidueField x =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.residue x)) (X.fromSpecStalk x)
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- A completely metrizable space is completely pseudometrizable.  -/
TopologicalSpace.IsCompletelyMetrizableSpace.toIsCompletelyPseudoMetrizableSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [TopologicalSpace.IsCompletelyMetrizableSpace X],
  TopologicalSpace.IsCompletelyPseudoMetrizableSpace X
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.innerSkip_flatMapM : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [inst_3 : Std.Iterator α m β] [inst_4 : Std.Iterator α₂ m γ] {f : β → m (Std.IterM m γ)} {it₁ : Std.IterM m β}
  {it₂ it₂' : Std.IterM m γ},
  it₂.IsPlausibleStep (Std.IterStep.skip it₂') →
    (Std.IterM.flatMapAfterM f it₁ (some it₂)).IsPlausibleStep
      (Std.IterStep.skip (Std.IterM.flatMapAfterM f it₁ (some it₂')))
-- Mathlib.GroupTheory.Commutator.Basic
/-- The commutator of direct product is contained in the direct product of the
commutators. See `commutator_pi_pi_of_finite` for equality given `Fintype η`.  -/
AddSubgroup.addCommutator_pi_pi_le : ∀ {η : Type u_4} {Gs : η → Type u_5} [inst : (i : η) → AddGroup (Gs i)] (H K : (i : η) → AddSubgroup (Gs i)),
  ⁅AddSubgroup.pi Set.univ H, AddSubgroup.pi Set.univ K⁆ ≤ AddSubgroup.pi Set.univ fun i => ⁅H i, K i⁆
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- If the order of a formal power series `f` is finite,
then some coefficient of weight equal to the order of `f` is nonzero.  -/
MvPowerSeries.exists_coeff_ne_zero_and_weightedOrder : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R},
  ↑(MvPowerSeries.weightedOrder w f).toNat = MvPowerSeries.weightedOrder w f →
    ∃ d, (MvPowerSeries.coeff d) f ≠ 0 ∧ ↑((Finsupp.weight w) d) = MvPowerSeries.weightedOrder w f
-- Lean.Parser.Command
Lean.Parser.Command.include.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
alternatingGroup.kleinFour_card_of_card_eq_four : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α],
  Nat.card α = 4 → Nat.card ↥(alternatingGroup.kleinFour α) = 4
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- Version of `exp_decay_sub_atImInfty` stating a less precise result but easier to apply in
practice (not specifying the growth rate precisely).

Note that the `Fact` hypothesis is automatically synthesized for arithmetic subgroups.
The discreteness hypothesis may be unnecessary, but it is satisfied in the cases of interest.  -/
ModularFormClass.exp_decay_sub_atImInfty' : ∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} (f : F)
  [ModularFormClass F Γ k] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] [Fact (IsCusp OnePoint.infty Γ)],
  ∃ c > 0, (fun τ => f τ - UpperHalfPlane.valueAtInfty ⇑f) =O[UpperHalfPlane.atImInfty] fun τ => Real.exp (-c * τ.im)
-- Std.Data.DTreeMap.Internal.Balanced
Std.DTreeMap.Internal.Impl.BalancedAtRoot.eq_1 : ∀ (left right : ℕ),
  Std.DTreeMap.Internal.Impl.BalancedAtRoot left right =
    (left + right ≤ 1 ∨ left ≤ Std.DTreeMap.Internal.delta * right ∧ right ≤ Std.DTreeMap.Internal.delta * left)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderivWithin_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸' : Type u_6} [inst_3 : NormedCommRing 𝔸']
  [inst_4 : NormedAlgebra 𝕜 𝔸'] {c d : E → 𝔸'},
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 c s x →
      DifferentiableWithinAt 𝕜 d s x →
        fderivWithin 𝕜 (c * d) s x = c x • fderivWithin 𝕜 d s x + d x • fderivWithin 𝕜 c s x
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `r` is a negative constant, `fun x ↦ f x * r` tends to negative infinity along a filter `l`
if and only if `f` tends to infinity along `l`.  -/
Filter.tendsto_mul_const_atBot_of_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, r < 0 → (Filter.Tendsto (fun x => f x * r) l Filter.atBot ↔ Filter.Tendsto f l Filter.atTop)
-- Mathlib.Analysis.Convex.StrictConvexSpace
lt_norm_sub_of_not_sameRay : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [StrictConvexSpace ℝ E] {x y : E},
  ¬SameRay ℝ x y → ‖x‖ - ‖y‖ < ‖x - y‖
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_le_sub : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀)
  {x y : R} {g : Γ₀}, g ≤ v x → g ≤ v y → g ≤ v (x - y)
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- If G preserves equalizers and finite products, it preserves finite limits.  -/
CategoryTheory.Limits.preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasFiniteProducts C] (G : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair G]
  [CategoryTheory.Limits.PreservesFiniteProducts G], CategoryTheory.Limits.PreservesFiniteLimits G
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedAddMonoid.instAddMonoid : {α : Type u_1} → {rels : FreeAddMonoid α → FreeAddMonoid α → Prop} → AddMonoid (PresentedAddMonoid rels)
-- Mathlib.Analysis.Analytic.Inverse
FormalMultilinearSeries.leftInv.eq_def : ∀ {𝕜 : 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]
  (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) (x_1 : ℕ),
  p.leftInv i x x_1 =
    match x_1 with
    | 0 => ContinuousMultilinearMap.uncurry0 𝕜 F x
    | 1 => (continuousMultilinearCurryFin1 𝕜 F E).symm ↑i.symm
    | n.succ.succ =>
      -∑ c,
          ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap ↑i.symm) (↑c)
            (p.leftInv i x (↑c).length)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (n : ℤ)
  {X Y : Cᵒᵖ} (f : X ⟶ Y) {Z : Cᵒᵖ} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor Cᵒᵖ n).map f).unop).op
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app Y) h) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app X)
      (CategoryTheory.CategoryStruct.comp f h)
-- Lean.Server.References
/-- Version number of the ilean format.  -/
Lean.Server.Ilean.version : Lean.Server.Ilean → ℕ
-- Mathlib.LinearAlgebra.Complex.Module
realPart_comp_subtype_selfAdjoint : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A],
  realPart ∘ₗ (selfAdjoint.submodule ℝ A).subtype = LinearMap.id
-- Init.Data.Nat.Basic
Nat.mul_sub_left_distrib : ∀ (n m k : ℕ), n * (m - k) = n * m - n * k
-- Mathlib.Algebra.Group.Units.Equiv
AddGroup.addRight_bijective : ∀ {G : Type u_5} [inst : AddGroup G] (a : G), Function.Bijective fun x => x + a
-- Lean.Elab.Term.TermElabM
/-- Main loop for `elabTerm`  -/
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.elabTermAux : Option Lean.Expr → Bool → Bool → Lean.Syntax → Lean.Elab.TermElabM Lean.Expr
-- Lean.Parser.Basic
Lean.Parser.orelseInfo : Lean.Parser.ParserInfo → Lean.Parser.ParserInfo → Lean.Parser.ParserInfo
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.throwCannotInferResultingUniverse : {α : Type} → Lean.Level → Lean.MessageData → Lean.Elab.TermElabM α
-- Init.Data.UInt.Bitwise
UInt32.toBitVec_xor : ∀ (a b : UInt32), (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- Adjunction between two 1-morphisms.  -/
CategoryTheory.Bicategory.Adjunction : {B : Type u₁} → [inst : CategoryTheory.Bicategory B] → {a b : B} → (a ⟶ b) → (b ⟶ a) → Type w₁
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- `HasLimit F` represents the mere existence of a limit for `F`.  -/
CategoryTheory.Limits.HasLimit : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor J C → Prop
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Ioc_of_Icc : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a b : ι → α}
  {A B : α} [MeasureTheory.NullSingletonClass μ],
  Filter.Tendsto a l (nhds A) →
    Filter.Tendsto b l (nhds B) → MeasureTheory.AECover (μ.restrict (Set.Ioc A B)) l fun i => Set.Icc (a i) (b i)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_inter_eq_size_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (∀ a ∈ m₁, a ∈ m₂) → (m₁ ∩ m₂).size = m₁.size
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.jacobson_eq_self_of_isMaximal : ∀ {R : Type u} [inst : Ring R] {I : Ideal R} [H : I.IsMaximal], I.jacobson = I
-- Mathlib.Order.WithBot
WithBot.decidableLT.eq_3 : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] (a b : α),
  WithBot.decidableLT (some a) (some b) = decidable_of_iff' (a < b) ⋯
-- Mathlib.Data.Nat.Count
Nat.count_lt_card : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {n : ℕ} (hp : (Set.ofPred p).Finite), p n → Nat.count p n < hp.toFinset.card
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- Any two zero objects are isomorphic.  -/
CategoryTheory.Limits.IsZero.iso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → CategoryTheory.Limits.IsZero X → CategoryTheory.Limits.IsZero Y → (X ≅ Y)
-- Mathlib.Topology.Algebra.ConstMulAction
Units.continuousConstSMul : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : Monoid M] [inst_2 : MulAction M α]
  [ContinuousConstSMul M α], ContinuousConstSMul Mˣ α
-- Mathlib.MeasureTheory.Function.UnifTight
MeasureTheory.unifTight_iff_real : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : NormedAddCommGroup β] {x : MeasurableSpace α} (f : ι → α → β)
  (p : ENNReal) (μ : MeasureTheory.Measure α),
  MeasureTheory.UnifTight f p μ ↔
    ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), MeasureTheory.eLpNorm (sᶜ.indicator (f i)) p μ ≤ ENNReal.ofReal ε
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopic.refl : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y)), f.Homotopic f
-- Mathlib.LinearAlgebra.Semisimple
Module.End.eq_zero_of_isNilpotent_isSemisimple : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {f : Module.End R M}, IsNilpotent f → f.IsSemisimple → f = 0
-- Mathlib.CategoryTheory.Limits.FinallySmall
/-- An arbitrarily chosen small model for an initially small category.  -/
CategoryTheory.InitialModel : (J : Type u) → [inst : CategoryTheory.Category.{v, u} J] → [CategoryTheory.InitiallySmall J] → Type w
-- Init.Data.Vector.Lex
Vector.mk_lt_mk : ∀ {α : Type u_1} {n : ℕ} {data₁ : Array α} {size₁ : data₁.size = n} {data₂ : Array α} {size₂ : data₂.size = n}
  [inst : LT α], Vector.mk data₁ size₁ < Vector.mk data₂ size₂ ↔ data₁ < data₂
-- Mathlib.MeasureTheory.Integral.Average
/-- Average value of an `ℝ≥0∞`-valued function `f` w.r.t. a measure `μ`, denoted `⨍⁻ x, f x ∂μ`.

It is equal to `(μ univ)⁻¹ * ∫⁻ x, f x ∂μ`, so it takes value zero if `μ` is an infinite measure. If
`μ` is a probability measure, then the average of any function is equal to its integral.

For the average on a set, use `⨍⁻ x in s, f x ∂μ`, defined as `⨍⁻ x, f x ∂(μ.restrict s)`. For the
average w.r.t. the volume, one can omit `∂volume`.  -/
MeasureTheory.laverage : {α : Type u_1} → {m0 : MeasurableSpace α} → MeasureTheory.Measure α → (α → ENNReal) → ENNReal
-- Mathlib.Data.Seq.Basic
Stream'.Seq.take.eq_def : ∀ {α : Type u} (x : ℕ) (x_1 : Stream'.Seq α),
  Stream'.Seq.take x x_1 =
    match x, x_1 with
    | 0, x => []
    | n.succ, s =>
      match s.destruct with
      | none => []
      | some (x, r) => x :: Stream'.Seq.take n r
-- Mathlib.Analysis.Complex.UnitDisc.Basic
/-- Imaginary part of a point of the unit disc.  -/
Complex.UnitDisc.im : Complex.UnitDisc → ℝ
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instIntCast : {α : Type u} →
  [inst : TopologicalSpace α] →
    {β : Type u_2} → [inst_1 : PseudoMetricSpace β] → [IntCast β] → IntCast (BoundedContinuousFunction α β)
-- Mathlib.Order.WellFounded
/-- **Alias** of `WellFounded.asymm`. -/
WellFounded.isAsymm : ∀ {α : Type u_1} {r : α → α → Prop}, WellFounded r → Std.Asymm r
-- Mathlib.Data.Finset.Prod
Finset.singleton_product_singleton : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β}, {a} ×ˢ {b} = {(a, b)}
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.units_smul_def : ∀ {M : Type u_2} [inst : Monoid M] (g : ConjAct Mˣ) (h : M),
  g • h = ↑(ConjAct.ofConjAct g) * h * ↑(ConjAct.ofConjAct g)⁻¹
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_insertListConst_of_mem : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α}
  {v fallback : β},
  Std.Internal.List.DistinctKeys l →
    (k == k') = true →
      List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert →
        (k, v) ∈ toInsert → Std.Internal.List.getValueD k' (Std.Internal.List.insertListConst l toInsert) fallback = v
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.rightOp_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C),
  X.rightOp.left = Opposite.op X.right
-- Std.Do.SPred.Laws
Std.Do.SPred.imp_curry : ∀ {σs : List (Type u)} {P Q : Std.Do.SVal.StateTuple σs → Prop},
  ((Std.Do.SVal.curry fun t => { down := P t }) → Std.Do.SVal.curry fun t => { down := Q t }) ⊣⊢ₛ
    Std.Do.SVal.curry fun t => { down := P t → Q t }
-- Mathlib.Algebra.Star.StarProjection
/-- The sum of star projections is a star projection if their product is `0`.  -/
IsStarProjection.add : ∀ {R : Type u_1} {p q : R} [inst : NonUnitalNonAssocSemiring R] [inst_1 : StarRing R],
  IsStarProjection p → IsStarProjection q → p * q = 0 → IsStarProjection (p + q)
-- Lean.Util.ForEachExprWhere
Lean.ForEachExprWhere.visited : {ω : Type} →
  {m : Type → Type} →
    [inst : STWorld ω m] → [MonadLiftT (ST ω) m] → [Monad m] → Lean.Expr → Lean.ForEachExprWhere.ForEachM m Bool
-- Mathlib.CategoryTheory.Generator.Presheaf
CategoryTheory.Presheaf.isSeparating : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasCoproducts A] {ι : Type w} {S : ι → A},
  (CategoryTheory.ObjectProperty.ofObj S).IsSeparating →
    (CategoryTheory.ObjectProperty.ofObj fun x =>
        match x with
        | (X, i) => CategoryTheory.Presheaf.freeYoneda X (S i)).IsSeparating
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_const : ∀ {α : Type u_4} (c : ENNReal), ∑' (x : α), c = ↑(ENat.card α) * c
-- Mathlib.ModelTheory.Substructures
/-- `closure` forms a Galois insertion with the coercion to set.  -/
FirstOrder.Language.Substructure.gi : (L : FirstOrder.Language) →
  (M : Type w) → [inst : L.Structure M] → GaloisInsertion (FirstOrder.Language.Substructure.closure L).toFun SetLike.coe
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.checkTailWs.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializationOptions.mk.sizeOf_spec : ∀ (hasWidgets? : Option Bool) (logCfg? : Option Lean.Lsp.LogConfig),
  sizeOf { hasWidgets? := hasWidgets?, logCfg? := logCfg? } = 1 + sizeOf hasWidgets? + sizeOf logCfg?
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.mulRight_symm : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [inst_2 : MulRightMono α] (a : α),
  (OrderIso.mulRight a).symm = OrderIso.mulRight a⁻¹
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- A side of a right-angled triangle divided by the cosine of the adjacent angle equals the
hypotenuse.  -/
EuclideanGeometry.dist_div_cos_oangle_right_of_oangle_eq_pi_div_two : ∀ {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},
  EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → dist p₃ p₂ / (EuclideanGeometry.oangle p₂ p₃ p₁).cos = dist p₁ p₃
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
/-- If `f g : α → ℝ≥0∞` are two functions and one of them is (a.e.) measurable, then the Lebesgue
integral of `f + g` equals the sum of integrals. This lemma assumes that `f` is integrable, see also
`MeasureTheory.lintegral_add_right` and primed versions of these lemmas.  -/
MeasureTheory.lintegral_add_left : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  Measurable f → ∀ (g : α → ENNReal), ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.spanningSetsIndex.congr_simp : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ μ_1 : MeasureTheory.Measure α) (e_μ : μ = μ_1)
  [inst : MeasureTheory.SigmaFinite μ] (x x_1 : α),
  x = x_1 → MeasureTheory.spanningSetsIndex μ x = MeasureTheory.spanningSetsIndex μ_1 x_1
-- Mathlib.Topology.Algebra.InfiniteSum.Real
dist_le_tsum_dist_of_tendsto : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {f : ℕ → α} {a : α},
  (Summable fun n => dist (f n) (f n.succ)) →
    Filter.Tendsto f Filter.atTop (nhds a) → ∀ (n : ℕ), dist (f n) a ≤ ∑' (m : ℕ), dist (f (n + m)) (f (n + m).succ)
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalProducts
/-- A family of objects (parametrized by any `J : Type w`) has a conical product.  -/
CategoryTheory.Enriched.HasConicalProducts.hasConicalLimitsOfShape : ∀ {V : outParam (Type u')} {inst : CategoryTheory.Category.{v', u'} V} {inst_1 : CategoryTheory.MonoidalCategory V}
  {C : Type u} {inst_2 : CategoryTheory.Category.{v, u} C} {inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C}
  [self : CategoryTheory.Enriched.HasConicalProducts V C] (J : Type w),
  CategoryTheory.Enriched.HasConicalLimitsOfShape (CategoryTheory.Discrete J) V C
-- Mathlib.GroupTheory.GroupAction.Hom
/-- `Prod.fst` as a bundled `MulActionHom`.  -/
MulActionHom.fst : (M : Type u_1) → (α : Type u_2) → (β : Type u_3) → [inst : SMul M α] → [inst_1 : SMul M β] → α × β →ₑ[id] α
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.measure_stieltjesFunction_univ : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : ProbabilityTheory.IsMeasurableRatCDF f) (a : α),
  (hf.stieltjesFunction a).measure Set.univ = 1
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.map.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β), FreeAbelianGroup.map f = FreeAbelianGroup.lift (FreeAbelianGroup.of ∘ f)
-- Std.Data.DTreeMap.Basic
/-- Inserts multiple mappings into the tree map by iterating over the given collection and calling
`insertIfNew`. If the same key appears multiple times, the first occurrence takes precedence.
 -/
Std.DTreeMap.insertManyIfNew : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {ρ : Type u_1} → [ForIn Id ρ ((a : α) × β a)] → Std.DTreeMap α β cmp → ρ → Std.DTreeMap α β cmp
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The `vectorSpan` is the span of the pairwise subtractions with a given point on the right,
excluding the subtraction of that point from itself.  -/
vectorSpan_eq_span_vsub_set_right_ne : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P} {p : P},
  p ∈ s → vectorSpan k s = Submodule.span k ((fun x => x -ᵥ p) '' (s \ {p}))
-- Mathlib.Data.Set.Image
Set.inter_preimage_subset : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) (f : α → β), s ∩ f ⁻¹' t ⊆ f ⁻¹' (f '' s ∩ t)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.awayMapₐ_apply : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] (𝒜 : ι → σ)
  [inst_5 : GradedRing 𝒜] {e : ι} {f g : A} (hg : g ∈ 𝒜 e) {x : A} (hx : x = f * g)
  (a : HomogeneousLocalization.Away 𝒜 f),
  (HomogeneousLocalization.awayMapₐ 𝒜 hg hx) a = (HomogeneousLocalization.awayMap 𝒜 hg hx) a
-- Mathlib.AlgebraicGeometry.GluingOneHypercover
AlgebraicGeometry.Scheme.GlueData.oneHypercover_Y : ∀ (D : AlgebraicGeometry.Scheme.GlueData) (i₁ i₂ : D.J) (x : PUnit.{u + 1}), D.oneHypercover.Y x = D.V (i₁, i₂)
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- A clique is a set of vertices whose induced graph is complete.  -/
SimpleGraph.isClique_iff_induce_eq : ∀ {α : Type u_1} (G : SimpleGraph α) {s : Set α}, G.IsClique s ↔ SimpleGraph.induce s G = ⊤
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.factor_surjective : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p p' : Submodule R M}
  (H : p ≤ p'), Function.Surjective ⇑(Submodule.factor H)