mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Divisibility.Units
IsRelPrime.mul_right : ∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α} [DecompositionMonoid α],
  IsRelPrime x y → IsRelPrime x z → IsRelPrime x (y * z)
-- Mathlib.RingTheory.Valuation.Basic
/-- The subgroup of elements whose valuation is less than a certain unit.  -/
Valuation.ltAddSubgroup : {R : Type u_3} →
  {Γ₀ : Type u_4} →
    [inst : Ring R] → [inst_1 : LinearOrderedCommGroupWithZero Γ₀] → Valuation R Γ₀ → Γ₀ˣ → AddSubgroup R
-- Mathlib.Analysis.Calculus.TangentCone.Defs
/-- Let `c n` be a family of scalars, `d n` be a family of vectors, and `l` be a filter such that

- `d n → 0` along `l`;
- `x + d n ∈ s` frequently along `l`;
- `c n • d n → y` along `l`.

Then `y` belongs to the tangent cone of `s` at `x`.
See also

- `mem_tangentConeAt_of_seq` for a version assuming that `x + d n ∈ s` eventually along `l`.
- `exists_fun_of_mem_tangentConeAt` for the other implication.
 -/
mem_tangentConeAt_of_frequently : ∀ {R : Type u} {E : Type v} [inst : AddCommGroup E] [inst_1 : SMul R E] [inst_2 : TopologicalSpace E] {s : Set E}
  {x y : E} {α : Type u_1} (l : Filter α) (c : α → R) (d : α → E),
  Filter.Tendsto d l (nhds 0) →
    (∃ᶠ (n : α) in l, x + d n ∈ s) → Filter.Tendsto (fun n => c n • d n) l (nhds y) → y ∈ tangentConeAt R s x
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.ofNat_mul_continuum : ∀ {n : ℕ} [inst : n.AtLeastTwo], OfNat.ofNat n * Cardinal.continuum = Cardinal.continuum
-- Mathlib.RingTheory.Congruence.Defs
RingCon.mk'_surjective : ∀ {R : Type u_1} [inst : NonAssocSemiring R] (c : RingCon R), Function.Surjective ⇑c.mk'
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
NNReal.closedBall_zero_eq_Icc : ∀ {c : ℝ}, 0 ≤ c → Metric.closedBall 0 c = Set.Icc 0 c.toNNReal
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSet_precomp_of_bijective : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {s : ι → Set Ω} {ι' : Type u_5} {g : ι' → ι},
  Function.Bijective g → (ProbabilityTheory.Kernel.iIndepSet (s ∘ g) κ μ ↔ ProbabilityTheory.Kernel.iIndepSet s κ μ)
