mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- `Finset α` is a division monoid under pointwise operations if `α` is.  -/
Finset.divisionMonoid : {α : Type u_2} → [DecidableEq α] → [DivisionMonoid α] → DivisionMonoid (Finset α)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotEquivQuotOfLE_quotQuotMk : ∀ {R : Type u} [inst : CommRing R] {I J : Ideal R} (x : R) (h : I ≤ J),
  (DoubleQuot.quotQuotEquivQuotOfLE h) ((DoubleQuot.quotQuotMk I J) x) = (Ideal.Quotient.mk J) x
-- Mathlib.Topology.Hom.Open
ContinuousOpenMap.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {g₁ g₂ : β →CO γ} {f : α →CO β},
  Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_range : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {E : Type u_3} [inst_2 : EquivLike E α β]
  [OrderIsoClass E α β] (e : E), (Set.range ⇑e).OrdConnected
-- Std.Data.DTreeMap.Internal.Model
/-- Model implementation of the `getEntry` function.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.getEntryₘ : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] → (l : Std.DTreeMap.Internal.Impl α β) → (k : α) → (l.getEntry?ₘ k).isSome = true → (a : α) × β a
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.ratio_zpow : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (e : X ≃ᵈ X) (n : ℤ), Dilation.ratio (e ^ n) = Dilation.ratio e ^ n
-- Mathlib.Topology.NhdsWithin
nhds_eq_nhdsWithin_sup_nhdsWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] (b : α) {I₁ I₂ : Set α},
  Set.univ = I₁ ∪ I₂ → nhds b = nhdsWithin b I₁ ⊔ nhdsWithin b I₂
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.SmallCategoryOfSet.mk.inj : ∀ {Ω : Type w} {obj : Set Ω} {hom : ↑obj → ↑obj → Set Ω} {id : (X : ↑obj) → ↑(hom X X)}
  {comp : {X Y Z : ↑obj} → ↑(hom X Y) → ↑(hom Y Z) → ↑(hom X Z)}
  {id_comp :
    autoParam (∀ {X Y : ↑obj} (f : ↑(hom X Y)), comp (id X) f = f) CategoryTheory.SmallCategoryOfSet.id_comp._autoParam}
  {comp_id :
    autoParam (∀ {X Y : ↑obj} (f : ↑(hom X Y)), comp f (id Y) = f) CategoryTheory.SmallCategoryOfSet.comp_id._autoParam}
  {assoc :
    autoParam
      (∀ {X Y Z T : ↑obj} (f : ↑(hom X Y)) (g : ↑(hom Y Z)) (h : ↑(hom Z T)), comp (comp f g) h = comp f (comp g h))
      CategoryTheory.SmallCategoryOfSet.assoc._autoParam}
  {obj_1 : Set Ω} {hom_1 : ↑obj_1 → ↑obj_1 → Set Ω} {id_1 : (X : ↑obj_1) → ↑(hom_1 X X)}
  {comp_1 : {X Y Z : ↑obj_1} → ↑(hom_1 X Y) → ↑(hom_1 Y Z) → ↑(hom_1 X Z)}
  {id_comp_1 :
    autoParam (∀ {X Y : ↑obj_1} (f : ↑(hom_1 X Y)), comp_1 (id_1 X) f = f)
      CategoryTheory.SmallCategoryOfSet.id_comp._autoParam}
  {comp_id_1 :
    autoParam (∀ {X Y : ↑obj_1} (f : ↑(hom_1 X Y)), comp_1 f (id_1 Y) = f)
      CategoryTheory.SmallCategoryOfSet.comp_id._autoParam}
  {assoc_1 :
    autoParam
      (∀ {X Y Z T : ↑obj_1} (f : ↑(hom_1 X Y)) (g : ↑(hom_1 Y Z)) (h : ↑(hom_1 Z T)),
        comp_1 (comp_1 f g) h = comp_1 f (comp_1 g h))
      CategoryTheory.SmallCategoryOfSet.assoc._autoParam},
  { obj := obj, hom := hom, id := id, comp := comp, id_comp := id_comp, comp_id := comp_id, assoc := assoc } =
      { obj := obj_1, hom := hom_1, id := id_1, comp := comp_1, id_comp := id_comp_1, comp_id := comp_id_1,
        assoc := assoc_1 } →
    obj = obj_1 ∧ hom ≍ hom_1 ∧ id ≍ id_1 ∧ comp ≍ comp_1
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearIsometryEquiv.conjStarAlgEquiv_refl : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {H : Type u_5} [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [inst_3 : CompleteSpace H], (LinearIsometryEquiv.refl 𝕜 H).conjStarAlgEquiv = StarAlgEquiv.refl 𝕜 (H →L[𝕜] H)
-- Mathlib.MeasureTheory.Covering.VitaliFamily
/-- Given a vitali family `v`, then `v.filterAt x` is the filter on `Set X` made of those families
that contain all sets of `v.setsAt x` of a sufficiently small diameter. This filter makes it
possible to express limiting behavior when sets in `v.setsAt x` shrink to `x`.  -/
VitaliFamily.filterAt : {X : Type u_1} →
  [inst : PseudoMetricSpace X] →
    {m0 : MeasurableSpace X} → {μ : MeasureTheory.Measure X} → VitaliFamily μ → X → Filter (Set X)
-- Lean.Log
/-- Log a named warning using the given message data. The position is provided by `getRef`.

Note: Use the macro `logNamedWarning`, which validates error names, instead of calling this function
directly.
 -/
Lean.logNamedWarning : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadLog m] → [Lean.AddMessageContext m] → [Lean.MonadOptions m] → Lean.Name → Lean.MessageData → m Unit
-- Mathlib.Probability.CDF
ProbabilityTheory.instIsProbabilityMeasurecdf : ∀ (μ : MeasureTheory.Measure ℝ), MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.cdf μ).measure
-- Mathlib.RingTheory.Valuation.Archimedean
MonoidWithZeroHom.instLinearOrderedCommGroupWithZeroMrange : {F : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : Field F] →
      [inst_1 : LinearOrderedCommGroupWithZero Γ₀] →
        (v : F →*₀ Γ₀) → LinearOrderedCommGroupWithZero ↥(MonoidHom.mrange v)
