mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- An arbitrary choice of terminal object, if one exists.
You can use the notation `⊤_ C`.
This object is characterized by having a unique morphism from any object.
 -/
CategoryTheory.Limits.terminal : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.Limits.HasTerminal C] → C
-- Mathlib.Algebra.LinearRecurrence
/-- If `u` is a solution to `E` and `init` designates its first `E.order` values,
then `∀ n, u n = E.mkSol init n`.  -/
LinearRecurrence.eq_mk_of_is_sol_of_eq_init : ∀ {R : Type u_1} [inst : CommSemiring R] (E : LinearRecurrence R) {u : ℕ → R} {init : Fin E.order → R},
  E.IsSolution u → (∀ (n : Fin E.order), u ↑n = init n) → ∀ (n : ℕ), u n = E.mkSol init n
-- Mathlib.Data.Set.Countable
/-- Convert `Set.Countable s` to `Encodable s` (noncomputable).  -/
Set.Countable.toEncodable : {α : Type u} → {s : Set α} → s.Countable → Encodable ↑s
-- Mathlib.Topology.SeparatedMap
isLocallyInjective_iff_isOpen_diagonal : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f : X → Y},
  IsLocallyInjective f ↔ IsOpen (Function.pullbackDiagonal f)
-- Mathlib.Data.Multiset.Filter
Multiset.Nodup.notMem_erase : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, s.Nodup → a ∉ s.erase a
-- Lean.Elab.DefView
Lean.Elab.DefViewElabHeaderData.mk : Lean.Name → Lean.Name → List Lean.Name → Array Lean.Syntax → ℕ → Lean.Expr → Lean.Elab.DefViewElabHeaderData
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- If `f` has derivative `f'` at `x`, and `σ, σ'` are mutually inverse normed-ring automorphisms,
then `σ ∘ f ∘ σ'` has derivative `σ f'` at `σ x`.  -/
HasDerivAt.comp_ringHom : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} (σ σ' : 𝕜 →+* 𝕜) [RingHomIsometric σ] [RingHomInvPair σ σ']
  {f : 𝕜 → 𝕜} {f' : 𝕜}, HasDerivAt f f' x → HasDerivAt (⇑σ ∘ f ∘ ⇑σ') (σ f') (σ x)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor_map_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) {X Y : CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G)}
  (f : X ⟶ Y),
  ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c).map f).right =
    (CategoryTheory.StructuredArrow.Hom.right f).right
-- Mathlib.Data.Set.MulAntidiagonal
Set.MulAntidiagonal.finite_of_isWF : ∀ {α : Type u_1} [inst : CancelCommMonoid α] [inst_1 : LinearOrder α] [MulLeftMono α] [MulRightStrictMono α]
  {s t : Set α}, s.IsWF → t.IsWF → ∀ (a : α), (s.mulAntidiagonal t a).Finite
-- Init.Data.List.Lemmas
List.mem_singleton : ∀ {α : Type u_1} {a b : α}, a ∈ [b] ↔ a = b
-- Lean.EnvExtension
Lean.SimplePersistentEnvExtensionDescr.mk : {α σ : Type} →
  autoParam Lean.Name Lean.SimplePersistentEnvExtensionDescr.name._autoParam →
    (σ → α → σ) →
      (Array (Array α) → σ) →
        (List α → Array α) →
          Option (Lean.Environment → σ → List α → Lean.OLeanEntries (Array α)) →
            Lean.EnvExtension.AsyncMode →
              Option (List α → σ → σ → List α × σ) → Lean.SimplePersistentEnvExtensionDescr α σ
