mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.HorizontalComp.of.inj : ∀ {η η_1 : Mathlib.Tactic.BicategoryLike.WhiskerRight},
  Mathlib.Tactic.BicategoryLike.HorizontalComp.of η = Mathlib.Tactic.BicategoryLike.HorizontalComp.of η_1 → η = η_1
-- Mathlib.Topology.UniformSpace.Ultra.Basic
IsTransitiveRel.mem_filter_prod_trans : ∀ {X : Type u_1} {s : SetRel X X} {f g h : Filter X} [g.NeBot] [s.IsTrans], s ∈ f ×ˢ g → s ∈ g ×ˢ h → s ∈ f ×ˢ h
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.foldl_perm_cong : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {init₁ init₂ l : List ((a : α) × β a)}
  {f : List ((a : α) × β a) → (a : α) × β a → List ((a : α) × β a)},
  init₁.Perm init₂ →
    (∀ (h : (a : α) × β a) (l₁ l₂ : List ((a : α) × β a)),
        Std.Internal.List.DistinctKeys l₁ →
          l₁.Perm l₂ → (f l₁ h).Perm (f l₂ h) ∧ Std.Internal.List.DistinctKeys (f l₁ h)) →
      Std.Internal.List.DistinctKeys init₁ → (List.foldl f init₁ l).Perm (List.foldl f init₂ l)
-- Mathlib.Analysis.Convex.EGauge
le_egauge_iff : ∀ {𝕜 : Type u_1} [inst : NNNorm 𝕜] {E : Type u_2} [inst_1 : SMul 𝕜 E] {s : Set E} {x : E} {r : ENNReal},
  r ≤ egauge 𝕜 s x ↔ ∀ (c : 𝕜), x ∈ c • s → r ≤ ‖c‖ₑ
-- Mathlib.Algebra.Group.AddChar
/-- When `M` is commutative, `AddChar A M` is an additive commutative monoid.  -/
AddChar.instAddCommMonoid : {A : Type u_2} → {M : Type u_3} → [inst : AddMonoid A] → [inst_1 : CommMonoid M] → AddCommMonoid (AddChar A M)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instMul : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [inst_4 : (i : ι) → Mul (G i)] →
                  [∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)] → Mul (DirectLimit G f)
-- Batteries.Data.List.Lemmas
List.swap_eq_of_lt : ∀ {α : Type u_1} {i j : ℕ} {xs : List α} (hi : i < xs.length) (hj : j < xs.length),
  xs.swap i j = (xs.set i xs[j]).set j xs[i]
-- Lean.Message
Lean.MessageData.ofFormatWithInfos.injEq : ∀ (a a_1 : Lean.FormatWithInfos),
  (Lean.MessageData.ofFormatWithInfos a = Lean.MessageData.ofFormatWithInfos a_1) = (a = a_1)
-- Lean.Environment
/-- The header contains additional information that is set at import time.  -/
Lean.Kernel.Environment.header : Lean.Kernel.Environment → Lean.EnvironmentHeader
-- Mathlib.Data.Multiset.Pi
Multiset.pi_cons : ∀ {α : Type u_1} [inst : DecidableEq α] {β : α → Type u_2} (m : Multiset α) (t : (a : α) → Multiset (β a)) (a : α),
  (a ::ₘ m).pi t = (t a).bind fun b => Multiset.map (Multiset.Pi.cons m a b) (m.pi t)
