mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.GroupWithZero.Units.Fintype
Fintype.card_eq_card_units_add_one : ∀ (α : Type u_1) [inst : GroupWithZero α] [inst_1 : Fintype α] [inst_2 : DecidableEq α],
  Fintype.card α = Fintype.card αˣ + 1
-- Mathlib.Control.Fold
Monoid.foldlM : (m : Type u → Type u) → [Monad m] → Type u → Type u
-- Mathlib.RingTheory.TensorProduct.Free
Algebra.TensorProduct.basis_repr_tmul : ∀ {R : Type u_1} {A : Type u_2} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (b : Module.Basis ι R M) (a : A) (m : M),
  (Algebra.TensorProduct.basis A b).repr (a ⊗ₜ[R] m) = a • Finsupp.mapRange ⇑(algebraMap R A) ⋯ (b.repr m)
-- Std.Data.TreeMap.Basic
/-- Folds the given monadic function over the mappings in the map in descending order.  -/
Std.TreeMap.foldrM : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {δ : Type w} → {m : Type w → Type w₂} → [Monad m] → (α → β → δ → m δ) → δ → Std.TreeMap α β cmp → m δ
-- Mathlib.Order.Filter.Pointwise
Filter.instVAddFilter.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β],
  Filter.instVAddFilter = { vadd := fun a => Filter.map fun x => a +ᵥ x }
-- Mathlib.Analysis.Normed.Field.Lemmas
/-- Eta-expanded form of `TendstoLocallyUniformly.inv₀_of_disjoint` -/
TendstoLocallyUniformly.fun_inv₀_of_disjoint : ∀ {α : Type u_1} [inst : NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [inst_1 : TopologicalSpace X]
  {F : ι → X → α} {f : X → α} {l : Filter ι},
  TendstoLocallyUniformly F f l →
    (∀ (x : X), Disjoint (Filter.map f (nhds x)) (nhds 0)) →
      TendstoLocallyUniformly (fun i i_1 => (F i i_1)⁻¹) (fun i => (f i)⁻¹) l
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.trStAct.eq_3 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] {k : K}
  (q : Turing.TM1.Stmt (Turing.TM2to1.Γ' K Γ) (Turing.TM2to1.Λ' K Γ Λ σ) σ) (f : σ → Option (Γ k) → σ),
  Turing.TM2to1.trStAct q (Turing.TM2to1.StAct.pop f) =
    Turing.TM1.Stmt.branch (fun a x => a.1) (Turing.TM1.Stmt.load (fun x s => f s none) q)
      (Turing.TM1.Stmt.move Turing.Dir.left
        (Turing.TM1.Stmt.load (fun a s => f s (a.2 k))
          (Turing.TM1.Stmt.write (fun a x => (a.1, Function.update a.2 k none)) q)))
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_erase_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α], (↑m).WF → ∀ {k : α}, Std.DHashMap.Internal.Raw₀.Const.get? (m.erase k) k = none
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Int.castDef.eq_1 : ∀ {R : Type u} [inst : NatCast R] [inst_1 : Neg R] (n : ℕ), (Int.ofNat n).castDef = ↑n
-- Init.Data.Order.Classes
/-- This typeclass states that being less or equal to `min a b` is equivalent to being less or
equal to both `a` and `b`..
 -/
