mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_vecMul : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace R]
  [inst_2 : NonUnitalNonAssocSemiring R] [ContinuousAdd R] [ContinuousMul R] [inst_5 : Fintype m] {A : X → m → R}
  {B : X → Matrix m n R}, Continuous A → Continuous B → Continuous fun x => Matrix.vecMul (A x) (B x)
-- Mathlib.GroupTheory.Index
/-- A subgroup `H` has index two if and only if there exists `a ∉ H` such that for all `b`, one
of `b * a` and `b` belongs to `H`.  -/
Subgroup.index_eq_two_iff_exists_notMem_and : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.index = 2 ↔ ∃ a ∉ H, ∀ (b : G), b * a ∈ H ∨ b ∈ H
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.HomologySequence.exact₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C))
  (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ n₁ : ℤ)
  (h : autoParam (n₀ + 1 = n₁) DerivedCategory.HomologySequence.exact₃._auto_1),
  { X₁ := (DerivedCategory.homologyFunctor C n₀).obj T.obj₂, X₂ := (DerivedCategory.homologyFunctor C n₀).obj T.obj₃,
      X₃ := (DerivedCategory.homologyFunctor C n₁).obj T.obj₁, f := (DerivedCategory.homologyFunctor C n₀).map T.mor₂,
      g := DerivedCategory.HomologySequence.δ T n₀ n₁ h, zero := ⋯ }.Exact
-- Mathlib.Topology.Connected.PathComponentOne
OpenNormalAddSubgroup.instIsClosedCoePathComponentZero : ∀ (G : Type u_1) [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : LocallyPathConnectedSpace G], IsClosed ↑(OpenNormalAddSubgroup.pathComponentZero G)
-- Mathlib.Topology.Sober
IsGenericPoint.image : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {x : α} {S : Set α},
  IsGenericPoint x S → ∀ {f : α → β}, Continuous f → IsGenericPoint (f x) (closure (f '' S))
-- Mathlib.Algebra.Ring.Defs
/-- A unital but not-necessarily-associative ring.  -/
NonAssocRing : Type u_1 → Type u_1
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.ofNat_lt_aleph0 : ∀ {n : ℕ} [inst : n.AtLeastTwo], OfNat.ofNat n < Cardinal.aleph0
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.ofNat_eq_map_iff : ∀ {α : Type u} {β : Type v} [inst : AddMonoidWithOne α] {f : β → α} {n : ℕ} [inst_1 : n.AtLeastTwo] {a : WithTop β},
  OfNat.ofNat n = WithTop.map f a ↔ ∃ x, a = ↑x ∧ f x = ↑n
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.instElemOrbit : {M : Type u_1} →
  {α : Type u_3} → [inst : Monoid M] → [inst_1 : MulAction M α] → {a : α} → MulAction M ↑(MulAction.orbit M a)
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.totalShift₂XIso.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)]
  (n n' : ℤ) (h : n + y = n'), K.totalShift₂XIso y n n' h = K.totalShift₂XIso y n n' h
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
ContinuousLinearMap.rayleighQuotient_zero_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E), ContinuousLinearMap.rayleighQuotient 0 x = 0
-- Mathlib.Data.EReal.Operations
/-- For any extended real number `x` which is not `⊥`, the sum of `⊤` and `x` is equal to `⊤`.  -/
EReal.top_add_of_ne_bot : ∀ {x : EReal}, x ≠ ⊥ → ⊤ + x = ⊤
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.coe_map_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) (s : LowerSet α),
  ↑((LowerSet.map f) s) = ⇑f '' ↑s
-- Init.Grind.PP
Lean.Grind.node_def : ℕ → {α : Sort u} → {a : α} → NodeDef
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Empty
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.Empty.0.Std.IterM.forIn'_eq_match_step.match_1.eq_2 : ∀ {γ : Type u_1} (motive : ForInStep γ → Sort u_2) (c : γ) (h_1 : (c : γ) → motive (ForInStep.yield c))
  (h_2 : (c : γ) → motive (ForInStep.done c)),
  (match ForInStep.done c with
    | ForInStep.yield c => h_1 c
    | ForInStep.done c => h_2 c) =
    h_2 c
-- Std.Data.ExtTreeMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `none`.
The result in the `some` case is guaranteed to be pointer equal to the key in the map.
 -/
