mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- Characterizing the forward direction of `leftUnitor` via the universal maps.  -/
CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_hom_unit_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (U : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolutionUnit U]
  (F : CategoryTheory.Functor C V)
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution U F] (y : C) {Z : V}
  (h :
    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.DayConvolutionUnit.can
        (F.obj y))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategory.DayConvolution.unit U F).app
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C, y))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor U F).hom.app
            (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) y))
          h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj y)).hom
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor y).inv) h)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.updateCell.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (l : Std.DTreeMap.Internal.Impl α β) →
      (motive : Std.DTreeMap.Internal.Impl.SizedBalancedTree α β (l.size - 1) (l.size + 1) → Sort u_3) →
        (x : Std.DTreeMap.Internal.Impl.SizedBalancedTree α β (l.size - 1) (l.size + 1)) →
          ((newL : Std.DTreeMap.Internal.Impl α β) →
              (h₁ : newL.Balanced) →
                (h₂ : l.size - 1 ≤ newL.size) →
                  (h₃ : newL.size ≤ l.size + 1) →
                    motive { impl := newL, balanced_impl := h₁, lb_le_size_impl := h₂, size_impl_le_ub := h₃ }) →
            motive x
-- Mathlib.Logic.Basic
forall_mem_comm : ∀ {α : Type u_1} {β : Type u_2} [inst : Membership α β] {s : β} {p : α → α → Prop},
  (∀ a ∈ s, ∀ b ∈ s, p a b) ↔ ∀ (a b : α), a ∈ s → b ∈ s → p a b
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.sameCycle_apply_left : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle (f x) y ↔ f.SameCycle x y
-- Mathlib.Topology.VectorBundle.Basic
VectorPrebundle.totalSpaceMk_isInducing : ∀ {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)]
  (self : VectorPrebundle R F E) (b : B), Topology.IsInducing (↑(self.pretrivializationAt b) ∘ Bundle.TotalSpace.mk b)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.ofSubmodule'_toContinuousLinearMap : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid M₂] [inst_5 : TopologicalSpace M₂]
  {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M ≃SL[σ₁₂] M₂) (U : Submodule R₂ M₂),
  ↑(f.ofSubmodule' U) = (↑f ∘SL (Submodule.comap (↑↑f) U).subtypeL).codRestrict U ⋯
-- Mathlib.Topology.Algebra.Monoid
Subsemigroup.coe_topologicalClosure : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Semigroup M] [inst_2 : SeparatelyContinuousMul M]
  (s : Subsemigroup M), ↑s.topologicalClosure = closure ↑s
