mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Pi
LinearMap.range_compLeft : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (f : M →ₗ[R] M₂) (I : Type u_1),
  (f.compLeft I).range = Submodule.pi Set.univ fun x => f.range
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The bottom left map in the oplax associativity hexagon.
 -/
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          (F : CategoryTheory.Functor C D) →
            CategoryTheory.MonoidalCategory.curriedTensorPrePre F ⟶
              CategoryTheory.MonoidalCategory.curriedTensorPrePre' F
-- Mathlib.RingTheory.Multiplicity
multiplicity_eq_zero_of_coprime : ∀ {p a b : ℕ}, p ≠ 1 → multiplicity p a ≤ multiplicity p b → a.Coprime b → multiplicity p a = 0
-- Mathlib.Data.Nat.Digits.Defs
Nat.ofDigits_one_cons : ∀ {α : Type u_1} [inst : Semiring α] (h : ℕ) (L : List ℕ), Nat.ofDigits 1 (h :: L) = ↑h + Nat.ofDigits 1 L
-- Mathlib.Algebra.Module.PUnit
PUnit.instIsCentralVAdd : ∀ {R : Type u_1}, IsCentralVAdd R PUnit.{u_3 + 1}
-- Mathlib.Data.Finset.Density
/-- **Alias** of the reverse direction of `Finset.dens_ne_zero`. -/
Finset.Nonempty.dens_ne_zero : ∀ {α : Type u_2} [inst : Fintype α] {s : Finset α}, s.Nonempty → s.dens ≠ 0
-- Mathlib.RingTheory.Support
LinearEquiv.support_eq : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (e : M ≃ₗ[R] N), Module.support R M = Module.support R N
-- Mathlib.Data.Finset.Card
Finset.card_eq_zero : ∀ {α : Type u_1} {s : Finset α}, s.card = 0 ↔ s = ∅
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.constantCoeff_rename : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) [inst : Filter.TendstoCofinite f] [inst_1 : CommSemiring R]
  (p : MvPowerSeries σ R), MvPowerSeries.constantCoeff ((MvPowerSeries.rename f) p) = MvPowerSeries.constantCoeff p
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.pUnitAlgEquiv_monomial : ∀ (R : Type u) [inst : CommSemiring R] {d : PUnit.{1} →₀ ℕ} {r : R},
  (MvPolynomial.pUnitAlgEquiv R) ((MvPolynomial.monomial d) r) = (Polynomial.monomial (d ())) r
-- Lean.Environment
Lean.instInhabitedImportState.default : Lean.ImportState
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.LogConfig : Type
-- Init.Data.ByteArray.Basic
ByteArray.fastAppend.eq_1 : ∀ (a b : ByteArray), a.fastAppend b = b.copySlice 0 a a.size b.size false
-- Mathlib.Data.Sum.Order
Sum.noMinOrder_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β], NoMinOrder (α ⊕ β) ↔ NoMinOrder α ∧ NoMinOrder β
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.closure_nsmul_le : ∀ {M : Type u_3} [inst : AddMonoid M] {s : Set M} {n : ℕ}, AddSubmonoid.closure (n • s) ≤ AddSubmonoid.closure s
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.Transported.instMonoidalCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          (e : C ≌ D) → CategoryTheory.MonoidalCategory (CategoryTheory.Monoidal.Transported e)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.RenameParams.mk.sizeOf_spec : ∀ (toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams) (newName : String),
  sizeOf { toTextDocumentPositionParams := toTextDocumentPositionParams, newName := newName } =
    1 + sizeOf toTextDocumentPositionParams + sizeOf newName
-- Mathlib.Algebra.Group.Opposite
AddCommute.unop : ∀ {α : Type u_1} [inst : Add α] {x y : αᵃᵒᵖ}, AddCommute x y → AddCommute (AddOpposite.unop x) (AddOpposite.unop y)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
/-- `simplicialInsert` preserves admissibility  -/
SimplexCategoryGenRel.simplicialInsert_isAdmissible : ∀ (m : ℕ) (L : List ℕ),
  SimplexCategoryGenRel.IsAdmissible (m + 1) L →
    ∀ j ≤ m, SimplexCategoryGenRel.IsAdmissible m (SimplexCategoryGenRel.simplicialInsert j L)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