-- Mathlib.Topology.KrullDimension
Topology.IsOpenEmbedding.coheight_map : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  (hf : Topology.IsOpenEmbedding f) (Z : TopologicalSpace.IrreducibleCloseds X),
  Order.coheight (TopologicalSpace.IrreducibleCloseds.map f ⋯ Z) = Order.coheight Z
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.instAddCommGroupHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (R : CategoryTheory.Sheaf J RingCat) → (M N : SheafOfModules R) → AddCommGroup (M ⟶ N)
-- Init.Data.BitVec.Lemmas
BitVec.msb_of_zero_length : ∀ {w : ℕ}, w = 0 → ∀ (x : BitVec w), x.msb = false
-- Mathlib.Testing.Plausible.Functions
Plausible.InjectiveFunction.applyId_injective : ∀ {α : Type u} [inst : DecidableEq α] {xs ys : List α},
  xs.Nodup → xs.Perm ys → Function.Injective (Plausible.InjectiveFunction.List.applyId (xs.zip ys))
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.Result.step.sizeOf_spec : ∀ (e' : Lean.Expr) (done : optParam Bool false),
  sizeOf (Lean.Meta.Sym.DSimp.Result.step e' done) = 1 + sizeOf e' + sizeOf done
-- Mathlib.Data.Num.Bitwise
/-- The `tail` of a `SNum` is obtained by removing the LSB.
Edge cases: `tail 1 = 0`, `tail (-2) = -1`, `tail 0 = 0` and `tail (-1) = -1`.  -/
SNum.tail : SNum → SNum
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.hom_ext : ∀ {R : Type u} [inst : CommRing R] {X Y : BialgCat R} (f g : X ⟶ Y),
  BialgCat.Hom.toBialgHom f = BialgCat.Hom.toBialgHom g → f = g
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.evalMulHom.eq_1 : ∀ {I : Type u} (f : I → Type v) [inst : (i : I) → Mul (f i)] (i : I),
  Pi.evalMulHom f i = { toFun := fun g => g i, map_mul' := ⋯ }
-- Mathlib.Algebra.GroupWithZero.Submonoid.Instances
MonoidWithZeroHom.val_mrange_zero : ∀ {G : Type u_1} {H : Type u_2} [inst : MulZeroOneClass G] [inst_1 : MulZeroOneClass H] (f : G →*₀ H), ↑0 = 0
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Icc_subset_Ico_union_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Icc a c ⊆ Set.Ico a b ∪ Set.Icc b c
-- Mathlib.Topology.Order.IntermediateValue
/-- Suppose `α` is equipped with a conditionally complete linear dense order and `f : α → δ` is
continuous and injective. Then `f` is strictly monotone or antitone (increasing or decreasing).  -/
Continuous.strictMono_of_inj : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {f : α → δ}, Continuous f → Function.Injective f → StrictMono f ∨ StrictAnti f
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- The mates equivalence commutes with vertical composition.  -/
CategoryTheory.Bicategory.mateEquiv_vcomp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e f : B} {g₁ : a ⟶ c} {g₂ : c ⟶ e} {h₁ : b ⟶ d}
  {h₂ : d ⟶ f} {l₁ : a ⟶ b} {r₁ : b ⟶ a} {l₂ : c ⟶ d} {r₂ : d ⟶ c} {l₃ : e ⟶ f} {r₃ : f ⟶ e}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂)
  (adj₃ : CategoryTheory.Bicategory.Adjunction l₃ r₃)
  (α : CategoryTheory.CategoryStruct.comp g₁ l₂ ⟶ CategoryTheory.CategoryStruct.comp l₁ h₁)
  (β : CategoryTheory.CategoryStruct.comp g₂ l₃ ⟶ CategoryTheory.CategoryStruct.comp l₂ h₂),
  (CategoryTheory.Bicategory.mateEquiv adj₁ adj₃) (CategoryTheory.Bicategory.leftAdjointSquare.vcomp α β) =
    CategoryTheory.Bicategory.rightAdjointSquare.vcomp ((CategoryTheory.Bicategory.mateEquiv adj₁ adj₂) α)
      ((CategoryTheory.Bicategory.mateEquiv adj₂ adj₃) β)
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.opEquiv.match_5.eq_1 : ∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] {x y : (CategoryTheory.WithTerminal C)ᵒᵖ}
  (motive : (x ⟶ y) → Sort u_3) (f : Opposite.unop y ⟶ Opposite.unop x)
  (h_1 : (f : Opposite.unop y ⟶ Opposite.unop x) → motive (Opposite.op f)),
  (match Opposite.op f with
    | Opposite.op f => h_1 f) =
    h_1 f
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF →
    ∀ {l : List ((a : α) × β a)} {k : α}, (List.map Sigma.fst l).contains k = false → (m.insertMany l).get? k = m.get? k
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.const : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (p : Prop),
  MeasureTheory.NullMeasurableSet {_a | p} μ
