mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Floor.Defs
/-- `FloorSemiring.floor` of a negative element is zero.  -/
FloorSemiring.floor_of_neg : ∀ {α : Type u_4} {inst : Semiring α} {inst_1 : PartialOrder α} [self : FloorSemiring α] {a : α},
  a < 0 → FloorSemiring.floor a = 0
-- Init.Data.String.Pattern.Basic
/-- Converts a `SearchStep (s.sliceFrom p)` into a `SearchStep s` by applying
`Slice.Pos.ofSliceFrom` to the start and end position.
 -/
String.Slice.Pattern.SearchStep.ofSliceFrom : {s : String.Slice} → {p : s.Pos} → String.Slice.Pattern.SearchStep (s.sliceFrom p) → String.Slice.Pattern.SearchStep s
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
/-- `Rel` relates each `ι m * ι m`, for `m : M`, with `Q m`.

The Clifford algebra of `M` is defined as the quotient modulo this relation.
 -/
CliffordAlgebra.Rel : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → QuadraticForm R M → TensorAlgebra R M → TensorAlgebra R M → Prop
-- Batteries.Data.BinomialHeap.Basic
/-- `O(1)`. Is the heap empty?  -/
Batteries.BinomialHeap.Imp.Heap.isEmpty : {α : Type u_1} → Batteries.BinomialHeap.Imp.Heap α → Bool
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalOpen : Lean.Elab.Tactic.Tactic
-- Init.Data.String.Lemmas.Pattern.Split.Char
_private.Init.Data.String.Lemmas.Pattern.Split.Char.0.String.Slice.Pattern.Model.split.match_1.splitter : {s : String.Slice} →
  (motive : Option s.Pos → Sort u_1) →
    (x : Option s.Pos) → ((pos : s.Pos) → x = some pos → motive (some pos)) → (x = none → motive none) → motive x
-- Lean.Elab.Match
Lean.Elab.Term.PatternVarDecl.mk : Lean.FVarId → Lean.Elab.Term.PatternVarDecl
-- Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
AlgebraicGeometry.AffineTargetMorphismProperty.toProperty.eq_1 : ∀ (P : AlgebraicGeometry.AffineTargetMorphismProperty) (x x_1 : AlgebraicGeometry.Scheme) (f : x ⟶ x_1),
  P.toProperty f = ∃ (h : AlgebraicGeometry.IsAffine x_1), P f
-- Mathlib.Data.Vector3
/-- Append two vectors  -/
Vector3.append : {α : Type u_1} → {m n : ℕ} → Vector3 α m → Vector3 α n → Vector3 α (n + m)
-- Init.Data.ByteArray.Basic
/-- The byte at the current position.

On an invalid position, returns `(default : UInt8)`.
 -/
ByteArray.Iterator.curr : ByteArray.Iterator → UInt8
-- Mathlib.CategoryTheory.Sites.Types
/-- A Grothendieck topology associated to the category of all types.
A sieve is a covering iff it is jointly surjective.  -/
CategoryTheory.typesGrothendieckTopology : CategoryTheory.GrothendieckTopology (Type u)
-- Mathlib.Data.Nat.Factorization.Induction
/-- Given `P 0`, `P (p ^ n)` for all prime powers, and a way to extend `P a` and `P b` to
`P (a * b)` when `a, b` are positive coprime, we can define `P` for all natural numbers.  -/
Nat.recOnPrimeCoprime : {motive : ℕ → Sort u_1} →
  motive 0 →
    ((p n : ℕ) → Nat.Prime p → motive (p ^ n)) →
      ((a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)) → (a : ℕ) → motive a
