mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.isClosed_singleton_iff_isClosedImmersion : ∀ {X : AlgebraicGeometry.Scheme} {x : ↥X}, IsClosed {x} ↔ AlgebraicGeometry.IsClosedImmersion (X.fromSpecResidueField x)
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
MeasureTheory.IntegrableOn.continuousOn_Ici_primitive_Ioi : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {f : ℝ → E}
  [MeasureTheory.NullSingletonClass μ] {a₀ : ℝ},
  MeasureTheory.IntegrableOn f (Set.Ioi a₀) μ → ContinuousOn (fun b => ∫ (x : ℝ) in Set.Ioi b, f x ∂μ) (Set.Ici a₀)
-- Mathlib.Data.Set.Subsingleton
Set.singleton_ssubset_univ : ∀ {α : Type u} [Nontrivial α] (a : α), {a} ⊂ Set.univ
-- Mathlib.CategoryTheory.Triangulated.Orthogonal
CategoryTheory.ObjectProperty.isLocal_trW : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.Preadditive C] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C] [P.IsTriangulated], P.trW.isLocal = P.rightOrthogonal
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.cons₁ : Turing.ToPartrec.Code → List ℕ → Turing.ToPartrec.Cont → Turing.ToPartrec.Cont
-- Mathlib.Tactic.GCongr.Core
/-- Run a `GCongrM` computation in `MetaM`.  -/
Mathlib.Tactic.GCongr.GCongrM.run : {α : Type} →
  Mathlib.Tactic.GCongr.GCongrM α →
    optParam (List (Lean.TSyntax `rintroPat)) [] →
      optParam (Lean.MVarId → Lean.MetaM Bool) Mathlib.Tactic.GCongr.gcongrForwardDischarger →
        optParam (Lean.MVarId → Lean.MetaM Unit) Mathlib.Tactic.GCongr.gcongrDischarger →
          Lean.MetaM (α × Array Lean.MVarId)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_unitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J Cᵒᵖ},
  CategoryTheory.Limits.coneLeftOpOfCoconeEquiv.unitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)ᵒᵖ)
-- Mathlib.Topology.Category.Profinite.Extend
/-- A continuous map from a profinite set to a finite set factors through one of the components of
the profinite set when written as a cofiltered limit of finite sets.
 -/
Profinite.exists_hom : ∀ {I : Type u} [inst : CategoryTheory.SmallCategory I] [CategoryTheory.IsCofiltered I]
  {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite))
  (hc : CategoryTheory.Limits.IsLimit c) {X : FintypeCat} (f : c.pt ⟶ FintypeCat.toProfinite.obj X),
  ∃ i g, f = CategoryTheory.CategoryStruct.comp (c.π.app i) (FintypeCat.toProfinite.map g)
-- Init.Data.Array.Lemmas
Array.back?_empty : ∀ {α : Type u_1}, #[].back? = none
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.map.of : ∀ {α : Type u} {β : Type v} {f : α → β} {x : α}, (FreeGroup.map f) (FreeGroup.of x) = FreeGroup.of (f x)
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.map.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {N₁ : Type u_6} {N₂ : Type u_7} {N : Type u_8}
  [inst_7 : AddCommMonoid N₁] [inst_8 : AddCommMonoid N₂] [inst_9 : AddCommMonoid N] [inst_10 : Module R N₁]
  [inst_11 : Module R N₂] [inst_12 : Module R N] {g : N₁ →ₗ[R] N₂ →ₗ[R] N} (hf : IsTensorProduct f)
  (hg : IsTensorProduct g) (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂),
  hf.map hg i₁ i₂ = ↑hg.equiv ∘ₗ TensorProduct.map i₁ i₂ ∘ₗ ↑hf.equiv.symm
-- Mathlib.Order.Hom.Basic
OrderIso.funUnique_symm_apply : ∀ {α : Type u_6} {β : Type u_7} [inst : Unique α] [inst_1 : Preorder β],
  ⇑(OrderIso.funUnique α β).symm = Function.const α
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_ric_eq_zero_iff : ∀ {n i : ℕ}, (*...=n).toArray[i]! = 0 ↔ n < i ∨ i = 0
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonLeanIleanInfoParams : Lean.FromJson Lean.Lsp.LeanIleanInfoParams
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospanExt_inv_app_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z')
  {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'}
  (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom)
  (wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom),
  (CategoryTheory.Limits.cospanExt iX iY iZ wf wg).inv.app CategoryTheory.Limits.WalkingCospan.one = iZ.inv
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroupClass.inclusion_self : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_4} {H : S} [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G]
  [inst_3 : Preorder S] [inst_4 : IsConcreteLE S G] (x : ↥H), (AddSubgroupClass.inclusion ⋯) x = x
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
ergodic_add_left_iff_denseRange_zsmul : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [SecondCountableTopology G] [BorelSpace G] {g : G} (μ : MeasureTheory.Measure G)
  [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [μ.IsAddLeftInvariant] [NeZero μ],
  Ergodic (fun x => g + x) μ ↔ DenseRange fun x => x • g
-- Mathlib.Algebra.Torsor.Basic
Set.one_mem_sdiv_iff : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] {s t : Set P}, 1 ∈ s /ₛ t ↔ ¬Disjoint s t
-- Mathlib.Algebra.Category.Grp.Limits
AddCommGrpCat.forget_createsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddCommGrpCat) → CategoryTheory.CreatesLimit F (CategoryTheory.forget AddCommGrpCat)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.fstPiMapOfIsLimit_proj_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left)
  {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (i : J.R) {Z : C} (h : I.right i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (I.fstPiMapOfIsLimit c hd) (CategoryTheory.CategoryStruct.comp (d.proj i) h) =
    CategoryTheory.CategoryStruct.comp (c.proj (J.fst i)) (CategoryTheory.CategoryStruct.comp (I.fst i) h)
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.apply_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F] [inst_8 : ∀ (i : ι), ContinuousSMul 𝕜 (E i)] [inst_9 : ContinuousConstSMul 𝕜 F]
  {m : (i : ι) → E i} {c : ContinuousMultilinearMap 𝕜 E F}, (ContinuousMultilinearMap.apply 𝕜 E F m) c = c m
-- Mathlib.Probability.Kernel.WithDensity
ProbabilityTheory.Kernel.withDensity_one : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  [inst : ProbabilityTheory.IsSFiniteKernel κ], κ.withDensity 1 = κ
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.fundamentalFrontier_smul : ∀ (G : Type u_1) {H : Type u_2} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α) [inst_2 : Group H]
  [inst_3 : MulAction H α] [SMulCommClass H G α] (g : H),
  MeasureTheory.fundamentalFrontier G (g • s) = g • MeasureTheory.fundamentalFrontier G s
-- Lean.CoreM
Lean.Core.Cache.mk.sizeOf_spec : ∀ (instLevelType instLevelValue : Lean.Core.InstantiateLevelCache),
  sizeOf { instLevelType := instLevelType, instLevelValue := instLevelValue } =
    1 + sizeOf instLevelType + sizeOf instLevelValue
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.trans : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat}
  (x y z : MonCat.Colimits.Prequotient F),
  MonCat.Colimits.Relation F x y → MonCat.Colimits.Relation F y z → MonCat.Colimits.Relation F x z
-- Mathlib.Data.Set.Card
/-- A surjective function `f : α → β` decreases cardinality by at most one if and only if
there is at most a collision between a unique pair of elements.  -/
Function.Surjective.card_le_card_add_one_iff : ∀ {α : Type u_1} {β : Type u_2} [Finite α] {f : α → β},
  Function.Surjective f →
    (Nat.card α ≤ Nat.card β + 1 ↔ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d})
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaMonObj.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (M : C) [inst_2 : CategoryTheory.MonObj M],
  CategoryTheory.yonedaMonObj M =
    { obj := fun X => MonCat.of (Opposite.unop X ⟶ M),
      map := fun {X Y₂} φ =>
        MonCat.ofHom { toFun := fun x => CategoryTheory.CategoryStruct.comp φ.unop x, map_one' := ⋯, map_mul' := ⋯ },
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Topology.LocallyFinite
LocallyFinite.comp_injective : ∀ {ι : Type u_1} {ι' : Type u_2} {X : Type u_4} [inst : TopologicalSpace X] {f : ι → Set X} {g : ι' → ι},
  LocallyFinite f → Function.Injective g → LocallyFinite (f ∘ g)
-- Mathlib.Topology.Order.IntermediateValue
intermediate_value_Iio : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a : α} {f : α → δ},
  ContinuousOn f (Set.Iic a) → Filter.Tendsto f Filter.atBot Filter.atBot → Set.Iio (f a) ⊆ f '' Set.Iio a
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.apply_prod_le_sum_map : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : AddCommMonoid β] [inst_2 : Preorder β] [AddLeftMono β]
  (m : Multiset α) (f : α → β), f 1 ≤ 0 → (∀ (a b : α), f (a * b) ≤ f a + f b) → f m.prod ≤ (Multiset.map f m).sum
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.GeneralTheorems.mk.sizeOf_spec : ∀ (theorems : Lean.Meta.RefinedDiscrTree Mathlib.Meta.FunProp.GeneralTheorem),
  sizeOf { theorems := theorems } = 1 + sizeOf theorems
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_insertList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited α] {l toInsert : List ((a : α) × β a)}
  {k : α},
  (List.map Sigma.fst toInsert).contains k = false →
    Std.Internal.List.getKey! k (Std.Internal.List.insertList l toInsert) = Std.Internal.List.getKey! k l
-- Mathlib.Data.List.ProdSigma
List.nil_sigma : ∀ {α : Type u_1} {σ : α → Type u_3} (l : (a : α) → List (σ a)), [].sigma l = []
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.leftAdjointUniq_refl : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G), (adj1.leftAdjointUniq adj1).hom = CategoryTheory.CategoryStruct.id F
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.getEntry!_eq_getEntry!ₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited ((a : α) × β a)]
  (m : Std.DHashMap.Internal.Raw₀ α β) (a : α), m.getEntry! a = m.getEntry!ₘ a
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.imageMonoIsoSource.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f],
  CategoryTheory.Limits.imageMonoIsoSource f =
    (CategoryTheory.Limits.Image.isImage f).isoExt (CategoryTheory.Limits.IsImage.self f)
-- Mathlib.Analysis.Complex.CanonicalDecomposition
_private.Mathlib.Analysis.Complex.CanonicalDecomposition.0.Complex.mulSupport_pow_subset_support : ∀ {α : Type u_2} {β : Type u_3} [inst : DivInvMonoid α] (f : β → α) (g : β → ℤ),
  (Function.mulSupport fun x => f x ^ g x) ⊆ Function.support g
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπObjToKaroubi : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive A] [inst_4 : ι.Additive] (X : A),
  CategoryTheory.Epi
    ((CategoryTheory.Abelian.LeftResolution.karoubi.π Λ).app ((CategoryTheory.Idempotents.toKaroubi A).obj X))
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.mul'.eq_def : ∀ (p : Int.Internal.Linear.Poly) (k : ℤ),
  p.mul' k =
    match p with
    | Int.Internal.Linear.Poly.num k' => Int.Internal.Linear.Poly.num (k * k')
    | Int.Internal.Linear.Poly.add k' v p => Int.Internal.Linear.Poly.add (k * k') v (p.mul' k)
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ResolveSimpIdResult.none : Lean.Elab.Tactic.ResolveSimpIdResult
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
/-- A 1-cochain of a presheaf of groups `G : Cᵒᵖ ⥤ GrpCat` on a family `U : I → C` of objects
consists of the data of an element in `G.obj (Opposite.op T)` whenever we have elements
`i` and `j` in `I` and maps `a : T ⟶ U i` and `b : T ⟶ U j`, and it must satisfy a compatibility
with respect to precomposition. (When the binary product of `U i` and `U j` exists, this
data for all `T`, `a` and `b` corresponds to the data of a section of `G` on this product.)  -/
CategoryTheory.PresheafOfGroups.OneCochain : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor Cᵒᵖ GrpCat → {I : Type w'} → (I → C) → Type (max (max (max u v) w) w')
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- If `G : Cone F ⥤ Cone F'` reflects terminal objects, it reflects limit cones.  -/
CategoryTheory.Limits.IsLimit.ofReflectsConeTerminal : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {D : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} D] →
                {F : CategoryTheory.Functor J C} →
                  {F' : CategoryTheory.Functor K D} →
                    (G : CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone F')) →
                      [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Functor.empty (CategoryTheory.Limits.Cone F))
                            G] →
                        {c : CategoryTheory.Limits.Cone F} →
                          CategoryTheory.Limits.IsLimit (G.obj c) → CategoryTheory.Limits.IsLimit c
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.exists_eq_singleton_append_of_ne_startPos : ∀ {t₁ t₂ : String} {s : String.Slice} {p : s.Pos} (hp : p ≠ s.startPos),
  (p.prev hp).Splits t₁ t₂ → ∃ t₂', t₂ = String.singleton ((p.prev hp).get ⋯) ++ t₂'
-- Mathlib.Data.Finset.NAry
Finset.biUnion_image_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β},
  (t.biUnion fun b => Finset.image (fun a => f a b) s) = Finset.image₂ f s t
-- Mathlib.Data.Nat.ModEq
Nat.modEq_sub_modulus_iff : ∀ {n a b : ℕ}, n ≤ b → (a ≡ b - n [MOD n] ↔ a ≡ b [MOD n])
-- Mathlib.Combinatorics.Matroid.Closure
/-- **Alias** of `Matroid.IsBasis.isBasis_insert_sdiff_of_mem_closure`. -/
Matroid.IsBasis.isBasis_insert_diff_of_mem_closure : ∀ {α : Type u_2} {M : Matroid α} {X : Set α} {e f : α} {B : Set α},
  M.IsBasis B X → e ∈ M.closure (insert f B \ {e}) → e ∈ insert f B → f ∈ X → M.IsBasis (insert f B \ {e}) X
-- Mathlib.Data.Num.Lemmas
Num.cast_toZNum : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : Add α] [inst_3 : Neg α] (n : Num), ↑n.toZNum = ↑n
-- Mathlib.Topology.Semicontinuity.Defs
semicontinuous_iff_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop},
  Semicontinuous r ↔ ∀ (x : α) (y : β), (∃ᶠ (x' : α) in nhds x, ¬r x' y) → ¬r x y
-- Init.Data.Range.Polymorphic.Iterators
Std.Rco.Internal.isPlausibleIndirectOutput_iter_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : LT α] [inst_3 : DecidableLT α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLE α]
  {r : Std.Rco α} {a : α}, (Std.Rco.Internal.iter r).IsPlausibleIndirectOutput a ↔ a ∈ r