-- Mathlib.Order.Filter.Finite
Filter.eventually_all_finite : ∀ {α : Type u} {ι : Type u_2} {I : Set ι},
  I.Finite → ∀ {l : Filter α} {p : ι → α → Prop}, (∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x
-- Lean.Parser.Extra
Lean.Parser.sepBy1.parenthesizer : Lean.PrettyPrinter.Parenthesizer →
  String → Lean.PrettyPrinter.Parenthesizer → optParam Bool false → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.zero_smul : ∀ {α : Type u_1} [inst : AddCommMonoid α] (c : ℕ), Mathlib.Tactic.Abel.smul c 0 = 0
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_sInf' : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [inst_3 : RingHomClass F R S] (s : Set (Ideal S)), Ideal.comap f (sInf s) = ⨅ I ∈ Ideal.comap f '' s, I
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pushout.map_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.Limits.pushout.map f g f g (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z)
      (CategoryTheory.CategoryStruct.id X) ⋯ ⋯ =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pushout f g)
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- The `S`-`finrank` of `M ⊗[R] M'` is `(finrank S M) * (finrank R M')`.  -/
Module.finrank_tensorProduct : ∀ {R : Type u} {S : Type u'} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M] [StrongRankCondition R]
  [StrongRankCondition S] [inst_7 : Module S M] [inst_8 : Module S M'] [Module.Free S M'] [inst_10 : Algebra S R]
  [inst_11 : IsScalarTower S R M] [Module.Free R M],
  Module.finrank R (TensorProduct S M M') = Module.finrank R M * Module.finrank S M'
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.pairingIn_rat : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [Nontrivial R]
  [inst_6 : P.IsCrystallographic] [inst_7 : Algebra ℚ R] (i j : ι), P.pairingIn ℚ i j = ↑(P.pairingIn ℤ i j)
-- Mathlib.MeasureTheory.Function.L2Space
integral_eq_zero_of_forall_integral_inner_eq_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} (𝕜 : Type u_3) [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [CompleteSpace E] [inst_4 : NormedSpace ℝ E]
  (f : α → E), MeasureTheory.Integrable f μ → (∀ (c : E), ∫ (x : α), inner 𝕜 c (f x) ∂μ = 0) → ∫ (x : α), f x ∂μ = 0
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get!_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  [inst_1 : Inhabited β], (t₁ \ t₂).get! k = if k ∈ t₂ then default else t₁.get! k
-- Init.Data.Option.Lemmas
Option.isSome_map : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1} {x : Option α}, (Option.map f x).isSome = x.isSome
-- Mathlib.Analysis.RCLike.Basic
RCLike.toIsStrictOrderedModule : ∀ {K : Type u_1} [inst : RCLike K], IsStrictOrderedModule ℝ K
-- Mathlib.SetTheory.ZFC.PSet
PSet.equiv_iff_mem : ∀ {x y : PSet.{u}}, x.Equiv y ↔ ∀ {w : PSet.{u}}, w ∈ x ↔ w ∈ y
-- Mathlib.CategoryTheory.Limits.VanKampen
/-- A (colimit) cocone over a diagram `F : J ⥤ C` is universal if it is stable under pullbacks.  -/
CategoryTheory.IsUniversalColimit : {J : Type v'} →
  [inst : CategoryTheory.Category.{u', v'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} → CategoryTheory.Limits.Cocone F → Prop
-- Mathlib.CategoryTheory.Functor.TwoSquare
CategoryTheory.TwoSquare.vId_app : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] (T : CategoryTheory.Functor C₁ C₂) (X : C₁),
  (CategoryTheory.TwoSquare.vId T).app X = CategoryTheory.CategoryStruct.id (T.obj X)
-- Mathlib.Topology.VectorBundle.Basic
VectorPrebundle.continuous_totalSpaceMk : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : (x : B) → TopologicalSpace (E x)]
  (a : VectorPrebundle R F E) (b : B), Continuous (Bundle.TotalSpace.mk b)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformOnFun.continuous_rng_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] {𝔖 : Set (Set α)} {X : Type u_5} [inst_1 : TopologicalSpace X]
  {f : X → UniformOnFun α β 𝔖},
  Continuous f ↔ ∀ s ∈ 𝔖, Continuous (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖) ∘ f)
-- Mathlib.RingTheory.Polynomial.Pochhammer
descPochhammer_ne_zero_eval_zero : ∀ (R : Type u) [inst : Ring R] {n : ℕ}, n ≠ 0 → Polynomial.eval 0 (descPochhammer R n) = 0
-- Mathlib.Tactic.Abel
/-- Populate a `context` object for evaluating `e`.  -/
Mathlib.Tactic.Abel.mkContext : Lean.Expr → Lean.MetaM Mathlib.Tactic.Abel.Context
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.Adhesive.isPullback_of_isPushout_of_mono_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  [CategoryTheory.Adhesive C],
  CategoryTheory.IsPushout f g h i → ∀ [CategoryTheory.Mono g], CategoryTheory.IsPullback f g h i
