mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.isLocalizing_pushforward_of_isLocalizing : ∀ {R S : CommRingCat} (φ : R ⟶ S) {M : (AlgebraicGeometry.Spec S).Modules},
  AlgebraicGeometry.IsLocalizing (AlgebraicGeometry.modulesSpecToSheaf.obj M) →
    AlgebraicGeometry.IsLocalizing
      (AlgebraicGeometry.modulesSpecToSheaf.obj
        ((AlgebraicGeometry.Scheme.Modules.pushforward (AlgebraicGeometry.Spec.map φ)).obj M))
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingDegree_le_of_ne_zero : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, p.coeff n ≠ 0 → p.trailingDegree ≤ ↑n
-- Init.Data.SInt.Bitwise
Int32.and_assoc : ∀ (a b c : Int32), a &&& b &&& c = a &&& (b &&& c)
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Copy of a `RingHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
NonUnitalRingHom.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : NonUnitalNonAssocSemiring α] →
      [inst_1 : NonUnitalNonAssocSemiring β] → (f : α →ₙ+* β) → (f' : α → β) → f' = ⇑f → α →ₙ+* β
-- Mathlib.Algebra.GroupWithZero.Units.Fintype
Nat.card_units : ∀ (α : Type u_1) [inst : GroupWithZero α], Nat.card αˣ = Nat.card α - 1
-- Mathlib.Order.WellFoundedSet
Set.wellFoundedOn_empty : ∀ {α : Type u_2} (r : α → α → Prop), ∅.WellFoundedOn r
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.get_cast : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig1 aig2 : Std.Sat.AIG α} (s : aig1.RefVec len)
  (idx : ℕ) (hidx : idx < len) (hcast : aig1.decls.size ≤ aig2.decls.size),
  (s.cast hcast).get idx hidx = (s.get idx hidx).cast hcast
-- Mathlib.NumberTheory.Padics.Measure.Basic
AbstractMeasure.isAddApply : ∀ {X : Type u_1} {R : Type u_3} {E : Type u_4} [inst : TopologicalSpace X] [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : CommRing R] [inst_5 : TopologicalSpace R]
  [inst_6 : IsTopologicalRing R] [inst_7 : Module R E], IsAddApply (AbstractMeasure X R E) C(X, R) E
-- Lean.Meta.Tactic.TryThis
/-- Add `exact e` or `refine e` suggestions if they can be successfully generated; for those that
cannot, display messages indicating the invalid generated tactics.

The parameters are:
* `ref`: the span of the widget diagnostic
* `es`: the array of replacement expressions
* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
  If not provided it defaults to `ref`.
* `addSubgoalsMsg`: if true (default false), any remaining subgoals will be shown after
  `Remaining subgoals:`
* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text for all
  suggestions which do not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is
  used.
* `checkState?`: if passed, the tactic state in which the generated tactics will be validated,
  inserting `expose_names` if necessary.
* `tacticErrorAsInfo`: if true (default true), invalid generated tactics will log info messages
  instead of throwing an error. The default behavior differs from `addExactSuggestion` because
  throwing an error means that any subsequent suggestions will not be displayed. Has no effect if
  `checkState?` is `none`.
 -/
Lean.Meta.Tactic.TryThis.addExactSuggestions : Lean.Syntax →
  Array Lean.Expr →
    optParam (Option Lean.Syntax) none →
      optParam Bool false →
        optParam (Option String) none →
          optParam (Option Lean.Elab.Tactic.SavedState) none → optParam Bool true → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Algebra.Field.GeomSum
Commute.geom_sum₂_Ico : ∀ {K : Type u_2} [inst : DivisionRing K] {x y : K},
  Commute x y →
    x ≠ y → ∀ {m n : ℕ}, m ≤ n → ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)
-- Lean.Structure
Lean.getProjFnInfoForField? : Lean.Environment → Lean.Name → Lean.Name → Option (Lean.Name × Lean.ProjectionFunctionInfo)
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.projectiveDimension_lt_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C} {n : ℕ},
  CategoryTheory.projectiveDimension X < ↑n ↔ CategoryTheory.HasProjectiveDimensionLT X n
-- Mathlib.RingTheory.Ideal.UFD
UniqueFactorizationMonoid.iff_of_isLocalizationAway_of_prime : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [IsNoetherianRing R] {x : R},
  Prime x →
    ∀ (S : Type u_2) [inst_3 : CommRing S] [inst_4 : Algebra R S] [IsLocalization.Away x S],
      UniqueFactorizationMonoid R ↔ UniqueFactorizationMonoid S
-- Lean.Parser.Do
Lean.Parser.Term.termTry : Lean.Parser.Parser
-- Mathlib.Tactic.ClickSuggestions.SectionState
Mathlib.Tactic.ClickSuggestions.SectionKind.currFile.sizeOf_spec : sizeOf Mathlib.Tactic.ClickSuggestions.SectionKind.currFile = 1
-- Mathlib.Analysis.Normed.Algebra.GelfandMazur
/-- A (private) abbreviation introduced for conciseness below.
We will show that for every `x : F`, `φ x` takes the value zero.  -/
_private.Mathlib.Analysis.Normed.Algebra.GelfandMazur.0.NormedAlgebra.Real.φ : {F : Type u_1} → [inst : NormedRing F] → [NormedAlgebra ℝ F] → F → ℝ × ℝ → F
-- Init.Control.Lawful.Instances
ExceptT.bindCont.eq_2 : ∀ {ε : Type u} {m : Type u → Type v} [inst : Monad m] {α β : Type u} (f : α → ExceptT ε m β) (e : ε),
  ExceptT.bindCont f (Except.error e) = pure (Except.error e)
-- Mathlib.Analysis.Normed.Operator.NormedSpace
ContinuousLinearMap.norm_smulRightL_le : ∀ {𝕜 : Type u_1} {E : Type u_5} {Fₗ : Type u_7} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup Fₗ]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 Fₗ],
  ‖ContinuousLinearMap.smulRightL 𝕜 E Fₗ‖ ≤ 1
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.kahler_map : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace ℝ F]
  [hF : Fact (Module.finrank ℝ F = 2)] (φ : E ≃ₗᵢ[ℝ] F) (x y : F),
  (((Orientation.map (Fin 2) φ.toLinearEquiv) o).kahler x) y = (o.kahler (φ.symm x)) (φ.symm y)
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.getSimprocFromDeclImpl : Lean.Name → Lean.ImportM (Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc)
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithTerminal.coneBack_obj_π_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)}
  (t : CategoryTheory.Limits.Cone (CategoryTheory.WithTerminal.liftFromOver.obj K)) (a : J),
  (CategoryTheory.WithTerminal.coneBack✝.obj t).π.app a =
    CategoryTheory.Over.homMk (t.π.app (CategoryTheory.WithTerminal.of a)) ⋯
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- Variant of `prod_insert` not applied to a function.  -/
Finset.prod_insert' : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [inst : CommMonoid M] [inst_1 : DecidableEq ι],
  a ∉ s → (insert a s).prod = fun f => f a * ∏ x ∈ s, f x
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
/-- The inner fibrations are the morphisms which have the right lifting property
with respect to inner horn inclusions.  -/
SSet.innerFibrations : CategoryTheory.MorphismProperty SSet
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.rightDistributor_ext₂_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] {f : J → C} {X Y Z : C}
  {g h :
    X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) Y) Z},
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp g
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y) Z) =
        CategoryTheory.CategoryStruct.comp h
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y) Z)) →
    g = h
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.AddValuation.map_zero : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], Padic.addValuationDef 0 = ⊤
-- Init.Data.Nat.Lemmas
Nat.eq_sub_of_add_eq' : ∀ {a b c : ℕ}, b + c = a → c = a - b
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Matrix.GeneralLinearGroup.congr_simp : ∀ (n : Type u) (R : Type v) {inst : DecidableEq n} [inst_1 : DecidableEq n] [inst_2 : Fintype n] [inst_3 : Semiring R],
  GL n R = GL n R
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ParameterInformationLabel.name.inj : ∀ {name name_1 : String},
  Lean.Lsp.ParameterInformationLabel.name name = Lean.Lsp.ParameterInformationLabel.name name_1 → name = name_1
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.lex_lt_of_lt : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  (r : ι → ι → Prop) [IsStrictOrder ι r] {x y : Π₀ (i : ι), α i}, x < y → Pi.Lex r (fun {i} x1 x2 => x1 < x2) ⇑x ⇑y
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.Ref.seen : {α : Sort u_1} → Lean.Doc.Ref✝ α → Bool
-- Mathlib.RingTheory.Ideal.Height
Ideal.height_strict_mono_of_isPrime : ∀ {R : Type u_1} [inst : CommRing R] {I J : Ideal R} [I.IsPrime], I < J → ∀ [I.FiniteHeight], I.height < J.height
-- Mathlib.Data.List.Lattice
List.Sublist.bagInter_inter : ∀ {α : Type u_1} {l₁ l₂ : List α} [inst : DecidableEq α], (l₁.bagInter l₂).Sublist (l₁ ∩ l₂)
-- Mathlib.LinearAlgebra.Pi
LinearMap.toAddMonoidHom_proj : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type i} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] (i : ι), (LinearMap.proj i).toAddMonoidHom = Pi.evalAddMonoidHom φ i
-- Init.Data.Array.Find
Array.findIdx?_isSome : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, (Array.findIdx? p xs).isSome = xs.any p
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.superpose_certC : ℤ →
  Lean.Grind.CommRing.Mon →
    Lean.Grind.CommRing.Poly →
      ℤ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → ℕ → Bool
-- Std.Data.HashMap.IteratorLemmas
Std.HashMap.toArray_keysIter : ∀ {α β : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m.keysIter.toArray = m.keysArray
-- Std.Http.Data.URI.Encoding
/-- Attempts to create an `EncodedQueryString` from a `ByteArray`. Returns `some` if the byte array contains
only valid encoded query characters and all percent signs are followed by exactly two hex digits, `none` otherwise.
 -/
Std.Http.URI.EncodedQueryString.ofByteArray? : ByteArray →
  (r : optParam (UInt8 → Bool) Std.Http.Internal.Char.isQueryChar) → Option (Std.Http.URI.EncodedQueryString r)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.fst_op_opIso_hom_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P Q : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct P Q] {Z : Cᵒᵖ} (h : Opposite.op P ⊞ Opposite.op Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst.op
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).hom h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h
-- Mathlib.Order.Filter.AtTopBot.Interval
Finset.tendsto_Ico_neg_atTop_atTop : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : LocallyFiniteOrder α] [NoTopOrder α], Filter.Tendsto (fun a => Finset.Ico (-a) a) Filter.atTop Filter.atTop
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- Helper function for typechecking.  -/
CategoryTheory.WithTerminal.down : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → (CategoryTheory.WithTerminal.of X ⟶ CategoryTheory.WithTerminal.of Y) → (X ⟶ Y)
-- Mathlib.Data.Matrix.Block
/-- Given a matrix whose row and column indexes are sum types, we can extract the corresponding
"bottom left" submatrix.  -/
Matrix.toBlocks₂₁ : {l : Type u_1} →
  {m : Type u_2} → {n : Type u_3} → {o : Type u_4} → {α : Type u_12} → Matrix (n ⊕ o) (l ⊕ m) α → Matrix o l α
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheorem.numParams : Lean.Meta.Grind.EMatchTheorem → ℕ
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceE_X₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceE._auto_3),
  (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₁ = X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
-- Mathlib.NumberTheory.Dioph
/-- Projection preserves Diophantine functions.  -/
Dioph.«termD&_» : Lean.ParserDescr
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_congr : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m.WF → ∀ {k k' : α}, (k == k') = true → m.getKey! k = m.getKey! k'
-- Mathlib.Algebra.Order.Ring.Abs
_private.Mathlib.Algebra.Order.Ring.Abs.0.geomSum.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min?_eq_some_iff_get?_eq_self_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km : α}, t.min? = some km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isNClique_iff : ∀ {α : Type u_1} (G : SimpleGraph α) {n : ℕ} {s : Finset α}, G.IsNClique n s ↔ G.IsClique ↑s ∧ s.card = n
-- Mathlib.Data.Fintype.Inv
Function.Injective.invOfMemRange_surjective : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] {f : α → β} (hf : Function.Injective f),
  Function.Surjective hf.invOfMemRange
-- Init.Data.BitVec.Lemmas
BitVec.toFin_mul : ∀ {n : ℕ} (x y : BitVec n), (x * y).toFin = x.toFin * y.toFin
-- Mathlib.CategoryTheory.Shift.CommShift
/-- Auxiliary definition for `Functor.CommShift.ofComp`.  -/
CategoryTheory.Functor.CommShift.OfComp.iso : {C : Type u_1} →
  {D : Type u_2} →
    {E : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            {F : CategoryTheory.Functor C D} →
              {G : CategoryTheory.Functor D E} →
                {H : CategoryTheory.Functor C E} →
                  (F.comp G ≅ H) →
                    [G.Full] →
                      [G.Faithful] →
                        {A : Type u_5} →
                          [inst_5 : AddMonoid A] →
                            [inst_6 : CategoryTheory.HasShift C A] →
                              [inst_7 : CategoryTheory.HasShift D A] →
                                [inst_8 : CategoryTheory.HasShift E A] →
                                  [G.CommShift A] →
                                    [H.CommShift A] →
                                      (a : A) →
                                        (CategoryTheory.shiftFunctor C a).comp F ≅
                                          F.comp (CategoryTheory.shiftFunctor D a)
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.const_app : ∀ {X Y : SSet} (y : Y.obj (Opposite.op { len := 0 })) (n : SimplexCategoryᵒᵖ),
  (SSet.const y).app n =
    TypeCat.ofHom fun x => (CategoryTheory.ConcreteCategory.hom (Y.map ((Opposite.unop n).const { len := 0 } 0).op)) y
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.comap_obj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A B : C} [inst_4 : CategoryTheory.AddMonObj A] [inst_5 : CategoryTheory.AddMonObj B] (f : A ⟶ B)
  [inst_6 : CategoryTheory.IsAddMonHom f] (M : CategoryTheory.AddMod D B),
  ((CategoryTheory.AddMod.comap f).obj M).X = M.X
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSubgraph.isNonloopAt_congr : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β},
  H ≤ G → e ∈ H.edgeSet → (H.IsNonloopAt e x ↔ G.IsNonloopAt e x)
-- Std.Http.Data.Method
/-- Set or remove properties on a resource (WebDAV).
Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.2
 -/
Std.Http.Method.proppatch : Std.Http.Method
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.card_support_eraseLead_add_one : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f ≠ 0 → f.eraseLead.support.card + 1 = f.support.card
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succMany_succ : ∀ {n : ℕ} {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.PRange.InfinitelyUpwardEnumerable α] {a : α},
  Std.PRange.succMany (n + 1) a = Std.PRange.succ (Std.PRange.succMany n a)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.locallyQuasiFinite_iff_isDiscrete_preimage_singleton : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.LocallyOfFiniteType f],
  AlgebraicGeometry.LocallyQuasiFinite f ↔ ∀ (x : ↥Y), IsDiscrete (⇑f ⁻¹' {x})
-- Mathlib.Data.ENNReal.Operations
ENNReal.image_coe_Ioi : ∀ (x : NNReal), ENNReal.ofNNReal '' Set.Ioi x = Set.Ioo ↑x ⊤
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.MethodsRefPointed : NonemptyType
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.instPreservesLimitsProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ ProfiniteAddGrp.{u_1} Profinite)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getEntry?.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : List ((a : α) × β a) → Sort u_3) (k : α) (v : β k)
  (l : List ((a : α) × β a)) (h_1 : Unit → motive [])
  (h_2 : (k : α) → (v : β k) → (l : List ((a : α) × β a)) → motive (⟨k, v⟩ :: l)),
  (match ⟨k, v⟩ :: l with
    | [] => h_1 ()
    | ⟨k, v⟩ :: l => h_2 k v l) =
    h_2 k v l
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Given three points not equal to `p`, the angle between the first and the third at `p` minus
the angle between the second and the third equals the angle between the first and the second.  -/
EuclideanGeometry.oangle_sub_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p p₁ p₂ p₃ : P},
  p₁ ≠ p →
    p₂ ≠ p →
      p₃ ≠ p → EuclideanGeometry.oangle p₁ p p₃ - EuclideanGeometry.oangle p₂ p p₃ = EuclideanGeometry.oangle p₁ p p₂
-- Mathlib.Tactic.Linter.Whitespace
/-- Deprecated in favour of `linter.style.whitespace`  -/
Mathlib.Linter.linter.style.commandStart : Lean.Option Bool
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If `K / E / F` is a field extension tower, such that `E / F` is algebraic, then
`E` adjoin `separableClosure F K` is equal to `separableClosure E K`.  -/
separableClosure.adjoin_eq_of_isAlgebraic : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] [Algebra.IsAlgebraic F E],
  IntermediateField.adjoin E ↑(separableClosure F K) = separableClosure E K
-- Mathlib.MeasureTheory.Function.AEMeasurableSequence
aeSeq.eq_1 : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : ι → α → β}
  {μ : MeasureTheory.Measure α} (hf : ∀ (i : ι), AEMeasurable (f i) μ) (p : α → (ι → β) → Prop) (i : ι) (x : α),
  aeSeq hf p i x = if x ∈ aeSeqSet hf p then AEMeasurable.mk (f i) ⋯ x else ⋯.some
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
AddMonoidHom.compLeftContinuous.congr_simp : ∀ (α : Type u_1) {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {γ : Type u_3}
  [inst_2 : AddMonoid β] [inst_3 : ContinuousAdd β] [inst_4 : TopologicalSpace γ] [inst_5 : AddMonoid γ]
  [inst_6 : ContinuousAdd γ] (g g_1 : β →+ γ) (e_g : g = g_1) (hg : Continuous ⇑g),
  AddMonoidHom.compLeftContinuous α g hg = AddMonoidHom.compLeftContinuous α g_1 ⋯
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey?_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α},
  (Std.ExtDTreeMap.filter f t).getKey? k = (t.getKey? k).pfilter fun x h' => f x (Std.ExtDTreeMap.Const.get t x ⋯)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoLocallyUniformly.sub` -/
