mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.EuclideanDist
toEuclidean.congr_simp : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : T2Space E] [inst_4 : Module ℝ E] [inst_5 : ContinuousSMul ℝ E] [inst_6 : FiniteDimensional ℝ E],
  toEuclidean = toEuclidean
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
sq_nonpos_iff : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R]
  [NoZeroDivisors R] (r : R), r ^ 2 ≤ 0 ↔ r = 0
-- Init.Tactics
/-- `ac_rfl` proves equalities up to application of an associative and commutative operator.
```
instance : Std.Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩
instance : Std.Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩

example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by ac_rfl
```
 -/
Lean.Parser.Tactic.acRfl : Lean.ParserDescr
-- Init.Grind.Config
/-- If `etaStruct` is `true`, then for each term `t : S` such that `S` is a structure,
and is tagged with `[grind ext]`, `grind` adds the equation `t = ⟨t.1, ..., t.n⟩`
which holds by reflexivity. Moreover, the extensionality theorem for `S` is not used.
 -/
Lean.Grind.Config.etaStruct : Lean.Grind.Config → Bool
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.σ₀Iter_σ' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (i : ℕ) {n m : ℕ}
  (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : autoParam (n + i = m) CategoryTheory.SimplicialObject.σ₀Iter_σ'._auto_1),
  autoParam (↑j = ↑j' + i) CategoryTheory.SimplicialObject.σ₀Iter_σ'._auto_3 →
    CategoryTheory.CategoryStruct.comp (X.σ₀Iter i hi) (X.σ j) =
      CategoryTheory.CategoryStruct.comp (X.σ j') (X.σ₀Iter i ⋯)
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  (k : α) (f : Option β → Option β), m₁.Equiv m₂ → (m₁.alter k f).Equiv (m₂.alter k f)
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.IsCycles.reachable_sdiff_toSubgraph_spanningCoe : ∀ {V : Type u_1} {G : SimpleGraph V} [Finite V] {v w : V},
  G.IsCycles → ∀ (p : G.Walk v w), p.IsPath → (G \ p.toSubgraph.spanningCoe).Reachable w v
-- Mathlib.Data.TypeVec
TypeVec.typevecCasesNil₂_appendFun : ∀ {β : TypeVec.Arrow Fin2.elim0 Fin2.elim0 → Sort u_1} (f : β TypeVec.nilFun),
  TypeVec.typevecCasesNil₂ f TypeVec.nilFun = f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.insertMany_list_equiv_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ : Std.DTreeMap α (fun x => β) cmp} {l : List (α × β)},
  (Std.DTreeMap.Const.insertMany t₁ l).Equiv (List.foldl (fun acc p => acc.insert p.1 p.2) t₁ l)
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.coe_injective : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  Function.Injective SetLike.coe
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.comp_eqToHom_heq_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z Z' : C} (f : X ⟶ Y) (g : Z ⟶ Z') (h : Y = W),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom h) ≍ g ↔ f ≍ g
-- Mathlib.Data.Analysis.Filter
/-- A filter realizes itself.  -/
Filter.Realizer.ofFilter : {α : Type u_1} → (f : Filter α) → f.Realizer
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- The degree of `cyclotomic n R` is positive.  -/
Polynomial.degree_cyclotomic_pos : ∀ (n : ℕ) (R : Type u_1), 0 < n → ∀ [inst : Ring R] [Nontrivial R], 0 < (Polynomial.cyclotomic n R).degree
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyι_comp_fromOpcycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [inst_2 : K.HasHomology i],
  CategoryTheory.CategoryStruct.comp (K.homologyι i) (K.fromOpcycles i j) = 0
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.RelevantArg.noArg.sizeOf_spec : sizeOf Mathlib.Tactic.Translate.RelevantArg.noArg = 1
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nontrivial.add_right : ∀ {α : Type u_2} [inst : Add α] [IsRightCancelAdd α] {s t : Set α}, s.Nontrivial → t.Nonempty → (s + t).Nontrivial
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
FreeMonoid.equivWithOneFreeSemigroup.eq_1 : ∀ {α : Type u_1},
  FreeMonoid.equivWithOneFreeSemigroup =
    { toFun := ⇑(FreeMonoid.lift fun x => ↑(FreeSemigroup.of x)), invFun := ⇑(WithOne.lift FreeSemigroup.toFreeMonoid),
      left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.mem_top : ∀ {R : Type u} [inst : NonAssocRing R] (x : R), x ∈ ⊤
-- Mathlib.Topology.Sheaves.Abelian
TopCat.Sheaf.instAdditivePresheafForget : ∀ {X : TopCat} {C : Type v₁} [inst : CategoryTheory.Category.{v₂, v₁} C]
  [inst_1 : CategoryTheory.HasSheafify (Opens.grothendieckTopology ↑X) C] [inst_2 : CategoryTheory.Abelian C],
  (TopCat.Sheaf.forget C X).Additive
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.IntroResult : Type
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.rootLength_reflectionPerm_self : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S 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.IsValuedIn S]
  (B : RootPairing.RootPositiveForm S P) [inst_9 : FaithfulSMul S R] [inst_10 : Module S M]
  [inst_11 : IsScalarTower S R M] (i : ι), B.rootLength ((P.reflectionPerm i) i) = B.rootLength i
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.inv_smul_finset_distrib₀ : ∀ {α : Type u_1} [inst : GroupWithZero α] [inst_1 : DecidableEq α] (a : α) (s : Finset α),
  (a • s)⁻¹ = MulOpposite.op a⁻¹ • s⁻¹
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk_jointly_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  {N : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} N] {p : CategoryTheory.Functor N C}
  [inst_3 : CategoryTheory.InitiallySmall N] {X : C}
  (x : (CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiber p).obj X),
  ∃ U f, CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk f = x
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.ext : ∀ {R : Type u} {M : Type v} {x y : TrivSqZeroExt R M}, x.fst = y.fst → x.snd = y.snd → x = y
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.Wedge.IsLimit.lift_ι : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} {c : CategoryTheory.Limits.Wedge F}
  (hc : CategoryTheory.Limits.IsLimit c) {X : C} (f : (j : J) → X ⟶ (F.obj (Opposite.op j)).obj j)
  (hf :
    ∀ ⦃i j : J⦄ (g : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) =
        CategoryTheory.CategoryStruct.comp (f j) ((F.map g.op).app j))
  (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Wedge.IsLimit.lift hc f hf)
      (CategoryTheory.Limits.Multifork.ι c j) =
    f j
