mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHint.mk.injEq : ∀ (toInlayHintInfo : Lean.Elab.InlayHintInfo) (lctx : Lean.LocalContext)
  (deferredResolution : Lean.Elab.InlayHintInfo → Lean.MetaM Lean.Elab.InlayHintInfo)
  (toInlayHintInfo_1 : Lean.Elab.InlayHintInfo) (lctx_1 : Lean.LocalContext)
  (deferredResolution_1 : Lean.Elab.InlayHintInfo → Lean.MetaM Lean.Elab.InlayHintInfo),
  ({ toInlayHintInfo := toInlayHintInfo, lctx := lctx, deferredResolution := deferredResolution } =
      { toInlayHintInfo := toInlayHintInfo_1, lctx := lctx_1, deferredResolution := deferredResolution_1 }) =
    (toInlayHintInfo = toInlayHintInfo_1 ∧ lctx = lctx_1 ∧ deferredResolution = deferredResolution_1)
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.instCanLiftSetCoeAndForallForallForallMemForallHAddForallForallForallForallHMulForallCoeRingHomAlgebraMapForallForallStar : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A],
  CanLift (Set A) (StarSubalgebra R A) SetLike.coe fun s =>
    (∀ {x y : A}, x ∈ s → y ∈ s → x + y ∈ s) ∧
      (∀ {x y : A}, x ∈ s → y ∈ s → x * y ∈ s) ∧ (∀ (r : R), (algebraMap R A) r ∈ s) ∧ ∀ {x : A}, x ∈ s → star x ∈ s
-- Mathlib.Topology.Constructions
IsOpenMap.subtype_map : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsOpenMap f → ∀ {s : Set X} {t : Set Y}, IsOpen s → ∀ (hst : ∀ x ∈ s, f x ∈ t), IsOpenMap (Subtype.map f hst)
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleIntegral_def_Icc : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) (c : ℂ) (R : ℝ),
  ∮ (z : ℂ) in C(c, R), f z = ∫ (θ : ℝ) in Set.Icc 0 (2 * Real.pi), deriv (circleMap c R) θ • f (circleMap c R θ)
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.fromCols_apply_inr : ∀ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (i : m)
  (j : n₂), A₁.fromCols A₂ i (Sum.inr j) = A₂ i j
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.Pos.Raw.utf8GetAux.match_1.eq_1 : ∀ (motive : List Char → String.Pos.Raw → String.Pos.Raw → Sort u_1) (x x_1 : String.Pos.Raw)
  (h_1 : (x x_2 : String.Pos.Raw) → motive [] x x_2)
  (h_2 : (c : Char) → (cs : List Char) → (i p : String.Pos.Raw) → motive (c :: cs) i p),
  (match [], x, x_1 with
    | [], x, x_2 => h_1 x x_2
    | c :: cs, i, p => h_2 c cs i p) =
    h_1 x x_1
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasMulAntidiagonal.mk : {A : Type u_1} →
  [inst : Monoid A] →
    (mulAntidiagonal : A → Finset (A × A)) →
      (∀ {n : A} {a : A × A}, a ∈ mulAntidiagonal n ↔ a.1 * a.2 = n) → Finset.HasMulAntidiagonal A
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.constructor : Lean.Lsp.CompletionItemKind
-- Init.Data.List.Lemmas
List.head!_eq_getElem! : ∀ {α : Type u_1} [inst : Inhabited α] {l : List α}, l.head! = l[0]!
-- Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_hom_hom₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (X : Cᵒᵖ),
  (CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso X).hom.hom₁ = CategoryTheory.CategoryStruct.id X
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.eq_append_of_dropSuffix?_eq_some : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s res : String.Slice},
  s.dropSuffix? pat = some res → ∃ t, String.Slice.Pattern.Model.PatternModel.Matches pat t ∧ s.copy = res.copy ++ t
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.one : CategoryTheory.Limits.WalkingReflexivePair
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.eval_additive : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} (i : ι), (HomologicalComplex.eval V c i).Additive
-- Mathlib.RingTheory.Ideal.Maps
/-- The smallest `S`-submodule that contains all `x ∈ I * y ∈ J`
is also the smallest `R`-submodule that does so.  -/
Ideal.restrictScalars_mul : ∀ {R : Type u_4} {S : Type u_5} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  [inst_3 : IsScalarTower R S S] (I J : Ideal S),
  Submodule.restrictScalars R (I * J) = Submodule.restrictScalars R I * Submodule.restrictScalars R J
