mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddRightCancelSemigroup.eq_1 : ∀ {α : Type u_1} [inst : AddRightCancelSemigroup α],
  Lex.instAddRightCancelSemigroup = { toAddSemigroup := Lex.instAddSemigroup, toIsRightCancelAdd := ⋯ }
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- **Alias** of `AddMonoidHom.pi_injective`. -/
AddMonoidHom.injective_pi : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → AddZeroClass (f i)] {γ : Type w} [Nonempty I]
  [inst_2 : AddZeroClass γ] (g : (i : I) → γ →+ f i),
  (∀ (i : I), Function.Injective ⇑(g i)) → Function.Injective ⇑(AddMonoidHom.pi g)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instSemiring : {n : Type u_2} → {A : Type u_5} → [Fintype n] → [DecidableEq n] → [Semiring A] → Semiring (CStarMatrix n n A)
-- Lean.Meta.Tactic.Rewrite
Lean.Meta.RewriteResult.eNew : Lean.Meta.RewriteResult → Lean.Expr
-- Lean.Parser.Syntax
Lean.Parser.Command.macroRhs : Lean.Parser.Parser
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_insertEntry_le_self : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : Std.Internal.List.DistinctKeys l) {kmi : α},
  (Std.Internal.List.minKey? (Std.Internal.List.insertEntry k v l)).get ⋯ = kmi → (compare kmi k).isLE = true
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_inter_le_size_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ ∩ m₂).size ≤ m₂.size
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_dvd_gcd_mul_right : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (m n k : α), gcd m n ∣ gcd (m * k) n
-- Mathlib.Order.WithBot
WithTop.instBoundedOrder.eq_1 : ∀ {α : Type u_1} [inst : LE α] [inst_1 : OrderBot α],
  WithTop.instBoundedOrder = { toOrderTop := WithTop.instOrderTop, toOrderBot := WithTop.instOrderBot }
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.id_of_comp_right_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (f : X ⟶ X),
  (∀ {Y : C} (g : Y ⟶ X), CategoryTheory.CategoryStruct.comp g f = g) → f = CategoryTheory.CategoryStruct.id X
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.toList_toArray : ∀ {α : Type u} {r : Std.Rco α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxo.IsAlwaysFinite α], r.toArray.toList = r.toList
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pushoutCoconeOfLeftIso_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.IsIso f],
  (CategoryTheory.Limits.pushoutCoconeOfLeftIso f g).inr = CategoryTheory.CategoryStruct.id Z
-- Mathlib.CategoryTheory.Types.Basic
/-- `uliftFunctor : Type u ⥤ Type max u v` is fully faithful.  -/
CategoryTheory.fullyFaithfulULiftFunctor : CategoryTheory.uliftFunctor.{v, u}.FullyFaithful
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.ordered_keys_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp],
  List.Pairwise (fun a b => cmp a.1 b.1 = Ordering.lt) (Std.DTreeMap.Const.toList t)
-- Mathlib.Tactic.Simproc.Factors
Mathlib.Meta.Simproc.FactorsHelper.primeFactorsList_eq : ∀ {n : ℕ} {l : List ℕ}, Mathlib.Meta.Simproc.FactorsHelper n 2 l → n.primeFactorsList = l
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.equiv.refl : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y), f.equiv f
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.instIsStableUnderShiftByShiftClosure : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] (a : A), (P.shiftClosure A).IsStableUnderShiftBy a
-- Std.Async.System
Std.Async.System.instReprCPUTimes.repr : Std.Async.System.CPUTimes → ℕ → Std.Format
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_transpose : ∀ {n : Type u_3} {R : Type u_6} [inst : Fintype n] [inst_1 : AddCommMonoid R] (A : Matrix n n R),
  A.transpose.trace = A.trace