-- Mathlib.Data.Num.Bitwise
NzsNum.bit.sizeOf_spec : ∀ (a : Bool) (a_1 : NzsNum), sizeOf (NzsNum.bit a a_1) = 1 + sizeOf a + sizeOf a_1
-- Init.Data.Array.Count
Array.countP_toList : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, List.countP p xs.toList = Array.countP p xs
-- Mathlib.Data.Part
Part.some_ne_none : ∀ {α : Type u_1} (x : α), Part.some x ≠ Part.none
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.insertMany_append : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} {l₁ l₂ : List (α × β)},
  Std.DTreeMap.Raw.Const.insertMany t (l₁ ++ l₂) =
    Std.DTreeMap.Raw.Const.insertMany (Std.DTreeMap.Raw.Const.insertMany t l₁) l₂
-- Mathlib.Data.List.AList
AList.mem_replace : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a a' : α} {b : β a} {s : AList β},
  a' ∈ AList.replace a b s ↔ a' ∈ s
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.functorIsoMk_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J]
  (A B : CategoryTheory.Functor J (CategoryTheory.Pretriangulated.Triangle C))
  (iso₁ : A.comp CategoryTheory.Pretriangulated.Triangle.π₁ ≅ B.comp CategoryTheory.Pretriangulated.Triangle.π₁)
  (iso₂ : A.comp CategoryTheory.Pretriangulated.Triangle.π₂ ≅ B.comp CategoryTheory.Pretriangulated.Triangle.π₂)
  (iso₃ : A.comp CategoryTheory.Pretriangulated.Triangle.π₃ ≅ B.comp CategoryTheory.Pretriangulated.Triangle.π₃)
  (comm₁ :
    CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂) iso₂.hom =
      CategoryTheory.CategoryStruct.comp iso₁.hom (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂))
  (comm₂ :
    CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃) iso₃.hom =
      CategoryTheory.CategoryStruct.comp iso₂.hom (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃))
  (comm₃ :
    CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁)
        (CategoryTheory.Functor.whiskerRight iso₁.hom (CategoryTheory.shiftFunctor C 1)) =
      CategoryTheory.CategoryStruct.comp iso₃.hom (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁)),
  (CategoryTheory.Pretriangulated.Triangle.functorIsoMk A B iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).hom =
    CategoryTheory.Pretriangulated.Triangle.functorHomMk A B iso₁.hom iso₂.hom iso₃.hom comm₁ comm₂ comm₃
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.toList_filter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {f : (a : α) → β a → Bool},
  (↑(Std.DHashMap.Internal.Raw₀.filter f m)).toList.Perm (List.filter (fun p => f p.fst p.snd) (↑m).toList)
