mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.ofCoalgHom_symm : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (f : A →ₗc[R] B) (g : B →ₗc[R] A) (h₁ : f.comp g = CoalgHom.id R B)
  (h₂ : g.comp f = CoalgHom.id R A), (CoalgEquiv.ofCoalgHom f g h₁ h₂).symm = CoalgEquiv.ofCoalgHom g f h₂ h₁
-- Init.Data.Array.Lemmas
Array.replicate_eq_append_iff : ∀ {α : Type u_1} {n : ℕ} {xs ys : Array α} {a : α},
  Array.replicate n a = xs ++ ys ↔
    xs.size + ys.size = n ∧ xs = Array.replicate xs.size a ∧ ys = Array.replicate ys.size a
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- **Weierstrass preparation theorem** ([washington_cyclotomic], Theorem 7.3):
let `g` be a power series over a complete local ring,
such that its image in the residue field is not zero. Then there exists a distinguished
polynomial `f` and a power series `h` which is a unit, such that `g = f * h`.  -/
PowerSeries.exists_isWeierstrassFactorization : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A]
  {g : PowerSeries A}, (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0 → ∃ f h, g.IsWeierstrassFactorization f h
-- Lean.Elab.InfoTree.Types
Lean.Elab.DocInfo.mk.inj : ∀ {toElabInfo toElabInfo_1 : Lean.Elab.ElabInfo},
  { toElabInfo := toElabInfo } = { toElabInfo := toElabInfo_1 } → toElabInfo = toElabInfo_1
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.LeftHomotopyRel.equivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] (X Y : C)
  [HomotopicalAlgebra.IsCofibrant X], Equivalence HomotopicalAlgebra.LeftHomotopyRel
-- Mathlib.CategoryTheory.Monoidal.Hopf_
CategoryTheory.HopfObj.antipode_counit_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : C) [inst_3 : CategoryTheory.HopfObj A] {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.HopfObj.antipode
      (CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit h
-- Mathlib.GroupTheory.Coxeter.Basic
/-- The Coxeter relation associated to a Coxeter matrix $M$ and two indices $i, i' \in B$.
That is, the relation $(s_i s_{i'})^{M_{i, i'}}$, considered as an element of the free group
on $\{s_i\}_{i \in B}$.
If $M_{i, i'} = 0$, then this is the identity, indicating that there is no relation between
$s_i$ and $s_{i'}$.  -/
CoxeterMatrix.relation : {B : Type u_1} → CoxeterMatrix B → B → B → FreeGroup B
-- Mathlib.Data.Holor
Holor.CPRankMax1.below.cons : ∀ {α : Type} [inst : Mul α] {motive : {ds : List ℕ} → (a : Holor α ds) → a.CPRankMax1 → Prop} {d : ℕ} {ds : List ℕ}
  (x : Holor α [d]) (y : Holor α ds) (a : y.CPRankMax1),
  Holor.CPRankMax1.below a → motive y a → Holor.CPRankMax1.below ⋯
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.instInhabited.eq_1 : ∀ (α : Type u_2) [inst : Preorder α] [inst_1 : AddZeroClass α],
  OrderAddMonoidHom.instInhabited α = { default := OrderAddMonoidHom.id α }
-- Mathlib.Algebra.Free
FreeAddSemigroup.ext : ∀ {α : Type u} {x y : FreeAddSemigroup α}, x.head = y.head → x.tail = y.tail → x = y
-- Mathlib.Algebra.Group.Fin.Tuple
Fin.insertNth_add : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} [inst : (j : Fin (n + 1)) → Add (α j)] (i : Fin (n + 1)) (x y : α i)
  (p q : (j : Fin n) → α (i.succAbove j)), i.insertNth (x + y) (p + q) = i.insertNth x p + i.insertNth y q
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- If `cons (exp, coef) tl` is `Sorted`, then `coef` and `tl` are `Sorted`, and the
leading exponent of `tl` is less than `exp`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.elim_cons : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl}
  {tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl).Sorted →
    coef.Sorted ∧ tl.leadingExp < ↑exp ∧ tl.Sorted
-- Mathlib.Topology.MetricSpace.HausdorffAlexandroff
/-- A continuous surjection from the Cantor space to the Hilbert cube.  -/
cantorToHilbert : (ℕ → Bool) → ℕ → ↑unitInterval
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.constGetThenInsertIfNew?! : ∀ {α : Type u} {β : Type v} {x : Ord α} [Std.TransOrd α] {k : α} {v : β} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.WF → (Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?! t k v).2.WF
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_insertMany!_list : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α],
  t.WF → ∀ {l : List ((a : α) × β a)} {k : α}, k ∈ ↑(t.insertMany! l) ↔ k ∈ t ∨ (List.map Sigma.fst l).contains k = true
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.multiples_eq_image_range_addOrderOf : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} [inst_1 : DecidableEq G],
  IsOfFinAddOrder x → ↑(AddSubmonoid.multiples x) = ↑(Finset.image (fun x_1 => x_1 • x) (Finset.range (addOrderOf x)))
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Break.runK.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive x
-- Std.Data.DHashMap.Basic
/-- Compares two hash maps using Boolean equality on keys and values.

