mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- **Alias** of `MeasureTheory.setIntegral_sdiff`. -/
MeasureTheory.setIntegral_diff : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
  MeasurableSet t →
    MeasureTheory.IntegrableOn f s μ →
      t ⊆ s → ∫ (x : X) in s \ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ - ∫ (x : X) in t, f x ∂μ
-- Mathlib.RingTheory.Ideal.Operations
Ideal.isRadical_iff_pow_one_lt : ∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R} (k : ℕ), 1 < k → (I.IsRadical ↔ ∀ (r : R), r ^ k ∈ I → r ∈ I)
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- The cofan consisting of the inclusions given by `ιMapBifunctorBifunctor₂₃MapObj`.  -/
CategoryTheory.GradedObject.cofan₃MapBifunctorBifunctor₂₃MapObj : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {C₂₃ : Type u_6} →
          [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} C₃] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] →
                    (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) →
                      (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) →
                        {I₁ : Type u_7} →
                          {I₂ : Type u_8} →
                            {I₃ : Type u_9} →
                              {J : Type u_10} →
                                {r : I₁ × I₂ × I₃ → J} →
                                  (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) →
                                    (X₁ : CategoryTheory.GradedObject I₁ C₁) →
                                      (X₂ : CategoryTheory.GradedObject I₂ C₂) →
                                        (X₃ : CategoryTheory.GradedObject I₃ C₃) →
                                          [inst_5 :
                                              (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj
                                                    X₃).HasMap
                                                ρ₂₃.p] →
                                            [(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
                                                      (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂
                                                        X₃)).HasMap
                                                  ρ₂₃.q] →
                                              (j : J) →
                                                ((((CategoryTheory.GradedObject.mapTrifunctor
                                                                  (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj
                                                              X₁).obj
                                                          X₂).obj
                                                      X₃).CofanMapObjFun
                                                  r j
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.instSymm : ∀ {S : Type u_3} [inst : Add S], Std.Symm AddCommute
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.finiteCoproduct.ι_jointly_surjective : ∀ {P : TopCat → Prop} {α : Type w} [inst : Finite α] (X : α → CompHausLike P)
  [inst_1 : CompHausLike.HasExplicitFiniteCoproduct X] (R : ↑(CompHausLike.finiteCoproduct X).toTop),
  ∃ a r, R = (CategoryTheory.ConcreteCategory.hom (CompHausLike.finiteCoproduct.ι X a)) r
-- Mathlib.Data.Finset.Sum
Finset.toRight_cons_inr : ∀ {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {b : β} (hb : Sum.inr b ∉ u),
  (Finset.cons (Sum.inr b) u hb).toRight = Finset.cons b u.toRight ⋯
-- Init.Data.Array.MapIdx
List.mapIdxM.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : ℕ → α → m β) (as : List α),
  List.mapIdxM f as = List.mapIdxM.go f as #[]
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.XIsoOfEq_inv_comp_d : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₂ p₁ : ι}
  (h : p₂ = p₁) (p₃ : ι), CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).inv (K.d p₂ p₃) = K.d p₁ p₃
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  (t₁ ∪ t₂).isEmpty = (t₁.isEmpty && t₂.isEmpty)
-- Mathlib.RingTheory.WittVector.Basic
/-- Auxiliary tactic for showing that `mapFun` respects the ring operations.  -/
WittVector.mapFun.tacticMap_fun_tac : Lean.ParserDescr
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceCompletionParams : Lean.Lsp.FileSource Lean.Lsp.CompletionParams
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isCircuit_mapLe : ∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u : V} {p : G.Walk u u},
  (SimpleGraph.Walk.mapLe h p).IsCircuit ↔ p.IsCircuit
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- Construct an isomorphism of bimodules by giving an isomorphism between the underlying objects
and checking compatibility with left and right actions only in the forward direction.
 -/
Bimod.isoOfIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X Y : CategoryTheory.Mon C} →
        {P Q : Bimod X Y} →
          (f : P.X ≅ Q.X) →
            CategoryTheory.CategoryStruct.comp P.actLeft f.hom =
                CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X f.hom)
                  Q.actLeft →
              CategoryTheory.CategoryStruct.comp P.actRight f.hom =
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Y.X)
                    Q.actRight →
                (P ≅ Q)
-- Init.Data.List.Basic
List.lengthTRAux.eq_def : ∀ {α : Type u_1} (x : List α) (x_1 : ℕ),
  x.lengthTRAux x_1 =
    match x, x_1 with
    | [], n => n
    | head :: as, n => as.lengthTRAux n.succ