-- Init.Data.BitVec.Bitblast
/-- A lawful DivModState with a fully consumed dividend (`wn = 0`) witnesses that the
remainder has been correctly computed.
 -/
BitVec.DivModState.umod_eq_of_lawful : ∀ {w : ℕ} {n d : BitVec w} {qr : BitVec.DivModState w},
  BitVec.DivModState.Lawful { n := n, d := d } qr → qr.wn = 0 → n % d = qr.r
-- Mathlib.Analysis.Fourier.LpSpace
MeasureTheory.Lp.inner_fourier_eq : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [inst_2 : BorelSpace E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace ℂ F] [inst_5 : CompleteSpace F]
  [inst_6 : InnerProductSpace ℝ E] [inst_7 : FiniteDimensional ℝ E] (f : ↥(MeasureTheory.Lp F 2 MeasureTheory.volume))
  (g : ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)),
  inner ℂ (FourierTransform.fourier f) (FourierTransform.fourier g) = inner ℂ f g
-- Mathlib.Logic.Equiv.Set
Equiv.ofPreimageEquiv_map : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : α → γ} {g : β → γ} (e : (c : γ) → ↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c}))
  (a : α), g ((Equiv.ofPreimageEquiv e) a) = f a
-- Std.Data.TreeSet.Raw.Basic
/-- Tries to retrieve the smallest element of the tree set, returning `fallback` if the tree set is empty.
 -/
Std.TreeSet.Raw.minD : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → α → α
-- Mathlib.Topology.Metrizable.Basic
TopologicalSpace.pseudoMetrizableSpace_pi : ∀ {ι : Type u_1} {A : ι → Type u_4} [Finite ι] [inst : (i : ι) → TopologicalSpace (A i)]
  [∀ (i : ι), TopologicalSpace.PseudoMetrizableSpace (A i)], TopologicalSpace.PseudoMetrizableSpace ((i : ι) → A i)
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.instIsIsoFunctorHomₚ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} (f : HP ⟶ HP') [CategoryTheory.IsIso f]
  (i : ι), CategoryTheory.IsIso (f.homₚ i)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.instDecidablePredMemSetColorClassOfDecidableEq : {V : Type u} →
  {G : SimpleGraph V} →
    {α : Type u_2} → (C : G.Coloring α) → [DecidableEq α] → {c : α} → DecidablePred fun x => x ∈ C.colorClass c
-- Mathlib.Topology.Separation.Basic
R1Space.induced : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [R1Space X] (f : Y → X), R1Space Y
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_toList_iff_getKey?_eq_some_and_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (k, v) ∈ t.toList ↔ t.getKey? k = some k ∧ t[k]? = some v
-- Mathlib.Logic.OpClass
IsSymmOp.mk : ∀ {α : Sort u} {β : Sort v} {op : α → α → β}, (∀ (a b : α), op a b = op b a) → IsSymmOp op
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.instInhabitedSymbolPriorityEntry.default : Lean.Meta.Grind.SymbolPriorityEntry
-- Mathlib.Tactic.FunProp.Theorems
/-- Tag for one of the 5 basic lambda theorems, that also hold extra data for composition theorem
 -/
Mathlib.Meta.FunProp.LambdaTheoremArgs : Type
-- Init.Data.Option.Lemmas
Option.pbind_none' : ∀ {α : Type u_1} {x : Option α} {α_1 : Type u_2} {f : (a : α) → x = some a → Option α_1}, x = none → x.pbind f = none
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- An oriented angle in a right-angled triangle (even a degenerate one) has absolute value less
than `π / 2`. The right-angled property is expressed using unoriented angles to cover either
orientation of right-angled triangles and include degenerate cases.  -/
EuclideanGeometry.abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 → |(EuclideanGeometry.oangle p₂ p₃ p₁).toReal| < Real.pi / 2
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} [EquivBEq α] [LawfulHashable α]
  {l : List α},
  List.Pairwise (fun a b => (a == b) = false) l →
    (∀ a ∈ m, l.contains a = false) → (Std.DHashMap.Const.insertManyIfNewUnit m l).size = m.size + l.length
