mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {k : α},
  k ∉ m₁ → Std.DHashMap.Const.get! (m₁.union m₂) k = Std.DHashMap.Const.get! m₂ k
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instCommSemiring : {R : Type u_1} →
  [inst : TopologicalSpace R] →
    [inst_1 : CommSemiring R] → [IsTopologicalSemiring R] → CommSemiring (SeparationQuotient R)
-- Init.Data.UInt.Bitwise
USize.or_comm : ∀ (a b : USize), a ||| b = b ||| a
-- Mathlib.RingTheory.Regular.RegularSequence
/-- The equivalence between M ⧸ (r₀, r₁, …, rₙ)M and (M ⧸ (r₁, …, rₙ)) ⧸ r₀ (M ⧸ (r₁, …, rₙ)).  -/
Submodule.quotOfListConsSMulTopEquivQuotSMulTopOuter : {R : Type u_1} →
  (M : Type u_3) →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (r : R) → (rs : List R) → (M ⧸ Ideal.ofList (r :: rs) • ⊤) ≃ₗ[R] QuotSMulTop r (M ⧸ Ideal.ofList rs • ⊤)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Stream.next?.eq_2 : ∀ {α : Type u_1} (v : α) (r : RBTree.RBNode α) (tail : RBTree.RBNode.Stream α),
  (RBTree.RBNode.Stream.cons v r tail).next? = some (v, r.toStream tail)
-- Mathlib.Data.Seq.Computation
Computation.destruct_eq_pure : ∀ {α : Type u} {s : Computation α} {a : α}, s.destruct = Sum.inl a → s = Computation.pure a
-- Mathlib.Data.Finmap
Finmap.lookup_isSome : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {s : Finmap β}, (Finmap.lookup a s).isSome = true ↔ a ∈ s
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
/-- Notation for `DayFunctor`.  -/
CategoryTheory.MonoidalCategory.DayFunctor.«term_⊛⥤_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.instIsClosedUnderLimitsOfShapeBotOfNonempty : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] [Nonempty J], ⊥.IsClosedUnderLimitsOfShape J
-- Aesop.Rule
Aesop.RegularRule : Type
-- Mathlib.Analysis.Analytic.CPolynomialDef
CPolynomialAt.continuousAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E},
  CPolynomialAt 𝕜 f x → ContinuousAt f x