-- Mathlib.Topology.Algebra.OpenSubgroup
IsTopologicalAddGroup.addNegClosureNhd.isOpen : ∀ {G : Type u_1} [inst : TopologicalSpace G] {T W : Set G} [inst_1 : AddGroup G],
  IsTopologicalAddGroup.addNegClosureNhd T W → IsOpen T
-- Mathlib.LinearAlgebra.Matrix.Basis
/-- A generalization of `Basis.toMatrix_self`, in the opposite direction.  -/
Module.Basis.toMatrix_mul_toMatrix : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (b : Module.Basis ι R M) (b' : Module.Basis ι' R M) {ι'' : Type u_10} [inst_3 : Fintype ι']
  (b'' : ι'' → M), b.toMatrix ⇑b' * b'.toMatrix b'' = b.toMatrix b''
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.id_toFunctor : ∀ {C : CategoryTheory.Cat}, (CategoryTheory.CategoryStruct.id C).toFunctor = CategoryTheory.Functor.id ↑C
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α}, (m.erase k).contains a = (!k == a && m.contains a)
-- Mathlib.Algebra.SkewMonoidAlgebra.Support
SkewMonoidAlgebra.support_sum : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {k' : Type u_3} {G' : Type u_4} [inst_1 : DecidableEq G']
  [inst_2 : AddCommMonoid k'] {f : SkewMonoidAlgebra k G} {g : G → k → SkewMonoidAlgebra k' G'},
  (f.sum g).support ⊆ f.support.biUnion fun a => (g a (f.coeff a)).support
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.LocalizationAwayPreserves.and : ∀ {P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => Q) →
      RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] f => P f ∧ Q f
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.zeta_prod_zeta : ∀ {𝕜 : Type u_2} {α : Type u_5} {β : Type u_6} [inst : Ring 𝕜] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : DecidableLE α] [inst_4 : DecidableLE β],
  (IncidenceAlgebra.zeta 𝕜).prod (IncidenceAlgebra.zeta 𝕜) = IncidenceAlgebra.zeta 𝕜
-- Init.Data.Int.Compare
Int.compare_ne_lt : ∀ {a b : ℤ}, compare a b ≠ Ordering.lt ↔ b ≤ a
-- Init.Data.UInt.Lemmas
UInt32.toNat_add : ∀ (a b : UInt32), (a + b).toNat = (a.toNat + b.toNat) % 2 ^ 32
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.op_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.HomologyData), h.op.iso = h.iso.op
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.liminf_neg : ∀ {α : Type u_3} {f : Filter α} {v : α → EReal}, Filter.liminf (-v) f = -Filter.limsup v f
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.edgeSet_map : ∀ {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : G.Subgraph),
  (SimpleGraph.Subgraph.map f H).edgeSet = Sym2.map ⇑f '' H.edgeSet
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.hasSumLocallyUniformly_weierstrassPExcept : ∀ (L : PeriodPair) (l₀ : ℂ),
  HasSumLocallyUniformly (fun l z => if ↑l = l₀ then 0 else 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2) (L.weierstrassPExcept l₀)
-- Mathlib.Algebra.Ring.Defs
/-- Multiplication is commutative in a commutative multiplicative magma.  -/
CommRing.mul_comm : ∀ {α : Type u} [self : CommRing α] (a b : α), a * b = b * a
-- Lean.Linter.Deprecated
Lean.Linter.setDeprecated : {m : Type → Type} →
  [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Name → Lean.Linter.DeprecationEntry → m Unit
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : IsScalarTower ℝ A A] [inst_5 : SMulCommClass ℝ A A]
  [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {a : A},
  IsSelfAdjoint a →
    QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal →
      ∃ x, IsSelfAdjoint x ∧ QuasispectrumRestricts x ⇑ContinuousMap.realToNNReal ∧ x * x = a
-- Mathlib.Data.Rel.Cover
SetRel.IsCover.rfl : ∀ {X : Type u_1} {U : SetRel X X} [U.IsRefl] {s : Set X}, U.IsCover s s
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
AEMeasurable.ereal_toENNReal : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → EReal} {μ : MeasureTheory.Measure α},
  AEMeasurable f μ → AEMeasurable (fun x => (f x).toENNReal) μ
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Triplet.mk : {n : ℤ} → (p q : ℤ) → p + n = q → CochainComplex.HomComplex.Triplet n
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.one_eq_refl : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  1 = LinearEquiv.refl R M
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instDistribSMul : {M : Type u_1} →
  {A : Type u_2} →
    [inst : TopologicalSpace A] →
      [inst_1 : AddZeroClass A] →
        [inst_2 : DistribSMul M A] →
          [inst_3 : ContinuousAdd A] → [ContinuousConstSMul M A] → DistribSMul M (SeparationQuotient A)
