mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Slope
/-- If `f` is convex on a set `s` in a linearly ordered field, and `f x < f y` for two points
`x < y` in `s`, then `f` is strictly monotone on `s ∩ [y, ∞)`.  -/
ConvexOn.strictMonoOn : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  ConvexOn 𝕜 s f → ∀ {x y : 𝕜}, x ∈ s → x < y → f x < f y → StrictMonoOn f (s ∩ Set.Ici y)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k k' : α} {f : Option β → Option β},
  (m.alter k f).getKey! k' = if (k == k') = true then if (f m[k]?).isSome = true then k else default else m.getKey! k'
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.connectivity_lt_iff : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {S : Finset G},
  K ≤ 1 → S.Nonempty → ∀ {r : ℝ}, Finset.connectivity✝ K S < r ↔ ∃ A, A.Nonempty ∧ Finset.expansion✝ K S A < r
-- Mathlib.Analysis.RCLike.ContinuousMap
ContinuousMap.realToRCLike_mul : ∀ {X : Type u_1} (𝕜 : Type u_2) [inst : TopologicalSpace X] [inst_1 : RCLike 𝕜] (f g : C(X, ℝ)),
  ContinuousMap.realToRCLike 𝕜 (f * g) = ContinuousMap.realToRCLike 𝕜 f * ContinuousMap.realToRCLike 𝕜 g
-- Mathlib.Data.Finmap
Multiset.keys.eq_1 : ∀ {α : Type u} {β : α → Type v} (s : Multiset (Sigma β)), s.keys = Multiset.map Sigma.fst s
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_filter_not_contains_of_containsKey_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    l₂.contains k = true → Std.Internal.List.getKey? k (List.filter (fun p => !l₂.contains p.fst) l₁) = none
-- Lean.Meta.Tactic.Grind.Attr
_private.Lean.Meta.Tactic.Grind.Attr.0.Lean.Meta.Grind.Extension.addExtAttr : Lean.Meta.Grind.Extension → Lean.Name → Lean.AttributeKind → Lean.CoreM Unit
-- Mathlib.CategoryTheory.Monoidal.Ring
/-- The forgetful functor from the category of ring objects in `C`
to the category of monoid objects in `C`.  -/
CategoryTheory.RingObjCat.forget₂Mon : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        CategoryTheory.Functor (CategoryTheory.RingObjCat C) (CategoryTheory.Mon C)
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- Theorem of Rudio (Wielandt, 1964, Th. 8.1)

For a preprimitive action, a subset which is neither empty nor full has a translate
which contains a given point and avoids another one.  -/
MulAction.IsPreprimitive.exists_mem_smul_and_notMem_smul : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] [MulAction.IsPreprimitive G X] {A : Set X},
  A.Finite → A.Nonempty → A ≠ Set.univ → ∀ {a b : X}, a ≠ b → ∃ g, a ∈ g • A ∧ b ∉ g • A
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_dvd : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {p q : Polynomial R}
  (x : A), p ∣ q → (Polynomial.aeval x) p ∣ (Polynomial.aeval x) q
-- Mathlib.Data.Seq.Basic
_private.Mathlib.Data.Seq.Basic.0.Stream'.Seq.join.match_3.splitter : {α : Type u_1} →
  (motive : Option (Stream'.Seq1 (Stream'.Seq1 α)) → Sort u_2) →
    (x : Option (Stream'.Seq1 (Stream'.Seq1 α))) →
      (Unit → motive none) →
        ((a : α) → (s : Stream'.Seq α) → (S' : Stream'.Seq (Stream'.Seq1 α)) → motive (some ((a, s), S'))) → motive x
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- A family of elements for a presheaf on the presieve `R₂` can be restricted to a smaller presieve
`R₁`.
 -/
CategoryTheory.Presieve.FamilyOfElements.restrict : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      {X : C} →
        {R₁ R₂ : CategoryTheory.Presieve X} →
          R₁ ≤ R₂ → CategoryTheory.Presieve.FamilyOfElements P R₂ → CategoryTheory.Presieve.FamilyOfElements P R₁
-- Mathlib.Algebra.Category.CoalgCat.Monoidal
CoalgCat.tensorUnit_instCoalgebra : ∀ (R : Type u) [inst : CommRing R],
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CoalgCat R)).instCoalgebra = inferInstance
-- Mathlib.Order.Filter.Tendsto
Filter.pure_le_iff : ∀ {α : Type u_1} {a : α} {l : Filter α}, pure a ≤ l ↔ ∀ s ∈ l, a ∈ s
-- Mathlib.Data.Fintype.BigOperators
Fintype.card_fun : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] [inst_2 : Fintype β],
  Fintype.card (α → β) = Fintype.card β ^ Fintype.card α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.deriv_cos : ∀ {x : ℝ}, deriv Real.cos x = -Real.sin x
