mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Lemmas
List.elem_eq_contains : ∀ {α : Type u_1} [inst : BEq α] {a : α} {l : List α}, List.elem a l = l.contains a
-- Init.Data.String.Basic
ByteArray.utf8Decode?.go.eq_1 : ∀ (b : ByteArray) (i : ℕ) (acc : Array Char) (hi : i ≤ b.size),
  ByteArray.utf8Decode?.go b i acc hi =
    if i < b.size then
      match h : b.utf8DecodeChar? i with
      | none => none
      | some c => ByteArray.utf8Decode?.go b (i + c.utf8Size) (acc.push c) ⋯
    else some acc
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.map_id : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R), (MvPolynomial.map (RingHom.id R)) p = p
-- Std.Async.Basic
/-- This function transforms the operation inside the monad `m` into a task and let it run in the background.
 -/
Std.Async.background : {m t : Type → Type} →
  {α : Type} → [Monad m] → [Std.Async.MonadAsync t m] → m α → optParam Task.Priority Task.Priority.default → m Unit
-- Mathlib.Order.Filter.IsBounded
Filter.isBoundedUnder_of_eventually_ge : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {f : Filter β} {u : β → α} {a : α},
  (∀ᶠ (x : β) in f, a ≤ u x) → Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f u
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_mul_left_singleton : ∀ {α : Type u_2} [inst : Group α] {a b : α}, (fun x => a * x) ⁻¹' {b} = {a⁻¹ * b}
-- Mathlib.Geometry.Manifold.StructureGroupoid
instSetLikeStructureGroupoidOpenPartialHomeomorph : (H : Type u_2) → [inst : TopologicalSpace H] → SetLike (StructureGroupoid H) (OpenPartialHomeomorph H H)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.append_right_cons : ∀ {n m : ℕ} {α : Sort u_2} (xs : Fin n → α) (y : α) (ys : Fin m → α),
  Fin.append xs (Fin.cons y ys) = Fin.append (Fin.snoc xs y) ys ∘ Fin.cast ⋯
-- Mathlib.Topology.Order.Lattice
Filter.Tendsto.finset_inf_nhds : ∀ {L : Type u_1} [inst : TopologicalSpace L] {ι : Type u_3} {α : Type u_4} {s : Finset ι} {f : ι → α → L} {l : Filter α}
  {g : ι → L} [inst_1 : SemilatticeInf L] [inst_2 : OrderTop L] [ContinuousInf L],
  (∀ i ∈ s, Filter.Tendsto (f i) l (nhds (g i))) → Filter.Tendsto (s.inf f) l (nhds (s.inf g))
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {k : α}, k ∉ m₂ → (m₁ \ m₂).get! k = m₁.get! k
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.instProjectiveXExtend : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (e : c.Embedding c') (K : HomologicalComplex C c)
  [∀ (i : ι), CategoryTheory.Projective (K.X i)] (i' : ι'), CategoryTheory.Projective ((K.extend e).X i')
-- Lean.Elab.DeclModifiers
Lean.Elab.ComputeKind.regular : Lean.Elab.ComputeKind
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.monoid.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α],
  Finset.monoid = Function.Injective.monoid SetLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- Suppose an indexed family of points is given, along with a subset
of the index type.  A vector can be expressed as
`weightedVSubOfPoint` using a `Finset` lying within that subset and
with a given sum of weights if and only if it can be expressed as
`weightedVSubOfPoint` with that sum of weights for the
corresponding indexed family whose index type is the subtype
corresponding to that subset.  -/
Finset.eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype : ∀ {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] {ι : Type u_4} {v : V} {x : k} {s : Set ι} {p : ι → P} {b : P},
  (∃ fs, ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = x ∧ v = (fs.weightedVSubOfPoint p b) w) ↔
    ∃ fs w, ∑ i ∈ fs, w i = x ∧ v = (fs.weightedVSubOfPoint (fun i => p ↑i) b) w
-- Mathlib.Combinatorics.Enumerative.Bell
Nat.bell_zero : Nat.bell 0 = 1
-- Mathlib.Algebra.GroupWithZero.WithZero
/-- If `α` is a group then `WithZero α` is a group with zero.  -/
WithZero.instGroupWithZero : {α : Type u_1} → [Group α] → GroupWithZero (WithZero α)
-- Mathlib.Order.Filter.Pointwise
Filter.pureMulHom_apply : ∀ {α : Type u_2} [inst : Mul α] (a : α), Filter.pureMulHom a = pure a
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {l : List α} {k : α},
  k ∉ m → l.contains k = false → (m.insertManyIfNewUnit l).getKey! k = default
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.instInhabited : {α : Type u_1} → Inhabited (Ordnode α)
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.instFullHomologicalComplexMapHomologicalComplexOfFaithful : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {W : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_2} W] [inst_3 : CategoryTheory.Preadditive W]
  (F : CategoryTheory.Functor V W) [inst_4 : F.Additive] (c : ComplexShape ι) [F.Faithful] [F.Full],
  (F.mapHomologicalComplex c).Full
