mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Monovary
AntivaryOn.add_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f₁ f₂ : ι → α} {g : ι → β},
  AntivaryOn f₁ g s → AntivaryOn f₂ g s → AntivaryOn (f₁ + f₂) g s
-- Aesop.Frontend.Command
Aesop.Frontend.Parser.showStats : Lean.ParserDescr
-- Mathlib.NumberTheory.NumberField.House
/-- `ξ` is the product of `x (l, r)` and the `r`-th basis element of the newBasis of `K`.  -/
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.ξ : (K : Type u_1) →
  [inst : Field K] → [NumberField K] → {β : Type u_3} → (β × (K →+* ℂ) → ℤ) → β → NumberField.RingOfIntegers K
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- In a normed vector space, the addition of a strongly measurable function and a measurable
function is measurable. Note that this is not true without further second-countability assumptions
for the addition of two measurable functions.  -/
Measurable.stronglyMeasurable_add : ∀ {α : Type u_5} {E : Type u_6} {x : MeasurableSpace α} [inst : AddCancelMonoid E] [inst_1 : TopologicalSpace E]
  [inst_2 : MeasurableSpace E] [BorelSpace E] [ContinuousAdd E] [TopologicalSpace.PseudoMetrizableSpace E]
  {g f : α → E}, Measurable g → MeasureTheory.StronglyMeasurable f → Measurable (f + g)
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- `centroidWeightsWithCircumcenter` sums to 1, if the `Finset` is nonempty.  -/
Affine.Simplex.sum_centroidWeightsWithCircumcenter : ∀ {n : ℕ} {fs : Finset (Fin (n + 1))}, fs.Nonempty → ∑ i, Affine.Simplex.centroidWeightsWithCircumcenter fs i = 1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey!_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {f : α → β → Option γ} {k : α},
  (Std.DHashMap.filterMap f m).getKey! k =
    ((m.getKey? k).pfilter fun x_2 h' => (f x_2 (Std.DHashMap.Const.get m x_2 ⋯)).isSome).get!
-- Mathlib.Algebra.Algebra.Basic
/-- Algebra over a subsemiring. This builds upon `Subsemiring.module`.  -/
Algebra.ofSubsemiring : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [Algebra R A] →
          {C : Type u_4} → [inst_3 : SetLike C R] → [inst_4 : SubsemiringClass C R] → (S : C) → Algebra (↥S) A
-- Mathlib.CategoryTheory.Sites.GlobalSections
/-- For sheaves of types, the global sections functor is isomorphic to the covariant hom
functor of the terminal sheaf.  -/
CategoryTheory.Sheaf.ΓNatIsoCoyoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (X : Type (max u v)) →
        [Unique X] →
          CategoryTheory.Sheaf.Γ J (Type (max u v)) ≅
            CategoryTheory.coyoneda.obj (Opposite.op ((CategoryTheory.constantSheaf J (Type (max u v))).obj X))
-- Mathlib.Topology.Algebra.Valued.NormedValued
/-- The valuation on a nonarchimedean normed field `K` defined as `nnnorm`.  -/
NormedField.valuation : {K : Type u_1} → [hK : NormedField K] → [IsUltrametricDist K] → Valuation K NNReal
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintKind.noConfusionType : Sort v✝ → Lean.Lsp.InlayHintKind → Lean.Lsp.InlayHintKind → Sort v✝
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α} (not_mem : k ∉ t₂) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).getKey k h' = t₁.getKey k ⋯
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
/-- A space is a compactly coherent space if the topology is generated by the compact sets.  -/
CompactlyCoherentSpace.isCoherentWith : ∀ {X : Type u_1} {inst : TopologicalSpace X} [self : CompactlyCoherentSpace X],
  Topology.IsCoherentWith {K | IsCompact K}