-- Mathlib.Analysis.Complex.UnitDisc.Basic
/-- Coercion to `ℂ`.  -/
Complex.UnitClosedDisc.coe : Complex.UnitClosedDisc → ℂ
-- Mathlib.GroupTheory.Exponent
/-- The exponent of finite product of monoids is the `Finset.lcm` of the exponents of the
constituent monoids.  -/
Monoid.exponent_pi : ∀ {ι : Type u_1} [inst : Fintype ι] {M : ι → Type u_2} [inst_1 : (i : ι) → Monoid (M i)],
  Monoid.exponent ((i : ι) → M i) = Finset.univ.lcm fun x => Monoid.exponent (M x)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {h : (Std.DHashMap.Const.get? m a).isSome = true},
  (Std.DHashMap.Const.get? m a).get h = Std.DHashMap.Const.get m a ⋯
-- Mathlib.Data.Nat.Factorization.Divisors
Nat.properDivisors_eq_map_attach_Iio_factorization_prod_pow : ∀ {n : ℕ},
  n.properDivisors =
    Finset.map { toFun := fun x => (↑x).prod fun x1 x2 => x1 ^ x2, inj' := ⋯ } (Finset.Iio n.factorization).attach
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.fg_subalgebra : ∀ (R : Type u_1) [inst : CommRing R] {A : Type u} {B : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra A B] (D : Algebra.Smooth.DescentAux✝ A B)
  [Finite (Algebra.Smooth.DescentAux.vars✝ D)] [Finite (Algebra.Smooth.DescentAux.rels✝ D)],
  (Algebra.Smooth.DescentAux.subalgebra✝ R D).FG
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
RootPairing.coxeterWeightIn.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P P_1 : RootPairing ι R M N) (e_P : P = P_1)
  (S : Type u_7) [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : P.IsValuedIn S] (i i_1 : ι),
  i = i_1 → ∀ (j j_1 : ι), j = j_1 → P.coxeterWeightIn S i j = P_1.coxeterWeightIn S i_1 j_1