-- Init.Data.Vector.Algebra
Vector.instNatModule : {α : Type u_1} → {n : ℕ} → [Lean.Grind.NatModule α] → Lean.Grind.NatModule (Vector α n)
-- Mathlib.Order.Interval.Finset.Defs
OrderIso.locallyFiniteOrderTop.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrderTop β]
  (f : α ≃o β),
  f.locallyFiniteOrderTop =
    { finsetIoi := fun a => Finset.map f.symm.toEmbedding (Finset.Ioi (f a)),
      finsetIci := fun a => Finset.map f.symm.toEmbedding (Finset.Ici (f a)), finset_mem_Ici := ⋯, finset_mem_Ioi := ⋯ }
-- Aesop.Stats.Basic
Aesop.enableStatsFile : {m : Type → Type} → [Monad m] → [Lean.MonadOptions m] → m Bool
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_surjective : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → β},
  Function.Surjective f → Function.Surjective (Finsupp.mapDomain f)
-- Mathlib.Data.Finsupp.Basic
Finsupp.equivMapDomain_single : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α ≃ β) (a : α) (b : M),
  (Finsupp.equivMapDomain f fun₀ | a => b) = fun₀ | f a => b
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.ordered_erase : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α} {t : Std.DTreeMap.Internal.Impl α β}
  (htb : t.Balanced), t.Ordered → (Std.DTreeMap.Internal.Impl.erase k t htb).impl.Ordered
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.limZero_sub_rev : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {f g : CauSeq β abv}, (f - g).LimZero → (g - f).LimZero
-- Mathlib.Algebra.Group.Torsion
IsAddTorsionFree.zsmul_eq_zero_iff : ∀ {G : Type u_2} [inst : AddGroup G] [IsAddTorsionFree G] {n : ℤ} {a : G}, n • a = 0 ↔ a = 0 ∨ n = 0
-- Mathlib.Topology.Order.NhdsSet
Ici_mem_nhdsSet_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c : α},
  a ≤ b → Set.Ici a ∈ nhdsSet (Set.Ioc b c)
-- Mathlib.CategoryTheory.Presentable.Directed
/-- The diagram with a unique terminal object containing a single object
(and its identity morphism).  -/
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.single : {J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} →
      [Fact κ.IsRegular] → J → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.factors_span_eq : ∀ {K : Type u_3} [inst : Field K] {p : Polynomial K},
  UniqueFactorizationMonoid.factors (Ideal.span {p}) =
    Multiset.map (fun q => Ideal.span {q}) (UniqueFactorizationMonoid.factors p)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α}
  {k fallback : α}, l.contains k = false → (Std.TreeSet.ofList l cmp).getD k fallback = fallback
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering} {a fallback : α}, ∅.getD a fallback = fallback
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsTangentAt.mem_space : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p : P} {as : AffineSubspace ℝ P},
  s.IsTangentAt p as → p ∈ as
-- Lean.Meta.CongrTheorems
/-- Helper function for applying the substitution `s`.
It assumes that all entries in `s` map free variables to free variables.
 -/
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.getFVarId : Lean.Meta.FVarSubst → Lean.FVarId → Lean.FVarId
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.IsCycle.cycleFactorsFinset_eq_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α}, f.IsCycle → f.cycleFactorsFinset = {f}
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.counitIso_inv_app_comp_functor_map_η_inverse_assoc : ∀ {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 D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal] {Z : D}
  (h : e.functor.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.counitIso.inv.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
      (CategoryTheory.CategoryStruct.comp (e.functor.map (CategoryTheory.Functor.OplaxMonoidal.η e.inverse)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε e.functor) h
-- Mathlib.Tactic.Have
/-- Given a main goal `ctx ⊢ t`, `suffices h : t' from e` replaces the main goal with `ctx ⊢ t'`,
`e` must have type `t` in the context `ctx, h : t'`.

The variant `suffices h : t' by tac` is a shorthand for `suffices h : t' from by tac`.
If `h :` is omitted, the name `this` is used.
  -/
Mathlib.Tactic.tacticSuffices_ : Lean.ParserDescr
-- Mathlib.FieldTheory.SeparableDegree
IntermediateField.isSeparable_top : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  Algebra.IsSeparable F ↥⊤ ↔ Algebra.IsSeparable F E
-- Mathlib.Order.UpperLower.Prod
UpperSet.codisjoint_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s₁ s₂ : UpperSet α} {t₁ t₂ : UpperSet β},
  Codisjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Codisjoint s₁ s₂ ∨ Codisjoint t₁ t₂
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.single_le_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y),
  CategoryTheory.MorphismProperty.single f ≤ W ↔ W f
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instIsScalarTower : ∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_3} {R₁ : Type u_4} {M : Type u_5} [inst_1 : TopologicalSpace M]
  [inst_2 : SMul R M] [inst_3 : ContinuousConstSMul R M] [inst_4 : SMul R₁ M] [inst_5 : ContinuousConstSMul R₁ M]
  [inst_6 : SMul R R₁] [IsScalarTower R R₁ M], IsScalarTower R R₁ C(α, M)