-- Mathlib.Combinatorics.Optimization.ValuedCSP
ValuedCSP.Term.mk.sizeOf_spec : ∀ {D : Type u_1} {C : Type u_2} [inst : AddCommMonoid C] [inst_1 : PartialOrder C] [inst_2 : IsOrderedAddMonoid C]
  {Γ : ValuedCSP D C} {ι : Type u_3} [inst_3 : SizeOf D] [inst_4 : SizeOf C]
  [inst_5 : (a : (n : ℕ) × ((Fin n → D) → C)) → SizeOf (Γ a)] [inst_6 : SizeOf ι] (n : ℕ) (f : (Fin n → D) → C)
  (inΓ : ⟨n, f⟩ ∈ Γ) (app : Fin n → ι), sizeOf { n := n, f := f, inΓ := inΓ, app := app } = 1 + sizeOf n + sizeOf inΓ
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
/-- The cocone for `G : J ⥤ Type w₀'` that is deduced from a cocone for `F : J ⥤ Type w₀`
and a natural map `G.obj j → F.obj j` for all `j : J`.  -/
CategoryTheory.Functor.CoconeTypes.precompose : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {F : CategoryTheory.Functor J (Type w₀)} →
      F.CoconeTypes →
        {G : CategoryTheory.Functor J (Type w₀')} →
          (app : (j : J) → G.obj j → F.obj j) →
            (∀ {j j' : J} (f : j ⟶ j'),
                app j' ∘ ⇑(CategoryTheory.ConcreteCategory.hom (G.map f)) =
                  ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ∘ app j) →
              G.CoconeTypes
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.mk.congr_simp : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {f : Polynomial R}
  (map map_1 : Polynomial R →ₐ[R] S) (e_map : map = map_1) (map_surjective : Function.Surjective ⇑map)
  (ker_map : RingHom.ker map = Ideal.span {f}),
  { map := map, map_surjective := map_surjective, ker_map := ker_map } =
    { map := map_1, map_surjective := ⋯, ker_map := ⋯ }
-- Mathlib.CategoryTheory.Functor.FunctorHom
/-- Morphisms `(𝟙_ (C ⥤ Type max v' v u) ⟶ F.functorHom G)` are in bijection with
morphisms `F ⟶ G`.  -/
CategoryTheory.Functor.natTransEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {F G : CategoryTheory.Functor C D} →
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor C (Type (max v' v u))) ⟶
              F.functorHom G) ≃
            (F ⟶ G)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Ring.mk.inj : ∀ {id : ℕ} {type : Lean.Expr} {u : Lean.Level} {ringInst semiringInst : Lean.Expr} {charInst? : Option (Lean.Expr × ℕ)}
  {addFn? mulFn? subFn? negFn? powFn? intCastFn? natCastFn? one? : Option Lean.Expr} {vars : Lean.PArray Lean.Expr}
  {varMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.CommRing.Var}
  {denote : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.CommRing.RingExpr} {id_1 : ℕ} {type_1 : Lean.Expr}
  {u_1 : Lean.Level} {ringInst_1 semiringInst_1 : Lean.Expr} {charInst?_1 : Option (Lean.Expr × ℕ)}
  {addFn?_1 mulFn?_1 subFn?_1 negFn?_1 powFn?_1 intCastFn?_1 natCastFn?_1 one?_1 : Option Lean.Expr}
  {vars_1 : Lean.PArray Lean.Expr} {varMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.CommRing.Var}
  {denote_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.CommRing.RingExpr},
  { id := id, type := type, u := u, ringInst := ringInst, semiringInst := semiringInst, charInst? := charInst?,
        addFn? := addFn?, mulFn? := mulFn?, subFn? := subFn?, negFn? := negFn?, powFn? := powFn?,
        intCastFn? := intCastFn?, natCastFn? := natCastFn?, one? := one?, vars := vars, varMap := varMap,
        denote := denote } =
      { id := id_1, type := type_1, u := u_1, ringInst := ringInst_1, semiringInst := semiringInst_1,
        charInst? := charInst?_1, addFn? := addFn?_1, mulFn? := mulFn?_1, subFn? := subFn?_1, negFn? := negFn?_1,
        powFn? := powFn?_1, intCastFn? := intCastFn?_1, natCastFn? := natCastFn?_1, one? := one?_1, vars := vars_1,
        varMap := varMap_1, denote := denote_1 } →
    id = id_1 ∧
      type = type_1 ∧
        u = u_1 ∧
          ringInst = ringInst_1 ∧
            semiringInst = semiringInst_1 ∧
              charInst? = charInst?_1 ∧
                addFn? = addFn?_1 ∧
                  mulFn? = mulFn?_1 ∧
                    subFn? = subFn?_1 ∧
                      negFn? = negFn?_1 ∧
                        powFn? = powFn?_1 ∧
                          intCastFn? = intCastFn?_1 ∧
                            natCastFn? = natCastFn?_1 ∧
                              one? = one?_1 ∧ vars = vars_1 ∧ varMap = varMap_1 ∧ denote = denote_1
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Pos.revSkipWhile_bool_eq_self_iff_get : ∀ {p : Char → Bool} {s : String} {pos : s.Pos},
  pos.revSkipWhile p = pos ↔ ∀ (h : pos ≠ s.startPos), p ((pos.prev h).get ⋯) = false
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.balanceR_aux : ∀ {α : Type u_1} [inst : Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ l ↑x →
    Ordnode.Valid' (↑x) r o₂ →
      (r.size = 0 → l.size ≤ 1) →
        (1 ≤ r.size → 1 ≤ l.size → l.size ≤ Ordnode.delta * r.size) →
          2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3 → Ordnode.Valid' o₁ (l.balanceR x r) o₂
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.isUnit_unit : ∀ {M : Type u_1} [inst : CommMonoid M] {ζ : M} {n : ℕ} (hn : n ≠ 0) (hζ : IsPrimitiveRoot ζ n), IsPrimitiveRoot ⋯.unit n
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.RightExtension.coneAtFunctor_obj : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (Y : D) (E : L.RightExtension F),
  (CategoryTheory.Functor.RightExtension.coneAtFunctor L F Y).obj E = E.coneAt Y
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.integralPowerBasis.eq_1 : ∀ {n : ℕ} {K : Type u} [inst : Field K] {ζ : K} [inst_1 : NeZero n] [inst_2 : CharZero K]
  [inst_3 : IsCyclotomicExtension {n} ℚ K] (hζ : IsPrimitiveRoot ζ n),
  hζ.integralPowerBasis = (Algebra.adjoin.powerBasis' ⋯).map hζ.adjoinEquivRingOfIntegers
-- 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] [inst_4 : Algebra R P] (I : Ideal S) [inst_5 : I.IsPrime] (J : Ideal P) [inst_6 : J.IsPrime]
  (f : S →ₐ[R] P) (hIJ : I = Ideal.comap f J) (x : Localization.AtPrime I),
  (Localization.localAlgHom I J f hIJ) x = (Localization.localRingHom I J f.toRingHom hIJ) x
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.typeEquiv_functor_obj_obj_map_hom_apply_hom_apply : ∀ (α : Type u) {X Y : Type uᵒᵖ} (f : X ⟶ Y) (g : Opposite.unop X ⟶ α) (a : Opposite.unop Y),
  (CategoryTheory.ConcreteCategory.hom
        ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.typeEquiv.functor.obj α).obj.map f)) g))
      a =
    g.hom' (f.unop.hom' a)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.Assignment.instToString.match_1.eq_2 : ∀ (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg)
  (h_3 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both)
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned),
  (match Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg with
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.both => h_3 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned => h_4 ()) =
    h_2 ()
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.one_add_natCast : ∀ (m : ℕ), 1 + ↑m = ↑(Order.succ m)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_neg_two : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.T R (-2) = 2 * Polynomial.X ^ 2 - 1
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- There are `r` parts or `t = 0`.  -/
SimpleGraph.CompleteEquipartiteSubgraph.card_parts : ∀ {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} (self : G.CompleteEquipartiteSubgraph r t), self.parts.card = r ∨ t = 0
-- Aesop.Options.Public
Aesop.instReprStrategy : Repr Aesop.Strategy
-- Mathlib.AlgebraicTopology.SimplicialSet.NonsingularColimit
/-- If `X` is a nonsingular simplicial set, this is the cocone consisting
of the (mono)morphisms `Δ[x.dim] ⟶ X` for all nondegenerate simplices `x : X.N`.  -/
SSet.coconeN' : (X : SSet) → [inst : X.Nonsingular] → CategoryTheory.Limits.Cocone X.functorN'
-- Mathlib.RingTheory.Polynomial.Pochhammer
descPochhammer_eval_eq_prod_range : ∀ {R : Type u_1} [inst : CommRing R] (n : ℕ) (r : R),
  Polynomial.eval r (descPochhammer R n) = ∏ j ∈ Finset.range n, (r - ↑j)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.beq_congr : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] [inst_1 : (k : α) → BEq (β k)] {m₃ m₄ : Std.DTreeMap.Internal.Impl α β},
  m₁.WF → m₂.WF → m₃.WF → m₄.WF → m₁.Equiv m₃ → m₂.Equiv m₄ → m₁.beq m₂ = m₃.beq m₄
