mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Iterator
/-- Returns a finite iterator over the keys of a tree map.
The iterator yields the keys in order and then terminates.

The key and value types must live in the same universe.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.TreeMap.keysIter : {α β : Type u} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → Std.Iter α
-- Mathlib.Algebra.Algebra.Hom
/-- Identity map as an `AlgHom`.  -/
AlgHom.id : (R : Type u) → (A : Type v) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → A →ₐ[R] A
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
powers_le_nonZeroDivisors_of_noZeroDivisors : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {x : M₀} [NoZeroDivisors M₀],
  x ≠ 0 → Submonoid.powers x ≤ nonZeroDivisors M₀
-- Mathlib.CategoryTheory.Filtered.FinallySmall
CategoryTheory.FinalModel.congr_simp : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] [inst_1 : CategoryTheory.FinallySmall J],
  CategoryTheory.FinalModel J = CategoryTheory.FinalModel J
-- Mathlib.RepresentationTheory.Maschke
MonoidAlgebra.Submodule.instIsSemisimpleRingAddMonoidAlgebra : ∀ {k : Type u_1} [inst : Field k] {G : Type u_2} [Finite G] [NeZero ↑(Nat.card G)] [inst_3 : AddGroup G],
  IsSemisimpleRing (AddMonoidAlgebra k G)
-- Mathlib.Algebra.Colimit.Module
AddCommGroup.DirectLimit.lift_injective : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (G i)]
  {f : (i j : ι) → i ≤ j → G i →+ G j} [inst_2 : DecidableEq ι] (P : Type u_4) [inst_3 : AddCommMonoid P]
  (g : (i : ι) → G i →+ P) (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x)
  [IsDirectedOrder ι],
  (∀ (i : ι), Function.Injective ⇑(g i)) → Function.Injective ⇑(AddCommGroup.DirectLimit.lift G f P g Hg)
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.UnifEigenvalues.mk_val : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {k : ℕ∞} (μ : f.UnifEigenvalues k), ⟨↑f k μ, ⋯⟩ = μ
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.LeftHomologyMapData.homologyMap_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
  CategoryTheory.ShortComplex.homologyMap φ =
    CategoryTheory.CategoryStruct.comp h₁.homologyIso.hom (CategoryTheory.CategoryStruct.comp γ.φH h₂.homologyIso.inv)
