mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.Extr
IsMaxFilter.sup : ∀ {α : Type u} {β : Type v} [inst : SemilatticeSup β] {f g : α → β} {a : α} {l : Filter α},
  IsMaxFilter f l a → IsMaxFilter g l a → IsMaxFilter (fun x => f x ⊔ g x) l a
-- Mathlib.Logic.Function.Defs
_private.Mathlib.Logic.Function.Defs.0.Function.«term_∘₂_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Group.Pi.Lemmas
AddMonoidHom.piMap_apply : ∀ {ι : Type u_1} {M : ι → Type u_3} {N : ι → Type u_4} [inst : (i : ι) → AddZeroClass (M i)]
  [inst_1 : (i : ι) → AddZeroClass (N i)] (g : (i : ι) → M i →+ N i) (x : (i : ι) → M i) (i : ι),
  (AddMonoidHom.piMap g) x i = (g i) (x i)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : BEq α] [Std.LawfulBEqCmp cmp] [Std.TransCmp cmp]
  {k : α}, t.toList.contains k = t.contains k
-- Mathlib.Data.Finset.Lattice.Fold
Finset.exists_mem_eq_inf : ∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] [inst_1 : OrderTop α] (s : Finset ι),
  s.Nonempty → ∀ (f : ι → α), ∃ i ∈ s, s.inf f = f i
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.source_inter_preimage_inv_preimage : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (s : Set X), e.source ∩ ↑e ⁻¹' ↑e.symm ⁻¹' s = e.source ∩ s
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- **Alias** of `CategoryTheory.Limits.HasColimit.ι_isoOfEquivalence_hom`. -/
CategoryTheory.Limits.HasColimit.isoOfEquivalence_hom_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasColimit F] {G : CategoryTheory.Functor K C}
  [inst_4 : CategoryTheory.Limits.HasColimit G] (e : J ≌ K) (w : e.functor.comp G ≅ F) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j)
      (CategoryTheory.Limits.HasColimit.isoOfEquivalence e w).hom =
    CategoryTheory.CategoryStruct.comp (F.map (e.unit.app j))
      (CategoryTheory.CategoryStruct.comp (w.inv.app ((e.functor.comp e.inverse).obj j))
        (CategoryTheory.Limits.colimit.ι G (e.functor.obj ((e.functor.comp e.inverse).obj j))))
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.uncurrySum_apply : ∀ {R : Type uR} {ι : Type uι} {ι' : Type uι'} {M₂ : Type v₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : Module R M₂] {N : ι ⊕ ι' → Type u_1} [inst_3 : (i : ι ⊕ ι') → AddCommMonoid (N i)]
  [inst_4 : (i : ι ⊕ ι') → Module R (N i)]
  (g : MultilinearMap R (fun i => N (Sum.inl i)) (MultilinearMap R (fun i => N (Sum.inr i)) M₂))
  (u : (i : ι ⊕ ι') → N i), g.uncurrySum u = (g fun i => u (Sum.inl i)) fun i' => u (Sum.inr i')
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
HasLineDerivWithinAt.mono_of_mem_nhdsWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : E → F}
  {f' : F} {s t : Set E} {x v : E},
  HasLineDerivWithinAt 𝕜 f f' t x v → t ∈ nhdsWithin x s → HasLineDerivWithinAt 𝕜 f f' s x v
-- Mathlib.CategoryTheory.Limits.Final
/-- The hypotheses also imply that `G` is final, see `final_of_comp_full_faithful'`.  -/
CategoryTheory.Functor.final_of_comp_full_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [G.Full] [G.Faithful] [(F.comp G).Final], F.Final
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Complex.hasDerivAt_logTaylor : ∀ (n : ℕ) (z : ℂ), HasDerivAt (Complex.logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
-- Mathlib.Tactic.NormNum.LegendreSymbol
/-- This evaluates `r := jacobiSymNat a b` recursively using quadratic reciprocity
and produces a proof term for the equality, assuming that `a < b` and `b` is odd.  -/
Mathlib.Meta.NormNum.proveJacobiSymOdd : (ea eb : Q(ℕ)) → (er : Q(ℤ)) × Q(Mathlib.Meta.NormNum.jacobiSymNat «$ea» «$eb» = «$er»)
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- Given `S : μ.FiniteSpanningSetsIn {s | MeasurableSet s}`,
`FiniteSpanningSetsIn.disjointed` provides a `FiniteSpanningSetsIn {s | MeasurableSet s}`
such that its underlying sets are pairwise disjoint.  -/
MeasureTheory.Measure.FiniteSpanningSetsIn.disjointed : {α : Type u_1} →
  {m0 : MeasurableSpace α} →
    {μ : MeasureTheory.Measure α} →
      μ.FiniteSpanningSetsIn {s | MeasurableSet s} → μ.FiniteSpanningSetsIn {s | MeasurableSet s}
-- Mathlib.Topology.Algebra.Group.Basic
isOpenMap_add_right : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] (a : G),
  IsOpenMap fun x => x + a
-- Mathlib.Lean.Expr.Basic
/-- Update the mutual-block `all` field of a `ConstantInfo`.

This applies to declaration kinds where `ConstantInfo.all` is stored directly.
 -/
Lean.ConstantInfo.updateAll : Lean.ConstantInfo → List Lean.Name → Lean.ConstantInfo
-- Mathlib.RingTheory.Localization.FractionRing
FractionRing.instDecidableEq : {R : Type u_1} → [inst : CommRing R] → [DecidableEq R] → DecidableEq (FractionRing R)
-- Mathlib.Algebra.Order.Group.Cone
GroupCone.instGroupConeClass : ∀ (G : Type u_1) [inst : CommGroup G], GroupConeClass (GroupCone G) G
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
DerivedCategory.instIsLEObjCochainComplexIntQOfIsLE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (K : CochainComplex C ℤ) (n : ℤ) [K.IsLE n], (DerivedCategory.Q.obj K).IsLE n
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
FreeAbelianGroup.support_nsmul : ∀ {X : Type u_1} (k : ℕ), k ≠ 0 → ∀ (a : FreeAbelianGroup X), (k • a).support = a.support
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.pairwise_disjoint_vadd_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {s : Set β},
  Pairwise (Function.onFun Disjoint fun a => a +ᵥ s) ↔ ∀ (a : α), ((a +ᵥ s) ∩ s).Nonempty → a = 0
-- Mathlib.MeasureTheory.Constructions.UnitInterval
unitInterval.volume_uIoo : ∀ (x y : ↑unitInterval), MeasureTheory.volume (Set.uIoo x y) = edist y x
-- Mathlib.Algebra.Quandle
Rack.act'_apply : ∀ {R : Type u_1} [inst : Rack R] (x y : R), (Rack.act' x) y = Shelf.act x y
-- Mathlib.Analysis.Normed.Group.Ultra
/-- All triangles are isosceles in an ultrametric normed additive group.  -/
IsUltrametricDist.norm_sub_eq_max_of_norm_sub_ne_norm_sub : ∀ {S : Type u_1} [inst : SeminormedAddGroup S] [IsUltrametricDist S] (x y z : S),
  ‖x - y‖ ≠ ‖y - z‖ → ‖x - z‖ = max ‖x - y‖ ‖y - z‖
-- Lean.Elab.Do.Control
/-- Substack at which the `break` handler was installed, if any.  -/
Lean.Elab.Do.EffectForwarder.breakBase? : Lean.Elab.Do.EffectForwarder → Option Lean.Elab.Do.ControlStack
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instAdd : {R : Type u_3} → {c₁ c₂ c₃ : R} → [Add R] → Add (QuaternionAlgebra R c₁ c₂ c₃)
-- Lean.Message
Lean.MessageData.instCoeOptionExpr : Coe (Option Lean.Expr) Lean.MessageData
-- Mathlib.LinearAlgebra.TensorProduct.Finiteness
/-- For a finite subset `s` of `M ⊗[R] N`, there are finitely generated
submodules `M'` and `N'` of `M` and `N`, respectively, such that `s` is contained in the image
of `M' ⊗[R] N'` in `M ⊗[R] N`.

In particular, every element of a tensor product lies in the tensor product of some finite
submodules.  -/
TensorProduct.exists_finite_submodule_of_setFinite : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (s : Set (TensorProduct R M N)),
  s.Finite → ∃ M' N', Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(TensorProduct.mapIncl M' N').range
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termZ₂ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.sigmaFunctor_map_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C] {X Y : C}
  (f : X ⟶ Y) (T : Type w),
  (CategoryTheory.Limits.sigmaFunctor.map f).app T = CategoryTheory.Limits.Sigma.map fun x => f
-- Mathlib.Data.Set.Card
Set.ncard_eq_four : ∀ {α : Type u_1} {s : Set α}, s.ncard = 4 ↔ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
-- Mathlib.Data.List.Infix
List.get_tails : ∀ {α : Type u_1} (l : List α) (n : Fin l.tails.length), l.tails.get n = List.drop (↑n) l
-- Init.Data.List.Sublist
List.cons_sublist_cons : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, (a :: l₁).Sublist (a :: l₂) ↔ l₁.Sublist l₂
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.coeff_preΨ₄ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), W.preΨ₄.coeff 6 = 2
-- Mathlib.Analysis.Calculus.Deriv.Star
/-- If `f` has derivative `f'` at `z`, then `conj ∘ f ∘ conj` has derivative `conj f'` at
`conj z`.  -/
HasDerivAt.conj_conj : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {x : 𝕜} [NormedStarGroup 𝕜] {f : 𝕜 → 𝕜}
  {f' : 𝕜},
  HasDerivAt f f' x → HasDerivAt (⇑(starRingEnd 𝕜) ∘ f ∘ ⇑(starRingEnd 𝕜)) ((starRingEnd 𝕜) f') ((starRingEnd 𝕜) x)
-- Mathlib.Algebra.Group.Hom.Basic
/-- Given two mul morphisms `f`, `g` to a commutative semigroup, `f * g` is the mul morphism
sending `x` to `f x * g x`.  -/
MulHom.instMul : {M : Type u_2} → {N : Type u_3} → [inst : Mul M] → [inst_1 : CommSemigroup N] → Mul (M →ₙ* N)
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upperCrossingTime_stabilize : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n m : ℕ} {ω : Ω},
  n ≤ m → MeasureTheory.upperCrossingTime a b f N n ω = N → MeasureTheory.upperCrossingTime a b f N m ω = N
-- Mathlib.Condensed.Discrete.Module
CompHausLike.LocallyConstantModule.functor_map_hom_app_hom_apply_apply : ∀ {P : TopCat → Prop} (R : Type (max u w)) [inst : Ring R] [inst_1 : CompHausLike.HasExplicitFiniteCoproducts P]
  [inst_2 : CompHausLike.HasExplicitPullbacks P]
  (hs :
    ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f))
  {X Y : ModuleCat R} (f : X ⟶ Y) (S : (CompHausLike P)ᵒᵖ) (g : LocallyConstant ↑(Opposite.unop S).toTop ↑X)
  (a : ↑(Opposite.unop S).toTop),
  ((ModuleCat.Hom.hom (((CompHausLike.LocallyConstantModule.functor R hs).map f).hom.app S)) g) a =
    (ModuleCat.Hom.hom f) (g a)
