mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Json.Basic
Lean.Json.brecOn_2.eq : ∀ {motive_1 : Lean.Json → Sort u} {motive_2 : Array Lean.Json → Sort u}
  {motive_3 : Std.TreeMap.Raw String Lean.Json compare → Sort u} {motive_4 : List Lean.Json → Sort u}
  {motive_5 : Std.DTreeMap.Raw String (fun x => Lean.Json) compare → Sort u}
  {motive_6 : (Std.DTreeMap.Internal.Impl String fun x => Lean.Json) → Sort u}
  (t : Std.TreeMap.Raw String Lean.Json compare) (F_1 : (t : Lean.Json) → t.below → motive_1 t)
  (F_2 : (t : Array Lean.Json) → Lean.Json.below_1 t → motive_2 t)
  (F_3 : (t : Std.TreeMap.Raw String Lean.Json compare) → Lean.Json.below_2 t → motive_3 t)
  (F_4 : (t : List Lean.Json) → Lean.Json.below_3 t → motive_4 t)
  (F_5 : (t : Std.DTreeMap.Raw String (fun x => Lean.Json) compare) → Lean.Json.below_4 t → motive_5 t)
  (F_6 : (t : Std.DTreeMap.Internal.Impl String fun x => Lean.Json) → Lean.Json.below_5 t → motive_6 t),
  Lean.Json.brecOn_2 t F_1 F_2 F_3 F_4 F_5 F_6 = F_3 t (Lean.Json.brecOn_2.go t F_1 F_2 F_3 F_4 F_5 F_6).2
-- Mathlib.Data.Real.ConjExponents
Real.holderTriple_iff : ∀ (p q r : ℝ), p.HolderTriple q r ↔ p⁻¹ + q⁻¹ = r⁻¹ ∧ 0 < p ∧ 0 < q
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_insertMany!_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α},
      compare k k' = Ordering.eq →
        List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
          k ∈ List.map Sigma.fst l → (↑(t.insertMany! l)).getKey? k' = some k
-- Lean.Elab.Tactic.Conv.Basic
Lean.Elab.Tactic.Conv.getRhs : Lean.Elab.Tactic.TacticM Lean.Expr
-- Mathlib.MeasureTheory.Measure.EverywherePos
/-- **Halmos' theorem: Haar measure is completion regular.** More precisely, any finite measure
set can be approximated from inside by a level set of a continuous function with compact support.  -/
MeasureTheory.Measure.innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_group : ∀ {G : Type u_2} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G]
  [inst_4 : MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant]
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop],
  μ.InnerRegularWRT (fun s => ∃ f, Continuous f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) fun s =>
    MeasurableSet s ∧ μ s ≠ ⊤
-- Mathlib.RingTheory.Support
Module.support_quotSMulTop : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Finite R M]
  (x : R), Module.support R (QuotSMulTop x M) = Module.support R M ∩ PrimeSpectrum.zeroLocus {x}
-- Mathlib.LinearAlgebra.FreeAlgebra
FreeAlgebra.instFree : ∀ (R : Type u) (X : Type v) [inst : CommSemiring R], Module.Free R (FreeAlgebra R X)
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.mapAlgHom_coe_ringHom : ∀ {R : Type u} {A : Type z} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B), ↑(Polynomial.mapAlgHom f) = Polynomial.mapRingHom ↑f
-- Init.Data.List.Nat.TakeDrop
List.zip_eq_zip_take_min : ∀ {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β},
  l₁.zip l₂ = (List.take (min l₁.length l₂.length) l₁).zip (List.take (min l₁.length l₂.length) l₂)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