-- Lean.Data.Json.FromToJson.Basic
Lean.instFromJsonName : Lean.FromJson Lean.Name
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.hasColimitsOfShape_iff_isRightAdjoint_const : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C],
  CategoryTheory.Limits.HasColimitsOfShape J C ↔ (CategoryTheory.Functor.const J).IsRightAdjoint
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.rootSpace_one_div_two_smul : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [inst_6 : H.IsCartanSubalgebra]
  [LieModule.IsTriangularizable K (↥H) L] (α : LieModule.Weight K (↥H) L),
  α.IsNonZero → LieAlgebra.rootSpace H (2⁻¹ • ⇑α) = ⊥
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.getElem_toArray_eq : ∀ {α : Type u} [inst : Std.PRange.Least? α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxo.IsAlwaysFinite α] {r : Std.Rio α} {i : ℕ} {h : i < r.toArray.size},
  r.toArray[i] = (Std.PRange.succMany? i Std.PRange.UpwardEnumerable.least).get ⋯
-- Init.Data.Int.Linear
Int.Internal.Linear.norm_le : ∀ (ctx : Int.Internal.Linear.Context) (lhs rhs : Int.Internal.Linear.Expr) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.norm_eq_cert lhs rhs p = true →
    (Int.Internal.Linear.Expr.denote ctx lhs ≤ Int.Internal.Linear.Expr.denote ctx rhs) =
      (Int.Internal.Linear.Poly.denote' ctx p ≤ 0)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.functorPullback_pushforward_covering : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D}
  {G : CategoryTheory.Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {X : C} (T : ↑(K (G.obj X))),
  CategoryTheory.Sieve.functorPushforward G (CategoryTheory.Sieve.functorPullback G ↑T) ∈ K (G.obj X)
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.instHasLimitsOfShape : ∀ {C : Type u_1} {ι : Type u_2} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} J] {c : ComplexShape ι}
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasLimitsOfShape J C],
  CategoryTheory.Limits.HasLimitsOfShape J (HomologicalComplex C c)
-- Std.Http.Protocol.H1
Std.Http.Protocol.H1.Machine.mk.sizeOf_spec : ∀ {dir : Std.Http.Protocol.H1.Direction} (reader : Std.Http.Protocol.H1.Reader dir)
  (writer : Std.Http.Protocol.H1.Writer dir) (config : Std.Http.Protocol.H1.Config)
  (events : Array (Std.Http.Protocol.H1.Event dir)) (error : Option Std.Http.Protocol.H1.Error)
  (instant : Option Std.Time.PlainDateTime) (keepAlive forcedFlush pullBodyStalled : Bool),
  sizeOf
      { reader := reader, writer := writer, config := config, events := events, error := error, instant := instant,
        keepAlive := keepAlive, forcedFlush := forcedFlush, pullBodyStalled := pullBodyStalled } =
    1 + sizeOf reader + sizeOf writer + sizeOf config + sizeOf events + sizeOf error + sizeOf instant +
          sizeOf keepAlive +
        sizeOf forcedFlush +
      sizeOf pullBodyStalled
-- Lean.Data.PersistentHashSet
Lean.PersistentHashSet.instInhabited : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Inhabited (Lean.PersistentHashSet α)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.rightUnitor_hom_base_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (X : B),
  φ.rightUnitor.hom.base.app X = CategoryTheory.CategoryStruct.id (φ.base.obj X)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.ofFixingSubgroupEmpty_equivariantMap_bijective : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α],
  Function.Bijective ⇑(SubMulAction.ofFixingSubgroup_equivariantMap M ∅)
-- Lean.Meta.Tactic.Replace
/-- Like `Lean.MVarId.withReverted`, but reverts all local variables starting from `fvarId`.
 -/