-- Mathlib.Computability.EpsilonNFA
εNFA.eval_append_singleton : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ) (x : List α) (a : α), M.eval (x ++ [a]) = M.stepSet (M.eval x) a
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.decompose_zero : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubmonoidClass σ M] (ℳ : ι → σ) [inst_4 : DirectSum.Decomposition ℳ], (DirectSum.decompose ℳ) 0 = 0
-- Lean.Parser.Basic
Lean.Parser.hexnumNoAntiquot : Lean.Parser.Parser
-- Mathlib.Topology.Homotopy.HSpaces
unitInterval.qRight_zero_left : ∀ (θ : ↑unitInterval), unitInterval.qRight (0, θ) = 0
-- Mathlib.Analysis.Complex.SqrtDeriv
Complex.hasStrictDerivAt_sqrt : ∀ {z : ℂ}, z ∈ Complex.slitPlane → HasStrictDerivAt Complex.sqrt (z ^ (-1 / 2) / 2) z
-- Mathlib.Computability.AkraBazzi.SumTransform
/-- The functions `r i` always reduce `n`.  -/
AkraBazziRecurrence.r_lt_n : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ}
  (self : AkraBazziRecurrence T g a b r) (i : α) (n : ℕ), self.n₀ ≤ n → r i n < n
-- Mathlib.Analysis.Normed.Group.Quotient
Submodule.Quotient.normedAddCommGroup : {M : Type u_1} →
  [inst : SeminormedAddCommGroup M] →
    {R : Type u_3} →
      [inst_1 : Ring R] → [inst_2 : Module R M] → (S : Submodule R M) → [hS : IsClosed ↑S] → NormedAddCommGroup (M ⧸ S)
-- Mathlib.Algebra.Lie.SerreConstruction
CartanMatrix.Generators.F.injEq : ∀ {B : Type v} (a a_1 : B), (CartanMatrix.Generators.F a = CartanMatrix.Generators.F a_1) = (a = a_1)
-- Mathlib.Topology.Algebra.UniformMulAction
UniformSpace.Completion.vadd_def : ∀ (M : Type v) (X : Type x) [inst : UniformSpace X] [inst_1 : VAdd M X] (c : M) (x : UniformSpace.Completion X),
  c +ᵥ x = UniformSpace.Completion.map (fun x => c +ᵥ x) x
-- Mathlib.Algebra.Group.AddChar
AddChar.mulShift_unit_eq_one_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : CommMonoid M] (ψ : AddChar R M) {u : R},
  IsUnit u → (ψ.mulShift u = 1 ↔ ψ = 1)
