mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k k' : α},
      cmp k k' = Ordering.eq →
        List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
          k ∈ List.map Prod.fst l →
            ∀ {h' : k' ∈ Std.DTreeMap.Raw.Const.insertMany t l},
              (Std.DTreeMap.Raw.Const.insertMany t l).getKey k' h' = k
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Fin.castPred.hcongr_3 : ∀ (n n' : ℕ),
  n = n' →
    ∀ (i : Fin (n + 1)) (i' : Fin (n' + 1)),
      i ≍ i' → ∀ (h : i ≠ Fin.last n) (h' : i' ≠ Fin.last n'), h ≍ h' → i.castPred h ≍ i'.castPred h'
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- If `b` is odd, then `J(-a | b) = χ₄ b * J(a | b)`.  -/
jacobiSym.neg : ∀ (a : ℤ) {b : ℕ}, Odd b → jacobiSym (-a) b = ZMod.χ₄ ↑b * jacobiSym a b
-- Mathlib.RingTheory.KrullDimension.Basic
ringKrullDim_ne_bot : ∀ {R : Type u_1} [inst : CommSemiring R] [FiniteRingKrullDim R], ringKrullDim R ≠ ⊥
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- Prepend an equality to an existing normalized certificate.

Given `c.proof : s.subject = c.norm` and `h : lhs = s.subject` return a
certificate with `proof : lhs = c.norm`.
 -/
Mathlib.Tactic.Determinant.Cert.chainProof : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} →
      {lhs rhs : Q(«$α»)} → Mathlib.Tactic.Determinant.Cert rα → Q(«$lhs» = «$rhs») → Mathlib.Tactic.Determinant.Cert rα
-- Mathlib.Order.BourbakiWitt
ChainCompletePartialOrder.IsExtremePt.setOfPred_isExtremePt_eq_bot : ∀ {α : Type u_1} [inst : ChainCompletePartialOrder α] {x : α} {f : α → α},
  (∀ (x : α), x ≤ f x) → {y | ChainCompletePartialOrder.IsExtremePt x f y} = ChainCompletePartialOrder.bot x f
-- Lean.Parser.Basic
Lean.Parser.rawCh : Char → optParam Bool false → Lean.Parser.Parser
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
/-- Detecting equality of morphisms factoring through a connected limit by pushing out along
the projections of the limit.  -/
CategoryTheory.Limits.IsLimit.pushout_hom_ext : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] [CategoryTheory.IsConnected J] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.Limits.HasPushouts C]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.HasExactLimitsOfShape J C]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) {X Y : C}
  {g h : Y ⟶ c.pt} {f : c.pt ⟶ X},
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp g
          (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.pushout.inr (c.π.app j) f)) =
        CategoryTheory.CategoryStruct.comp h
          (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.pushout.inr (c.π.app j) f))) →
    CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.comp h f
-- Mathlib.Algebra.Lie.SkewAdjoint
/-- An equivalence of modules with bilinear forms gives equivalence of Lie algebras of skew-adjoint
endomorphisms.  -/
skewAdjointLieSubalgebraEquiv : {R : Type u} →
  {M : Type v} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (B : LinearMap.BilinForm R M) →
            {N : Type w} →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  (e : N ≃ₗ[R] M) →
                    ↥(skewAdjointLieSubalgebra (LinearMap.compl₁₂ B ↑e ↑e)) ≃ₗ⁅R⁆ ↥(skewAdjointLieSubalgebra B)
-- Mathlib.Data.Matrix.Block
/-- Given a matrix whose row and column indexes are sum types, we can extract the corresponding
"top right" submatrix.  -/
Matrix.toBlocks₁₂ : {l : Type u_1} →
  {m : Type u_2} → {n : Type u_3} → {o : Type u_4} → {α : Type u_12} → Matrix (n ⊕ o) (l ⊕ m) α → Matrix n m α