-- Mathlib.Analysis.Distribution.FourierMultiplier
TemperedDistribution.fourierMultiplierCLM_apply_apply : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : NormedSpace ℂ F] [inst_4 : FiniteDimensional ℝ E]
  [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E] (g : E → ℂ) (f : TemperedDistribution E F) (u : SchwartzMap E ℂ),
  ((TemperedDistribution.fourierMultiplierCLM F g) f) u =
    f (FourierTransform.fourier ((SchwartzMap.smulLeftCLM ℂ g) (FourierTransformInv.fourierInv u)))
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.ofQuotientStabilizer.eq_1 : ∀ (G : Type u) {X : Type v} [inst : AddGroup G] [inst_1 : AddAction G X] (x : X) (g : G ⧸ AddAction.stabilizer G x),
  AddAction.ofQuotientStabilizer G x g = Quotient.liftOn' g (fun x_1 => x_1 +ᵥ x) ⋯
-- Mathlib.Topology.UniformSpace.CompactConvergence
/-- Convergence in the compact-open topology is the same as uniform convergence for sequences of
continuous functions on a compact space.  -/
ContinuousMap.tendsto_iff_tendstoUniformly : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {f : C(α, β)} {ι : Type u₃}
  {p : Filter ι} {F : ι → C(α, β)} [CompactSpace α],
  Filter.Tendsto F p (nhds f) ↔ TendstoUniformly (fun i a => (F i) a) (⇑f) p
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.closure_prod : ∀ {N : Type u_2} [inst : MulOneClass N] {M : Type u_5} [inst_1 : MulOneClass M] {s : Set M} {t : Set N},
  1 ∈ s → 1 ∈ t → Submonoid.closure (s ×ˢ t) = (Submonoid.closure s).prod (Submonoid.closure t)
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
CategoryTheory.Abelian.LeftResolution.karoubi.π'.congr_simp : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive A] [inst_4 : ι.Additive],
  CategoryTheory.Abelian.LeftResolution.karoubi.π' Λ = CategoryTheory.Abelian.LeftResolution.karoubi.π' Λ
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The weights for the Monge point of an (n+2)-simplex, minus the
centroid of an n-dimensional face, in terms of
`pointsWithCircumcenter`.  This definition is only valid when `i₁ ≠ i₂`.  -/
Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter : {n : ℕ} → Fin (n + 3) → Fin (n + 3) → Affine.Simplex.PointsWithCircumcenterIndex (n + 2) → ℝ
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.instRespectsIsoSchemeTopologicallyInjective : (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Function.Injective).RespectsIso
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset_univ : ∀ {α : Type u} [inst : Fintype α] (h : Set.univ.Finite), h.toFinset = Finset.univ
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.mk : {X : AlgebraicGeometry.Scheme} →
  (ideal : (U : ↑X.affineOpens) → Ideal ↑(X.presheaf.obj (Opposite.op ↑U))) →
    (∀ (U : ↑X.affineOpens) (f : ↑(X.presheaf.obj (Opposite.op ↑U))),
        Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (ideal U) =
          ideal (X.affineBasicOpen f)) →
      (supportSet : Set ↥X) →
        autoParam (supportSet = ⋂ U, X.zeroLocus ↑(ideal U))
            AlgebraicGeometry.Scheme.IdealSheafData.supportSet_eq_iInter_zeroLocus._autoParam →
          X.IdealSheafData
-- Mathlib.Algebra.Polynomial.Div
/-- The multiplicity of `a` as root of a nonzero polynomial `p` is at least `n` iff
`(X - a) ^ n` divides `p`.  -/
Polynomial.le_rootMultiplicity_iff : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R},
  p ≠ 0 → ∀ {a : R} {n : ℕ}, n ≤ Polynomial.rootMultiplicity a p ↔ (Polynomial.X - Polynomial.C a) ^ n ∣ p
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
/-- If `ξ` is an integer, all its convergents equal `ξ`.  -/
Real.convergent_of_int : ∀ {ξ : ℤ} (n : ℕ), (↑ξ).convergent n = ↑ξ
-- Mathlib.NumberTheory.Bernoulli
bernoulli_spec' : ∀ (n : ℕ),
  ∑ k ∈ Finset.HasAntidiagonal.antidiagonal n, ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli k.1 =
    if n = 0 then 1 else 0
