mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Lemmas.Splits
/-- You might want to invoke `Pos.Splits.exists_eq_singleton_append_of_ne_startPos` to be able to apply this.  -/
String.Pos.Splits.prev : ∀ {t₁ : String} {c : Char} {t₂ s : String} {p : s.Pos} (h : p.Splits (t₁ ++ String.singleton c) t₂),
  (p.prev ⋯).Splits t₁ (String.singleton c ++ t₂)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.add_isBigO : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {f₁ f₂ : α → E'}, f₁ =o[l] g → f₂ =O[l] g → (fun x => f₁ x + f₂ x) =O[l] g
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.swap_prod : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ]
  {η : ProbabilityTheory.Kernel α γ} [ProbabilityTheory.IsSFiniteKernel η],
  (ProbabilityTheory.Kernel.swap β γ).comp (κ.prod η) = η.prod κ
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.toPoly'.eq_1 : ∀ (e : Lean.Grind.Linarith.Expr), e.toPoly' = Lean.Grind.Linarith.Expr.toPoly'.go 1 e Lean.Grind.Linarith.Poly.nil
-- Mathlib.SetTheory.Ordinal.Univ
Cardinal.IsStrongLimit.univ : Cardinal.univ.{u, v}.IsStrongLimit
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.op_tensor_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : C}
  (f : W ⟶ X) (g : Y ⟶ Z),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f.op g.op = (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).op
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.SameKeys.brecOn : ∀ {α : Type u} {β : α → Type v} {β' : α → Type u_1}
  {motive : (a : Std.DTreeMap.Internal.Impl α β) → (a_1 : Std.DTreeMap.Internal.Impl α β') → a.SameKeys a_1 → Prop}
  {a : Std.DTreeMap.Internal.Impl α β} {a_1 : Std.DTreeMap.Internal.Impl α β'} (t : a.SameKeys a_1),
  (∀ (a : Std.DTreeMap.Internal.Impl α β) (a_2 : Std.DTreeMap.Internal.Impl α β') (t : a.SameKeys a_2),
      Std.DTreeMap.Internal.Impl.SameKeys.below t → motive a a_2 t) →
    motive a a_1 t
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.brecOn_1.eq : ∀ {pu : Lean.Compiler.LCNF.Purity} {motive_1 : Lean.Compiler.LCNF.Alt pu → Sort u}
  {motive_2 : Lean.Compiler.LCNF.FunDecl pu → Sort u} {motive_3 : Lean.Compiler.LCNF.Cases pu → Sort u}
  {motive_4 : Lean.Compiler.LCNF.Code pu → Sort u} {motive_5 : Array (Lean.Compiler.LCNF.Alt pu) → Sort u}
  {motive_6 : List (Lean.Compiler.LCNF.Alt pu) → Sort u} (t : Array (Lean.Compiler.LCNF.Alt pu))
  (F_1 : (t : Lean.Compiler.LCNF.Alt pu) → t.below → motive_1 t)
  (F_2 : (t : Lean.Compiler.LCNF.FunDecl pu) → t.below → motive_2 t)
  (F_3 : (t : Lean.Compiler.LCNF.Cases pu) → t.below → motive_3 t)
  (F_4 : (t : Lean.Compiler.LCNF.Code pu) → t.below → motive_4 t)
  (F_5 : (t : Array (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_1 t → motive_5 t)
  (F_6 : (t : List (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_2 t → motive_6 t),
  Lean.Compiler.LCNF.Alt.brecOn_1 t F_1 F_2 F_3 F_4 F_5 F_6 =
    F_5 t (Lean.Compiler.LCNF.Alt.brecOn_1.go t F_1 F_2 F_3 F_4 F_5 F_6).2
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- The leading term of the zero polynomial is zero  -/
MonomialOrder.leadingTerm_zero : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R], m.leadingTerm 0 = 0
-- Init.Data.BitVec.Lemmas
BitVec.append_left_inj : ∀ {w w' : ℕ} {s₁ s₂ : BitVec w} (t : BitVec w'), s₁ ++ t = s₂ ++ t ↔ s₁ = s₂
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.singleton_isCircuit : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsCircuit {e} ↔ M.IsLoop e
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.match_4.congr_eq_4 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_3 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)) (x_1 : Lean.Grind.CommRing.Var),
  x = Lean.Grind.CommRing.Expr.var x_1 →
    (match x with
      | Lean.Grind.CommRing.Expr.num k => h_1 k
      | Lean.Grind.CommRing.Expr.intCast k => h_2 k
      | Lean.Grind.CommRing.Expr.natCast k => h_3 k
      | Lean.Grind.CommRing.Expr.var x => h_4 x
      | a.add b => h_5 a b
      | a.mul b => h_6 a b
      | a.neg => h_7 a
      | a.sub b => h_8 a b
      | a.pow k => h_9 a k) ≍
      h_4 x_1
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.neg_cons : ∀ {α : Type u_1} {n : ℕ} [inst : Neg α] (x : α) (v : Fin n → α), -Matrix.vecCons x v = Matrix.vecCons (-x) (-v)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.forM.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {m : Type w → Type w₂} [inst : Monad m]
  [inst_1 : LawfulMonad m] [inst_2 : Std.TransCmp cmp] (f f_1 : (a : α) → β a → m PUnit.{w + 1}),
  f = f_1 → ∀ (t t_1 : Std.ExtDTreeMap α β cmp), t = t_1 → Std.ExtDTreeMap.forM f t = Std.ExtDTreeMap.forM f_1 t_1
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_natAdd_Icc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.image (Fin.natAdd m) (Finset.Icc i j) = Finset.Icc (Fin.natAdd m i) (Fin.natAdd m j)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instEmptyCollection : EmptyCollection ZFSet.{u_1}
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
/-- Grade reversion, inverting the multiplication order of basis vectors.
Also called *transpose* in some literature.  -/
CliffordAlgebra.reverse : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → {Q : QuadraticForm R M} → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q
-- Mathlib.Algebra.Algebra.Operations
Submodule.one_mul : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (M : Submodule R A), 1 * M = M
-- Lean.Meta.Constructions.BRecOn
/-- If `minorType` is the type of a minor premies of a recursor, such as
```
  (cons : (head : α) → (tail : List α) → (tail_hs : motive tail) → motive (head :: tail))
```
of `List.rec`, constructs the corresponding argument to `List.rec` in the construction
of `.brecOn` definition; in this case
```
fun head tail tail_ih =>
  ⟨F_1 (head :: tail) ⟨tail_ih, PUnit.unit⟩, ⟨tail_ih, PUnit.unit⟩⟩
```
of type
```
(head : α) → (tail : List α) →
  PProd (motive tail) (List.below tail) →
  PProd (motive (head :: tail)) (PProd (PProd (motive tail) (List.below tail)) PUnit)
```
 -/
_private.Lean.Meta.Constructions.BRecOn.0.Lean.buildBRecOnMinorPremise : Lean.Level → Array Lean.Expr → Array Lean.Expr → Array Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Lean.CoreM
Lean.MonadRuntimeException : (Type → Type) → Type 1
-- Mathlib.LinearAlgebra.Basis.Defs
/-- **Alias** of the reverse direction of `Module.Basis.ext_elem_iff`.

---

Two elements are equal iff their coordinates are equal.  -/
Module.Basis.ext_elem : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) {x y : M}, (∀ (i : ι), (b.repr x) i = (b.repr y) i) → x = y
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalGroup.IsSES.pushforward.eq_1 : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →* B} {ψ : B →* C}
  (H : TopologicalGroup.IsSES φ ψ) [inst_6 : IsTopologicalGroup A] [inst_7 : IsTopologicalGroup B]
  [inst_8 : NormedAddCommGroup E] [inst_9 : MeasurableSpace A] [inst_10 : BorelSpace A] (μA : MeasureTheory.Measure A)
  [hμA : μA.IsHaarMeasure] [inst_11 : NormedSpace ℝ E] [inst_12 : IsTopologicalGroup C]
  [inst_13 : LocallyCompactSpace B],
  H.pushforward μA =
    {
      toFun := fun f =>
        { toFun := fun c => ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ) c)) a ∂μA, continuous_toFun := ⋯,
          hasCompactSupport' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instPow.eq_1 : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : Monoid R]
  [inst_3 : BoundedMul R] [inst_4 : ContinuousMul R],
  BoundedContinuousFunction.instPow =
    { pow := fun f n => { toFun := fun x => f x ^ n, continuous_toFun := ⋯, map_bounded' := ⋯ } }
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenModifier.definition.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenModifier.definition = 1
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.coe_bracket_of_module : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (L' : LieRinehartSubalgebra A L) {M : Type u_3} [inst_3 : AddCommGroup M] [inst_4 : LieRingModule L M] (x : ↥L')
  (m : M), ⁅x, m⁆ = ⁅↑x, m⁆
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.IsClosedImmersion.instSubschemeι : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData), AlgebraicGeometry.IsClosedImmersion I.subschemeι
-- Mathlib.CategoryTheory.Conj
CategoryTheory.Iso.conjAut_mul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f g : CategoryTheory.Aut X),
  α.conjAut (f * g) = α.conjAut f * α.conjAut g
-- Init.Data.Vector.MapIdx
_private.Init.Data.Vector.MapIdx.0.Vector.mapFinIdxM.map.match_1.eq_1 : ∀ {n : ℕ} (j : ℕ) (motive : (i : ℕ) → i + j = n → Sort u_1) (inv : 0 + j = n) (h_1 : (inv : 0 + j = n) → motive 0 inv)
  (h_2 : (i : ℕ) → (inv : i + 1 + j = n) → motive i.succ inv),
  (match 0, inv with
    | 0, inv => h_1 inv
    | i.succ, inv => h_2 i inv) =
    h_1 inv
-- Mathlib.GroupTheory.Coxeter.Length
_private.Mathlib.GroupTheory.Coxeter.Length.0.CoxeterSystem.exists_word_with_prod : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W),
  ∃ n ω, n = ω.length ∧ cs.wordProd ω = w
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_C : ∀ {R : Type u_1} {n : ℕ} [inst : Semiring R] {a : R}, (SkewPolynomial.C a).coeff n = if n = 0 then a else 0
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
/-- The property of objects in the functor category `J ⥤ C`
which preserves the limit of a functor `F : K ⥤ J`.  -/
CategoryTheory.ObjectProperty.preservesLimit : {J : Type u_1} →
  {C : Type u_3} →
    {K : Type u_5} →
      [inst : CategoryTheory.Category.{v_1, u_5} K] →
        [inst_1 : CategoryTheory.Category.{v_3, u_1} J] →
          [inst_2 : CategoryTheory.Category.{v_5, u_3} C] →
            CategoryTheory.Functor K J → CategoryTheory.ObjectProperty (CategoryTheory.Functor J C)
-- Mathlib.Algebra.GroupWithZero.Defs
/-- Zero is a right absorbing element for multiplication  -/
CommMonoidWithZero.mul_zero : ∀ {M₀ : Type u_2} [self : CommMonoidWithZero M₀] (a : M₀), a * 0 = 0
-- Init.Data.String.Lemmas.Modify
/-- You might want to invoke `Pos.Splits.exists_eq_singleton_append` to be able to apply this.  -/
String.Pos.Splits.pastModify : ∀ {f : Char → Char} {s : String} {p : s.Pos} {t₁ t₂ : String} {c : Char} (h : p.Splits t₁ (String.singleton c ++ t₂)),
  (p.pastModify f ⋯).Splits (t₁ ++ String.singleton (f (p.get ⋯))) t₂
-- Mathlib.CategoryTheory.Opposites
/-- The opposite `CategoryStruct`.  -/
CategoryTheory.CategoryStruct.opposite : {C : Type u₁} → [CategoryTheory.CategoryStruct.{v₁, u₁} C] → CategoryTheory.CategoryStruct.{v₁, u₁} Cᵒᵖ
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.single_zero : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → Zero (G i)] [inst_3 : ∀ (i : ι), ZeroMemClass (S i) (G i)] (i : ι),
  RestrictedProduct.single A i 0 = 0
-- Mathlib.Topology.CompactOpen
/-- **Alias** of `ContinuousMap.isClopen_setOfPred_mapsTo`. -/
ContinuousMap.isClopen_setOf_mapsTo : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {K : Set X} {U : Set Y},
  IsCompact K → IsClopen U → IsClopen {f | Set.MapsTo (⇑f) K U}
-- Lean.Meta.Match.Match
/-- Throws an error indicating that the alternative at `ref` contains an unexpected number of patterns.
Remark: we allow `α` to be arbitrary because this error may be thrown before or after elaborating
pattern syntax.
 -/
Lean.Meta.Match.throwIncorrectNumberOfPatternsAt : {α : Type} → [Lean.ToMessageData α] → Lean.Syntax → String → ℕ → ℕ → List α → Lean.MetaM Unit
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
FractionalIdeal.adjoinIntegral.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P] (x x_1 : P) (e_x : x = x_1) (hx : IsIntegral R x),
  FractionalIdeal.adjoinIntegral S x hx = FractionalIdeal.adjoinIntegral S x_1 ⋯
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.norm_charFun_le : ∀ {E : Type u_2} {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [inst : SeminormedAddCommGroup E]
  [inst_1 : InnerProductSpace ℝ E] (t : E), ‖MeasureTheory.charFun μ t‖ ≤ μ.real Set.univ
-- Mathlib.Order.WithBot
WithBot.unbotA_le_iff : ∀ {α : Type u_1} {a : α} [inst : LE α] {x : WithBot α} [inst_1 : Nonempty α], x ≠ ⊥ → (x.unbotA ≤ a ↔ x ≤ ↑a)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
/-- Copy of a non-unital subsemiring with a new `carrier` equal to the old one. Useful to fix
definitional equalities.  -/
NonUnitalSubsemiring.copy : {R : Type u} →
  [inst : NonUnitalNonAssocSemiring R] → (S : NonUnitalSubsemiring R) → (s : Set R) → s = ↑S → NonUnitalSubsemiring R
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
mul_inv_lt_one_iff : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulRightStrictMono α] {a b : α}, b * a⁻¹ < 1 ↔ b < a
-- Mathlib.Analysis.ODE.PicardLindelof
/-- The domain is `Icc tmin tmax`.  -/
ODE.FunSpace.toFun : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    {tmin tmax : ℝ} →
      {t₀ : ↑(Set.Icc tmin tmax)} → {x₀ : E} → {r L : NNReal} → ODE.FunSpace t₀ x₀ r L → ↑(Set.Icc tmin tmax) → E
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderiv_fun_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {x : E},
  DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 g x → fderiv 𝕜 (fun y => f y - g y) x = fderiv 𝕜 f x - fderiv 𝕜 g x
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.add_mul_left_right_iff : ∀ {R : Type u_1} [inst : CommRing R] {x y z : R}, IsRelPrime x (y + x * z) ↔ IsRelPrime x y
-- Lean.Log
/-- Log a named error message using the given message data. The position is provided by `getRef`.