-- Lean.Structure
/-- The name of the structure.  -/
Lean.StructureDescr.structName : Lean.StructureDescr → Lean.Name
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Trie.node.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (vs : Array α) (children : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)),
  sizeOf (Lean.Meta.DiscrTree.Trie.node vs children) = 1 + sizeOf vs + sizeOf children
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
/-- An easier to use version of one direction of
`GenContFract.IntFractPair.succ_nth_stream_eq_some_iff`.  -/
GenContFract.IntFractPair.stream_succ_of_some : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] {v : K} {n : ℕ}
  {p : GenContFract.IntFractPair K},
  GenContFract.IntFractPair.stream v n = some p →
    p.fr ≠ 0 → GenContFract.IntFractPair.stream v (n + 1) = some (GenContFract.IntFractPair.of p.fr⁻¹)
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.ringFunc.add.sizeOf_spec : sizeOf FirstOrder.ringFunc.add = 1
-- Mathlib.Algebra.Algebra.Opposite
/-- The canonical algebra isomorphism from `A` to `Module.End Aᵐᵒᵖ A` induced by the left
multiplication.  -/
AlgEquiv.moduleEndSelfOp : (R : Type u_1) →
  {A : Type u_3} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → A ≃ₐ[R] Module.End Aᵐᵒᵖ A
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.reverseAux.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (x x_1 : List α) → ((r : List α) → motive [] r) → ((a : α) → (l r : List α) → motive (a :: l) r) → motive x x_1
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnriched.instEnrichedCategoryCat : {C : Type u_1} →
  [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] →
    CategoryTheory.EnrichedCategory CategoryTheory.Cat (CategoryTheory.CatEnriched C)
-- Lean.Parser.Command
Lean.Parser.Command.ctor.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- The interval integral `∫ x in a..b, f x ∂μ` is defined
as `∫ x in Ioc a b, f x ∂μ - ∫ x in Ioc b a, f x ∂μ`. If `a ≤ b`, then it equals
`∫ x in Ioc a b, f x ∂μ`, otherwise it equals `-∫ x in Ioc b a, f x ∂μ`.  -/
intervalIntegral : {E : Type u_5} → [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → (ℝ → E) → ℝ → ℝ → MeasureTheory.Measure ℝ → E
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.mem_annihilator_iff : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} {H : Set (ZMod n)ˣ} {χ : DirichletCharacter R n},
  χ ∈ DirichletCharacter.annihilator R H ↔ ∀ a ∈ H, χ ↑a = 1
-- Mathlib.GroupTheory.Commutator.Finite
rank_closureCommutatorRepresentatives_le : ∀ (G : Type u_1) [inst : Group G] [inst_1 : Finite ↑(commutatorSet G)],
  Group.rank ↥(closureCommutatorRepresentatives G) ≤ 2 * Nat.card ↑(commutatorSet G)
-- Aesop.Search.Queue
Aesop.instQueueBestFirstQueue : Aesop.Queue Aesop.BestFirstQueue
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatTrans.naturality_2 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ⟶ G) {X Y : C} (e : X ≅ Y),
  CategoryTheory.CategoryStruct.comp (F.map e.hom) (CategoryTheory.CategoryStruct.comp (α.app Y) (G.map e.inv)) =
    α.app X
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- **Alias** of the reverse direction of `hasDerivWithinAt_Iio_iff_Iic`. -/
HasDerivWithinAt.Iio_of_Iic : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} [inst_3 : PartialOrder 𝕜],
  HasDerivWithinAt f f' (Set.Iic x) x → HasDerivWithinAt f f' (Set.Iio x) x
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
/-- Given a functor `F : D ⥤ Cᵒᵖ`, where `C` is Grothendieck abelian, this is a ring `R` such that
`Cᵒᵖ` has a nice embedding into `ModuleCat (EmbeddingRing F)`; see
`OppositeModuleEmbedding.embedding`.  -/
CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.EmbeddingRing : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type v} →
      [inst_1 : CategoryTheory.SmallCategory D] →
        CategoryTheory.Functor D Cᵒᵖ →
          [inst_2 : CategoryTheory.Abelian C] → [CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] → Type v