-- Mathlib.SetTheory.Cardinal.Basic
/-- See also `Cardinal.nsmul_lt_aleph0_iff` for a hypothesis-free version.  -/
Cardinal.nsmul_lt_aleph0_iff_of_ne_zero : ∀ {n : ℕ} {a : Cardinal.{u_1}}, n ≠ 0 → (n • a < Cardinal.aleph0 ↔ a < Cardinal.aleph0)
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.restrict_eq_freeOn_iff : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.restrict I = Matroid.freeOn I ↔ M.Indep I
-- Lean.Compiler.IR.CompilerM
Lean.IR.Log.toString : Lean.IR.Log → String
-- Mathlib.Order.Max
isBot_toDual_iff : ∀ {α : Type u_1} [inst : LE α] {a : α}, IsBot (OrderDual.toDual a) ↔ IsTop a
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.image_coe_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithBot.some '' Set.Iio a = Set.Ioo ⊥ ↑a
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix : ∀ (R : Type u_1) [inst : CommRing R] (n m k : ℕ) (hn : n = m + k),
  (MvPolynomial.universalFactorizationMapPresentation R n m k hn).jacobiMatrix =
    -((Matrix.reindex (finCongr ⋯) (finCongr ⋯))
          ((Polynomial.map
                ((MvPolynomial.mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp
                    (MvPolynomial.rename Sum.inl)).toRingHom
                (Polynomial.freeMonic R m)).sylvester
            (Polynomial.map
              ((MvPolynomial.mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp
                  (MvPolynomial.rename Sum.inr)).toRingHom
              (Polynomial.freeMonic R k))
            m k)).transpose
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Dist.mk : {α : Type u_3} → (α → α → ℝ) → Dist α
-- Mathlib.Algebra.Category.Grp.LeftExactFunctor
_private.Mathlib.Algebra.Category.Grp.LeftExactFunctor.0.AddCommGrpCat.leftExactFunctorForgetEquivalence.instBraidedCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C] → CategoryTheory.BraidedCategory C
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobject_arrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f).hom
      (CategoryTheory.Limits.kernel.ι f) =
    (CategoryTheory.Limits.kernelSubobject f).arrow