-- Init.WFExtrinsicFix
_private.Init.WFExtrinsicFix.0.WellFounded.opaqueFix.congr_simp : ∀ {α : Sort u_1} {C : α → Sort u_2} [inst : ∀ (a : α), Nonempty (C a)] (R : α → α → Prop)
  (F F_1 : (a : α) → ((a' : α) → R a' a → C a') → C a),
  F = F_1 → ∀ (a : α), WellFounded.opaqueFix✝ R F a = WellFounded.opaqueFix✝ R F_1 a
-- Mathlib.RingTheory.PrincipalIdealDomainOfPrime
/-- If all prime ideals in a commutative ring that are not `(0)` are principal,
so are all other ideals.  -/
IsPrincipalIdealRing.of_prime_ne_bot : ∀ {R : Type u_1} [inst : CommSemiring R],
  (∀ (P : Ideal R), P.IsPrime → P ≠ ⊥ → Submodule.IsPrincipal P) → IsPrincipalIdealRing R
-- Mathlib.Topology.Closure
frontier_eq_closure_inter_closure : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, frontier s = closure s ∩ closure sᶜ
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Rewrite in terms of the `factorThruImage` interface.  -/
CategoryTheory.Limits.as_factorThruImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f],
  (CategoryTheory.Limits.Image.monoFactorisation f).e = CategoryTheory.Limits.factorThruImage f
-- Mathlib.Algebra.Quandle
/-- Shelf Homomorphism  -/
Quandles.«term_→◃_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.GroupWithZero.Units.Basic
/-- A variant of `mul_inv_eq_iff_eq_mul₀` that moves the nonzero hypothesis to another variable.  -/
eq_mul_of_mul_inv_eq₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c : G₀}, b ≠ 0 → a * c⁻¹ = b → a = b * c
-- Mathlib.Data.Sym.Basic
/-- `erase s a h` is the sym that subtracts 1 from the
multiplicity of `a` if `a` is present in the sym.  -/
Sym.erase : {α : Type u_1} → {n : ℕ} → [DecidableEq α] → (s : Sym α (n + 1)) → (a : α) → a ∈ s → Sym α n
-- Mathlib.Analysis.Convex.Slope
StrictConvexOn.secant_strict_mono_aux3 : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  StrictConvexOn 𝕜 s f → ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f x) / (z - x) < (f z - f y) / (z - y)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycleOn.eq_1 : ∀ {α : Type u_2} (f : Equiv.Perm α) (s : Set α),
  f.IsCycleOn s = (Set.BijOn (⇑f) s s ∧ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → f.SameCycle x y)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_inverse_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  (c : CategoryTheory.Limits.BinaryCofan (CategoryTheory.Under.mk f) (CategoryTheory.Under.mk g)),
  CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.inverse.obj c =
    CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.Under.Hom.right c.inl) (CategoryTheory.Under.Hom.right c.inr)
      ⋯
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.objMap_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  {f g h : CategoryTheory.Arrow C} (φ : f ⟶ g) (ψ : g ⟶ h),
  CategoryTheory.SmallObject.objMap I κ (CategoryTheory.CategoryStruct.comp φ ψ) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.objMap I κ φ)
      (CategoryTheory.SmallObject.objMap I κ ψ)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
UniqueFactorizationMonoid.toIsWellFounded : ∀ {α : Type u_2} {inst : CommMonoidWithZero α} [self : UniqueFactorizationMonoid α], IsWellFounded α DvdNotUnit
-- Mathlib.Algebra.Notation.Support
Function.support_update_zero : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] [inst_1 : DecidableEq ι] (f : ι → M) (x : ι),
  Function.support (Function.update f x 0) = Function.support f \ {x}
-- Mathlib.Analysis.InnerProductSpace.PiL2
_private.Mathlib.Analysis.InnerProductSpace.PiL2.0.«term⟪_,_⟫ₑ» : Lean.ParserDescr
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_alter_eq_self_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, k ∈ t → (f t[k]?).isSome = true → (t.alter k f).size = t.size
-- Mathlib.MeasureTheory.Group.FoelnerFilter
/-- If there exists a non-trivial Følner filter with respect to some additive group
`G` acting on a measure space `X`, then there exists a `G`-invariant finitely additive
probability measure on `X`.  -/
IsAddFoelner.amenable : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : AddGroup G]
  [inst_2 : AddAction G X] {ι : Type u_3} {l : Filter ι} {F : ι → Set X} [MeasureTheory.VAddInvariantMeasure G X μ]
  [l.NeBot],
  IsAddFoelner G μ l F →
    ∃ m,
      m Set.univ = 1 ∧
        (∀ (s t : Set X), MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t) ∧
          ∀ (g : G) (s : Set X), m (g +ᵥ s) = m s