-- Init.Data.SInt.Lemmas
Int64.toInt64_toUInt64 : ∀ (x : Int64), x.toUInt64.toInt64 = x
-- Lean.Util.FindLevelMVar
Lean.FindLevelMVar.visitLevel : (Lean.LMVarId → Bool) → Lean.Level → Lean.FindLevelMVar.Visitor
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The continuous homomorphism given by projection onto the second factor.  -/
ContinuousMonoidHom.snd : (A : Type u_2) →
  (B : Type u_3) →
    [inst : Monoid A] →
      [inst_1 : Monoid B] → [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → A × B →ₜ* B
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGE.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k k_1 : α) (e_k : k = k_1)
  (t t_1 : Std.DTreeMap.Internal.Impl α β) (e_t : t = t_1) (ho : t.Ordered) (he : ∃ a ∈ t, (compare a k).isGE = true),
  Std.DTreeMap.Internal.Impl.getEntryGE k t ho he = Std.DTreeMap.Internal.Impl.getEntryGE k_1 t_1 ⋯ ⋯
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.valueGroup₀Fun.eq_1 : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : LinearOrderedCommGroupWithZero Γ₀]
  [inst_1 : LinearOrderedCommGroupWithZero Γ'₀] [inst_2 : Ring R] {v : Valuation R Γ₀} {w : Valuation R Γ'₀}
  (h : v.IsEquiv w) (x : (MonoidWithZeroHom.ofClass v).ValueGroup₀),
  h.valueGroup₀Fun x =
    if hx : x = 0 then 0
    else ↑(MonoidWithZeroHom.valueGroup.mk (MonoidWithZeroHom.ofClass w) (↑⋯.choose).1 (↑⋯.choose).2 ⋯ ⋯)
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of `SimpleGraph.Walk.isPath_mapLe`. -/
SimpleGraph.Walk.mapLe_isPath : ∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v},
  (SimpleGraph.Walk.mapLe h p).IsPath ↔ p.IsPath
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.isZero_zero : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C],
  CategoryTheory.Limits.IsZero 0
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y : C} (f : W.LeftFraction X Y),
  CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk f =
    f.map (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W) ⋯
-- Mathlib.RingTheory.FiniteType
/-- If a set `S` generates an additive monoid `M`, then the image of `M` generates, as algebra,
`R[M]`.  -/
AddMonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure : ∀ {R : Type u_1} {M : Type u_2} [inst : AddMonoid M] [inst_1 : CommSemiring R] {S : Set M},
  AddSubmonoid.closure S = ⊤ → Function.Surjective ⇑((FreeAlgebra.lift R) fun s => AddMonoidAlgebra.of' R M ↑s)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {v : β k} {h₁ : a ∈ t.insert k v}, (t.insert k v).getKey a h₁ = if h₂ : cmp k a = Ordering.eq then k else t.getKey a ⋯
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_snd : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i).inv
      (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i)) =
    CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g