Returns `true` if the maps contain the same key-value pairs, `false` otherwise.
 -/
Std.DHashMap.Const.beq : {α : Type u} →
  {x : Hashable α} →
    {β : Type v} → [inst : BEq α] → [BEq β] → (Std.DHashMap α fun x => β) → (Std.DHashMap α fun x => β) → Bool
-- Mathlib.Topology.Algebra.RestrictedProduct.Units
/-- Constructs a unit in a restricted product `Πʳ i, [R i, B i]_[𝓕]` given an element `x` of
the usual product and the condition that `x` is eventually in the units of `B i` along `𝓕`.  -/
RestrictedProduct.mkUnit : {ι : Type u_1} →
  {R : ι → Type u_2} →
    [inst : (i : ι) → Monoid (R i)] →
      {S : ι → Type u_3} →
        [inst_1 : (i : ι) → SetLike (S i) (R i)] →
          [inst_2 : ∀ (i : ι), SubmonoidClass (S i) (R i)] →
            {B : (i : ι) → S i} →
              {𝓕 : Filter ι} →
                (x : (i : ι) → (R i)ˣ) →
                  (∀ᶠ (i : ι) in 𝓕, x i ∈ (Submonoid.ofClass (B i)).units) →
                    (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)ˣ
-- Aesop.RulePattern
Aesop.RulePattern.mk.sizeOf_spec : ∀ (pattern : Lean.Meta.AbstractMVarsResult) (argMap levelArgMap : Array (Option ℕ))
  (discrTreeKeys : Array Lean.Meta.DiscrTree.Key),
  sizeOf { pattern := pattern, argMap := argMap, levelArgMap := levelArgMap, discrTreeKeys := discrTreeKeys } =
    1 + sizeOf pattern + sizeOf argMap + sizeOf levelArgMap + sizeOf discrTreeKeys
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
/-- `V.restrictScalars S` is the `S`-submodule of the `S`-module given by restriction of scalars,
corresponding to `V`, an `R`-submodule of the original `R`-module.
 -/
Submodule.restrictScalars : (S : Type u_1) →
  {R : Type u_2} →
    {M : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Semiring S] →
            [inst_3 : Module S M] →
              [inst_4 : Module R M] → [inst_5 : SMul S R] → [IsScalarTower S R M] → Submodule R M → Submodule S M
-- Aesop.ElabM
Aesop.ElabM.Context.forAdditionalGlobalRules : Lean.MetaM Aesop.ElabM.Context
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
/-- The equivalence between group homs `G → H` and bialgebra homs `R[G] → R[H]` of group algebras
over a domain.  -/
AddMonoidAlgebra.mapDomainBialgHomEquiv : {R : Type u_1} →
  {G : Type u_5} →
    {H : Type u_6} →
      [inst : CommRing R] →
        [IsDomain R] →
          [inst_2 : AddGroup G] → [inst_3 : AddGroup H] → (G →+ H) ≃ (AddMonoidAlgebra R G →ₐc[R] AddMonoidAlgebra R H)
-- Mathlib.NumberTheory.FermatPsp
/-- Infinite set variant of `Nat.exists_infinite_pseudoprimes`
 -/
