mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Square
/-- the top-left object  -/
CategoryTheory.Square.X₁ : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Square C → C
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
CategoryTheory.Bicategory.LeftExtension.IsKan.uniqueUpToIso_inv_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  {s t : CategoryTheory.Bicategory.LeftExtension f g} (P : s.IsKan) (Q : t.IsKan),
  CategoryTheory.StructuredArrow.Hom.right (P.uniqueUpToIso Q).inv = Q.desc s
-- Mathlib.Logic.Equiv.Multiset
/-- If `α` is encodable, then so is `Multiset α`.  -/
Multiset.encodable : {α : Type u_1} → [Encodable α] → Encodable (Multiset α)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.union_insert_right_equiv_insert_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {p : (a : α) × β a}, t₁.WF → t₂.WF → (t₁ ∪ t₂.insert p.fst p.snd).Equiv ((t₁ ∪ t₂).insert p.fst p.snd)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.containsThenInsertIfNew!_fst : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew! k v t).1 = Std.DTreeMap.Internal.Impl.contains k t
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- The morphism property on `Over X` induced by a morphism property on `C`.  -/
CategoryTheory.MorphismProperty.over : {T : Type u_3} →
  [inst : CategoryTheory.Category.{v_3, u_3} T] →
    CategoryTheory.MorphismProperty T → {X : T} → CategoryTheory.MorphismProperty (CategoryTheory.Over X)
-- Mathlib.LinearAlgebra.Eigenspace.Triangularizable
/-- In finite dimensions, over an algebraically closed field, the generalized eigenspaces of any
linear endomorphism span the whole space.  -/
Module.End.iSup_maxGenEigenspace_eq_top : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [IsAlgClosed K]
  [FiniteDimensional K V] (f : Module.End K V), ⨆ μ, f.maxGenEigenspace μ = ⊤
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.mem_iSup_of_chain : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (a : ℕ →o Submodule R M) (m : M), m ∈ ⨆ k, a k ↔ ∃ k, m ∈ a k
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
/-- The type of morphisms in `SemiNormedGrp`  -/
SemiNormedGrp.Hom : SemiNormedGrp → SemiNormedGrp → Type u
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles_X₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles._auto_1),
  (X.kernelSequenceCycles f g n₀ n₁ hn₁).X₃ = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.instFunLike : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {f₀ f₁ : C(X, Y)} → FunLike (f₀.Homotopy f₁) (↑unitInterval × X) Y
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
_private.Mathlib.Combinatorics.SimpleGraph.CycleGraph.0.SimpleGraph.cycleGraph.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → (Unit → motive 1) → ((n : ℕ) → motive n.succ.succ) → motive x
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.applyPartition.go.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Ordering.lt = Ordering.lt → motive Ordering.lt)
  (h_2 : Ordering.lt = Ordering.eq → motive Ordering.eq) (h_3 : Ordering.lt = Ordering.gt → motive Ordering.gt),
  (match h : Ordering.lt with
    | Ordering.lt => h_1 h
    | Ordering.eq => h_2 h
    | Ordering.gt => h_3 h) =
    h_1 ⋯
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.map_right_cancel : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {x y : R} {c : ↥M},
  (algebraMap R S) (↑c * x) = (algebraMap R S) (↑c * y) → (algebraMap R S) x = (algebraMap R S) y
-- Mathlib.Data.EReal.Basic
EReal.toReal_eq_zero_iff : ∀ {x : EReal}, x.toReal = 0 ↔ x = 0 ∨ x = ⊤ ∨ x = ⊥
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.ae_compProd_of_ae_fst : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  (κ : ProbabilityTheory.Kernel α β) {p : α → Prop},
  MeasurableSet {x | p x} → (∀ᵐ (a : α) ∂μ, p a) → ∀ᵐ (x : α × β) ∂μ.compProd κ, p x.1
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.core.inj : ∀ {a b : Lean.Expr} {lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr} {a_1 b_1 : Lean.Expr}
  {lhs_1 rhs_1 : Lean.Meta.Grind.Arith.Linear.LinExpr},
  Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.core a b lhs rhs =
      Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.core a_1 b_1 lhs_1 rhs_1 →
    a = a_1 ∧ b = b_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.RightHomologyMapData.map_φH : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂}
  {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : h₁.IsPreservedBy F]
  [inst_6 : h₂.IsPreservedBy F], (ψ.map F).φH = F.map ψ.φH
