mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.foldrM_eq_foldrM_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} {δ : Type w} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : α → δ → m δ} {init : δ}, Std.TreeSet.foldrM f init t = List.foldrM f init t.toList
-- Mathlib.LinearAlgebra.TensorProduct.Defs
/-- Given two modules over a commutative semiring `R`, if one of the factors carries a
(distributive) action of a second type of scalars `R'`, which commutes with the action of `R`, then
the tensor product (over `R`) carries an action of `R'`.

This instance defines this `R'` action in the case that it is the left module which has the `R'`
action. Two natural ways in which this situation arises are:
* Extension of scalars
* A tensor product of a group representation with a module not carrying an action

Note that in the special case that `R = R'`, since `R` is commutative, we just get the usual scalar
action on a tensor product of two modules. This special case is important enough that, for
performance reasons, we define it explicitly below.  -/
TensorProduct.leftHasSMul : {R : Type u_1} →
  {R' : Type u_4} →
    [inst : CommSemiring R] →
      [inst_1 : Monoid R'] →
        {M : Type u_7} →
          {N : Type u_8} →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : DistribMulAction R' M] →
                  [inst_5 : Module R M] → [inst_6 : Module R N] → [SMulCommClass R R' M] → SMul R' (TensorProduct R M N)
-- Lean.Meta.SynthInstance
_private.Lean.Meta.SynthInstance.0.Lean.Meta.PreprocessKind.mvarsOutputParams.sizeOf_spec : sizeOf Lean.Meta.PreprocessKind.mvarsOutputParams✝ = 1
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.refl_h₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂), (CategoryTheory.ShortComplex.Homotopy.refl φ).h₁ = 0
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.sub : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {f₁ f₂ : α → E'}, f₁ =o[l] g → f₂ =o[l] g → (fun x => f₁ x - f₂ x) =o[l] g
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.homEquiv₀_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (a : X ⟶ Y),
  CategoryTheory.Abelian.Ext.homEquiv₀.symm a = CategoryTheory.Abelian.Ext.mk₀ a
-- Mathlib.Algebra.Group.Commute.Hom
AddCommute.map : ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Add M] [inst_1 : Add N] {x y : M} [inst_2 : FunLike F M N]
  [AddHomClass F M N], AddCommute x y → ∀ (f : F), AddCommute (f x) (f y)
-- Mathlib.Data.PNat.Defs
PNat.toPNat'_coe : ∀ {n : ℕ}, 0 < n → ↑n.toPNat' = n
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
/-- A family of functors is jointly faithful if whenever two morphisms `f : X ⟶ Y`
and `g : X ⟶ Y` become equal after applying all functors `F i`, then `f = g`.  -/
CategoryTheory.JointlyFaithful : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_4, u_1} C] →
    {I : Type u_2} →
      {D : I → Type u_3} →
        [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] →
          ((i : I) → CategoryTheory.Functor C (D i)) → Prop
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.toAffineLift_of_Z_eq_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hP : W.NonsingularLift ⟦P⟧),
  P 2 = 0 → { point := ⟦P⟧, nonsingular := hP }.toAffineLift = 0
-- Mathlib.Analysis.Convex.Deriv
/-- If a function `f` is continuous on a convex set `D ⊆ ℝ` and `f''` is strictly positive on the
interior, then `f` is strictly convex on `D`.
Note that we don't require twice differentiability explicitly as it is already implied by the second
derivative being strictly positive, except at at most one point.  -/
strictConvexOn_of_deriv2_pos : ∀ {D : Set ℝ},
  Convex ℝ D → ∀ {f : ℝ → ℝ}, ContinuousOn f D → (∀ x ∈ interior D, 0 < deriv^[2] f x) → StrictConvexOn ℝ D f
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Monad.forgetCreatesColimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} →
      [CategoryTheory.Limits.PreservesColimitsOfSize.{v, u, v₁, v₁, u₁, u₁} T.toFunctor] →
        CategoryTheory.CreatesColimitsOfSize.{v, u, v₁, v₁, max u₁ v₁, u₁} T.forget