-- Mathlib.Combinatorics.Colex
Finset.Colex.toColex_lt_toColex_iff_max'_mem : ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Finset α},
  toColex s < toColex t ↔ ∃ (hst : s ≠ t), (symmDiff s t).max' ⋯ ∈ t
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.foldM_eq_foldlM_toList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {δ : Type w} {m' : Type w → Type w'} {β : Type v}
  {m : Std.DHashMap.Raw α fun x => β} [inst_2 : Monad m'] [LawfulMonad m'],
  m.WF →
    ∀ {f : δ → α → β → m' δ} {init : δ},
      Std.DHashMap.Raw.foldM f init m = List.foldlM (fun a b => f a b.1 b.2) init (Std.DHashMap.Raw.Const.toList m)
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.Context.mk.sizeOf_spec : ∀ (funId : Lean.Ident) (ctorVal? : Option Lean.ConstructorVal) (explicit ellipsis : Bool)
  (paramDecls : Array (Lean.Name × Lean.BinderInfo)) (paramDeclIdx : ℕ) (namedArgs : Array Lean.Elab.Term.NamedArg)
  (usedNames : Std.HashSet Lean.Name) (args : List Lean.Elab.Term.Arg) (newArgs : Array Lean.Term),
  sizeOf
      { funId := funId, ctorVal? := ctorVal?, explicit := explicit, ellipsis := ellipsis, paramDecls := paramDecls,
        paramDeclIdx := paramDeclIdx, namedArgs := namedArgs, usedNames := usedNames, args := args,
        newArgs := newArgs } =
    1 + sizeOf funId + sizeOf ctorVal? + sizeOf explicit + sizeOf ellipsis + sizeOf paramDecls + sizeOf paramDeclIdx +
            sizeOf namedArgs +
          sizeOf usedNames +
        sizeOf args +
      sizeOf newArgs
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.veq_zero_iff : ∀ {K : Type u_2} [inst : DivisionRing K] [inst_1 : ValuativeRel K] {a : K}, 0 =ᵥ a ↔ 0 = a
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
/-- `HasAffineProperty P Q` is a type class asserting that `P` is local at the target, and over affine
schemes, it is equivalent to `Q : AffineTargetMorphismProperty`.
To make the proofs easier, we state it instead as
1. `Q` is local at the target
2. `P f` if and only if `∀ U, Q (f ∣_ U)` ranging over all affine opens of the target of `f`.

See `HasAffineProperty.iff`.
 -/
AlgebraicGeometry.HasAffineProperty : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme →
  outParam AlgebraicGeometry.AffineTargetMorphismProperty → Prop
-- Mathlib.Algebra.Ring.InjSurj
/-- Pullback a `NonUnitalNonAssocRing` instance along an injective function.  -/
Function.Injective.nonUnitalNonAssocRing : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Add S] →
      [inst_1 : Mul S] →
        [inst_2 : Zero S] →
          [inst_3 : Neg S] →
            [inst_4 : Sub S] →
              [inst_5 : SMul ℕ S] →
                [inst_6 : SMul ℤ S] →
                  [inst_7 : NonUnitalNonAssocRing R] →
                    (f : S → R) →
                      Function.Injective f →
                        f 0 = 0 →
                          (∀ (x y : S), f (x + y) = f x + f y) →
                            (∀ (x y : S), f (x * y) = f x * f y) →
                              (∀ (x : S), f (-x) = -f x) →
                                (∀ (x y : S), f (x - y) = f x - f y) →
                                  (∀ (n : ℕ) (x : S), f (n • x) = n • f x) →
                                    (∀ (n : ℤ) (x : S), f (n • x) = n • f x) → NonUnitalNonAssocRing S
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey!_eq_minKeyD_default : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)}, Std.Internal.List.minKey! l = Std.Internal.List.minKeyD l default
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.comm : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (self : SSet.RelativeMorphism A B φ),
  CategoryTheory.CategoryStruct.comp A.ι self.map = CategoryTheory.CategoryStruct.comp φ B.ι
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsAddFoelner.tendsto_nhds_mean : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : AddGroup G]
  [inst_2 : AddAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X},
  IsAddFoelner G μ (↑u) F →
    ∀ (s : Set X), Filter.Tendsto (fun i => μ (s ∩ F i) / μ (F i)) (↑u) (nhds (IsAddFoelner.mean μ u F s))
-- Mathlib.Algebra.Order.BigOperators.Expect
Finset.expect_nonneg : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : Module ℚ≥0 α] {s : Finset ι} {f : ι → α} [PosSMulMono ℚ≥0 α], (∀ i ∈ s, 0 ≤ f i) → 0 ≤ s.expect fun i => f i
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min!_eq_iff_mem_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → ∀ {km : α}, t.min! = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.RingTheory.Perfection
PreTilt.isDomain : ∀ (K : Type u₁) [inst : Field K] (v : Valuation K NNReal) (O : Type u₂) [inst_1 : CommRing O] [inst_2 : Algebra O K],
  v.Integers O → ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] [inst_3 : Fact ¬IsUnit ↑p], IsDomain (PreTilt O p)
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracket_swap : ∀ {𝕜 : 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] {V W : (x : M) → TangentSpace I x},
  VectorField.mlieBracket I V W = -VectorField.mlieBracket I W V
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.extend.eq_1 : ∀ {α : Type u} [inst : UniformSpace α] {β : Type v} [inst_1 : UniformSpace β] (f : α → β),
  CauchyFilter.extend f = if UniformContinuous f then ⋯.extend f else fun x => f ⋯.some
-- Mathlib.Probability.Moments.CovarianceBilinDual
/-- Continuous bilinear form with value `∫ x, (L₁ x - μ[L₁]) * (L₂ x - μ[L₂]) ∂μ` on `(L₁, L₂)`
if `MemLp id 2 μ`. If not, we set it to zero.  -/
ProbabilityTheory.covarianceBilinDual : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    {mE : MeasurableSpace E} →
      [inst_1 : NormedSpace ℝ E] →
        [BorelSpace E] → MeasureTheory.Measure E → StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