-- Mathlib.Analysis.Normed.Group.Quotient
NormedAddGroupHom.IsQuotient.norm_le : ∀ {M : Type u_1} {N : Type u_2} [inst : SeminormedAddCommGroup M] [inst_1 : SeminormedAddCommGroup N]
  {f : NormedAddGroupHom M N}, f.IsQuotient → ∀ (m : M), ‖f m‖ ≤ ‖m‖
-- Mathlib.CategoryTheory.Localization.OfQuotient
CategoryTheory.Functor.isLocalization_of_essSurj_of_full_of_exists_pathObjects : ∀ {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] (L : CategoryTheory.Functor C D) [L.EssSurj] [L.Full]
  (W : CategoryTheory.MorphismProperty C),
  W.IsInvertedBy L → (∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ P x, W P.ι) → L.IsLocalization W
-- Mathlib.Algebra.Module.Equiv.Basic
addMonoidHomLequivNat_symm_apply : ∀ {A : Type u_9} {B : Type u_10} (R : Type u_11) [inst : Semiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R B] (f : A →ₗ[ℕ] B), (addMonoidHomLequivNat R).symm f = f.toAddMonoidHom
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.apply_eq_iff_eq : ∀ {α : Sort u_1} {β : Sort u_2} (f : α ↪ β) (x y : α), f x = f y ↔ x = y
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
/-- Forgetting the zeroth term in a formal multilinear series, and interpreting the following terms
as multilinear maps into `E →L[𝕜] F`. If `p` is the Taylor series (`HasFTaylorSeriesUpTo`) of a
function, then `p.shift` is the Taylor series of the derivative of the function. Note that the
`p.sum` of a Taylor series `p` does not give the original function; for a formal multilinear
series that sums to the derivative of `p.sum`, see `HasFPowerSeriesOnBall.fderiv`.  -/
FormalMultilinearSeries.shift : {𝕜 : Type u} →
  {E : Type v} →
    {F : Type w} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] → FormalMultilinearSeries 𝕜 E F → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.mem_bot : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] {x : M} [inst_4 : T1Space M], x ∈ ⊥ ↔ x = 0
