mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.WithBot
WithBot.IsWellOrder.lt : ∀ {α : Type u_1} [inst : Preorder α] [IsWellOrder α fun x1 x2 => x1 < x2], IsWellOrder (WithBot α) fun x1 x2 => x1 < x2
-- Mathlib.Algebra.Regular.Basic
/-- If an element `b` becomes add-left-regular after adding to it on the left
an add-left-regular element, then `b` is add-left-regular.  -/
IsAddLeftRegular.of_add : ∀ {R : Type u_1} [inst : AddSemigroup R] {a b : R}, IsAddLeftRegular (a + b) → IsAddLeftRegular b
-- Lean.Meta.Tactic.Grind.Arith.CommRing.PP
_private.Lean.Meta.Tactic.Grind.Arith.CommRing.PP.0.Lean.Meta.Grind.Arith.CommRing.instMonadCanonM : Lean.Meta.Sym.Arith.MonadCanon Lean.Meta.Grind.Arith.CommRing.M✝
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.mk.injEq : ∀ {α : Type u} (next : Option α) (upperBound : α) (next_1 : Option α) (upperBound_1 : α),
  ({ next := next, upperBound := upperBound } = { next := next_1, upperBound := upperBound_1 }) =
    (next = next_1 ∧ upperBound = upperBound_1)
-- Init.Data.String.Basic
String.Slice.Pos.get_copy : ∀ {s : String.Slice} {pos : s.Pos} (h : pos.copy ≠ s.copy.endPos), pos.copy.get h = pos.get ⋯
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.up.eq_1 : ∀ (α : Type u_2) [inst : Add α] [inst_1 : IsRightCancelAdd α] [inst_2 : One α], ComplexShape.up α = ComplexShape.up' 1
-- Mathlib.GroupTheory.Nilpotent
Group.IsNilpotent.center_ne_bot : ∀ (G : Type u_1) [inst : Group G] [Nontrivial G] [Group.IsNilpotent G], Subgroup.center G ≠ ⊥
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.ψ_odd : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (m : ℤ),
  W.ψ (2 * m + 1) = W.ψ (m + 2) * W.ψ m ^ 3 - W.ψ (m - 1) * W.ψ (m + 1) ^ 3
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- `ContinuousAlternatingMap.ofSubsingleton` as a linear isometry.  -/
ContinuousAlternatingMap.ofSubsingletonLIE : {𝕜 : Type u} →
  {E : Type wE} →
    {F : Type wF} →
      {ι : Type v} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : SeminormedAddCommGroup E] →
            [inst_2 : NormedSpace 𝕜 E] →
              [inst_3 : SeminormedAddCommGroup F] →
                [inst_4 : NormedSpace 𝕜 F] →
                  [inst_5 : Fintype ι] → [Subsingleton ι] → ι → (E →L[𝕜] F) ≃ₗᵢ[𝕜] E [⋀^ι]→L[𝕜] F
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.toPartitionOfUnity_apply : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X),
  (f.toPartitionOfUnity i) x = (f i) x * ∏ᶠ (j : ι) (_ : WellOrderingRel j i), (1 - (f j) x)
-- Lean.ToExpr
Lean.instToExprName : Lean.ToExpr Lean.Name
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_comp_one_sub_X : ∀ {R : Type u} [inst : CommRing R] (p : Polynomial R) (k : ℕ),
  (⇑Polynomial.derivative)^[k] (p.comp (1 - Polynomial.X)) =
    (-1) ^ k * ((⇑Polynomial.derivative)^[k] p).comp (1 - Polynomial.X)
-- Lean.Environment
Lean.PersistentEnvExtensionDescrCore.mkInitial : {α β σ : Type} → Lean.PersistentEnvExtensionDescrCore α β σ → IO σ
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.le_linearGrowthInf_add : ∀ {u v : ℕ → EReal},
  LinearGrowth.linearGrowthInf u + LinearGrowth.linearGrowthInf v ≤ LinearGrowth.linearGrowthInf (u + v)