-- Mathlib.Data.FP.Basic
FP.FloatCfg.precMax : ∀ [self : FP.FloatCfg], FP.FloatCfg.prec ≤ FP.FloatCfg.emax
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.comap_inf_map_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F},
  Function.Injective ⇑f → ∀ (S T : Submonoid M), Submonoid.comap f (Submonoid.map f S ⊓ Submonoid.map f T) = S ⊓ T
-- Init.Tactics
/-- This is a "finishing" tactic modification of `simp`. It has two forms.

* `simpa [rules, ⋯] using e` will simplify the goal and the type of
  `e` using `rules`, then try to close the goal using `e`.

  Simplifying the type of `e` makes it more likely to match the goal
  (which has also been simplified). This construction also tends to be
  more robust under changes to the simp lemma set.

  The final match between the simplified `e` and the simplified goal uses
  **reducible** transparency, so it does not unfold semireducible definitions.
  Write `simpa [rules, ⋯] using! e` to perform the match at the ambient
  (default/semireducible) transparency instead.

* `simpa [rules, ⋯]` will simplify the goal and the type of a
  hypothesis `this` if present in the context, then try to close the goal using
  the `assumption` tactic.

As with `simp`, the `!` modifier after `simpa` enables auto-unfolding of
definitions in the simp set.
 -/