-- Lean.Expr
Lean.Nat.mkInstHMod : Lean.Expr
-- Mathlib.Algebra.Lie.Semisimple.Defs
/-- A Lie algebra *has trivial radical* if its radical is trivial.
This is equivalent to having no non-trivial solvable ideals,
and further equivalent to having no non-trivial abelian ideals.

In characteristic zero, it is also equivalent to `LieAlgebra.IsSemisimple`.

Note that the label 'semisimple' is apparently not universally agreed
[upon](https://mathoverflow.net/questions/149391/on-radicals-of-a-lie-algebra#comment383669_149391)
for general coefficients.

For example [Seligman, page 15](seligman1967) uses the label for `LieAlgebra.HasTrivialRadical`,
whereas we reserve it for Lie algebras that are a direct sum of simple Lie algebras.
 -/
LieAlgebra.HasTrivialRadical : (R : Type u_1) → (L : Type u_2) → [inst : CommRing R] → [inst_1 : LieRing L] → [LieAlgebra R L] → Prop
-- Mathlib.Algebra.Lie.IdealOperations
/-- See also `LieSubmodule.lieIdeal_oper_eq_linear_span'` and
`LieSubmodule.lieIdeal_oper_eq_tensor_map_range`.  -/
LieSubmodule.lieIdeal_oper_eq_linear_span : ∀ {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] (N : LieSubmodule R L M) [inst_5 : LieAlgebra R L]
  (I : LieIdeal R L) [LieModule R L M], ↑⁅I, N⁆ = Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
-- Mathlib.Order.WithBot
WithTop.decidableLE.eq_2 : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] (a_1 : α), WithTop.decidableLE none (some a_1) = isFalse ⋯
-- Mathlib.Data.NNReal.Basic
NNReal.finset_sup_div : ∀ {α : Type u_3} {f : α → NNReal} {s : Finset α} (r : NNReal), s.sup f / r = s.sup fun a => f a / r
-- Init.Data.List.MinMaxIdx
List.minIdxOn?_singleton : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {x : α} {f : α → β},
  List.minIdxOn? f [x] = some 0