-- Mathlib.Algebra.BigOperators.Ring.Finset
Nat.cast_multiset_prod : ∀ {R : Type u_4} [inst : CommSemiring R] (s : Multiset ℕ), ↑s.prod = (Multiset.map Nat.cast s).prod
-- Mathlib.SetTheory.Lists
Lists'.cons.eq_1 : ∀ {α : Type u_1} (x : Lists' α true) (fst : Bool) (a : Lists' α fst), Lists'.cons ⟨fst, a⟩ x = a.cons' x
-- Init.Data.Int.Order
Int.toNat_neg_natCast : ∀ (n : ℕ), (-↑n).toNat = 0
-- Mathlib.MeasureTheory.OuterMeasure.Induced
/-- We can trivially extend a function defined on a subclass of objects (with codomain `ℝ≥0∞`)
to all objects by defining it to be `∞` on the objects not in the class.  -/
MeasureTheory.extend : {α : Type u_2} → {P : α → Prop} → ((s : α) → P s → ENNReal) → α → ENNReal
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.whiskerRight_toNatTrans : ∀ {C D E : CategoryTheory.Cat} {F G : C ⟶ D} (H : D ⟶ E) (η : F ⟶ G),
  (CategoryTheory.Bicategory.whiskerRight η H).toNatTrans = CategoryTheory.Functor.whiskerRight η.toNatTrans H.toFunctor
-- Mathlib.Data.Seq.Basic
Stream'.Seq.drop_length' : ∀ {α : Type u} {n : ℕ} {s : Stream'.Seq α}, (s.drop n).length' = s.length' - ↑n
-- Mathlib.Algebra.Group.Basic
/-- Version of `add_left_iterate` that is fully applied, for `rw`.  -/
add_left_iterate_apply : ∀ {M : Type u_4} [inst : AddMonoid M] {n : ℕ} (a b : M), (fun x => a + x)^[n] b = n • a + b
-- Batteries.Data.List.Basic
/-- Auxiliary for `extractP`:
`extractP.go p l xs acc = (some a, acc.toList ++ out)` if `extractP p xs = (some a, out)`,
and `extractP.go p l xs acc = (none, l)` if `extractP p xs = (none, _)`.  -/
List.extractP.go : {α : Type u_1} → (α → Bool) → List α → List α → Array α → Option α × List α
-- Batteries.Lean.EStateM
EStateM.run'_orElse : ∀ {σ ε α δ : Type u_1} [h : EStateM.Backtrackable δ σ] (x₁ x₂ : EStateM ε σ α) (s : σ),
  (x₁ <|> x₂).run' s =
    match x₁.run s with
    | EStateM.Result.ok x a => some x
    | EStateM.Result.error a s' => x₂.run' (EStateM.Backtrackable.restore s' (EStateM.Backtrackable.save s))
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.IterM.step_flatMapAfterM.match_1.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it₁ : Std.IterM m β}
  (motive : it₁.Step → Sort u_3) (it₁' : Std.IterM m β) (b : β) (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' b))
  (h_1 :
    (it₁' : Std.IterM m β) →
      (b : β) → (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' b)) → motive ⟨Std.IterStep.yield it₁' b, h⟩)
  (h_2 :
    (it₁' : Std.IterM m β) → (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩)
  (h_3 : (h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it₁' b, h⟩ with
    | ⟨Std.IterStep.yield it₁' b, h⟩ => h_1 it₁' b h
    | ⟨Std.IterStep.skip it₁', h⟩ => h_2 it₁' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it₁' b h
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Polynomial.Chebyshev.integral_measureT_eq_integral_cos : ∀ {f : ℝ → ℝ}, ∫ (x : ℝ), f x ∂Polynomial.Chebyshev.measureT = ∫ (θ : ℝ) in 0..Real.pi, f (Real.cos θ)
-- Mathlib.LinearAlgebra.Dual.Defs
Module.Dual.instInhabited : (M : Type u_3) →
  [inst : AddCommMonoid M] →
    (R : Type u_4) → [inst_1 : Semiring R] → [inst_2 : Module R M] → Inhabited (Module.Dual R M)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_sub_pi_div_two : ∀ (x : ℝ), Real.cos (x - Real.pi / 2) = Real.sin x
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
quasispectrum.coe_zero : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalRing A] [inst_2 : Module R A]
  [inst_3 : Nontrivial R] (a : A), ↑0 = 0
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.mem_toList_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {k : α} {v : β},
      (k, v) ∈ Std.DHashMap.Raw.Const.toList ↑m ↔
        m.getKey? k = some k ∧ Std.DHashMap.Internal.Raw₀.Const.get? m k = some v
-- Lean.Elab.Arg
Lean.Elab.Term.Arg.expr.injEq : ∀ (val val_1 : Lean.Expr), (Lean.Elab.Term.Arg.expr val = Lean.Elab.Term.Arg.expr val_1) = (val = val_1)
-- Batteries.Data.String.Matcher
String.Matcher.mk.injEq : ∀ (toMatcher : Array.Matcher Char) (pattern : Substring.Raw) (toMatcher_1 : Array.Matcher Char)
  (pattern_1 : Substring.Raw),
  ({ toMatcher := toMatcher, pattern := pattern } = { toMatcher := toMatcher_1, pattern := pattern_1 }) =
    (toMatcher = toMatcher_1 ∧ pattern = pattern_1)
-- Mathlib.Topology.Constructions
Topology.IsEmbedding.inclusion : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X} (h : s ⊆ t), Topology.IsEmbedding (Set.inclusion h)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonTextDocumentPositionParams : Lean.ToJson Lean.Lsp.TextDocumentPositionParams
-- Init.Data.Nat.Internal.SOM
_private.Init.Data.Nat.Internal.SOM.0.Nat.Internal.SOM.Poly.add.go.match_1.eq_2 : ∀ (motive : Nat.Internal.SOM.Poly → Nat.Internal.SOM.Poly → Sort u_1) (p₂ : Nat.Internal.SOM.Poly)
  (h_1 : (p₁ : Nat.Internal.SOM.Poly) → motive p₁ []) (h_2 : (p₂ : Nat.Internal.SOM.Poly) → motive [] p₂)
  (h_3 :
    (k₁ : ℕ) →
      (m₁ : Nat.Internal.SOM.Mon) →
        (p₁ : List (ℕ × Nat.Internal.SOM.Mon)) →
          (k₂ : ℕ) →
            (m₂ : Nat.Internal.SOM.Mon) →
              (p₂ : List (ℕ × Nat.Internal.SOM.Mon)) → motive ((k₁, m₁) :: p₁) ((k₂, m₂) :: p₂)),
  (p₂ = [] → False) →
    (match [], p₂ with
      | p₁, [] => h_1 p₁
      | [], p₂ => h_2 p₂
      | (k₁, m₁) :: p₁, (k₂, m₂) :: p₂ => h_3 k₁ m₁ p₁ k₂ m₂ p₂) =
      h_2 p₂
-- Std.Data.DHashMap.RawLemmas
_private.Std.Data.DHashMap.RawLemmas.0.Std.DHashMap.Raw.isEmpty.eq_1 : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Raw α β), m.isEmpty = (m.size == 0)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.rpow_logb : ∀ {b x : ℝ}, 0 < b → b ≠ 1 → 0 < x → b ^ Real.logb b x = x
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.instAdditiveAdditiveFunctorFunctorForget : ∀ {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] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D], (CategoryTheory.AdditiveFunctor.forget C D).Additive
-- Mathlib.LinearAlgebra.SymplecticGroup
Matrix.J.congr_simp : ∀ (l : Type u_1) (R : Type u_2) {inst : DecidableEq l} [inst_1 : DecidableEq l] [inst_2 : CommRing R] (a a_1 : l ⊕ l),
  a = a_1 → ∀ (a_2 a_3 : l ⊕ l), a_2 = a_3 → Matrix.J l R a a_2 = Matrix.J l R a_1 a_3
-- Mathlib.SetTheory.Cardinal.EventuallyConst
Filter.EventuallyConst.of_monotone_of_lt_cof : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : PartialOrder β] {f : α → β},
  Monotone f →
    Cardinal.lift.{u, v} (Cardinal.mk β) < Cardinal.lift.{v, u} (Order.cof α) → Filter.EventuallyConst f Filter.atTop
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.Simps.symm_apply.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N), AddEquiv.Simps.symm_apply e = ⇑e.symm
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Naturality of the `coprodComparison` morphism in both arguments.  -/
CategoryTheory.Limits.coprodComparison_natural_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) {A A' B B' : C} [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct A' B']
  [inst_4 : CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)]
  [inst_5 : CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') {Z : D}
  (h : F.obj (A' ⨿ B') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprodComparison F A B)
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.coprod.map f g)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (F.map f) (F.map g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprodComparison F A' B') h)
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.exists_pow_nat_eq : ∀ {k : Type u} [inst : Field k] [IsAlgClosed k] (x : k) {n : ℕ}, 0 < n → ∃ z, z ^ n = x
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
Subsemigroup.centralizer_univ : ∀ (M : Type u_1) [inst : Semigroup M], Subsemigroup.centralizer Set.univ = Subsemigroup.center M
-- Mathlib.MeasureTheory.Covering.VitaliFamily
/-- A Vitali family for a measure `μ` is also a Vitali family for any measure absolutely continuous
with respect to `μ`.  -/
VitaliFamily.mono : {X : Type u_1} →
  [inst : PseudoMetricSpace X] →
    {m0 : MeasurableSpace X} →
      {μ : MeasureTheory.Measure X} →
        VitaliFamily μ → (ν : MeasureTheory.Measure X) → ν.AbsolutelyContinuous μ → VitaliFamily ν