Lean.Parser.Tactic.tacticSimpa?!__1 : Lean.ParserDescr
-- Aesop.Frontend.Saturate
Aesop.Frontend.evalSaturateCore : Lean.Syntax →
  Option (Lean.TSyntax `num) →
    Option (Lean.TSyntax `Aesop.Frontend.Parser.additionalRules) →
      Option (Lean.TSyntax `Aesop.Frontend.Parser.usingRuleSets) → Bool → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.completeSpace_iff : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (h : α ≃ᵤ β),
  CompleteSpace α ↔ CompleteSpace β
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
/-- Given the set `i`, if `i` is not negative, `someExistsOneDivLT` chooses the set
`k` from `ExistsOneDivLT s i (findExistsOneDivLT s i)`, otherwise, it returns the
empty set.  -/
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.someExistsOneDivLT : {α : Type u_1} → [inst : MeasurableSpace α] → MeasureTheory.SignedMeasure α → Set α → Set α
-- Mathlib.Order.RelIso.Basic
RelEmbedding.prodLexMkLeft_apply : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} (s : β → β → Prop) {a : α} (h : ¬r a a) (snd : β),
  (RelEmbedding.prodLexMkLeft s h) snd = (a, snd)
-- Mathlib.Topology.Connected.TotallyDisconnected
Continuous.connectedComponentsLift_comp_coe : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f),
  h.connectedComponentsLift ∘ ConnectedComponents.mk = f
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileEvent.uri : Lean.Lsp.FileEvent → Lean.Lsp.DocumentUri
-- Mathlib.Topology.DiscreteSubset
Disjoint.eventually_nhdsWithin_specializes : ∀ {X : Type u_1} [inst : TopologicalSpace X] {p : X} {s : Set X},
  Disjoint (nhdsWithin p s) Filter.cofinite → ∀ᶠ (x : X) in nhdsWithin p s, x ⤳ p
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.div_apply : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : (i : ι) → Div (G i)] (f g : (i : ι) → G i) (i : ι), (f / g) i = f i / g i
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_seq_gen : {p : ℕ} →
  [inst : Fact (Nat.Prime p)] →
    {R : Type u_1} →
      [inst_1 : CommSemiring R] →
        [inst_2 : Algebra R ℤ_[p]] →
          {F : Polynomial R} →
            {a : ℤ_[p]} → ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 → ℕ → ℤ_[p]
-- Mathlib.Analysis.CStarAlgebra.Multiplier
/-- The normed group structure is inherited as the pullback under the ring monomorphism
`DoubleCentralizer.toProdMulOppositeHom : 𝓜(𝕜, A) →+* (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ`.  -/
DoubleCentralizer.instNormedRing : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → NormedRing (DoubleCentralizer 𝕜 A)
-- Mathlib.Tactic.NormNum.Irrational
Mathlib.Meta.NormNum.irrational_rpow_nat_rat : ∀ {x y : ℝ} {x_num y_num y_den k : ℕ},
  Mathlib.Meta.NormNum.IsNat x x_num →
    Mathlib.Meta.NormNum.IsNNRat y y_num y_den →
      y_num.Coprime y_den → k ^ y_den < x_num → x_num < (k + 1) ^ y_den → Irrational (x ^ y)
-- Mathlib.Algebra.Order.Group.PosPart
/-- The *positive part* of an element `a` in a lattice ordered group is `a ⊔ 1`, denoted `a⁺ᵐ`.  -/
instOneLePart : {α : Type u_1} → [Lattice α] → [DivInvMonoid α] → OneLePart α
-- Mathlib.Data.Nat.Factorial.Basic
Nat.descFactorial_le_pow : ∀ (n k : ℕ), n.descFactorial k ≤ n ^ k
-- Mathlib.LinearAlgebra.Matrix.Action
Matrix.instSMulCommClassMulOppositeForallOfIsScalarTower_1 : ∀ {n : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : DistribSMul S R] [IsScalarTower S R R], SMulCommClass S (Matrix n n R)ᵐᵒᵖ (n → R)
-- Mathlib.Data.Finset.Max
Finset.min'_insert : ∀ {α : Type u_2} [inst : LinearOrder α] (a : α) (s : Finset α) (H : s.Nonempty), (insert a s).min' ⋯ = min a (s.min' H)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.flipEquivalence_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Square.flipEquivalence.functor = CategoryTheory.Square.flipFunctor
-- Lean.Data.PersistentArray
Lean.PersistentArray.mapMAux : {α : Type u} →
  {m : Type u → Type v} →
    [Monad m] → {β : Type u} → (α → m β) → Lean.PersistentArrayNode α → m (Lean.PersistentArrayNode β)
-- Mathlib.Combinatorics.SetFamily.Compression.UV
UV.compress_of_disjoint_of_le' : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  {u v a : α}, Disjoint v a → u ≤ a → UV.compress u v ((a ⊔ v) \ u) = a
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.inhabitedCoconeMorphism.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (A : CategoryTheory.Limits.Cocone F),
  CategoryTheory.Limits.inhabitedCoconeMorphism A =
    { default := { hom := CategoryTheory.CategoryStruct.id A.pt, w := ⋯ } }
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Measurable.enorm : ∀ {β : Type u_2} {ε : Type u_5} [inst : MeasurableSpace ε] [inst_1 : TopologicalSpace ε] [inst_2 : ContinuousENorm ε]
  [OpensMeasurableSpace ε] [inst_4 : MeasurableSpace β] {f : β → ε}, Measurable f → Measurable fun x => ‖f x‖ₑ
-- Mathlib.Order.Lattice.Nat
Nat.instSupSet : SupSet ℕ
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.findCell_of_lt : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α → Ordering} [Std.Internal.IsCut compare k]
  {sz : ℕ} {k' : α} {v' : β k'} {l r : Std.DTreeMap.Internal.Impl α β},
  k k' = Ordering.lt →
    (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).Ordered →
      Std.DTreeMap.Internal.List.findCell (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).toListModel k =
        Std.DTreeMap.Internal.List.findCell l.toListModel k
-- Mathlib.InformationTheory.Hamming
Hamming.toHamming_sub : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : (i : ι) → Sub (β i)] {x y : (i : ι) → β i},
  Hamming.toHamming (x - y) = Hamming.toHamming x - Hamming.toHamming y
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_sup : ∀ {R : Type u} [inst : CommSemiring R] (I J : Ideal R),
  PrimeSpectrum.zeroLocus ↑(I ⊔ J) = PrimeSpectrum.zeroLocus ↑I ∩ PrimeSpectrum.zeroLocus ↑J
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.destruct_append : ∀ {α : Type u} (s t : Stream'.WSeq α), (s.append t).destruct = s.destruct.bind (Stream'.WSeq.destruct_append.aux t)
-- Mathlib.Tactic.DepRewrite
/-- Configuration.  -/
Mathlib.Tactic.DepRewrite.Context.cfg : Mathlib.Tactic.DepRewrite.Context → Mathlib.Tactic.DepRewrite.Config
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.instLawfulUpwardEnumerableLeast? : Std.PRange.LawfulUpwardEnumerableLeast? Int32
-- Mathlib.Algebra.Order.Star.Basic
/-- An alias of `IsSelfAdjoint.of_nonneg` for use with dot notation.  -/
LE.le.isSelfAdjoint : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {x : R}, 0 ≤ x → IsSelfAdjoint x
-- Mathlib.Algebra.Order.Sub.Defs
le_add_tsub' : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b : α}
  [AddLeftReflectLE α], a ≤ a + b - b
-- Mathlib.Order.Antichain
IsStrongAntichain.eq : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α},
  IsStrongAntichain r s → ∀ {a b c : α}, a ∈ s → b ∈ s → r a c → r b c → a = b
-- Mathlib.CategoryTheory.Subfunctor.Equalizer
CategoryTheory.Subfunctor.equalizer_eq_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)}
  {A : CategoryTheory.Subfunctor F₁} (f g : A.toFunctor ⟶ F₂), CategoryTheory.Subfunctor.equalizer f g = A ↔ f = g
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.union_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp}, t₁.union t₂ = t₁ ∪ t₂
-- Mathlib.Topology.ContinuousMap.Units
ContinuousMap.spectrum_eq_preimage_range : ∀ {X : Type u_1} {R : Type u_3} {𝕜 : Type u_4} [inst : TopologicalSpace X] [inst_1 : NormedField 𝕜]
  [inst_2 : NormedDivisionRing R] [inst_3 : Algebra 𝕜 R] [CompleteSpace R] (f : C(X, R)),
  spectrum 𝕜 f = ⇑(algebraMap 𝕜 R) ⁻¹' Set.range ⇑f
-- Mathlib.RingTheory.FreeRing
instRingFreeRing : (α : Type u_1) → Ring (FreeRing α)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Entrypoint.mk.sizeOf_spec : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] [inst_2 : SizeOf α] (aig : Std.Sat.AIG α) (ref : aig.Ref),
  sizeOf { aig := aig, ref := ref } = 1 + sizeOf aig + sizeOf ref
-- Mathlib.Order.Max
NoMaxOrder.mk : ∀ {α : Type u_3} [inst : LT α], (∀ (a : α), ∃ b, a < b) → NoMaxOrder α
-- Mathlib.Data.Multiset.Defs
Multiset.coe_reverse : ∀ {α : Type u_1} (l : List α), ↑l.reverse = ↑l
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Functor.mapCommMon_obj_mon_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.Functor C D) [inst_6 : F.LaxBraided] (A : CategoryTheory.CommMon C),
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map CategoryTheory.MonObj.one)
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app' : ∀ (R : Type u) [inst : CommRing R],
  (AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.counit.app (Opposite.op (CommRingCat.of R))).unop =
    CommRingCat.ofHom
      (algebraMap R
        ((AlgebraicGeometry.structureSheafInType ↑(Opposite.unop (Opposite.op (CommRingCat.of R)))
                ↑(Opposite.unop (Opposite.op (CommRingCat.of R)))).obj.obj
          (Opposite.op ⊤)))
-- Mathlib.Data.ZMod.QuotientGroup
MulAction.orbitZPowersEquiv_symm_apply' : ∀ {α : Type u_3} {β : Type u_4} [inst : Group α] (a : α) [inst_1 : MulAction α β] (b : β) (k : ℤ),
  (MulAction.orbitZPowersEquiv a b).symm ↑k = ⟨a, ⋯⟩ ^ k • ⟨b, ⋯⟩
-- Aesop.Search.Expansion.Norm
Aesop.NormRuleResult : Type
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.ι_totalShift₂Iso_inv_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)]
  (a b n : ℤ) (h : a + b = n) (b' n' : ℤ) (hb' : a + b' = n') (hn' : n' = n + y) {Z : C}
  (h_1 : (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).total (ComplexShape.up ℤ)).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.ιTotal (ComplexShape.up ℤ) a b' n' hb')
      (CategoryTheory.CategoryStruct.comp
        (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) y n n' hn').inv
        (CategoryTheory.CategoryStruct.comp ((K.totalShift₂Iso y).inv.f n) h_1)) =
    CategoryTheory.CategoryStruct.comp
      ((a * y).negOnePow •
        CategoryTheory.CategoryStruct.comp (K.shiftFunctor₂XXIso a b y b' ⋯).inv
          (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).ιTotal (ComplexShape.up ℤ) a b n h))
      h_1
-- Mathlib.MeasureTheory.Measure.Count
Function.Injective.map_count_le : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β},
  Function.Injective f →
    Measurable f → MeasureTheory.Measure.map f MeasureTheory.Measure.count ≤ MeasureTheory.Measure.count
-- Mathlib.Topology.Algebra.Group.Pointwise
mul_singleton_mem_nhds_of_nhds_one : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s : Set α} (a : α),
  s ∈ nhds 1 → s * {a} ∈ nhds a
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.JB.eq_1 : ∀ (l : Type u_4) (R : Type u₂) [inst : DecidableEq l] [inst_1 : CommRing R],
  LieAlgebra.Orthogonal.JB l R = Matrix.fromBlocks (2 • 1) 0 0 (LieAlgebra.Orthogonal.JD l R)
-- Mathlib.AlgebraicTopology.SingularHomology.Basic
/-- If `X` is totally disconnected,
its singular chain complex is given by `R[X] ←0- R[X] ←𝟙- R[X] ←0- R[X] ⋯`,
where `R[X]` is the coproduct of copies of `R` indexed by elements of `X`.  -/
AlgebraicTopology.singularChainComplexFunctorIsoOfTotallyDisconnectedSpace : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        (R : C) →
          (X : TopCat) →
            [TotallyDisconnectedSpace ↑X] →
              ((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj X ≅
                ChainComplex.alternatingConst.obj (∐ fun x => R)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_union : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_4} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [T2Space M] [inst_3 : ContinuousAdd M] {v : MeasureTheory.VectorMeasure α M} {s t : Set α},
  Disjoint s t → MeasurableSet s → MeasurableSet t → v.restrict (s ∪ t) = v.restrict s + v.restrict t
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- An n-ary version of `Set.mul_subset_mul`.  -/
Set.finsetProd_subset_finsetProd : ∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] (t : Finset ι) (f₁ f₂ : ι → Set α),
  (∀ i ∈ t, f₁ i ⊆ f₂ i) → ∏ i ∈ t, f₁ i ⊆ ∏ i ∈ t, f₂ i
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.reindex_comp_assoc : ∀ {n₁ n₂ n₃ : Type u} (i : n₁ ⟶ n₂) (j : n₂ ⟶ n₃) (S : AlgebraicGeometry.Scheme) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.AffineSpace n₁ S ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.AffineSpace.reindex
        (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp i j))) S)
      h =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.AffineSpace.reindex (⇑(CategoryTheory.ConcreteCategory.hom j)) S)
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.AffineSpace.reindex (⇑(CategoryTheory.ConcreteCategory.hom i)) S) h)