-- Init.Data.UInt.Lemmas
USize.toNat_ofFin : ∀ (x : Fin USize.size), (USize.ofFin x).toNat = ↑x
-- Mathlib.RingTheory.NormalClosure
Ring.instIsDomainNormalClosure : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] [inst_5 : Module.IsTorsionFree R S], IsDomain (Ring.NormalClosure R S)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Subtracting a multiple of the second vector passed to `oangle` from the first vector does
not change the sign of the angle.  -/
Orientation.oangle_sign_sub_smul_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V) (r : ℝ), (o.oangle (x - r • y) y).sign = (o.oangle x y).sign
-- Batteries.Data.Random.MersenneTwister
_private.Batteries.Data.Random.MersenneTwister.0.Batteries.Random.MersenneTwister.Config.lMask : (cfg : Batteries.Random.MersenneTwister.Config) → BitVec cfg.wordSize
-- Lean.Environment
Lean.Environment.imports : Lean.Environment → Array Lean.Import
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey!_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k},
      Std.Internal.List.maxKey! (Std.Internal.List.insertEntryIfNew k v l) =
        (Std.Internal.List.maxKey? l).elim k fun k' => if compare k' k = Ordering.lt then k else k'
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Seed.mk.sizeOf_spec : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] [inst_12 : SizeOf K] [inst_13 : SizeOf M] [inst_14 : SizeOf R]
  (toArchimedeanStrata : HahnEmbedding.ArchimedeanStrata K M)
  (coeff : (c : FiniteArchimedeanClass M) → ↥(toArchimedeanStrata.stratum c) →ₗ[K] R)
  (strictMono_coeff : ∀ (c : FiniteArchimedeanClass M), StrictMono ⇑(coeff c)),
  sizeOf { toArchimedeanStrata := toArchimedeanStrata, coeff := coeff, strictMono_coeff := strictMono_coeff } =
    1 + sizeOf toArchimedeanStrata
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.distinct_keys : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → List.Pairwise (fun a b => (a == b) = false) m.keys
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKeyD_le_minKeyD_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).isEmpty = false → ∀ {fallback : α}, (cmp (t.minKeyD fallback) ((t.erase k).minKeyD fallback)).isLE = true
-- Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
HasDerivWithinAt.clog : ∀ {f : ℂ → ℂ} {f' x : ℂ} {s : Set ℂ},
  HasDerivWithinAt f f' s x → f x ∈ Complex.slitPlane → HasDerivWithinAt (fun t => Complex.log (f t)) (f' / f x) s x
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.symmEquiv_apply_symm_apply : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (a : M),
  (LinearEquiv.symmEquiv e).symm a = e a
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
hasCardinalLT_iff_cardinal_mk_lt : ∀ (X : Type u) (κ : Cardinal.{u}), HasCardinalLT X κ ↔ Cardinal.mk X < κ
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.induction_on : ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {C : α ⧸ s → Prop} (x : α ⧸ s), (∀ (z : α), C ↑z) → C x
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ),
  ¬ProbabilityTheory.IsSFiniteKernel κ → κ.compProd η = 0
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.Rel.smulOfTower : ∀ {R : Type u} {X : Type v} [inst : CommRing R] {S : Type u_1} [inst_1 : Monoid S] [inst_2 : DistribMulAction S R]
  [IsScalarTower S R R] (t : S) (a b : FreeNonUnitalNonAssocAlgebra R X),
  FreeLieAlgebra.Rel R X a b → FreeLieAlgebra.Rel R X (t • a) (t • b)
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.factors_subsingleton : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [Subsingleton α]
  {a : Associates α}, a.factors = ⊤
-- Mathlib.Algebra.Group.Hom.Defs
ne_zero_of_map : ∀ {R : Type u_10} {S : Type u_11} {F : Type u_12} [inst : Zero R] [inst_1 : Zero S] [inst_2 : FunLike F R S]
  [ZeroHomClass F R S] {f : F} {x : R}, f x ≠ 0 → x ≠ 0
-- Std.Time.Zoned.Database.PosixTz
_private.Std.Time.Zoned.Database.PosixTz.0.Std.Time.TimeZone.posixParseSpec : Std.Internal.Parsec.String.Parser Std.Time.TimeZone.TransitionSpec
-- Init.Prelude
/-- Converts a natural number to a `USize`. Requires a proof that the number is small enough to be
representable without overflow.

This function is overridden at runtime with an efficient implementation.
 -/