-- Init.Data.Vector.Perm
Vector.perm_iff_toArray_perm : ∀ {α : Type u_1} {n : ℕ} {as bs : Vector α n}, as.Perm bs ↔ as.toArray.Perm bs.toArray
-- Mathlib.CategoryTheory.Presentable.Basic
/-- An object `X` in a category is `κ`-presentable (for `κ` a regular cardinal)
when the functor `Hom(X, _)` preserves colimits indexed by
`κ`-filtered categories.  -/
CategoryTheory.IsCardinalPresentable : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → (κ : Cardinal.{w}) → [Fact κ.IsRegular] → Prop
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.coe_monoidHom : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] (f : α →*o β), ⇑↑f = ⇑f
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.restr_source' : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (s : Set X), IsOpen s → (e.restr s).source = e.source ∩ s
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.coreMonoidalTransport_εIso_inv : ∀ {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 D]
  {F G : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (i : F ≅ G),
  (CategoryTheory.Functor.Monoidal.coreMonoidalTransport i).εIso.inv =
    CategoryTheory.CategoryStruct.comp (i.inv.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.Functor.OplaxMonoidal.η F)
-- Lean.Parser.Types
_private.Lean.Parser.Types.0.Lean.Parser.SyntaxStack.mk.injEq : ∀ (raw : Array Lean.Syntax) (drop : ℕ) (raw_1 : Array Lean.Syntax) (drop_1 : ℕ),
  ({ raw := raw, drop := drop } = { raw := raw_1, drop := drop_1 }) = (raw = raw_1 ∧ drop = drop_1)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderFiniteCoproducts.isStableUnderCoproductsOfShape : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {W : CategoryTheory.MorphismProperty C}
  [self : W.IsStableUnderFiniteCoproducts] (J : Type) [Finite J], W.IsStableUnderCoproductsOfShape J
-- Mathlib.Data.Num.ZNum
PosNum.sub'.eq_4 : ∀ (a b : PosNum), a.bit0.sub' b.bit1 = (a.sub' b).bitm1
-- Mathlib.Topology.Metrizable.Basic
TopologicalSpace.IsSeparable.secondCountableTopology : ∀ {X : Type u_2} [inst : TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] {s : Set X},
  TopologicalSpace.IsSeparable s → SecondCountableTopology ↑s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ ∩ t₂).getKey? k = none
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.mulEquivSubgroup_apply : ∀ {G : Type u_2} [inst : Group G] {H K : Subgroup G} [inst_1 : H.Normal] (h : H.IsComplement' K)
  (a : ↥H ⋊[H.normalizerMonoidHom.comp (Subgroup.inclusion ⋯)] ↥K),
  (SemidirectProduct.mulEquivSubgroup h) a = ↑a.left * ↑a.right
-- Mathlib.RingTheory.Multiplicity
multiplicity_eq_of_emultiplicity_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst_1 : Monoid β] {a b : α} {c d : β},
  emultiplicity a b = emultiplicity c d → multiplicity a b = multiplicity c d
-- Std.Internal.Do.Order.Heyting
/-- Counit for `⇨`, the meet specialization of `PreservesSup.upperAdjoint_le`: `a ⊓ (a ⇨ b) ⊑ b`.  -/
Lean.Order.meet_himp_le : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] {a b : α} [Lean.Order.PreservesSup (Lean.Order.meet a)],
  Lean.Order.PartialOrder.rel (Lean.Order.meet a (Lean.Order.himp a b)) b
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.coe_div : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Div Y] (f g : LocallyConstant X Y),
  ⇑(f / g) = ⇑f / ⇑g
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.GrindTacticM.runAtGoal : {α : Type} →
  Lean.MVarId →
    Lean.Meta.Grind.Params →
      Lean.Elab.Tactic.Grind.GrindTacticM α →
        optParam Bool false → Lean.Elab.Tactic.TacticM (α × Lean.Elab.Tactic.Grind.State)
-- Mathlib.Order.Filter.Basic
Filter.generate_iUnion : ∀ {α : Type u} {ι : Sort x} {s : ι → Set (Set α)}, Filter.generate (⋃ i, s i) = ⨅ i, Filter.generate (s i)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.tensorLeftHomEquiv_whiskerRight_comp_evaluation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.HasLeftDual X] [inst_3 : CategoryTheory.HasLeftDual Y] (f : X ⟶ Y),
  (CategoryTheory.tensorLeftHomEquiv (ᘁY) (ᘁX) X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f ᘁY) (ε_ (ᘁY) Y)) =
    CategoryTheory.CategoryStruct.comp (ᘁf) (CategoryTheory.MonoidalCategoryStruct.rightUnitor ᘁX).inv
-- Mathlib.GroupTheory.GroupAction.Period
/-- If for some `n`, `(n • m) +ᵥ a = a`, then `period m a ≤ n`.  -/
AddAction.period_le_of_fixed : ∀ {α : Type v} {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α] {m : M} {a : α} {n : ℕ},
  0 < n → n • m +ᵥ a = a → AddAction.period m a ≤ n