-- Mathlib.LinearAlgebra.Basis.VectorSpace
LinearMap.exists_extend_of_notMem : ∀ {K : Type u_3} {V : Type u_4} {V' : Type u_5} [inst : DivisionRing K] [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup V'] [inst_3 : Module K V] [inst_4 : Module K V'] {p : Submodule K V} {v : V} (f : ↥p →ₗ[K] V'),
  v ∉ p → ∀ (y : V'), ∃ g, g ∘ₗ p.subtype = f ∧ g v = y
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Comonad.delta_naturality_assoc : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Comonad C) ⦃X Y : C⦄ (f : X ⟶ Y) {Z : C}
  (h : T.obj (T.obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (T.map f) (CategoryTheory.CategoryStruct.comp (T.δ.app Y) h) =
    CategoryTheory.CategoryStruct.comp (T.δ.app X) (CategoryTheory.CategoryStruct.comp (T.map (T.map f)) h)
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isLittleO_norm_left`. -/
Asymptotics.IsLittleO.norm_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {f' : α → E'} {l : Filter α}, f' =o[l] g → (fun x => ‖f' x‖) =o[l] g
-- Mathlib.Order.Hom.Lattice
/-- Copy of a `SupHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
SupHom.copy : {α : Type u_2} →
  {β : Type u_3} → [inst : Max α] → [inst_1 : Max β] → (f : SupHom α β) → (f' : α → β) → f' = ⇑f → SupHom α β
-- Mathlib.Tactic.Sat.FromLRAT
Mathlib.Tactic.Sat.LRATStep.add.sizeOf_spec : ∀ (id : ℕ) (lits proof : Array ℤ),
  sizeOf (Mathlib.Tactic.Sat.LRATStep.add id lits proof) = 1 + sizeOf id + sizeOf lits + sizeOf proof
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
/-- For every `W` with a family of morphisms `e a : Y a ⟶ W` that coequalizes every pair of morphisms
`g₁ : Z ⟶ Y a₁`, `g₂ : Z ⟶ Y a₂` which the family `π` coequalizes, `desc e h` is a morphism
`X ⟶ W`...
 -/
CategoryTheory.EffectiveEpiFamilyStruct.desc : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {B : C} →
      {α : Type u_2} →
        {X : α → C} →
          {π : (a : α) → X a ⟶ B} →
            CategoryTheory.EffectiveEpiFamilyStruct X π →
              {W : C} →
                (e : (a : α) → X a ⟶ W) →
                  (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
                      CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
                        CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) →
                    (B ⟶ W)
-- Mathlib.RingTheory.Ideal.Maps
Submodule.annihilator_iSup : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (ι : Sort w)
  (f : ι → Submodule R M), (⨆ i, f i).annihilator = ⨅ i, (f i).annihilator
-- Mathlib.Order.Heyting.Basic
himp_compl_comm : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a b : α), a ⇨ bᶜ = b ⇨ aᶜ
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Every Schwartz function is differentiable at any point.  -/
SchwartzMap.differentiableAt : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (f : SchwartzMap E F) {x : E}, DifferentiableAt ℝ (⇑f) x
-- Mathlib.Order.Defs.Unbundled
IsEquiv.toIsPreorder : ∀ {α : Sort u_1} {r : α → α → Prop} [self : IsEquiv α r], IsPreorder α r
-- Mathlib.Algebra.GCDMonoid.Basic
IsGCDMonoid.intro : ∀ {α : Type u_2} [inst : CommMonoidWithZero α] (a : GCDMonoid α), IsGCDMonoid α
-- Std.Data.ExtDTreeMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `fallback`.
If a mapping exists the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.ExtDTreeMap.getKeyD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → α → α → α
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_neg_one : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.T R (-1) = Polynomial.X
-- Mathlib.CategoryTheory.Filtered.Small
/-- Implementation detail for the instance
`EssentiallySmall.{max v w} (FullSubcategory (cofilteredClosure f))`.  -/
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.inductiveStepRealization : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.IsCofilteredOrEmpty C] →
      (n : ℕ) →
        (X : (k : ℕ) → k < n → (t : Type (max v w)) × (t → C)) →
          CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep✝ n X → C
-- Mathlib.CategoryTheory.Localization.SmallHom
/-- The type of morphisms from `X` to `Y` in the localized category
with respect to `W : MorphismProperty C` that is shrunk to `Type w`
when `HasSmallLocalizedHom.{w} W X Y` holds.  -/
CategoryTheory.Localization.SmallHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (X Y : C) → [CategoryTheory.Localization.HasSmallLocalizedHom W X Y] → Type w
-- Std.Http.Data.Method
/-- Create a collection resource (WebDAV directory).
Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.3
 -/
Std.Http.Method.mkcol : Std.Http.Method
-- Std.Time.DateTime.WallTime
Std.Time.instLEWallTime : LE Std.Time.WallTime
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_inter_eq_size_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (∀ a ∈ m₂, a ∈ m₁) → (m₁ ∩ m₂).size = m₂.size
-- Mathlib.Probability.Distributions.SetBernoulli
ProbabilityTheory.map_ncard_setBernoulli_singleton : ∀ {ι : Type u_1} [Countable ι] {u : Set ι},
  u.Finite →
    ∀ (p : ↑unitInterval) (k : ℕ),
      (MeasureTheory.Measure.map Set.ncard (ProbabilityTheory.setBernoulli u p)) {k} =
        ENNReal.ofReal (↑(u.ncard.choose k) * ↑p ^ k * (1 - ↑p) ^ (u.ncard - k))
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.ext_iff : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] [inst_6 : AddCommMonoid F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul 𝕜 F]
  {p q : FormalMultilinearSeries 𝕜 E F}, p = q ↔ ∀ (n : ℕ), p n = q n
-- Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
/-- The `vonMangoldt` function is the function on natural numbers that returns `log p` if the input can
be expressed as `p^k` for a prime `p`.
In the case when `n` is a prime power, `Nat.minFac` will give the appropriate prime, as it is the
smallest prime factor.

In the `ArithmeticFunction` locale, we have the notation `Λ` for this function.
This is also available in the `ArithmeticFunction.vonMangoldt` locale, allowing for selective
access to the notation.
 -/
ArithmeticFunction.vonMangoldt.termΛ : Lean.ParserDescr
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Replicate
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Replicate.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate.aux3 : ∀ {n a b c : ℕ}, a < b * c → c < n → a < b * n
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).size = if t.contains k = true then t.size - 1 else t.size
-- Mathlib.Topology.Category.Profinite.Basic
/-- The type of profinite topological spaces.  -/
Profinite : Type (u_1 + 1)
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.isClosedMap : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsInducing f → IsClosed (Set.range f) → IsClosedMap f
-- Lean.Compiler.IR.Basic
Lean.IR.instInhabitedJoinPointId : Inhabited Lean.IR.JoinPointId
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_filterMap! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  [inst : Std.TransOrd α] {f : (a : α) → β a → Option (γ a)} {k : α} (h : t.WF)
  {h' : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filterMap! f t) = true},
  (Std.DTreeMap.Internal.Impl.filterMap! f t).getKey k h' = t.getKey k ⋯
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitCandidateWithAnchor.isRec : Lean.Meta.Grind.SplitCandidateWithAnchor → Bool
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Nat.nthRoot.go.eq_2 : ∀ (n a x fuel : ℕ),
  Nat.nthRoot.go n a fuel.succ x =
    if (a / x ^ (n + 1) + (n + 1) * x) / (n + 2) < x then
      Nat.nthRoot.go n a fuel ((a / x ^ (n + 1) + (n + 1) * x) / (n + 2))
    else x
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
addRothNumber_le_ruzsaSzemerediNumber : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : DecidableEq α] [inst_2 : CommRing α] [Fact (IsUnit 2)],
  Fintype.card α * addRothNumber Finset.univ ≤ ruzsaSzemerediNumber (α ⊕ α ⊕ α)
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.IsOrthogonal.coreflection_apply_left : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {i j : ι},
  P.IsOrthogonal i j → (P.coreflection j) (P.coroot i) = P.coroot i