TendstoLocallyUniformly.fun_sub : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {l : Filter ι},
  TendstoLocallyUniformly F f l →
    TendstoLocallyUniformly G g l → TendstoLocallyUniformly (fun i i_1 => F i i_1 - G i i_1) (fun i => f i - g i) l
-- Mathlib.Order.Lattice
/-- Pointwise supremum of two antitone functions is an antitone function.  -/
AntitoneOn.sup : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : SemilatticeSup β] {f g : α → β} {s : Set α},
  AntitoneOn f s → AntitoneOn g s → AntitoneOn (f ⊔ g) s
-- Mathlib.Topology.Order.MonotoneContinuity
/-- If a function `f` with a densely ordered codomain is strictly monotone on a right neighborhood
of `a` and the image of this neighborhood under `f` is a right neighborhood of `f a`, then `f` is
continuous at `a` from the right.  -/
StrictMonoOn.continuousWithinAt_right_of_image_mem_nhdsWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α}
  {a : α},
  StrictMonoOn f s →
    s ∈ nhdsWithin a (Set.Ici a) → f '' s ∈ nhdsWithin (f a) (Set.Ici (f a)) → ContinuousWithinAt f (Set.Ici a) a
-- Mathlib.Algebra.Order.Star.Basic
StarOrderedRing.mk : ∀ {R : Type u_3} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R],
  (∀ (x y : R), x ≤ y ↔ ∃ p ∈ AddSubmonoid.closure (Set.range fun s => star s * s), y = x + p) → StarOrderedRing R
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_add_pi : ∀ (x : ℝ), Real.cos (x + Real.pi) = -Real.cos x
-- Mathlib.GroupTheory.Sylow
Sylow.inhabited : {p : ℕ} → {G : Type u_1} → [inst : Group G] → Inhabited (Sylow p G)
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.node4L.match_1.eq_2 : ∀ {α : Type u_1} (motive : Ordnode α → α → Ordnode α → α → Ordnode α → Sort u_2) (l : Ordnode α) (x z : α)
  (r : Ordnode α)
  (h_1 :
    (l : Ordnode α) →
      (x : α) →
        (size : ℕ) →
          (ml : Ordnode α) →
            (y : α) → (mr : Ordnode α) → (z : α) → (r : Ordnode α) → motive l x (Ordnode.node size ml y mr) z r)
  (h_2 : (l : Ordnode α) → (x z : α) → (r : Ordnode α) → motive l x Ordnode.nil z r),
  (match l, x, Ordnode.nil, z, r with
    | l, x, Ordnode.node size ml y mr, z, r => h_1 l x size ml y mr z r
    | l, x, Ordnode.nil, z, r => h_2 l x z r) =
    h_2 l x z r