-- Init.Data.List.Nat.Range
List.snd_lt_of_mem_zipIdx : ∀ {α : Type u_1} {x : α × ℕ} {l : List α} {k : ℕ}, x ∈ l.zipIdx k → x.2 < l.length + k
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
AdicCompletion.ofTensorProduct_tmul : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (r : AdicCompletion I R) (x : M), (AdicCompletion.ofTensorProduct I M) (r ⊗ₜ[R] x) = r • (AdicCompletion.of I M) x
-- Mathlib.Topology.Constructions
OrderDual.instNeBotNhdsWithinIio : ∀ {X : Type u} [inst : TopologicalSpace X] [inst_1 : Preorder X] {x : X} [(nhdsWithin x (Set.Ioi x)).NeBot],
  (nhdsWithin (OrderDual.toDual x) (Set.Iio (OrderDual.toDual x))).NeBot
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.findSyntheticTacticCompletion? : Lean.FileMap →
  String.Pos.Raw → Lean.Syntax → Lean.Elab.InfoTree → Option Lean.Server.Completion.ContextualizedCompletionInfo
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f)
        (CategoryTheory.Limits.pullback.snd g g)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst f g)
        (CategoryTheory.Limits.pullback.fst f g))
      (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- A typeclass for pairs of morphisms that are jointly monic.  -/
CategoryTheory.JointlyMono₂ : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {R X₁ X₂ : C} → (R ⟶ X₁) → (R ⟶ X₂) → Prop
-- Mathlib.Algebra.Ring.Defs
neg_mul_comm : ∀ {α : Type u} [inst : Mul α] [inst_1 : HasDistribNeg α] (a b : α), -a * b = a * -b
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValueD_filter_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {fallback : β} {f : α → β → Bool} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' : α},
      Std.Internal.List.getKey? k l = some k' →
        Std.Internal.List.getValueD k (List.filter (fun p => f p.fst p.snd) l) fallback =
          (Option.filter (fun x => f k' x) (Std.Internal.List.getValue? k l)).getD fallback
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.trStmts₁.eq_def : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (x : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2to1.trStmts₁ x =
    match x with
    | Turing.TM2.Stmt.push k f q =>
      {Turing.TM2to1.Λ'.go k (Turing.TM2to1.StAct.push f) q, Turing.TM2to1.Λ'.ret q} ∪ Turing.TM2to1.trStmts₁ q
    | Turing.TM2.Stmt.peek k f q =>
      {Turing.TM2to1.Λ'.go k (Turing.TM2to1.StAct.peek f) q, Turing.TM2to1.Λ'.ret q} ∪ Turing.TM2to1.trStmts₁ q
    | Turing.TM2.Stmt.pop k f q =>
      {Turing.TM2to1.Λ'.go k (Turing.TM2to1.StAct.pop f) q, Turing.TM2to1.Λ'.ret q} ∪ Turing.TM2to1.trStmts₁ q
    | Turing.TM2.Stmt.load a q => Turing.TM2to1.trStmts₁ q
    | Turing.TM2.Stmt.branch a q₁ q₂ => Turing.TM2to1.trStmts₁ q₁ ∪ Turing.TM2to1.trStmts₁ q₂
    | x => ∅
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.prun_lift : ∀ {α γ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {x : m α}
  {f : (a : α) → (Std.Iterators.HetT.lift x).Property a → m γ},
  (Std.Iterators.HetT.lift x).prun f = do
    let a ← x
    f a True.intro
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.unop.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.MorphismProperty Cᵒᵖ) (x x_1 : C)
  (f : x ⟶ x_1), P.unop f = P f.op
-- Init.Data.Iterators.Basic
Std.Iter.IsPlausibleStep.isPlausibleSuccessor_of_skip : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it' it : Std.Iter β},
  it.IsPlausibleStep (Std.IterStep.skip it') → it'.IsPlausibleSuccessorOf it
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.denoteS.match_1.eq_3 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (v : Lean.Grind.CommRing.Var)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (v : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var v))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_6 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)),
  (match Lean.Grind.CommRing.Expr.var v with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.natCast k => h_2 k
    | Lean.Grind.CommRing.Expr.var v => h_3 v
    | a.add b => h_4 a b
    | a.mul b => h_5 a b
    | a.pow k => h_6 a k
    | a.sub b => h_7 a b
    | a.neg => h_8 a
    | Lean.Grind.CommRing.Expr.intCast k => h_9 k) =
    h_3 v
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.toBiconeFunctor_obj_π : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (b : CategoryTheory.Limits.BinaryBicone X Y) (j : CategoryTheory.Limits.WalkingPair),
  (CategoryTheory.Limits.BinaryBicone.toBiconeFunctor.obj b).π j =
    CategoryTheory.Limits.WalkingPair.casesOn j b.fst b.snd
-- Mathlib.Data.ZMod.Basic
_private.Mathlib.Data.ZMod.Basic.0.ZMod.val.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Analysis.InnerProductSpace.NormPow
hasFDerivAt_norm_rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] (x : E) {p : ℝ},
  1 < p → HasFDerivAt (fun x => ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x
-- Mathlib.FieldTheory.IsPerfectClosure
mem_pNilradical : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} {x : R}, x ∈ pNilradical R p ↔ ∃ n, x ^ p ^ n = 0
-- Mathlib.Analysis.Complex.JensenFormula
_private.Mathlib.Analysis.Complex.JensenFormula.0.herglotzLogIntegrand : ℂ → ℂ → ℂ → ℝ
-- ProofWidgets.Component.Panel.Basic
ProofWidgets.PanelWidgetProps.mk.inj : ∀ {pos : Lean.Lsp.Position} {goals : Array Lean.Widget.InteractiveGoal}
  {termGoal? : Option Lean.Widget.InteractiveTermGoal} {selectedLocations : Array Lean.SubExpr.GoalsLocation}
  {pos_1 : Lean.Lsp.Position} {goals_1 : Array Lean.Widget.InteractiveGoal}
  {termGoal?_1 : Option Lean.Widget.InteractiveTermGoal} {selectedLocations_1 : Array Lean.SubExpr.GoalsLocation},
  { pos := pos, goals := goals, termGoal? := termGoal?, selectedLocations := selectedLocations } =
      { pos := pos_1, goals := goals_1, termGoal? := termGoal?_1, selectedLocations := selectedLocations_1 } →
    pos = pos_1 ∧ goals = goals_1 ∧ termGoal? = termGoal?_1 ∧ selectedLocations = selectedLocations_1
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.boundary_lt_top : ∀ (n : ℕ), SSet.boundary n < ⊤
-- Mathlib.CategoryTheory.Preadditive.Projective.Preserves
CategoryTheory.Functor.preservesProjectiveObjects_of_adjunction_of_preservesEpimorphisms : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [G.PreservesEpimorphisms],
  F.PreservesProjectiveObjects
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosure.equivOfEquiv_symm_comp_algebraMap : ∀ {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Field L]
  [inst_3 : Field M] [inst_4 : Algebra R M] [inst_5 : Module.IsTorsionFree R M] [inst_6 : IsAlgClosure R M]
  [inst_7 : Algebra S L] [inst_8 : Module.IsTorsionFree S L] [inst_9 : IsAlgClosure S L] [inst_10 : IsDomain R]
  [inst_11 : IsDomain S] (hSR : S ≃+* R),
  (↑(IsAlgClosure.equivOfEquiv L M hSR).symm).comp (algebraMap R M) = (algebraMap S L).comp ↑hSR.symm
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.HasIdealSupport.mk : ∀ {R : Type u_1} [inst : CommRing R] {P : RingPreordering R},
  (∀ (x : R) {a : R}, a ∈ P.supportAddSubgroup → x * a ∈ P.supportAddSubgroup) → P.HasIdealSupport
-- Mathlib.Data.List.Sigma
List.dlookup_cons_ne : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (l : List (Sigma β)) {a : α} (s : Sigma β),
  a ≠ s.fst → List.dlookup a (s :: l) = List.dlookup a l
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetRing.sdiff_mem : ∀ {α : Type u_1} {C : Set (Set α)}, MeasureTheory.IsSetRing C → ∀ ⦃s t : Set α⦄, s ∈ C → t ∈ C → s \ t ∈ C
-- Init.Data.Nat.Lemmas
Nat.decidableExistsLE : {p : ℕ → Prop} → [DecidablePred p] → DecidablePred fun n => ∃ m ≤ n, p m
-- Mathlib.Algebra.Category.ModuleCat.Colimits
ModuleCat.homMk.congr_simp : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R}
  (φ φ_1 :
    (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).obj M ⟶
      (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).obj N)
  (e_φ : φ = φ_1)
  (hφ : ∀ (r : R), CategoryTheory.CategoryStruct.comp φ (N.smul r) = CategoryTheory.CategoryStruct.comp (M.smul r) φ),
  ModuleCat.homMk φ hφ = ModuleCat.homMk φ_1 ⋯
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.isOfNatInst : Lean.Expr → Lean.Expr → Lean.Meta.Grind.Arith.FieldNormNum.M✝ Bool
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- Construct an isomorphism of `1`-hypercovers by giving the compatibility conditions only
in the forward direction.  -/
CategoryTheory.PreOneHypercover.isoMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E F : CategoryTheory.PreOneHypercover S} →
        (s₀ : E.I₀ ≃ F.I₀) →
          (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) →
            (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)) →
              (h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)) →
                autoParam (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i)
                    CategoryTheory.PreOneHypercover.isoMk._auto_1 →
                  autoParam
                      (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
                        CategoryTheory.CategoryStruct.comp (h₁ k).hom (F.p₁ (s₁ k)) =
                          CategoryTheory.CategoryStruct.comp (E.p₁ k) (h₀ i).hom)
                      CategoryTheory.PreOneHypercover.isoMk._auto_3 →
                    autoParam
                        (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
                          CategoryTheory.CategoryStruct.comp (h₁ k).hom (F.p₂ (s₁ k)) =
                            CategoryTheory.CategoryStruct.comp (E.p₂ k) (h₀ j).hom)
                        CategoryTheory.PreOneHypercover.isoMk._auto_5 →
                      (E ≅ F)
