mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.sub_apply : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (f g : M →ₗ⁅R,L⁆ N) (m : M), (f - g) m = f m - g m
-- Mathlib.Topology.Constructions
Filter.Tendsto.update : ∀ {Y : Type v} {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] [inst : DecidableEq ι]
  {l : Filter Y} {f : Y → (i : ι) → A i} {x : (i : ι) → A i},
  Filter.Tendsto f l (nhds x) →
    ∀ (i : ι) {g : Y → A i} {xi : A i},
      Filter.Tendsto g l (nhds xi) →
        Filter.Tendsto (fun a => Function.update (f a) i (g a)) l (nhds (Function.update x i xi))
-- Mathlib.Algebra.Category.MonCat.Colimits
_private.Mathlib.Algebra.Category.MonCat.Colimits.0.MonCat.Colimits.descFunLift.match_1.splitter : {J : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} J] →
    (F : CategoryTheory.Functor J MonCat) →
      (motive : MonCat.Colimits.Prequotient F → Sort u_3) →
        (x : MonCat.Colimits.Prequotient F) →
          ((j : J) → (x : ↑(F.obj j)) → motive (MonCat.Colimits.Prequotient.of j x)) →
            (Unit → motive MonCat.Colimits.Prequotient.one) →
              ((x y : MonCat.Colimits.Prequotient F) → motive (x.mul y)) → motive x
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientAddGroup.dense_image_mk : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] {N : AddSubgroup G}
  {s : Set G}, Dense (QuotientAddGroup.mk '' s) ↔ Dense (s + ↑N)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.isIso_cyclesMap'_of_isIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.IsIso φ] (h₁ : S₁.LeftHomologyData)
  (h₂ : S₂.LeftHomologyData), CategoryTheory.IsIso (CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂)
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquivClass.toAlgEquivClass : ∀ {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] [inst_7 : EquivLike F A B] [BialgEquivClass F R A B], AlgEquivClass F R A B
-- Mathlib.Algebra.Algebra.RestrictScalars
instCommSemiringRestrictScalars : (R : Type u_1) → (S : Type u_2) → (A : Type u_4) → [I : CommSemiring A] → CommSemiring (RestrictScalars R S A)
-- Mathlib.Analysis.Calculus.VectorField
VectorField.pullbackWithin_univ : ∀ {𝕜 : 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 : E → F}
  {V : F → F}, VectorField.pullbackWithin 𝕜 f V Set.univ = VectorField.pullback 𝕜 f V
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.keys_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Bool} (h : (↑m).WF),
  (↑(Std.DHashMap.Internal.Raw₀.filter f m)).keys.Perm
    (List.filter
        (fun x =>
          match x with
          | ⟨x, h'⟩ => f x (Std.DHashMap.Internal.Raw₀.Const.get m x ⋯))
        (↑m).keys.attach).unattach
-- Mathlib.CategoryTheory.Limits.Shapes.Equivalence
CategoryTheory.Equivalence.hasTerminal_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), CategoryTheory.Limits.HasTerminal C ↔ CategoryTheory.Limits.HasTerminal D
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.limitConeComp_cone : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.LimitCone G),
  (CategoryTheory.Functor.Initial.limitConeComp F t).cone = CategoryTheory.Limits.Cone.whisker F t.cone
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Without this lemma, `limit.hom_ext` would be applied, but the goal would involve terms
in `Discrete β` rather than `β` itself.  -/
CategoryTheory.Limits.Sigma.hom_ext : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] {X : C} (g₁ g₂ : ∐ f ⟶ X),
  (∀ (b : β),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) g₁ =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) g₂) →
    g₁ = g₂