-- Mathlib.RingTheory.LocalProperties.Submodule
Submodule.eq_top_of_localization_maximal : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4) [inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)]
  [inst_4 : (P : Ideal R) → [inst_4 : P.IsMaximal] → Algebra R (Rₚ P)]
  [inst_5 : ∀ (P : Ideal R) [inst_5 : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P]
  (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5) [inst_6 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_7 : (P : Ideal R) → [inst_7 : P.IsMaximal] → Module R (Mₚ P)]
  [inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)]
  [inst_9 : ∀ (P : Ideal R) [inst_9 : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)]
  (f : (P : Ideal R) → [inst_10 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [inst_10 : ∀ (P : Ideal R) [inst_10 : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (N : Submodule R M),
  (∀ (P : Ideal R) [inst_11 : P.IsMaximal], Submodule.localized' (Rₚ P) P.primeCompl (f P) N = ⊤) → N = ⊤
-- Mathlib.LinearAlgebra.Pi
LinearEquiv.sumArrowLequivProdArrow_symm_apply_inr : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_5}
  {β : Type u_6} (f : α → M) (g : β → M) (b : β),
  (LinearEquiv.sumArrowLequivProdArrow α β R M).symm (f, g) (Sum.inr b) = g b
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
/-- Assume that `f` is differentiable inside a convex set `s`, and that its derivative `f'` is
differentiable at a point `x`. Then, given two vectors `v` and `w` pointing inside `s`, one
has `f'' v w = f'' w v`. Superseded by `Convex.second_derivative_within_at_symmetric`, which
removes the assumption that `v` and `w` point inside `s`.  -/
Convex.second_derivative_within_at_symmetric_of_mem_interior : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {s : Set E},
  Convex ℝ s →
    ∀ {f : E → F} {f' : E → E →L[ℝ] F} {f'' : E →L[ℝ] E →L[ℝ] F},
      (∀ x ∈ interior s, HasFDerivAt f (f' x) x) →
        ∀ {x : E},
          x ∈ s →
            HasFDerivWithinAt f' f'' (interior s) x →
              ∀ {v w : E}, x + 4 • v ∈ interior s → x + 4 • w ∈ interior s → (f'' w) v = (f'' v) w
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.Pushout.condition : ∀ {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Types.Pushout.inl f g) =
    CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.Types.Pushout.inr f g)
-- Mathlib.FieldTheory.Relrank
/-- If `A ≤ B`, then `Subfield.relrank A B` is `[B : A]`.  -/
Subfield.relrank_eq_rank_of_le : ∀ {E : Type v} [inst : Field E] {A B : Subfield E} (h : A ≤ B), A.relrank B = Module.rank ↥A ↥(Subfield.extendScalars h)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.snd_δ_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C) {Z : C} (h : S.L₃.X₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd S.L₁.g S.v₀₁.τ₃)
      (CategoryTheory.CategoryStruct.comp S.δ h) =
    CategoryTheory.CategoryStruct.comp S.φ₁ (CategoryTheory.CategoryStruct.comp S.v₂₃.τ₁ h)
-- Mathlib.Analysis.Convex.Function
/-- The pointwise maximum of strictly convex functions is strictly convex.  -/
StrictConvexOn.sup : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  [PosSMulStrictMono 𝕜 β] {s : Set E} {f g : E → β},
  StrictConvexOn 𝕜 s f → StrictConvexOn 𝕜 s g → StrictConvexOn 𝕜 s (f ⊔ g)
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
/-- `Multiset.Nat.antidiagonalTuple k n` is a multiset of `k`-tuples summing to `n`  -/
Multiset.Nat.antidiagonalTuple : (k : ℕ) → ℕ → Multiset (Fin k → ℕ)
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.ofHoms.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_3} {X Y : ι → C} {f : (i : ι) → X i ⟶ Y i} (i : ι),
  CategoryTheory.MorphismProperty.ofHoms f (f i)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.pop'.eq_1 : ∀ (k : Turing.PartrecToTM2.K'), Turing.PartrecToTM2.pop' k = Turing.TM2.Stmt.pop k fun x v => v
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrpFunctor_map_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F G : C ⥤ₗ D} (α : F ⟶ G) (A : CategoryTheory.Grp C),
  (CategoryTheory.Functor.mapGrpFunctor.map α).app A = CategoryTheory.Grp.homMk'' (α.hom.app A.X) ⋯ ⋯
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullbackWithin_add_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M}
  {V V₁ : (x : M') → TangentSpace I' x},
  VectorField.mpullbackWithin I I' f (V + V₁) s x =
    VectorField.mpullbackWithin I I' f V s x + VectorField.mpullbackWithin I I' f V₁ s x
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β}, (m.insert k v)[a]? = if (k == a) = true then some v else m[a]?
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
/-- The map `HoCat.pResolutionObj`, when applied to already cofibrant objects, gives
a natural transformation `ι ⋙ HoCat.resolution ⟶ toHoCat`.  -/
HomotopicalAlgebra.CofibrantObject.HoCat.ιCompResolutionNatTrans : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      HomotopicalAlgebra.CofibrantObject.ι.comp HomotopicalAlgebra.CofibrantObject.HoCat.resolution ⟶
        HomotopicalAlgebra.CofibrantObject.toHoCat
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.stRun.eq_1 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {k : K} (f : σ → Γ k),
  Turing.TM2to1.stRun (Turing.TM2to1.StAct.push f) = Turing.TM2.Stmt.push k f
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderiv_mul' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {a b : E → 𝔸},
  DifferentiableAt 𝕜 a x →
    DifferentiableAt 𝕜 b x → fderiv 𝕜 (a * b) x = a x • fderiv 𝕜 b x + MulOpposite.op (b x) • fderiv 𝕜 a x
-- Batteries.Data.BinomialHeap.Basic
/-- The "real size" of the node, counting up how many values of type `α` are stored.
This is `O(n)` and is intended mainly for specification purposes.
For a well formed `HeapNode` the size is always `2^n - 1` where `n` is the depth.
 -/
Batteries.BinomialHeap.Imp.HeapNode.realSize : {α : Type u_1} → Batteries.BinomialHeap.Imp.HeapNode α → ℕ
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffWithinAt.clm_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {x : E} {n : WithTop ℕ∞} {f : E → F →L[𝕜] G}
  {g : E → F}, ContDiffWithinAt 𝕜 n f s x → ContDiffWithinAt 𝕜 n g s x → ContDiffWithinAt 𝕜 n (fun x => (f x) (g x)) s x
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for signed less than or equal `sle` on `BitVec`s.  -/
BitVec.reduceSLE : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.ι_π : ∀ {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] (n₁ : ℤ),
  CategoryTheory.CategoryStruct.comp (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.ι✝ f n₁)
      (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.π✝ K L n₁) =
    f
-- Lean.Elab.Term.TermElabM
/-- Create an auxiliary annotation to make sure we create an `Info` even if `e` is a metavariable.
See `mkTermInfo`.

We use this function because some elaboration functions elaborate subterms that may not be immediately
part of the resulting term. Example:
```
let_mvar% ?m := b; wait_if_type_mvar% ?m; body
```
If the type of `b` is not known, then `wait_if_type_mvar% ?m; body` is postponed and just returns a fresh
metavariable `?n`. The elaborator for
```
let_mvar% ?m := b; wait_if_type_mvar% ?m; body
```
returns `mkSaveInfoAnnotation ?n` to make sure the info nodes created when elaborating `b` are "saved".
This is a bit hackish, but elaborators like `let_mvar%` are rare.
 -/
Lean.Elab.Term.mkSaveInfoAnnotation : Lean.Expr → Lean.Expr
-- Lean.Meta.Tactic.Grind.Internalize
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.forbiddenSplitTypes : List Lean.Name
-- Mathlib.Analysis.Convex.Deriv
/-- If a function `f` is continuous on a convex set `D ⊆ ℝ` and `f''` is strictly negative on the
interior, then `f` is strictly concave on `D`.
Note that we don't require twice differentiability explicitly as it already implied by the second
derivative being strictly negative, except at at most one point.  -/
strictConcaveOn_of_deriv2_neg : ∀ {D : Set ℝ},
  Convex ℝ D → ∀ {f : ℝ → ℝ}, ContinuousOn f D → (∀ x ∈ interior D, deriv^[2] f x < 0) → StrictConcaveOn ℝ D f
-- Mathlib.GroupTheory.Coxeter.Matrix
/-- The Coxeter matrix of type G₂.

The corresponding Coxeter-Dynkin diagram is:
```
       6
    o --- o
```
 -/
CoxeterMatrix.G₂ : CoxeterMatrix (Fin 2)
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.conjTranspose_kronecker' : ∀ {R : Type u_1} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [inst : Mul R] [inst_1 : StarMul R]
  (x : Matrix l m R) (y : Matrix n p R),
  (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) x y).conjTranspose =
    (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) y.conjTranspose x.conjTranspose).submatrix Prod.swap Prod.swap