-- Init.Data.String.Slice
/-- Splits a slice at each subslice that matches the pattern `pat`.

The subslices that matched the pattern are not included in any of the resulting subslices. If
multiple subslices in a row match the pattern, the resulting list will contain empty strings.

This function is generic over all currently supported patterns.

Examples:

* `("coffee tea water".toSlice.split Char.isWhitespace).toStringList == ["coffee", "tea", "water"]`

* `("coffee tea water".toSlice.split ' ').toStringList == ["coffee", "tea", "water"]`

* `("coffee tea water".toSlice.split " tea ").toStringList == ["coffee", "water"]`

* `("ababababa".toSlice.split "aba").toStringList == ["coffee", "water"]`

* `("baaab".toSlice.split "aa").toStringList == ["b", "ab"]`
 -/
String.Slice.split : {ρ : Type} →
  {σ : String.Slice → Type} →
    [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      (s : String.Slice) → (pat : ρ) → [inst : String.Slice.Pattern.ToForwardSearcher pat σ] → Std.Iter String.Slice
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.reference.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.reference = 1
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_zpow : ∀ {α : Type u_1} {N : Type u_16} [inst : DivisionCommMonoid N] [inst_1 : Fintype α] (f : α →₀ ℤ) (g : α → N),
  (f.prod fun a b => g a ^ b) = ∏ a, g a ^ f a
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_mono_l : ∀ {σs : List (Type u)} {P P' Q : Std.Do.SPred σs}, (P ⊢ₛ P') → P ∧ Q ⊢ₛ P' ∧ Q
-- Mathlib.Topology.UniformSpace.Cauchy
Cauchy.map : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : UniformSpace β] {f : Filter α} {m : α → β},
  Cauchy f → UniformContinuous m → Cauchy (Filter.map m f)
-- Mathlib.Logic.Equiv.Defs
DFunLike.coe.hcongr_6 : ∀ (F F' : Sort u_1),
  F = F' →
    ∀ (α α' : Sort u_2),
      α = α' →
        ∀ (β : α → Sort u_3) (β' : α' → Sort u_3),
          β ≍ β' →
            ∀ (self : DFunLike F α β) (self' : DFunLike F' α' β'),
              self ≍ self' → ∀ (a : F) (a' : F'), a ≍ a' → ∀ (a_1 : α) (a'_1 : α'), a_1 ≍ a'_1 → a a_1 ≍ a' a'_1
-- Init.Data.List.Lemmas
List.ne_nil_of_tail_ne_nil : ∀ {α : Type u_1} {l : List α}, l.tail ≠ [] → l ≠ []
-- Mathlib.Data.Prod.Lex
Prod.Lex.lt_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {x y : Lex (α × β)},
  x < y ↔ (ofLex x).1 < (ofLex y).1 ∨ (ofLex x).1 = (ofLex y).1 ∧ (ofLex x).2 < (ofLex y).2
-- Mathlib.Algebra.Group.Prod
Prod.instRightCancelSemigroup.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : RightCancelSemigroup G] [inst_1 : RightCancelSemigroup H],
  Prod.instRightCancelSemigroup = { toSemigroup := Prod.instSemigroup, toIsRightCancelMul := ⋯ }
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.GoodProducts.max_eq_o_cons_tail : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}},
  Profinite.NobelingProof.contained C (Order.succ o) →
    ∀ (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)),
      ↑↑l = Profinite.NobelingProof.term I ho :: ↑(↑l).Tail