-- Mathlib.Topology.Algebra.Support
range_subset_insert_image_tsupport : ∀ {X : Type u_1} {α : Type u_2} [inst : Zero α] [inst_1 : TopologicalSpace X] (f : X → α),
  Set.range f ⊆ insert 0 (f '' tsupport f)
-- Mathlib.Order.Interval.Finset.Basic
Finset.uIcc.eq_1 : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] (a b : α),
  Finset.uIcc a b = Finset.Icc (a ⊓ b) (a ⊔ b)
-- Mathlib.Util.AtLocation
/-- Stay silent if this action has no effect.  -/
Mathlib.Tactic.BehaviorIfUnchanged.silent : Mathlib.Tactic.BehaviorIfUnchanged
-- Mathlib.Algebra.Group.Submonoid.Operations
AddEquiv.addSubmonoidCongr.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M] {S T : AddSubmonoid M} (h : S = T),
  AddEquiv.addSubmonoidCongr h = { toEquiv := Equiv.setCongr ⋯, map_add' := ⋯ }
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.offset_eq_rawEndPos : ∀ {s : String} {p : s.Pos} {t₁ t₂ : String}, p.Splits t₁ t₂ → p.offset = t₁.rawEndPos
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.ModuleColimit.homEquiv'_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R}
  {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) {N : ModuleCat ↑cR.pt}
  (β : M.presheaf ⟶ (CategoryTheory.Functor.const Cᵒᵖ).obj (AddCommGrpCat.of ↑N)) {X : Cᵒᵖ} (x : ↑(M.obj X)),
  ((PresheafOfModules.ModuleColimit.homEquiv' hcR hcM).symm β) ((CategoryTheory.ConcreteCategory.hom (cM.ι.app X)) x) =
    (CategoryTheory.ConcreteCategory.hom (β.app X)) x
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_expMap_symm : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : K},
  x ≠ 0 →
    NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace
        (↑NumberField.mixedEmbedding.fundamentalCone.expMap.symm
          (NumberField.mixedEmbedding.normAtAllPlaces ((NumberField.mixedEmbedding K) x))) =
      NumberField.mixedEmbedding.logMap ((NumberField.mixedEmbedding K) x)
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α], sizeOf Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth = 1
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- Change-of-variables formula for `Ioi` integrals of scalar-valued functions  -/
MeasureTheory.integral_comp_mul_deriv_Ioi : ∀ {f f' g : ℝ → ℝ} {a : ℝ},
  ContinuousOn f (Set.Ici a) →
    Filter.Tendsto f Filter.atTop Filter.atTop →
      (∀ x ∈ Set.Ioi a, HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
        ContinuousOn g (f '' Set.Ioi a) →
          MeasureTheory.IntegrableOn g (f '' Set.Ici a) MeasureTheory.volume →
            MeasureTheory.IntegrableOn (fun x => (g ∘ f) x * f' x) (Set.Ici a) MeasureTheory.volume →
              ∫ (x : ℝ) in Set.Ioi a, (g ∘ f) x * f' x = ∫ (u : ℝ) in Set.Ioi (f a), g u
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.card_roots_eq_natDegree : ∀ {k : Type u} [inst : Field k] [IsAlgClosed k] {p : Polynomial k}, p.roots.card = p.natDegree
-- Mathlib.FieldTheory.KummerExtension
adjoinRootXPowSubCEquiv_root : ∀ {K : Type u} [inst : Field K] {n : ℕ} (hζ : (primitiveRoots n K).Nonempty) {a : K}
  (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) {L : Type u_1} [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] {α : L}
  (hα : α ^ n = (algebraMap K L) a),
  (adjoinRootXPowSubCEquiv hζ H hα) (AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)) = α
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.congr_right : ∀ {α : Type u} {m₁ m₂ m₃ : Std.HashSet.Raw α}, m₁.Equiv m₂ → (m₃.Equiv m₁ ↔ m₃.Equiv m₂)
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.equivSum_apply : ∀ {n : ℕ} (x : DihedralGroup n),
  DihedralGroup.equivSum x =
    match x with
    | DihedralGroup.r j => Sum.inl j
    | DihedralGroup.sr j => Sum.inr j
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
/-- Transfer creation of finite limits along a natural isomorphism in the functor.  -/
CategoryTheory.Limits.createsFiniteCoproductsOfNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G : CategoryTheory.Functor C D} →
          {h : F ≅ G} →
            [CategoryTheory.Limits.CreatesFiniteCoproducts F] → CategoryTheory.Limits.CreatesFiniteCoproducts G
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Zag.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] (j₁ j₂ : J),
  CategoryTheory.Zag j₁ j₂ = (Nonempty (j₁ ⟶ j₂) ∨ Nonempty (j₂ ⟶ j₁))
-- Mathlib.Analysis.Analytic.CPolynomialDef
CPolynomialOn.congr : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {s : Set E},
  IsOpen s → CPolynomialOn 𝕜 f s → Set.EqOn f g s → CPolynomialOn 𝕜 g s
-- Mathlib.LinearAlgebra.Dimension.Finite
exists_linearIndependent_of_le_rank : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ},
  ↑n ≤ Module.rank R M → ∃ f, LinearIndependent R f
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.addCustomEliminator : Lean.Name → Lean.AttributeKind → Bool → Lean.MetaM Unit
-- Mathlib.Algebra.Algebra.Defs
Algebra.algebra_ext_iff : ∀ {R : Type u_2} [inst : CommSemiring R] {A : Type u_3} [inst_1 : Semiring A] {P Q : Algebra R A},
  P = Q ↔ ∀ (r : R), (algebraMap R A) r = (algebraMap R A) r
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.shortComplexFunctor'_obj_X₁ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i j k : ι) (K : HomologicalComplex C c),
  ((HomologicalComplex.shortComplexFunctor' C c i j k).obj K).X₁ = K.X i
-- Init.Grind.Config
/-- Maximum number of steps performed by the `ring` solver.
A step is counted whenever one polynomial is used to simplify another,
weighted by the number of terms in the resulting polynomial.
 -/
Lean.Grind.Config.ringSteps : Lean.Grind.Config → ℕ
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- If `I ≠ 0`, then `val_v(I) = 0` for all but finitely many maximal ideals of `R`.  -/
FractionalIdeal.finite_factors' : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] {I : FractionalIdeal (nonZeroDivisors R) K},
  I ≠ 0 →
    ∀ {a : R} {J : Ideal R},
      I = FractionalIdeal.spanSingleton (nonZeroDivisors R) ((algebraMap R K) a)⁻¹ * ↑J →
        ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite,
          ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
              ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
            0
-- Mathlib.Data.Nat.Choose.Central
Nat.centralBinom_eq_two_mul_choose : ∀ (n : ℕ), n.centralBinom = (2 * n).choose n
-- Mathlib.FieldTheory.Perfect
Polynomial.rootsExpandPowToRoots_apply : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (p n : ℕ) [inst_2 : ExpChar R p] (f : Polynomial R)
  [inst_3 : DecidableEq R] (x : ↥((Polynomial.expand R (p ^ n)) f).roots.toFinset),
  ↑((Polynomial.rootsExpandPowToRoots p n f) x) = ↑x ^ p ^ n
-- Init.System.IOError
IO.Error.timeExpired.inj : ∀ {osCode : UInt32} {details : String} {osCode_1 : UInt32} {details_1 : String},
  IO.Error.timeExpired osCode details = IO.Error.timeExpired osCode_1 details_1 →
    osCode = osCode_1 ∧ details = details_1
-- Mathlib.CategoryTheory.Sites.Limits
CategoryTheory.Sheaf.createsLimits : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          [CategoryTheory.Limits.HasLimitsOfSize.{u₁, u₂, w', w} D] →
            CategoryTheory.CreatesLimitsOfSize.{u₁, u₂, max u w', max u w', max (max (max u v) w) w',
                max (max (max u v) w) w'}
              (CategoryTheory.sheafToPresheaf J D)
-- Mathlib.MeasureTheory.OuterMeasure.OfAddContent
/-- The measure `MeasureTheory.AddContent.measureCaratheodory` generated from an
`m : AddContent C` on a `IsSetSemiring C` coincides with the `MeasureTheory.inducedOuterMeasure`.  -/
MeasureTheory.AddContent.measureCaratheodory_eq_inducedOuterMeasure : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent ENNReal C) (m_sigma_subadd : m.IsSigmaSubadditive),
  (m.measureCaratheodory hC m_sigma_subadd) s = (MeasureTheory.inducedOuterMeasure (fun x x_1 => m x) ⋯ ⋯) s
-- Mathlib.SetTheory.Cardinal.NatCard
Finite.card_subtype_le : ∀ {α : Type u_1} [Finite α] (p : α → Prop), Nat.card { x // p x } ≤ Nat.card α
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
/-- In case `f : S ⟶ X₁` is a monomorphism, this relation is the equivalence relation
generated by `Pushout.Rel f g`.  -/
CategoryTheory.Limits.Types.Pushout.Rel' : {S X₁ X₂ : Type u} → (S ⟶ X₁) → (S ⟶ X₂) → X₁ ⊕ X₂ → X₁ ⊕ X₂ → Prop
-- Mathlib.Order.Defs.LinearOrder
/-- This attempts to prove that a given instance of `compare` is equal to `compareOfLessAndEq` by
introducing the arguments and trying the following approaches in order:

1. seeing if `rfl` works
2. seeing if the `compare` at hand is nonetheless essentially `compareOfLessAndEq`, but, because of
   implicit arguments, requires us to unfold the defs and split the `if`s in the definition of
   `compareOfLessAndEq`
3. seeing if we can split by cases on the arguments, then see if the defs work themselves out
   (useful when `compare` is defined via a `match` statement, as it is for `Bool`)
 -/
tacticCompareOfLessAndEq_rfl : Lean.ParserDescr
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.instOrderTop : {K : Type u} → [inst : Field K] → OrderTop (ValuationSubring K)
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.mapEquiv_symm_apply : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (g : M ≃ₗ[R] N) (a : DividedPowerAlgebra R N),
  (DividedPowerAlgebra.mapEquiv g).symm a = (DividedPowerAlgebra.map R ↑g.symm) a
-- Mathlib.Algebra.Module.Congruence.Defs
/-- The kernel of a `DistribMulActionHom` as a congruence relation.  -/
ModuleCon.ker : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : Monoid R] →
          [inst_1 : Monoid S] →
            [inst_2 : AddMonoid M] →
              [inst_3 : AddMonoid N] →
                [inst_4 : DistribMulAction R M] →
                  [inst_5 : DistribMulAction S N] → {φ : R →* S} → (M →ₑ+[φ] N) → ModuleCon R M
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement_singleton_right : ∀ {G : Type u_1} [inst : Group G] {S : Set G} {g : G}, Subgroup.IsComplement S {g} ↔ S = Set.univ
-- Mathlib.Data.Nat.Factorial.Basic
Nat.descFactorial_pos : ∀ {n k : ℕ}, 0 < n.descFactorial k ↔ k ≤ n
-- Init.Data.Option.Monadic
Option.bindM_some : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Pure m] (a : α) (f : α → m (Option β)),
  Option.bindM f (some a) = f a
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.variable : Lean.Lsp.CompletionItemKind
-- Mathlib.Analysis.Complex.Conformal
ContinuousLinearMap.coe_complexOfReal : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {ℓ : ℂ →L[ℝ] E}
  (h : ℓ Complex.I = Complex.I • ℓ 1), ⇑(ℓ.complexOfReal h) = ⇑ℓ
-- Mathlib.Order.Filter.Map
Filter.instAlternative : Alternative Filter
-- Mathlib.Algebra.Algebra.Opposite
AlgHom.opComm_symm_apply_apply : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (a : Aᵐᵒᵖ →ₐ[R] B) (a_1 : A),
  (AlgHom.opComm.symm a) a_1 = MulOpposite.op (a (MulOpposite.op a_1))
-- Init.Data.SInt.Basic
instDecidableEqISize : DecidableEq ISize
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.Iso.to_eq : ∀ {X : Type u} [inst : PartialOrder X] {x y : X} (f : x ≅ y), x = y
-- Mathlib.Topology.Order.LeftRightLim
/-- A monotone function is continuous to the right at a point if and only if its right limit
coincides with the value of the function.  -/
Monotone.continuousWithinAt_Ioi_iff_rightLim_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Monotone f →
    ∀ {x : α} [inst_4 : TopologicalSpace α] [OrderTopology α],
      ContinuousWithinAt f (Set.Ioi x) x ↔ Function.rightLim f x = f x
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.instContinuousAdd : ∀ {R : Type u_3} {M : Type u_4} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M] [inst_2 : Add R]
  [inst_3 : Add M] [ContinuousAdd R] [ContinuousAdd M], ContinuousAdd (TrivSqZeroExt R M)
-- Mathlib.Data.Set.Insert
Set.insert_nonempty : ∀ {α : Type u_1} (a : α) (s : Set α), (insert a s).Nonempty