/-- The first element of `op (a :: s)` depends only on `a`.  -/
Tactic.ComputeAsymptotics.Seq.FriendlyOperation.op_cons_head_eq : ∀ {α : Type u_1} {op : Stream'.Seq α → Stream'.Seq α},
  Tactic.ComputeAsymptotics.Seq.FriendlyOperation op →
    ∀ {a : α} {s t : Stream'.Seq α}, (op (Stream'.Seq.cons a s)).head = (op (Stream'.Seq.cons a t)).head
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
/-- For a sheaf `F`, `F(U ⊔ V)` is the pullback of `F(U) ⟶ F(U ⊓ V)` and `F(V) ⟶ F(U ⊓ V)`.  -/
TopCat.Sheaf.isLimitPullbackCone : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : TopCat} →
      (F : TopCat.Sheaf C X) →
        (U V : TopologicalSpace.Opens ↑X) → CategoryTheory.Limits.IsLimit (F.interUnionPullbackCone U V)
-- Mathlib.Algebra.Group.Submonoid.Pointwise
coe_set_pow : ∀ {M : Type u_3} {S : Type u_6} [inst : Monoid M] [inst_1 : SetLike S M] [SubmonoidClass S M] {n : ℕ},
  n ≠ 0 → ∀ (H : S), ↑H ^ n = ↑H
-- Mathlib.RingTheory.Extension.Cotangent.Basis
/-- Let `S` be a finitely presented `R`-algebra and suppose `P : R[X] → S` generates `S` with
kernel `I`. If `I/I²` is free, there exists an `R`-presentation `P'` of `S` extending `P` with
kernel `I'`, such that `I'/I'²` is free on the images of the relations of `P'`.
See `Algebra.Generators.exists_presentation_of_basis_cotangent` for a version taking
a basis of `I/I²` instead.  -/
Algebra.Generators.exists_presentation_of_free_cotangent : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FinitePresentation R S] {α : Type u_4} (P : Algebra.Generators R S α) [Finite α]
  [Module.Free S P.toExtension.Cotangent],
  ∃ P' b,
    P'.val ∘ Sum.inr = P.val ∧
      ∀ (r : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)),
        b r = Algebra.Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩
-- Mathlib.Logic.Equiv.Sum
Equiv.sumCompl_symm_apply_neg : ∀ {α : Type u_9} {p : α → Prop} [inst : DecidablePred p] (x : { x // ¬p x }), (Equiv.sumCompl p).symm ↑x = Sum.inr x
-- Lean.Meta.AppBuilder
/-- `mkLetFun x v e` creates `letFun v (fun x => e)`.
The expression `x` can either be a free variable or a metavariable, and the function suitably abstracts `x` in `e`.
 -/
Lean.Meta.mkLetFun : Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedSubgroup.instPartialOrder : (G : Type u) → [inst : Group G] → [inst_1 : TopologicalSpace G] → PartialOrder (ClosedSubgroup G)
-- Mathlib.Algebra.BigOperators.Fin
List.alternatingProd.eq_def : ∀ {G : Type u_4} [inst : One G] [inst_1 : Mul G] [inst_2 : Inv G] (x : List G),
  x.alternatingProd =
    match x with
    | [] => 1
    | [g] => g
    | g :: h :: t => g * h⁻¹ * t.alternatingProd
-- Init.Data.SInt.Lemmas
ISize.toInt64_ofInt : ∀ {n : ℤ}, ISize.minValue.toInt ≤ n → n ≤ ISize.maxValue.toInt → (ISize.ofInt n).toInt64 = Int64.ofInt n
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- The map `opZ^n(f₁ ≫ f₂, f₃) ⟶ E^n(f₁, f₂, f₃)`.  -/
CategoryTheory.Abelian.SpectralObject.opcyclesToE : {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₀ i₁ i₂ i₃ : ι} →
              (f₁ : i₀ ⟶ i₁) →
                (f₂ : i₁ ⟶ i₂) →
                  (f₃ : i₂ ⟶ i₃) →
                    (f₁₂ : i₀ ⟶ i₂) →
                      CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂ →
                        (n₀ n₁ n₂ : ℤ) →
                          (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.opcyclesToE._auto_1) →
                            (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.opcyclesToE._auto_3) →
                              X.opcycles f₁₂ f₃ n₁ ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
-- ProofWidgets.Component.RefreshComponent
_private.ProofWidgets.Component.RefreshComponent.0.ProofWidgets.RefreshToken.mk : IO.Ref ProofWidgets.RefreshComponent.RefreshState →
  IO.CancelToken → IO.Ref (IO.Promise Unit) → ProofWidgets.RefreshToken
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
/-- When `B` is a manifold with respect to a model `IB` and `E` is a
topological vector bundle over `B` with fibers isomorphic to `F`,
then `ContMDiffVectorBundle n F E IB` registers that the bundle is `C^n`, in the sense of having
`C^n` transition functions. This is a mixin, not carrying any new data.  -/
ContMDiffVectorBundle : WithTop ℕ∞ →
  {𝕜 : Type u_1} →
    {B : Type u_2} →
      (F : Type u_4) →
        (E : B → Type u_6) →
          [inst : NontriviallyNormedField 𝕜] →
            {EB : Type u_7} →
              [inst_1 : NormedAddCommGroup EB] →
                [inst_2 : NormedSpace 𝕜 EB] →
                  {HB : Type u_8} →
                    [inst_3 : TopologicalSpace HB] →
                      ModelWithCorners 𝕜 EB HB →
                        [inst_4 : TopologicalSpace B] →
                          [ChartedSpace HB B] →
                            [inst_6 : (x : B) → AddCommMonoid (E x)] →
                              [inst_7 : (x : B) → Module 𝕜 (E x)] →
                                [inst_8 : NormedAddCommGroup F] →
                                  [inst_9 : NormedSpace 𝕜 F] →
                                    [inst_10 : TopologicalSpace (Bundle.TotalSpace F E)] →
                                      [inst_11 : (x : B) → TopologicalSpace (E x)] →
                                        [inst_12 : FiberBundle F E] → [VectorBundle 𝕜 F E] → Prop
-- Lean.Parser.Types
Lean.Parser.SyntaxStack.shrink : Lean.Parser.SyntaxStack → ℕ → Lean.Parser.SyntaxStack
-- Mathlib.Analysis.Convex.Between
Wbtw.collinear : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P}, Wbtw R x y z → Collinear R {x, y, z}
-- Mathlib.Analysis.Convolution
/-- Commutativity of convolution  -/
MeasureTheory.convolution_flip : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : NormedSpace ℝ F]
  [inst_9 : AddCommGroup G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] [MeasurableNeg G] [MeasurableAdd G],
  MeasureTheory.convolution g f L.flip μ = MeasureTheory.convolution f g L μ
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.instAlgebra : {𝕜₁ : Type u_1} →
  [inst : NormedField 𝕜₁] →
    {E : Type u_3} →
      [inst_1 : AddCommGroup E] →
        [inst_2 : TopologicalSpace E] →
          [inst_3 : Module 𝕜₁ E] →
            {S : Type u_5} →
              [inst_4 : CommSemiring S] →
                [inst_5 : Module S E] →
                  [SMulCommClass 𝕜₁ S E] →
                    [inst_7 : SMul S 𝕜₁] →
                      [IsScalarTower S 𝕜₁ E] →
                        [ContinuousConstSMul S E] → [inst_10 : IsTopologicalAddGroup E] → Algebra S (E →WOT[𝕜₁] E)