Std.ExtTreeMap.getKey? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → Option α
-- Mathlib.Order.Bounded
Set.unbounded_lt_Ici : ∀ {α : Type u_1} [inst : SemilatticeSup α] (a : α), Set.Unbounded (fun x1 x2 => x1 < x2) (Set.Ici a)
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.coe_tosSupHom : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : CompleteLatticeHom α β),
  ⇑f.tosSupHom = ⇑f
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.apply_prod_le_sum_map : ∀ {α : Type u_5} {β : Type u_6} [inst : Monoid α] [inst_1 : AddMonoid β] [inst_2 : Preorder β] [AddLeftMono β]
  (l : List α) (f : α → β), f 1 ≤ 0 → (∀ (a b : α), f (a * b) ≤ f a + f b) → f l.prod ≤ (List.map f l).sum
-- Init.Data.Array.Attach
Array.mem_unattach : ∀ {α : Type u_1} {p : α → Prop} {xs : Array { x // p x }} {a : α}, a ∈ xs.unattach ↔ ∃ (h : p a), ⟨a, h⟩ ∈ xs
-- Mathlib.Topology.Category.CompactlyGenerated
CompactlyGenerated.isoOfHomeo_hom : ∀ {X Y : CompactlyGenerated} (f : ↑X.toTop ≃ₜ ↑Y.toTop),
  (CompactlyGenerated.isoOfHomeo f).hom = CompactlyGenerated.ofHom { toFun := ⇑f, continuous_toFun := ⋯ }
-- Mathlib.Algebra.Order.Ring.Finset
/-- Also see `Finset.sup'_mul₀` for a version for `GroupWithZero`s.  -/
Finset.sup_mul₀ : ∀ {R : Type u_1} {ι : Type u_2} [inst : LinearOrder R] [inst_1 : NonUnitalNonAssocSemiring R] [CanonicallyOrderedAdd R]
  [inst_3 : OrderBot R] (s : Finset ι) (f : ι → R) (a : R), s.sup f * a = s.sup fun x => f x * a
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.Coloring.valid : ∀ {V : Type u} {G : SimpleGraph V} {α : Type u_2} (C : G.Coloring α) {v w : V}, G.Adj v w → C v ≠ C w
-- Mathlib.Topology.Homotopy.TopCat.Basic
/-- The morphism `X ⊗ I ⟶ Y` that is part of a homotopy between two morphisms in `TopCat`.  -/
TopCat.Homotopy.h : {X Y : TopCat} →
  {f₀ f₁ : X ⟶ Y} → TopCat.Homotopy f₀ f₁ → (CategoryTheory.MonoidalCategoryStruct.tensorObj X TopCat.I ⟶ Y)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem_ofList_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k k' : α},
  (k == k') = true →
    ∀ {v : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l → ∀ {h : k' ∈ Std.ExtHashMap.ofList l}, (Std.ExtHashMap.ofList l)[k'] = v
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.exists_ne_one_of_prod_ne_one : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] {f : ι → M}, ∏ x ∈ s, f x ≠ 1 → ∃ a ∈ s, f a ≠ 1
-- Mathlib.Algebra.Order.Group.Abs
/-- `|a / b|ₘ ≤ n` if `1 ≤ a ≤ n` and `1 ≤ b ≤ n`.  -/
mabs_div_le_of_one_le_of_le : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b n : G},
  1 ≤ a → a ≤ n → 1 ≤ b → b ≤ n → |a / b|ₘ ≤ n
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionParams.textDocument : Lean.Lsp.CodeActionParams → Lean.Lsp.TextDocumentIdentifier
-- Mathlib.Combinatorics.Quiver.Schreier
/-- The labelling of arrows in a Schreier graph by elements of `S`.
This is encoded as a prefunctor to `SingleObj S`.  -/
Quiver.SchreierGraph.labelling : (V : Type u_1) →
  {M : Type u_2} → [inst : SMul M V] → {S : Type u_3} → (ι : S → M) → Quiver.SchreierGraph V ι ⥤q Quiver.SingleObj S
-- Init.Data.BitVec.Basic
BitVec.not_eq : ∀ {w : ℕ} (x : BitVec w), x.not = ~~~x
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.equivCostructuredArrow_functor : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C),
  (CategoryTheory.Limits.Cone.equivCostructuredArrow F).functor = CategoryTheory.Limits.Cone.toCostructuredArrow F
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.toSubgroup_sup : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : SeparatelyContinuousMul G]
  (U V : OpenSubgroup G), ↑(U ⊔ V) = ↑U ⊔ ↑V