-- Mathlib.RepresentationTheory.Tannaka
/-- `leftRegular` as a morphism `rightFDRep k G ⟶ rightFDRep k G` in `FDRep k G`.  -/
TannakaDuality.FiniteGroup.leftRegularFDRepHom : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → [inst_2 : Finite G] → G → CategoryTheory.End TannakaDuality.FiniteGroup.rightFDRep
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatTrans.mk.sizeOf_spec : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} {F G : CategoryTheory.BasedFunctor 𝒳 𝒴} [inst_1 : SizeOf 𝒮]
  (toNatTrans : CategoryTheory.NatTrans F.toFunctor G.toFunctor)
  (isHomLift' :
    autoParam (∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (CategoryTheory.CategoryStruct.id (𝒳.p.obj a)) (toNatTrans.app a))
      CategoryTheory.BasedNatTrans.isHomLift'._autoParam),
  sizeOf { toNatTrans := toNatTrans, isHomLift' := isHomLift' } = 1 + sizeOf toNatTrans
-- Mathlib.LinearAlgebra.DFinsupp
/-- `DFinsupp.mk` as a `LinearMap`.  -/
DFinsupp.lmk : {ι : Type u_1} →
  {R : Type u_3} →
    {M : ι → Type u_5} →
      [inst : Semiring R] →
        [inst_1 : (i : ι) → AddCommMonoid (M i)] →
          [inst_2 : (i : ι) → Module R (M i)] →
            [DecidableEq ι] → (s : Finset ι) → ((i : ↑↑s) → M ↑i) →ₗ[R] Π₀ (i : ι), M i
-- Mathlib.RingTheory.FractionalIdeal.Extended
/-- The extension of a principal fractional ideal is the principal ideal generated by the extension
of a generator.  -/
FractionalIdeal.extended_spanSingleton : ∀ {A : Type u_1} [inst : CommRing A] {B : Type u_2} [inst_1 : CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A}
  [inst_2 : CommRing K] [inst_3 : Algebra A K] [inst_4 : IsLocalization M K] (L : Type u_4) {N : Submonoid B}
  [inst_5 : CommRing L] [inst_6 : Algebra B L] [inst_7 : IsLocalization N L] (hf : M ≤ Submonoid.comap f N) (x : K),
  FractionalIdeal.extended L hf (FractionalIdeal.spanSingleton M x) =
    FractionalIdeal.spanSingleton N ((IsLocalization.map L f hf) x)
-- Mathlib.GroupTheory.Transfer
/-- A cyclic Sylow subgroup for the smallest prime has a normal complement.  -/
IsCyclic.isComplement' : ∀ {G : Type u_3} [inst : Group G] [inst_1 : Finite G] {p : ℕ} (hp : (Nat.card G).minFac = p) {P : Sylow p G}
  (hP : IsCyclic ↥↑P), (MonoidHom.transferSylow P ⋯).ker.IsComplement' ↑P
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsRankOneDiscrete.generator_zpowers_eq_range : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] (K : Type u_3) [inst_1 : Field K] (w : Valuation K Γ)
  [inst_2 : w.IsRankOneDiscrete],
  Units.val '' ↑(Subgroup.zpowers (Valuation.IsRankOneDiscrete.generator w)) = Set.range ⇑w \ {0}