-- Lean.Data.PersistentArray
Lean.PersistentArray.tailOff : {α : Type u} → Lean.PersistentArray α → ℕ
-- Mathlib.RingTheory.Coalgebra.Quotient
Coalgebra.Quotient.instCoalgebraStructQuotientSubmodule : {R : Type u_1} →
  {C : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup C] →
        [inst_2 : Module R C] →
          [inst_3 : CoalgebraStruct R C] → (I : Submodule R C) → [I.IsCoideal] → CoalgebraStruct R (C ⧸ I)
-- Mathlib.Algebra.Module.Submodule.LinearMap
LinearMap.restrict_eq_domRestrict_codRestrict : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {f : M →ₛₗ[σ₁₂] M₂} {p : Submodule R M} {q : Submodule R₂ M₂} (hf : ∀ (x : M), f x ∈ q),
  f.restrict ⋯ = (LinearMap.codRestrict q f hf).domRestrict p
-- Lean.Meta.Tactic.Delta
/-- Low-level delta expansion. It is used to implement equation lemmas and elimination principles for recursive definitions.  -/
Lean.Meta.deltaExpand : Lean.Expr → (Lean.Name → Bool) → optParam Bool false → Lean.CoreM Lean.Expr
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.verify₃_eq_isSome_assemble₃ : ∀ {w x y : UInt8}, ByteArray.utf8DecodeChar?.verify₃ w x y = (ByteArray.utf8DecodeChar?.assemble₃ w x y).isSome
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.currying₃_unitIso_hom_app_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (X₁ : C₁) (X₂ : C₂)
  (X₃ : C₃),
  (((CategoryTheory.Functor.currying₃.unitIso.hom.app F).app X₁).app X₂).app X₃ =
    CategoryTheory.CategoryStruct.id
      (((((CategoryTheory.Functor.id
                        (CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E)))).obj
                    F).obj
                X₁).obj
            X₂).obj
        X₃)
-- Init.Data.Array.Lemmas
Array.set_comm : ∀ {α : Type u_1} (a b : α) {i j : ℕ} {xs : Array α} {hi : i < xs.size} {hj : j < (xs.set i a hi).size},
  i ≠ j → (xs.set i a hi).set j b hj = (xs.set j b ⋯).set i a ⋯
-- Mathlib.Algebra.Group.Basic
add_neg_add_add_cancel : ∀ {G : Type u_3} [inst : AddGroup G] (a b c : G), a + -b + (b + c) = a + c
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
/-- If ring `S` acts on a ring `R` and `M` is a module over both (compatibly with this action) then
we can turn an `R`-submodule into an `S`-submodule by forgetting the action of `R`.  -/
Submodule.restrictScalarsLatticeHom : (S : Type u_1) →
  (R : Type u_2) →
    (M : Type u_3) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Semiring S] →
            [inst_3 : Module S M] →
              [inst_4 : Module R M] →
                [inst_5 : SMul S R] → [IsScalarTower S R M] → CompleteLatticeHom (Submodule R M) (Submodule S M)
-- Mathlib.Order.Filter.CardinalInter
CardinalInterFilter.of_cardinalInterFilter_of_lt : ∀ {α : Type u} {c : Cardinal.{u}} (l : Filter α) [CardinalInterFilter l c] {a : Cardinal.{u}},
  a < c → CardinalInterFilter l a
-- Mathlib.Tactic.ClickSuggestions.Util
/-- The current document  -/
Mathlib.Tactic.ClickSuggestions.Context.meta : Mathlib.Tactic.ClickSuggestions.Context → Lean.Server.DocumentMeta
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.CohomologyClass.mk_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ}, Function.Surjective CochainComplex.HomComplex.CohomologyClass.mk
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.stabilizer_smul_eq_left : ∀ {G : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MulAction G β]
  [inst_3 : SMul α β] [IsScalarTower G α β] (a : α) (b : β),
  (Function.Injective fun x => x • b) → MulAction.stabilizer G (a • b) = MulAction.stabilizer G a