Nat.infinite_setOfPred_pseudoprimes : ∀ {b : ℕ}, 1 ≤ b → {n | n.FermatPsp b}.Infinite
-- Lean.Meta.Tactic.Grind.PropagatorAttr
Lean.Meta.Grind.instInhabitedBuiltinPropagators.default : Lean.Meta.Grind.BuiltinPropagators
-- Mathlib.RingTheory.Noetherian.Basic
isNoetherianRing_of_ringEquiv : ∀ (R : Type u_1) [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] (f : R ≃+* S) [IsNoetherianRing R],
  IsNoetherianRing S
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSuppLTSubfield_carrier : ∀ (Γ : Type u_1) (R : Type u_2) (κ : Cardinal.{u_1}) [inst : LinearOrder Γ] [inst_1 : AddCommGroup Γ]
  [inst_2 : IsOrderedAddMonoid Γ] [inst_3 : Field R] [hκ : Fact (Cardinal.aleph0 < κ)],
  ↑(HahnSeries.cardSuppLTSubfield Γ R κ) = (HahnSeries.cardSuppLTAddSubgroup Γ R κ).carrier
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_nonUnitalRingHom_inj_iff : ∀ {R : Type u_7} {S : Type u_8} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (f g : R ≃+* S), f = g ↔ ↑f = ↑g
-- Mathlib.Data.Int.Lemmas
Int.natAbs_inj_of_nonneg_of_nonpos : ∀ {a b : ℤ}, 0 ≤ a → b ≤ 0 → (a.natAbs = b.natAbs ↔ a = -b)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach.0.Std.Iterators.Types.Attach.Monadic.modifyStep.eq_3 : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {P : β → Prop}
  (it : Std.IterM m { out // P out }) (property : it.internalState.inner.IsPlausibleStep Std.IterStep.done),
  Std.Iterators.Types.Attach.Monadic.modifyStep it ⟨Std.IterStep.done, property⟩ = Std.IterStep.done
-- Mathlib.Order.Cover
instIsNonstrictStrictOrderWCovByCovBy : ∀ {α : Type u_1} [inst : Preorder α], IsNonstrictStrictOrder α (fun x1 x2 => x1 ⩿ x2) fun x1 x2 => x1 ⋖ x2
-- Init.Data.Option.Attach
Option.attachWith.congr_simp : ∀ {α : Type u_1} (xs xs_1 : Option α) (e_xs : xs = xs_1) (P : α → Prop) (H : ∀ (x : α), xs = some x → P x),
  xs.attachWith P H = xs_1.attachWith P ⋯
-- Batteries.Tactic.Lint.TypeClass
/-- A linter for checking if any declaration whose type is not a class is marked as an instance.
 -/
Batteries.Tactic.Lint.nonClassInstance : Batteries.Tactic.Lint.Linter
-- Init.Sym.Simp.SimprocDSL
Lean.Parser.Sym.Simp.sym_discharger.quot : Lean.ParserDescr
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct_apply : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] [inst_9 : Semiring C]
  [inst_10 : Algebra S C] (f : TensorProduct R A B ≃ₗ[S] C)
  (h_mul : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂))
  (h_one : f (1 ⊗ₜ[R] 1) = 1) (x : TensorProduct R A B),
  (Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct f h_mul h_one) x = f x
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The product of two strictly antitone functions is strictly antitone.  -/
StrictAntiOn.mul' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
  [MulLeftStrictMono α] [MulRightStrictMono α],
  StrictAntiOn f s → StrictAntiOn g s → StrictAntiOn (fun x => f x * g x) s
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D)
  {F G : CategoryTheory.Functor J C} {α : F ≅ G} {c : CategoryTheory.Limits.Cone F},
  H.mapConePostcomposeEquivalenceFunctor.inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- In a category in which every epimorphism is normal, we can express every epimorphism as