Lean.MVarId.withRevertedFrom : {α : Type} →
  Lean.MVarId →
    Lean.FVarId →
      (Lean.MVarId → Array Lean.FVarId → Lean.MetaM (α × Array (Option Lean.FVarId) × Lean.MVarId)) →
        Lean.MetaM (α × Lean.MVarId)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.stmts₁_trans : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {q₁ q₂ : Turing.TM1.Stmt Γ Λ σ},
  q₁ ∈ Turing.TM1.stmts₁ q₂ → Turing.TM1.stmts₁ q₁ ⊆ Turing.TM1.stmts₁ q₂
-- Mathlib.Util.Export
Lean.Export.Entry.name.inj : ∀ {n n_1 : Lean.Name}, Lean.Export.Entry.name n = Lean.Export.Entry.name n_1 → n = n_1
-- Mathlib.Tactic.Finiteness
/-- `finiteness` proves goals of the form `*** < ∞` and (equivalently) `*** ≠ ∞` in the extended
nonnegative reals (`ℝ≥0∞`). If the goal cannot be proven, `finiteness` prints a warning and shows
its intermediate progress.

This tactic is based on `aesop`. It calls `assumption`, `intros`, `positivity`, and any
lemma or rule added to the `finiteness` ruleset, except that all `simp` rules are disabled.

This tactic is extensible. By adding more rules, `finiteness` can prove more goals. For example:
* `@[aesop (rule_sets := [finiteness]) safe 50] lemma ...`
* `add_aesop_rules safe tactic (rule_sets := [finiteness]) (by ...)`

(Note that a `simp` rule cannot be added this way, since all `simp` rules are disabled.)

* `finiteness (clause)` customizes the `aesop` call using the given clause. See `aesop`
  documentation for detailed explanation. Note that `finiteness` disables `simp`, so
  `finiteness (add simp [lemma1, lemma2])` does not do anything more than a bare `finiteness`.
* `finiteness [t₁, ..., tₙ]` adds the terms `t₁`, ..., `tₙ` as local hypotheses before applying
  the search rules.
* `finiteness?` additionally shows the proof that `finiteness` found.
* `finiteness_nonterminal` is a version of `finiteness` that does not report a warning if it fails
  to close the goal.
 -/
finiteness_nonterminal : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_filter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  [inst_1 : Inhabited α] {f : α → β → Bool} {k : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.getKey! k =
    ((t.getKey? k).pfilter fun x h' => f x (Std.DTreeMap.Internal.Impl.Const.get t x ⋯)).get!
-- Mathlib.Data.Set.Sups
Set.infs_inter_subset_right : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s t₁ t₂ : Set α}, s ⊼ (t₁ ∩ t₂) ⊆ s ⊼ t₁ ∩ s ⊼ t₂
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.pushoutCocone_pt : ∀ (R A B : Type u) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B] [inst_3 : Algebra R A]
  [inst_4 : Algebra R B], (CommRingCat.pushoutCocone R A B).pt = CommRingCat.of (TensorProduct R A B)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.jmp : {pu : Lean.Compiler.LCNF.Purity} → Lean.FVarId → Array (Lean.Compiler.LCNF.Arg pu) → Lean.Compiler.LCNF.Code pu
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.mk' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P},
  CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr →
    (∀ ⦃T : C⦄ ⦃φ φ' : P ⟶ T⦄,
        CategoryTheory.CategoryStruct.comp inl φ = CategoryTheory.CategoryStruct.comp inl φ' →
          CategoryTheory.CategoryStruct.comp inr φ = CategoryTheory.CategoryStruct.comp inr φ' → φ = φ') →
      (∀ ⦃T : C⦄ (a : X ⟶ T) (b : Y ⟶ T),
          CategoryTheory.CategoryStruct.comp f a = CategoryTheory.CategoryStruct.comp g b →
            ∃ l, CategoryTheory.CategoryStruct.comp inl l = a ∧ CategoryTheory.CategoryStruct.comp inr l = b) →
        CategoryTheory.IsPushout f g inl inr
-- Init.Data.List.Lemmas
List.getElem_of_mem : ∀ {α : Type u_1} {a : α} {l : List α}, a ∈ l → ∃ i, ∃ (h : i < l.length), l[i] = a
-- Mathlib.Analysis.Convex.Caratheodory
Caratheodory.affineIndependent_minCardFinsetOfMemConvexHull : ∀ {𝕜 : Type u_1} {E : Type u} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s : Set E} {x : E} (hx : x ∈ (convexHull 𝕜) s),
  AffineIndependent 𝕜 Subtype.val
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.whiskerLeft_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X : C)
  {Y Z : C} (f : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)
      (CategoryTheory.SemiCartesianMonoidalCategory.snd X Z) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y) f