-- Init.Grind.ToInt
/-- The embedding is monotone with respect to `≤`.  -/
Lean.Grind.ToInt.LE.le_iff : ∀ {α : Type u} {inst : LE α} {I : outParam Lean.Grind.IntInterval} {inst_1 : Lean.Grind.ToInt α I}
  [self : Lean.Grind.ToInt.LE α I] (x y : α), x ≤ y ↔ ↑x ≤ ↑y
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.containsThenInsert_fst : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] {k : α}
  {v : β k}, (m.containsThenInsert k v).1 = m.contains k
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.isIso_toCycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [CategoryTheory.Balanced C],
  S.Exact → ∀ [CategoryTheory.Mono S.f] [inst_4 : S.HasLeftHomology], CategoryTheory.IsIso S.toCycles
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.lidIsometry_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : TensorProduct 𝕜 𝕜 E), (TensorProduct.lidIsometry 𝕜 E) x = (TensorProduct.lid 𝕜 E) x
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.ofHom_apply : ∀ {X Y : Type u} [inst : Monoid X] [inst_1 : Monoid Y] (f : X →* Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (MonCat.ofHom f)) x = f x
-- Mathlib.Data.List.Cycle
/-- `nextOr` does not depend on the default value, if the next value appears.  -/
List.nextOr_eq_nextOr_of_mem_dropLast : ∀ {α : Type u_1} [inst : DecidableEq α] (xs : List α) (x d d' : α), x ∈ xs.dropLast → xs.nextOr x d = xs.nextOr x d'
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.conductor_pow_dvd : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) (m : ℕ),
  (χ ^ m).conductor ∣ χ.conductor
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueAdd.iff_card_le_one : ∀ {G : Type u_1} [inst : Add G] {A B : Finset G} {a0 b0 : G} [inst_1 : DecidableEq G],
  a0 ∈ A → b0 ∈ B → (UniqueAdd A B a0 b0 ↔ {p ∈ A ×ˢ B | p.1 + p.2 = a0 + b0}.card ≤ 1)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.ext_iff : ∀ {α : Type u_1} {x y : Matroid α}, x = y ↔ x.E = y.E ∧ x.IsBase = y.IsBase ∧ x.Indep = y.Indep
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.add_eq_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s t : Finset α}, s + t = ∅ ↔ s = ∅ ∨ t = ∅
-- Init.Meta.Defs
Lean.Syntax.hasArgs : Lean.Syntax → Bool
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkPullbackHom.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (x : ↑X),
  TopCat.Presheaf.stalkPullbackHom C f F x =
    CategoryTheory.CategoryStruct.comp
      ((TopCat.Presheaf.stalkFunctor C ((CategoryTheory.ConcreteCategory.hom f) x)).map
        ((TopCat.Presheaf.pullbackPushforwardAdjunction C f).unit.app F))
      (TopCat.Presheaf.stalkPushforward C f ((TopCat.Presheaf.pullback C f).obj F) x)
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- This is a specialization of `Quotient.lift_unique'` rather than `Quotient.lift_unique`, hence
the prime in the name.  -/
CategoryTheory.Cat.FreeRefl.lift_unique' : ∀ {V : Type u_2} [inst : CategoryTheory.ReflQuiver V] {D : Type u_4} [inst_1 : CategoryTheory.Category.{v_1, u_4} D]
  (F₁ F₂ : CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl V) D),
  (CategoryTheory.Cat.FreeRefl.quotientFunctor V).comp F₁ = (CategoryTheory.Cat.FreeRefl.quotientFunctor V).comp F₂ →
    F₁ = F₂