a kernel. This is not an instance because it would create an instance loop.  -/
CategoryTheory.normalEpiOfEpi : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        [CategoryTheory.IsNormalEpiCategory C] → (f : X ⟶ Y) → [CategoryTheory.Epi f] → CategoryTheory.NormalEpi f
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.C_eval_two : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ), Polynomial.eval 2 (Polynomial.Chebyshev.C R n) = 2
-- Lean.Data.JsonRpc
Lean.JsonRpc.Request.mk : {α : Type u} → Lean.JsonRpc.RequestID → String → α → Lean.JsonRpc.Request α
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- Make a morphism between triangles from the required data.  -/
CategoryTheory.Pretriangulated.Triangle.homMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      (A B : CategoryTheory.Pretriangulated.Triangle C) →
        (hom₁ : A.obj₁ ⟶ B.obj₁) →
          (hom₂ : A.obj₂ ⟶ B.obj₂) →
            (hom₃ : A.obj₃ ⟶ B.obj₃) →
              autoParam
                  (CategoryTheory.CategoryStruct.comp A.mor₁ hom₂ = CategoryTheory.CategoryStruct.comp hom₁ B.mor₁)
                  CategoryTheory.Pretriangulated.Triangle.homMk._auto_1 →
                autoParam
                    (CategoryTheory.CategoryStruct.comp A.mor₂ hom₃ = CategoryTheory.CategoryStruct.comp hom₂ B.mor₂)
                    CategoryTheory.Pretriangulated.Triangle.homMk._auto_3 →
                  autoParam
                      (CategoryTheory.CategoryStruct.comp A.mor₃ ((CategoryTheory.shiftFunctor C 1).map hom₁) =
                        CategoryTheory.CategoryStruct.comp hom₃ B.mor₃)
                      CategoryTheory.Pretriangulated.Triangle.homMk._auto_5 →
                    (A ⟶ B)
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
/-- The adjunction between the nerve functor and the homotopy category functor is, up to
isomorphism, the composite of the adjunctions `SSet.coskAdj 2` and `nerve₂Adj`.  -/
CategoryTheory.nerveAdjunction : SSet.hoFunctor ⊣ CategoryTheory.nerveFunctor
-- Lean.Elab.Attributes
Lean.Elab.elabDeclAttrs : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [Lean.MonadResolveName m] →
        [Lean.MonadError m] →
          [Lean.Elab.MonadMacroAdapter m] →
            [Lean.MonadRecDepth m] →
              [Lean.MonadTrace m] →
                [Lean.MonadOptions m] →
                  [Lean.AddMessageContext m] →
                    [Lean.MonadLog m] →
                      [MonadLiftT IO m] → [MonadFinally m] → Lean.Syntax → m (Array Lean.Elab.Attribute)
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- The boundary is the complement of the interior.  -/
ModelWithCorners.compl_interior : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M],
  (ModelWithCorners.interior M)ᶜ = ModelWithCorners.boundary M
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.sum_map_le_sum : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : Preorder α] {s : Multiset α} [AddLeftMono α] (f : α → α),
  (∀ x ∈ s, f x ≤ x) → (Multiset.map f s).sum ≤ s.sum
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- Inclusion of unbundled `n`-times continuously differentiable function with support included
in a compact `K` into the space `𝓓^{n}_{K}`.  -/
ContDiffMapSupportedIn.of_support_subset : {E : Type u_2} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℝ F] →
            {n : ℕ∞} →
              {K : TopologicalSpace.Compacts E} →
                {f : E → F} → ContDiff ℝ (↑n) f → Function.support f ⊆ ↑K → ContDiffMapSupportedIn E F n K
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.ofSubtype_comp_subtype : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s : Finset α),
  (alternatingGroup α).subtype.comp (alternatingGroup.ofSubtype s) =
    Equiv.Perm.ofSubtype.comp (alternatingGroup ↥s).subtype
-- Mathlib.Algebra.Group.Defs
/-- Raising to the power `(n + 1 : ℕ)` behaves as expected.  -/
Monoid.npow_succ : ∀ {M : Type u} [self : Monoid M] (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instInhabitedCallHierarchyOutgoingCall.default : Lean.Lsp.CallHierarchyOutgoingCall
-- Mathlib.Algebra.DirectSum.Algebra
DirectSum.gMulLHom_apply_apply : ∀ {ι : Type uι} (R : Type uR) (A : ι → Type uA) [inst : CommSemiring R] [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : (i : ι) → Module R (A i)] [inst_3 : AddMonoid ι] [inst_4 : DirectSum.GSemiring A]
  [inst_5 : DirectSum.GAlgebra R A] {i j : ι} (a : A i) (b : A j),
  ((DirectSum.gMulLHom R A) a) b = GradedMonoid.GMul.mul a b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.mem_of_mem_insertManyIfNewUnit_list : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α] (h : t.WF) {l : List α} {k : α},
  l.contains k = false → k ∈ ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯) → k ∈ t
-- Mathlib.Logic.Encodable.Basic
/-- See also `nonempty_fintype`, `nonempty_denumerable`.  -/
nonempty_encodable : ∀ (α : Type u_1) [Countable α], Nonempty (Encodable α)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getKeyLTD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyLTD k fallback = t₂.getKeyLTD k fallback
-- Batteries.Data.Float.Lemmas
/-- Returns true if the bits represent an NaN value  -/
Float.Model.UnpackedFloat.isNaNBits : {spec : Float.Model.Format} → BitVec spec.numBits → Bool
-- Mathlib.Data.Num.Basic
ZNum.instLE : LE ZNum
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_union_le_size_add_size : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  (t₁ ∪ t₂).size ≤ t₁.size + t₂.size
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.op_iInf : ∀ {ι : Sort u_1} {M : Type u_2} [inst : Add M] (S : ι → AddSubsemigroup M), (iInf S).op = ⨅ i, (S i).op
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
/-- Part of an `sl₂` triple used in Geck's construction of a Lie algebra from a root system.  -/
RootPairing.GeckConstruction.h : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {P : RootPairing ι R M N} →
                    [P.IsCrystallographic] → {b : P.Base} → ↥b.support → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