-- Mathlib.Tactic.Sat.FromLRAT
/-- Returns `a` and `pr : reify v c a` given a nonempty clause `c`  -/
Mathlib.Tactic.Sat.buildReify.reifyClause1 : ℕ → Lean.Expr → Lean.Expr × Lean.Expr
-- Mathlib.CategoryTheory.GradedObject.Braiding
CategoryTheory.GradedObject.Monoidal.braiding_naturality_right : ∀ {I : Type u_1} [inst : AddCommMonoid I] {C : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X : CategoryTheory.GradedObject I C)
  {Y Z : CategoryTheory.GradedObject I C} [inst_3 : CategoryTheory.BraidedCategory C] [inst_4 : X.HasTensor Y]
  [inst_5 : Y.HasTensor X] [inst_6 : X.HasTensor Z] [inst_7 : Z.HasTensor X] (f : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.whiskerLeft X f)
      (CategoryTheory.GradedObject.Monoidal.braiding X Z).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.braiding X Y).hom
      (CategoryTheory.GradedObject.Monoidal.whiskerRight f X)
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.rootForm_self_eq_zero_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [inst_4 : LinearOrder R] [IsStrictOrderedRing R] [inst_6 : Module R M]
  [inst_7 : Module R N] (P : RootPairing ι R M N) {x : M}, (P.RootForm x) x = 0 ↔ x ∈ LinearMap.ker P.RootForm
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instTop : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → Top (LieSubmodule R L M)
-- Mathlib.Algebra.CharP.Two
CharTwo.range_intCast : ∀ {R : Type u_1} [inst : Ring R] [CharP R 2], Set.range Int.cast = {0, 1}
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_41 : HAdd Std.Time.Week.Offset Std.Time.Day.Offset Std.Time.Day.Offset
-- Mathlib.Algebra.Group.Conj
AddConjClasses.instDecidableEqOfDecidableRelIsAddConj : {α : Type u} → [inst : AddMonoid α] → [DecidableRel IsAddConj] → DecidableEq (AddConjClasses α)
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
/-- Internal iterator combinator that is used to implement all `flatMap` variants
 -/