_private.Mathlib.RingTheory.DedekindDomain.Ideal.Basic.0.isDedekindDomainInv_iff : ∀ {A : Type u_2} {K : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K] [inst_4 : IsDomain A],
  IsDedekindDomainInv✝ A ↔ ∀ (I : FractionalIdeal (nonZeroDivisors A) K), I ≠ ⊥ → I * I⁻¹ = 1
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.beth_mono : Monotone Cardinal.beth
-- Mathlib.Data.NNReal.Defs
NNReal.coe_natCast : ∀ (n : ℕ), ↑↑n = ↑n
-- Mathlib.CategoryTheory.Sites.RegularEpi
CategoryTheory.instIsRegularEpiCategorySheafTypeOfHasSheafify : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  [CategoryTheory.HasSheafify J (Type u)], CategoryTheory.IsRegularEpiCategory (CategoryTheory.Sheaf J (Type u))
-- Init.Internal.Order.Lemmas
Lean.Order.Array.monotone_mapM : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] (xs : Array α) (f : γ → α → m β),
  Lean.Order.monotone f → Lean.Order.monotone fun x => Array.mapM (f x) xs
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation
_private.Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation.0.MeasureTheory.VectorMeasure.semivariation_univ_lt_top : ∀ {X : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mX : MeasurableSpace X}
  {μ : MeasureTheory.VectorMeasure X E}, μ.semivariation Set.univ < ⊤
-- Mathlib.Order.LiminfLimsup
Filter.sdiff_limsup : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteBooleanAlgebra α] (f : Filter β) (u : β → α) [f.NeBot] (a : α),
  a \ Filter.limsup u f = Filter.liminf (fun b => a \ u b) f
-- Lean.Util.PPExt
Lean.PPFns : Type
-- Mathlib.Topology.Algebra.Valued.ValuedField
/-- A valued field is completable.  -/
Valued.completable : ∀ {K : Type u_1} [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀],
  CompletableTopField K
-- Init.Data.Nat.Dvd
Nat.dvd_add : ∀ {a b c : ℕ}, a ∣ b → a ∣ c → a ∣ b + c
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- If the `d`th coefficient of a formal power series is nonzero,
then the weighted order of the power series is less than or equal to `weight d w`.  -/
MvPowerSeries.weightedOrder_le : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R} {d : σ →₀ ℕ},
  (MvPowerSeries.coeff d) f ≠ 0 → MvPowerSeries.weightedOrder w f ≤ ↑((Finsupp.weight w) d)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_modify_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {fallback : β k} {f : β k → β k}, (m.modify k f).getD k fallback = (Option.map f (m.get? k)).getD fallback
-- Mathlib.Topology.Instances.ENNReal.Lemmas
Continuous.edist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : TopologicalSpace β] {f g : β → α},
  Continuous f → Continuous g → Continuous fun b => edist (f b) (g b)
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_monomial : ∀ {R : Type u_1} [inst : Semiring R] (r : R) {S : Type u_2} [inst_1 : AddCommMonoid S] [inst_2 : Pow S ℕ]
  [inst_3 : MulActionWithZero R S] (x : S) (n : ℕ), ((Polynomial.monomial n) r).smeval x = r • x ^ n
-- Mathlib.Algebra.Homology.ImageToKernel
imageToKernel_comp_hom_inv_comp : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V}
  (f : A ⟶ B) (g : B ⟶ C) [inst_2 : CategoryTheory.Limits.HasEqualizers V] [inst_3 : CategoryTheory.Limits.HasImages V]
  {Z : V} {i : B ≅ Z}
  (w :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f i.hom)
        (CategoryTheory.CategoryStruct.comp i.inv g) =
      0),
  imageToKernel (CategoryTheory.CategoryStruct.comp f i.hom) (CategoryTheory.CategoryStruct.comp i.inv g) w =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f i.hom).hom
      (CategoryTheory.CategoryStruct.comp (imageToKernel f g ⋯)
        (CategoryTheory.Limits.kernelSubobjectIsoComp i.inv g).inv)
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
/-- A tagged partition `π` is subordinate to `r : (ι → ℝ) → ℝ` if each box `J ∈ π` is included in
the closed ball with center `π.tag J` and radius `r (π.tag J)`.  -/
BoxIntegral.TaggedPrepartition.IsSubordinate : {ι : Type u_1} →
  {I : BoxIntegral.Box ι} → [Fintype ι] → BoxIntegral.TaggedPrepartition I → ((ι → ℝ) → ↑(Set.Ioi 0)) → Prop
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.UnsatProof.lt.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Linear.IneqCnstr},
  Lean.Meta.Grind.Arith.Linear.UnsatProof.lt c = Lean.Meta.Grind.Arith.Linear.UnsatProof.lt c_1 → c = c_1