-- Std.Time.Date.Unit.Day
Std.Time.Day.Ordinal.instDecidableEqOfYear : {leap : Bool} → DecidableEq (Std.Time.Day.Ordinal.OfYear leap)
-- Mathlib.Condensed.Discrete.Module
CompHausLike.LocallyConstantModule.functorToPresheaves_obj_obj_carrier : ∀ {P : TopCat → Prop} (R : Type (max u w)) [inst : Ring R] (X : ModuleCat R) (x : (CompHausLike P)ᵒᵖ),
  ↑(((CompHausLike.LocallyConstantModule.functorToPresheaves R).obj X).obj x) =
    LocallyConstant ↑(Opposite.unop x).toTop ↑X
-- Mathlib.Topology.Algebra.Group.Basic
isClosedMap_mul_right : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] (a : G),
  IsClosedMap fun x => x * a
-- Mathlib.Data.FunLike.Module
FunLike.addAction.eq_1 : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_4} {β : Type u_5} [i : FunLike F α β] [inst : VAdd M F]
  [inst_1 : AddMonoid M] [inst_2 : AddAction M β] [inst_3 : IsVAddApply M F α β],
  FunLike.addAction = Function.Injective.addAction DFunLike.coe ⋯ ⋯
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- Naturally isomorphic endofunctors give equivalent categories of algebras.
Furthermore, they are equivalent as categories over `C`, that is,
we have `equiv_of_nat_iso h ⋙ forget = forget`.
 -/
CategoryTheory.Endofunctor.Algebra.equivOfNatIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C C} →
      (F ≅ G) → (CategoryTheory.Endofunctor.Algebra F ≌ CategoryTheory.Endofunctor.Algebra G)
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.rightInvSeq_singleton : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B),
  cs.rightInvSeq [i] = [cs.simple i]
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.relIndex_strictPeriods : ∀ {R : Type u_1} [inst : Ring R] (𝒢 : Subgroup (GL (Fin 2) R)),
  𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2
-- Mathlib.Geometry.Convex.Cone.Pointed
ConvexCone.mem_toPointedCone : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] {C : ConvexCone R E} (hC : C.Pointed) (x : E),
  x ∈ C.toPointedCone hC ↔ x ∈ C
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.single_pow : ∀ {R : Type u_1} [inst : CommSemiring R] {a c : R} {b : ℕ}, a ^ b = c → (a + 0) ^ b = c + 0
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.DiagramOfCones.mk.inj : ∀ {J : Type u_1} {K : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} J}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} K} {C : Type u_3} {inst_2 : CategoryTheory.Category.{v_3, u_3} C}
  {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} {obj : (j : J) → CategoryTheory.Limits.Cone (F.obj j)}
  {map : {j j' : J} → (f : j ⟶ j') → (CategoryTheory.Limits.Cone.postcompose (F.map f)).obj (obj j) ⟶ obj j'}
  {id :
    autoParam
      (∀ (j : J),
        (map (CategoryTheory.CategoryStruct.id j)).hom =
          CategoryTheory.CategoryStruct.id
            ((CategoryTheory.Limits.Cone.postcompose (F.map (CategoryTheory.CategoryStruct.id j))).obj (obj j)).pt)
      CategoryTheory.Limits.DiagramOfCones.id._autoParam}
  {comp :
    autoParam
      (∀ {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃),
        (map (CategoryTheory.CategoryStruct.comp f g)).hom = CategoryTheory.CategoryStruct.comp (map f).hom (map g).hom)
      CategoryTheory.Limits.DiagramOfCones.comp._autoParam}
  {obj_1 : (j : J) → CategoryTheory.Limits.Cone (F.obj j)}
  {map_1 : {j j' : J} → (f : j ⟶ j') → (CategoryTheory.Limits.Cone.postcompose (F.map f)).obj (obj_1 j) ⟶ obj_1 j'}
  {id_1 :
    autoParam
      (∀ (j : J),
        (map_1 (CategoryTheory.CategoryStruct.id j)).hom =
          CategoryTheory.CategoryStruct.id
            ((CategoryTheory.Limits.Cone.postcompose (F.map (CategoryTheory.CategoryStruct.id j))).obj (obj_1 j)).pt)
      CategoryTheory.Limits.DiagramOfCones.id._autoParam}
  {comp_1 :
    autoParam
      (∀ {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃),
        (map_1 (CategoryTheory.CategoryStruct.comp f g)).hom =
          CategoryTheory.CategoryStruct.comp (map_1 f).hom (map_1 g).hom)
      CategoryTheory.Limits.DiagramOfCones.comp._autoParam},
  { obj := obj, map := map, id := id, comp := comp } = { obj := obj_1, map := map_1, id := id_1, comp := comp_1 } →
    obj = obj_1 ∧ map ≍ map_1