_private.Init.Data.Iterators.Combinators.Monadic.FlatMap.0.Std.IterM.flattenAfter : {α α₂ β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [Std.Iterator α m (Std.IterM m β)] →
        [Std.Iterator α₂ m β] → Std.IterM m (Std.IterM m β) → Option (Std.IterM m β) → Std.IterM m β
-- Mathlib.Algebra.Group.Shrink
Shrink.instIsRightCancelAdd : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Add α] [IsRightCancelAdd α], IsRightCancelAdd (Shrink.{v, u_2} α)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.brecOn.eq : ∀ {motive_1 : Lean.Meta.Grind.AC.DiseqCnstr → Sort u} {motive_2 : Lean.Meta.Grind.AC.DiseqCnstrProof → Sort u}
  (t : Lean.Meta.Grind.AC.DiseqCnstrProof) (F_1 : (t : Lean.Meta.Grind.AC.DiseqCnstr) → t.below → motive_1 t)
  (F_2 : (t : Lean.Meta.Grind.AC.DiseqCnstrProof) → t.below → motive_2 t),
  t.brecOn F_1 F_2 = F_2 t (Lean.Meta.Grind.AC.DiseqCnstrProof.brecOn.go t F_1 F_2).2
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.variance_linearMap_gaussianReal : ∀ {μ : ℝ} {v : NNReal} (L : ℝ →ₗ[ℝ] ℝ),
  ProbabilityTheory.variance (⇑L) (ProbabilityTheory.gaussianReal μ v) = ↑(L 1 ^ 2).toNNReal * ↑v
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.mk.sizeOf_spec : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : SizeOf R]
  [inst_4 : SizeOf A] (toSubsemiring : Subsemiring A)
  (algebraMap_mem' : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring.carrier),
  sizeOf { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' } = 1 + sizeOf toSubsemiring
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
CochainComplex.homologyMap_exact₂_of_distTriang : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ))
  (hT : DerivedCategory.Q.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n : ℤ),
  { X₁ := HomologicalComplex.homology T.obj₁ n, X₂ := HomologicalComplex.homology T.obj₂ n,
      X₃ := HomologicalComplex.homology T.obj₃ n, f := HomologicalComplex.homologyMap T.mor₁ n,
      g := HomologicalComplex.homologyMap T.mor₂ n, zero := ⋯ }.Exact
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The underlying object in the ambient category  -/
CategoryTheory.Mod.X : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {A : C} → [inst_4 : CategoryTheory.MonObj A] → CategoryTheory.Mod D A → D
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.measureReal_prod_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] (s : Set α) (t : Set β),
  (μ.prod ν).real (s ×ˢ t) = μ.real s * ν.real t
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.tensorHom_def : ∀ {X₁ Y₁ X₂ Y₂ : SFinKer} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f g =
    CategoryTheory.CategoryStruct.comp
      ((fun {X₁ X₂} κ Y => { hom := κ.hom.parallelComp ProbabilityTheory.Kernel.id, property := ⋯ }) f X₂)
      ((fun X Y₁ Y₂ κ => { hom := ProbabilityTheory.Kernel.id.parallelComp κ.hom, property := ⋯ }) Y₁ X₂ Y₂ g)