-- Mathlib.CategoryTheory.Limits.MonoCoprod
CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inl : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ ⊕ I₂ → C}
  (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl))
  (c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)) (hc : CategoryTheory.Limits.IsColimit c)
  (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hc₂ : CategoryTheory.Limits.IsColimit c₂)
  [CategoryTheory.Limits.MonoCoprod C],
  CategoryTheory.Mono (CategoryTheory.Limits.MonoCoprod.binaryCofanSum c c₁ c₂ hc₁ hc₂).inl
-- Mathlib.Order.CompleteLattice.Defs
/-- **Alias** of the forward direction of `isGLB_iff_sInf_eq`. -/
IsGLB.sInf_eq : ∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α}, IsGLB s a → sInf s = a
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.step.eq_2 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (tree : Std.DTreeMap.Internal.Impl α β)
  (next : Std.DTreeMap.Internal.Zipper α β),
  (Std.DTreeMap.Internal.Zipper.cons k v tree next).step =
    Std.IterStep.yield { internalState := Std.DTreeMap.Internal.Zipper.prependMap tree next } ⟨k, v⟩
-- Mathlib.RingTheory.Algebraic.Basic
Algebra.IsAlgebraic.tower_bot : ∀ (K : Type u_6) (L : Type u_7) (A : Type u_8) [inst : CommRing K] [inst_1 : Field L] [inst_2 : Ring A]
  [inst_3 : Algebra K L] [inst_4 : Algebra L A] [inst_5 : Algebra K A] [IsScalarTower K L A] [Nontrivial A]
  [Algebra.IsAlgebraic K A], Algebra.IsAlgebraic K L
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mk'.inj : ∀ {ι : Type u} {β : ι → Type v} {inst : (i : ι) → Zero (β i)} {toFun : (i : ι) → β i}
  {support' : Trunc { s // ∀ (i : ι), i ∈ s ∨ toFun i = 0 }} {toFun_1 : (i : ι) → β i}
  {support'_1 : Trunc { s // ∀ (i : ι), i ∈ s ∨ toFun_1 i = 0 }},
  { toFun := toFun, support' := support' } = { toFun := toFun_1, support' := support'_1 } →
    toFun = toFun_1 ∧ support' ≍ support'_1
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.separatingRight_toLinearMap₂'_of_det_ne_zero' : ∀ {R : Type u_1} {n : Type u_11} [inst : CommRing R] [inst_1 : DecidableEq n] [inst_2 : Fintype n] [IsDomain R]
  {M : Matrix n n R}, M.det ≠ 0 → ((Matrix.toLinearMap₂' R) M).SeparatingRight
-- Mathlib.Data.Sym.NatCard
Sym2.natCard_subtype_not_diag : ∀ (α : Type u_1), Nat.card { a // ¬a.IsDiag } = (Nat.card α).choose 2
-- Mathlib.MeasureTheory.Measure.Restrict
MeasurableEmbedding.comap_apply : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β},
  MeasurableEmbedding f → ∀ (μ : MeasureTheory.Measure β) (s : Set α), (MeasureTheory.Measure.comap f μ) s = μ (f '' s)
-- Init.Data.SInt.Basic
/-- Truncating division for word-sized signed integers, rounding towards zero. Usually accessed via the
`/` operator.

Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.

Examples:
* `ISize.div 10 3 = 3`
* `ISize.div 10 (-3) = (-3)`
* `ISize.div (-10) (-3) = 3`
* `ISize.div (-10) 3 = (-3)`
* `ISize.div 10 0 = 0`
 -/
ISize.div : ISize → ISize → ISize
-- Lean.Elab.InfoTree.Types
Lean.Elab.PartialContextInfo.autoImplicitCtx.inj : ∀ {autoImplicits autoImplicits_1 : Array Lean.Expr},
  Lean.Elab.PartialContextInfo.autoImplicitCtx autoImplicits =
      Lean.Elab.PartialContextInfo.autoImplicitCtx autoImplicits_1 →
    autoImplicits = autoImplicits_1
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.coe_prod : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7}
  [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1]
  [inst_4 : AddCommGroup V2] [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] [inst_7 : AddCommGroup V3]
  [inst_8 : Module k V3] [inst_9 : AddTorsor V3 P3] (f : P1 →ᵃ[k] P2) (g : P1 →ᵃ[k] P3),
  ⇑(f.prod g) = Function.prod ⇑f ⇑g
-- Init.Data.String.Bootstrap
/-- Variant of `getUTF8Byte` that takes the byte index as a `USize`, which avoids `Nat` boxing
in tight loops over the bytes of a string.
 -/
String.Internal.ugetUTF8Byte : (s : String) → (n : USize) → n.toNat < s.utf8ByteSize → UInt8
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.nthHom_zero : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {p : ℕ} (f : (k : ℕ) → R →+* ZMod (p ^ k)), PadicInt.nthHom f 0 = 0
-- Mathlib.Geometry.Convex.ConvexSpace.Module
Convexity.IsModuleConvexSpace.ofModule : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M], Convexity.IsModuleConvexSpace R M
-- Init.Data.String.Lemmas.Pattern.Memcmp
_private.Init.Data.String.Pattern.Basic.0.String.Slice.Pattern.Internal.memcmpStr.go.congr_simp : ∀ (lhs lhs_1 : String) (e_lhs : lhs = lhs_1) (rhs rhs_1 : String) (e_rhs : rhs = rhs_1)
  (lstart lstart_1 : String.Pos.Raw) (e_lstart : lstart = lstart_1) (rstart rstart_1 : String.Pos.Raw)
  (e_rstart : rstart = rstart_1) (len len_1 : String.Pos.Raw) (e_len : len = len_1)
  (h1 : len.offsetBy lstart ≤ lhs.rawEndPos) (h2 : len.offsetBy rstart ≤ rhs.rawEndPos) (curr curr_1 : String.Pos.Raw),
  curr = curr_1 →
    String.Slice.Pattern.Internal.memcmpStr.go✝ lhs rhs lstart rstart len h1 h2 curr =
      String.Slice.Pattern.Internal.memcmpStr.go✝ lhs_1 rhs_1 lstart_1 rstart_1 len_1 ⋯ ⋯ curr_1
-- Mathlib.GroupTheory.Perm.Sign
/-- set of all pairs (⟨a, b⟩ : Σ a : fin n, fin n) such that b < a  -/
Equiv.Perm.finPairsLT : (n : ℕ) → Finset ((_ : Fin n) × Fin n)
-- Mathlib.Data.Finset.NAry
Finset.image₂_curry : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] (f : α × β → γ) (s : Finset α) (t : Finset β),
  Finset.image₂ (Function.curry f) s t = Finset.image f (s ×ˢ t)
-- Mathlib.Data.Int.ModEq
Int.modEq_add_modulus_iff : ∀ {n a b : ℤ}, a ≡ b + n [ZMOD n] ↔ a ≡ b [ZMOD n]
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion.inj : ∀ {R : Type u_1} {inst : CommRing R} {inst_1 : IsDedekindDomain R} {K : Type u_2} {inst_2 : Field K}
  {inst_3 : Algebra R K} {inst_4 : IsFractionRing R K} {v : IsDedekindDomain.HeightOneSpectrum R}
  {toCompletion toCompletion_1 : (IsDedekindDomain.HeightOneSpectrum.valuation K v).Completion},
  { toCompletion := toCompletion } = { toCompletion := toCompletion_1 } → toCompletion = toCompletion_1
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.rightComm_symm : ∀ (R : Type uR) {S : Type uS} (B : Type uB) {M : Type uM} {P : Type uP} {Q : Type uQ} [inst : CommSemiring R]
  [inst_1 : Semiring B] [inst_2 : Algebra R B] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module B M]
  [inst_6 : IsScalarTower R B M] [inst_7 : AddCommMonoid P] [inst_8 : AddCommMonoid Q] [inst_9 : Module R Q]
  [inst_10 : CommSemiring S] [inst_11 : Module S M] [inst_12 : Module S P] [inst_13 : Algebra S B]
  [inst_14 : IsScalarTower S B M] [inst_15 : SMulCommClass R S M] [inst_16 : SMulCommClass S R M],
  (TensorProduct.AlgebraTensorModule.rightComm R S B M P Q).symm =
    TensorProduct.AlgebraTensorModule.rightComm S R B M Q P