USize.ofNatLT : (n : ℕ) → n < USize.size → USize
-- Mathlib.Analysis.Convex.Hull
convexHull_eq_iInter : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] (s : Set E), (convexHull 𝕜) s = ⋂ t, ⋂ (_ : s ⊆ t), ⋂ (_ : Convex 𝕜 t), t
-- Mathlib.Order.Ideal
Order.Ideal.instInfSet : {P : Type u_1} → [inst : SemilatticeSup P] → [OrderBot P] → InfSet (Order.Ideal P)
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.matchesAt_iff_splits : ∀ {pat s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.MatchesAt pat pos ↔ ∃ t₁ t₂, pos.Splits t₁ (pat.copy ++ t₂)
-- Init.Tactics
/-- `case'` is similar to the `case tag => tac` tactic, but does not ensure the goal
has been solved after applying `tac`, nor admits the goal if `tac` failed.
Recall that `case` closes the goal using `sorry` when `tac` fails, and
the tactic execution is not interrupted.
 -/
Lean.Parser.Tactic.case' : Lean.ParserDescr
-- Mathlib.CategoryTheory.LiftingProperties.Limits
CategoryTheory.instHasLiftingPropertySnd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Y Z W : C} {g : Z ⟶ W} {t : Y ⟶ W}
  [inst_1 : CategoryTheory.Limits.HasPullback g t] {T₁ T₂ : C} (p : T₁ ⟶ T₂) [CategoryTheory.HasLiftingProperty p g],
  CategoryTheory.HasLiftingProperty p (CategoryTheory.Limits.pullback.snd g t)
-- Batteries.Data.Random.MersenneTwister
Batteries.Random.MersenneTwister.State.mk.injEq : ∀ {cfg : Batteries.Random.MersenneTwister.Config} (data : Vector (BitVec cfg.wordSize) cfg.stateSize)
  (index : Fin cfg.stateSize) (data_1 : Vector (BitVec cfg.wordSize) cfg.stateSize) (index_1 : Fin cfg.stateSize),
  ({ data := data, index := index } = { data := data_1, index := index_1 }) = (data = data_1 ∧ index = index_1)
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.ihom.ev_coev_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A B : C)
  [inst_2 : CategoryTheory.Closed A] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A ((CategoryTheory.ihom.coev A).app B))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.ihom.ev A).app (CategoryTheory.MonoidalCategoryStruct.tensorObj A B)) h) =
    h
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.addHaarScalarFactor_smul_congr : ∀ {G : Type u_1} {A : Type u_2} [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A]
  [inst_3 : MeasurableSpace A] [inst_4 : TopologicalSpace A] [inst_5 : BorelSpace A] [inst_6 : IsTopologicalAddGroup A]
  [LocallyCompactSpace A] [inst_8 : ContinuousConstSMul G A] (μ : MeasureTheory.Measure A) {ν : MeasureTheory.Measure A}
  [inst_9 : μ.IsAddHaarMeasure] [inst_10 : ν.IsAddHaarMeasure] (g : Gᵈᵐᵃ),
  μ.addHaarScalarFactor (g • μ) = ν.addHaarScalarFactor (g • ν)