-- Mathlib.Topology.MetricSpace.Congruence
/-- Change the index set ι to an index ι' that maps to ι.  -/
Congruent.index_map : ∀ {ι : Type u_1} {ι' : Type u_2} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂}
  [inst : PseudoEMetricSpace P₁] [inst_1 : PseudoEMetricSpace P₂],
  Congruent v₁ v₂ → ∀ (f : ι' → ι), Congruent (v₁ ∘ f) (v₂ ∘ f)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- `IsCharP` instance for `type` if available.  -/
Lean.Meta.Grind.Arith.CommRing.Ring.charInst? : Lean.Meta.Grind.Arith.CommRing.Ring → Option (Lean.Expr × ℕ)
-- Mathlib.Order.Concept
Concept.leftInvOn_ofObjects_intent : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop},
  Set.LeftInvOn Concept.intent (Concept.ofAttributes r) {s | Order.IsIntent r s}
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate_fin_three_of : ∀ {α : Type w} [inst : CommRing α] (a b c d e f g h i : α),
  !![a, b, c; d, e, f; g, h, i].adjugate =
    !![e * i - f * h, -(b * i) + c * h, b * f - c * e;
      -(d * i) + f * g, a * i - c * g, -(a * f) + c * d;
      d * h - e * g, -(a * h) + b * g, a * e - b * d]
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.inf' : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : SemilatticeInf M] {ι : Type u_3} {f : ι → α → M}
  (s : Finset ι),
  (∀ i ∈ s, Function.HasFiniteSupport (f i)) →
    ∀ (hs : s.Nonempty), Function.HasFiniteSupport fun a => s.inf' hs fun x => f x a
-- Init.Data.UInt.Lemmas
UInt16.ofNatLT_uSizeToNat : ∀ (n : USize) (h : n.toNat < UInt16.size), UInt16.ofNatLT n.toNat h = n.toUInt16
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.Pivot.length_listTransvecCol : ∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜),
  (Matrix.Pivot.listTransvecCol M).length = r
-- Mathlib.RingTheory.Ideal.Operations
Submodule.coe_mapAlgEquiv_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_3} {B : Type u_4} [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A ≃ₐ[R] B) (a : Submodule R A),
  ↑((Submodule.mapAlgEquiv f) a) = ⇑f '' ↑a
-- Mathlib.RingTheory.Spectrum.Prime.Basic
/-- The vanishing ideal of a set `t` of points of the prime spectrum of a commutative ring `R` is
the intersection of all the prime ideals in the set `t`.

An element `f` of `R` can be thought of as a dependent function on the prime spectrum of `R`.
At a point `x` (a prime ideal) the function (i.e., element) `f` takes values in the quotient ring
`R` modulo the prime ideal `x`. In this manner, `vanishingIdeal t` is exactly the ideal of `R`
consisting of all "functions" that vanish on all of `t`.
 -/
PrimeSpectrum.vanishingIdeal : {R : Type u} → [inst : CommSemiring R] → Set (PrimeSpectrum R) → Ideal R
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_const_eq_indicator_const : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : Zero M] {s : Set α} {a : α} {t : Set β} {b : β} {c : M},
  (a ∈ s ↔ b ∈ t) → s.indicator (fun x => c) a = t.indicator (fun x => c) b
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- Given `Subgroup`s `H`, `K` of groups `G`, `N` respectively, `H × K` as a subgroup of `G × N`.  -/
Subgroup.prod : {G : Type u_1} → [inst : Group G] → {N : Type u_5} → [inst_1 : Group N] → Subgroup G → Subgroup N → Subgroup (G × N)
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
QuadraticForm.associated_tmul : ∀ {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : AddCommGroup M₁] [inst_3 : AddCommGroup M₂] [inst_4 : Algebra R A] [inst_5 : Module R M₁]
  [inst_6 : Module A M₁] [inst_7 : SMulCommClass R A M₁] [inst_8 : IsScalarTower R A M₁] [inst_9 : Module R M₂]
  [inst_10 : Invertible 2] [inst_11 : Invertible 2] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂),
  QuadraticMap.associated (Q₁.tmul Q₂) =
    LinearMap.BilinForm.tmul (QuadraticMap.associated Q₁) (QuadraticMap.associated Q₂)
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.intEquivalence_functor : AlgCat.intEquivalence.functor = CategoryTheory.forget₂ (AlgCat ℤ) RingCat
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.hasColimit : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {B : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃}
  [inst_3 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  (F : CategoryTheory.Functor J (CategoryTheory.Comma L R))
  [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.Comma.fst L R))]
  [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.Comma.snd L R))]
  [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L], CategoryTheory.Limits.HasColimit F