-- Mathlib.Order.Copy
/-- A function to create a provable equal copy of a generalised heyting algebra
with possibly different definitional equalities.  -/
GeneralizedHeytingAlgebra.copy : {α : Type u} →
  (c : GeneralizedHeytingAlgebra α) →
    (le : α → α → Prop) →
      le = LE.le →
        (top : α) →
          top = ⊤ →
            (sup : α → α → α) →
              sup = max →
                (inf : α → α → α) → inf = min → (himp : α → α → α) → himp = HImp.himp → GeneralizedHeytingAlgebra α
-- Mathlib.Topology.Algebra.ConstMulAction
/-- Class `ContinuousConstSMul Γ T` says that the scalar multiplication `(•) : Γ → T → T`
is continuous in the second argument. We use the same class for all kinds of multiplicative
actions, including (semi)modules and algebras.

Note that both `ContinuousConstSMul α α` and `ContinuousConstSMul αᵐᵒᵖ α` are
weaker versions of `ContinuousMul α`.  -/
ContinuousConstSMul : (Γ : Type u_1) → (T : Type u_2) → [TopologicalSpace T] → [SMul Γ T] → Prop
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.instFaithfulSheafAddCommGrpCatToSheaf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat), (SheafOfModules.toSheaf R).Faithful
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Differentiable.arsinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ},
  Differentiable ℝ f → Differentiable ℝ fun x => Real.arsinh (f x)
