mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_alter!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.alter! k f t) = (f (t.get? k)).isSome
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_congr_measure_of_add_left : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C C' : ℝ} {μ' : MeasureTheory.Measure α}
  (hT_add : MeasureTheory.DominatedFinMeasAdditive (μ + μ') T C') (hT : MeasureTheory.DominatedFinMeasAdditive μ' T C)
  (f : α → E),
  MeasureTheory.Integrable f (μ + μ') → MeasureTheory.setToFun (μ + μ') T hT_add f = MeasureTheory.setToFun μ' T hT f
-- Std.Time.Time.Unit.Second
/-- `Offset` represents an offset in seconds. It is defined as an `Int`.
 -/
Std.Time.Second.Offset : Type
-- Mathlib.NumberTheory.LSeries.Basic
LSeries.term_delta : ∀ (s : ℂ) (n : ℕ), LSeries.term LSeries.delta s n = if n = 1 then 1 else 0
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get?_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₂ → (t₁ \ t₂).get? k = none
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.mul_X_modMonomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (x : MvPolynomial σ R) (i : σ),
  ((x * MvPolynomial.X i).modMonomial fun₀ | i => 1) = 0
-- Init.Data.SInt.Basic
/-- The smallest number that `Int64` can represent: `-2^63 = -9223372036854775808`.  -/
Int64.minValue : Int64
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
LocallyFiniteOrder.orderAddMonoidEquiv_apply : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedAddMonoid G]
  [inst_3 : LocallyFiniteOrder G] [inst_4 : Nontrivial G] (x : G),
  (LocallyFiniteOrder.orderAddMonoidEquiv G) x = (LocallyFiniteOrder.addMonoidHom G) x
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.MorApplication.underApplied.sizeOf_spec : sizeOf Mathlib.Meta.FunProp.MorApplication.underApplied = 1
-- Mathlib.Order.Monotone.Monovary
MonovaryOn.comp_monotoneOn_right : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder α] [inst_1 : LinearOrder β]
  [inst_2 : Preorder γ] {f : ι → α} {g : ι → β} {g' : β → γ} {s : Set ι},
  MonovaryOn f g s → MonotoneOn g' (g '' s) → MonovaryOn f (g' ∘ g) s
-- Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
/-- [Stacks Tag 00H5](https://stacks.math.columbia.edu/tag/00H5) -/
Polynomial.exists_monic_aeval_eq_zero_forall_mem_of_mem_map : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsIntegral R S] {I : Ideal R} {x : S},
  x ∈ Ideal.map (algebraMap R S) I →
    ∃ p, p.Monic ∧ (Polynomial.aeval x) p = 0 ∧ ∀ (i : ℕ), i ≠ p.natDegree → p.coeff i ∈ I
-- Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite
_private.Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite.0.step1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} {F : Type u_3}
  [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [inst_9 : TopologicalSpace F]
  [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] (u : E →L[𝕜] F) (A : Submodule 𝕜 E),
  IsClosed ↑A →
    ∀ [A_cofg : A.CoFG],
      Disjoint (↑u).ker A →
        (↑u).range = ⊤ →
          IsClosed ↑(↑(u.domRestrict A)).range → (Topology.IsStrictMap ⇑u ↔ Topology.IsStrictMap ⇑(u.domRestrict A))
-- Init.GrindInstances.Ring.SInt
Lean.Grind.instCommRingInt32 : Lean.Grind.CommRing Int32
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.domRestrict₂_def`. -/
Set.restrict₂_def : ∀ {α : Type u_1} {π : α → Type u_6} {s t : Set α} (hst : s ⊆ t), Set.domRestrict₂ hst = fun f x => f ⟨↑x, ⋯⟩
-- Mathlib.LinearAlgebra.Semisimple
Module.End.isSemisimple_restrict_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  (p : Submodule R M) (hp : p ∈ f.invtSubmodule),
  Module.End.IsSemisimple (LinearMap.restrict f hp) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p
-- Mathlib.CategoryTheory.Discrete.Basic
/-- A simple tactic to run `cases` on any `Discrete α` hypotheses.  -/
CategoryTheory.Discrete.tacticDiscrete_cases : Lean.ParserDescr
-- Mathlib.Data.List.Forall2
List.SublistForall₂.cons_right : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {a : β} {l₁ : List α} {l₂ : List β},
  List.SublistForall₂ R l₁ l₂ → List.SublistForall₂ R l₁ (a :: l₂)
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
/-- If a path `p` is Hamiltonian, then `p.getVert` defines an equivalence between
`Fin p.support.length` and `α`.  -/
SimpleGraph.Walk.IsHamiltonian.getVertEquiv : {α : Type u_1} →
  [inst : DecidableEq α] →
    {G : SimpleGraph α} → {a b : α} → {p : G.Walk a b} → p.IsHamiltonian → Fin p.support.length ≃ α
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- Definition of the logarithmic counting function, as a group morphism mapping functions `D` with
locally finite support to maps `ℝ → ℝ`.  Given `D`, the result map `logCounting D` takes `r : ℝ` to
a logarithmically weighted measure of values that `D` takes within the disk `∣z∣ ≤ r`.

Implementation Note: In case where `z = 0`, the term `log (r * ‖z‖⁻¹)` evaluates to zero, which is
typically different from `log r - log ‖z‖ = log r`. The summand `(D 0) * log r` compensates this,
producing cleaner formulas when the logarithmic counting function is used in the main theorems of
Value Distribution Theory.  We refer the reader to page 164 of [Lang: Introduction to Complex
Hyperbolic Spaces](https://link.springer.com/book/10.1007/978-1-4757-1945-1) for more details, and
to the lemma `countingFunction_finsum_eq_finsum_add` in
`Mathlib/Analysis/Complex/JensenFormula.lean` for a formal statement.
 -/
Function.locallyFinsuppWithin.logCounting : {E : Type u_2} → [inst : NormedAddCommGroup E] → [ProperSpace E] → Function.locallyFinsupp E ℤ →+ ℝ → ℝ
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.revMatchesAt_iff_splits : ∀ {c : Char} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.RevMatchesAt c pos ↔ ∃ t₁ t₂, pos.Splits (t₁ ++ String.singleton c) t₂
-- Mathlib.Order.Hom.Basic
map_inv_le_iff : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] [inst_2 : EquivLike F α β]
  [OrderIsoClass F α β] (f : F) {a : α} {b : β}, EquivLike.inv f b ≤ a ↔ b ≤ f a
-- Mathlib.NumberTheory.SmoothNumbers
Nat.equivProdNatFactoredNumbers_apply : ∀ {s : Finset ℕ} {p e m : ℕ} (hp : Nat.Prime p) (hs : p ∉ s) (hm : m ∈ Nat.factoredNumbers s),
  ↑((Nat.equivProdNatFactoredNumbers hp hs) (e, ⟨m, hm⟩)) = p ^ e * m
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_eq_contains_map_fst : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.containsKey k l = (List.map Sigma.fst l).contains k
-- Mathlib.Data.Multiset.Range
Multiset.range_zero : Multiset.range 0 = 0
-- Mathlib.NumberTheory.Chebyshev
/-- `ψ n` is the logarithm of `lcmUpto n`.  -/
Chebyshev.psi_eq_log_lcmUpto : ∀ (n : ℕ), Chebyshev.psi ↑n = Real.log ↑n.lcmUpto
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- We say that a set `H : Set (X → α)` of functions is equicontinuous at a point if the family
`(↑) : ↥H → (X → α)` is equicontinuous at that point.  -/
Set.EquicontinuousAt : {X : Type u_3} → {α : Type u_6} → [tX : TopologicalSpace X] → [uα : UniformSpace α] → Set (X → α) → X → Prop
-- Mathlib.NumberTheory.ModularForms.LFunction
ModularForm.weakFEPair.congr_simp : ∀ {Γ Γ_1 : Subgroup (GL (Fin 2) ℝ)} (e_Γ : Γ = Γ_1) [inst : Γ.IsArithmetic] {k k_1 : ℤ} (e_k : k = k_1) (hk : 0 < k)
  {F : Type u_1} [inst_1 : FunLike F UpperHalfPlane ℂ] (f f_1 : F),
  f = f_1 → ∀ [inst_2 : ModularFormClass F Γ k], ModularForm.weakFEPair hk f = ModularForm.weakFEPair ⋯ f_1
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_maxKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {he : l.isEmpty = false},
      Std.Internal.List.getKey? (Std.Internal.List.maxKey l he) l = some (Std.Internal.List.maxKey l he)
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.Quot_mk_eq_mk : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R]
  (I : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ),
  Quot.mk (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range)) I = (ClassGroup.mk (FractionRing R)) I
-- Init.Data.SInt.Lemmas
ISize.toNatClampNeg_ofIntClamp_of_lt_two_pow_numBits : ∀ {n : ℤ}, n < 2 ^ (System.Platform.numBits - 1) → (ISize.ofIntClamp n).toNatClampNeg = n.toNat
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.topMapₗ_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) (X : C),
  (CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.topMapₗ F).app X =
    F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.presentationOfIsCokernelFree_generators : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {ι σ : Type u} {M : SheafOfModules R}
  (f : SheafOfModules.free ι ⟶ SheafOfModules.free σ) (g : SheafOfModules.free σ ⟶ M)
  (H : CategoryTheory.CategoryStruct.comp f g = 0)
  (H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g H)),
  (SheafOfModules.presentationOfIsCokernelFree f g H H').generators = SheafOfModules.generatorsOfIsCokernelFree f g H H'
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
tsupport_iteratedFDeriv_subset : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  (n : ℕ), tsupport (iteratedFDeriv 𝕜 n f) ⊆ tsupport f
-- Lean.Data.Iterators.Producers.PersistentHashMap
Lean.PersistentHashMap.Zipper.prependNode : {α : Type u_1} →
  {β : Type u_2} →
    Lean.PersistentHashMap.Node α β → Lean.PersistentHashMap.Zipper α β → Lean.PersistentHashMap.Zipper α β
-- Mathlib.Data.WSeq.Basic
/-- auxiliary definition of drop over weak sequences  -/
Stream'.WSeq.drop.aux : {α : Type u} → ℕ → Option (α × Stream'.WSeq α) → Computation (Option (α × Stream'.WSeq α))
-- Mathlib.Topology.Algebra.Order.Archimedean
/-- An additive subgroup of an archimedean linear ordered additive commutative group
with order topology is dense provided that for all positive `ε` there exists a positive element of
the subgroup that is less than `ε`.  -/
AddSubgroup.dense_of_not_isolated_zero : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [inst_3 : TopologicalSpace G]
  [OrderTopology G] [Archimedean G] (S : AddSubgroup G), (∀ ε > 0, ∃ g ∈ S, g ∈ Set.Ioo 0 ε) → Dense ↑S
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.coe_copy : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (S : NonUnitalSubring R) (s : Set R) (hs : s = ↑S), ↑(S.copy s hs) = s
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The special case of the first cosimplicial identity  -/
CategoryTheory.CosimplicialObject.δ_comp_δ_self_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {i : Fin (n + 2)} {Z : C} (h : X.obj { len := n + 1 + 1 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.δ i) (CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) h) =
    CategoryTheory.CategoryStruct.comp (X.δ i) (CategoryTheory.CategoryStruct.comp (X.δ i.succ) h)
-- Mathlib.Algebra.Lie.Semisimple.Defs
LieAlgebra.IsSimple.eq_bot_or_eq_top : ∀ {R : Type u_1} {L : Type u_2} {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L}
  [self : LieAlgebra.IsSimple R L] (I : LieIdeal R L), I = ⊥ ∨ I = ⊤
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_hom_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : AlgebraicGeometry.PresheafedSpace C}
  (Y : AlgebraicGeometry.SheafedSpace C) (f : X ⟶ Y.toPresheafedSpace)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f],
  (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom Y f).hom.base = f.base
-- Init.Data.Vector.Lemmas
Vector.getElem_swap_right : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j : ℕ} (hi : i < n) (hj : j < n), (xs.swap i j hi hj)[j] = xs[i]
-- Lean.Level
/-- Return true if `u` and `v` denote the same level.
Check is currently incomplete.
 -/
Lean.Level.isEquiv : Lean.Level → Lean.Level → Bool
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsKolmogorovProcess.mk_of_secondCountableTopology : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {p q : ℝ} {M : NNReal} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst_2 : MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E],
  (∀ (s : T), Measurable (X s)) →
    (∀ (s t : T), ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ ↑M * edist s t ^ q) →
      0 < p → 0 < q → ProbabilityTheory.IsKolmogorovProcess X P p q M
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
/-- If `a.card = b.card + 1`, then the hypergeometric series has convergence radius greater or equal
to `1`.  -/
Complex.radius_regularizedHGFunSeries_ge_one : ∀ {a b : Multiset ℂ}, a.card = b.card + 1 → 1 ≤ (Complex.regularizedHGFunSeries a b).radius
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.exsphere_reindex : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {m n : ℕ} [inst_4 : NeZero m] [inst_5 : NeZero n] (s : Affine.Simplex ℝ P n)
  (e : Fin (n + 1) ≃ Fin (m + 1)) (signs : Finset (Fin (m + 1))),
  (s.reindex e).exsphere signs = s.exsphere (Finset.map e.symm.toEmbedding signs)
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.instIsPreorderQ : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] [inst_1 : LE α] [inst_2 : Std.IsPreorder α]
  [inst_3 : Lean.Grind.OrderedAdd α], Std.IsPreorder (Lean.Grind.IntModule.OfNatModule.Q α)
-- Mathlib.Order.Bounds.Basic
lowerBounds_insert : ∀ {α : Type u_1} [inst : Preorder α] (a : α) (s : Set α), lowerBounds (insert a s) = Set.Iic a ∩ lowerBounds s
-- Lean.Parser.Term
Lean.Parser.Termination.terminationBy?.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.instPreservesFiniteLimitsπ₁ : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteLimits C], CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.ShortComplex.π₁
-- Mathlib.Data.List.Map2
List.zipLeft'_nil_right : ∀ {α : Type u} {β : Type v} (as : List α), as.zipLeft' [] = (List.map (fun a => (a, none)) as, [])
-- Init.Data.Nat.Gcd
Nat.gcd_add_self_left : ∀ (m n : ℕ), (n + m).gcd m = n.gcd m
-- Std.Data.TreeMap.Lemmas
/-- Variant of `getElem!_map` that holds without `LawfulEqCmp`.  -/
Std.TreeMap.getElem!_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited γ] {f : α → β → γ} {k : α},
  (Std.TreeMap.map f t)[k]! = (Option.pmap (fun v h => f (t.getKey k h) v) t[k]? ⋯).get!
-- Mathlib.CategoryTheory.ObjectProperty.HasCardinalLT
CategoryTheory.ObjectProperty.HasCardinalLT.iSup : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {P : ι → CategoryTheory.ObjectProperty C}
  {κ : Cardinal.{w}} [Fact κ.IsRegular],
  (∀ (i : ι), (P i).HasCardinalLT κ) → HasCardinalLT ι κ → (⨆ i, P i).HasCardinalLT κ
-- Mathlib.Order.MinMax
MonotoneOn.map_max : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β} {s : Set α} {a b : α},
  MonotoneOn f s → a ∈ s → b ∈ s → f (max a b) = max (f a) (f b)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.BindStruct.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      {S : CategoryTheory.Presieve X} →
        {R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Presieve Y} →
          {Z : C} →
            {h : Z ⟶ X} →
              (Y : C) →
                (g : Z ⟶ Y) →
                  (f : Y ⟶ X) → (hf : S f) → R hf g → CategoryTheory.CategoryStruct.comp g f = h → S.BindStruct R h
-- Mathlib.Algebra.Quaternion
Quaternion.instInhabited : {R : Type u_3} → [inst : CommRing R] → Inhabited (Quaternion R)
-- Init.Data.Vector.Basic
/-- Push an element `x` to the end of a vector.  -/
Vector.push : {α : Type u_1} → {n : ℕ} → Vector α n → α → Vector α (n + 1)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.HasImageMap.comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g h : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom]
  [inst_3 : CategoryTheory.Limits.HasImage h.hom] (sq1 : f ⟶ g) (sq2 : g ⟶ h) [CategoryTheory.Limits.HasImageMap sq1]
  [CategoryTheory.Limits.HasImageMap sq2],
  CategoryTheory.Limits.HasImageMap (CategoryTheory.CategoryStruct.comp sq1 sq2)
-- Mathlib.Order.RelClasses
isWellOrder_lt : ∀ {α : Type u} [inst : LinearOrder α] [WellFoundedLT α], IsWellOrder α fun x1 x2 => x1 < x2
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_π_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasProduct I.left]
  [inst_2 : CategoryTheory.Limits.HasProduct I.right] (K : CategoryTheory.Limits.Multifork I)
  (X : CategoryTheory.Limits.WalkingParallelPair),
  (I.multiforkEquivPiFork.functor.obj K).π.app X =
    CategoryTheory.Limits.WalkingParallelPair.rec (motive := fun t =>
      X = t →
        (K.pt ⟶
          (CategoryTheory.Limits.parallelPair
                (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left))
                  (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))
                (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left))
                  (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))).obj
            X))
      (fun h =>
        ⋯ ▸
          CategoryTheory.Limits.Fan.IsLimit.lift
            (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.left)) K.ι)
      (fun h =>
        ⋯ ▸
          CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.Fan.IsLimit.lift
              (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.left)) K.ι)
            (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left))
              (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))))
      X ⋯
-- Mathlib.CategoryTheory.Functor.Basic
CategoryTheory.Functor.map_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v_1, u₁} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v_2, u₂} D] (F : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  {W : D} (h : F.obj Z ⟶ W),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (F.map g) h)
-- Mathlib.GroupTheory.Coxeter.Inversion
_private.Mathlib.GroupTheory.Coxeter.Inversion.0.CoxeterSystem.termLis_ : Lean.ParserDescr
-- Mathlib.Data.List.Sort
List.sortedGT_iff_pairwise : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedGT ↔ List.Pairwise (fun x1 x2 => x1 > x2) l
-- Mathlib.Analysis.Normed.Operator.NormedSpace
/-- Postcomposition with a linear isometry preserves the operator norm.  -/
ContinuousLinearMap.opNNNorm_linearIsometryEquiv_comp : ∀ {𝕜₁ : Type u_2} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_8}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜₁] [inst_4 : NormedSpace 𝕜₁ E] [inst_5 : NontriviallyNormedField 𝕜₂]
  [inst_6 : NormedSpace 𝕜₂ F] [inst_7 : NontriviallyNormedField 𝕜₃] [inst_8 : NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
  {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₃₂ : 𝕜₃ →+* 𝕜₂} [inst_9 : RingHomInvPair σ₂₃ σ₃₂] [inst_10 : RingHomInvPair σ₃₂ σ₂₃]
  {σ₁₃ : 𝕜₁ →+* 𝕜₃} [inst_11 : RingHomIsometric σ₁₃] [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
  [inst_13 : RingHomIsometric σ₁₂] (e : F ≃ₛₗᵢ[σ₂₃] G) (f : E →SL[σ₁₂] F), ‖↑↑e ∘SL f‖₊ = ‖f‖₊
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
/-- Auxiliary definition for `Enriched.FunctorCategory.isLimitConeFunctorEnrichedHom`.  -/
CategoryTheory.Enriched.FunctorCategory.isLimitConeFunctorEnrichedHom.lift : {V : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} C] →
          {J : Type u₃} →
            [inst_3 : CategoryTheory.Category.{v₃, u₃} J] →
              [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] →
                {F₁ F₂ : CategoryTheory.Functor J C} →
                  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂] →
                    [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] →
                      (s :
                          CategoryTheory.Limits.Cone
                            (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂)) →
                        s.pt ⟶ CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂
-- Mathlib.Data.Nat.Fib.Basic
Nat.fastFib.eq_1 : ∀ (n : ℕ), n.fastFib = n.fastFibAux.1
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
_private.Std.Tactic.BVDecide.LRAT.Internal.Clause.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.isUnit.match_1.eq_1 : ∀ {n : ℕ} (motive : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1)
  (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
  (h_1 : (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) → motive [l])
  (h_2 : (x : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) → motive x),
  (match [l] with
    | [l] => h_1 l
    | x => h_2 x) =
    h_1 l
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_eq_default : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : Inhabited α] [EquivBEq α] [LawfulHashable α]
  {a : α}, a ∉ m → m.get! a = default
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
CategoryTheory.MorphismProperty.instIsStableUnderCoproductsMonomorphismsOfAB4OfSize : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [CategoryTheory.AB4OfSize.{u', v, u} C],
  CategoryTheory.MorphismProperty.IsStableUnderCoproducts.{u', v, u} (CategoryTheory.MorphismProperty.monomorphisms C)