-- Mathlib.RingTheory.AdicCompletion.Completeness
/-- An auxiliary lift function used in the definition of `ofValEqZero`.
Use `ofValEqZero` instead.  -/
AdicCompletion.ofValEqZeroAux : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      {M : Type u_2} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            {a b c : ℕ} → {x : AdicCompletion I M} → c = b + a → ↑x a = 0 → ↥(I ^ a • ⊤) ⧸ I ^ b • ⊤
-- Mathlib.Algebra.Category.Grp.Limits
CommGrpCat.forget₂Group_preservesLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J],
  CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget₂ CommGrpCat GrpCat)
-- Init.Core
PSum.inr.inj : ∀ {α : Sort u} {β : Sort v} {val val_1 : β}, PSum.inr val = PSum.inr val_1 → val = val_1
-- Mathlib.GroupTheory.FiniteAbelian.Duality
CommGroup.monoidHomMonoidHomEquiv_symm_apply_apply : ∀ (G : Type u_1) (M : Type u_2) [inst : CommGroup G] [inst_1 : Finite G] [inst_2 : CommMonoid M]
  [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] (a : G) (φ : G →* Mˣ),
  ((CommGroup.monoidHomMonoidHomEquiv G M).symm a) φ = φ a
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.of_fac' : ∀ {𝒮 : 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) (ha : p.obj a = R) (hb : p.obj b = S),
  p.map φ =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ha)
        (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯)) →
    p.IsHomLift f φ
-- Mathlib.NumberTheory.MulChar.Basic
/-- The inverse of a multiplicative character. We define it as `inverse ∘ χ`.  -/
MulChar.inv : {R : Type u_1} →
  [inst : CommMonoid R] → {R' : Type u_2} → [inst_1 : CommMonoidWithZero R'] → MulChar R R' → MulChar R R'
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- `OrthonormalBasis.singleton ι 𝕜` is the orthonormal basis sending the unique element of `ι` to
`1 : 𝕜`.  -/
OrthonormalBasis.singleton : (ι : Type u_7) → (𝕜 : Type u_8) → [inst : Unique ι] → [inst_1 : RCLike 𝕜] → OrthonormalBasis ι 𝕜 𝕜
-- Init.GrindInstances.ToInt
Lean.Grind.instZeroInt8SintOfNatNat : Lean.Grind.ToInt.Zero Int8 (Lean.Grind.IntInterval.sint 8)
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.toAbs_mul : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S) (x y : R), WithAbs.toAbs v (x * y) = WithAbs.toAbs v x * WithAbs.toAbs v y
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.foldM_eq_foldlM_keysArray : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {δ : Type w}
  {m' : Type w → Type w'} [inst_2 : Monad m'] [LawfulMonad m'] {f : δ → α → m' δ} {init : δ},
  m.WF → Std.DHashMap.Raw.foldM (fun d a x => f d a) init m = Array.foldlM f init m.keysArray
-- Lean.Widget.Diff
_private.Lean.Widget.Diff.0.Lean.Widget.ExprDiffTag.delete : Lean.Widget.ExprDiffTag✝
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- An equivalence of categories lifts to an equivalence of their additive group objects.  -/
CategoryTheory.Equivalence.mapAddGrp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            (e : C ≌ D) →
              [e.functor.Monoidal] → [e.inverse.Monoidal] → CategoryTheory.AddGrp C ≌ CategoryTheory.AddGrp D
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.extendComp_hom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cocone F) {X Y : C} (g : s.pt ⟶ Y) (f : Y ⟶ X),
  (s.extendComp g f).hom.hom = CategoryTheory.CategoryStruct.id X
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.instWellFoundedRelation : {R : Type u} → [inst : Semiring R] → WellFoundedRelation (Polynomial R)
-- Mathlib.RingTheory.Noetherian.OfPrime
/-- `Ideal.FG` is an Oka predicate.  -/
Ideal.isOka_fg : ∀ {R : Type u_1} [inst : CommRing R], Ideal.IsOka Ideal.FG
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddLeftCancelSemigroup.eq_1 : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : AddLeftCancelSemigroup M],
  Filter.Germ.instAddLeftCancelSemigroup = { toAddSemigroup := Filter.Germ.instAddSemigroup, toIsLeftCancelAdd := ⋯ }
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.WindowClientCapabilities.showDocument? : Lean.Lsp.WindowClientCapabilities → Option Lean.Lsp.ShowDocumentClientCapabilities
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  [inst_4 : SizeOf α] [inst_5 : SizeOf β] (toMulEquiv : α ≃* β)
  (map_le_map_iff' : ∀ {a b : α}, toMulEquiv.toFun a ≤ toMulEquiv.toFun b ↔ a ≤ b),
  sizeOf { toMulEquiv := toMulEquiv, map_le_map_iff' := map_le_map_iff' } = 1 + sizeOf toMulEquiv
-- Mathlib.Algebra.Lie.Loop
/-- An Lie algebra isomorphism between the Loop algebra (with `A = ℤ`) and the tensor product with
Laurent polynomials.  -/
LieAlgebra.loopAlgebraEquivLaurent : (R : Type u_1) →
  (L : Type u_3) →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] → LieAlgebra.loopAlgebra R ℤ L ≃ₗ⁅R⁆ TensorProduct R (LaurentPolynomial R) L
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_union!_of_contains_eq_false_left : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k m₁ = false →
          Std.DTreeMap.Internal.Impl.Const.get? (m₁.union! m₂) k = Std.DTreeMap.Internal.Impl.Const.get? m₂ k