-- Mathlib.Topology.Algebra.UniformConvergence
instGroupUniformFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Group β],
  instGroupUniformFun =
    { toMonoid := instMonoidUniformFun, toInv := instInvUniformFun, toDiv := instDivUniformFun, toZPow := ZPow.ofPow,
      div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯ }
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.Functor.mapHomologicalComplexIdIso_hom_app_f : ∀ {ι : Type u_1} (W₁ : Type u_3) [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms W₁] (c : ComplexShape ι) (X : HomologicalComplex W₁ c) (i : ι),
  ((CategoryTheory.Functor.mapHomologicalComplexIdIso W₁ c).hom.app X).f i = CategoryTheory.CategoryStruct.id (X.X i)
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
quasispectrumRestricts_iff_spectrumRestricts : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Semifield S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] {a : A} {f : S → R},
  QuasispectrumRestricts a f ↔ SpectrumRestricts a f
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_add_unitIso_inv_app_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ)
  (m n p : ℤ)
  (h : autoParam (m + n = p) CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_add_unitIso_inv_app_eq._auto_1),
  (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C p).unitIso.inv.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor C p).map ((CategoryTheory.shiftFunctorAdd' Cᵒᵖ n m p ⋯).hom.app X).unop).op
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctorAdd' C m n p h).inv.app
            (Opposite.unop (((CategoryTheory.shiftFunctor Cᵒᵖ n).comp (CategoryTheory.shiftFunctor Cᵒᵖ m)).obj X))).op
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctor C n).map
              ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C m).unitIso.inv.app
                  ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X)).unop).op
          ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app X)))
-- Mathlib.Algebra.Order.Floor.Defs
FloorSemiring.instZeroLEOneClass : ∀ {α : Type u_2} [inst : Semiring α] [inst_1 : PartialOrder α] [FloorSemiring α], ZeroLEOneClass α
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun_bijective : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] (o : Ordinal.{u}),
  Function.Bijective (Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun C o)
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.map_inv₂ : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {x : AddGroup M} {x_1 : AddZeroClass N} {x_2 : AddCommGroup P}
  (f : M →+ N →+ P) (m : M) (n : N), (f (-m)) n = -(f m) n
-- Mathlib.Topology.Algebra.GroupCompletion
AddMonoidHom.continuous_completion : ∀ {α : Type u_3} {β : Type u_4} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : IsUniformAddGroup α]
  [inst_3 : UniformSpace β] [inst_4 : AddGroup β] [inst_5 : IsUniformAddGroup β] (f : α →+ β) (hf : Continuous ⇑f),
  Continuous ⇑(f.completion hf)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.submatrix_map : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {β : Type w} (f : α → β) (e₁ : l → m)
  (e₂ : o → n) (A : Matrix m n α), (A.map f).submatrix e₁ e₂ = (A.submatrix e₁ e₂).map f
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso_inv_app_hom_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] [inst_3 : CategoryTheory.BraidedCategory D]
  (X : CategoryTheory.CommMon (CategoryTheory.Functor C D)) (X_1 : C),
  (CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso.inv.app X).hom.hom.app X_1 =
    CategoryTheory.CategoryStruct.id (X.X.obj X_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- The source of a 1-simplex in a path is identified with the source vertex.  -/
SSet.Truncated.Path₁.arrow_src : ∀ {X : SSet.Truncated 1} {n : ℕ} (self : X.Path₁ n) (i : Fin n),
  (CategoryTheory.ConcreteCategory.hom
        (X.map
          (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 1) SSet.Truncated.Path₁._proof_1
              SSet.Truncated.Path₁._proof_5).op))
      (self.arrow i) =
    self.vertex i.castSucc