-- Init.Data.UInt.Lemmas
UInt64.instIsLinearOrder : Std.IsLinearOrder UInt64
-- Mathlib.Order.SupClosed
isSublattice_iInter : ∀ {α : Type u_3} {ι : Sort u_5} [inst : Lattice α] {f : ι → Set α},
  (∀ (i : ι), IsSublattice (f i)) → IsSublattice (⋂ i, f i)
-- Mathlib.Analysis.InnerProductSpace.Dual
_private.Mathlib.Analysis.InnerProductSpace.Dual.0.InnerProductSpace.«term⟪_,_⟫» : Lean.ParserDescr
-- Lean.Expr
Lean.instReprMVarId : Repr Lean.MVarId
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instSubNegAddMonoidOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : SubNegMonoid Mᵃᵒᵖ], DomAddAct.instSubNegAddMonoidOfAddOpposite = inst
-- Mathlib.Topology.Semicontinuity.Defs
/-- A real function `f` is upper semicontinuous if, for any `ε > 0`, for any `x`, for all `x'`
close enough to `x`, then `f x'` is at most `f x + ε`. We formulate this in a general preordered
space, using an arbitrary `y > f x` instead of `f x + ε`.  -/
UpperSemicontinuous : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → [Preorder β] → (α → β) → Prop
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ_w_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)] (q₁ q₂ : ℕ) (hq : q₁ ≤ q₂) (i : ℤ),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ✝ f n₀ q₂).f i)
      (((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.functor✝ f n₀).map (CategoryTheory.homOfLE hq).op).hom.h.f
        i) =
    (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ✝ f n₀ q₁).f i
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
ContinuousMultilinearMap.integral_apply : ∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_6}
  [inst_1 : RCLike 𝕜] [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace ℝ E]
  {ι : Type u_8} [inst_5 : Fintype ι] {M : ι → Type u_9} [inst_6 : (i : ι) → NormedAddCommGroup (M i)]
  [inst_7 : (i : ι) → NormedSpace 𝕜 (M i)] {φ : X → ContinuousMultilinearMap 𝕜 M E},
  MeasureTheory.Integrable φ μ → ∀ (m : (i : ι) → M i), (∫ (x : X), φ x ∂μ) m = ∫ (x : X), (φ x) m ∂μ
-- Mathlib.Order.CompleteLattice.Defs
iInf_eq_bot : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLinearOrder α] {f : ι → α}, iInf f = ⊥ ↔ ∀ (b : α), ⊥ < b → ∃ i, f i < b
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.comap_lt_comap_of_integral_mem_sdiff : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {I J : Ideal S} [inst_2 : Algebra R S]
  [hI : I.IsPrime],
  I ≤ J → ∀ {x : S}, x ∈ ↑J \ ↑I → IsIntegral R x → Ideal.comap (algebraMap R S) I < Ideal.comap (algebraMap R S) J
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.length_zero : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α], NonemptyInterval.length 0 = 0