-- Mathlib.RingTheory.SimpleModule.Basic
isSimpleModule_iff : ∀ (R : Type u_2) [inst : Ring R] (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsSimpleModule R M ↔ IsSimpleOrder (Submodule R M)
-- Lean.MetavarContext
Lean.instInhabitedMetavarDecl : Inhabited Lean.MetavarDecl
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
PreAbstractSimplicialComplex.instTop : (ι : Type u_1) → Top (PreAbstractSimplicialComplex ι)
-- Init.Data.SInt.Lemmas
Int16.toInt64_ofInt : ∀ {n : ℤ}, Int16.minValue.toInt ≤ n → n ≤ Int16.maxValue.toInt → (Int16.ofInt n).toInt64 = Int64.ofInt n
-- Mathlib.Algebra.CubicDiscriminant
Cubic.coeff_eq_c : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.toPoly.coeff 1 = P.c
-- Mathlib.NumberTheory.LSeries.PrimesInAP
/-- The auxiliary function used, e.g., with the Wiener-Ikehara Theorem to prove
Dirichlet's Theorem. On `re s > 1`, it agrees with the L-series of the von Mangoldt
function restricted to the residue class `a : ZMod q` minus the principal part
`(q.totient)⁻¹/(s-1)` of the pole at `s = 1`;
see `ArithmeticFunction.vonMangoldt.eqOn_LFunctionResidueClassAux`.  -/
ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux : {q : ℕ} → ZMod q → [NeZero q] → ℂ → ℂ
-- Init.Data.Range.Polymorphic.IntLemmas
Std.PRange.Int.succMany_eq : ∀ {n : ℕ} {m : ℤ}, Std.PRange.succMany n m = m + ↑n
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsLittleO.of_tendsto_div_atBot : ∀ {α : Type u_1} {𝕜 : Type u_17} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜}, Filter.Tendsto (fun x => g x / f x) l Filter.atBot → f =o[l] g
-- Mathlib.Order.Basic
/-- A function `a` is strongly less than a function `b` if `a i < b i` for all `i`.  -/
_private.Mathlib.Order.Basic.0.«term_≺_» : Lean.TrailingParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
/-- The recursion principle for nonempty walks  -/
SimpleGraph.Walk.notNilRec : {V : Type u} →
  {G : SimpleGraph V} →
    {u w : V} →
      {motive : {u w : V} → (p : G.Walk u w) → ¬p.Nil → Sort u_1} →
        ({u v w : V} → (h : G.Adj u v) → (q : G.Walk v w) → motive (SimpleGraph.Walk.cons h q) ⋯) →
          (p : G.Walk u w) → (hp : ¬p.Nil) → motive p hp
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_pos_of_eval₂_root : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {p : Polynomial R},
  p ≠ 0 → ∀ (f : R →+* S) {z : S}, Polynomial.eval₂ f z p = 0 → (∀ (x : R), f x = 0 → x = 0) → 0 < p.natDegree
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.hasProducts_of_limit_fans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (lf : {J : Type w} → (f : J → C) → CategoryTheory.Limits.Fan f)
  (lf_isLimit : {J : Type w} → (f : J → C) → CategoryTheory.Limits.IsLimit (lf f)), CategoryTheory.Limits.HasProducts C