-- Init.Data.Vector.Lex
Vector.empty_le : ∀ {α : Type u_1} [inst : LT α] (xs : Vector α 0), #v[] ≤ xs
-- Init.Data.BitVec.Lemmas
BitVec.twoPow.eq_1 : ∀ (w i : ℕ), BitVec.twoPow w i = 1#w <<< i
-- Init.Data.String.Basic
String.Pos.ofSliceTo_endPos : ∀ {s : String} {pos : s.Pos}, String.Pos.ofSliceTo (s.sliceTo pos).endPos = pos
-- Init.Data.Nat.Lemmas
Nat.max_assoc : ∀ (a b c : ℕ), max (max a b) c = max a (max b c)
-- Mathlib.RingTheory.Polynomial.Nilpotent
Polynomial.instIsLocalHomRingHomC : ∀ {R : Type u_1} [inst : CommRing R], IsLocalHom Polynomial.C
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.fundamentalSequence.match_1.splitter : (motive : Option ONote ⊕ (ℕ → ONote) → ℕ → Sort u_1) →
  (x : Option ONote ⊕ (ℕ → ONote)) →
    (x_1 : ℕ) →
      (Unit → motive (Sum.inl none) 0) →
        ((m : ℕ) → motive (Sum.inl none) m.succ) →
          ((a' : ONote) → motive (Sum.inl (some a')) 0) →
            ((a' : ONote) → (m : ℕ) → motive (Sum.inl (some a')) m.succ) →
              ((f : ℕ → ONote) → motive (Sum.inr f) 0) →
                ((f : ℕ → ONote) → (m : ℕ) → motive (Sum.inr f) m.succ) → motive x x_1
-- Mathlib.Order.WithBot
WithBot.decidableEq : {α : Type u_1} → [DecidableEq α] → DecidableEq (WithBot α)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.one_sub_prime_cpow_ne_zero : ∀ {p : ℕ}, Nat.Prime p → ∀ {s : ℂ}, 1 < s.re → 1 - ↑p ^ (-s) ≠ 0
-- Init.Omega.Constraint
Option.merge.eq_2 : ∀ {α : Type u_1} (fn : α → α → α) (x_2 : α), Option.merge fn (some x_2) none = some x_2
-- Mathlib.Algebra.Lie.UniversalEnveloping
UniversalEnvelopingAlgebra.Rel.lie_compat : ∀ {R : Type u₁} {L : Type u₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (x y : L),
  UniversalEnvelopingAlgebra.Rel R L ((TensorAlgebra.ι R) ⁅x, y⁆ + (TensorAlgebra.ι R) y * (TensorAlgebra.ι R) x)
    ((TensorAlgebra.ι R) x * (TensorAlgebra.ι R) y)
-- Init.Grind.ToIntLemmas
Lean.Grind.IntInterval.hi?.eq_1 : ∀ (lo hi : ℤ), (Lean.Grind.IntInterval.co lo hi).hi? = some hi
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.fromSpecStalk_appTop : ∀ {X : AlgebraicGeometry.Scheme} {x : ↥X},
  AlgebraicGeometry.Scheme.Hom.appTop (X.fromSpecStalk x) =
    CategoryTheory.CategoryStruct.comp (X.presheaf.germ ⊤ x trivial)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.stalk x)).inv
        ((AlgebraicGeometry.Spec (X.presheaf.stalk x)).presheaf.map (CategoryTheory.homOfLE ⋯).op))
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
PresheafOfModules.instPreservesLimitsOfShapeFunctorOppositeAbToPresheaf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (J : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J] [Small.{v, u₂} J],
  CategoryTheory.Limits.PreservesLimitsOfShape J (PresheafOfModules.toPresheaf R)
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- `(1 + t/n + o(1/n)) ^ n → exp t` for `t ∈ ℂ`.  -/
Complex.tendsto_pow_exp_of_isLittleO_sub_add_div : ∀ {f : ℕ → ℂ} (t : ℂ),
  ((fun n => f n - (1 + t / ↑n)) =o[Filter.atTop] fun n => 1 / ↑n) →
    Filter.Tendsto (fun n => f n ^ n) Filter.atTop (nhds (Complex.exp t))
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.IsStableUnderRetracts.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C},
  (∀ {X Y : C} (x : CategoryTheory.Retract X Y), P Y → P X) → P.IsStableUnderRetracts
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_insert_le_minKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k} {km kmi : α},
  t.minKey? = some km →
    (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.minKey?.get ⋯ = kmi → (compare kmi km).isLE = true
-- Mathlib.Topology.MetricSpace.Holder
HolderOnWith.edist_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal} {f : X → Y}
  {s : Set X}, HolderOnWith C r f s → ∀ {x y : X}, x ∈ s → y ∈ s → edist (f x) (f y) ≤ ↑C * edist x y ^ ↑r