-- Mathlib.Data.Sum.Order
OrderIso.sumDualDistrib_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] (b : β),
  (OrderIso.sumDualDistrib α β) (OrderDual.toDual (Sum.inr b)) = Sum.inr (OrderDual.toDual b)
-- Init.Data.List.Find
List.IsInfix.findIdx?_eq_none : ∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool}, l₁ <:+: l₂ → List.findIdx? p l₂ = none → List.findIdx? p l₁ = none
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrpCompIso_inv_app_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {E : Type u₃} [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.CartesianMonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.Monoidal] [inst_7 : G.Monoidal]
  (X : CategoryTheory.AddGrp C),
  (CategoryTheory.Functor.mapAddGrpCompIso.inv.app X).hom.hom = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.X))
-- Init.Core
String.Pos.Raw.mk.inj : ∀ {byteIdx byteIdx_1 : ℕ}, { byteIdx := byteIdx } = { byteIdx := byteIdx_1 } → byteIdx = byteIdx_1
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- An equivalence of groups, from the center of the special linear group to the roots of unity.

See also `center_equiv_rootsOfUnity'`.  -/
Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {R : Type v} →
        [inst_2 : CommRing R] →
          ↥(Subgroup.center (Matrix.SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (max (Fintype.card n) 1) R)
-- Mathlib.CategoryTheory.MorphismProperty.Concrete
/-- Injectivity (in a concrete category) as a `MorphismProperty`  -/
CategoryTheory.MorphismProperty.injective : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type u_2} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [CategoryTheory.ConcreteCategory C FC] → CategoryTheory.MorphismProperty C
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instMonoid : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommMonoid R] →
      [inst_1 : NonUnitalSemiring A] →
        [inst_2 : DistribMulAction R A] → [IsScalarTower R A A] → [SMulCommClass R A A] → Monoid (Unitization R A)
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- The `p`-adic norm is nonnegative.  -/
padicNorm.nonneg : ∀ {p : ℕ} (q : ℚ), 0 ≤ padicNorm p q
-- Mathlib.Algebra.TrivSqZeroExt.Ideal
/-- The kernel of the `AlgHom` `fstHom R R M`  -/
TrivSqZeroExt.kerIdeal : (R : Type u_1) →
  (M : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → [inst_3 : Module Rᵐᵒᵖ M] → [inst_4 : IsCentralScalar R M] → Ideal (TrivSqZeroExt R M)
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.sigma_isBasis_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} {M : (i : ι) → Matroid (α i)} {I X : Set ((i : ι) × α i)},
  (Matroid.sigma M).IsBasis I X ↔ ∀ (i : ι), (M i).IsBasis (Sigma.mk i ⁻¹' I) (Sigma.mk i ⁻¹' X)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isSome_minKey?_of_isSome_minKey?_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).minKey?.isSome = true → t.minKey?.isSome = true
-- Init.Data.Array.Lemmas
Array.append_right_eq_self : ∀ {α : Type u_1} {xs ys : Array α}, xs ++ ys = xs ↔ ys = #[]
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKeyD_le_maxKeyD_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    t.isEmpty = false →
      ∀ {k : α} {v : β} {fallback : α}, (cmp (t.maxKeyD fallback) ((t.insertIfNew k v).maxKeyD fallback)).isLE = true
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.valid : ∀ {l m r : List Char} {s : Substring.Raw}, Substring.Raw.ValidFor l m r s → s.Valid
-- Mathlib.Algebra.Exact.Basic
Function.MulExact.apply_apply_eq_one : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} {f : M → N} {g : N → P} [inst : One P],
  Function.MulExact f g → ∀ (x : M), g (f x) = 1
-- Mathlib.RingTheory.Ideal.Height
Ideal.height_eq_zero_iff_eq_bot : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {I : Ideal R}, I.height = 0 ↔ I = ⊥
-- Lean.Meta.Constructions.CtorIdx
/-- For an inductive type `T` with more than one function builds a function `T.ctorIdx : T → Nat` that
returns the constructor index of the given value.
Does nothing if `T` does not eliminate into `Type` or if `T` is unsafe.
Assumes `T.casesOn` to be defined already.
 -/