-- Mathlib.Data.Nat.Prime.Defs
Nat.Prime.one_lt : ∀ {p : ℕ}, Nat.Prime p → 1 < p
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.insert : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {a : α} {b : β a},
  m.WF → (m.insert a b).WF
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Summable.hasSum_iff_tendsto_nat : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {m : M} [T2Space M] {f : ℕ → M},
  Summable f → (HasSum f m ↔ Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds m))
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.map_isFunc : ∀ {f : ZFSet.{u_1} → ZFSet.{u_1}} [inst : ZFSet.Definable₁ f] {x y : ZFSet.{u_1}},
  x.IsFunc y (ZFSet.map f x) ↔ ∀ z ∈ x, f z ∈ y
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
SimpleGraph.Path.instFintype : {V : Type u} →
  (G : SimpleGraph V) → [DecidableEq V] → [Fintype V] → [DecidableRel G.Adj] → {u v : V} → Fintype (G.Path u v)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNth_binop : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (op : (j : Fin (n + 1)) → α j → α j → α j) (i : Fin (n + 1)) (x y : α i)
  (p q : (j : Fin n) → α (i.succAbove j)),
  (i.insertNth (op i x y) fun j => op (i.succAbove j) (p j) (q j)) = fun j =>
    op j (i.insertNth x p j) (i.insertNth y q j)
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
hasCardinalLT_subtype_iSup : ∀ {ι : Type u_1} {X : Type u_2} (P : ι → X → Prop) {κ : Cardinal.{u_3}} [Fact κ.IsRegular],
  HasCardinalLT ι κ → (∀ (i : ι), HasCardinalLT (Subtype (P i)) κ) → HasCardinalLT (Subtype (⨆ i, P i)) κ
-- Mathlib.Analysis.Normed.Group.FunctionSeries
/-- An infinite sum of functions with summable sup norm is the uniform limit of its partial sums.
Version with general index set.  -/
tendstoUniformly_tsum : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ}
  {f : α → β → F},
  Summable u →
    (∀ (n : α) (x : β), ‖f n x‖ ≤ u n) →
      TendstoUniformly (fun t x => ∑ n ∈ t, f n x) (fun x => ∑' (n : α), f n x) Filter.atTop
-- Mathlib.RepresentationTheory.Maschke
LinearMap.conjugate.congr_simp : ∀ {k : Type u_1} [inst : CommRing k] {G : Type u_2} [inst_1 : Group G] {V : Type u_3} [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : Module (MonoidAlgebra k G) V] [inst_5 : IsScalarTower k (MonoidAlgebra k G) V]
  {W : Type u_4} [inst_6 : AddCommGroup W] [inst_7 : Module k W] [inst_8 : Module (MonoidAlgebra k G) W]
  [inst_9 : IsScalarTower k (MonoidAlgebra k G) W] (π π_1 : W →ₗ[k] V),
  π = π_1 → ∀ (g g_1 : G), g = g_1 → π.conjugate g = π_1.conjugate g_1
-- Mathlib.Data.PNat.Xgcd
PNat.instInhabitedXgcdType : Inhabited PNat.XgcdType
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ParentSet : Type
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.comp : {C : Type u} → {X Y Z : CategoryTheory.FreeMonoidalCategory C} → X.Hom Y → Y.Hom Z → X.Hom Z
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.IsAcc.eq_1 : ∀ (o : Ordinal.{u_1}) (S : Set Ordinal.{u_1}), o.IsAcc S = AccPt o (Filter.principal S)
-- Init.Data.List.Count
List.IsPrefix.countP_le : ∀ {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α}, l₁ <+: l₂ → List.countP p l₁ ≤ List.countP p l₂
-- Mathlib.Topology.Algebra.AsymptoticCone
asymptoticCone_univ : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] [inst_6 : TopologicalSpace k]
  [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V],
  asymptoticCone k Set.univ = Set.univ