-- Aesop.Tree.RunMetaM
Aesop.instMonadLiftTSTRealWorld_aesop : {m : Type → Type u_1} → [MonadLiftT Lean.MetaM m] → MonadLiftT (ST IO.RealWorld) m
-- Init.Grind.Module.NatModuleNorm
_private.Init.Grind.Module.NatModuleNorm.0.Lean.Grind.Linarith.Poly.denote.match_1.eq_1 : ∀ (motive : Lean.Grind.Linarith.Poly → Sort u_1) (h_1 : Unit → motive Lean.Grind.Linarith.Poly.nil)
  (h_2 :
    (k : ℤ) →
      (v : Lean.Grind.Linarith.Var) → (p : Lean.Grind.Linarith.Poly) → motive (Lean.Grind.Linarith.Poly.add k v p)),
  (match Lean.Grind.Linarith.Poly.nil with
    | Lean.Grind.Linarith.Poly.nil => h_1 ()
    | Lean.Grind.Linarith.Poly.add k v p => h_2 k v p) =
    h_1 ()
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
/-- The category `Etale X` is the category of schemes étale over `X`.  -/
AlgebraicGeometry.Scheme.Etale : AlgebraicGeometry.Scheme → Type (u + 1)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.cmp.eq_1 : ONote.zero.cmp ONote.zero = Ordering.eq
-- Mathlib.Data.Multiset.FinsetOps
/-- `ndinsert a s` is the lift of the list `insert` operation. This operation
does not respect multiplicities, unlike `cons`, but it is suitable as
an insert operation on `Finset`.  -/
Multiset.ndinsert : {α : Type u_1} → [DecidableEq α] → α → Multiset α → Multiset α
-- Mathlib.Topology.Algebra.GroupCompletion
UniformSpace.Completion.coe_add : ∀ {α : Type u_3} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] (a b : α), ↑(a + b) = ↑a + ↑b
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.subtractionCommMonoid.eq_1 : ∀ {α : Type u_2} [inst : SubtractionCommMonoid α],
  Set.subtractionCommMonoid = { toSubtractionMonoid := Set.subtractionMonoid, add_comm := ⋯ }
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.precompL.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_4} (Eₗ : Type u_5) {Fₗ : Type u_7} {Gₗ : Type u_9} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup Eₗ] [inst_2 : SeminormedAddCommGroup Fₗ] [inst_3 : SeminormedAddCommGroup Gₗ]
  [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 E] [inst_6 : NormedSpace 𝕜 Eₗ]
  [inst_7 : NormedSpace 𝕜 Fₗ] [inst_8 : NormedSpace 𝕜 Gₗ] (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ),
  ContinuousLinearMap.precompL Eₗ L = (ContinuousLinearMap.precompR Eₗ L.flip).flip
-- Mathlib.Algebra.Colimit.Module
/-- A component that corresponds to zero in the direct limit is already zero in some
bigger module in the directed system.  -/
Module.DirectLimit.of.zero_exact : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
  [inst_4 : DecidableEq ι] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] {i : ι} {x : G i},
  (Module.DirectLimit.of R ι G f i) x = 0 → ∃ j, ∃ (hij : i ≤ j), (f i j hij) x = 0
-- Lean.ExtraModUses
Lean.ExtraModUse.mk : Lean.Name → Bool → Bool → Lean.ExtraModUse
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.commSq : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsHomLift f φ],
  CategoryTheory.CommSq (p.map φ) (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯) f
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_inter_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₂ → (t₁ ∩ t₂).get? k = t₁.get? k
-- Mathlib.SetTheory.ZFC.Ordinal
Ordinal.mem_toPSet_iff : ∀ {o : Ordinal.{u_1}} {x : PSet.{u_1}}, x ∈ o.toPSet ↔ ∃ a < o, x.Equiv a.toPSet
-- Mathlib.Data.Finsupp.Defs
Finsupp.mapRange_mapRange : ∀ {α : Type u_1} {M : Type u_4} {N : Type u_5} {O : Type u_6} [inst : Zero M] [inst_1 : Zero N] [inst_2 : Zero O]
  (e₁ : N → O) (e₂ : M → N) (he₁ : e₁ 0 = 0) (he₂ : e₂ 0 = 0) (f : α →₀ M),
  Finsupp.mapRange e₁ he₁ (Finsupp.mapRange e₂ he₂ f) = Finsupp.mapRange (e₁ ∘ e₂) ⋯ f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_eq_pi_iff : ∀ {θ : Real.Angle}, θ.toReal = Real.pi ↔ θ = ↑Real.pi