Lean.mkCtorIdx : Lean.Name → Lean.MetaM Unit
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.mkIso_hom : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {X Y : Type w} [inst_2 : AddCommGroup X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module k X] [inst_5 : Module k Y] {ρ : Representation k G X}
  {σ : Representation k G Y} (e : ρ.Equiv σ), (Rep.mkIso e).hom = Rep.ofHom ↑e
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.neg : Lean.Meta.Grind.Arith.Linear.DiseqCnstr → Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof
-- Mathlib.Analysis.Distribution.DerivNotation
/-- The second derivative in terms `lineDerivOp` as a linear map from the tensor product.

Mainly used to give an abstract definition of the Laplacian.  -/
LineDeriv.tensorLineDerivTwo : (R : Type u_4) →
  {E : Type u_6} →
    {V₁ : Type u_8} →
      {V₂ : Type u_9} →
        {V₃ : Type u_10} →
          [inst : LineDeriv E V₁ V₂] →
            [inst_1 : LineDeriv E V₂ V₃] →
              [inst_2 : AddCommGroup V₁] →
                [inst_3 : AddCommGroup V₂] →
                  [inst_4 : AddCommGroup V₃] →
                    [inst_5 : CommRing R] →
                      [inst_6 : AddCommGroup E] →
                        [inst_7 : Module R E] →
                          [inst_8 : Module R V₂] →
                            [inst_9 : Module R V₃] →
                              [LineDerivAdd E V₂ V₃] →
                                [LineDerivAdd E V₁ V₂] →
                                  [LineDerivSMul R E V₂ V₃] →
                                    [LineDerivLeftSMul R E V₁ V₂] →
                                      [LineDerivLeftSMul R E V₂ V₃] → V₁ → TensorProduct R E E →ₗ[R] V₃
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.smul_right_of_tower : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_3}
  [inst_3 : CommSemiring S] [inst_4 : Algebra S R] [inst_5 : Module S M] [IsScalarTower S R M]
  {B : LinearMap.BilinForm R M} (r : S) (x y : M), (B x) (r • y) = r • (B x) y
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero' : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] (p : Polynomial R) (s : Finset R),
  (∀ i ∈ s, Polynomial.eval i p = 0) → p.natDegree < s.card → p = 0
-- Mathlib.GroupTheory.Submonoid.Center
AddSubmonoid.centerCongr_symm_apply_coe : ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (e : M ≃+ N)
  (s : ↥(AddSubsemigroup.center N)), ↑((AddSubmonoid.centerCongr e).symm s) = e.symm ↑s