-- Mathlib.NumberTheory.LSeries.HurwitzZetaValues
/-- Reformulation of `sinZeta_two_mul_nat_add_one` using `Gammaℂ`.  -/
HurwitzZeta.sinZeta_two_mul_nat_add_one' : ∀ {k : ℕ} {x : ℝ},
  k ≠ 0 →
    x ∈ Set.Icc 0 1 →
      HurwitzZeta.sinZeta (↑x) (2 * ↑k + 1) =
        (-1) ^ (k + 1) / (2 * ↑k + 1) / (2 * ↑k + 1).Gammaℂ *
          Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffOn_empty : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {n : WithTop ℕ∞},
  ContMDiffOn I I' n f ∅
-- Mathlib.NumberTheory.MahlerMeasure
Polynomial.abs_leadingCoeff_eq_one_of_mahlerMeasure_eq_one : ∀ {p : Polynomial ℤ}, (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure = 1 → |p.leadingCoeff| = 1
-- Mathlib.CategoryTheory.Abelian.Preradical.Radical
CategoryTheory.Abelian.Radical.isZero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Radical C), CategoryTheory.Limits.IsZero (Φ.obj.quotient.comp Φ.obj.r)
-- Mathlib.Data.Set.Finite.Basic
OrderIso.finsetSetFinite_symm_apply : ∀ {α : Type u} (s : { s // s.Finite }), (RelIso.symm OrderIso.finsetSetFinite) s = ⋯.toFinset
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
/-- The functor `(F.obj (.mk (op S))).obj ⥤ F.DescentDataAsCoalgebra f`
when `f i : X i ⟶ S` is a family of morphisms.  -/
CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebra : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F :
        CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
          (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)) →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            (f : (i : ι) → X i ⟶ S) →
              CategoryTheory.Functor (↑(F.obj { as := Opposite.op S }).obj) (F.DescentDataAsCoalgebra f)
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.instFiniteUniversalFactorizationRing : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : Polynomial.MonicDegreeEq R n),
  Module.Finite R (Polynomial.UniversalFactorizationRing m k hn p)
-- Mathlib.Algebra.GroupWithZero.Defs
mul_eq_mul_left_iff : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [IsLeftCancelMulZero M₀] {a b c : M₀}, a * b = a * c ↔ b = c ∨ a = 0
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.grind_filter.quot : Lean.ParserDescr
-- Init.Data.List.Basic
List.beq_nil_cons : ∀ {α : Type u} [inst : BEq α] {a : α} {as : List α}, [].beq (a :: as) = false
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.HasProjectiveDimensionLT.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X : C} {n : ℕ},
  (∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : CategoryTheory.Abelian.Ext X Y i), e = 0) →
    CategoryTheory.HasProjectiveDimensionLT X n
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsRestriction.isStrictRestriction_of_ne : ∀ {α : Type u_1} {M N : Matroid α}, N.IsRestriction M → N ≠ M → N.IsStrictRestriction M
-- Mathlib.Combinatorics.SimpleGraph.DegreeSum
SimpleGraph.odd_card_odd_degree_vertices_ne : ∀ {V : Type u} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableEq V] [inst_2 : DecidableRel G.Adj] (v : V),
  Odd (G.degree v) → Odd {w | w ≠ v ∧ Odd (G.degree w)}.card
-- Mathlib.Data.Fin.Tuple.Embedding
/-- Adding a new element at the beginning of an injective n-tuple, to get an injective n+1-tuple.  -/
Fin.Embedding.cons : {α : Type u_1} → {n : ℕ} → (x : Fin n ↪ α) → {a : α} → a ∉ Set.range ⇑x → Fin (n + 1) ↪ α
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.algEquiv.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] (M M_1 : Submonoid R) (e_M : M = M_1) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (Q : Type u_4) [inst_4 : CommSemiring Q] [inst_5 : Algebra R Q]
  [inst_6 : IsLocalization M Q], IsLocalization.algEquiv M S Q = IsLocalization.algEquiv M_1 S Q