-- Mathlib.Topology.CWComplex.Classical.Graph
Topology.CWComplex.OneSkeletonGraph.isLink_iff_pair : ∀ {X : Type u_1} [inst : TopologicalSpace X] {C : Set X} [inst_1 : Topology.CWComplex C]
  (e : Topology.RelCWComplex.cell C 1) (x y : Topology.RelCWComplex.cell C 0),
  (Topology.CWComplex.OneSkeletonGraph C).IsLink e x y ↔
    Topology.RelCWComplex.cellFrontier 1 e =
      {↑(Topology.RelCWComplex.map 0 x) ![], ↑(Topology.RelCWComplex.map 0 y) ![]}
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.toEdge.surjective : ∀ {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} (h : M.IsMatching), Function.Surjective h.toEdge
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.singleton_not_indep : ∀ {α : Type u_1} {M : Matroid α} {e : α},
  autoParam (e ∈ M.E) Matroid.singleton_not_indep._auto_1 → (¬M.Indep {e} ↔ M.IsLoop e)
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.op_toSubsemigroup : ∀ {M : Type u_2} [inst : MulOneClass M] (H : Submonoid M), H.op.toSubsemigroup = H.op
-- Lean.CoreM
Lean.Core.Context.mk.inj : ∀ {fileName : String} {fileMap : Lean.FileMap} {options : Lean.Options} {currRecDepth maxRecDepth : ℕ}
  {ref : Lean.Syntax} {currNamespace : Lean.Name} {openDecls : List Lean.OpenDecl} {initHeartbeats maxHeartbeats : ℕ}
  {quotContext : Lean.Name} {currMacroScope : Lean.MacroScope} {diag : Bool} {cancelTk? : Option IO.CancelToken}
  {suppressElabErrors : Bool} {inheritedTraceOptions : Std.HashSet Lean.Name} {fileName_1 : String}
  {fileMap_1 : Lean.FileMap} {options_1 : Lean.Options} {currRecDepth_1 maxRecDepth_1 : ℕ} {ref_1 : Lean.Syntax}
  {currNamespace_1 : Lean.Name} {openDecls_1 : List Lean.OpenDecl} {initHeartbeats_1 maxHeartbeats_1 : ℕ}
  {quotContext_1 : Lean.Name} {currMacroScope_1 : Lean.MacroScope} {diag_1 : Bool} {cancelTk?_1 : Option IO.CancelToken}
  {suppressElabErrors_1 : Bool} {inheritedTraceOptions_1 : Std.HashSet Lean.Name},
  { fileName := fileName, fileMap := fileMap, options := options, currRecDepth := currRecDepth,
        maxRecDepth := maxRecDepth, ref := ref, currNamespace := currNamespace, openDecls := openDecls,
        initHeartbeats := initHeartbeats, maxHeartbeats := maxHeartbeats, quotContext := quotContext,
        currMacroScope := currMacroScope, diag := diag, cancelTk? := cancelTk?,
        suppressElabErrors := suppressElabErrors, inheritedTraceOptions := inheritedTraceOptions } =
      { fileName := fileName_1, fileMap := fileMap_1, options := options_1, currRecDepth := currRecDepth_1,
        maxRecDepth := maxRecDepth_1, ref := ref_1, currNamespace := currNamespace_1, openDecls := openDecls_1,
        initHeartbeats := initHeartbeats_1, maxHeartbeats := maxHeartbeats_1, quotContext := quotContext_1,
        currMacroScope := currMacroScope_1, diag := diag_1, cancelTk? := cancelTk?_1,
        suppressElabErrors := suppressElabErrors_1, inheritedTraceOptions := inheritedTraceOptions_1 } →
    fileName = fileName_1 ∧
      fileMap = fileMap_1 ∧
        options = options_1 ∧
          currRecDepth = currRecDepth_1 ∧
            maxRecDepth = maxRecDepth_1 ∧
              ref = ref_1 ∧
                currNamespace = currNamespace_1 ∧
                  openDecls = openDecls_1 ∧
                    initHeartbeats = initHeartbeats_1 ∧
                      maxHeartbeats = maxHeartbeats_1 ∧
                        quotContext = quotContext_1 ∧
                          currMacroScope = currMacroScope_1 ∧
                            diag = diag_1 ∧
                              cancelTk? = cancelTk?_1 ∧
                                suppressElabErrors = suppressElabErrors_1 ∧
                                  inheritedTraceOptions = inheritedTraceOptions_1
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
IntermediateField.AdjoinDouble.normal_algebraicClosure : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {x y : L},
  IsIntegral K x → IsIntegral K y → Normal K (AlgebraicClosure ↥K⟮x, y⟯)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- `ContinuousLinearMap.toLinearMap` as a `RingHom`.  -/
ContinuousLinearMap.toLinearMapRingHom : {R₁ : Type u_1} →
  [inst : Semiring R₁] →
    {M₁ : Type u_4} →
      [inst_1 : TopologicalSpace M₁] →
        [inst_2 : AddCommMonoid M₁] →
          [inst_3 : Module R₁ M₁] → [inst_4 : ContinuousAdd M₁] → (M₁ →L[R₁] M₁) →+* M₁ →ₗ[R₁] M₁
-- Mathlib.SetTheory.ZFC.VonNeumann
ZFSet.vonNeumann_injective : Function.Injective ZFSet.vonNeumann
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.instIsTorsionFree_2 : ∀ (K : Type u_4) (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
  Module.IsTorsionFree (NumberField.RingOfIntegers K) L
-- Mathlib.Order.WellQuasiOrder
WellQuasiOrderedLE.mk : ∀ {α : Type u_3} [inst : LE α], (WellQuasiOrdered fun x1 x2 => x1 ≤ x2) → WellQuasiOrderedLE α
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.explicitCokernelDesc_unique : ∀ {X Y Z : SemiNormedGrp} {f : X ⟶ Y} {g : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = 0)
  (e : SemiNormedGrp.explicitCokernel f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SemiNormedGrp.explicitCokernelπ f) e = g →
    e = SemiNormedGrp.explicitCokernelDesc w
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.Ref.denote_flip : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {aig : Std.Sat.AIG α} {ref : aig.Ref}
  {inv : Bool}, ⟦assign, { aig := aig, ref := ref.flip inv }⟧ = (⟦assign, { aig := aig, ref := ref }⟧ ^^ inv)
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.enrichedFunctorTypeEquivFunctor_apply_obj : ∀ {C : Type u₁} [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] {D : Type u₂}
  [𝒟 : CategoryTheory.EnrichedCategory (Type v) D] (F : CategoryTheory.EnrichedFunctor (Type v) C D) (X : C),
  (CategoryTheory.enrichedFunctorTypeEquivFunctor F).obj X = F.obj X
-- Mathlib.Order.Partition.Basic
/-- The supremum of all parts is `s`.  -/
Partition.sSup_eq' : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : α} (self : Partition s), sSup self.parts = s
-- Mathlib.Algebra.Order.Ring.Synonym
Lex.instAddCommGroupWithOne : {R : Type u_1} → [AddCommGroupWithOne R] → AddCommGroupWithOne (Lex R)
-- Mathlib.Algebra.GCDMonoid.Basic
normalize_coe_units : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] (u : αˣ), normalize ↑u = 1
-- Mathlib.Order.Bounds.Basic
/-- **Alias** of `LE.le.isCofinalFor`.