-- Mathlib.CategoryTheory.Action.Continuous
ContAction.instHasForget₂HomSubtypeObjActionIsContinuousVTopCatContinuousMapCarrier : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {FV : V → V → Type u_2} →
      {CV : V → Type u_3} →
        [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory V FV] →
            [inst_3 : CategoryTheory.HasForget₂ V TopCat] →
              (G : Type u_4) →
                [inst_4 : Monoid G] → [inst_5 : TopologicalSpace G] → CategoryTheory.HasForget₂ (ContAction V G) TopCat
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.hasseDeriv_single_add : ∀ {R : Type u_1} [inst : Semiring R] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module R V] (k : ℕ) (n : ℤ)
  (x : V),
  (LaurentSeries.hasseDeriv R k) ((HahnSeries.single (n + ↑k)) x) = (HahnSeries.single n) (Ring.choose (n + ↑k) k • x)
-- Mathlib.CategoryTheory.Equivalence
/-- The unit of an equivalence of categories.  -/
CategoryTheory.Equivalence.unit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (e : C ≌ D) → CategoryTheory.Functor.id C ⟶ e.functor.comp e.inverse
-- Mathlib.Data.PFunctor.Multivariate.W
/-- Specialized destructor on `WPath`  -/
MvPFunctor.wPathDestLeft : {n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) →
    {α : TypeVec.{u_1} n} →
      {a : P.A} → {f : P.last.B a → P.last.W} → TypeVec.Arrow (P.WPath (WType.mk a f)) α → (P.drop.B a).Arrow α