-- Mathlib.Algebra.Notation.Pi.Defs
Function.const_one : ∀ {α : Type u_2} {M : Type u_7} [inst : One M], Function.const α 1 = 1
-- Mathlib.Data.Finset.Insert
/-- A version of `LawfulSingleton.insert_empty_eq` that works with `dsimp`.  -/
Finset.insert_empty : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α}, insert a ∅ = {a}
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.roots_eq_zero_iff_natDegree_eq_zero : ∀ {k : Type u} [inst : Field k] [IsAlgClosed k] {p : Polynomial k}, p.roots = 0 ↔ p.natDegree = 0
-- Mathlib.LinearAlgebra.Matrix.ToLin
vecMulVecBilin_apply_apply : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_4) (S : Type u_5) {A : Type u_6} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : Module R A] [inst_4 : Module S A] [inst_5 : SMulCommClass S R A]
  [inst_6 : SMulCommClass S A A] [inst_7 : IsScalarTower R A A] (x : m → A) (y : n → A),
  ((vecMulVecBilin R S) x) y = Matrix.vecMulVec x y
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.inhabited : {V : Type u} → {G : SimpleGraph V} → [Inhabited V] → Inhabited G.ConnectedComponent
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.glue.eq_2 : ∀ {α : Type u} {β : α → Type v} (size : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
  (hl_2 : (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').Balanced)
  (hr_2 : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (hlr_3 :
    Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').size
      Std.DTreeMap.Internal.Impl.leaf.size),
  (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').glue Std.DTreeMap.Internal.Impl.leaf hl_2 hr_2 hlr_3 =
    Std.DTreeMap.Internal.Impl.inner size k' v' l' r'
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.count_pow : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
  [inst_2 : DecidableEq (Associates α)] [inst_3 : (p : Associates α) → Decidable (Irreducible p)] [Nontrivial α]
  {a : Associates α},
  a ≠ 0 → ∀ {p : Associates α}, Irreducible p → ∀ (k : ℕ), p.count (a ^ k).factors = k * p.count a.factors
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_swap' : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] {x y : α},
  Equiv.Perm.sign (Equiv.swap x y) = if x = y then 1 else -1