-- Batteries.Data.List.Lemmas
List.prod_concat : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α] [Std.LawfulIdentity (fun x1 x2 => x1 * x2) 1]
  [Std.Associative fun x1 x2 => x1 * x2] {l : List α} {a : α}, (l.concat a).prod = l.prod * a
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentColorOptions.mk.sizeOf_spec : ∀ (toWorkDoneProgressOptions : Lean.Lsp.WorkDoneProgressOptions),
  sizeOf { toWorkDoneProgressOptions := toWorkDoneProgressOptions } = 1 + sizeOf toWorkDoneProgressOptions
-- Mathlib.Topology.Order
isClosed_induced_iff' : ∀ {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {f : α → β} {s : Set α},
  IsClosed s ↔ ∀ (a : α), f a ∈ closure (f '' s) → a ∈ s
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleIso_hom_app_hom₃ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] {F₁ F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) [inst_4 : F₁.CommShift ℤ]
  [inst_5 : F₂.CommShift ℤ] [inst_6 : CategoryTheory.NatTrans.CommShift e.hom ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Functor.mapTriangleIso e).hom.app X).hom₃ = e.hom.app X.obj₃
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.IsSubwalk.concat : ∀ {V : Type u_1} {G : SimpleGraph V} {u v u' v' w : V} {p : G.Walk u v} {q : G.Walk u' v'},
  p.IsSubwalk q → ∀ (h : G.Adj v' w), p.IsSubwalk (q.concat h)
-- Mathlib.Data.Ordmap.Ordset
_private.Mathlib.Data.Ordmap.Ordset.0.Ordnode.adjustWith.match_1.eq_1 : ∀ {α : Type u_1} (motive : Ordnode α → Sort u_2) (h_1 : Unit → motive Ordnode.nil)
  (h_2 :
    (_t : Ordnode α) →
      (sz : ℕ) →
        (l : Ordnode α) → (y : α) → (r : Ordnode α) → _t = Ordnode.node sz l y r → motive (Ordnode.node sz l y r)),
  (match Ordnode.nil with
    | Ordnode.nil => h_1 ()
    | _t@h:(Ordnode.node sz l y r) => h_2 _t sz l y r h) =
    h_1 ()
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.comap_carrier : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : CompleteLatticeHom α β)
  (L : CompleteSublattice β), (CompleteSublattice.comap f L).carrier = ⇑f ⁻¹' ↑L
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_castLE_of_eq : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {m n : ℕ} (h : m = n) {h' : m ≤ n}
  {φ : L.BoundedFormula α m} {v : α → M} {xs : Fin n → M},
  (FirstOrder.Language.BoundedFormula.castLE h' φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.cast h)
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.HasFiniteRange.zero : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Semiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂], LinearMap.HasFiniteRange 0
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.ω_mul_ω : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [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} {b : P.Base}
  [inst_5 : DecidableEq ι] [inst_6 : Fintype ι], RootPairing.GeckConstruction.ω b * RootPairing.GeckConstruction.ω b = 1
-- Mathlib.Algebra.DirectSum.Module
/-- Create the direct sum given a family `M` of `R` modules indexed over `ι`.  -/
DirectSum.lmk : (R : Type u) →
  [inst : Semiring R] →
    (ι : Type v) →
      (M : ι → Type w) →
        [inst_1 : (i : ι) → AddCommMonoid (M i)] →
          [inst_2 : (i : ι) → Module R (M i)] →
            [DecidableEq ι] → (s : Finset ι) → ((i : ↑↑s) → M ↑i) →ₗ[R] DirectSum ι fun i => M i
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.coe_continuous : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  (f : ContinuousMultilinearMap R M₁ M₂), Continuous ⇑f
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.Matroidᵣ.ofMatroid.sizeOf_spec : ∀ {α : Type u_2} [inst : SizeOf α] (toMatroid : Matroid α), sizeOf { toMatroid := toMatroid } = 1 + sizeOf toMatroid
-- Init.Data.Slice.Array.Lemmas
_private.Init.Data.Slice.Array.Lemmas.0.Std.IterStep.successor.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Std.IterStep α β → Sort u_3) (it : α)
  (h_1 : (it : α) → (out : β) → motive (Std.IterStep.yield it out)) (h_2 : (it : α) → motive (Std.IterStep.skip it))
  (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it with
    | Std.IterStep.yield it out => h_1 it out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_2 it