-- Mathlib.RingTheory.Regular.IsSMulRegular
LinearEquiv.isSMulRegular_congr' : ∀ {R : Type u_3} {S : Type u_2} {M : Type u_4} {N : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S}
  {σ' : S →+* R} [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : AddCommMonoid N] [inst_7 : Module S N] (e : M ≃ₛₗ[σ] N) (r : R),
  IsSMulRegular M r ↔ IsSMulRegular N (σ r)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_left_injOn : ∀ {x : ℝ}, x ≠ 0 → Set.InjOn (fun y => y ^ x) {y | 0 ≤ y}
-- Init.Data.UInt.BasicAux
/-- Converts a `UInt16` into the corresponding `Fin UInt16.size`.  -/
UInt16.toFin : UInt16 → Fin UInt16.size
-- Mathlib.Data.Finset.Sum
Finset.toLeft_disjSum_toRight : ∀ {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)}, u.toLeft.disjSum u.toRight = u
-- Lean.Elab.DeclNameGen
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.MkNameState.mk : Lean.ExprSet → Lean.NameSet → Lean.Elab.Command.NameGen.MkNameState✝
-- Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
/-- Close the goal of the form `η = θ`, where `η` and `θ` are 2-isomorphisms made up only of
associators, unitors, and identities.
```lean
example {C : Type} [Category* C] [MonoidalCategory C] :
  (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom := by
  monoidal_coherence
```
 -/
Mathlib.Tactic.Monoidal.pureCoherence : Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The category of multiforks is equivalent to the category of forks over `∏ᶜ I.left ⇉ ∏ᶜ I.right`.
It then follows from `CategoryTheory.IsLimit.ofPreservesConeTerminal` (or `reflects`) that it
preserves and reflects limit cones.
 -/
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      (I : CategoryTheory.Limits.MulticospanIndex J C) →
        {c : CategoryTheory.Limits.Fan I.left} →
          CategoryTheory.Limits.IsLimit c →
            {d : CategoryTheory.Limits.Fan I.right} →
              (hd : CategoryTheory.Limits.IsLimit d) →
                CategoryTheory.Limits.Multifork I ≌
                  CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
-- Mathlib.Topology.Category.Profinite.Extend
Profinite.Extend.cone_pt : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor Profinite C) (S : Profinite),
  (Profinite.Extend.cone G S).pt = G.obj S
-- Mathlib.Data.Multiset.Count
Multiset.countP_eq_zero : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Multiset α}, Multiset.countP p s = 0 ↔ ∀ a ∈ s, ¬p a
-- Mathlib.RingTheory.SurjectiveOnStalks
RingHom.SurjectiveOnStalks.baseChange' : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {T : Type u_3} [inst_2 : CommRing T]
  [inst_3 : Algebra R T] [inst_4 : Algebra R S],
  (algebraMap R S).SurjectiveOnStalks → Algebra.TensorProduct.includeRight.SurjectiveOnStalks
-- Mathlib.FieldTheory.Separable
Polynomial.separable_of_subsingleton : ∀ {R : Type u} [inst : CommSemiring R] [Subsingleton R] (f : Polynomial R), f.Separable
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.extraction_forall_of_eventually' : ∀ {P : ℕ → ℕ → Prop}, (∀ (n : ℕ), ∃ N, ∀ k ≥ N, P n k) → ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
-- Mathlib.Topology.Connected.Clopen
/-- The preimage of a connected component is preconnected if the function has connected fibers
and a subset is closed iff the preimage is.  -/
Topology.IsCoinducing.isConnected_preimage_of_isClosed : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  (∀ (t : β), IsConnected (f ⁻¹' {t})) →
    Topology.IsCoinducing f → ∀ {t : Set β}, IsClosed t → IsConnected t → IsConnected (f ⁻¹' t)
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The symbol `J(a | b)` vanishes if and only if `b ≠ 0` and `a` and `b` are not coprime.  -/
jacobiSym.eq_zero_iff : ∀ {a : ℤ} {b : ℕ}, jacobiSym a b = 0 ↔ b ≠ 0 ∧ a.gcd ↑b ≠ 1
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Subalgebra.center_eq_top : ∀ (R : Type u) [inst : CommSemiring R] (A : Type u_1) [inst_1 : CommSemiring A] [inst_2 : Algebra R A],
  Subalgebra.center R A = ⊤
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.DelayedTheoremInstance.prop : Lean.Meta.Grind.DelayedTheoremInstance → Lean.Expr
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.comp_f₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) (g : S₂ ⟶ S₃),
  (CategoryTheory.CategoryStruct.comp f g).f₁ = CategoryTheory.CategoryStruct.comp f.f₁ g.f₁
-- Mathlib.Tactic.Lift
PiSubtype.canLift' : ∀ (ι : Sort u_1) (α : Sort u_2) [Nonempty α] (p : ι → Prop),
  CanLift (Subtype p → α) (ι → α) (fun f i => f ↑i) fun x => True
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.HaveLebesgueDecomposition.add_left : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν μ' : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν]
  [μ'.HaveLebesgueDecomposition ν], (μ + μ').HaveLebesgueDecomposition ν
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContinuousLinearMap.contMDiffWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_6} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  (L : E →L[𝕜] F) {s : Set E} {x : E},
  ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) n (⇑L) s x
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.symm_bijective : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N], Function.Bijective ContinuousMulEquiv.symm
-- Batteries.Data.Int
_private.Batteries.Data.Int.0.Int.testBit.match_1.eq_2 : ∀ (motive : ℤ → ℕ → Sort u_1) (m n : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) n)
  (h_2 : (m n : ℕ) → motive (Int.negSucc m) n),
  (match Int.negSucc m, n with
    | Int.ofNat m, n => h_1 m n
    | Int.negSucc m, n => h_2 m n) =
    h_2 m n