Std.LawfulOrderInf : (α : Type u) → [Min α] → [LE α] → Prop
-- Init.System.IOError
IO.Error.userError.inj : ∀ {msg msg_1 : String}, IO.Error.userError msg = IO.Error.userError msg_1 → msg = msg_1
-- Mathlib.Topology.Order.LiminfLimsup
/-- Ad hoc typeclass stating that neighborhoods are eventually bounded above.  -/
BoundedLENhdsClass : (α : Type u_7) → [Preorder α] → [TopologicalSpace α] → Prop
-- Mathlib.Data.Multiset.DershowitzManna
Multiset.instWellFoundedIsDershowitzMannaLT : {α : Type u_1} → [inst : Preorder α] → [WellFoundedLT α] → WellFoundedRelation (Multiset α)
-- Mathlib.Order.CompleteLattice.Lemmas
codisjoint_of_sInf_codisjoint : ∀ {α : Type u_1} [inst : CompleteLattice α] {a b : Set α}, Codisjoint (sInf a) (sInf b) → ⊤ ∉ a ∨ ⊤ ∉ b → Disjoint a b
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
/-- The plausible-step predicate for `Flatten` iterators  -/
Std.Iterators.Types.Flatten.IsPlausibleStep : {α α₂ β : Type w} →
  {m : Type w → Type w'} →
    [Std.Iterator α m (Std.IterM m β)] → [Std.Iterator α₂ m β] → Std.IterM m β → Std.IterStep (Std.IterM m β) β → Prop
-- Init.Data.Range.Polymorphic.Nat
Std.instHasRcoIntersectionNat_2 : Std.Roi.HasRcoIntersection ℕ
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Set.ncard_smul_set : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (a : G) (s : Set α), (a • s).ncard = s.ncard
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instAddCommMonoid : {R : Type u_3} → {A : Type u_4} → [AddCommMonoid R] → [AddCommMonoid A] → AddCommMonoid (Unitization R A)
-- Lean.Meta.Tactic.FunIndInfo
/-- A `FunIndInfo` indicates how a function's arguments map to the arguments of the functional induction
(resp. cases) theorem.

The size of `params` also indicates the arity of the function.
 -/
Lean.Meta.FunIndInfo : Type
-- Mathlib.Data.Set.Restrict
Set.MapsTo.restrict_commutes : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) (t : Set β) (h : Set.MapsTo f s t),
  Subtype.val ∘ Set.MapsTo.restrict f s t h = f ∘ Subtype.val
-- Mathlib.Data.Fintype.Basic
Fin.univ_image_get' : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (l : List α) (f : α → β),
  Finset.image (fun x => f (l.get x)) Finset.univ = (List.map f l).toFinset
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- Given any distinguished triangle
```
      f       g       h
  X  ───> Y  ───> Z  ───> X⟦1⟧
```
the composition `h ≫ f⟦1⟧ = 0`.  -/
CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj T.obj₂ ⟶ Z),
      CategoryTheory.CategoryStruct.comp T.mor₃
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map T.mor₁) h) =
        CategoryTheory.CategoryStruct.comp 0 h
-- Init.PropLemmas
Decidable.or_iff_not_not_and_not : ∀ {a b : Prop} [Decidable a] [Decidable b], a ∨ b ↔ ¬(¬a ∧ ¬b)
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.limNthHom_one : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)]
  (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1),
  PadicInt.limNthHom f_compat 1 = 1
-- Init.Data.Rat.Lemmas
Rat.abs_neg : ∀ {x : ℚ}, (-x).abs = x.abs
-- Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
GenContFract.coe_of_s_rat_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] [IsStrictOrderedRing K] {v : K}
  {q : ℚ}, v = ↑q → Stream'.Seq.map (GenContFract.Pair.map Rat.cast) (GenContFract.of q).s = (GenContFract.of v).s
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernel.zeroCokernelCofork_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasZeroObject C],
  (CategoryTheory.Limits.cokernel.zeroCokernelCofork f).pt = 0
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_C_mul_X_pow : ∀ {R : Type u} {a : R} [inst : Semiring R] (n : ℕ), a ≠ 0 → (Polynomial.C a * Polynomial.X ^ n).degree = ↑n
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.union_insert_right_eq_insert_union : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {p : (_ : α) × β}, m₁ ∪ m₂.insert p.fst p.snd = (m₁ ∪ m₂).insert p.fst p.snd
-- Mathlib.Algebra.Ring.CompTypeclasses
/-- `σ'` is a left inverse of `σ`  -/
RingHomInvPair.comp_eq : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {inst : Semiring R₁} {inst_1 : Semiring R₂} {σ : R₁ →+* R₂}
  {σ' : outParam (R₂ →+* R₁)} [self : RingHomInvPair σ σ'], σ'.comp σ = RingHom.id R₁
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.lineMap.congr_simp : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] (p₀ p₀_1 : P),
  p₀ = p₀_1 →
    ∀ (p₁ p₁_1 : P),
      p₁ = p₁_1 →
        ∀ [inst_5 : TopologicalSpace R] [inst_6 : TopologicalSpace V] [inst_7 : ContinuousSMul R V]
          [inst_8 : ContinuousVAdd V P], ContinuousAffineMap.lineMap p₀ p₁ = ContinuousAffineMap.lineMap p₀_1 p₁_1
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.content_eq_gcd_range_of_lt : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] (p : Polynomial R) (n : ℕ),
  p.natDegree < n → p.content = (Finset.range n).gcd p.coeff