-- Mathlib.Algebra.Algebra.Hom
AlgHom.toRingHom_toMonoidHom : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B), ↑↑f = ↑f
-- Mathlib.CategoryTheory.ConnectedComponents
/-- The inclusion functor from a connected component to the whole category.  -/
CategoryTheory.ConnectedComponents.ι : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    (j : CategoryTheory.ConnectedComponents J) → CategoryTheory.Functor j.Component J
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β),
  ⇑(g.comp f) = ⇑g ∘ ⇑f
-- Mathlib.Topology.Algebra.LinearMapCompletion
ContinuousLinearMap.coe_completion : ∀ {α : Type u_1} {β : Type u_2} {R₁ : Type u_3} {R₂ : Type u_4} [inst : UniformSpace α] [inst_1 : AddCommGroup α]
  [inst_2 : IsUniformAddGroup α] [inst_3 : Semiring R₁] [inst_4 : Module R₁ α]
  [inst_5 : UniformContinuousConstSMul R₁ α] [inst_6 : Semiring R₂] [inst_7 : UniformSpace β] [inst_8 : AddCommGroup β]
  [inst_9 : IsUniformAddGroup β] [inst_10 : Module R₂ β] [inst_11 : UniformContinuousConstSMul R₂ β] {σ : R₁ →+* R₂}
  (f : α →SL[σ] β), ⇑f.completion = UniformSpace.Completion.map ⇑f
-- Mathlib.CategoryTheory.Monoidal.Braided.Reflection
_private.Mathlib.CategoryTheory.Monoidal.Braided.Reflection.0.CategoryTheory.Monoidal.Reflective.adjRetractionAux.eq_1 : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory D]
  [inst_3 : CategoryTheory.SymmetricCategory D] [inst_4 : CategoryTheory.MonoidalClosed D]
  {R : CategoryTheory.Functor C D} [inst_5 : R.Faithful] [inst_6 : R.Full] {L : CategoryTheory.Functor D C}
  (adj : L ⊣ R) (c : C) (d : D)
  [inst_7 :
    CategoryTheory.IsIso
      (L.map (CategoryTheory.MonoidalCategoryStruct.tensorHom (adj.unit.app (d ⟹ R.obj c)) (adj.unit.app d)))],
  CategoryTheory.Monoidal.Reflective.adjRetractionAux✝ adj c d =
    CategoryTheory.CategoryStruct.comp (β_ d ((L.comp R).obj (d ⟹ R.obj c))).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((L.comp R).obj (d ⟹ R.obj c)) (adj.unit.app d))
        (CategoryTheory.CategoryStruct.comp
          (adj.unit.app
            (CategoryTheory.MonoidalCategoryStruct.tensorObj ((L.comp R).obj (d ⟹ R.obj c)) ((L.comp R).obj d)))
          (CategoryTheory.CategoryStruct.comp
            (R.map
              (CategoryTheory.inv
                (L.map
                  (CategoryTheory.MonoidalCategoryStruct.tensorHom (adj.unit.app (d ⟹ R.obj c)) (adj.unit.app d)))))
            (CategoryTheory.CategoryStruct.comp
              ((L.comp R).map
                (β_ ((CategoryTheory.Functor.id D).obj (d ⟹ R.obj c)) ((CategoryTheory.Functor.id D).obj d)).hom)
              (CategoryTheory.CategoryStruct.comp
                ((L.comp R).map ((CategoryTheory.ihom.ev ((CategoryTheory.Functor.id D).obj d)).app (R.obj c)))
                (CategoryTheory.inv (adj.unit.app (R.1 c))))))))
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.iConvexComb_convexCombPair_comm_left : ∀ {R : Type u_9} {M : Type u_10} {I : Type u_11} [inst : PartialOrder R] [inst_1 : CommSemiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t)
  (h : s + t = 1) (f : Convexity.StdSimplex R I) (m : M) (e : I → M),
  (Convexity.iConvexComb f fun x => Convexity.convexCombPair s t hs ht h (e x) m) =
    Convexity.convexCombPair s t hs ht h (Convexity.iConvexComb f e) m
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- A terminal object in the opposite category is initial in the original category.  -/
CategoryTheory.Limits.IsTerminal.unop : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : Cᵒᵖ} → CategoryTheory.Limits.IsTerminal X → CategoryTheory.Limits.IsInitial (Opposite.unop X)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- When both maps `S.f` and `S.g` of a short complex `S` are zero, this is the homology map
data (for the identity of `S`) which relates the homology data `ofZeros` and
`ofIsColimitCokernelCofork`.  -/
CategoryTheory.ShortComplex.HomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (hf : S.f = 0) →
          (hg : S.g = 0) →
            (c : CategoryTheory.Limits.CokernelCofork S.f) →
              (hc : CategoryTheory.Limits.IsColimit c) →
                CategoryTheory.ShortComplex.HomologyMapData (CategoryTheory.CategoryStruct.id S)
                  (CategoryTheory.ShortComplex.HomologyData.ofZeros S hf hg)
                  (CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork S hg c hc)