-- Lean.Data.Lsp.Extra
Lean.Lsp.instBEqLeanFileProgressKind.beq : Lean.Lsp.LeanFileProgressKind → Lean.Lsp.LeanFileProgressKind → Bool
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.commute_id_right : ∀ {R : Type u_9} {M : Type u_10} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M),
  Commute f LinearMap.id
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.apply_symm_apply : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ) (v : W), φ (φ.symm v) = v
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.logSizeRadius.eq_1 : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] (t : T) (V : Finset T) (a c : ENNReal),
  PairReduction.logSizeRadius t V a c = if h : 1 < a then Nat.find ⋯ else 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.j_eq_zero_of_char_two : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : W.IsElliptic] [CharP R 2], W.a₁ = 0 → W.j = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.length_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.keys.length = t.size
-- Mathlib.RingTheory.Int.Basic
Int.eq_pow_of_mul_eq_pow_odd : ∀ {a b c : ℤ}, IsCoprime a b → ∀ {k : ℕ}, Odd k → a * b = c ^ k → (∃ d, a = d ^ k) ∧ ∃ e, b = e ^ k
-- Mathlib.NumberTheory.LSeries.PrimesInAP
/-- The auxiliary function takes real values for real arguments `x > 1`.  -/
ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux_real : ∀ {q : ℕ} {a : ZMod q} [inst : NeZero q],
  IsUnit a →
    ∀ {x : ℝ},
      1 < x →
        ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux a ↑x =
          ↑(ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux a ↑x).re
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndependent.pair_neg_left_iff : ∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M},
  LinearIndependent R ![-x, y] ↔ LinearIndependent R ![x, y]