-- Mathlib.RingTheory.LocalProperties.Basic
Ideal.localized'_eq_map : ∀ {R : Type u_1} (S : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (p : Submonoid R) [inst_3 : IsLocalization p S] (I : Ideal R),
  Submodule.localized' S p (Algebra.linearMap R S) I = Ideal.map (algebraMap R S) I
-- Mathlib.CategoryTheory.SingleObj
MonCat.toCat_full : MonCat.toCat.Full
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_filter_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {f : α → β → Bool}, (Std.HashMap.filter f m).isEmpty = true ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) m[k] = false
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.curryRight_norm : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G), ‖f.curryRight‖ = ‖f‖
-- Mathlib.Data.Num.Lemmas
Num.size_to_nat : ∀ (n : Num), ↑n.size = (↑n).size
-- Mathlib.AlgebraicTopology.SimplicialObject.II
SimplexCategory.II.last_mem_finset : ∀ {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) (x : Fin (m + 2)), Fin.last (n + 1) ∈ SimplexCategory.II.finset f x
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.Birational.trans : ∀ {X Y Z : AlgebraicGeometry.Scheme}, X.Birational Y → Y.Birational Z → X.Birational Z
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.vadd_ae_eq_of_ae_eq : ∀ {G : Type u_5} {α : Type u_6} [inst : AddGroup G] [inst_1 : AddAction G α] {x : MeasurableSpace α} {s t : Set α}
  {μ : MeasureTheory.Measure α} (g : G),
  MeasureTheory.Measure.QuasiMeasurePreserving (fun x => -g +ᵥ x) μ μ → s =ᵐ[μ] t → g +ᵥ s =ᵐ[μ] g +ᵥ t
-- Mathlib.Order.Hom.Bounded
BotHom.bot_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : LE β] [inst_2 : OrderBot β] (a : α), ⊥ a = ⊥
-- Std.Data.ByteSlice
instSliceableByteSliceNat_7 : Std.Rio.Sliceable ByteSlice ℕ ByteSlice
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- The canonical isomorphism `G/(ker φ) ≃+ H` induced by a surjection `φ : G →+ H`.
For a `computable` version, see `QuotientAddGroup.quotientKerEquivOfRightInverse`.  -/
QuotientAddGroup.quotientKerEquivOfSurjective : {G : Type u} →
  [inst : AddGroup G] → {H : Type v} → [inst_1 : AddGroup H] → (φ : G →+ H) → Function.Surjective ⇑φ → G ⧸ φ.ker ≃+ H
-- Init.Data.Vector.Count
Vector.count_flatMap : ∀ {β : Type u_1} {n m : ℕ} {α : Type u_2} [inst : BEq β] {xs : Vector α n} {f : α → Vector β m} {x : β},
  Vector.count x (xs.flatMap f) = (Vector.map (Vector.count x ∘ f) xs).sum
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- Convert a binary rooted tree to a Dyck word.

