mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.DocString.Markdown
_private.Lean.DocString.Markdown.0.Lean.Doc.blockMarkdown : {i : Type u_1} →
  {b : Type u_2} →
    [Lean.Doc.MarkdownInline i] → [Lean.Doc.MarkdownBlock i b] → Lean.Doc.Block i b → Lean.Doc.MarkdownM (Array String)
-- Mathlib.Data.NNReal.Defs
NNReal.coe_eq_one : ∀ {r : NNReal}, ↑r = 1 ↔ r = 1
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- **Alias** of `Multiset.finsetSum_eq_sup_iff_disjoint`. -/
Multiset.finset_sum_eq_sup_iff_disjoint : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] {i : Finset β} {f : β → Multiset α},
  i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.mem_or_not_mem : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (p : T.CompleteType α) (φ : (L.withConstants α).Sentence),
  φ ∈ p ∨ FirstOrder.Language.Formula.not φ ∈ p
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.H1π_comp_map_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↥(groupCohomology.cocycles₁ A)),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.map f φ 1))
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H1π A)) x) =
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.H1π B))
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.mapCocycles₁ f φ)) x)
-- Lean.Elab.Tactic.Grind.Config
_private.Lean.Elab.Tactic.Grind.Config.0.Lean.Elab.Tactic.instEvalExprOrderConfig : Lean.Elab.ConfigEval.EvalExpr Lean.Grind.OrderConfig
-- Mathlib.Algebra.Polynomial.Expand
/-- **Alias** of the reverse direction of `Polynomial.monic_expand_iff`. -/
Polynomial.Monic.expand : ∀ {R : Type u} [inst : CommSemiring R] {p : ℕ} {f : Polynomial R}, 0 < p → f.Monic → ((Polynomial.expand R p) f).Monic
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_iff_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂), S₁.Exact ↔ S₂.Exact
-- Mathlib.Data.Set.Image
Set.disjoint_powerset_insert : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∉ s → Disjoint (𝒫 s) (insert a '' 𝒫 s)
-- Mathlib.Analysis.Real.Pi.Wallis
Real.Wallis.W_succ : ∀ (k : ℕ), Real.Wallis.W (k + 1) = Real.Wallis.W k * ((2 * ↑k + 2) / (2 * ↑k + 1) * ((2 * ↑k + 2) / (2 * ↑k + 3)))
-- Init.Data.Int.Order
Int.mul_lt_mul_of_neg_right : ∀ {a b c : ℤ}, b < a → c < 0 → a * c < b * c
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.uniqueHomToZero : {Δ : SimplexCategory} → Unique (Δ ⟶ { len := 0 })
-- Mathlib.Combinatorics.Additive.FreimanHom
IsAddFreimanHom.prodMap : ∀ {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} [inst : AddCommMonoid α₁] [inst_1 : AddCommMonoid α₂]
  [inst_2 : AddCommMonoid β₁] [inst_3 : AddCommMonoid β₂] {A₁ : Set α₁} {A₂ : Set α₂} {B₁ : Set β₁} {B₂ : Set β₂}
  {f₁ : α₁ → β₁} {f₂ : α₂ → β₂} {n : ℕ},
  IsAddFreimanHom n A₁ B₁ f₁ → IsAddFreimanHom n A₂ B₂ f₂ → IsAddFreimanHom n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂)
-- Mathlib.Data.Finset.Card
Finset.card_image_of_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : DecidableEq β] (s : Finset α),
  Function.Injective f → (Finset.image f s).card = s.card
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_indicatorConstLp : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {t : Set X} {μ : MeasureTheory.Measure X} [CompleteSpace E] {p : ENNReal} (ht : MeasurableSet t) (hμt : μ t ≠ ⊤)
  (e : E), ∫ (x : X), ↑↑(MeasureTheory.indicatorConstLp p ht hμt e) x ∂μ = μ.real t • e
-- Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
/-- Given a finite cyclic group `G` generated by `g` and `A : Rep k G`, this is the quotient map
`Ker(N) ⟶ Ker(N)/Im(ρ(g) - Id(A)) ≅ Hᵢ(G, A)` for any nonzero even `i`.  -/
Rep.FiniteCyclicGroup.groupHomologyπEven : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : CommGroup G] →
      [inst_2 : Fintype G] →
        (A : Rep.{u, u, u} k G) →
          (g : G) →
            [DecidableEq G] →
              (∀ (x : G), x ∈ Subgroup.zpowers g) →
                (i : ℕ) → [NeZero i] → Even i → (ModuleCat.of k ↥(LinearMap.ker A.ρ.norm) ⟶ groupHomology A i)
-- Mathlib.Data.Set.Finite.Basic
Set.card_le_card : ∀ {α : Type u} {s t : Set α} [inst : Fintype ↑s] [inst_1 : Fintype ↑t], s ⊆ t → Fintype.card ↑s ≤ Fintype.card ↑t
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.notMem_bot : ∀ {M : Type u_1} [inst : Mul M] {x : M}, x ∉ ⊥
-- Mathlib.Topology.Sheaves.Over
TopologicalSpace.Opens.coe_overEquivalence_inverse_obj_left : ∀ {X : Type u} [inst : TopologicalSpace X] (U : TopologicalSpace.Opens X) (W : TopologicalSpace.Opens ↥U),
  ↑(U.overEquivalence.inverse.obj W).left = Subtype.val '' ↑W
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.State.usedTheorems : Lean.Meta.SimpAll.State → Lean.Meta.Simp.UsedSimps
-- Qq.Macro
Qq.Impl.unquoteLCtx : Qq.Impl.UnquoteM Unit
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.term_atomg : ∀ {α : Type u_1} [inst : AddCommGroup α] (x : α), x = Mathlib.Tactic.Abel.termg 1 x 0
-- Mathlib.Algebra.Ring.Prod
/-- Product of two `NonAssocSemiring`s is a `NonAssocSemiring`.  -/
Prod.instNonAssocSemiring : {R : Type u_1} → {S : Type u_3} → [NonAssocSemiring R] → [NonAssocSemiring S] → NonAssocSemiring (R × S)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pullbackCoverOfRight_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Y : C} (E : CategoryTheory.PreZeroHypercover Y) {X Z : C}
  (f : X ⟶ Z) (g : Y ⟶ Z) [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (CategoryTheory.CategoryStruct.comp (E.f i) g)]
  (i : E.I₀),
  (E.pullbackCoverOfRight f g).X i = CategoryTheory.Limits.pullback f (CategoryTheory.CategoryStruct.comp (E.f i) g)
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- The length of the new subexpression.  -/
Mathlib.Tactic.ClickSuggestions.GrwKey.replacementSize : Mathlib.Tactic.ClickSuggestions.GrwKey → ℕ
-- Batteries.Data.List.Count
List.surjective_sigmaCountToIdx : ∀ {α : Type u_1} [inst : BEq α] [ReflBEq α] {xs : List α}, Function.Surjective xs.sigmaCountToIdx
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.any_eq_false_iff_forall_contains_getKey_get : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [LawfulHashable α]
  [EquivBEq α] {p : α → β → Bool},
  m.WF →
    (m.any p = false ↔ ∀ (a : α) (h : m.contains a = true), p (m.getKey a h) (Std.DHashMap.Raw.Const.get m a h) = false)
-- Std.Internal.Do.PredTrans
/-- Adds an early-termination layer to a predicate transformer, modelling `Option` as
early termination. Given a transformer over `Option α`, produces one over `α` with an
additional exception postcondition for the `none` case.  -/
Std.Internal.Do.PredTrans.pushOption : {α Pred : Type u} →
  {EPred : Type v} →
    Std.Internal.Do.PredTrans Pred EPred (Option α) → Std.Internal.Do.PredTrans Pred (EPost.Cons✝ Pred EPred) α
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
FreeSimplexQuiver.Hom.σ.sizeOf_spec : ∀ {n : ℕ} (i : Fin (n + 1)), sizeOf (FreeSimplexQuiver.Hom.σ i) = 1 + sizeOf n + sizeOf i
-- Lean.Elab.Command
/-- `elabCommand` wrapper that should be used for the initial invocation, not for recursive calls after
macro expansion etc.
 -/