-- Lean.Meta.Hint
Lean.Meta.Hint.DiffGranularity.all.sizeOf_spec : sizeOf Lean.Meta.Hint.DiffGranularity.all = 1
-- Mathlib.Topology.Bases
/-- In a second countable topological space, any family generating the topology admits a
countable generating subfamily.  -/
TopologicalSpace.exists_countable_of_generateFrom : ∀ {α : Type u_1} [ts : TopologicalSpace α] [SecondCountableTopology α] {t : Set (Set α)},
  ts = TopologicalSpace.generateFrom t → ∃ s ⊆ t, s.Countable ∧ ts = TopologicalSpace.generateFrom s
-- Mathlib.Order.Hom.Lattice
SupHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Max β] {f g : SupHom α β}, f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.Analysis.Normed.Lp.lpHolder
/-- `lp.holder` as a continuous bilinear map.  -/
lp.holderL : {ι : Type u_1} →
  {𝕜 : Type u_2} →
    {E : ι → Type u_3} →
      {F : ι → Type u_4} →
        {G : ι → Type u_5} →
          [inst : RCLike 𝕜] →
            [inst_1 : (i : ι) → NormedAddCommGroup (E i)] →
              [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
                [inst_3 : (i : ι) → NormedAddCommGroup (F i)] →
                  [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)] →
                    [inst_5 : (i : ι) → NormedAddCommGroup (G i)] →
                      [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)] →
                        {p q : ENNReal} →
                          (r : ENNReal) →
                            [hpqr : p.HolderTriple q r] →
                              [inst_7 : Fact (1 ≤ p)] →
                                [inst_8 : Fact (1 ≤ q)] →
                                  [inst_9 : Fact (1 ≤ r)] →
                                    (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) →
                                      {K : NNReal} → (∀ (i : ι), ‖B i‖ ≤ ↑K) → ↥(lp E p) →L[𝕜] ↥(lp F q) →L[𝕜] ↥(lp G r)
-- Mathlib.Order.SuccPred.LinearLocallyFinite
LinearLocallyFiniteOrder.isGLB_Ioc_of_isGLB_Ioi : ∀ {ι : Type u_1} [inst : LinearOrder ι] {i j k : ι}, i < j → IsGLB (Set.Ioi i) k → IsGLB (Set.Ioc i j) k
-- Mathlib.Algebra.Polynomial.Div
/-- `divByMonic`, denoted as `p /ₘ q`, gives the quotient of `p` by a monic polynomial `q`.  -/
Polynomial.divByMonic : {R : Type u} → [inst : Ring R] → Polynomial R → Polynomial R → Polynomial R
-- Init.Data.BitVec.Lemmas
BitVec.ofBoolListLE.eq_2 : ∀ (b : Bool) (bs : List Bool), BitVec.ofBoolListLE (b :: bs) = (BitVec.ofBoolListLE bs).concat b
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_mul_nat : ∀ (x y : ℂ) (n : ℕ), x ^ (y * ↑n) = (x ^ y) ^ n