-- Mathlib.Data.Finset.Sups
Finset.univ_sups_univ : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] [inst_2 : Fintype α],
  Finset.univ ⊻ Finset.univ = Finset.univ
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.le_def : ∀ {α : Type u_2} [inst : TopologicalSpace α] {β : Type u_5} [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  [inst_3 : PartialOrder β] {f g : CompactlySupportedContinuousMap α β}, f ≤ g ↔ ∀ (a : α), f a ≤ g a
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- The category of locally ringed spaces.  -/
AlgebraicGeometry.LocallyRingedSpace.instCategory : CategoryTheory.Category.{u, u + 1} AlgebraicGeometry.LocallyRingedSpace
-- Init.Data.String.Basic
String.Pos.get_eq_get_toSlice : ∀ {s : String} {p : s.Pos} {h : p ≠ s.endPos}, p.get h = p.toSlice.get ⋯
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.Const.alter!.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (sz : ℕ) →
      (k' : α) →
        (v' : β) →
          (l' r' : Std.DTreeMap.Internal.Impl α fun x => β) → motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r')),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner sz k' v' l' r' => h_2 sz k' v' l' r') =
    h_1 ()
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cosh_periodic : Function.Periodic Complex.cosh (2 * ↑Real.pi * Complex.I)
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.coe_algebraMap : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddMonoid M], ⇑(algebraMap R (AddMonoidAlgebra A M)) = AddMonoidAlgebra.single 0 ∘ ⇑(algebraMap R A)
-- Mathlib.LinearAlgebra.Pi
/-- Linear equivalence between dependent functions `(i : Fin 2) → M i` and `M 0 × M 1`.  -/
LinearEquiv.piFinTwo : (R : Type u) →
  [inst : Semiring R] →
    (M : Fin 2 → Type v) →
      [inst_1 : (i : Fin 2) → AddCommMonoid (M i)] →
        [inst_2 : (i : Fin 2) → Module R (M i)] → ((i : Fin 2) → M i) ≃ₗ[R] M 0 × M 1
-- Init.Grind.Ring.Envelope
Lean.Grind.CommRing.OfCommSemiring.mul_comm : ∀ {α : Type u} [inst : Lean.Grind.CommSemiring α] (a b : Lean.Grind.Ring.OfSemiring.Q α),
  Lean.Grind.Ring.OfSemiring.mul a b = Lean.Grind.Ring.OfSemiring.mul b a
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
derivWithin_rpow_const : ∀ {f : ℝ → ℝ} {x p : ℝ} {s : Set ℝ},
  DifferentiableWithinAt ℝ f s x →
    f x ≠ 0 ∨ 1 ≤ p →
      UniqueDiffWithinAt ℝ s x → derivWithin (fun x => f x ^ p) s x = derivWithin f s x * p * f x ^ (p - 1)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.comapDomain_single_of_not_mem_range : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] {f : M → N} {r : R} {n : N},
  n ∉ Set.range f → ∀ (hf : Function.Injective f), MonoidAlgebra.comapDomain f hf (MonoidAlgebra.single n r) = 0
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.find? : {α : Type u_1} → {β : Type u_2} → {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α β → α → Option β
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.comap_loops : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid β} {f : α → β}, (M.comap f).loops = f ⁻¹' M.loops
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.IsMaximal.isPrime : ∀ {α : Type u} [inst : CommSemiring α] {I : Ideal α}, I.IsMaximal → I.IsPrime
-- Lean.Expr
Lean.instBEqData_1 : BEq Lean.Expr.Data
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientEquiv_symm_apply : ∀ {R : Type u} [inst : Ring R] {S : Type v} [inst_1 : Ring S] (I : Ideal R) (J : Ideal S) [inst_2 : I.IsTwoSided]
  [inst_3 : J.IsTwoSided] (f : R ≃+* S) (hIJ : J = Ideal.map (↑f) I) (a : S ⧸ J),
  (I.quotientEquiv J f hIJ).symm a = (Ideal.quotientMap I ↑f.symm ⋯) a
-- Mathlib.CategoryTheory.Monoidal.Opposite
/-- The identification `- ⊗ mop X = mop (- ⊗ unmop X)` as a natural isomorphism.  -/
CategoryTheory.MonoidalOpposite.tensorRightMopIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X : C) →
        CategoryTheory.MonoidalCategory.tensorRight { unmop := X } ≅
          (CategoryTheory.unmopFunctor C).comp
            ((CategoryTheory.MonoidalCategory.tensorLeft X).comp (CategoryTheory.mopFunctor C))