-- Mathlib.ModelTheory.Basic
/-- Given a language with a nonempty type of constants, any structure will be nonempty. This cannot
be a global instance, because `L` becomes a metavariable.  -/
FirstOrder.Language.nonempty_of_nonempty_constants : ∀ (L : FirstOrder.Language) (M : Type w) [L.Structure M] [h : Nonempty L.Constants], Nonempty M
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Return the minimum element of the tree, if it exists.

```
findMin {1, 2, 3} = some 1
findMin ∅ = none
```  -/
Ordnode.findMin : {α : Type u_1} → Ordnode α → Option α
-- Mathlib.CategoryTheory.Monad.Algebra
/-- An Eilenberg-Moore algebra for a monad `T`.
cf Definition 5.2.3 in [Riehl][riehl2017].  -/
CategoryTheory.Monad.Algebra : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Monad C → Type (max u₁ v₁)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.prevn.eq_1 : ∀ (x : String.Legacy.Iterator), x.prevn 0 = x
-- Mathlib.Topology.Order.LeftRightLim
Monotone.rightLim_eq_sInf : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Monotone f →
    ∀ {x : α} [inst_4 : TopologicalSpace α] [OrderTopology α] [(nhdsWithin x (Set.Ioi x)).NeBot],
      Function.rightLim f x = sInf (f '' Set.Ioi x)
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
ContMDiffVectorBundle.mk : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8}
  [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)]
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_11 : (x : B) → TopologicalSpace (E x)] [inst_12 : FiberBundle F E] [inst_13 : VectorBundle 𝕜 F E],
  (∀ (e e' : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_14 : MemTrivializationAtlas e]
      [inst_15 : MemTrivializationAtlas e'],
      ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun b => ↑(Bundle.Trivialization.coordChangeL 𝕜 e e' b))
        (e.baseSet ∩ e'.baseSet)) →
    ContMDiffVectorBundle n F E IB
-- Mathlib.CategoryTheory.Category.Cat.Adjunction
_private.Mathlib.CategoryTheory.Category.Cat.Adjunction.0.CategoryTheory.Cat.typeToCatObjectsAdjHomEquiv : (X : Type u) → (C : CategoryTheory.Cat) → (CategoryTheory.typeToCat.obj X ⟶ C) ≃ (X ⟶ CategoryTheory.Cat.objects.obj C)
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.mk.injEq : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (toPrepartition : BoxIntegral.Prepartition I) (tag : BoxIntegral.Box ι → ι → ℝ)
  (tag_mem_Icc : ∀ (J : BoxIntegral.Box ι), tag J ∈ BoxIntegral.Box.Icc I)
  (toPrepartition_1 : BoxIntegral.Prepartition I) (tag_1 : BoxIntegral.Box ι → ι → ℝ)
  (tag_mem_Icc_1 : ∀ (J : BoxIntegral.Box ι), tag_1 J ∈ BoxIntegral.Box.Icc I),
  ({ toPrepartition := toPrepartition, tag := tag, tag_mem_Icc := tag_mem_Icc } =
      { toPrepartition := toPrepartition_1, tag := tag_1, tag_mem_Icc := tag_mem_Icc_1 }) =
    (toPrepartition = toPrepartition_1 ∧ tag = tag_1)
-- Mathlib.Control.Traversable.Instances
_private.Mathlib.Control.Traversable.Instances.0.Sum.traverse.match_1.eq_2 : ∀ {σ : Type u_1} {α : Type u_2} (motive : σ ⊕ α → Sort u_3) (x : α) (h_1 : (x : σ) → motive (Sum.inl x))
  (h_2 : (x : α) → motive (Sum.inr x)),
  (match Sum.inr x with
    | Sum.inl x => h_1 x
    | Sum.inr x => h_2 x) =
    h_2 x
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.univ_pow : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] {n : ℕ} [inst_2 : Fintype α],
  n ≠ 0 → Finset.univ ^ n = Finset.univ
-- Std.Http.Server.Config
/-- Whether to enable keep-alive connections by default.
 -/
Std.Http.Config.enableKeepAlive : Std.Http.Config → Bool
-- Lean.Meta.Tactic.Grind.EMatch
/-- Process choice stack until we don't have more choices to be processed.  -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.processChoices : Lean.Meta.Grind.EMatch.M Unit
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.bitblast.goCache.eq_def : ∀ {w : ℕ} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (expr : Std.Tactic.BVDecide.BVExpr w)
  (cache : Std.Tactic.BVDecide.BVExpr.Cache aig),
  Std.Tactic.BVDecide.BVExpr.bitblast.goCache aig expr cache =
    match cache.get? expr with
    | some vec => { result := ⟨{ aig := aig, vec := vec }, ⋯⟩, cache := cache }
    | none =>
      match Std.Tactic.BVDecide.BVExpr.bitblast.go aig expr cache with
      | { result := result, cache := cache } => { result := result, cache := cache.insert expr (↑result).vec }
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_sub_cancel_right : ∀ {a b : ENNReal}, b ≠ ⊤ → a + b - b = a
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.fold_mapM : ∀ {α β γ δ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : MonadAttach n] [WeaklyLawfulMonadAttach n]
  [inst_5 : Std.Internal.Do.Assertion Pred] [inst_6 : Std.Internal.Do.Assertion EPred]
  [inst_7 : Std.Internal.Do.WPMonad n Pred EPred] [inst_8 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n]
  {f : β → n γ} {g : δ → γ → δ} {init : δ} {it : Std.Iter β} {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.Iter.foldM
        (fun d b => do
          let c ← f b
          pure (g d c))
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.fold g init (Std.Iter.mapM f it) ⦃ Q; eQ ⦄
-- Mathlib.RingTheory.FractionalIdeal.Basic
/-- The fractional ideals of a Noetherian ring are finitely generated.  -/
FractionalIdeal.fg_of_isNoetherianRing : ∀ {R : Type u_3} [inst : CommRing R] [IsDomain R] {S : Submonoid R} {P : Type u_4} [Nontrivial P] [inst_3 : CommRing P]
  [inst_4 : Algebra R P] [Module.IsTorsionFree R P] [hR : IsNoetherianRing R],
  S ≤ nonZeroDivisors R → ∀ (I : FractionalIdeal S P), (↑I).FG
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- Additive closure of an additive subgroup `K` equals `K`  -/
AddSubgroup.closure_eq : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G), AddSubgroup.closure ↑K = K
-- Mathlib.FieldTheory.AbelRuffini
gal_X_pow_sub_C_isSolvable : ∀ {F : Type u_1} [inst : Field F] (n : ℕ) (x : F), Group.IsSolvable (Polynomial.X ^ n - Polynomial.C x).Gal
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
/-- The arrow isomorphism `(∅ ⟶ W) ⋔ (f : A ⟶ B) ≅ (W ⟹ A ⟶ W ⟹ B)` in a braided CCC with
pullbacks and an initial object.  -/
CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isInitialIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      [inst_2 : CategoryTheory.CartesianMonoidalCategory C] →
        [inst_3 : CategoryTheory.MonoidalClosed C] →
          [CategoryTheory.BraidedCategory C] →
            (X : CategoryTheory.Arrow C) →
              {I : C} →
                (i : CategoryTheory.Limits.IsInitial I) →
                  {W : C} →
                    (Opposite.op (CategoryTheory.Arrow.mk (i.to W)) ⋔ X) ≅
                      CategoryTheory.Arrow.mk ((CategoryTheory.ihom W).map X.hom)
-- Mathlib.MeasureTheory.Group.Arithmetic
measurable_mul_unop : ∀ {α : Type u_2} [inst : MeasurableSpace α], Measurable MulOpposite.unop
-- Init.Data.List.Sort.Lemmas
List.MergeSort.Internal.splitInTwo_fst_le_splitInTwo_snd : ∀ {α : Type u_1} {n : ℕ} {le : α → α → Prop} {l : { l // l.length = n }},
  List.Pairwise le ↑l →
    ∀ (a b : α), a ∈ ↑(List.MergeSort.Internal.splitInTwo l).1 → b ∈ ↑(List.MergeSort.Internal.splitInTwo l).2 → le a b
-- Mathlib.Algebra.Tropical.Basic
Tropical.trop_add : ∀ {R : Type u} [inst : Add R] (x y : R), Tropical.trop (x + y) = Tropical.trop x * Tropical.trop y
-- Mathlib.Logic.Denumerable
nonempty_denumerable_iff : ∀ {α : Type u_3}, Nonempty (Denumerable α) ↔ Countable α ∧ Infinite α
-- Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
/-- The canonical embedding of this small category to the canonical (large) category
`FGModuleCat R`.  -/
FGModuleRepr.embed : (R : Type u) → [inst : Ring R] → CategoryTheory.Functor (FGModuleRepr R) (FGModuleCat R)
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthSup_add : ∀ {u v : ℕ → ENNReal}, ExpGrowth.expGrowthSup (u + v) = max (ExpGrowth.expGrowthSup u) (ExpGrowth.expGrowthSup v)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pos_and_pos_or_neg_and_neg_of_mul_pos : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : LinearOrder α] [PosMulMono α] [MulPosMono α],
  0 < a * b → 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
-- Mathlib.Order.WellFoundedSet
Set.isPWO_of_wellQuasiOrderedLE : ∀ {α : Type u_2} [inst : Preorder α] [h : WellQuasiOrderedLE α] (s : Set α), s.IsPWO
-- Mathlib.Data.Set.Lattice.Image
Set.kernImage_preimage_union : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β},
  Set.kernImage f (f ⁻¹' t ∪ s) = t ∪ Set.kernImage f s
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
_private.Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass.0.CategoryTheory.ShortComplex.ShortExact.termS' : Lean.ParserDescr
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {a : α}, m.contains a = false → m.getKey! a = default
-- Init.Data.List.Nat.TakeDrop
List.getElem?_drop : ∀ {α : Type u_1} {xs : List α} {i j : ℕ}, (List.drop i xs)[j]? = xs[i + j]?
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trNum_natEnd : ∀ (n : Num), ∀ x ∈ Turing.PartrecToTM2.trNum n, Turing.PartrecToTM2.natEnd x = false
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.mk.injEq : ∀ {ι : Type u_3} {M : Type u_4} [inst : AddCommMonoid M] {I : WithTop (BoxIntegral.Box ι)}
  (toFun : BoxIntegral.Box ι → M)
  (sum_partition_boxes' :
    ∀ (J : BoxIntegral.Box ι),
      ↑J ≤ I → ∀ (π : BoxIntegral.Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, toFun Ji = toFun J)
  (toFun_1 : BoxIntegral.Box ι → M)
  (sum_partition_boxes'_1 :
    ∀ (J : BoxIntegral.Box ι),
      ↑J ≤ I → ∀ (π : BoxIntegral.Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, toFun_1 Ji = toFun_1 J),
  ({ toFun := toFun, sum_partition_boxes' := sum_partition_boxes' } =
      { toFun := toFun_1, sum_partition_boxes' := sum_partition_boxes'_1 }) =
    (toFun = toFun_1)
-- Lean.Elab.App
Lean.Elab.Term.LValResolution.localRec.sizeOf_spec : ∀ (baseName : Lean.Name) (fvar : Lean.Expr),
  sizeOf (Lean.Elab.Term.LValResolution.localRec baseName fvar) = 1 + sizeOf baseName + sizeOf fvar
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
Filter.Tendsto.uniformity_neg_iff : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {f : ι → α × α}
  {l : Filter ι}, Filter.Tendsto (-f) l (uniformity α) ↔ Filter.Tendsto f l (uniformity α)
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.adjMatrix_hadamard_intCast : ∀ (α : Type u_1) {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : DecidableEq V]
  [inst_2 : MulZeroOneClass α] [inst_3 : IntCast α] (a : ℤ), (SimpleGraph.adjMatrix α G).hadamard ↑a = 0
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.isSupportedOutside₁_iff : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c},
  e₁.AreComplementary e₂ → ∀ (K : HomologicalComplex C c), K.IsSupportedOutside e₁ ↔ K.IsSupported e₂
-- Mathlib.Algebra.Lie.CartanSubalgebra
LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (H : LieSubalgebra R L)
  [H.IsCartanSubalgebra], LieRing.IsNilpotent ↥H
-- Mathlib.Data.Fin.SuccPred
Fin.succ_castPred_eq_castPred_succ : ∀ {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ Fin.last n) (ha' : optParam (a.succ ≠ Fin.last (n + 1)) ⋯),
  (a.castPred ha).succ = a.succ.castPred ha'
-- Mathlib.Algebra.Colimit.Ring
Ring.DirectLimit.ringEquiv.eq_1 : ∀ {ι : Type u_1} [inst : Preorder ι] (G : ι → Type u_2) [inst_1 : (i : ι) → CommRing (G i)]
  (f' : (i j : ι) → i ≤ j → G i →+* G j) [inst_2 : DirectedSystem G fun i j h => ⇑(f' i j h)]
  [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι],
  Ring.DirectLimit.ringEquiv G f' =
    RingEquiv.ofRingHom
      (Ring.DirectLimit.lift G (fun x1 x2 x3 => ⇑(f' x1 x2 x3)) (DirectLimit G f') (DirectLimit.Ring.of G f') ⋯)
      (DirectLimit.Ring.lift G f' (Ring.DirectLimit G fun x1 x2 x3 => ⇑(f' x1 x2 x3))
        (Ring.DirectLimit.of G fun x1 x2 x3 => ⇑(f' x1 x2 x3)) ⋯)
      ⋯ ⋯
-- Mathlib.Data.List.SplitBy
_private.Mathlib.Data.List.SplitBy.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- The canonical `S`-algebra projection `TrivSqZeroExt R M → R`.  -/
TrivSqZeroExt.fstHom : (S : Type u_1) →
  (R : Type u) →
    (M : Type v) →
      [inst : CommSemiring S] →
        [inst_1 : Semiring R] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Algebra S R] →
              [inst_4 : Module S M] →
                [inst_5 : Module R M] →
                  [inst_6 : Module Rᵐᵒᵖ M] →
                    [inst_7 : SMulCommClass R Rᵐᵒᵖ M] →
                      [inst_8 : IsScalarTower S R M] → [inst_9 : IsScalarTower S Rᵐᵒᵖ M] → TrivSqZeroExt R M →ₐ[S] R
-- Mathlib.Topology.Sober
coe_irreducibleEquivPoints_symm_apply : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : QuasiSober α] [inst_2 : T0Space α] (x : α),
  ↑(irreducibleSetEquivPoints.symm x) = closure {x}
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.not_inseparable_coe_infty : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X}, ¬Inseparable (↑x) OnePoint.infty
-- Aesop.Frontend.Attribute
Aesop.Frontend.instInhabitedAttrConfig.default : Aesop.Frontend.AttrConfig
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
/-- An auxiliary lemma en route to `RootPairing.Base.lie_e_f_ne`.  -/
_private.Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations.0.RootPairing.GeckConstruction.lie_e_f_ne_aux₁ : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : IsDomain R] [inst_3 : CharZero R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {b : P.Base} [inst_9 : Fintype ι]
  {i j : ↥b.support},
  i ≠ j → ⁅RootPairing.GeckConstruction.e i, RootPairing.GeckConstruction.f j⁆.transpose (Sum.inr ↑j) = 0