-- Lean.Expr
Lean.Expr.consumeMData : Lean.Expr → Lean.Expr
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {G'' : Type u_8} [inst_2 : NormedAddCommGroup G''] [inst_3 : PartialOrder G'']
  [IsOrderedAddMonoid G''] [inst_5 : NormedSpace ℝ G''] {T T' : Set α → E →L[ℝ] G''} {C C' : ℝ}
  (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'),
  (∀ (s : Set α) (x : E), (T s) x ≤ (T' s) x) →
    ∀ (f : ↥(α →₁ₛ[μ] E)),
      (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f ≤ (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT') f
-- Init.Data.BitVec.Lemmas
BitVec.ofFin_lt : ∀ {n : ℕ} {x : Fin (2 ^ n)} {y : BitVec n}, { toFin := x } < y ↔ x < y.toFin
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.spanHomMk_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C}
  (z : F.obj CategoryTheory.Limits.WalkingSpan.zero ⟶ G.obj CategoryTheory.Limits.WalkingSpan.zero)
  (l : F.obj CategoryTheory.Limits.WalkingSpan.left ⟶ G.obj CategoryTheory.Limits.WalkingSpan.left)
  (r : F.obj CategoryTheory.Limits.WalkingSpan.right ⟶ G.obj CategoryTheory.Limits.WalkingSpan.right)
  (hl :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingSpan.Hom.fst) l =
        CategoryTheory.CategoryStruct.comp z (G.map CategoryTheory.Limits.WalkingSpan.Hom.fst))
      CategoryTheory.Limits.spanHomMk._auto_1)
  (hr :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingSpan.Hom.snd) r =
        CategoryTheory.CategoryStruct.comp z (G.map CategoryTheory.Limits.WalkingSpan.Hom.snd))
      CategoryTheory.Limits.spanHomMk._auto_3)
  (X : CategoryTheory.Limits.WalkingSpan),
  (CategoryTheory.Limits.spanHomMk z l r hl hr).app X =
    Option.casesOn X z fun val => CategoryTheory.Limits.WalkingPair.casesOn val l r
-- Lean.Data.PersistentHashSet
Lean.PersistentHashSet.findD : {α : Type u_1} → {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet α → α → α → α
-- Init.Meta.Defs
Lean.instQuoteArrayMkStr1 : {α : Type} → [Lean.Quote α] → Lean.Quote (Array α)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul_finset_insert : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] (a : α) (b : β) (s : Finset β),
  a • insert b s = insert (a • b) (a • s)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toList_rcc : ∀ {m n k : ℕ}, List.map (fun x => x + k) (m...=n).toList = ((m + k)...=n + k).toList
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivAtFilter.tendsto_nhds : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} [ContinuousAdd E] [ContinuousSMul 𝕜 E]
  [ContinuousAdd F] [ContinuousSMul 𝕜 F] {L : Filter E},
  L ≤ nhds x → HasFDerivAtFilter f f' (L ×ˢ pure x) → Filter.Tendsto f L (nhds (f x))
-- Mathlib.Data.Set.Function
Set.rightInvOn_id : ∀ {α : Type u_1} (s : Set α), Set.RightInvOn id id s
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_alter_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  [inst_1 : Inhabited α] {k : α} {f : Option (β k) → Option (β k)},
  (m.alter k f).getKey! k = if (f (m.get? k)).isSome = true then k else default