-- Mathlib.Algebra.Order.UpperLower
lowerClosure_add_distrib : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α] (s t : Set α),
  lowerClosure (s + t) = lowerClosure s + lowerClosure t
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.HasOfPrecompProperty.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W W' : CategoryTheory.MorphismProperty C},
  (∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), W' f → W (CategoryTheory.CategoryStruct.comp f g) → W g) →
    W.HasOfPrecompProperty W'
-- Mathlib.Topology.Algebra.Module.Equiv
/-- The continuous linear equivalence between `ULift M₁` and `M₁`.

This is a continuous version of `ULift.moduleEquiv`.  -/
ContinuousLinearEquiv.ulift : {R₁ : Type u_1} →
  [inst : Semiring R₁] →
    {M₁ : Type u_4} →
      [inst_1 : TopologicalSpace M₁] →
        [inst_2 : AddCommMonoid M₁] → [inst_3 : Module R₁ M₁] → ULift.{u_9, u_4} M₁ ≃L[R₁] M₁
-- Mathlib.Algebra.Ring.Subsemiring.Defs
SubsemiringClass.mk : ∀ {S : Type u_1} {R : outParam (Type u)} [inst : NonAssocSemiring R] [inst_1 : SetLike S R]
  [toSubmonoidClass : SubmonoidClass S R] [toAddSubmonoidClass : AddSubmonoidClass S R], SubsemiringClass S R
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.instOneHom.eq_1 : ∀ (X Y : MonCat), X.instOneHom Y = { one := MonCat.ofHom 1 }
-- Mathlib.Algebra.Free
_private.Mathlib.Algebra.Free.0.FreeMagma.liftAux.match_1.eq_1 : ∀ {α : Type u_1} (motive : FreeMagma α → Sort u_2) (x : α) (h_1 : (x : α) → motive (FreeMagma.of x))
  (h_2 : (x y : FreeMagma α) → motive (x.mul y)),
  (match FreeMagma.of x with
    | FreeMagma.of x => h_1 x
    | x.mul y => h_2 x y) =
    h_1 x