-- Mathlib.Order.Interval.Set.Defs
Set.mem_Iic : ∀ {α : Type u_1} [inst : Preorder α] {b x : α}, x ∈ Set.Iic b ↔ x ≤ b
-- Mathlib.Data.Set.Operations
/-- Two functions `f₁ f₂ : α → β` are equal on `s` if `f₁ x = f₂ x` for all `x ∈ s`.  -/
Set.EqOn : {α : Type u} → {β : Type v} → (α → β) → (α → β) → Set α → Prop
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.op_toSubsemigroup : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup G), H.op.toAddSubsemigroup = H.op
-- Mathlib.Data.List.Sigma
List.notMem_keys_of_nodupKeys_cons : ∀ {α : Type u} {β : α → Type v} {s : Sigma β} {l : List (Sigma β)}, (s :: l).NodupKeys → s.fst ∉ l.keys
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.instComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {E : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} E] →
                [inst_5 : CategoryTheory.MonoidalCategory E] →
                  (F : CategoryTheory.Functor C D) →
                    (G : CategoryTheory.Functor D E) → [F.Monoidal] → [G.Monoidal] → (F.comp G).Monoidal
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.mem_powers_iff_mem_zpowers : ∀ {G : Type u_1} [inst : Group G] {x y : G}, IsOfFinOrder x → (y ∈ Submonoid.powers x ↔ y ∈ Subgroup.zpowers x)
-- Mathlib.Data.Int.Order.Units
Int.sq_eq_one_of_sq_le_three : ∀ {x : ℤ}, x ^ 2 ≤ 3 → x ≠ 0 → x ^ 2 = 1
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.symm_toNonUnitalRingHom_comp_toNonUnitalRingHom : ∀ {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (e : R ≃+* S), e.symm.toNonUnitalRingHom.comp e.toNonUnitalRingHom = NonUnitalRingHom.id R
-- Init.Data.Nat.Bitwise.Lemmas
Nat.and_self : ∀ (x : ℕ), x &&& x = x
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Gauss
/-- The monad for the Gaussian Elimination algorithm.  -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss.GaussM : ℕ → ℕ → (ℕ → ℕ → Type) → Type → Type
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.IsWeightedHomogeneous.add : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {w : σ → ℕ} {f g : MvPowerSeries σ R} {p : ℕ},
  MvPowerSeries.IsWeightedHomogeneous w f p →
    MvPowerSeries.IsWeightedHomogeneous w g p → MvPowerSeries.IsWeightedHomogeneous w (f + g) p
-- Lean.Meta.Tactic.Grind.Cases
/-- `grind` always case-splits on the following types. Even when using `grind only`.
The goal is to reduce noise in the tactic generated by `grind?`
 -/
_private.Lean.Meta.Tactic.Grind.Cases.0.Lean.Meta.Grind.builtinEagerCases : Lean.NameSet
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vsub.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β], Set.vsub = { vsub := Set.image2 fun x1 x2 => x1 -ᵥ x2 }
-- Mathlib.Probability.Process.Adapted
MeasureTheory.adapted_const' : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {β : ι → Type u_3}
  [inst_1 : (i : ι) → MeasurableSpace (β i)] (f : MeasureTheory.Filtration ι m) (x : (i : ι) → β i),
  MeasureTheory.Adapted f fun i x_1 => x i