---

**Alias** of `IsCofinalFor.of_subset`. -/
HasSubset.Subset.isCofinalFor : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, s ⊆ t → IsCofinalFor s t
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.liftPath_trans : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X}
  (cov : IsCoveringMap p) {x y z : X} {e : E} (hpe : x = p e) (γ : Path x y) (γ' : Path y z),
  cov.liftPath (↑(γ.trans γ')) e ⋯ =
    ↑({ toContinuousMap := cov.liftPath (↑γ) e ⋯, source' := ⋯, target' := ⋯ }.trans
        { toContinuousMap := cov.liftPath (↑γ') ((cov.liftPath (↑γ) e ⋯) 1) ⋯, source' := ⋯, target' := ⋯ })
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
/-- The cardinality of a Galois group of `B/A` equals the rank of `B` as an `A`-module.

See `IsGaloisGroup.card_eq_finrank`, a field-theoretic version that does not assume finiteness.  -/
IsGaloisGroup.card_eq_finrank' : ∀ (G : Type u_1) [inst : Group G] (A : Type u_5) (B : Type u_6) [inst_1 : CommRing A] [inst_2 : CommRing B] [IsDomain B]
  [inst_4 : Algebra A B] [FaithfulSMul A B] [inst_6 : MulSemiringAction G B] [IsGaloisGroup G A B] [Finite G],
  Nat.card G = Module.finrank A B
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Read off the continuity of a function `f : Z → X` at `z : Z` by transferring via a
trivialization of `Z` containing `z`.  -/
Bundle.Trivialization.continuousAt_of_comp_right : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] {X : Type u_5} [inst_3 : TopologicalSpace X] {f : Z → X} {z : Z}
  (e : Bundle.Trivialization F proj), proj z ∈ e.baseSet → ContinuousAt (f ∘ ↑e.symm) (↑e z) → ContinuousAt f z
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.δ_pOpcycles_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.δ_pOpcycles._auto_1) {Z : C}
  (h : X.opcycles f g n₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) (CategoryTheory.CategoryStruct.comp (X.pOpcycles f g n₁) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : (a : α) → β a → Bool} {k : α} {h' : k ∈ Std.ExtDTreeMap.filter f t},
  (Std.ExtDTreeMap.filter f t).getKey k h' = t.getKey k ⋯
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.inter_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ m₃ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₃.WF → m₂.Equiv m₃ → (m₁ ∩ m₂).Equiv (m₁ ∩ m₃)
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.EStateM.tryCatch.match_1.eq_2 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (ok : EStateM.Result ε σ α)
  (h_1 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)) (h_2 : (ok : EStateM.Result ε σ α) → motive ok),
  (∀ (e : ε) (s : σ), ok = EStateM.Result.error e s → False) →
    (match ok with
      | EStateM.Result.error e s => h_1 e s
      | ok => h_2 ok) =
      h_2 ok
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.centralizer_eq_iInf : ∀ {G : Type u_1} [inst : AddGroup G] (s : Set G), AddSubgroup.centralizer s = ⨅ g ∈ s, AddSubgroup.centralizer {g}
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l l' : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l → l.Perm l' → Std.Internal.List.minKey? l = Std.Internal.List.minKey? l'
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- A noncomputable remainder to define the Euclidean domain structure. The GCD algorithm only takes
two steps to terminate. Given `GCD(x,y)`, if `x ∣ y` then `y%x = 0` so we're done in one step;
otherwise `y%x = y` and then `GCD(x,y) = GCD(y,x)` which brings us back to the first case.  -/
IsDiscreteValuationRing.remainder : {R : Type u_2} → [CommRing R] → R → R → R
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsPrenex.ex : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α (n + 1)}, φ.IsPrenex → φ.ex.IsPrenex