-- Mathlib.Analysis.Complex.Norm
Complex.norm_real : ∀ (r : ℝ), ‖↑r‖ = ‖r‖
-- Init.Data.List.Range
List.getElem_range : ∀ {j n : ℕ} (h : j < (List.range n).length), (List.range n)[j] = j
-- Init.Data.Vector.Lemmas
Vector.findSomeRev?_mk : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Array α} (h : xs.size = n) (f : α → Option β),
  Vector.findSomeRev? f (Vector.mk xs h) = Array.findSomeRev? f xs
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.qsmul_eq_C_mul : ∀ {R : Type u} [inst : DivisionRing R] (a : ℚ) (f : Polynomial R), a • f = Polynomial.C ↑a * f
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_atTop : ∀ {β : Type u_2} [Nonempty β] [inst : SemilatticeSup β] {f : β → ENNReal} {a : ENNReal},
  a ≠ ⊤ → (Filter.Tendsto f Filter.atTop (nhds a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ∈ Set.Icc (a - ε) (a + ε))
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.polynomial.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve.Affine R),
  W.polynomial =
    Polynomial.X ^ 2 + Polynomial.C (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃) * Polynomial.X -
      Polynomial.C
        (Polynomial.X ^ 3 + Polynomial.C W.a₂ * Polynomial.X ^ 2 + Polynomial.C W.a₄ * Polynomial.X + Polynomial.C W.a₆)
-- Mathlib.RingTheory.Frobenius
/-- `φ : S →ₐ[R] S` is an (arithmetic) Frobenius at `Q` if
`φ x ≡ x ^ #(R/p) (mod Q)` for all `x : S` (`AlgHom.IsArithFrobAt`).  -/
AlgHom.IsArithFrobAt : {R : Type u_1} →
  {S : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (S →ₐ[R] S) → Ideal S → Prop
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.pentagon_hom_hom_inv_inv_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W
          (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
        (CategoryTheory.MonoidalCategoryStruct.associator W X
            (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).inv) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator W X Y).inv
        Z)
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).hom
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.simpArrow : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Result
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressParams.mk.inj : ∀ {workDoneToken? workDoneToken?_1 : Option Lean.Lsp.ProgressToken},
  { workDoneToken? := workDoneToken? } = { workDoneToken? := workDoneToken?_1 } → workDoneToken? = workDoneToken?_1