-- Mathlib.FieldTheory.SeparableClosure
Field.insepDegree_le_rank : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  Field.insepDegree F E ≤ Module.rank F E
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_iff_isSome_get? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α}, a ∈ t ↔ (t.get? a).isSome = true
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. `alterP cut f t` simultaneously handles inserting, erasing and replacing an element
using a function `f : Option α → Option α`. It is passed the result of `t.findP? cut`
and can either return `none` to remove the element or `some a` to replace/insert
the element with `a` (which must have the same ordering properties as the original element).

The element is used linearly if `t` is unshared.

The `AlterWF` assumption is required because `f` may change
the ordering properties of the element, which would break the invariants.
 -/
RBTree.RBSet.alterP : {α : Type u_1} →
  {cmp : α → α → Ordering} →
    (t : RBTree.RBSet α cmp) →
      (cut : α → Ordering) → (f : Option α → Option α) → [wf : t.AlterWF cut f] → RBTree.RBSet α cmp
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.contains_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, (m₁ ∪ m₂).contains k = (m₁.contains k || m₂.contains k)
-- Mathlib.RingTheory.Ideal.Maps
Submodule.annihilator_sup : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (N P : Submodule R M), (N ⊔ P).annihilator = N.annihilator ⊓ P.annihilator
-- Init.Data.Order.MinMaxOn
apply_minOn_le_right : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x y : α},
  f (minOn f x y) ≤ f y
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.map : ∀ {M : Type u_1} [inst : AddCommMonoid M] {a b p : M} {N : Type u_2} {F : Type u_3} [inst_1 : AddCommMonoid N]
  [inst_2 : FunLike F M N] [AddMonoidHomClass F M N] (f : F), a ≡ b [PMOD p] → f a ≡ f b [PMOD f p]
-- Mathlib.Topology.Category.Stonean.Adjunctions
/-- The equivalence of homsets to establish the adjunction between the Stone-Cech compactification
functor and the forgetful functor.  -/
Stonean.stoneCechEquivalence : (X : Type u) → (Y : Stonean) → (Stonean.stoneCechObj X ⟶ Y) ≃ (X ⟶ ↑Y.toTop)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.comp_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G X Y : C} [inst_2 : CategoryTheory.AddGrpObj G] (f : X ⟶ Y) (g : Y ⟶ G),
  CategoryTheory.CategoryStruct.comp f (-g) = -CategoryTheory.CategoryStruct.comp f g
-- Mathlib.NumberTheory.LSeries.RiemannZeta
HurwitzZeta.completedHurwitzZetaEven₀_zero : ∀ (s : ℂ), HurwitzZeta.completedHurwitzZetaEven₀ 0 s = completedRiemannZeta₀ s
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.isLocallyDirected : ∀ {X : AlgebraicGeometry.Scheme} (F : CategoryTheory.Functor X.AffineZariskiSiteᵒᵖ CommRingCat)
  (α : (AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).op.comp X.presheaf ⟶ F),
  CategoryTheory.NatTrans.Coequifibered α →
    ((F.rightOp.comp AlgebraicGeometry.Scheme.Spec).comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected
-- Lean.Meta.Match.SimpH
_private.Lean.Meta.Match.SimpH.0.Lean.Meta.Match.SimpH.State.xs : Lean.Meta.Match.SimpH.State✝ → List Lean.FVarId
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- An `AddSubgroup` of an `AddCommGroup` is an `AddCommGroup`.  -/
AddSubgroup.toAddCommGroup : {G : Type u_3} → [inst : AddCommGroup G] → (H : AddSubgroup G) → AddCommGroup ↥H
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.stepAux.eq_3 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] (x : σ)
  (x_1 : (k : K) → List (Γ k)) (k : K) (f : σ → Option (Γ k) → σ) (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2.stepAux (Turing.TM2.Stmt.pop k f q) x x_1 =
    Turing.TM2.stepAux q (f x (x_1 k).head?) (Function.update x_1 k (x_1 k).tail)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSemanticTokens.fromJson : Lean.Json → Except String Lean.Lsp.SemanticTokens
-- Init.Data.UInt.Bitwise
UInt32.not_neg_one : ~~~(-1) = 0
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.continuous : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂), Continuous ⇑f
-- Mathlib.Analysis.Complex.Trigonometric
Real.cos_one_pos : 0 < Real.cos 1