-- Lean.Meta.Match.Match
/-- Find an alternative constraint of the form `x ≋ e` where `x` is an alternative
local declarations, and `x` and `e` have definitionally equal types.
Then, replace `x` with `e` in the alternative, and return it.
Return `none` if the alternative does not contain a constraint of this form.
 -/
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.solveSomeLocalFVarIdCnstr? : Lean.Meta.Match.Alt → Lean.MetaM (Option Lean.Meta.Match.Alt)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∈ m₂ → (m₁ ∩ m₂).getKey? k = m₁.getKey? k
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.toArray_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.toArray = t₂.toArray
-- Lean.Util.Trace
Lean.MonadAlwaysExcept.mk : {ε : outParam (Type u)} → {m : Type u → Type v} → MonadExceptOf ε m → Lean.MonadAlwaysExcept ε m
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.lt_symm_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (e : α ≃+o β) {x : α} {y : β}, x < e.symm y ↔ e x < y
-- Mathlib.RingTheory.Finiteness.Defs
Submodule.fg_iff_addSubmonoid_fg : ∀ {M : Type u_2} [inst : AddCommMonoid M] (P : Submodule ℕ M), P.FG ↔ P.FG
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
CategoryTheory.hasCardinalLT_arrow_walkingParallelFamily : ∀ {T : Type u} {κ : Cardinal.{w}},
  HasCardinalLT T κ →
    Cardinal.aleph0 ≤ κ → HasCardinalLT (CategoryTheory.Arrow (CategoryTheory.Limits.WalkingParallelFamily T)) κ
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
/-- The isomorphism `singleFunctor C n ≅ CochainComplex.singleFunctor C n ⋙ Q`.  -/
DerivedCategory.singleFunctorIsoCompQ : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] →
        (n : ℤ) → DerivedCategory.singleFunctor C n ≅ (CochainComplex.singleFunctor C n).comp DerivedCategory.Q
-- Mathlib.MeasureTheory.Group.Action
/-- See also `vadd_ae`.  -/
MeasureTheory.tendsto_vadd_ae : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : VAdd G α] (μ : MeasureTheory.Measure α)
  [MeasureTheory.VAddInvariantMeasure G α μ] (c : G),
  Filter.Tendsto (fun x => c +ᵥ x) (MeasureTheory.ae μ) (MeasureTheory.ae μ)
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.transitionMap_comp_eval_apply : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {m n : ℕ} (hmn : m ≤ n) (x : AdicCompletion I M), (AdicCompletion.transitionMap I M hmn) (↑x n) = ↑x m
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.ofSlice_next : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {h' : p ≠ (s.slice p₀ p₁ h).endPos},
  String.Slice.Pos.ofSlice (p.next h') = (String.Slice.Pos.ofSlice p).next ⋯
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.coe_compl : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : T2Space α]
  (s : TopologicalSpace.CompactOpens α), ↑sᶜ = (↑s)ᶜ
-- Mathlib.Analysis.Convex.Star
starConvex_iff_segment_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {x : E} {s : Set E}, StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → segment 𝕜 x y ⊆ s
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.continuous_coe : Continuous UpperHalfPlane.coe
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- If one nonempty affine subspace is less than another, the same applies to their directions  -/
AffineSubspace.direction_lt_of_nonempty : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {s₁ s₂ : AffineSubspace k P}, s₁ < s₂ → (↑s₁).Nonempty → s₁.direction < s₂.direction
-- Mathlib.Algebra.GroupWithZero.Commute
Commute.inv_left_iff₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {a b : G₀}, Commute a⁻¹ b ↔ Commute a b
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.Zoomed.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode.Path α → Sort u_2) →
    (x : RBTree.RBNode.Path α) →
      (Unit → motive RBTree.RBNode.Path.root) →
        ((c : RBTree.RBColor) →
            (parent : RBTree.RBNode.Path α) →
              (x : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left c parent x r)) →
          ((c : RBTree.RBColor) →
              (l : RBTree.RBNode α) →
                (x : α) → (parent : RBTree.RBNode.Path α) → motive (RBTree.RBNode.Path.right c l x parent)) →
            motive x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getKeyLE!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyLE! k = t₂.getKeyLE! k
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciInf_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α] {f : β × γ → α},
  BddBelow (Set.range f) → ⨅ p, f p = ⨅ b, ⨅ c, f (b, c)
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.pow_apply : ∀ {M : Type uM} {N : Type uN} [inst : MulOneClass M] [inst_1 : CommMonoid N] (f : M →* N) (n : ℕ) (x : M),
  (f ^ n) x = f x ^ n