-- Mathlib.Computability.Reduce
/-- A many-one degree is an equivalence class of sets up to many-one equivalence.  -/
ManyOneDegree : Type
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.filterAt_enlarge : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (v : VitaliFamily μ) {δ : ℝ} (δpos : 0 < δ), (v.enlarge δ δpos).filterAt = v.filterAt
-- Mathlib.Topology.Order.OrderClosed
Ioc_mem_nhdsGE_of_mem : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b c : α},
  b ∈ Set.Ioo c a → Set.Ioc c a ∈ nhdsWithin b (Set.Ici b)
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ : B} (f : b₀ ⟶ b₁) (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₁)}
  (h : (F.map (CategoryTheory.CategoryStruct.id b₁)).toFunctor.obj ((F.map f).toFunctor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp' f (CategoryTheory.CategoryStruct.id b₁) f ⋯).hom.toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((F.mapId b₁).inv.toNatTrans.app ((F.map f).toFunctor.obj X)) h
-- Lean.Elab.Match
Lean.Elab.Term.PatternElabException.mk.injEq : ∀ (ex : Lean.Exception) (patternIdx : ℕ) (pathToIndex : List ℕ) (ex_1 : Lean.Exception) (patternIdx_1 : ℕ)
  (pathToIndex_1 : List ℕ),
  ({ ex := ex, patternIdx := patternIdx, pathToIndex := pathToIndex } =
      { ex := ex_1, patternIdx := patternIdx_1, pathToIndex := pathToIndex_1 }) =
    (ex = ex_1 ∧ patternIdx = patternIdx_1 ∧ pathToIndex = pathToIndex_1)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.instFaithfulSimplexCategoryInclusion : AugmentedSimplexCategory.inclusion.Faithful
-- Mathlib.Topology.Order.NhdsSet
hasBasis_nhdsSet_Ici_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] (a : α)
  [(nhdsWithin a (Set.Iio a)).NeBot], (nhdsSet (Set.Ici a)).HasBasis (fun x => x < a) Set.Ici
-- Mathlib.CategoryTheory.Category.Cat.Limit
/-- Auxiliary definition: the proposed cone is a limit cone.  -/
CategoryTheory.Cat.HasLimits.limitConeIsLimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J CategoryTheory.Cat) →
      CategoryTheory.Limits.IsLimit (CategoryTheory.Cat.HasLimits.limitCone F)
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
/-- A prepartition of `I : BoxIntegral.Box ι` is a finite set of pairwise disjoint subboxes of
`I`.  -/
BoxIntegral.Prepartition : {ι : Type u_1} → BoxIntegral.Box ι → Type u_1
-- Lean.Syntax
Lean.Syntax.Range.mk.sizeOf_spec : ∀ (start stop : String.Pos.Raw), sizeOf { start := start, stop := stop } = 1 + sizeOf start + sizeOf stop
-- Mathlib.MeasureTheory.Measure.AEMeasurable
_private.Mathlib.MeasureTheory.Measure.AEMeasurable.0.cond.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_alter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] [Inhabited α] (h : t.WF) {k k' : α} {f : Option (β k) → Option (β k)}
  {hc : k' ∈ (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.getKey k' hc =
    if heq : compare k k' = Ordering.eq then k else t.getKey k' ⋯
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get!_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β], k ∉ t₂ → (t₁ ∪ t₂).get! k = t₁.get! k
-- Init.Data.Array.Lemmas
Array.sum_singleton : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α] [Std.LawfulRightIdentity (fun x1 x2 => x1 + x2) 0] {x : α},
  #[x].sum = x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp_inv_app_fst_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅} {Z : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] [inst_4 : CategoryTheory.Category.{v₅, u₅} Y]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} Z] (U : CategoryTheory.Functor X Y) (V : CategoryTheory.Functor Y Z)
  (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Z) (x : X),
  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp F G U V).inv.app X_1).fst.app x =
    CategoryTheory.CategoryStruct.id (X_1.fst.obj (V.obj (U.obj x)))
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
IsAbsoluteValue.mk : ∀ {S : Type u_5} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_6} [inst_2 : Semiring R] {f : R → S},
  (∀ (x : R), 0 ≤ f x) →
    (∀ {x : R}, f x = 0 ↔ x = 0) →
      (∀ (x y : R), f (x + y) ≤ f x + f y) → (∀ (x y : R), f (x * y) = f x * f y) → IsAbsoluteValue f