-- Init.Data.List.FinRange
Fin.foldr_eq_finRange_foldr : ∀ {n : ℕ} {α : Type u_1} (f : Fin n → α → α) (x : α), Fin.foldr n f x = List.foldr f x (List.finRange n)
-- Batteries.Logic
subsingleton_iff_forall_eq : ∀ {α : Sort u_1} (x : α), Subsingleton α ↔ ∀ (y : α), y = x
-- Mathlib.Data.List.Palindrome
List.Palindrome.append_reverse : ∀ {α : Type u_1} (l : List α), (l ++ l.reverse).Palindrome
-- Mathlib.Data.Finmap
Finmap.induction_on₂ : ∀ {α : Type u} {β : α → Type v} {C : Finmap β → Finmap β → Prop} (s₁ s₂ : Finmap β),
  (∀ (a₁ a₂ : AList β), C a₁.toFinmap a₂.toFinmap) → C s₁ s₂
-- Mathlib.Geometry.Manifold.Notation
/-- Given an `Expr`ession `e`, try to find a `NormedSpace` instance on `e` and return the
underlying base field. Search local instances, before recursing into product and bundled
continuous linear maps.  -/
Manifold.Elab.guessBaseFieldForNormedSpace : Lean.Expr → Lean.Elab.TermElabM (Option Lean.Expr)
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContDiffAt.comp_contMDiffAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_6} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {F' : Type u_7} [inst_8 : NormedAddCommGroup F'] [inst_9 : NormedSpace 𝕜 F']
  {n : WithTop ℕ∞} {g : F → F'} {f : M → F} {x : M},
  ContDiffAt 𝕜 n g (f x) →
    ContMDiffAt I (modelWithCornersSelf 𝕜 F) n f x → ContMDiffAt I (modelWithCornersSelf 𝕜 F') n (g ∘ f) x
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_add_intCast : ∀ {x : NNReal}, x ≠ 0 → ∀ (y : ℝ) (n : ℤ), x ^ (y + ↑n) = x ^ y * x ^ n
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.comm₄ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃),
  CategoryTheory.CategoryStruct.comp w₁₃ ((CategoryTheory.shiftFunctor C 1).map u₁₂) =
    CategoryTheory.CategoryStruct.comp self.m₃ w₂₃
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.Context.mk.injEq : ∀ (levelParams : List Lean.Name) (largeElim : Bool) (params motives : Array Lean.Expr) (motiveToIdx : Lean.FVarIdMap ℕ)
  (minors : Array Lean.Expr) (recNames belowNames brecOnNames : Array Lean.Name) (levelParams_1 : List Lean.Name)
  (largeElim_1 : Bool) (params_1 motives_1 : Array Lean.Expr) (motiveToIdx_1 : Lean.FVarIdMap ℕ)
  (minors_1 : Array Lean.Expr) (recNames_1 belowNames_1 brecOnNames_1 : Array Lean.Name),
  ({ levelParams := levelParams, largeElim := largeElim, params := params, motives := motives,
        motiveToIdx := motiveToIdx, minors := minors, recNames := recNames, belowNames := belowNames,
        brecOnNames := brecOnNames } =
      { levelParams := levelParams_1, largeElim := largeElim_1, params := params_1, motives := motives_1,
        motiveToIdx := motiveToIdx_1, minors := minors_1, recNames := recNames_1, belowNames := belowNames_1,
        brecOnNames := brecOnNames_1 }) =
    (levelParams = levelParams_1 ∧
      largeElim = largeElim_1 ∧
        params = params_1 ∧
          motives = motives_1 ∧
            motiveToIdx = motiveToIdx_1 ∧
              minors = minors_1 ∧ recNames = recNames_1 ∧ belowNames = belowNames_1 ∧ brecOnNames = brecOnNames_1)
-- Mathlib.GroupTheory.Finiteness
instFGFreeGroupOfFinite : ∀ (α : Type u_5) [Finite α], Group.FG (FreeGroup α)
-- Init.Guard
/-- Default-reducibility defeq matching for `guard_expr`  -/
Lean.Parser.equalD : Lean.ParserDescr
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.of_val : ∀ (C : Type u) [inst : CategoryTheory.ReflQuiver C], ↑(CategoryTheory.ReflQuiv.of C) = C
-- Mathlib.Algebra.Order.Ring.Basic
Odd.pow_nonneg_iff : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ} [ExistsAddOfLE R],
  Odd n → (0 ≤ a ^ n ↔ 0 ≤ a)
-- Mathlib.Topology.Category.LightProfinite.AsLimit
/-- The projection from `S` to the `n`th component of `S.diagram`.  -/
LightProfinite.proj : (S : LightProfinite) → (n : ℕ) → S ⟶ S.diagram.obj (Opposite.op n)
-- Mathlib.Data.Multiset.ZeroCons
Multiset.card_eq_four : ∀ {α : Type u_1} {s : Multiset α}, s.card = 4 ↔ ∃ x y z w, s = {x, y, z, w}
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.instFunLike : {A : Type u_2} →
  {B : Type u_3} →
    [inst : Monoid A] →
      [inst_1 : Monoid B] → [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → FunLike (A →ₜ* B) A B
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.degHom_le : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) {X Z Y : C} (f : X ⟶ Z) (g : Z ⟶ Y),
  r.degHom (CategoryTheory.CategoryStruct.comp f g) ≤ r.deg Z
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.singleton_prod_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : T1Space α]
  [inst_3 : T1Space β] (x : α) (y : β), {x} ×ˢ {y} = {(x, y)}