-- Mathlib.Algebra.Group.Action.Faithful
/-- `AddMonoid.toOppositeAddAction` is faithful on additive cancellative monoids.  -/
AddLeftCancelMonoid.to_faithfulVAdd_addOpposite : ∀ {α : Type u_3} [inst : AddLeftCancelMonoid α], FaithfulVAdd αᵃᵒᵖ α
-- Batteries.Data.List.Interleave
List.reverse_interleave_of_length_eq_length : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.length = l₂.length → (l₁.interleave l₂).reverse = l₂.reverse.interleave l₁.reverse
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.isHomogeneous_C : ∀ (σ : Type u_1) {R : Type u_3} [inst : CommSemiring R] (r : R), (MvPolynomial.C r).IsHomogeneous 0
-- Mathlib.RingTheory.Finiteness.Finsupp
AddMonoidAlgebra.moduleFinite : ∀ {M : Type u_1} {R : Type u_2} {S : Type u_3} [Finite M] [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Module R S] [Module.Finite R S], Module.Finite R (AddMonoidAlgebra S M)
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instHasModelBitVecOfNatNat : HasModel✝ Int64 (BitVec 64)
-- Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
AddChar.wInner_cWeight_eq_one_iff_eq : ∀ {G : Type u_1} {R : Type u_3} [inst : AddCommGroup G] [inst_1 : RCLike R] {ψ₁ ψ₂ : AddChar G R} [inst_2 : Fintype G],
  ⟪⇑ψ₁, ⇑ψ₂⟫ₙ_[R] = 1 ↔ ψ₁ = ψ₂
-- Mathlib.NumberTheory.SiegelsLemma
_private.Mathlib.NumberTheory.SiegelsLemma.0.Int.Matrix.N_le_P_add_one : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (A : Matrix α β ℤ) (i : α),
  (fun i =>
        ∑ j,
          ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ *
            -(A i j)⁻)
      i ≤
    (fun i =>
          ∑ j,
            ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ *
              (A i j)⁺)
        i +
      1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → γ} {k : α}, (Std.ExtTreeMap.map f t).getKey? k = t.getKey? k
-- Lean.SubExpr
Lean.SubExpr.Pos.toString : Lean.SubExpr.Pos → String
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.isUnit_det_of_left_inverse : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {A B : Matrix n n α},
  B * A = 1 → IsUnit A.det
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjHomologySelfIso_hom_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  {A B : C} (f : A ⟶ B),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((HomologicalComplex.single C c j).map f) j)
      (HomologicalComplex.singleObjHomologySelfIso c j B).hom =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjHomologySelfIso c j A).hom f
-- Mathlib.Algebra.Homology.Embedding.Boundary
ComplexShape.Embedding.BoundaryLE.notMem : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} {j : ι},
  e.BoundaryLE j → ∀ {k' : ι'}, c'.Rel (e.f j) k' → ∀ (a : ι), e.f a ≠ k'
-- Mathlib.Data.Num.Lemmas
PosNum.natSize.eq_def : ∀ (x : PosNum),
  x.natSize =
    match x with
    | PosNum.one => 1
    | n.bit0 => n.natSize.succ
    | n.bit1 => n.natSize.succ