-- Mathlib.Logic.Small.Defs
not_small_type : ¬Small.{u, max (u + 1) (v + 1)} (Type (max u v))
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.isHashSelf_filterₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [ReflBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β} {f : (a : α) → β a → Bool},
  Std.DHashMap.Internal.Raw.WFImp ↑m → Std.DHashMap.Internal.IsHashSelf (↑(m.filterₘ f)).buckets
-- Init.Data.Nat.Basic
Nat.lt_asymm : ∀ {a b : ℕ}, a < b → ¬b < a
-- Init.Data.BitVec.Lemmas
BitVec.msb_concat : ∀ {w : ℕ} {b : Bool} {x : BitVec w}, (x.concat b).msb = if 0 < w then x.msb else b
-- Aesop.Forward.State
/-- The variable map for this cluster.  -/
Aesop.ClusterState.variableMap : Aesop.ClusterState → Aesop.VariableMap
-- Mathlib.Analysis.Calculus.Deriv.Mul
deriv_mul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {c d : 𝕜 → 𝔸},
  DifferentiableAt 𝕜 c x → DifferentiableAt 𝕜 d x → deriv (c * d) x = deriv c x * d x + c x * deriv d x
-- Mathlib.Topology.Separation.Regular
RegularSpace.of_hasBasis : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : X → Sort u_3} {p : (a : X) → ι a → Prop} {s : (a : X) → ι a → Set X},
  (∀ (a : X), (nhds a).HasBasis (p a) (s a)) → (∀ (a : X) (i : ι a), p a i → IsClosed (s a i)) → RegularSpace X
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.eqToHom_map_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} (p : X = Y) (q : Y = Z) {Z_1 : D} (h : F.obj Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom p))
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom q)) h) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom ⋯)) h
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.IsRamified.isMixed_conjugate_embedding : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K},
  NumberField.InfinitePlace.IsRamified k w →
    NumberField.ComplexEmbedding.IsMixed k (NumberField.ComplexEmbedding.conjugate w.embedding)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.one_lt_iff_one_lt : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀},
  v₁.IsEquiv v₂ → ∀ {x : R}, 1 < v₁ x ↔ 1 < v₂ x
-- Mathlib.Analysis.CStarAlgebra.Unitary.Span
selfAdjoint.unitarySelfAddISMul.congr_simp : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A]
  (a a_1 : ↥(selfAdjoint A)) (e_a : a = a_1) (ha_norm : ‖a‖ ≤ 1),
  selfAdjoint.unitarySelfAddISMul a ha_norm = selfAdjoint.unitarySelfAddISMul a_1 ⋯
-- Mathlib.Tactic.Translate.ToDual
/-- The `to_dual_insert_cast` attribute is used to tag declarations `foo` that should not be
unfolded in a proof that is translated. Instead, a rewrite with an equality theorem is inserted.
This equality theorem can then be translated by the translation attribute.  -/
Mathlib.Tactic.ToDual.«commandTo_dual_insert_cast_:=_» : Lean.ParserDescr
-- Mathlib.SetTheory.ZFC.Class
Class.coe_insert : ∀ (x y : ZFSet.{u}), ↑(insert x y) = insert x ↑y
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.optionMap_apply : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β), ⇑f.optionMap = Option.map ⇑f
-- Mathlib.Topology.Algebra.InfiniteSum.Real
dist_le_tsum_of_dist_le_of_tendsto₀ : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {f : ℕ → α} {a : α} (d : ℕ → ℝ),
  (∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n) → Summable d → Filter.Tendsto f Filter.atTop (nhds a) → dist (f 0) a ≤ tsum d