-- Mathlib.LinearAlgebra.SModEq.Basic
/-- A predicate saying two elements of a module are equivalent modulo a submodule.  -/
«term_≡_[SMOD_]» : Lean.TrailingParserDescr
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- The action `G ↷ G` by left translations is proper.  -/
instProperSMulOfIsTopologicalGroup : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G], ProperSMul G G
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
/-- Use `head_edges_eq_mk_start_snd` to rewrite in the reverse direction.  -/
SimpleGraph.Walk.mk_start_snd_eq_head_edges : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : ¬p.Nil), s(v, p.snd) = p.edges.head ⋯
-- Std.Data.ExtTreeSet.Basic
Std.ExtTreeSet.instSingletonOfTransCmp : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Singleton α (Std.ExtTreeSet α cmp)
-- Mathlib.Data.List.Sort
StrictAnti.sortedGT_listMap : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {l : List α},
  StrictAnti f → ((List.map f l).SortedGT ↔ l.SortedLT)
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Filter.EventuallyEq.iteratedDerivWithin' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {f g : 𝕜 → F} {s t : Set 𝕜},
  f =ᶠ[nhdsWithin x s] g → t ⊆ s → ∀ (n : ℕ), iteratedDerivWithin n f t =ᶠ[nhdsWithin x s] iteratedDerivWithin n g t