-- Init.Data.UInt.Lemmas
USize.neg_add_mul_eq_mul_not : ∀ {a b : USize}, -(a + a * b) = a * ~~~b
-- Init.Data.UInt.Bitwise
UInt8.ofBitVec_or : ∀ (a b : BitVec 8), { toBitVec := a ||| b } = { toBitVec := a } ||| { toBitVec := b }
-- Init.Data.Vector.MapIdx
Vector.mapFinIdx_eq_replicate_iff : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : (i : ℕ) → α → i < n → β} {b : β},
  xs.mapFinIdx f = Vector.replicate n b ↔ ∀ (i : ℕ) (h : i < n), f i xs[i] h = b
-- Mathlib.Combinatorics.Matroid.Map
Matroid.mapSetEmbedding_indep_iff : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : ↑M.E ↪ β} {I : Set β},
  (M.mapSetEmbedding f).Indep I ↔ M.Indep (Subtype.val '' ⇑f ⁻¹' I) ∧ I ⊆ Set.range ⇑f
-- Init.Meta.Defs
/-- Finds the trailing size of the first `SourceInfo` from the back of `stx`.
If no `SourceInfo` can be found or the first `SourceInfo` from the back of `stx` contains no
trailing whitespace, the result is `0`.
 -/
Lean.Syntax.getTrailingSize : Lean.Syntax → ℕ
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- A family `𝓕 : ι → X → α` is equicontinuous on `S` iff the function `swap 𝓕 : X → ι → α` is
continuous on `S` *when `ι → α` is equipped with the topology of uniform convergence*. This is
very useful for developing the equicontinuity API, but it should not be used directly for other
purposes.  -/
equicontinuousOn_iff_continuousOn : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α}
  {S : Set X}, EquicontinuousOn F S ↔ ContinuousOn (⇑UniformFun.ofFun ∘ Function.swap F) S