`g(nil) = 0`. A nonempty tree with left subtree `l` and right subtree `r`
is sent to `g(l).nest + g(r)`.  -/
DyckWord.ofTree : BinaryTree Unit → DyckWord
-- Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
/-- The inversion with center `c` and radius `R` maps a sphere passing through the center to a
hyperplane.  -/
EuclideanGeometry.inversion_mem_perpBisector_inversion_iff' : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c x y : P} {R : ℝ},
  R ≠ 0 →
    y ≠ c →
      (EuclideanGeometry.inversion c R x ∈ AffineSubspace.perpBisector c (EuclideanGeometry.inversion c R y) ↔
        dist x y = dist y c ∧ x ≠ c)
-- Lean.ResolveName
/-- Given a namespace name, return a list of possible interpretations.
Names extracted from syntax should be passed to `resolveNamespace` instead.
 -/
Lean.resolveNamespaceCore : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadResolveName m] →
      [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Name → optParam Bool false → m (List Lean.Name)
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.unreachable.sizeOf_spec : sizeOf Lean.IR.FnBody.unreachable = 1
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.pullback₃.π.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)],
  CategoryTheory.Functor.relativelyRepresentable.pullback₃.π hf₁ f₂ f₃ =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁ hf₁ f₂ f₃))
      f₁
-- Mathlib.Topology.Algebra.InfiniteSum.Module
QuotientAddGroup.automorphize.eq_1 : ∀ {M : Type u_11} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M] {G : Type u_13} [inst_2 : AddGroup G]
  {Γ : AddSubgroup G} (f : G → M), QuotientAddGroup.automorphize f = AddAction.automorphize f
-- Mathlib.Computability.RegularExpressions
RegularExpression.matches'.eq_4 : ∀ {α : Type u_1} (P Q : RegularExpression α), (P.plus Q).matches' = P.matches' + Q.matches'
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- The isomorphism `tensorObj X₁ Y₁ ≅ tensorObj X₂ Y₂` induced by isomorphisms of graded
objects `e : X₁ ≅ X₂` and `e' : Y₁ ≅ Y₂`.  -/
CategoryTheory.GradedObject.Monoidal.tensorIso : {I : Type u} →
  [inst : AddMonoid I] →
    {C : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          {X₁ X₂ Y₁ Y₂ : CategoryTheory.GradedObject I C} →
            (X₁ ≅ X₂) →
              (Y₁ ≅ Y₂) →
                [inst_3 : X₁.HasTensor Y₁] →
                  [inst_4 : X₂.HasTensor Y₂] →
                    CategoryTheory.GradedObject.Monoidal.tensorObj X₁ Y₁ ≅
                      CategoryTheory.GradedObject.Monoidal.tensorObj X₂ Y₂
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.single_mem_cycles₂_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (g : G × G) (a : ↑A),
  (fun₀ | g => a) ∈ groupHomology.cycles₂ A ↔
    (fun₀ | g.1 * g.2 => (A.ρ g.1) a) = (fun₀ | g.2 => a) + fun₀ | g.1 => (A.ρ g.1) a
-- Mathlib.Order.Lex
instNontrivialColex : ∀ (α : Type u_2) [Nontrivial α], Nontrivial (Colex α)
-- Std.Do.WP.SimpLemmas
Std.Do.WP.bind : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α β : Type u} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (x : m α)
  (f : α → m β) (Q : Std.Do.PostCond β ps),
  (Std.Do.wp (x >>= f)).apply Q = (Std.Do.wp x).apply (fun a => (Std.Do.wp (f a)).apply Q, Q.2)
-- Mathlib.Logic.Equiv.Basic
/-- `Unique (Unique α)` is equivalent to `Unique α`.  -/
uniqueUniqueEquiv : {α : Sort u_1} → Unique (Unique α) ≃ Unique α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- The function `Real.cosh` is real analytic.  -/
Real.analyticOn_cosh : ∀ {s : Set ℝ}, AnalyticOn ℝ Real.cosh s
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.interSmallerFn.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3)
  (h_1 : (kv' : (a : α) × β a) → motive (some kv')) (h_2 : Unit → motive none),
  (match none with
    | some kv' => h_1 kv'
    | none => h_2 ()) =
    h_2 ()