-- Mathlib.Order.Filter.Basic
Filter.frequently_imp_distrib_right : ∀ {α : Type u} {f : Filter α} [f.NeBot] {p : α → Prop} {q : Prop},
  (∃ᶠ (x : α) in f, p x → q) ↔ (∀ᶠ (x : α) in f, p x) → q
-- Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
/-- The kernel of the surjective map from `Fin n → R` (i.e. `R^n`) to the module represented.  -/
FGModuleRepr.S : {R : Type u} → [inst : Ring R] → (self : FGModuleRepr R) → Submodule R (Fin self.n → R)
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.add_def_apply : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (f g : M →ₚₗ[R] N) (S : Type u) [inst_5 : CommSemiring S]
  [inst_6 : Algebra R S] (m : TensorProduct R S M), (f + g).toFun' S m = f.toFun' S m + g.toFun' S m
-- Mathlib.RingTheory.MatrixPolynomialAlgebra
matPolyEquiv_symm_apply_coeff : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (p : Polynomial (Matrix n n R)) (i j : n) (k : ℕ), (matPolyEquiv.symm p i j).coeff k = p.coeff k i j
-- Init.Conv
/-- `rw [thm]` rewrites the target using `thm`. See the `rw` tactic for more information.  -/
Lean.Parser.Tactic.Conv.rewrite : Lean.ParserDescr
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.mulActionHom_singleton.eq_1 : ∀ (G : Type u_1) [inst : Group G] (α : Type u_2) [inst_1 : MulAction G α] [inst_2 : DecidableEq α],
  Set.powersetCard.mulActionHom_singleton G α = { toFun := ⇑Set.powersetCard.ofSingleton, map_smul' := ⋯ }
-- Std.Data.TreeMap.Raw.Slice
Std.TreeMap.Raw.toList_rco : ∀ {α : Type u} {β : Type v} (cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw.toList_rco._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeMap.Raw α β cmp},
  t.WF →
    ∀ {lowerBound upperBound : α},
      Std.Slice.toList (Std.Rco.Sliceable.mkSlice t lowerBound...upperBound) =
        List.filter (fun e => decide ((cmp e.1 lowerBound).isGE = true ∧ (cmp e.1 upperBound).isLT = true)) t.toList
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.zero_mul : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] {a : FreeAlgebra.Pre R X}, FreeAlgebra.Rel R X (0 * a) 0
-- Mathlib.Data.Finset.SDiff
Finset.union_sdiff_self_eq_union : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ∪ t \ s = s ∪ t
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.balance1_toList : ∀ {α : Type u_1} {l : RBTree.RBNode α} {v : α} {r : RBTree.RBNode α},
  (l.balance1 v r).toList = l.toList ++ v :: r.toList