-- Mathlib.Data.EReal.Basic
EReal.natCast_ne_bot : ∀ (n : ℕ), ↑n ≠ ⊥
-- Mathlib.Algebra.Divisibility.Basic
mul_rightDvd_mul_iff_left : ∀ {α : Type u_1} [inst : RightCancelSemigroup α] {a b c : α}, b * a ∣ᵣ c * a ↔ b ∣ᵣ c
-- Mathlib.Computability.Encoding
Computability.Encoding.mk.injEq : ∀ {α : Type u} {Γ : Type v} (encode : α → List Γ) (decode : List Γ → Option α)
  (decode_encode : ∀ (x : α), decode (encode x) = some x) (encode_1 : α → List Γ) (decode_1 : List Γ → Option α)
  (decode_encode_1 : ∀ (x : α), decode_1 (encode_1 x) = some x),
  ({ encode := encode, decode := decode, decode_encode := decode_encode } =
      { encode := encode_1, decode := decode_1, decode_encode := decode_encode_1 }) =
    (encode = encode_1 ∧ decode = decode_1)
-- Mathlib.Data.Setoid.Partition
/-- Constructive information associated with a partition of a type `α` indexed by another type `ι`,
`s : ι → Set α`.

`IndexedPartition.index` sends an element to its index, while `IndexedPartition.some` sends
an index to an element of the corresponding set.

This type is primarily useful for definitional control of `s` - if this is not needed, then
`Setoid.ker index` by itself may be sufficient.  -/
IndexedPartition : {ι : Type u_1} → {α : Type u_2} → (ι → Set α) → Type (max u_1 u_2)
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.sheafifyMap_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D),
  J.sheafifyMap (CategoryTheory.CategoryStruct.id P) = CategoryTheory.CategoryStruct.id (J.sheafify P)
-- Init.Data.Float.Float
/-- Compares two floating point numbers for strict inequality.

This function does not reduce in the kernel. It is compiled to the C inequality operator.
 -/
Float.decLt : (a b : Float) → Decidable (a < b)
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.mem_ordConnectedComponent_comm : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x y : α},
  y ∈ s.ordConnectedComponent x ↔ x ∈ s.ordConnectedComponent y
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.isInitialMul_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasStrictInitialObjects C]
  {I : C} (X : C) [inst_2 : CategoryTheory.Limits.HasBinaryProduct I X] (hI : CategoryTheory.Limits.IsInitial I),
  (CategoryTheory.Limits.isInitialMul X hI).hom = CategoryTheory.Limits.prod.fst
-- Mathlib.Order.Hom.Lattice
LatticeHom.instInhabited : (α : Type u_2) → [inst : Lattice α] → Inhabited (LatticeHom α α)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
CategoryTheory.IsPushout.hasPushout_biprod_fst_biprod_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.Limits.HasPushout CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- If some predicate holds for all `x ∈ (s : Set A)` and this predicate is closed under the
`algebraMap`, addition, multiplication and star operations, then it holds for `a ∈ adjoin R s`.  -/
NonUnitalAlgebra.adjoin_induction : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {s : Set A}
  {p : (x : A) → x ∈ NonUnitalAlgebra.adjoin R s → Prop},
  (∀ (x : A) (hx : x ∈ s), p x ⋯) →
    (∀ (x y : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s),
        p x hx → p y hy → p (x + y) ⋯) →
      p 0 ⋯ →
        (∀ (x y : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s),
            p x hx → p y hy → p (x * y) ⋯) →
          (∀ (r : R) (x : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s), p x hx → p (r • x) ⋯) →
            ∀ {x : A} (hx : x ∈ NonUnitalAlgebra.adjoin R s), p x hx
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.smul_integral_comp_mul_sub : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} (f : ℝ → E) (c d : ℝ),
  c • ∫ (x : ℝ) in a..b, f (c * x - d) = ∫ (x : ℝ) in c * a - d..c * b - d, f x