-- Init.Data.Nat.Div.Basic
Nat.div.go.eq_def : ∀ (y : ℕ) (hy : 0 < y) (fuel x : ℕ) (hfuel : x < fuel),
  Nat.div.go y hy fuel x hfuel =
    match fuel, hfuel with
    | fuel.succ, hfuel => if h : y ≤ x then Nat.div.go y hy fuel (x - y) ⋯ + 1 else 0
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.Option.orElse.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → (Unit → Option α) → Sort u_2) (b : Unit → Option α)
  (h_1 : (a : α) → (x : Unit → Option α) → motive (some a) x) (h_2 : (b : Unit → Option α) → motive none b),
  (match none, b with
    | some a, x => h_1 a x
    | none, b => h_2 b) =
    h_2 b
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticRelatedInformation.location : Lean.Lsp.DiagnosticRelatedInformation → Lean.Lsp.Location
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.invariants_le_invariants_restrict : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Ring R] [inst_2 : AddCommGroup V]
  [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V] {H : Type u_6}
  [inst_6 : Monoid H] (π : ContRepresentation R G V) (φ : H →* G), π.invariants ≤ (π.restrict φ).invariants
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.isRegular_prod_X : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (s : Finset σ), IsRegular (∏ n ∈ s, MvPolynomial.X n)
-- Mathlib.Tactic.Module
_private.Mathlib.Tactic.Module.0.Mathlib.Tactic.Module.qNF.add.match_1.eq_1 : ∀ {u v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)}
  (motive : Mathlib.Tactic.Module.qNF R M → Mathlib.Tactic.Module.qNF R M → Sort u_1)
  (l : Mathlib.Tactic.Module.qNF R M) (h_1 : (l : Mathlib.Tactic.Module.qNF R M) → motive [] l)
  (h_2 : (l : Mathlib.Tactic.Module.qNF R M) → motive l [])
  (h_3 :
    (a₁ : Q(«$R»)) →
      (x₁ : Q(«$M»)) →
        (k₁ : ℕ) →
          (t₁ : Mathlib.Tactic.Module.NF (Q(«$R») × Q(«$M»)) ℕ) →
            (a₂ : Q(«$R»)) →
              (x₂ : Q(«$M»)) →
                (k₂ : ℕ) →
                  (t₂ : Mathlib.Tactic.Module.NF (Q(«$R») × Q(«$M»)) ℕ) →
                    motive (((a₁, x₁), k₁) :: t₁) (((a₂, x₂), k₂) :: t₂)),
  (match [], l with
    | [], l => h_1 l
    | l, [] => h_2 l
    | ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ => h_3 a₁ x₁ k₁ t₁ a₂ x₂ k₂ t₂) =
    h_1 l
-- Mathlib.Algebra.GCDMonoid.FinsetLemmas
Finset.associated_lcm_prod : ∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset ι}
  {f : ι → α}, (↑s).Pairwise (Function.onFun IsRelPrime f) → Associated (s.lcm f) (s.prod f)