-- Mathlib.Probability.Martingale.OptionalSampling
MeasureTheory.IsStoppingTime.measurableSpace.congr_simp : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {f f_1 : MeasureTheory.Filtration ι m}
  (e_f : f = f_1) {τ τ_1 : Ω → WithTop ι} (e_τ : τ = τ_1) (hτ : MeasureTheory.IsStoppingTime f τ),
  hτ.measurableSpace = ⋯.measurableSpace
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.mapArrowRight_comp : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {f₁ : CategoryTheory.Arrow C₁}
  {f₂ f₂' : CategoryTheory.Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom)
  {f₂'' : CategoryTheory.Arrow C₂} (sq₁₂'' : F.PushoutObjObj f₁.hom f₂''.hom) (sq : f₂ ⟶ f₂') (sq' : f₂' ⟶ f₂''),
  CategoryTheory.CategoryStruct.comp (sq₁₂.mapArrowRight sq₁₂' sq) (sq₁₂'.mapArrowRight sq₁₂'' sq') =
    sq₁₂.mapArrowRight sq₁₂'' (CategoryTheory.CategoryStruct.comp sq sq')
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_le_one_iff : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalRing R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A]
  (f : R → R) (a : A),
  autoParam (ContinuousOn f (spectrum R a)) cfc_le_one_iff._auto_1 →
    autoParam (p a) cfc_le_one_iff._auto_3 → (cfc f a ≤ 1 ↔ ∀ x ∈ spectrum R a, f x ≤ 1)
-- Mathlib.Data.Set.Card
Set.cast_ncard_sdiff : ∀ {α : Type u_1} {s t : Set α} {R : Type u_3} [inst : AddGroupWithOne R],
  s ⊆ t → t.Finite → ↑(t \ s).ncard = ↑t.ncard - ↑s.ncard
-- Mathlib.Data.DFinsupp.Interval
DFinsupp.instLocallyFiniteOrder : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [DecidableEq ι] →
      [(i : ι) → DecidableEq (α i)] →
        [inst : (i : ι) → PartialOrder (α i)] →
          [inst_1 : (i : ι) → Zero (α i)] → [(i : ι) → LocallyFiniteOrder (α i)] → LocallyFiniteOrder (Π₀ (i : ι), α i)
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.mk : (toLinOrd : LinOrd) → [nonempty : Nonempty ↑toLinOrd] → [fintype : Fintype ↑toLinOrd] → NonemptyFinLinOrd
-- Mathlib.Algebra.Group.Action.Defs
Function.Injective.addAction.eq_1 : ∀ {M : Type u_1} {α : Type u_5} {β : Type u_6} [inst : AddMonoid M] [inst_1 : AddAction M α] [inst_2 : VAdd M β]
  (f : β → α) (hf : Function.Injective f) (smul : ∀ (c : M) (x : β), f (c +ᵥ x) = c +ᵥ f x),
  Function.Injective.addAction f hf smul = { toVAdd := inst_2, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.Algebra.Ring.Subring.Defs
/-- Turn a `Subring` into a `NonUnitalSubring` by forgetting that it contains `1`.  -/
Subring.toNonUnitalSubring : {R : Type u} → [inst : NonAssocRing R] → Subring R → NonUnitalSubring R
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.WorkGroup : Type
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- The characterization of the orthogonal projection.  -/
Submodule.starProjection_inner_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] (v w : E), w ∈ K → inner 𝕜 (v - K.starProjection v) w = 0
-- Mathlib.Algebra.Order.Hom.Basic
MulRingSeminormClass.toMonoidHomClass : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : NonAssocRing α} {inst_1 : Semiring β}
  {inst_2 : PartialOrder β} {inst_3 : FunLike F α β} [self : MulRingSeminormClass F α β], MonoidHomClass F α β
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.isIso_of_components : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (f : C₁ ⟶ C₂) [∀ (n : ι), CategoryTheory.IsIso (f.f n)], CategoryTheory.IsIso f
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.Context.symPrios : Lean.Meta.Grind.NormalizePattern.Context✝ → Lean.Meta.Grind.SymbolPriorities
-- Mathlib.Topology.Order.IsLUB
exists_seq_strictAnti_strictMono_tendsto : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [FirstCountableTopology α] {x y : α},
  x < y →
    ∃ u v,
      StrictAnti u ∧
        StrictMono v ∧
          (∀ (k : ℕ), u k ∈ Set.Ioo x y) ∧
            (∀ (l : ℕ), v l ∈ Set.Ioo x y) ∧
              (∀ (k l : ℕ), u k < v l) ∧ Filter.Tendsto u Filter.atTop (nhds x) ∧ Filter.Tendsto v Filter.atTop (nhds y)
-- Std.Data.DHashMap.Basic
/-- Computes the difference of the given hash maps.

This function always iterates through the smaller map, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.DHashMap.diff : {α : Type u} →
  {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.DHashMap α β → Std.DHashMap α β → Std.DHashMap α β
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to0.trAux.eq_6 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (M : Λ → Turing.TM1.Stmt Γ Λ σ) (s : Γ) (x : σ),
  Turing.TM1to0.trAux M s Turing.TM1.Stmt.halt x = ((none, x), Turing.TM0.Stmt.write s)
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isLittleO_iff_forall_isBigOWith`.

---

Definition of `IsLittleO` in terms of `IsBigOWith`.  -/
Asymptotics.IsLittleO.forall_isBigOWith : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {l : Filter α},
  f =o[l] g → ∀ ⦃c : ℝ⦄, 0 < c → Asymptotics.IsBigOWith c l f g
-- Mathlib.RingTheory.MvPolynomial.Groebner
/-- Division by a *set* of multivariate polynomials
whose leading coefficients are invertible with respect to a monomial order  -/
MonomialOrder.div_set : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] {B : Set (MvPolynomial σ R)},
  (∀ b ∈ B, IsUnit (m.leadingCoeff b)) →
    ∀ (f : MvPolynomial σ R),
      ∃ g r,
        f = (Finsupp.linearCombination (MvPolynomial σ R) fun b => ↑b) g + r ∧
          (∀ (b : ↑B), m.toSyn (m.degree (↑b * g b)) ≤ m.toSyn (m.degree f)) ∧ ∀ c ∈ r.support, ∀ b ∈ B, ¬m.degree b ≤ c
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodeSigma.match_1.splitter : (n : ℕ) →
  (f : Fin (n + 1) → ℕ) →
    (motive : Fin (Fin.sum fun x => f x.succ) → Sort u_1) →
      (x : Fin (Fin.sum fun x => f x.succ)) →
        ((k : ℕ) → (hk : k < Fin.sum fun x => f x.succ) → motive ⟨k, hk⟩) → motive x
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
/-- Constructor for the type of nondegenerate simplices which
do not belong to a given subcomplex of a simplicial set.  -/
SSet.Subcomplex.N.mk : {X : SSet} →
  {A : X.Subcomplex} →
    {n : ℕ} →
      (x : X.obj (Opposite.op { len := n })) → x ∈ X.nonDegenerate n → x ∉ A.obj (Opposite.op { len := n }) → A.N
-- Mathlib.Logic.Basic
/-- **Alias** of `Classical.em`. -/
em : ∀ (p : Prop), p ∨ ¬p
-- Mathlib.Order.Heyting.Basic
sup_le_of_le_sdiff_left : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, b ≤ c \ a → a ≤ c → a ⊔ b ≤ c
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.denote : {α : Type u_1} → [Lean.Grind.IntModule α] → Lean.Grind.Linarith.Context α → Lean.Grind.Linarith.Expr → α
-- Mathlib.Tactic.Algebra.Basic
/-- Evaluate the sum of two normalized expressions in `R` using `ring`.  -/
Mathlib.Tactic.Algebra.RingCompute.add : {u v : Lean.Level} →
  {R : Q(Type u)} →
    {A : Q(Type v)} →
      {sR : Q(CommSemiring «$R»)} →
        {sA : Q(CommSemiring «$A»)} →
          (sAlg : Q(Algebra «$R» «$A»)) →
            Mathlib.Tactic.Ring.Common.Cache sR →
              {a b : Q(«$A»)} →
                Mathlib.Tactic.Algebra.BaseType sAlg a →
                  Mathlib.Tactic.Algebra.BaseType sAlg b →
                    Lean.MetaM
                      (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Algebra.BaseType sAlg) q(«$a» + «$b») ×
                        Option Q(Mathlib.Meta.NormNum.IsNat («$a» + «$b») 0))
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `L` are linearly disjoint over `F`, one of them is algebraic,
then `[L(A) : L] = [A : F]`.  -/
IntermediateField.LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L →
    Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L →
      Module.rank L ↥(IntermediateField.adjoin L ↑A) = Module.rank F ↥A
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isLimitConeUnopOfCocone_lift : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c)
  (s : CategoryTheory.Limits.Cone F.unop),
  (CategoryTheory.Limits.isLimitConeUnopOfCocone F hc).lift s =
    (hc.desc (CategoryTheory.Limits.coconeOfConeUnop s)).unop
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.opOrderIso_apply : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (I : TwoSidedIdeal R), TwoSidedIdeal.opOrderIso I = I.op
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_neg_le : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Neg α] {s : Finset α}, (-s).card ≤ s.card
-- Lean.Server.Requests
Lean.Server.lookupStatefulLspRequestHandler : String → BaseIO (Option Lean.Server.StatefulRequestHandler)
-- Std.Do.SPred.Laws
Std.Do.SPred.bientails.eq_1 : ∀ (P_2 Q_2 : Std.Do.SPred []), (P_2 ⊣⊢ₛ Q_2) = (P_2.down ↔ Q_2.down)
-- Mathlib.Tactic.NormNum.LegendreSymbol
/-- This evaluates `r := jacobiSym a b` and produces a proof term for the equality.
This is done by reducing to `r := jacobiSymNat (a % b) b`.  -/
Mathlib.Meta.NormNum.proveJacobiSym : (ea : Q(ℤ)) → (eb : Q(ℕ)) → (er : Q(ℤ)) × Q(jacobiSym «$ea» «$eb» = «$er»)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.insertMany_nil : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp], t.insertMany [] = t
-- Mathlib.Data.List.TakeDrop
_private.Mathlib.Data.List.TakeDrop.0.List.span.loop_eq_take_drop : ∀ {α : Type u} (p : α → Bool) (l₁ l₂ : List α),
  List.span.loop p l₁ l₂ = (l₂.reverse ++ List.takeWhile p l₁, List.dropWhile p l₁)