Lean.Elab.Command.elabCommandTopLevel : Lean.Syntax → optParam (Array Lean.Syntax) #[] → Lean.Elab.Command.CommandElabM Unit
-- Init.Data.UInt.Lemmas
UInt32.ofNatClamp_eq_ofNat : ∀ n < UInt32.size, UInt32.ofNatClamp n = UInt32.ofNat n
-- Init.System.IO
instMonadFinallyBaseIO : MonadFinally BaseIO
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Left.add_nonpos`.  -/
add_nonpos : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftMono α] {a b : α}, a ≤ 0 → b ≤ 0 → a + b ≤ 0
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.instInhabitedPartialMatch : Inhabited Lean.Meta.RefinedDiscrTree.PartialMatch✝
-- Mathlib.Algebra.Order.Floor.Ring
Int.mul_cast_floor_div_cancel_of_pos : ∀ {R : Type u_4} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorRing R] {n : ℤ},
  0 < n → ∀ (a : R), ⌊a * ↑n⌋ / n = ⌊a⌋
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.instField : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : AddCommGroup Γ] →
      [inst_1 : LinearOrder Γ] → [IsOrderedAddMonoid Γ] → [inst : Field R] → Field (HahnSeries Γ R)
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `IsMulTorsion.torsionMulEquiv_apply`. -/
Monoid.IsTorsion.torsionMulEquiv_apply : ∀ {G : Type u_1} [inst : CommMonoid G] (tG : IsMulTorsion G) (a : ↥(CommMonoid.torsion G)),
  tG.torsionMulEquiv a = ↑((MulEquiv.submonoidCongr ⋯) a)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Result.addExtraArgs : Lean.Meta.Simp.Result → Array Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.changeForm_self_apply : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : CliffordAlgebra Q), (CliffordAlgebra.changeForm ⋯) x = x
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_of_not_memLp : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.AEStronglyMeasurable X μ → ¬MeasureTheory.MemLp X 2 μ → ProbabilityTheory.variance X μ = 0
-- Mathlib.Computability.Language
Language.reverse_bijective : ∀ {α : Type u_1}, Function.Bijective Language.reverse
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableAt.hasMFDerivAt : ∀ {𝕜 : 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'} {x : M},
  MDiffAt f x → HasMFDerivAt% f x (mfderiv% f x)
-- Lean.Meta.ForEachExpr
_private.Lean.Meta.ForEachExpr.0.Lean.Meta.visitLet.visit : {m : Type → Type u_1} →
  [Monad m] → [MonadControlT Lean.MetaM m] → (Lean.Expr → m Unit) → Array Lean.Expr → Lean.Expr → m Unit
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.coeFnAlgHom_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (R : Type u_6) [inst_1 : CommSemiring R]
  [inst_2 : Semiring Y] [inst_3 : Algebra R Y] (a : LocallyConstant X Y) (a_1 : X),
  (LocallyConstant.coeFnAlgHom R) a a_1 = a a_1
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.zsmul_nonneg : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.IntModule M] [Lean.Grind.OrderedAdd M]
  {k : ℤ} {x : M}, 0 ≤ k → 0 ≤ x → 0 ≤ k • x
-- Mathlib.Algebra.Group.Basic
zpow_iterate : ∀ {G : Type u_3} [inst : Group G] (k : ℤ) (n : ℕ), (fun x => x ^ k)^[n] = fun x => x ^ k ^ n
-- Init.Data.SInt.Lemmas
ISize.neg_mul_comm : ∀ (a b : ISize), -a * b = a * -b
-- Mathlib.Data.List.Induction
/-- Like `reverseRec`, but with the list parameter placed first.  -/
List.reverseRecOn : {α : Type u_1} →
  {motive : List α → Sort u_2} →
    (l : List α) → motive [] → ((l : List α) → (a : α) → motive l → motive (l ++ [a])) → motive l
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_erase : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  m.WF → ∀ {k a : α}, (m.erase k).getKey! a = if (k == a) = true then default else m.getKey! a
-- Mathlib.Algebra.Ring.InjSurj
/-- A type endowed with `0`, `1`, `+` is an additive commutative group with one, if it admits a
surjective map that preserves `0`, `1`, and `+` to an additive commutative group with one.
See note [reducible non-instances].  -/
Function.Surjective.addCommGroupWithOne : {R : Type u_1} →
  {S : Type u_2} →
    (f : R → S) →
      Function.Surjective f →
        [inst : Add S] →
          [inst_1 : Zero S] →
            [inst_2 : One S] →
              [inst_3 : Neg S] →
                [inst_4 : Sub S] →
                  [inst_5 : SMul ℕ S] →
                    [inst_6 : SMul ℤ S] →
                      [inst_7 : NatCast S] →
                        [inst_8 : IntCast S] →
                          [inst_9 : AddCommGroupWithOne R] →
                            f 0 = 0 →
                              f 1 = 1 →
                                (∀ (x y : R), f (x + y) = f x + f y) →
                                  (∀ (x : R), f (-x) = -f x) →
                                    (∀ (x y : R), f (x - y) = f x - f y) →
                                      (∀ (n : ℕ) (x : R), f (n • x) = n • f x) →
                                        (∀ (n : ℤ) (x : R), f (n • x) = n • f x) →
                                          (∀ (n : ℕ), f ↑n = ↑n) → (∀ (n : ℤ), f ↑n = ↑n) → AddCommGroupWithOne S
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigO_const_smul_right : ∀ {α : Type u_1} {E : Type u_3} {E' : Type u_6} {𝕜 : Type u_15} [inst : Norm E] [inst_1 : SeminormedAddCommGroup E']
  [inst_2 : NormedDivisionRing 𝕜] {f : α → E} {f' : α → E'} {l : Filter α} [inst_3 : Module 𝕜 E'] [NormSMulClass 𝕜 E']
  {c : 𝕜}, c ≠ 0 → ((f =O[l] fun x => c • f' x) ↔ f =O[l] f')
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- Given `AddSubsemigroup`s `s`, `t` of `AddSemigroup`s `A`, `B` respectively,
`s × t` as an `AddSubsemigroup` of `A × B`.  -/
AddSubsemigroup.prod : {M : Type u_1} →
  {N : Type u_2} → [inst : Add M] → [inst_1 : Add N] → AddSubsemigroup M → AddSubsemigroup N → AddSubsemigroup (M × N)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_inter_eq_false_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₂.contains k = false → (m₁.inter m₂).contains k = false
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.mem_of_mem_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k : α},
  l.contains k = false → k ∈ Std.ExtDHashMap.Const.insertManyIfNewUnit m l → k ∈ m
-- Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
UpperHalfPlane.gl_smul_I_eq_I_iff_of_neg : ∀ {g : GL (Fin 2) ℝ},
  ↑(Matrix.GeneralLinearGroup.det g) < 0 →
    (g • UpperHalfPlane.I = UpperHalfPlane.I ↔ ↑g 0 0 = -↑g 1 1 ∧ ↑g 0 1 = ↑g 1 0)
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.IsPlot.continuous : ∀ {X : Type u_1} [inst : DiffeologicalSpace X] {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X},
  Diffeology.IsPlot p → Continuous p
-- Mathlib.Tactic.Convert
_private.Mathlib.Tactic.Convert.0.instEvalExprConfig : Lean.Elab.ConfigEval.EvalExpr Congr!.Config
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom_assoc : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f g : X ⟶ Y) (hfg : f = g) (x : ↑X.toTopCat) {Z : CommRingCat}
  (h : X.presheaf.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x) h =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap g x) h)
-- Init.Data.UInt.Bitwise
UInt32.ofBitVec_shiftRight_mod : ∀ (a : BitVec 32) (b : ℕ), { toBitVec := a >>> (b % 32) } = { toBitVec := a } >>> UInt32.ofNat b
-- Mathlib.NumberTheory.NumberField.Units.Basic
/-- The torsion subgroup is cyclic.  -/
NumberField.Units.instIsCyclicSubtypeUnitsRingOfIntegersMemSubgroupTorsion : ∀ (K : Type u_1) [inst : Field K] [NumberField K], IsCyclic ↥(NumberField.Units.torsion K)
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.iUnion_op_vadd_set : ∀ {α : Type u_2} [inst : Add α] (s t : Set α), ⋃ a ∈ t, AddOpposite.op a +ᵥ s = s + t
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] {f g : BoundedOrderHom α β}, (∀ (a : α), f a = g a) → f = g
-- Mathlib.RepresentationTheory.Basic
Representation.directSum_apply : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Monoid G] {ι : Type u_3} {V : ι → Type u_4}
  [inst_2 : (i : ι) → AddCommMonoid (V i)] [inst_3 : (i : ι) → Module k (V i)] (ρ : (i : ι) → Representation k G (V i))
  (g : G), (Representation.directSum ρ) g = DirectSum.lmap fun x => (ρ x) g
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.map_coord_zero : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) {m : (i : ι) → M₁ i} (i : ι), m i = 0 → f m = 0
-- Lean.Compiler.IR.Basic
Lean.IR.instBEqLitVal.beq : Lean.IR.LitVal → Lean.IR.LitVal → Bool
-- Mathlib.Algebra.Algebra.Equiv
/-- See Note [custom simps projection]  -/
AlgEquiv.Simps.toEquiv : {R : Type uR} →
  {A₁ : Type uA₁} →
    {A₂ : Type uA₂} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A₁] →
          [inst_2 : Semiring A₂] → [inst_3 : Algebra R A₁] → [inst_4 : Algebra R A₂] → (A₁ ≃ₐ[R] A₂) → A₁ ≃ A₂
-- Mathlib.Data.Multiset.Sum
/-- Disjoint sum of multisets.  -/
Multiset.disjSum : {α : Type u_1} → {β : Type u_2} → Multiset α → Multiset β → Multiset (α ⊕ β)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
/-- The category of PresheafedSpaces. Morphisms are pairs, a continuous map and a presheaf map
from the presheaf on the target to the pushforward of the presheaf on the source.  -/
AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.Category.{max v_1 u_2, max (max (u_2 + 1) u_1) v_1} (AlgebraicGeometry.PresheafedSpace C)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_of_mem_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α}, a ∈ t.erase k → a ∈ t
-- Init.Data.Iterators.Basic
/-- Asserts that a certain iterator `it'` could plausibly be the directly succeeding iterator of another
given iterator `it` while no value is emitted (see `IterStep.skip`).
 -/