-- Mathlib.Topology.VectorBundle.Hom
/-- Consider a `C^n` map `v : M → E₁` to a vector bundle, over a basemap `b : M → B`, and
linear maps `ϕ m : E₁ (b m) → E₂ (b m)` depending smoothly on `m`.
One can apply `ϕ m` to `v m`, and the resulting map is `C^n`.  -/
ContinuousOn.clm_bundle_apply : ∀ {𝕜 : Type u_8} {B : Type u_9} {F₁ : Type u_10} {F₂ : Type u_11} {M : Type u_13} [inst : NontriviallyNormedField 𝕜]
  {E₁ : B → Type u_14} [inst_1 : (x : B) → AddCommGroup (E₁ x)] [inst_2 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁] [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_6 : (x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_15} [inst_7 : (x : B) → AddCommGroup (E₂ x)]
  [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_12 : (x : B) → TopologicalSpace (E₂ x)]
  [inst_13 : TopologicalSpace B] [inst_14 : TopologicalSpace M] [inst_15 : FiberBundle F₁ E₁]
  [inst_16 : VectorBundle 𝕜 F₁ E₁] [inst_17 : FiberBundle F₂ E₂] [inst_18 : VectorBundle 𝕜 F₂ E₂] {b : M → B}
  {v : (x : M) → E₁ (b x)} {s : Set M} [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)]
  [inst_20 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] {ϕ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x)},
  ContinuousOn (fun m => ⟨b m, ϕ m⟩) s →
    ContinuousOn (fun m => ⟨b m, v m⟩) s → ContinuousOn (fun m => ⟨b m, (ϕ m) (v m)⟩) s
-- Init.Data.Int.DivMod.Lemmas
Int.tmod_nonneg : ∀ {a : ℤ} (b : ℤ), 0 ≤ a → 0 ≤ a.tmod b
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.mem_blockTriangularSubalgebra : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {A : Type u_8} {b : m → α} [inst : LinearOrder α] [inst_1 : CommSemiring R]
  [inst_2 : Semiring A] [inst_3 : Algebra R A] [inst_4 : DecidableEq m] [inst_5 : Fintype m] {M : Matrix m m A},
  M ∈ Matrix.blockTriangularSubalgebra R A b ↔ M.BlockTriangular b
-- Mathlib.CategoryTheory.ConnectedComponents
/-- Given an index for a connected component, this is the property of the
objects which belong to this component.  -/
CategoryTheory.ConnectedComponents.objectProperty : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] → CategoryTheory.ConnectedComponents J → CategoryTheory.ObjectProperty J
-- Std.Http.Protocol.H1.Writer
/-- The state of the `Writer` state machine.
 -/
Std.Http.Protocol.H1.Writer.State : Type
-- Mathlib.Data.Nat.GCD.Basic
Nat.gcd_mul_gcd_eq_iff_dvd_mul_of_coprime : ∀ {x n m : ℕ}, n.Coprime m → (x.gcd n * x.gcd m = x ↔ x ∣ n * m)
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_tsum : ∀ {Ω : Type u_1} {mΩ₀ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} (mΩ : MeasurableSpace Ω)
  [Countable ι] {X : ι → Ω → ENNReal},
  (∀ (i : ι), AEMeasurable (X i) P) → P⁻[∑' (i : ι), X i | mΩ] =ᵐ[P] ∑' (i : ι), P⁻[X i | mΩ]
-- Mathlib.Algebra.Lie.Weights.RootSystem
/-- The length of the `α`-chain through `β`. See `chainBotCoeff_add_chainTopCoeff`.  -/
LieAlgebra.IsKilling.chainLength : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [CharZero K] →
        [inst_2 : LieRing L] →
          [inst_3 : LieAlgebra K L] →
            [LieAlgebra.IsKilling K L] →
              [FiniteDimensional K L] →
                {H : LieSubalgebra K L} →
                  [inst_6 : H.IsCartanSubalgebra] →
                    [LieModule.IsTriangularizable K (↥H) L] → LieModule.Weight K (↥H) L → LieModule.Weight K (↥H) L → ℕ