-- Mathlib.Tactic.NormNum.Result
/-- A shortcut (non)instance for `AddMonoidWithOne α`
from `Semiring α` to shrink generated proofs.  -/
Mathlib.Meta.NormNum.instAddMonoidWithOne' : {α : Type u} → [Semiring α] → AddMonoidWithOne α
-- Mathlib.RepresentationTheory.Intertwining
/-- A coercion from intertwining maps to additive monoid homomorphisms.  -/
Representation.IntertwiningMap.coeFnAddMonoidHom : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    (ρ : Representation A G V) → (σ : Representation A G W) → ρ.IntertwiningMap σ →+ V → W
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LEquiv.mk.sizeOf_spec : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (toLHom : L →ᴸ L') (invLHom : L' →ᴸ L)
  (left_inv : invLHom.comp toLHom = FirstOrder.Language.LHom.id L)
  (right_inv : toLHom.comp invLHom = FirstOrder.Language.LHom.id L'),
  sizeOf { toLHom := toLHom, invLHom := invLHom, left_inv := left_inv, right_inv := right_inv } =
    1 + sizeOf toLHom + sizeOf invLHom + sizeOf left_inv + sizeOf right_inv
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.union_ae_eq_right_iff_ae_subset : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, s ∪ t =ᵐ[μ] t ↔ s ≤ᵐ[μ] t
-- Mathlib.Algebra.BigOperators.Field
Finset.dens_biUnion_le : ∀ {α : Type u_3} {β : Type u_4} [inst : Fintype β] {s : Finset α} {t : α → Finset β} [inst_1 : DecidableEq β],
  (s.biUnion t).dens ≤ ∑ a ∈ s, (t a).dens
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsRankOneDiscrete.generator_mem_valueGroup : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] (v : Valuation A Γ)
  [inst_2 : v.IsRankOneDiscrete], Valuation.IsRankOneDiscrete.generator v ∈ (MonoidWithZeroHom.ofClass v).valueGroup
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_ofSubsingleton : ∀ {𝕜 : Type u} {ι : Type v} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] [inst_3 : SeminormedAddCommGroup G']
  [inst_4 : NormedSpace 𝕜 G'] [inst_5 : Fintype ι] [inst_6 : Subsingleton ι] (i : ι) (f : G →L[𝕜] G'),
  ‖(ContinuousMultilinearMap.ofSubsingleton 𝕜 G G' i) f‖ = ‖f‖
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.instContinuousFourier : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : AddCommGroup F]
  [inst_6 : Module ℂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul ℂ F], ContinuousFourier (TemperedDistribution E F) (TemperedDistribution E F)
-- Mathlib.Algebra.Group.Defs
AddCancelMonoid.toIsRightCancelAdd : ∀ {M : Type u} [self : AddCancelMonoid M], IsRightCancelAdd M
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.id_hComp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {a b : CategoryTheory.CatEnrichedOrdinary C}
  {f f' : a ⟶ b} (η : f ⟶ f'),
  CategoryTheory.CatEnrichedOrdinary.hComp (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id a)) η =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp η (CategoryTheory.eqToHom ⋯))
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_univ_fun_getElem : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (l : List ι) (f : ι → M), ∑ i, f l[↑i] = (List.map f l).sum
-- Init.Data.SInt.Lemmas
Int16.sub_le : ∀ {a b : Int16}, 0 ≤ b → b ≤ a → a - b ≤ a
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.coe_toTop_map_hom_apply_asIdeal : ∀ {x x_1 : CommRingCatᵒᵖ} (f : x ⟶ x_1) (p : PrimeSpectrum ↑(Opposite.unop x)),
  ↑((TopCat.Hom.hom (AlgebraicGeometry.Spec.toTop.map f)) p).asIdeal = ⇑(CommRingCat.Hom.hom f.unop) ⁻¹' ↑p.asIdeal