-- Init.Data.Range.Polymorphic.UInt
UInt8.succMany?_ofBitVec : ∀ {k : ℕ} {x : BitVec 8}, Std.PRange.succMany? k { toBitVec := x } = UInt8.ofBitVec <$> Std.PRange.succMany? k x
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_inter_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ ∩ m₂)[k]! = default
-- Mathlib.Topology.UniformSpace.Basic
instUniformSpaceMultiplicative : {α : Type ua} → [UniformSpace α] → UniformSpace (Multiplicative α)
-- Mathlib.GroupTheory.Sylow
Sylow.conj_eq_normalizer_conj_of_mem_centralizer : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) (x g : G),
  x ∈ Subgroup.centralizer ↑P →
    g⁻¹ * x * g ∈ Subgroup.centralizer ↑P → ∃ n ∈ Subgroup.normalizer ↑P, g⁻¹ * x * g = n⁻¹ * x * n
-- Mathlib.RingTheory.Bialgebra.Quotient
Bialgebra.Quotient.counitAlgHom.congr_simp : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Bialgebra R A] (I : Ideal A)
  [inst_3 : I.IsTwoSided] [inst_4 : (Submodule.restrictScalars R I).IsCoideal],
  Bialgebra.Quotient.counitAlgHom I = Bialgebra.Quotient.counitAlgHom I
-- Mathlib.Logic.Small.Basic
small_subtype : ∀ (α : Type v) [Small.{w, v} α] (P : α → Prop), Small.{w, v} { x // P x }
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singletonMulHom_apply : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] (a : α), Finset.singletonMulHom a = {a}
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.unique : {ι : Type v} →
  {β : ι → Type w} →
    [inst : (i : ι) → AddCommMonoid (β i)] → [∀ (i : ι), Subsingleton (β i)] → Unique (DirectSum ι fun i => β i)
-- Mathlib.Analysis.Matrix.Order
/-- For `A` positive semidefinite, we have `x⋆ A x = 0` iff `A x = 0`.  -/
Matrix.PosSemidef.dotProduct_mulVec_zero_iff : ∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] {A : Matrix n n 𝕜},
  A.PosSemidef → ∀ (x : n → 𝕜), star x ⬝ᵥ A.mulVec x = 0 ↔ A.mulVec x = 0
-- Std.Data.DTreeMap.Internal.Operations
/-- Iterate over `l` and insert all of its elements into `t`.  -/
Std.DTreeMap.Internal.Impl.Const.insertMany : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      {ρ : Type w} →
        [ForIn Id ρ (α × β)] →
          (t : Std.DTreeMap.Internal.Impl α fun x => β) →
            ρ → t.Balanced → Std.DTreeMap.Internal.Impl.Const.IteratedInsertionInto t
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
/-- `Multiset.sum`, the sum of the elements of a multiset, promoted to a morphism of
`AddCommMonoid`s.  -/
Multiset.sumAddMonoidHom : {M : Type u_5} → [inst : AddCommMonoid M] → Multiset M →+ M
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_mul : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u v : ι → Ω → β} {τ : Ω → WithTop ι}
  [inst_1 : LinearOrder ι] [inst_2 : Mul β],
  MeasureTheory.stoppedProcess (u * v) τ = MeasureTheory.stoppedProcess u τ * MeasureTheory.stoppedProcess v τ
-- Init.Data.String.Termination
String.Slice.Pos.lt_next_next : ∀ {s : String.Slice} {p : s.Pos} {h : p ≠ s.endPos} {h' : p.next h ≠ s.endPos}, p < (p.next h).next h'
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mkPostcomp_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {Y Y' : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y) (g : Y ⟶ Y'),
  (CategoryTheory.StructuredArrow.mkPostcomp f g).left =
    CategoryTheory.CategoryStruct.id (CategoryTheory.StructuredArrow.mk f).left
-- Mathlib.Algebra.Homology.Precylinder
/-- The precylinder object of a homological complex that is given by
`HomologicalComplex.cylinder`.  -/
HomologicalComplex.precylinder : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          [DecidableRel c.Rel] →
            (K : HomologicalComplex C c) →
              [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] →
                [K.HasCylinder] → HomotopicalAlgebra.Precylinder K