-- Mathlib.Condensed.Light.Monoidal
LightCondensed.instMonoidalCategoryLightCondMod : (R : Type u) → [inst : CommRing R] → CategoryTheory.MonoidalCategory (LightCondMod R)
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.smul_zero_nonneg : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] {f : Filter α},
  f.NeBot → 0 ≤ f • 0
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.instInhabited : {M : Type u_1} → [inst : Add M] → Inhabited (AddSubsemigroup M)
-- Init.While
Lean.Loop.mk.sizeOf_spec : sizeOf { } = 1
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
CategoryTheory.TwoSquare.CostructuredArrowDownwards.mk.congr_simp : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) {X₂ : C₂}
  {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃) (X₁ : C₁) (a a_1 : X₂ ⟶ T.obj X₁) (e_a : a = a_1) (b b_1 : L.obj X₁ ⟶ X₃)
  (e_b : b = b_1)
  (comm : CategoryTheory.CategoryStruct.comp (R.map a) (CategoryTheory.CategoryStruct.comp (w.app X₁) (B.map b)) = g),
  CategoryTheory.TwoSquare.CostructuredArrowDownwards.mk w g X₁ a b comm =
    CategoryTheory.TwoSquare.CostructuredArrowDownwards.mk w g X₁ a_1 b_1 ⋯
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₁.of.sizeOf_spec : ∀ (a : Mathlib.Tactic.BicategoryLike.Atom₁), sizeOf (Mathlib.Tactic.BicategoryLike.Mor₁.of a) = 1 + sizeOf a
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
MonotoneOn.nnnorm_cfc : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A] [inst_3 : PartialOrder A]
  [inst_4 : StarOrderedRing A] [inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_6 : NonnegSpectrumClass ℝ A] [Nontrivial A] (f : NNReal → NNReal) (a : A),
  MonotoneOn f (spectrum NNReal a) →
    autoParam (ContinuousOn f (spectrum NNReal a)) MonotoneOn.nnnorm_cfc._auto_1 →
      autoParam (0 ≤ a) MonotoneOn.nnnorm_cfc._auto_3 → ‖cfc f a‖₊ = f ‖a‖₊
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.coxeterWeight_zero_iff_isOrthogonal : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {i j : ι} [NeZero 2]
  [IsDomain R], P.coxeterWeight i j = 0 ↔ P.IsOrthogonal i j
-- Mathlib.Combinatorics.Graph.Basic
/-- `G.loopSet x` is the set of loops at `x` in `G`.  -/
Graph.loopSet : {α : Type u_1} → {β : Type u_2} → {G : Graph α β} → α → Set β
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.ThinSkeleton.skeletal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [Quiver.IsThin C],
  CategoryTheory.Skeletal (CategoryTheory.ThinSkeleton C)
-- Mathlib.NumberTheory.Padics.PadicNumbers
/-- The rational-valued `p`-adic norm on `ℚ_[p]` is lifted from the norm on Cauchy sequences. The
canonical form of this function is the normed space instance, with notation `‖ ‖`.  -/
padicNormE : {p : ℕ} → [hp : Fact (Nat.Prime p)] → AbsoluteValue ℚ_[p] ℚ
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasurableEmbedding.variation_transpose_map : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {β : Type u_9}
  [inst_6 : MeasurableSpace β] {φ : X → β},
  MeasurableEmbedding φ → ((μ.map φ).transpose B).variation = MeasureTheory.Measure.map φ (μ.transpose B).variation
-- Mathlib.Algebra.Polynomial.Degree.Support
Polynomial.as_sum_range' : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ),
  p.natDegree < n → p = ∑ i ∈ Finset.range n, (Polynomial.monomial i) (p.coeff i)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.GeneratingSections.mapFreeHom.eq_1 : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₁} [inst_3 : CategoryTheory.Category.{v₁, u₁} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  {M : SheafOfModules R} (G : M.GeneratingSections) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S))
  [inst_6 :
    CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v',
        max (max (u + 1) u₁) v₁}
      F]
  (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)),
  G.mapFreeHom F η = CategoryTheory.CategoryStruct.comp (SheafOfModules.mapFreeIso F G.I η).hom (F.map G.π)
-- Std.Internal.Do.WP.Basic
Std.Internal.Do.PredTrans.apply_pushExcept : ∀ {α : Type u_1} {ε : Type u_2} {Pred : Type u_3} {EPred : Type u_4}
  (x : Std.Internal.Do.PredTrans Pred EPred (Except ε α)) (post : α → Pred) (epost : EPost.Cons✝ (ε → Pred) EPred),
  x.pushExcept.apply post epost = x.apply (Std.Internal.Do.EPost.Cons.pushExcept post epost) epost.tail