-- Mathlib.CategoryTheory.Localization.Bifunctor
/-- Given localization functor `L₁ : C₁ ⥤ D₁` and `L₂ : C₂ ⥤ D₂` with respect
to `W₁ : MorphismProperty C₁` and `W₂ : MorphismProperty C₂` respectively,
and a bifunctor `F : C₁ ⥤ C₂ ⥤ E` which inverts `W₁` and `W₂`, this is
the induced localized bifunctor `D₁ ⥤ D₂ ⥤ E`.  -/
CategoryTheory.Localization.lift₂ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        {E : Type u_5} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} E] →
                    (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)) →
                      {W₁ : CategoryTheory.MorphismProperty C₁} →
                        {W₂ : CategoryTheory.MorphismProperty C₂} →
                          W₁.IsInvertedBy₂ W₂ F →
                            (L₁ : CategoryTheory.Functor C₁ D₁) →
                              (L₂ : CategoryTheory.Functor C₂ D₂) →
                                [L₁.IsLocalization W₁] →
                                  [L₂.IsLocalization W₂] →
                                    [W₁.ContainsIdentities] →
                                      [W₂.ContainsIdentities] → CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.skipSuffix?_char_eq_skipSuffix?_beq : ∀ {c : Char} {s : String.Slice}, s.skipSuffix? c = s.skipSuffix? fun x => x == c
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.instIsIsoH₀Inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F)
  (i : F.I₀), CategoryTheory.IsIso (e.inv.h₀ i)
-- Mathlib.Data.Num.ZNum
ZNum.lt_to_int : ∀ {m n : ZNum}, ↑m < ↑n ↔ m < n
-- Std.Http.Data.Headers
/-- Filters and maps over header key-value pairs. Returns only the pairs for which the function returns `some`.
 -/
Std.Http.Headers.filterMap : Std.Http.Headers → (Std.Http.Header.Name → Std.Http.Header.Value → Option Std.Http.Header.Value) → Std.Http.Headers
-- Mathlib.RingTheory.RingHom.QuasiFinite
RingHom.QuasiFinite.holdsForLocalizationAway : RingHom.HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => RingHom.QuasiFinite
-- Init.Data.Option.Lemmas
Option.isNone_pmap : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {o : Option α} {h : ∀ (a : α), o = some a → p a},
  (Option.pmap f o h).isNone = o.isNone
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : TopologicalSpace α]
  [inst_3 : TopologicalSpace β] [inst_4 : SizeOf α] [inst_5 : SizeOf β] (toOrderHom : α →o β)
  (continuous_toFun : Continuous toOrderHom.toFun),
  sizeOf { toOrderHom := toOrderHom, continuous_toFun := continuous_toFun } =
    1 + sizeOf toOrderHom + sizeOf continuous_toFun
-- Mathlib.Data.Fintype.Pi
Fintype.piFinset_nonempty : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {γ : α → Type u_3} {s : (a : α) → Finset (γ a)},
  (Fintype.piFinset s).Nonempty ↔ ∀ (a : α), (s a).Nonempty
-- Mathlib.Topology.Connected.PathComponentOne
/-- The path component of the identity in a locally path connected topological group,
as an open normal subgroup. It is, in fact, clopen.  -/
OpenNormalSubgroup.pathComponentOne : (G : Type u_1) →
  [inst : TopologicalSpace G] →
    [inst_1 : Group G] → [IsTopologicalGroup G] → [LocallyPathConnectedSpace G] → OpenNormalSubgroup G
-- Init.Data.Rat.Lemmas
Rat.mul_nonneg : ∀ {a b : ℚ}, 0 ≤ a → 0 ≤ b → 0 ≤ a * b
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.get?ₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.OrientedOrd α] [inst_2 : Std.LawfulEqOrd α]
  (l : Std.DTreeMap.Internal.Impl α β) (k : α), l.get?ₘ k = Std.DTreeMap.Internal.Impl.applyCell k l fun c x => c.get?