-- Mathlib.NumberTheory.LocalField.Basic
IsNonarchimedeanLocalField.instIsAdicCompleteSubtypeMemSubringIntegerValueGroupWithZeroValuationMaximalIdeal : ∀ (K : Type u_1) [inst : Field K] [inst_1 : ValuativeRel K] [inst_2 : UniformSpace K] [IsUniformAddGroup K]
  [inst_4 : IsNonarchimedeanLocalField K],
  IsAdicComplete (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer) ↥(ValuativeRel.valuation K).integer
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.instIsLocalizationHoCatToHoCatWeakEquivalences : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  HomotopicalAlgebra.BifibrantObject.toHoCat.IsLocalization
    (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.BifibrantObject C))
-- Mathlib.Algebra.WithConv
/-- Converts an element of `A` to `WithConv A`.  -/
WithConv.toConv : {A : Sort u_1} → A → WithConv A
-- Mathlib.Topology.DiscreteSubset
/-- A set `s` is discrete iff for every `t ⊆ s` there is an open `u` with `u ∩ s = t`.
See `isDiscrete_iff_forall_mem_exists_isOpen` for a similar version of this with singletons.  -/
isDiscrete_iff_forall_subset_exists_isOpen : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsDiscrete s ↔ ∀ t ⊆ s, ∃ u, IsOpen u ∧ u ∩ s = t
-- Std.Internal.Parsec.Basic
/-- Peeks at the next element, returns `some elem` if it satisfies `p`, else `none`. Does not consume input.
 -/
Std.Internal.Parsec.peekWhen? : {ι elem idx : Type} →
  [inst : DecidableEq idx] →
    [inst_1 : DecidableEq elem] →
      [Std.Internal.Parsec.Input ι elem idx] → (elem → Bool) → Std.Internal.Parsec ι (Option elem)
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.mk.sizeOf_spec : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} [inst_1 : SizeOf 𝒮]
  (base : 𝒮) (fiber : ↑(F.obj { as := Opposite.op base })),
  sizeOf { base := base, fiber := fiber } = 1 + sizeOf base + sizeOf fiber
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
Homeomorph.transOpenPartialHomeomorph_apply : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : X ≃ₜ Y) (f' : OpenPartialHomeomorph Y Z),
  ↑(e.transOpenPartialHomeomorph f') = ↑f' ∘ ⇑e
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.hom_ext_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C}
  {f g : P ⟶ Q}, f = g ↔ f.f = g.f
-- Mathlib.Algebra.BigOperators.ModEq
Int.ModEq.listProd_map : ∀ {α : Type u_1} {n : ℤ} {l : List α} {f g : α → ℤ},
  (∀ x ∈ l, f x ≡ g x [ZMOD n]) → (List.map f l).prod ≡ (List.map g l).prod [ZMOD n]
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- A version of `OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary` that works for bases with
different index types.  -/
OrthonormalBasis.toMatrix_orthonormalBasis_self_mul_conjTranspose : ∀ {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] [inst_5 : Fintype ι']
  (a : OrthonormalBasis ι 𝕜 E) (b : OrthonormalBasis ι' 𝕜 E),
  a.toBasis.toMatrix ⇑b * (a.toBasis.toMatrix ⇑b).conjTranspose = 1
-- Mathlib.Algebra.Homology.HomologicalComplexAbelian
HomologicalComplex.exact_of_degreewise_exact : ∀ {C : Type u_1} {ι : Type u_2} {c : ComplexShape ι} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (HomologicalComplex C c)),
  (∀ (i : ι), (S.map (HomologicalComplex.eval C c i)).Exact) → S.Exact
-- Mathlib.Algebra.GCDMonoid.Basic
instNonemptyStrongNormalizationMonoid : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [StrongNormalizationMonoid α], Nonempty (StrongNormalizationMonoid α)
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.sheafToPresheaf_isRightAdjoint : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w)
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD]
  [∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [(CategoryTheory.forget D).ReflectsIsomorphisms], (CategoryTheory.sheafToPresheaf J D).IsRightAdjoint
-- Mathlib.Order.Cover
reflTransGen_wcovBy_eq_reflTransGen_covBy : ∀ {α : Type u_1} [inst : PartialOrder α],
  (Relation.ReflTransGen fun x1 x2 => x1 ⩿ x2) = Relation.ReflTransGen fun x1 x2 => x1 ⋖ x2
-- Mathlib.Topology.Algebra.OpenSubgroup
AddSubgroup.instDiscreteTopologyQuotientOfSeparatelyContinuousAdd : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousAdd G] (U : OpenAddSubgroup G),
  DiscreteTopology (G ⧸ ↑U)