-- Mathlib.GroupTheory.OrderOfElement
AddSubgroup.addOrderOf_le_card : ∀ {G : Type u_6} [inst : AddGroup G] (s : AddSubgroup G), (↑s).Finite → ∀ {x : G}, x ∈ s → addOrderOf x ≤ Nat.card ↥s
-- Aesop.Tree.ExtractProof
_private.Aesop.Tree.ExtractProof.0.Aesop.SafePrefixState.goals : Aesop.SafePrefixState✝ → Array Lean.MVarId
-- Mathlib.CategoryTheory.Center.Basic
CategoryTheory.CatCenter.naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (z : CategoryTheory.CatCenter C) {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp f (z.app Y) = CategoryTheory.CategoryStruct.comp (z.app X) f
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_cons_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.getEntry? k (⟨k, v⟩ :: l) = some ⟨k, v⟩
-- Init.Data.List.Range
List.zipIdx_cons' : ∀ {α : Type u_1} {i : ℕ} {x : α} {xs : List α},
  (x :: xs).zipIdx i = (x, i) :: List.map (Prod.map id fun x => x + 1) (xs.zipIdx i)
-- Std.Internal.Do.PredTrans
/-- Push an `Option α` result into separate normal and none postconditions:
`some a` uses `post a`, and `none` uses `epost.head`.  -/
Std.Internal.Do.EPost.Cons.pushOption : {α Pred : Type u} → {EPred : Type v} → (α → Pred) → EPost.Cons✝ Pred EPred → Option α → Pred
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.as.inj : ∀ {varId : Lean.FVarId} {p : Lean.Meta.Match.Pattern} {hId varId_1 : Lean.FVarId} {p_1 : Lean.Meta.Match.Pattern}
  {hId_1 : Lean.FVarId},
  Lean.Meta.Match.Pattern.as varId p hId = Lean.Meta.Match.Pattern.as varId_1 p_1 hId_1 →
    varId = varId_1 ∧ p = p_1 ∧ hId = hId_1
-- Lean.Util.CollectLooseBVars
Lean.Expr.CollectLooseBVars.State.mk.injEq : ∀ (visited : Std.HashSet (ℕ × Lean.Expr)) (bvars : Std.HashSet ℕ) (visited_1 : Std.HashSet (ℕ × Lean.Expr))
  (bvars_1 : Std.HashSet ℕ),
  ({ visited := visited, bvars := bvars } = { visited := visited_1, bvars := bvars_1 }) =
    (visited = visited_1 ∧ bvars = bvars_1)
-- Lean.Parser.Tactic
Lean.Parser.Tactic.nestedTactic : Lean.Parser.Parser
-- Init.Data.SInt.Lemmas
ISize.neg_sub : ∀ {a b : ISize}, -(a - b) = b - a
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
ProbabilityTheory.integral_id_multivariateGaussian' : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ},
  ∫ (x : EuclideanSpace ℝ ι), id x ∂ProbabilityTheory.multivariateGaussian μ S = μ
-- Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
/-- Reinterpret an element of a type of completely positive maps as a completely positive linear
map.  -/
CompletelyPositiveMapClass.instCoeToCompletelyPositiveMap : {F : Type u_1} →
  {A₁ : Type u_2} →
    {A₂ : Type u_3} →
      [inst : NonUnitalCStarAlgebra A₁] →
        [inst_1 : NonUnitalCStarAlgebra A₂] →
          [inst_2 : PartialOrder A₁] →
            [inst_3 : PartialOrder A₂] →
              [inst_4 : StarOrderedRing A₁] →
                [inst_5 : StarOrderedRing A₂] →
                  [inst_6 : FunLike F A₁ A₂] →
                    [LinearMapClass F ℂ A₁ A₂] →
                      [CompletelyPositiveMapClass F A₁ A₂] → CoeHead F (CompletelyPositiveMap A₁ A₂)
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.natCast_le_natCast`. -/
ENat.coe_le_coe : ∀ {n m : ℕ}, ↑n ≤ ↑m ↔ n ≤ m
-- Mathlib.Geometry.RingedSpace.SheafedSpace
/-- Forgetting the sheaf condition is a functor from `SheafedSpace C` to `PresheafedSpace C`.  -/
AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor (AlgebraicGeometry.SheafedSpace C) (AlgebraicGeometry.PresheafedSpace C)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.cos_coe : ∀ (x : ℝ), (↑x).cos = Real.cos x
-- Lean.Data.Lsp.Diagnostics
/-- Parametrised by the type of message data. LSP diagnostics use `String`,
whereas in Lean's interactive diagnostics we use the type of widget-enriched text.
See `Lean.Widget.InteractiveDiagnostic`.  -/
Lean.Lsp.DiagnosticWith.message : {α : Type} → Lean.Lsp.DiagnosticWith α → α
-- Mathlib.RingTheory.DedekindDomain.PID
/-- An invertible ideal in a commutative ring with finitely many maximal ideals is principal.

https://math.stackexchange.com/a/95857  -/
Ideal.IsPrincipal.of_finite_maximals_of_isUnit : ∀ {R : Type u_1} [inst : CommRing R], {I | I.IsMaximal}.Finite → ∀ {I : Ideal R}, IsUnit ↑I → Submodule.IsPrincipal I
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_list_singleton : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) {k : α},
  ↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m [k]) = m.insertIfNew k ()
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.instIsAlgebraicEmpty : FirstOrder.Language.empty.IsAlgebraic
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.mem_invtSubmodule_adjoint_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {T : E →L[𝕜] E} {U : Submodule 𝕜 E} [U.HasOrthogonalProjection],
  U ∈ Module.End.invtSubmodule ↑(ContinuousLinearMap.adjoint T) ↔ Uᗮ ∈ Module.End.invtSubmodule ↑T
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.weightedOrder_neg : ∀ {σ : Type u_1} (w : σ → ℕ) {R : Type u_3} [inst : Ring R] (f : MvPowerSeries σ R),
  MvPowerSeries.weightedOrder w (-f) = MvPowerSeries.weightedOrder w f
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.coboundaries₂.val_eq_coe : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G}
  (f : ↥(groupCohomology.coboundaries₂ A)), ↑f = ⇑f
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.comap_smul : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] {F : Type u_3} [inst_2 : Field F]
  [inst_3 : Algebra k K] (σ : Gal(K/k)) (w : NumberField.InfinitePlace K) {f : F →+* K},
  (σ • w).comap f = w.comap ((↑σ.symm).comp f)
-- Init.Data.UInt.Bitwise
UInt8.ne_not_self : ∀ {a : UInt8}, a ≠ ~~~a
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.baseChange_Ψ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (W : WeierstrassCurve R) [inst_2 : Algebra R S]
  {A : Type u} [inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] {B : Type v}
  [inst_7 : CommRing B] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (n : ℤ),
  (W.baseChange B).Ψ n = Polynomial.map (Polynomial.mapRingHom ↑f) ((W.baseChange A).Ψ n)
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.ext_iff : ∀ {S : Type u_1} [inst : Semiring S] [inst_1 : PartialOrder S] {X : Type u_2} [inst_2 : Fintype X]
  {s t : ↑(stdSimplex S X)}, s = t ↔ ⇑s = ⇑t
-- Mathlib.Order.Antisymmetrization
/-- **Alias** of `not_antisymmRel_of_lt`. -/
LT.lt.not_antisymmRel : ∀ {α : Type u_1} {a b : α} [inst : Preorder α], a < b → ¬AntisymmRel (fun x1 x2 => x1 ≤ x2) a b
-- Mathlib.Data.FinEnum
FinEnum.PSigma.finEnum : {α : Type u} → {β : α → Type v} → [FinEnum α] → [(a : α) → FinEnum (β a)] → FinEnum ((a : α) ×' β a)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.mk_eq_mk : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y : R} {t s : ↥(ValuativeRel.posSubmonoid R)},
  ValuativeRel.ValueGroupWithZero.mk x t = ValuativeRel.ValueGroupWithZero.mk y s ↔ x * ↑s ≤ᵥ y * ↑t ∧ y * ↑t ≤ᵥ x * ↑s
-- Mathlib.RingTheory.Jacobson.Ring
/-- If `R` is a Jacobson ring, then maximal ideals in the localization at `y`
correspond to maximal ideals in the original ring `R` that don't contain `y`.
This lemma gives the correspondence in the particular case of an ideal and its map.
See `le_relIso_of_maximal` for the more general statement, and the reverse of this implication  -/
IsLocalization.isMaximal_of_isMaximal_disjoint : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (y : R) [inst_2 : Algebra R S]
  [IsLocalization.Away y S] [IsJacobsonRing R] (I : Ideal R),
  I.IsMaximal → y ∉ I → (Ideal.map (algebraMap R S) I).IsMaximal
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isBigOTVS_prodMk_left : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] [inst_7 : AddCommGroup G] [inst_8 : TopologicalSpace G]
  [inst_9 : Module 𝕜 G] {l : Filter α} {f : α → E} {g : α → F} [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 F] {k : α → G},
  (fun x => (f x, g x)) =O[𝕜; l] k ↔ f =O[𝕜; l] k ∧ g =O[𝕜; l] k
-- Aesop.Util.UnorderedArraySet
/-- O(n)  -/
Aesop.UnorderedArraySet.foldM : {α : Type u_1} →
  [inst : BEq α] →
    {m : Type u_2 → Type u_3} → {σ : Type u_2} → [Monad m] → (σ → α → m σ) → σ → Aesop.UnorderedArraySet α → m σ
-- Init.Data.BitVec.Bitblast
/-- carry i x y c returns true if the `i` carry bit is true when computing `x + y + c`.  -/
BitVec.carry : {w : ℕ} → ℕ → BitVec w → BitVec w → Bool → Bool
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
ContDiffOn.ccos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {s : Set E} {n : WithTop ℕ∞},
  ContDiffOn ℂ n f s → ContDiffOn ℂ n (fun x => Complex.cos (f x)) s
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.norm_zero : ∀ (A : Type u_1) {E : Type u_2} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ E] [inst_4 : SMul A E] [inst_5 : Norm E] [CStarModule A E], ‖0‖ = 0
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.inf_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Min β] (f g : MeasureTheory.SimpleFunc α β)
  (a : α), (f ⊓ g) a = f a ⊓ g a
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_list_map_count : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] (l : List ι) (f : ι → M),
  (List.map f l).sum = ∑ m ∈ l.toFinset, List.count m l • f m
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodeSubtype.match_3.eq_1 : ∀ (n : ℕ) (P : Fin (n + 1) → Prop) (inst : DecidablePred P)
  (motive : (k : ℕ) → (k < Fin.countP fun x => decide (P x)) → Sort u_1) (hk : 0 < Fin.countP fun x => decide (P x))
  (h_1 : (hk : 0 < Fin.countP fun x => decide (P x)) → motive 0 hk)
  (h_2 : (k : ℕ) → (hk : k + 1 < Fin.countP fun x => decide (P x)) → motive k.succ hk),
  (match 0, hk with
    | 0, hk => h_1 hk
    | k.succ, hk => h_2 k hk) =
    h_1 hk
-- Mathlib.Topology.Order.NhdsSet
Iic_mem_nhdsSet_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c : α},
  b ≤ c → Set.Iic c ∈ nhdsSet (Set.Ico a b)
-- Mathlib.RingTheory.OrderOfVanishing.Basic
Ring.ord_ne_top : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] [Ring.KrullDimLE 1 R] {a : R},
  a ∈ nonZeroDivisors R → Ring.ord R a ≠ ⊤
-- Aesop.RuleTac.RuleTerm
Aesop.ElabRuleTerm.scope : Aesop.ElabRuleTerm → Aesop.ScopeName
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.mul_def : ∀ {X : Type u_1} [inst : TopologicalSpace X] (f g : X ≃ₜ X), f * g = g.trans f
-- Mathlib.Algebra.GCDMonoid.Basic
associated_gcd_right_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {x y : α}, Associated y (gcd x y) ↔ y ∣ x
-- Mathlib.Geometry.Euclidean.Angle.Incenter
/-- A point lying on two external angle bisectors is the excenter opposite the third vertex.  -/
Affine.Triangle.eq_excenter_singleton_of_oangle_eq_add_pi_of_oangle_eq_add_pi : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {t : Affine.Triangle ℝ P} {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        ∀ {p : P},
          EuclideanGeometry.oangle (t.points i₂) (t.points i₁) p =
              EuclideanGeometry.oangle p (t.points i₁) (t.points i₃) + ↑Real.pi →
            EuclideanGeometry.oangle (t.points i₃) (t.points i₂) p =
                EuclideanGeometry.oangle p (t.points i₂) (t.points i₁) + ↑Real.pi →
              p = Affine.Simplex.excenter t {i₃}
-- Mathlib.Order.Preorder.Chain
Flag.mk_coe : ∀ {α : Type u_1} [inst : LE α] (s : Flag α), { carrier := ↑s, Chain' := ⋯, max_chain' := ⋯ } = s
-- Mathlib.CategoryTheory.ComposableArrows.Two
CategoryTheory.ComposableArrows.twoδ₂Toδ₁_app_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i j k : C} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg), (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h).app 1 = g
-- Mathlib.Data.List.Infix
List.tails_cons : ∀ {α : Type u_1} (a : α) (l : List α), (a :: l).tails = (a :: l) :: l.tails
-- Mathlib.Algebra.Order.UpperLower
IsLowerSet.smul : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α] {s : Set α} {a : α},
  IsLowerSet s → IsLowerSet (a • s)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_alter!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      k ∈ Std.DTreeMap.Internal.Impl.alter! k f t ↔ (f (t.get? k)).isSome = true
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
/-- The left-inverse of `ι`.

As an implementation detail, we implement this using `TrivSqZeroExt` which has a suitable
algebra structure.  -/
TensorAlgebra.ιInv : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Type u_2} → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → TensorAlgebra R M →ₗ[R] M
-- Mathlib.Algebra.Lie.Abelian
TrivialLieModule.instIsTrivial : ∀ (R : Type u_1) (L : Type u_2) (M : Type u_3) [inst : LieRing L] [inst_1 : AddCommGroup M],
  LieModule.IsTrivial L (TrivialLieModule R L M)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_ofList_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    ∀ {v : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l → Std.DHashMap.Raw.Const.get? (Std.DHashMap.Raw.Const.ofList l) k' = some v
-- Mathlib.Algebra.Lie.Ideal
LieHom.idealRange_eq_top_of_surjective : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L'), Function.Surjective ⇑f → f.idealRange = ⊤
-- Init.Omega.Constraint
/-- The conjunction of two constraints.  -/
Lean.Omega.Constraint.combine : Lean.Omega.Constraint → Lean.Omega.Constraint → Lean.Omega.Constraint
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves_hom_fac_assoc : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesRightKanExtension F L] [inst_5 : L.HasRightKanExtension F]
  {Z : CategoryTheory.Functor A D} (h : F.comp G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft (G.rightKanExtensionCompIsoOfPreserves F L).hom)
      (CategoryTheory.CategoryStruct.comp (L.rightKanExtensionCounit (F.comp G)) h) =
    CategoryTheory.CategoryStruct.comp (L.associator (L.rightKanExtension F) G).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (L.rightKanExtensionCounit F) G) h)
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.coe_toLocalizationMap : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S], ⇑(IsLocalization.toLocalizationMap M S) = ⇑(algebraMap R S)
-- Init.Data.Nat.Div.Basic
Nat.mul_mod_left : ∀ (m n : ℕ), m * n % n = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.isIso_of_nonDegenerate : ∀ (X : SSet) {n : ℕ} (x : ↑(X.nonDegenerate n)) {m : SimplexCategory} (f : { len := n } ⟶ m) [CategoryTheory.Epi f]
  (y : X.obj (Opposite.op m)), (CategoryTheory.ConcreteCategory.hom (X.map f.op)) y = ↑x → CategoryTheory.IsIso f
-- Mathlib.RingTheory.PowerSeries.PiTopology
/-- Separation of the topology on `PowerSeries`  -/
PowerSeries.WithPiTopology.instT0Space : ∀ (R : Type u_1) [inst : TopologicalSpace R] [T0Space R], T0Space (PowerSeries R)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonLocationLink.toJson : Lean.Lsp.LocationLink → Lean.Json
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.FunDecl.fvarId : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.FunDecl pu → Lean.FVarId
-- Lean.Elab.Command
Lean.Elab.Command.Linter.mk : (Lean.Syntax → Lean.Elab.Command.CommandElabM Unit) →
  autoParam Lean.Name Lean.Elab.Command.Linter.name._autoParam → Lean.Linter
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.nat_sub_iff : ∀ {p x : ℝ} {n : ℕ}, LiouvilleWith p (↑n - x) ↔ LiouvilleWith p x
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.mem_inverse_graph : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {f : E →ₗ.[R] F},
  f.toFun.ker = ⊥ → ∀ (x : ↥f.domain), (↑f x, ↑x) ∈ f.inverse.graph
-- Mathlib.Topology.Order.WithTop
/-- Homeomorphism between the non-top elements of `WithTop ι` and `ι`.  -/
WithTop.neTopHomeomorph : (ι : Type u_1) → [inst : LinearOrder ι] → [inst_1 : TopologicalSpace ι] → [inst_2 : OrderTopology ι] → ↑{a | a ≠ ⊤} ≃ₜ ι
-- Mathlib.Algebra.BigOperators.Group.Finset.Powerset
/-- A sum over all subsets of `s ∪ {x}` is obtained by summing the sum over all
subsets of `s`, and over all subsets of `s` to which one adds `x`.  -/
Finset.sum_powerset_insert : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {a : α} [inst : AddCommMonoid β] [inst_1 : DecidableEq α],
  a ∉ s →
    ∀ (f : Finset α → β), ∑ t ∈ (insert a s).powerset, f t = ∑ t ∈ s.powerset, f t + ∑ t ∈ s.powerset, f (insert a t)