-- Mathlib.Data.Set.FiniteExhaustion
Set.FiniteExhaustion.instFiniteElemCoeNat : ∀ {α : Type u_1} {s : Set α} {K : s.FiniteExhaustion} {n : ℕ}, Finite ↑(K n)
-- Mathlib.Data.Set.Lattice
Set.biUnion_eq_iUnion : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) (t : (x : α) → x ∈ s → Set β), ⋃ x, ⋃ (h : x ∈ s), t x h = ⋃ x, t ↑x ⋯
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
Orthonormal.equiv_trans : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {ι' : Type u_5} {ι'' : Type u_6} {E' : Type u_7} [inst_3 : SeminormedAddCommGroup E']
  [inst_4 : InnerProductSpace 𝕜 E'] {E'' : Type u_8} [inst_5 : SeminormedAddCommGroup E'']
  [inst_6 : InnerProductSpace 𝕜 E''] {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) {v' : Module.Basis ι' 𝕜 E'}
  (hv' : Orthonormal 𝕜 ⇑v') (e : ι ≃ ι') {v'' : Module.Basis ι'' 𝕜 E''} (hv'' : Orthonormal 𝕜 ⇑v'') (e' : ι' ≃ ι''),
  (hv.equiv hv' e).trans (hv'.equiv hv'' e') = hv.equiv hv'' (e.trans e')
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.length_toPath : ∀ {V : Type u} [inst : Quiver V] {a b : V} (e : a ⟶ b), e.toPath.length = 1
-- Mathlib.Topology.UniformSpace.Separation
SeparationQuotient.uniformContinuous_uncurry_lift₂ : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  {f : α → β → γ} (h : ∀ (a : α) (c : β) (b : α) (d : β), Inseparable a b → Inseparable c d → f a c = f b d),
  UniformContinuous (Function.uncurry (SeparationQuotient.lift₂ f h)) ↔ UniformContinuous (Function.uncurry f)
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
/-- If two functions agree in a neighborhood within `s`, then so do their iterated derivatives.  -/
Filter.EventuallyEq.iteratedDerivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {f g : 𝕜 → F} {s : Set 𝕜},
  f =ᶠ[nhdsWithin x s] g → ∀ (n : ℕ), iteratedDerivWithin n f s =ᶠ[nhdsWithin x s] iteratedDerivWithin n g s
-- Std.Data.ExtDTreeMap.Basic
/-- Returns an array of all values present in the tree map in ascending  order.  -/
Std.ExtDTreeMap.valuesArray : {α : Type u} →
  {cmp : α → α → Ordering} → [Std.TransCmp cmp] → {β : Type v} → Std.ExtDTreeMap α (fun x => β) cmp → Array β
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHomClass.instCoeToBialgHom : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {F : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : Semiring B] →
                [inst_4 : Algebra R B] →
                  [inst_5 : CoalgebraStruct R A] →
                    [inst_6 : CoalgebraStruct R B] →
                      [inst_7 : FunLike F A B] → [BialgHomClass F R A B] → CoeHead F (A →ₐc[R] B)
-- Mathlib.Algebra.Order.Group.Lattice
sup_sub : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddRightMono α] (a b c : α), a ⊔ b - c = (a - c) ⊔ (b - c)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- the first map `L → R`  -/
CategoryTheory.Limits.MultispanShape.fst : (self : CategoryTheory.Limits.MultispanShape) → self.L → self.R
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.toSubgroupEquiv_neg_apply : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) (u : ℤˣ) (a : ↥(HNNExtension.toSubgroup A B u)),
  ↑((HNNExtension.toSubgroupEquiv φ (-u)) ((HNNExtension.toSubgroupEquiv φ u) a)) = ↑a
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Real.Gamma_pos_of_pos : ∀ {s : ℝ}, 0 < s → 0 < Real.Gamma s
-- Mathlib.Logic.Equiv.List
_private.Mathlib.Logic.Equiv.List.0.Encodable.decodeList.match_1.splitter : (v : ℕ) →
  (motive : (x : ℕ × ℕ) → x.2 ≤ v → Sort u_1) →
    (x : ℕ × ℕ) → (x_1 : x.2 ≤ v) → ((v₁ v₂ : ℕ) → (h : (v₁, v₂).2 ≤ v) → motive (v₁, v₂) h) → motive x x_1
-- Init.Data.SInt.Lemmas
Int32.toInt16_neg : ∀ (x : Int32), (-x).toInt16 = -x.toInt16
-- Init.Data.Nat.Lcm
Nat.lcm_eq_one_iff : ∀ {m n : ℕ}, m.lcm n = 1 ↔ m = 1 ∧ n = 1
-- Mathlib.Topology.Instances.Int
Int.isUniformEmbedding_coe_real : IsUniformEmbedding Int.cast
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.toCycles_comp_homologyπ_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [inst_2 : K.HasHomology j] {Z : C}
  (h : K.homology j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.toCycles i j) (CategoryTheory.CategoryStruct.comp (K.homologyπ j) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.instIsAddMonHomNegOfHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N : C}
  [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N] (f : M ≅ N)
  [CategoryTheory.IsAddMonHom f.hom], CategoryTheory.IsAddMonHom f.inv