-- Std.Time.Duration
Std.Time.Duration.instHAddOffset_4 : HAdd Std.Time.Duration Std.Time.Second.Offset Std.Time.Duration
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RcoSliceData.treeMap : {α : Type u} →
  {β : Type v} → [inst : Ord α] → Std.DTreeMap.Internal.Const.RcoSliceData α β → Std.DTreeMap.Internal.Impl α fun x => β
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.as_obj_normalizeObj' : ∀ {C : Type u} (X : CategoryTheory.FreeMonoidalCategory C)
  (n : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C),
  (X.normalizeObj'.obj n).as = X.normalizeObj n.as
-- Lean.Elab.DocString
/-- Elaborates the syntax of an inline document element to an actual inline document element.
 -/
Lean.Doc.elabInline : Lean.TSyntax `inline → Lean.Doc.DocM (Lean.Doc.Inline Lean.ElabInline)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_le_size_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, t.size ≤ (t.insert k v).size
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the second of three points is strictly between the other two, the oriented angle at that
point (reversed) is π.  -/
Sbtw.oangle₃₂₁_eq_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)]
  {p₁ p₂ p₃ : P}, Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.oangle p₃ p₂ p₁ = ↑Real.pi
-- Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
CategoryTheory.Limits.SequentialProduct.functorMap_commSq_aux : ∀ {C : Type u_1} {M N : ℕ → C} [inst : CategoryTheory.Category.{v_1, u_1} C] (f : (n : ℕ) → M n ⟶ N n)
  [inst_1 : CategoryTheory.Limits.HasCountableProducts C] {n m k : ℕ} (h : n ≤ m) (hh : ¬k < m),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.ofOpSequence (CategoryTheory.Limits.SequentialProduct.functorMap f)).map
        (CategoryTheory.homOfLE h).op)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.Pi.π (fun m => if x : m < Opposite.unop (Opposite.op n) then M m else N m) k)
        (CategoryTheory.eqToHom ⋯)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun i => if x : i < m then M i else N i) k)
      (CategoryTheory.eqToHom ⋯)
-- Batteries.Data.List.Basic
List.foldrIdx.eq_def : ∀ {α : Type u} {β : Type v} (f : ℕ → α → β → β) (init : β) (x : List α) (x_1 : ℕ),
  List.foldrIdx f init x x_1 =
    match x, x_1 with
    | [], x => init
    | a :: l, s => f s a (List.foldrIdx f init l (s + 1))
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.CondIndepFun.neg_left : ∀ {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {f : Ω → β} {g : Ω → β'}
  {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} [inst_2 : Neg β] [MeasurableNeg β],
  ProbabilityTheory.CondIndepFun m' hm' f g μ → ProbabilityTheory.CondIndepFun m' hm' (-f) g μ
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.embeddingLiftIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (X : C),
  (CategoryTheory.Mat_.embeddingLiftIso F).inv.app X =
    CategoryTheory.Limits.biproduct.lift fun x => CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
/-- Given functors `F₁` and `F₂` in `J ⥤ C`, where `C` is a `V`-enriched ordinary category,
this is the bijection `(F₁ ⟶ F₂) ≃ (𝟙_ (J ⥤ V) ⟶ functorEnrichedHom V F₁ F₂)`.  -/
CategoryTheory.Enriched.FunctorCategory.functorHomEquiv : (V : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} C] →
          {J : Type u₃} →
            [inst_3 : CategoryTheory.Category.{v₃, u₃} J] →
              [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] →
                {F₁ F₂ : CategoryTheory.Functor J C} →
                  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂] →
                    [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] →
                      (F₁ ⟶ F₂) ≃
                        (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor J V) ⟶
                          CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂)
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.isElliptic_conj'_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Preorder R] {m : Matrix (Fin 2) (Fin 2) R} (g : GL (Fin 2) R),
  ((↑g)⁻¹ * m * ↑g).IsElliptic ↔ m.IsElliptic
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.injective_pairingIn : ∀ {ι : 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] [CharZero R] [IsDomain R] [Finite ι]
  {P : RootPairing ι R M N} [P.IsRootSystem] [inst_9 : P.IsCrystallographic] (b : P.Base),
  Function.Injective fun i k => P.pairingIn ℤ i ↑k
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.add_iff_right : ∀ {α : Type u_1} {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : MeasurableSpace α] [inst_2 : AddCommGroup G]
  [MeasurableAdd₂ G] [MeasurableNeg G] {μ : MeasureTheory.Measure α} {f g : α → G},
  AEMeasurable f μ → (AEMeasurable (f + g) μ ↔ AEMeasurable g μ)
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.degree_derivative : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} [IsAddTorsionFree R],
  p.natDegree ≠ 0 → (Polynomial.derivative p).degree = ↑(p.natDegree - 1)
-- Init.Data.Vector.Find
Vector.findSome?_append : ∀ {α : Type u_1} {n₁ n₂ : ℕ} {α_1 : Type u_2} {f : α → Option α_1} {xs : Vector α n₁} {ys : Vector α n₂},
  Vector.findSome? f (xs ++ ys) = (Vector.findSome? f xs).or (Vector.findSome? f ys)
-- Mathlib.Analysis.Convex.Strong
UniformConvexOn.convexOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {φ : ℝ → ℝ} {s : Set E} {f : E → ℝ},
  UniformConvexOn s φ f → 0 ≤ φ → ConvexOn ℝ s f
-- Init.Data.List.Find
List.find?_cons_of_neg : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, ¬p a = true → List.find? p (a :: l) = List.find? p l
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.localAlgHom'_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {P : Type u_3}
  [inst_3 : CommSemiring P] (I : Ideal R) [hI : I.IsPrime] [inst_4 : Algebra R P] (J : Ideal S) (K : Ideal P)
  [inst_5 : J.IsPrime] [inst_6 : K.IsPrime] [inst_7 : J.LiesOver I]
  [inst_8 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)]
  [inst_9 : Localization.AtPrime.IsLiesOverAlgebra I J] [inst_10 : K.LiesOver I]
  [inst_11 : Algebra (Localization.AtPrime I) (Localization.AtPrime K)]
  [inst_12 : Localization.AtPrime.IsLiesOverAlgebra I K] (f : S →ₐ[R] P) (h : J = Ideal.comap f K)
  (a : Localization.AtPrime J),
  (Localization.localAlgHom' I J K f h) a =
    ((Localization.monoidOf J.primeCompl).lift₀ ((algebraMap P (Localization.AtPrime K)).comp ↑f).toMonoidWithZeroHom ⋯)
      a
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- The submonoid `Δ` lies in the commensurator of the right subgroup (hence, the subgroups
being commensurable, also in that of the left one; see `le_commensurator_left`).  -/
IsHeckeTriple.le_commensurator_right : ∀ {G : Type u_1} {inst : Group G} {Δ : Submonoid G} (H₁ : Subgroup G) {H₂ : Subgroup G} [self : IsHeckeTriple Δ H₁ H₂],
  Δ ≤ (Subgroup.Commensurable.commensurator H₂).toSubmonoid
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instFromJsonCodeActionOptions : Lean.FromJson Lean.Lsp.CodeActionOptions
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
/-- The fundamental groupoid of a topological space.  -/
FundamentalGroupoid.termπₓ : Lean.ParserDescr
-- Mathlib.Logic.Function.Basic
Function.Surjective.of_comp : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α},
  Function.Surjective (f ∘ g) → Function.Surjective f
-- Mathlib.Data.Set.Lattice
Set.biUnion_insert : ∀ {α : Type u_1} {β : Type u_2} (a : α) (s : Set α) (t : α → Set β), ⋃ x ∈ insert a s, t x = t a ∪ ⋃ x ∈ s, t x
-- Mathlib.Order.Std
/-- The `Ord` instance of the order. This can always be automatically derived.  -/
LinearOrder.OfStdArgs.ord : {α : Type u_1} →
  (self : LinearOrder.OfStdArgs α) →
    let this := self.lt;
    let this := self.decidableEq;
    let this := self.decidableLT;
    Ord α
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_congr_ae : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f g : X → E} {s : Set X} {μ : MeasureTheory.Measure X},
  MeasurableSet s → (∀ᵐ (x : X) ∂μ, x ∈ s → f x = g x) → ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.toOrderHom : {α : Type u_2} →
  {β : Type u_3} → [inst : OmegaCompletePartialOrder α] → [inst_1 : OmegaCompletePartialOrder β] → (α →𝒄 β) → α →o β
-- Batteries.Data.Int
Int.testBit_ofBits_ge : ∀ {n i : ℕ} {f : Fin n → Bool}, i ≥ n → (Int.ofBits f).testBit i = decide (Int.ofBits f < 0)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- If `F : C ⥤ D` is a fully faithful monoidal functor, then
`CommMonCat(F) : CommMonCat C ⥤ CommMonCat D` is fully faithful too.  -/
CategoryTheory.Functor.FullyFaithful.mapCommMon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                {F : CategoryTheory.Functor C D} → [inst_6 : F.Braided] → F.FullyFaithful → F.mapCommMon.FullyFaithful
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.chainLength_zero : ∀ {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)
  [inst_8 : Nontrivial L], LieAlgebra.IsKilling.chainLength 0 β = 0
-- Lean.Elab.Tactic.Omega.Core
/-- Solve an "easy" equality, i.e. one with a coefficient that is `±1`.

After solving, the variable will have been eliminated from all constraints.
 -/
Lean.Elab.Tactic.Omega.Problem.solveEasyEquality : Lean.Elab.Tactic.Omega.Problem → Lean.Omega.Coeffs → Lean.Elab.Tactic.Omega.Problem
-- Init.Data.List.Count
List.countP_eq_length : ∀ {α : Type u_1} {l : List α} {p : α → Bool}, List.countP p l = l.length ↔ ∀ a ∈ l, p a = true
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_dual : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, (⇑OrderDual.ofDual ⁻¹' s).OrdConnected ↔ s.OrdConnected
-- Std.Sat.AIG.Basic
Std.Sat.AIG.TernaryInput.discr : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → aig.TernaryInput → aig.Ref
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.prod_comp : ∀ {R : Type u} [inst : CommSemiring R] {ι : Type u_1} (s : Finset ι) (p : ι → Polynomial R) (q : Polynomial R),
  (∏ j ∈ s, p j).comp q = ∏ j ∈ s, (p j).comp q
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.circuit_iff_delete_of_disjoint : ∀ {α : Type u_1} {M : Matroid α} {D C : Set α}, Disjoint C D → (M.IsCircuit C ↔ (M.delete D).IsCircuit C)