-- Mathlib.Algebra.Star.Basic
RingHom.star_def : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : StarRing R] {S : Type u_1} [inst_2 : NonAssocSemiring S] (f : S →+* R),
  star f = (starRingEnd R).comp f
-- Init.Data.BitVec.Lemmas
BitVec.toNat_umod : ∀ {n : ℕ} {x y : BitVec n}, (x % y).toNat = x.toNat % y.toNat
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.objUp_objDown : ∀ {C : Type u_1} (A : CategoryTheory.ULiftHom C), CategoryTheory.ULiftHom.objUp A.objDown = A
-- Mathlib.Data.Num.ZNum
ZNum.cast_bit1 : ∀ {α : Type u_1} [inst : AddGroupWithOne α] (n : ZNum), ↑n.bit1 = ↑n + ↑n + 1
-- Mathlib.Analysis.Normed.Ring.Basic
eventually_norm_pow_le : ∀ {α : Type u_2} [inst : SeminormedRing α] (a : α), ∀ᶠ (n : ℕ) in Filter.atTop, ‖a ^ n‖ ≤ ‖a‖ ^ n
-- Mathlib.GroupTheory.Torsion
/-- The image of a surjective torsion additive group homomorphism is torsion.  -/
IsAddTorsion.of_surjective : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] {f : G →+ H},
  Function.Surjective ⇑f → IsAddTorsion G → IsAddTorsion H
-- Mathlib.SetTheory.Cardinal.Free
Cardinal.mk_freeAbelianGroup : ∀ (α : Type u) [Nonempty α], Cardinal.mk (FreeAbelianGroup α) = max (Cardinal.mk α) Cardinal.aleph0
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.isEmbedding_of_pullback : ∀ {X Y S : TopCat} {f : X ⟶ S} {g : Y ⟶ S},
  Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f) →
    Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom g) →
      Topology.IsEmbedding
        ⇑(CategoryTheory.ConcreteCategory.hom
            (CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.one))
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.Batteries.AssocList.foldlM.match_1.eq_2 : ∀ {δ : Type u_4} {α : Type u_1} {β : Type u_2} (motive : δ → Batteries.AssocList α β → Sort u_3) (d : δ) (a : α) (b : β)
  (es : Batteries.AssocList α β) (h_1 : (d : δ) → motive d Batteries.AssocList.nil)
  (h_2 : (d : δ) → (a : α) → (b : β) → (es : Batteries.AssocList α β) → motive d (Batteries.AssocList.cons a b es)),
  (match d, Batteries.AssocList.cons a b es with
    | d, Batteries.AssocList.nil => h_1 d
    | d, Batteries.AssocList.cons a b es => h_2 d a b es) =
    h_2 d a b es
-- Mathlib.Algebra.Group.InjSurj
/-- A type has cancellative addition, if it admits an injective map that
preserves `+` to another type with cancellative addition.  -/
Function.Injective.isCancelAdd : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst_1 : Add M₂] [IsCancelAdd M₂] (f : M₁ → M₂),
  Function.Injective f → (∀ (x y : M₁), f (x + y) = f x + f y) → IsCancelAdd M₁
-- Lean.Util.FindMVar
Lean.FindMVar.visit : (Lean.MVarId → Bool) → Lean.Expr → Lean.FindMVar.Visitor