Note: Use the macro `logNamedError`, which validates error names, instead of calling this function
directly.
 -/
Lean.logNamedError : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadLog m] → [Lean.AddMessageContext m] → [Lean.MonadOptions m] → Lean.Name → Lean.MessageData → m Unit
-- Mathlib.Algebra.DirectSum.Module
/-- Note that this is not generally true for `[Semiring R]`; see
`iSupIndep.dfinsupp_lsum_injective` for details.  -/
DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top : ∀ {R : Type u} [inst : Ring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] {A : ι → Submodule R M}, iSupIndep A → iSup A = ⊤ → DirectSum.IsInternal A
-- Init.Data.List.Lemmas
List.some_getElem_eq_getElem?_iff : ∀ {α : Type u_1} {xs : List α} {i : ℕ} (h : i < xs.length), some xs[i] = xs[i]? ↔ True
-- Init.Notation
/-- Precedence used for terms not supposed to be used as arguments (`let`, `have`, ...).  -/
precLead : Lean.ParserDescr
-- Mathlib.CategoryTheory.Enriched.EnrichedCat
CategoryTheory.EnrichedCat.associator_inv_out_app : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₁} [inst_3 : CategoryTheory.EnrichedCategory V D]
  {E : Type u₂} [inst_4 : CategoryTheory.EnrichedCategory V E] {E' : Type u₃}
  [inst_5 : CategoryTheory.EnrichedCategory V E'] (F : CategoryTheory.EnrichedFunctor V C D)
  (G : CategoryTheory.EnrichedFunctor V D E) (H : CategoryTheory.EnrichedFunctor V E E')
  (X : CategoryTheory.ForgetEnrichment V C),
  (CategoryTheory.EnrichedCat.associator F G H).inv.out.app X =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.ForgetEnrichment.of V (H.obj (G.obj (F.obj (CategoryTheory.ForgetEnrichment.to V X)))))
-- Mathlib.Order.Fin.Basic
Fin.cast_top : ∀ {m n : ℕ} [inst : NeZero m] [inst_1 : NeZero n] (h : m = n), Fin.cast h ⊤ = ⊤
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.instToStringBVBit : ToString Std.Tactic.BVDecide.BVBit
-- Mathlib.Order.Category.CompleteLat
CompleteLat.instInhabited : Inhabited CompleteLat
-- Mathlib.Data.ZMod.Basic
/-- **Alias** of the reverse direction of `ZMod.intCast_eq_one_iff_odd`. -/
Odd.intCast_zmod_two : ∀ {n : ℤ}, Odd n → ↑n = 1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_insert_le : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k : α} {v : β k}, (↑(m.insert k v)).size ≤ (↑m).size + 1
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.reflectRoot.eq_1 : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L),
  LieAlgebra.IsKilling.reflectRoot α β =
    { toFun := ⇑β - β (LieAlgebra.IsKilling.coroot α) • ⇑α, genWeightSpace_ne_bot' := ⋯ }
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.nonUnitalRing : {I : Type u_5} → {B : I → Type u_6} → [inst : (i : I) → NonUnitalNormedRing (B i)] → NonUnitalRing ↥(lp B ⊤)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
isUnit_cfc_iff : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [inst_9 : ContinuousFunctionalCalculus R A p] (f : R → R) (a : A),
  autoParam (ContinuousOn f (spectrum R a)) isUnit_cfc_iff._auto_1 →
    autoParam (p a) isUnit_cfc_iff._auto_3 → (IsUnit (cfc f a) ↔ ∀ x ∈ spectrum R a, f x ≠ 0)
-- Lean.Parser.Term
Lean.Parser.Term.letIdLhs : Lean.Parser.Parser
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.mulLeft_symm : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [inst_2 : MulLeftMono α] (a : α),
  (OrderIso.mulLeft a).symm = OrderIso.mulLeft a⁻¹
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.snd_apply_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] (x : N),
  Monoid.Coprod.snd (Monoid.Coprod.inr x) = x
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- If the inverse of a Freiman homomorphism is itself a Freiman homomorphism, then it is a Freiman
isomorphism.
 -/