-- Mathlib.Topology.Algebra.Group.Basic
AddUnits.isEmbedding_val : ∀ {G : Type w} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [ContinuousNeg G], Topology.IsEmbedding AddUnits.val
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
/-- The cardinality of `(M ⧸ S)`, if `(M ⧸ S)` is finite, and `0` otherwise.
This is used to define the absolute ideal norm `Ideal.absNorm`.
 -/
Submodule.cardQuot : {R : Type u_1} →
  {M : Type u_2} → [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Submodule R M → ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
/-- The `PullbackCone` obtained by pasting two `PullbackCone`'s vertically  -/
CategoryTheory.Limits.PullbackCone.pasteVert : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ Y₁ : C} →
      {f₁ : X₂ ⟶ X₁} →
        {f₂ : X₃ ⟶ X₂} →
          {i₁ : Y₁ ⟶ X₁} →
            (t₁ : CategoryTheory.Limits.PullbackCone i₁ f₁) →
              {i₂ : t₁.pt ⟶ X₂} →
                CategoryTheory.Limits.PullbackCone i₂ f₂ →
                  i₂ = t₁.snd → CategoryTheory.Limits.PullbackCone i₁ (CategoryTheory.CategoryStruct.comp f₂ f₁)
-- Mathlib.Data.Nat.Init
/-- A natural number `m` divides the sum `n + m` if and only if `m` divides `n`.  -/
Nat.dvd_add_self_right : ∀ {m n : ℕ}, m ∣ n + m ↔ m ∣ n
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- Auxiliary type for normalizing `Ring` and `Field` equalities.  -/
Lean.Meta.Grind.Arith.Linear.RingEqCnstr : Type
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- The right unitor as a bimodule isomorphism.  -/
Bimod.rightUnitorBimod : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Limits.HasCoequalizers C] →
        [inst_3 :
            ∀ (X : C),
              CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                (CategoryTheory.MonoidalCategory.tensorLeft X)] →
          [inst_4 :
              ∀ (X : C),
                CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                  (CategoryTheory.MonoidalCategory.tensorRight X)] →
            {X Y : CategoryTheory.Mon C} → (M : Bimod X Y) → M.tensorBimod (Bimod.regular Y) ≅ M
-- Init.Core
PSigma.mk.sizeOf_spec : ∀ {α : Sort u} {β : α → Sort v} [inst : SizeOf α] [inst_1 : (a : α) → SizeOf (β a)] (fst : α) (snd : β fst),
  sizeOf ⟨fst, snd⟩ = 1 + sizeOf fst + sizeOf snd
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- The canonical isomorphism relating `span f.unop g.unop` and `(cospan f g).leftOp`  -/
CategoryTheory.Limits.spanUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : Cᵒᵖ} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          CategoryTheory.Limits.span f.unop g.unop ≅
            CategoryTheory.Limits.walkingCospanOpEquiv.inverse.comp (CategoryTheory.Limits.cospan f g).leftOp
-- Init.Data.Ord.Basic
Ordering.eq_swap_iff_eq_eq : ∀ {o : Ordering}, o = o.swap ↔ o = Ordering.eq
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
WStarAlgebra.mk : ∀ {M : Type u} [inst : CStarAlgebra M],
  (∃ X x x_1, ∃ (_ : CompleteSpace X), Nonempty (StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)) → WStarAlgebra M
-- Lean.Elab.App
Lean.Elab.Term.elabIdent : Lean.Elab.Term.TermElab
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.SymmetricRelation.symmetry₁_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.SymmetricRelation p₁ p₂) {F : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_1 : CategoryTheory.ConcreteCategory C F]
  (x : carrier R),
  (CategoryTheory.ConcreteCategory.hom p₁) ((CategoryTheory.ConcreteCategory.hom self.s) x) =
    (CategoryTheory.ConcreteCategory.hom p₂) x