-- Mathlib.Algebra.Order.Group.Cone
/-- Construct a partially ordered abelian group by designating a cone in an abelian group.  -/
IsOrderedMonoid.mkOfCone : ∀ {S : Type u_1} {G : Type u_2} [inst : CommGroup G] [inst_1 : SetLike S G] (C : S) [inst_2 : GroupConeClass S G],
  have x := PartialOrder.mkOfGroupCone C;
  IsOrderedMonoid G
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseWeekdayTwoLetter : Std.Time.DateFormatSymbols → Std.Internal.Parsec.String.Parser Std.Time.Weekday
-- Lean.Hygiene
/-- `x` ~> 2 if we're already using `x✝`, `x✝¹`  -/
Lean.NameSanitizerState.nameStem2Idx : Lean.NameSanitizerState → Lean.NameMap ℕ
-- Mathlib.Algebra.Regular.Defs
/-- An add-regular element `c` is left-regular  -/
IsAddRegular.left : ∀ {R : Type u_2} [inst : Add R] {c : R}, IsAddRegular c → IsAddLeftRegular c
-- Mathlib.Data.Nat.Upto
/-- Zero is always a member of `Nat.Upto p` because it has no predecessors.  -/
Nat.Upto.zero : {p : ℕ → Prop} → Nat.Upto p
-- Init.Data.UInt.Bitwise
UInt8.ofNat_and : ∀ (a b : ℕ), UInt8.ofNat (a &&& b) = UInt8.ofNat a &&& UInt8.ofNat b
-- Init.Data.SInt.Lemmas
Int64.sub_lt : ∀ {a b : Int64}, 0 < b → b ≤ a → a - b < a
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- If `R` contains an `n`-th primitive root, and `S/R` is a ring extension,
then the `n`-th roots of unity in `R` and `S` are isomorphic.
Also see `IsPrimitiveRoot.map_rootsOfUnity` for the equality as `Subgroup Sˣ`.  -/
rootsOfUnityEquivOfPrimitiveRoots : {R : Type u_4} →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      {S : Type u_7} →
        {F : Type u_8} →
          [inst_2 : CommRing S] →
            [IsDomain S] →
              [inst_4 : FunLike F R S] →
                [MonoidHomClass F R S] →
                  {n : ℕ} →
                    [NeZero n] →
                      {f : F} →
                        Function.Injective ⇑f →
                          (primitiveRoots n R).Nonempty → ↥(rootsOfUnity n R) ≃* ↥(rootsOfUnity n S)