IsAddFreimanHom.to_isAddFreimanIso : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A : Set α} {B : Set β} {f : α → β}
  {n : ℕ} {g : β → α}, Set.InvOn g f A B → IsAddFreimanHom n A B f → IsAddFreimanHom n B A g → IsAddFreimanIso n A B f
-- Mathlib.Topology.Semicontinuity.Defs
upperSemicontinuous_iff_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β},
  UpperSemicontinuous f ↔ ∀ (x : α) (y : β), (∃ᶠ (x' : α) in nhds x, f x' ≥ y) → f x ≥ y
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.instNonemptyRetractClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.Nonempty],
  P.retractClosure.Nonempty
-- Lean.HeadIndex
Lean.HeadIndex.fvar.injEq : ∀ (fvarId fvarId_1 : Lean.FVarId), (Lean.HeadIndex.fvar fvarId = Lean.HeadIndex.fvar fvarId_1) = (fvarId = fvarId_1)
-- Init.Data.Int.Lemmas
Int.mul_assoc : ∀ (a b c : ℤ), a * b * c = a * (b * c)
-- Mathlib.Data.TypeVec
/-- decompose a vector into its prefix appended with its last element  -/
TypeVec.toAppend1DropLast : {n : ℕ} → {α : TypeVec.{u_1} (n + 1)} → α.Arrow (α.drop ::: α.last)
-- Mathlib.Data.ENat.Basic
ENat.add_right_injective_of_ne_top : ∀ {n : ℕ∞}, n ≠ ⊤ → Function.Injective fun x => n + x
-- Mathlib.Computability.Reduce
manyOneReducible_toNat_toNat : ∀ {α : Type u} [inst : Primcodable α] [inst_1 : Inhabited α] {β : Type v} [inst_2 : Primcodable β]
  [inst_3 : Inhabited β] {p : Set α} {q : Set β}, toNat p ≤₀ toNat q ↔ p ≤₀ q
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct
SSet.prodStdSimplex.innerAnodyneExtensions_unionProd_ι : ∀ {m : ℕ} (k : Fin (m + 2)),
  0 < k →
    k < Fin.last (m + 1) → ∀ (n : ℕ), SSet.innerAnodyneExtensions ((SSet.horn (m + 1) k).unionProd (SSet.boundary n)).ι