-- Mathlib.Condensed.TopComparison
TopCat.toSheafCompHausLike_obj_map : ∀ (P : TopCat → Prop) (X : TopCat) [inst : CompHausLike.HasExplicitFiniteCoproducts P]
  [inst_1 : CompHausLike.HasExplicitPullbacks P]
  (hs :
    ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f))
  {X_1 Y : (CompHausLike P)ᵒᵖ} (f : X_1 ⟶ Y),
  (TopCat.toSheafCompHausLike P X hs).obj.map f = TypeCat.ofHom fun g => g.comp (TopCat.Hom.hom f.unop.hom)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.coe_normComp : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  (f : BoundedContinuousFunction α β), ⇑f.normComp = norm ∘ ⇑f
-- Lean.Language.Lean.Types
/-- Pushes `a?` into the array if it is `some`.  -/
Lean.Language.Lean.pushOpt : {α : Type u_1} → Option α → Array α → Array α
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
iterateInduction.eq_def : ∀ {X : ℕ → Type u_1} {a : ℕ} (x : (i : ↥(Finset.Iic a)) → X ↑i)
  (ind : (n : ℕ) → ((i : ↥(Finset.Iic n)) → X ↑i) → X (n + 1)) (x_1 : ℕ),
  iterateInduction x ind x_1 =
    match x_1 with
    | 0 => x ⟨0, ⋯⟩
    | k.succ => if h : k + 1 ≤ a then x ⟨k + 1, ⋯⟩ else ind k fun i => iterateInduction x ind ↑i
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.instCompleteSemilatticeInf : (R : Type u_1) → [inst : NonUnitalNonAssocRing R] → CompleteSemilatticeInf (TwoSidedIdeal R)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.homologyMap_nullHomotopic : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S₁ S₂ : CategoryTheory.ShortComplex C) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (h₀ : S₁.X₁ ⟶ S₂.X₁)
  (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃)
  (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0),
  CategoryTheory.ShortComplex.homologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0
-- Lean.Meta.Constructions.NoConfusion
_private.Lean.Meta.Constructions.NoConfusion.0.Lean.mkNoConfusionEnum : Lean.Name → Lean.MetaM Unit
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.bdEqual.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)),
  t₁.bdEqual t₂ = FirstOrder.Language.BoundedFormula.equal t₁ t₂
-- Mathlib.Algebra.Exact.Basic
/-- Two maps `f : M →ₗ[R] N` and `g : N →ₗ[R] P` are exact if and only if the induced maps
`LinearMap.range f → N → LinearMap.range g` are exact.  -/
Function.Exact.iff_linearMap_rangeRestrict : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P},
  Function.Exact ⇑f ⇑g ↔ Function.Exact ⇑f.range.subtype ⇑g.rangeRestrict
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- The class of morphisms in `C` that are limits of shape `J` of
natural transformations involving morphisms in `W`.  -/
CategoryTheory.MorphismProperty.limitsOfShape : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.MorphismProperty C →
      (J : Type u_1) → [CategoryTheory.Category.{v_1, u_1} J] → CategoryTheory.MorphismProperty C