Std.IterM.IsPlausibleSkipSuccessorOf : {α : Type w} → {m : Type w → Type w'} → {β : Type w} → [Std.Iterator α m β] → Std.IterM m β → Std.IterM m β → Prop
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agm_le_agmSequences_snd : ∀ {x y : NNReal} (n : ℕ), x.agm y ≤ (x.agmSequences y n).2
-- Lean.Meta.Instances
Lean.Meta.addDefaultInstanceEntry : Lean.Meta.DefaultInstances → Lean.Meta.DefaultInstanceEntry → Lean.Meta.DefaultInstances
-- Mathlib.RingTheory.Congruence.Hom
/-- Given a ring congruence relation `c` on a semiring `M`, the order-preserving
bijection between the set of ring congruence relations containing `c` and the
ring congruence relations on the quotient of `M` by `c`.  -/
RingCon.correspondence : {M : Type u_1} → [inst : NonAssocSemiring M] → {c : RingCon M} → ↑(Set.Ici c) ≃o RingCon c.Quotient
-- Mathlib.Algebra.Ring.Basic
isDomain_iff_cancelMulZero_and_nontrivial : ∀ (α : Type u_3) [inst : Semiring α], IsDomain α ↔ IsCancelMulZero α ∧ Nontrivial α
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.CodescendsAlong.top : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Q : CategoryTheory.MorphismProperty C},
  ⊤.CodescendsAlong Q
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toPMF_eq_iff_toMeasure_eq : ∀ {α : Type u_1} [inst : Countable α] [inst_1 : MeasurableSpace α] [inst_2 : MeasurableSingletonClass α] (p : PMF α)
  (μ : MeasureTheory.Measure α) [inst_3 : MeasureTheory.IsProbabilityMeasure μ], μ.toPMF = p ↔ μ = p.toMeasure
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate_smul : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (r : α)
  (A : Matrix n n α), (r • A).adjugate = r ^ (Fintype.card n - 1) • A.adjugate
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_mor₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b c : EInt) (hab : a ≤ b)
  (hbc : b ≤ c) (j : C),
  ((t.triangleω₁δ a b c hab hbc).obj j).mor₃ =
    CategoryTheory.CategoryStruct.comp ((t.eTruncGEδLT.app b).app ((t.eTruncLT.obj c).obj j))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor C 1).map
          ((t.eTruncLT.obj b).map ((t.eTruncGEπ a).app ((t.eTruncLT.obj c).obj j))))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctor C 1).map ((t.eTruncLTGEIsoGELT a b).hom.app ((t.eTruncLT.obj c).obj j)))
          ((CategoryTheory.shiftFunctor C 1).map
            ((t.eTruncGE.obj a).map ((t.eTruncLT.obj b).map ((t.eTruncLTι c).app j))))))
-- Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Summable.multipliableLocallyUniformlyOn_nat_one_add : ∀ {α : Type u_1} {K : Set α} {R : Type u_3} [inst : NormedCommRing R] [NormOneClass R] [CompleteSpace R]
  [inst_3 : TopologicalSpace α] [LocallyCompactSpace α] {f : ℕ → α → R},
  IsOpen K →
    ∀ {u : ℕ → ℝ},
      Summable u →
        (∀ᶠ (n : ℕ) in Filter.atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n) →
          (∀ (n : ℕ), ContinuousOn (f n) K) → MultipliableLocallyUniformlyOn (fun n x => 1 + f n x) K
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.nilpotencyLength_eq_zero_iff : ∀ (L : Type v) (M : Type w) [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M]
  [LieModule.IsNilpotent L M], LieModule.nilpotencyLength L M = 0 ↔ Subsingleton M
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.mul.eq_1 : ∀ {M : Type u_4} [inst : MulOneClass M] (S : Submonoid M), S.mul = { mul := fun a b => ⟨↑a * ↑b, ⋯⟩ }
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- The isomorphism giving rise to the lax unity constraint  -/
CategoryTheory.LaxFunctor.PseudoCore.mapIdIso : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F : CategoryTheory.LaxFunctor B C} →
          F.PseudoCore →
            (a : B) → F.map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id (F.obj a)
-- Lean.Server.Requests
Lean.Server.SerializedLspResponse.mk.sizeOf_spec : ∀ (response? : Option Lean.Json) (serialized : String) (isComplete : Bool),
  sizeOf { response? := response?, serialized := serialized, isComplete := isComplete } =
    1 + sizeOf response? + sizeOf serialized + sizeOf isComplete
-- Mathlib.Topology.Order.WithTop
WithBot.tendsto_unbotD : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] (d : ι)
  {a : WithBot ι}, a ≠ ⊥ → Filter.Tendsto (WithBot.unbotD d) (nhds a) (nhds (WithBot.unbotD d a))
-- Plausible.Random
Plausible.Random.instFinSucc : {m : Type → Type u_1} → [Monad m] → {n : ℕ} → Plausible.Random m (Fin n.succ)
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
PiToModule.fromEnd_apply_single_one : ∀ {ι : Type u_1} [inst : Fintype ι] {M : Type u_2} [inst_1 : AddCommGroup M] (R : Type u_3) [inst_2 : CommRing R]
  [inst_3 : Module R M] (b : ι → M) [inst_4 : DecidableEq ι] (f : Module.End R M) (i : ι),
  ((PiToModule.fromEnd R b) f) (Pi.single i 1) = f (b i)