-- Mathlib.Tactic.ClickSuggestions.Rewrite
/-- The new subexpression.  -/
Mathlib.Tactic.ClickSuggestions.RwKey.replacement : Mathlib.Tactic.ClickSuggestions.RwKey → Lean.Meta.AbstractMVarsResult
-- Mathlib.Order.SuccPred.Basic
Order.Iic_subset_Iio_succ_of_not_isMax : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a : α}, ¬IsMax a → Set.Iic a ⊆ Set.Iio (Order.succ a)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf'_congr : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] {s : Finset β} (H : s.Nonempty) {t : Finset β} {f g : β → α}
  (h₁ : s = t), (∀ x ∈ s, f x = g x) → s.inf' H f = t.inf' ⋯ g
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.coroot_neg : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [inst_6 : LieModule.IsTriangularizable K (↥H) L] (α : LieModule.Weight K (↥H) L),
  LieAlgebra.IsKilling.coroot (-α) = -LieAlgebra.IsKilling.coroot α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_empty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} [Std.TransOrd α] [inst : Std.LawfulEqOrd α] {a : α}
  [inst_1 : Inhabited (β a)], Std.DTreeMap.Internal.Impl.empty.get! a = default
-- Mathlib.RingTheory.KrullDimension.Basic
/-- Type class for rings with krull dimension at most `n`.  -/
Ring.KrullDimLE : ℕ → (R : Type u_1) → [CommSemiring R] → Prop
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.yoneda'_comp : CategoryTheory.yoneda'.comp (CategoryTheory.sheafToPresheaf CategoryTheory.typesGrothendieckTopology (Type u)) =
  CategoryTheory.yoneda
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.mul_add_right_left : ∀ {R : Type u_1} [inst : CommRing R] {x y : R}, IsRelPrime x y → ∀ (z : R), IsRelPrime (z * y + x) y
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.mem_sInf : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {S : Set (L.Substructure M)} {x : M},
  x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.ext_iff : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  {P : C(X, Y) → Prop} {F G : f₀.HomotopyWith f₁ P}, F = G ↔ ∀ (x : ↑unitInterval × X), F x = G x
-- Init.Data.Vector.Basic
/-- Variant of `mapIdxM` which receives the index `i` along with the bound `i < n.  -/
Vector.mapFinIdxM : {n : ℕ} →
  {α : Type u} →
    {β : Type v} → {m : Type v → Type w} → [Monad m] → Vector α n → ((i : ℕ) → α → i < n → m β) → m (Vector β n)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  [inst_1 : Inhabited β], k ∈ t₂ → (t₁ ∩ t₂)[k]! = t₁[k]!
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_pEmpty : Ordinal.type emptyRelation = 0
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.NullMeasurableSet.addFundamentalInterior : ∀ (G : Type u_1) {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α) [Countable G]
  [inst_3 : MeasurableSpace α] [MeasurableConstVAdd G α] {μ : MeasureTheory.Measure α}
  [MeasureTheory.VAddInvariantMeasure G α μ],
  MeasureTheory.NullMeasurableSet s μ → MeasureTheory.NullMeasurableSet (MeasureTheory.addFundamentalInterior G s) μ
-- Mathlib.Algebra.Group.Hom.Basic
MonoidHom.coe_of_map_mul_inv : ∀ {G : Type u_5} [inst : Group G] {H : Type u_8} [inst_1 : Group H] (f : G → H)
  (map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹), ⇑(MonoidHom.ofMapMulInv f map_div) = f
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.zero_eq_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (M : C) [inst_2 : CategoryTheory.AddMonObj M], CategoryTheory.AddMonObj.zero = 0
-- Plausible.Random
/-- Generate a value of type `α` randomly using generator `g`.
 -/
Plausible.Random.random : {m : Type u → Type u_1} →
  {α : Type u} → [self : Plausible.Random m α] → {g : Type} → [RandomGen g] → Plausible.RandGT g m α
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` creates limits of shape `Jᵒᵖ`, then `F : Cᵒᵖ ⥤ D` creates colimits
of shape `J`.  -/
CategoryTheory.Limits.createsColimitsOfShapeOfRightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (J : Type w) →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (F : CategoryTheory.Functor Cᵒᵖ D) →
              [CategoryTheory.CreatesLimitsOfShape Jᵒᵖ F.rightOp] → CategoryTheory.CreatesColimitsOfShape J F