-- Mathlib.Analysis.Normed.Group.Basic
SeminormedGroup.toNNNorm.eq_1 : ∀ {E : Type u_5} [inst : SeminormedGroup E], SeminormedGroup.toNNNorm = { nnnorm := fun a => NNReal.mk ‖a‖ ⋯ }
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_eq_some_getKeyD_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a fallback : α}, t.contains a = true → t.getKey? a = some (t.getKeyD a fallback)
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.val_dvd_le : ∀ {R : Type u} [inst : EuclideanDomain R] (a b : R), b ∣ a → a ≠ 0 → ¬EuclideanDomain.r a b
-- Mathlib.Data.Fintype.EquivFin
Int.infinite : Infinite ℤ
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.val_add : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  (x y : P.Cotangent), (x + y).val = x.val + y.val
-- Mathlib.Data.Finset.MulAntidiagonal
Set.IsPWO.mul : ∀ {α : Type u_1} {s t : Set α} [inst : CommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelMonoid α],
  s.IsPWO → t.IsPWO → (s * t).IsPWO
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.le_op_iff : ∀ {M : Type u_2} [inst : AddZeroClass M] {S₁ : AddSubmonoid Mᵃᵒᵖ} {S₂ : AddSubmonoid M}, S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- Eta-expanded form of `HasDerivAtFilter.neg` -/
HasDerivAtFilter.fun_neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {L : Filter (𝕜 × 𝕜)},
  HasDerivAtFilter f f' L → HasDerivAtFilter (fun i => -f i) (-f') L
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Context.setConfig : Lean.Meta.Simp.Context → Lean.Meta.Simp.Config → Lean.MetaM Lean.Meta.Simp.Context
-- Init.Data.String.Basic
String.bytes_ofList : ∀ {l : List Char}, (String.ofList l).toByteArray = l.utf8Encode
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {f : Option β → Option β},
  (m.alter k f).size =
    if k ∈ m ∧ (f m[k]?).isNone = true then m.size - 1
    else if k ∉ m ∧ (f m[k]?).isSome = true then m.size + 1 else m.size
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.localized₀_inf : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (p : Submonoid R) (f : M →ₗ[R] N)
  [inst_5 : IsLocalizedModule p f] (M' M'' : Submodule R M),
  Submodule.localized₀ p f (M' ⊓ M'') = Submodule.localized₀ p f M' ⊓ Submodule.localized₀ p f M''
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonCallHierarchyIncomingCall.toJson : Lean.Lsp.CallHierarchyIncomingCall → Lean.Json
-- Mathlib.Topology.Algebra.InfiniteSum.Module
/-- **Alias** of `ContinuousLinearMap.summable`. -/
Summable.mapL : ∀ {ι : Type u_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : Module R₂ M₂] [inst_6 : TopologicalSpace M] [inst_7 : TopologicalSpace M₂] {σ : R →+* R₂}
  {L : SummationFilter ι} {f : ι → M} (φ : M →SL[σ] M₂), Summable f L → Summable (fun b => φ (f b)) L
-- Mathlib.Algebra.Module.LinearMap.Basic
LinearMap.mulRight_eq_zero_iff : ∀ (R : Type u_6) (A : Type u_7) [inst : Semiring R] [inst_1 : NonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (a : A), LinearMap.mulRight R a = 0 ↔ a = 0
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dHomologyData_right_Q : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅)
  (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (f₅₆ : i₄ ⟶ i₆)
  (h₅₆ : CategoryTheory.CategoryStruct.comp f₅ f₆ = f₅₆) (n₀ n₁ n₂ n₃ n₄ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_5)
  (hn₄ : autoParam (n₃ + 1 = n₄) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_7),
  (X.dHomologyData f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₂₃ h₂₃ f₅₆ h₅₆ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).right.Q =
    X.E f₃ f₄ f₅₆ n₁ n₂ n₃ ⋯ ⋯
-- Init.Data.String.Basic
String.Pos.ofReplaceEnd : {s : String} → {p₀ : s.Pos} → (s.sliceTo p₀).Pos → s.Pos
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_eq_zero_iff_eq_empty_of_vaddInvariant : ∀ (G : Type u) {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] [inst_3 : TopologicalSpace α]
  [ContinuousConstVAdd G α] [AddAction.IsMinimal G α] {U : Set α} [μ.Regular], μ ≠ 0 → IsOpen U → (μ U = 0 ↔ U = ∅)
-- Lean.Data.Iterators.Producers.PersistentHashMap
/-- A zipper for traversing a `PersistentHashMap`. This is an inductive structure
representing the remaining key-value pairs to yield.
 -/
Lean.PersistentHashMap.Zipper : Type u → Type v → Type (max u v)
-- Lean.Meta.Tactic.Grind.Types
/-- Returns the root element in the equivalence class of `e`.  -/
Lean.Meta.Grind.getRoot : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Aesop.Forward.State
/-- Modify the `InstMap` associated to variable `var`. If no such `InstMap`
exists, the function `f` is applied to the empty `InstMap` and the result is
associated with `var`. Returns the new variable map and the result of `f`.  -/
Aesop.VariableMap.modify : {α : Type u_1} → Aesop.VariableMap → Aesop.PremiseIndex → (Aesop.InstMap → Aesop.InstMap × α) → Aesop.VariableMap × α
-- Init.Data.Fin.Lemmas
Fin.castSucc_inj : ∀ {n : ℕ} {a b : Fin n}, a.castSucc = b.castSucc ↔ a = b
-- Mathlib.Algebra.Group.Basic
add_zsmul : ∀ {G : Type u_3} [inst : AddGroup G] (a : G) (m n : ℤ), (m + n) • a = m • a + n • a
-- Init.Data.UInt.Lemmas
UInt32.add_zero : ∀ (a : UInt32), a + 0 = a
-- Mathlib.Algebra.Quaternion
Quaternion.re_ofScientific : ∀ {R : Type u_1} [inst : Field R] (m : ℕ) (s : Bool) (e : ℕ),
  QuaternionAlgebra.re (OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e
-- Mathlib.Order.Bounded
Set.unbounded_ge_iff : ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α], Set.Unbounded (fun x1 x2 => x1 ≥ x2) s ↔ ∀ (a : α), ∃ b ∈ s, b < a
-- Init.Data.List.Nat.Sum
List.sum_div_length_le_max_of_max?_eq_some_nat : ∀ {x : ℕ} {xs : List ℕ}, xs.max? = some x → xs.sum / xs.length ≤ x
-- Batteries.Data.List.Basic
/-- **Deprecated:** Use `reverse ∘ eraseDups ∘ reverse` or just `eraseDups` instead.  -/
List.eraseDup : {α : Type u_1} → [BEq α] → List α → List α
-- Mathlib.Topology.Algebra.TopologicallyNilpotent
/-- If `a` and `b` are topologically nilpotent and commute,
then `a + b` is topologically nilpotent.  -/
IsTopologicallyNilpotent.add_of_commute : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Ring R] [IsLinearTopology R R] {a b : R},
  IsTopologicallyNilpotent a → IsTopologicallyNilpotent b → Commute a b → IsTopologicallyNilpotent (a + b)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.canonical_left_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  (CategoryTheory.ShortComplex.HomologyData.canonical S).left.π = S.homologyπ
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minKeyD.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → α → Sort u_3) (size : ℕ) (k : α)
  (v : β k) (r : Std.DTreeMap.Internal.Impl α β) (x : α)
  (h_1 : (fallback : α) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            (x : α) → motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α β) →
                        (fallback : α) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)
                            fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_2 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
      fallback => h_3 size k v l size_1 k_1 v_1 l_1 r h r_1 fallback) =
    h_2 size k v r x
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.instLawfulToForwardSearcherModelForallCharPropDefaultForwardSearcherForallBoolDecide : ∀ {p : Char → Prop} [inst : DecidablePred p], String.Slice.Pattern.Model.LawfulToForwardSearcherModel p
-- Init.Data.String.Basic
String.Pos.offset_ofSlice : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {pos : (s.slice p₀ p₁ h).Pos},
  (String.Pos.ofSlice pos).offset = pos.offset.offsetBy p₀.offset
-- Mathlib.GroupTheory.IsSubnormal
/-- A subnormal subgroup of a simple group is normal.  -/
Subgroup.IsSubnormal.normal_of_isSimpleGroup : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, IsSimpleGroup G → H.IsSubnormal → H.Normal