-- Init.Prelude
/-- The typeclass behind the notation `a ||| b : γ` where `a : α`, `b : β`.  -/
HOr : Type u → Type v → outParam (Type w) → Type (max (max u v) w)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.MatchesAt.mk : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  (∃ endPos, String.Slice.Pattern.Model.IsLongestMatchAt pat pos endPos) → String.Slice.Pattern.Model.MatchesAt pat pos
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.mk0_surjective : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDedekindDomain R],
  Function.Surjective ⇑ClassGroup.mk0
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.Path.ins.match_1.eq_5 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (y : α)
  (parent : RBTree.RBNode.Path α) (b : RBTree.RBNode α) (h_1 : (t : RBTree.RBNode α) → motive RBTree.RBNode.Path.root t)
  (h_2 :
    (parent : RBTree.RBNode.Path α) →
      (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.red parent y b) a)
  (h_3 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (parent : RBTree.RBNode.Path α) →
          (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.red a y parent) b)
  (h_4 :
    (parent : RBTree.RBNode.Path α) →
      (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.black parent y b) a)
  (h_5 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (parent : RBTree.RBNode.Path α) →
          (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.black a y parent) b),
  (match RBTree.RBNode.Path.right RBTree.RBColor.black a y parent, b with
    | RBTree.RBNode.Path.root, t => h_1 t
    | RBTree.RBNode.Path.left RBTree.RBColor.red parent y b, a => h_2 parent y b a
    | RBTree.RBNode.Path.right RBTree.RBColor.red a y parent, b => h_3 a y parent b
    | RBTree.RBNode.Path.left RBTree.RBColor.black parent y b, a => h_4 parent y b a
    | RBTree.RBNode.Path.right RBTree.RBColor.black a y parent, b => h_5 a y parent b) =
    h_5 a y parent b
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.containsKey_toListModel : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.OrientedOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {l : Std.DTreeMap.Internal.Impl α β},
  Std.DTreeMap.Internal.Impl.contains' (compare k) l = true → Std.Internal.List.containsKey k l.toListModel = true
-- Mathlib.Probability.Kernel.Posterior
ProbabilityTheory.posterior_comp_self : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : ProbabilityTheory.Kernel Ω 𝓧}
  {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : ProbabilityTheory.IsFiniteKernel κ]
  [inst_2 : StandardBorelSpace Ω] [inst_3 : Nonempty Ω] [ProbabilityTheory.IsMarkovKernel κ],
  (μ.bind ⇑κ).bind ⇑(ProbabilityTheory.posterior κ μ) = μ
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.pow : {R : Type u} → [inst : Semiring R] → Pow (Polynomial R) ℕ
-- Mathlib.Combinatorics.Quiver.Path.Weight
Quiver.Path.weightOfEPs_comp : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : Monoid R] (w : V → V → R) {a b c : V} (p : Quiver.Path a b)
  (q : Quiver.Path b c),
  Quiver.Path.weightOfEPs w (p.comp q) = Quiver.Path.weightOfEPs w p * Quiver.Path.weightOfEPs w q