-- Mathlib.ModelTheory.Bundled
/-- A structure that is elementarily equivalent to a model, bundled as a model.  -/
FirstOrder.Language.ElementarilyEquivalent.toModel : {L : FirstOrder.Language} →
  (T : L.Theory) →
    {M : T.ModelType} → {N : Type u_1} → [LN : L.Structure N] → L.ElementarilyEquivalent (↑M) N → T.ModelType
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.evalList.match_1.splitter : (motive : List ℕ → Sort u_1) →
  (x : List ℕ) →
    (Unit → motive []) →
      ((x : ℕ) → motive [x]) → ((x : ℕ) → (xs : List ℕ) → (xs = [] → False) → motive (x :: xs)) → motive x
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.finsubgraphOfAdj.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (e : G.Adj u v), SimpleGraph.finsubgraphOfAdj e = ⟨G.subgraphOfAdj e, ⋯⟩
-- Mathlib.Order.Filter.Pi
Filter.pi_mono : ∀ {ι : Type u_1} {α : ι → Type u_2} {f₁ f₂ : (i : ι) → Filter (α i)},
  (∀ (i : ι), f₁ i ≤ f₂ i) → Filter.pi f₁ ≤ Filter.pi f₂
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Submodule.isAssociatedPrime_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {I : Ideal R} [IsNoetherianRing R], N.IsAssociatedPrime I ↔ I.IsPrime ∧ ∃ x, I = N.colon {x}
-- Mathlib.Data.List.Sort
List.sortedLT_range : ∀ (n : ℕ), (List.range n).SortedLT
-- Mathlib.CategoryTheory.Preadditive.Schur
/-- As a corollary of Schur's lemma for preadditive categories,
any morphism between simple objects is (exclusively) either an isomorphism or zero.
 -/
CategoryTheory.isIso_iff_nonzero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasKernels C] {X Y : C} [CategoryTheory.Simple X] [CategoryTheory.Simple Y] (f : X ⟶ Y),
  CategoryTheory.IsIso f ↔ f ≠ 0
-- Mathlib.Order.Category.FinBddDistLat
/-- Typecheck a `BoundedLatticeHom` as a morphism in `FinBddDistLat`.  -/
FinBddDistLat.ofHom : {X Y : Type u} →
  [inst : DistribLattice X] →
    [inst_1 : BoundedOrder X] →
      [inst_2 : Fintype X] →
        [inst_3 : DistribLattice Y] →
          [inst_4 : BoundedOrder Y] →
            [inst_5 : Fintype Y] → BoundedLatticeHom X Y → (FinBddDistLat.of X ⟶ FinBddDistLat.of Y)
-- Mathlib.Logic.Basic
iff_eq_eq : ∀ {a b : Prop}, (a ↔ b) = (a = b)
-- Mathlib.Order.RelClasses
Order.Preimage.instIsStrictOrder : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} [IsStrictOrder α r] {f : β → α}, IsStrictOrder β (f ⁻¹'o r)
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.instDecidablePredMemAddSubmonoidStabilizerAddSubmonoidOfDecidableEq : {M : Type u_1} →
  {α : Type u_3} →
    [inst : AddMonoid M] →
      [inst_1 : AddAction M α] →
        [DecidableEq α] → (a : α) → DecidablePred fun x => x ∈ AddAction.stabilizerAddSubmonoid M a
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instIsTriangulatedFullSubcategory : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [inst_6 : P.IsTriangulated] [CategoryTheory.IsTriangulated C],
  CategoryTheory.IsTriangulated P.FullSubcategory