-- Mathlib.CategoryTheory.Sites.Descent.IsStack
CategoryTheory.Pseudofunctor.IsStack.essSurj_of_sieve : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat)
  {J : CategoryTheory.GrothendieckTopology C} [self : F.IsStack J] {S : C},
  ∀ R ∈ J S, (F.toDescentData fun f => f.obj.hom).EssSurj
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.MkPreResultResult : Type
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ind : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (p : CategoryTheory.Subobject X → Prop),
  (∀ ⦃A : C⦄ (f : A ⟶ X) [inst_1 : CategoryTheory.Mono f], p (CategoryTheory.Subobject.mk f)) →
    ∀ (P : CategoryTheory.Subobject X), p P
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.mem_support_iff : ∀ {R : Type u_1} {n : ℕ} [inst : Semiring R] {p : SkewPolynomial R}, n ∈ p.support ↔ p.coeff n ≠ 0
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instIteratorLoop.loop.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) →
    (x : Option α) → ((next' : α) → x = some next' → motive (some next')) → (x = none → motive none) → motive x
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.isEmbedding_coe : Topology.IsEmbedding Complex.UnitDisc.coe
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- **Class formula** : let `G` be an additive group acting on `X` and let `φ` be a function
mapping each orbit of `X` under this action (that is, each element of the quotient of `X` by
the relation `orbitRel G X`) to an element in this orbit. This definition is a (noncomputable)
bijection between `X` and the disjoint union of `G/Stab(φ(ω))` over all orbits `ω : Ω`. In
most cases you'll want `φ` to be `Quotient.out`, so we provide
  `AddAction.selfEquivSigmaOrbitsQuotientStabilizer'` as a special case.  -/
AddAction.selfEquivSigmaOrbitsQuotientStabilizer' : (G : Type u) →
  (X : Type v) →
    [inst : AddGroup G] →
      [inst_1 : AddAction G X] →
        {φ : Quotient (AddAction.orbitRel G X) → X} →
          Function.LeftInverse Quotient.mk'' φ →
            X ≃ (ω : Quotient (AddAction.orbitRel G X)) × G ⧸ AddAction.stabilizer G (φ ω)
-- Std.Async.System
/-- Sets an environment variable to `value`.
 -/
Std.Async.System.setEnvVar : String → String → IO Unit
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
PresheafOfModules.toPresheaf_map_sheafificationHomEquiv_def : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  [inst_3 : J.WEqualsLocallyBijective AddCommGrpCat] [inst_4 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  {P : PresheafOfModules R₀} {F : SheafOfModules R} (f : (PresheafOfModules.sheafification α).obj P ⟶ F),
  (PresheafOfModules.toPresheaf R₀).map ((PresheafOfModules.sheafificationHomEquiv α) f) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P.presheaf)
      ((PresheafOfModules.toPresheaf R.obj).map f.val)
-- Std.Http.Protocol.H1.Reader
/-- The state of the `Reader` state machine.
 -/
Std.Http.Protocol.H1.Reader.State : Std.Http.Protocol.H1.Direction → Type
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.truncate_surjective : ∀ (p n : ℕ) (R : Type u_1) [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)],
  Function.Surjective ⇑(WittVector.truncate n)
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsFoelner.mk : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : Group G]
  [inst_2 : MulAction G X] {ι : Type u_3} {l : Filter ι} {F : ι → Set X},
  (∀ᶠ (i : ι) in l, MeasurableSet (F i)) →
    (∀ᶠ (i : ι) in l, μ (F i) ≠ 0) →
      (∀ᶠ (i : ι) in l, μ (F i) ≠ ⊤) →
        (∀ (g : G), Filter.Tendsto (fun i => μ (symmDiff (g • F i) (F i)) / μ (F i)) l (nhds 0)) → IsFoelner G μ l F
-- Init.Data.SInt.Lemmas
Int16.ofIntLE_add : ∀ {a b : ℤ} {hab₁ : Int16.minValue.toInt ≤ a + b} {hab₂ : a + b ≤ Int16.maxValue.toInt},
  Int16.ofIntLE (a + b) hab₁ hab₂ = Int16.ofInt a + Int16.ofInt b
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
/-- The multicoequalizer diagram which expresses `Λ[n, i]` as a gluing
of all `1`-codimensional faces of the standard simplex but one
along suitable `2`-codimensional faces.  -/
SSet.horn.multicoequalizerDiagram : ∀ {n : ℕ} (i : Fin (n + 1)),
  (SSet.horn n i).MulticoequalizerDiagram (fun j => SSet.stdSimplex.face {↑j}ᶜ) fun j k =>
    SSet.stdSimplex.face {↑j, ↑k}ᶜ
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.monadToFunctor_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C),
  (CategoryTheory.monadToFunctor C).obj T = T.toFunctor