-- Init.Data.String.Lemmas.Intercalate
String.Slice.intercalate_eq : ∀ {s : String.Slice} {l : List String.Slice}, s.intercalate l = s.copy.intercalate (List.map String.Slice.copy l)
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.toPlus_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D}
  (η : P ⟶ Q),
  CategoryTheory.CategoryStruct.comp η (J.toPlus Q) = CategoryTheory.CategoryStruct.comp (J.toPlus P) (J.plusMap η)
-- Mathlib.RepresentationTheory.Coinvariants
Representation.Coinvariants.mem_ker_of_eq : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] {ρ : Representation k G V} (g : G) (x a : V),
  (ρ g) x - x = a → a ∈ Representation.Coinvariants.ker ρ
-- Mathlib.Data.Finset.Card
Finset.card_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), (s ∩ t).card = s.card + t.card - (s ∪ t).card
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionTriggerKind.automatic.sizeOf_spec : sizeOf Lean.Lsp.CodeActionTriggerKind.automatic = 1
-- Mathlib.Order.Compare
cmp_self_eq_eq : ∀ {α : Type u_1} [inst : LinearOrder α] (x : α), cmp x x = Ordering.eq
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_sub_intCast : ∀ {x : NNReal}, x ≠ 0 → ∀ (y : ℝ) (n : ℕ), x ^ (y - ↑n) = x ^ y / x ^ n
-- Lean.Meta.MkIffOfInductiveProp
/-- `select m n` runs `right` `m` times; if `m < n`, then it also runs `left` once.
Fails if `n < m`.  -/
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.select : ℕ → ℕ → Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_inverse : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (n : ℤ),
  (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).inverse = (CategoryTheory.shiftFunctor C n).op
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.isNonneg_def : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {I₁ I₂ : R →+* R} [inst_3 : LE R] {B : M →ₛₗ[I₁] M →ₛₗ[I₂] R}, B.IsNonneg ↔ ∀ (x : M), 0 ≤ (B x) x
-- Lean.Data.Lsp.Basic
Lean.Lsp.ResolveSupport.mk.injEq : ∀ (properties properties_1 : Array String),
  ({ properties := properties } = { properties := properties_1 }) = (properties = properties_1)