-- Mathlib.GroupTheory.OrderOfElement
mem_zpowers_pow_iff : ∀ {G : Type u_1} [inst : Group G] {g : G} {k : ℕ}, g ∈ Subgroup.zpowers (g ^ k) ↔ k.gcd (orderOf g) = 1
-- Mathlib.Geometry.Manifold.Notation
Manifold.Elab.instInhabitedFindModelResult.default : Manifold.Elab.FindModelResult
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
IsUnit.mul_le_mul_right : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulRightMono M] {a b c : M}, IsUnit c → (a * c ≤ b * c ↔ a ≤ b)
-- Lean.Elab.MutualDef
Lean.Elab.Term.AsyncBodyInfo.noConfusionType : Sort v✝ → Lean.Elab.Term.AsyncBodyInfo → Lean.Elab.Term.AsyncBodyInfo → Sort v✝
-- Aesop.Search.Expansion.Norm
Aesop.NormRuleResult.proved.sizeOf_spec : ∀ (steps? : Option (Array Aesop.Script.LazyStep)), sizeOf (Aesop.NormRuleResult.proved steps?) = 1 + sizeOf steps?
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` preserves limits of `K.leftOp : Jᵒᵖ ⥤ C`, then `F.leftOp : Cᵒᵖ ⥤ D` preserves
colimits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.preservesColimit_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J Cᵒᵖ)
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesLimit K.leftOp F],
  CategoryTheory.Limits.PreservesColimit K F.leftOp
-- Mathlib.Order.Filter.Extr
IsMinFilter.sup : ∀ {α : Type u} {β : Type v} [inst : SemilatticeSup β] {f g : α → β} {a : α} {l : Filter α},
  IsMinFilter f l a → IsMinFilter g l a → IsMinFilter (fun x => f x ⊔ g x) l a
-- Mathlib.Tactic.Abel
/-- A type synonym used by `abel` to represent `n • x + a` in an additive commutative monoid.  -/
Mathlib.Tactic.Abel.term : {α : Type u_1} → [AddCommMonoid α] → ℕ → α → α → α
-- Mathlib.Topology.Algebra.FilterBasis
RingFilterBasis.mul_right : ∀ {R : Type u} [inst : Ring R] (B : RingFilterBasis R) (x₀ : R) {U : Set R},
  U ∈ B → ∃ V ∈ B, V ⊆ (fun x => x * x₀) ⁻¹' U
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
NNReal.hasMeasurablePow : MeasurablePow NNReal ℝ
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.N : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.Nanosecond.Offset
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measurePreserving_smul : ∀ {M : Type v} {α : Type w} {m : MeasurableSpace α} [inst : SMul M α] [MeasurableConstSMul M α] (c : M)
  (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure M α μ],
  MeasureTheory.MeasurePreserving (fun x => c • x) μ μ
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.Context.u : Lean.Meta.Grind.Arith.FieldNormNum.Context✝ → Lean.Level
-- Mathlib.GroupTheory.Finiteness
Group.fg_iff' : ∀ {G : Type u_3} [inst : Group G], Group.FG G ↔ ∃ n S, S.card = n ∧ Subgroup.closure ↑S = ⊤
-- Mathlib.Data.Finsupp.AList
AList.empty_lookupFinsupp : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M], ∅.lookupFinsupp = 0
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.coe_ofBijective : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (f : A₁ →ₐ[R] A₂) (hf : Function.Bijective ⇑f),
  ⇑(AlgEquiv.ofBijective f hf) = ⇑f
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKeyD_eq_fallback : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} {fallback : α}, l.isEmpty = true → Std.Internal.List.maxKeyD l fallback = fallback
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable.0.EisensteinSeries.aux_sum_Ico_S_identity : ∀ (z : UpperHalfPlane) (N : ℕ),
  (↑z ^ 2)⁻¹ * ∑ x ∈ Finset.Ico (-↑N) ↑N, ∑' (n : ℤ), ((↑x * (-↑z)⁻¹ + ↑n) ^ 2)⁻¹ =
    ∑' (n : ℤ), ∑ x ∈ Finset.Ico (-↑N) ↑N, ((↑n * ↑z + ↑x) ^ 2)⁻¹
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coreCommRing.inj : ∀ {a b : Lean.Expr} {ra rb : Lean.Grind.CommRing.Expr} {p : Lean.Grind.CommRing.Poly}
  {lhs' : Lean.Meta.Grind.Arith.Linear.LinExpr} {a_1 b_1 : Lean.Expr} {ra_1 rb_1 : Lean.Grind.CommRing.Expr}
  {p_1 : Lean.Grind.CommRing.Poly} {lhs'_1 : Lean.Meta.Grind.Arith.Linear.LinExpr},
  Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coreCommRing a b ra rb p lhs' =
      Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coreCommRing a_1 b_1 ra_1 rb_1 p_1 lhs'_1 →
    a = a_1 ∧ b = b_1 ∧ ra = ra_1 ∧ rb = rb_1 ∧ p = p_1 ∧ lhs' = lhs'_1
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
PresheafOfModules.evaluation_preservesLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R))
  [∀ (X : Cᵒᵖ),
      Small.{v, max u₂ v}
        ↑((F.comp (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections]
  (X : Cᵒᵖ), CategoryTheory.Limits.PreservesLimit F (PresheafOfModules.evaluation R X)
-- Init.NotationExtra
Lean.«term_Matches_|» : Lean.TrailingParserDescr
-- Mathlib.Data.Nat.ModEq
Nat.add_modEq_left : ∀ {n a : ℕ}, n + a ≡ a [MOD n]
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.δ_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ],
  CochainComplex.HomComplex.δ 0 1 (CochainComplex.mappingCone.snd φ) =
    -(↑(CochainComplex.mappingCone.fst φ)).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.liftOn₂_mk : ∀ {M : Type u_1} [inst : AddCommMonoid M] {α : Type u_2} (m m' : M) (s s' : ℕ+) (f : M → ℕ+ → M → ℕ+ → α)
  (h :
    ∀ (m n m' n' : M) (s t s' t' : ℕ+),
      DivisibleHull.mk m s = DivisibleHull.mk m' s' →
        DivisibleHull.mk n t = DivisibleHull.mk n' t' → f m s n t = f m' s' n' t'),
  (DivisibleHull.mk m s).liftOn₂ (DivisibleHull.mk m' s') f h = f m s m' s'
-- Mathlib.Tactic.TFAE
/-- Extract a list of `Prop` expressions from an expression of the form `TFAE [P₁, P₂, ...]` as
long as `[P₁, P₂, ...]` is an explicit list.  -/
Mathlib.Tactic.TFAE.getTFAEList : Lean.Expr → Lean.MetaM (Q(List Prop) × List Q(Prop))
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_filter_of_getKey?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β] {f : α → β → Bool} {k k' : α},
  (↑m).WF →
    m.getKey? k = some k' →
      Std.DHashMap.Internal.Raw₀.Const.get! (Std.DHashMap.Internal.Raw₀.filter f m) k =
        (Option.filter (fun x => f k' x) (Std.DHashMap.Internal.Raw₀.Const.get? m k)).get!
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.minimalPeriod_pos_iff_mem_periodicPts : ∀ {α : Type u_1} {f : α → α} {x : α}, 0 < Function.minimalPeriod f x ↔ x ∈ Function.periodicPts f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {l : List (α × β)}
  {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → ∀ {h' : k' ∈ t.insertMany l}, (t.insertMany l).getKey k' h' = k
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.comp_assoc : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (h g f : CentroidHom α), (h.comp g).comp f = h.comp (g.comp f)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_singleton : ∀ {x y : ZFSet.{u}}, x ∈ {y} ↔ x = y
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.Coloring.not_adj_of_mem_colorClass : ∀ {V : Type u} {G : SimpleGraph V} {α : Type u_2} (C : G.Coloring α) {c : α} {v w : V},
  v ∈ C.colorClass c → w ∈ C.colorClass c → ¬G.Adj v w
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.throwNotMarkedWithGrindAttribute : {α : Type} → Lean.Name → Lean.CoreM α
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.productTriangle_mor₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  (T : J → CategoryTheory.Pretriangulated.Triangle C) [inst_2 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₁]
  [inst_3 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₂]
  [inst_4 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₃]
  [inst_5 : CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁],
  (CategoryTheory.Pretriangulated.productTriangle T).mor₁ = CategoryTheory.Limits.Pi.map fun j => (T j).mor₁