mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
/-- **Continuous functional calculus.** Given a normal element `a : A` of a unital C⋆-algebra,
the continuous functional calculus is a `StarAlgEquiv` from the complex-valued continuous
functions on the spectrum of `a` to the unital C⋆-subalgebra generated by `a`. Moreover, this
equivalence identifies `(ContinuousMap.id ℂ).restrict (spectrum ℂ a))` with `a`; see
`continuousFunctionalCalculus_map_id`. As such it extends the polynomial functional calculus.  -/
continuousFunctionalCalculus : {A : Type u_1} →
  [inst : CStarAlgebra A] →
    (a : A) → [inst_1 : IsStarNormal a] → C(↑(spectrum ℂ a), ℂ) ≃⋆ₐ[ℂ] ↥(StarAlgebra.elemental ℂ a)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- The Bochner integral  -/
MeasureTheory.«term∫_,_» : Lean.ParserDescr
-- Mathlib.Topology.Constructions
Topology.IsInducing.of_codRestrict : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {t : Set Y}
  (ht : ∀ (x : X), f x ∈ t), Topology.IsInducing (Set.codRestrict f t ht) → Topology.IsInducing f
-- Mathlib.Order.CompleteBooleanAlgebra
compl_sInf : ∀ {α : Type u} [inst : CompleteBooleanAlgebra α] {s : Set α}, (sInf s)ᶜ = ⨆ i ∈ s, iᶜ
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Hom.ext_iff : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G} {x y : CategoryTheory.Pseudofunctor.StrongTrans.Hom η θ},
  x = y ↔ x.as = y.as
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
MeasureTheory.Integrable.comp_mul_right' : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] {g : ℝ → F},
  MeasureTheory.Integrable g MeasureTheory.volume →
    ∀ {R : ℝ}, R ≠ 0 → MeasureTheory.Integrable (fun x => g (x * R)) MeasureTheory.volume
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The `≤` order on subspaces is the same as that on the corresponding sets.  -/
AffineSubspace.le_def : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (s₁ s₂ : AffineSubspace k P), s₁ ≤ s₂ ↔ ↑s₁ ⊆ ↑s₂
-- Lean.Util.Profile
Lean.profiler.threshold : Lean.Option ℕ
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.verify₁.eq_1 : ∀ {w : UInt8} (_w : UInt8) (_h : ByteArray.utf8DecodeChar?.parseFirstByte w = ByteArray.utf8DecodeChar?.FirstByte.done),
  ByteArray.utf8DecodeChar?.verify₁ _w _h = true
-- Mathlib.Topology.Order
/-- This construction is left adjoint to the operation sending a topology on `α`
to its neighborhood filter at a fixed point `a : α`.  -/
nhdsAdjoint : {α : Type u} → α → Filter α → TopologicalSpace α
-- Mathlib.Algebra.GroupWithZero.Subgroup
AddSubgroup.smul_mem_pointwise_smul_iff₀ : ∀ {G₀ : Type u_1} {A : Type u_4} [inst : GroupWithZero G₀] [inst_1 : AddGroup A] [inst_2 : DistribMulAction G₀ A]
  {a : G₀}, a ≠ 0 → ∀ (S : AddSubgroup A) (x : A), a • x ∈ a • S ↔ x ∈ S
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.instTransZigzagZag : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    Trans (fun x1 x2 => CategoryTheory.Zigzag x1 x2) (fun x1 x2 => CategoryTheory.Zag x1 x2) fun x1 x2 =>
      CategoryTheory.Zigzag x1 x2
-- Mathlib.Analysis.SpecialFunctions.Exponential
/-- If `f` has sum `a`, then `NormedSpace.exp ∘ f` has product `NormedSpace.exp a`.  -/
HasSum.exp : ∀ {𝔸 : Type u_1} [inst : NormedCommRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] {ι : Type u_2} {f : ι → 𝔸} {a : 𝔸},
  HasSum f a → HasProd (NormedSpace.exp ∘ f) (NormedSpace.exp a)
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_lt_ceil : ∀ {r s : ENNReal}, r < s → ⌊r⌋ₑ < ⌈s⌉ₑ
-- Mathlib.RingTheory.Support
Module.support_of_noZeroSMulDivisors : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] [Nontrivial M], Module.support R M = Set.univ
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.comp_apply : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : PseudoMetricSpace γ] (G : β → γ) {C : NNReal} (H : LipschitzWith C G) (f : BoundedContinuousFunction α β)
  (a : α), (BoundedContinuousFunction.comp G H f) a = G (f a)
-- Mathlib.Data.Multiset.Antidiagonal
Multiset.antidiagonal_coe : ∀ {α : Type u_1} (l : List α), (↑l).antidiagonal = ↑(Multiset.powersetAux l).revzip
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.polynomialX.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R),
  W'.polynomialX = (MvPolynomial.pderiv 0) W'.polynomial
-- Mathlib.Topology.Order.UpperLowerSetTopology
OrderDual.instIsUpperSet : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLowerSet α], Topology.IsUpperSet αᵒᵈ
-- Mathlib.Algebra.Homology.Homotopy
dNext_eq : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : (i j : ι) → C.X i ⟶ D.X j) {i i' : ι},
  c.Rel i i' → (dNext i) f = CategoryTheory.CategoryStruct.comp (C.d i i') (f i' i)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_right : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (s : CategoryTheory.Limits.Cofork f g),
  s.ι.app CategoryTheory.Limits.WalkingParallelPair.zero = CategoryTheory.CategoryStruct.comp g s.π
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_inter_of_contains_eq_false_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m₁).WF →
    (↑m₂).WF → ∀ {k : α}, m₂.contains k = false → Std.DHashMap.Internal.Raw₀.Const.get! (m₁.inter m₂) k = default
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
/-- A commutative group object is a group object.  -/
CategoryTheory.CommGrp.toGrp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.CommGrp C → CategoryTheory.Grp C
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.eraseListₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β),
  m.eraseListₘ [] = m
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_single_one_mul : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : MulSemiringAction G k]
  (f : SkewMonoidAlgebra k G) (r : k) (x : G), (SkewMonoidAlgebra.single 1 r * f).coeff x = r * f.coeff x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} [inst_1 : Inhabited (β k')],
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l → ⟨k, v⟩ ∈ l → (m.insertMany l).get! k' = cast ⋯ v
-- Mathlib.Topology.Constructible
Topology.IsLocallyConstructible.iInter : ∀ {ι : Sort u_1} {X : Type u_2} [inst : TopologicalSpace X] [Finite ι] {f : ι → Set X},
  (∀ (i : ι), Topology.IsLocallyConstructible (f i)) → Topology.IsLocallyConstructible (⋂ i, f i)
-- Mathlib.Algebra.Order.Group.Basic
zpow_left_mono : ∀ (α : Type u_1) [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {n : ℤ},
  0 ≤ n → Monotone fun x => x ^ n
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwiseDisjoint_singleton_iff_injOn : ∀ {α : Type u_1} {ι : Type u_4} {s : Set ι} {f : ι → α}, (s.PairwiseDisjoint fun i => {f i}) ↔ Set.InjOn f s
-- Mathlib.Analysis.SpecificLimits.Basic
tendsto_nat_ceil_atTop : ∀ {α : Type u_4} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorSemiring α],
  Filter.Tendsto (fun x => ⌈x⌉₊) Filter.atTop Filter.atTop
-- Aesop.Forward.State
/-- Extract stats from a `ClusterState`.  -/
Aesop.ClusterState.stats : Aesop.ClusterState → Aesop.ForwardClusterStateStats
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.cofibrations_op : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C],
  HomotopicalAlgebra.cofibrations Cᵒᵖ = (HomotopicalAlgebra.fibrations C).op
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_ric : ∀ {n i : ℕ}, (*...=n).toArray[i]! = if i ≤ n then i else 0
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
/-- Constructs intermediate states of an iterator created with the combinator `IterM.zip`.
When `left.zip right` has already obtained a value from `left` but not yet from right,
it remembers `left`'s value in a field of its internal state. This intermediate state
cannot be created directly with `IterM.zip`.

`Intermediate.zip` is meant to be used only for verification purposes.
 -/
Std.IterM.Intermediate.zip : {α₁ α₂ β₁ β₂ : Type w} →
  {m : Type w → Type w'} →
    [inst : Std.Iterator α₁ m β₁] →
      Std.IterM m β₁ → Option { out // ∃ it, it.IsPlausibleOutput out } → Std.IterM m β₂ → Std.IterM m (β₁ × β₂)
-- Mathlib.NumberTheory.NumberField.Discriminant.Different
/-- Also see `not_dvd_discr_iff_forall_mem` for a slightly easier to use RHS.  -/
NumberField.not_dvd_discr_iff_forall_liesOver : ∀ (K : Type u_1) (𝒪 : Type u_2) [inst : Field K] [inst_1 : NumberField K] [inst_2 : CommRing 𝒪] [inst_3 : Algebra 𝒪 K]
  [IsIntegralClosure 𝒪 ℤ K] {p : ℤ},
  Prime p →
    (¬p ∣ NumberField.discr K ↔
      ∀ (P : Ideal 𝒪) (x : P.IsMaximal), P.LiesOver (Ideal.span {p}) → Algebra.IsUnramifiedAt ℤ P)
-- Mathlib.Data.List.Sym
List.left_mem_of_mk_mem_sym2 : ∀ {α : Type u_1} {xs : List α} {a b : α}, s(a, b) ∈ xs.sym2 → a ∈ xs
-- Init.Data.Array.Lemmas
Array.setIfInBounds_append : ∀ {α : Type u_1} {xs ys : Array α} {i : ℕ} {x : α},
  (xs ++ ys).setIfInBounds i x =
    if i < xs.size then xs.setIfInBounds i x ++ ys else xs ++ ys.setIfInBounds (i - xs.size) x
-- Mathlib.Topology.Maps.Basic
/-- If `g ∘ f` is open, where `f` is continuous and surjective, then `g` is open.  -/
IsOpenMap.of_comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
  Continuous f → Function.Surjective f → IsOpenMap (g ∘ f) → IsOpenMap g
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} {h_mem : k ∈ t₁ ∩ t₂},
  (t₁ ∩ t₂).get k h_mem = t₁.get k ⋯
-- Mathlib.Order.Interval.Set.Image
StrictMonoOn.mapsTo_Iio : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {b : α},
  StrictMonoOn f (Set.Iic b) → Set.MapsTo f (Set.Iio b) (Set.Iio (f b))
-- Init.Data.Zero
One.toOfNat1 : {α : Type u_1} → [One α] → OfNat α 1
-- Lean.Meta.Tactic.LibrarySearch
/-- LibrarySearch has an extension mechanism for replacing the function used
to find candidate lemmas.
 -/
Lean.Meta.LibrarySearch.CandidateFinder : Type
-- Init.Data.Vector.Perm
Vector.Perm.toArray : ∀ {α : Type u_1} {n : ℕ} {as bs : Vector α n}, as.Perm bs → as.toArray.Perm bs.toArray
-- Aesop.Forward.LevelIndex
Aesop.instHashableLevelIndex : Hashable Aesop.LevelIndex
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
UniformSpace.Completion.mapRingEquiv.congr_simp : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : UniformSpace α] [inst_2 : IsTopologicalRing α] [inst_3 : IsUniformAddGroup α]
  {β : Type u} [inst_4 : UniformSpace β] [inst_5 : Ring β] [inst_6 : IsUniformAddGroup β] [inst_7 : IsTopologicalRing β]
  (f f_1 : α ≃+* β) (e_f : f = f_1) (hf : Continuous ⇑f) (hf' : Continuous ⇑f.symm),
  UniformSpace.Completion.mapRingEquiv f hf hf' = UniformSpace.Completion.mapRingEquiv f_1 ⋯ ⋯
-- Mathlib.ModelTheory.Equivalence
/-- Two (bounded) formulas are semantically equivalent over a theory `T` when they have the same
interpretation in every model of `T`. (This is also known as logical equivalence, which also has a
proof-theoretic definition.)  -/
FirstOrder.«term_⇔[_]_» : Lean.TrailingParserDescr
-- Mathlib.Data.ENNReal.Basic
ENNReal.toNNReal_ne_zero : ∀ {a : ENNReal}, a.toNNReal ≠ 0 ↔ a ≠ 0 ∧ a ≠ ⊤
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.pathObject.lift_π₁_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} {F K : HomologicalComplex C c} [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasPathObject]
  (φ₀ φ₁ : F ⟶ K) (h : Homotopy φ₀ φ₁) {Z : HomologicalComplex C c} (h_1 : K ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.pathObject.lift φ₀ φ₁ h)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.pathObject.π₁ K) h_1) =
    CategoryTheory.CategoryStruct.comp φ₁ h_1
-- Mathlib.Algebra.Category.Grp.Colimits
AddCommGrpCat.Colimits.Quot.map_ι : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat)
  [inst_1 : DecidableEq J] {j j' : J} {f : j ⟶ j'} (x : ↑(F.obj j)),
  (AddCommGrpCat.Colimits.Quot.ι F j') ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) =
    (AddCommGrpCat.Colimits.Quot.ι F j) x
-- Mathlib.Algebra.Ring.Commute
Commute.sq_sub_sq : ∀ {R : Type u} [inst : Ring R] {a b : R}, Commute a b → a ^ 2 - b ^ 2 = (a + b) * (a - b)
-- Mathlib.Data.List.Defs
List.map₂Left'.eq_2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (a : α) (as : List α),
  List.map₂Left' f (a :: as) [] = (List.map (fun a => f a none) (a :: as), [])
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey_erase_eq_of_not_compare_eq_maxKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : (t.erase k).isEmpty = false}, ¬cmp k (t.maxKey ⋯) = Ordering.eq → (t.erase k).maxKey he = t.maxKey ⋯
-- Mathlib.CategoryTheory.Iso
/-- `IsIso.mk'` is the dual of `IsIso.mk`, which we need for `to_dual`.
Please avoid using this directly.  -/
CategoryTheory.IsIso.mk' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : Y ⟶ X},
  (∃ inv,
      CategoryTheory.CategoryStruct.comp inv f = CategoryTheory.CategoryStruct.id X ∧
        CategoryTheory.CategoryStruct.comp f inv = CategoryTheory.CategoryStruct.id Y) →
    CategoryTheory.IsIso f
-- Mathlib.Topology.Order.LeftRightLim
tendsto_rightLim_atBot_of_tendsto : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace α]
  [OrderTopology α] [NoBotOrder α] [T3Space β] {f : α → β} {b : β},
  Filter.Tendsto f Filter.atBot (nhds b) → Filter.Tendsto (Function.rightLim f) Filter.atBot (nhds b)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.instNontrivialEdgeLabelingOfNonemptyElemSym2EdgeSet : ∀ {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} [Nonempty ↑G.edgeSet] [Nontrivial K], Nontrivial (G.EdgeLabeling K)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- Given a left homology data `h` of a short complex `S`, we can construct another left homology
data by choosing another kernel and cokernel that are isomorphic to the ones in `h`.  -/
CategoryTheory.ShortComplex.LeftHomologyData.copy : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (h : S.LeftHomologyData) → {K' H' : C} → (K' ≅ h.K) → (H' ≅ h.H) → S.LeftHomologyData
-- Mathlib.Topology.Instances.ENat
ENat.isOpen_singleton : ∀ {x : ℕ∞}, x ≠ ⊤ → IsOpen {x}
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.codeSupp'.eq_2 : ∀ (x : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.codeSupp' Turing.ToPartrec.Code.succ x =
    Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal Turing.ToPartrec.Code.succ x)
-- Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
CategoryTheory.Functor.IsDenseAt.of_final : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {C' : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} C']
  (G : CategoryTheory.Functor C' C) [(CategoryTheory.CostructuredArrow.pre G F Y).Final],
  F.isDenseAt Y → (G.comp F).isDenseAt Y
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.lsingle_comp_chainsMap_f : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (n : ℕ) (x : Fin n → G),
  CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Finsupp.lsingle x)) ((groupHomology.chainsMap f φ).f n) =
    ModuleCat.ofHom (Finsupp.lsingle (⇑f ∘ x) ∘ₗ (Rep.Hom.hom φ).toLinearMap)
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.finSuccEquiv_C : ∀ {R : Type u_2} [inst : CommSemiring R] {n : ℕ} (r : R),
  (MvPowerSeries.finSuccEquiv R n) (MvPowerSeries.C r) = PowerSeries.C (MvPowerSeries.C r)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
/-- A non-unital star `R`-algebra `A` has a *continuous functional calculus* for elements
satisfying the property `p : A → Prop` if

+ for every such element `a : A` there is a non-unital star algebra homomorphism
  `cfcₙHom : C(quasispectrum R a, R)₀ →⋆ₙₐ[R] A` sending the (restriction of) the identity map
  to `a`.
+ `cfcHom` is continuous and injective and the quasispectrum of the image of function `f` is
  its range.
+ `cfcₙHom` preserves the property `p`.

The property `p` is marked as an `outParam` so that the user need not specify it. In practice,

+ for `R := ℂ`, we choose `p := IsStarNormal`,
+ for `R := ℝ`, we choose `p := IsSelfAdjoint`,
+ for `R := ℝ≥0`, we choose `p := (0 ≤ ·)`.

Instead of directly providing the data we opt instead for a `Prop` class. In all relevant cases,
the continuous functional calculus is uniquely determined, and utilizing this approach
prevents diamonds or problems arising from multiple instances.  -/
NonUnitalContinuousFunctionalCalculus : (R : Type u_1) →
  (A : Type u_2) →
    outParam (A → Prop) →
      [inst : CommSemiring R] →
        [Nontrivial R] →
          [inst_2 : StarRing R] →
            [inst_3 : MetricSpace R] →
              [IsTopologicalSemiring R] →
                [ContinuousStar R] →
                  [inst_6 : NonUnitalRing A] →
                    [StarRing A] →
                      [TopologicalSpace A] →
                        [inst_9 : Module R A] → [IsScalarTower R A A] → [SMulCommClass R A A] → Prop
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
/-- The free functor `Type u ⥤ ModuleCat R` sending a type `X` to the
free `R`-module with generators `x : X`, implemented as the type `X →₀ R`.
 -/
ModuleCat.free : (R : Type u) → [inst : Ring R] → CategoryTheory.Functor (Type u) (ModuleCat R)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.instMonoHomologyι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [inst_2 : K.HasHomology i],
  CategoryTheory.Mono (K.homologyι i)
-- Mathlib.Data.Nat.Cast.Basic
map_ofNat' : ∀ {B : Type u_4} {F : Type u_5} [inst : AddMonoidWithOne B] {A : Type u_6} [inst_1 : AddMonoidWithOne A]
  [inst_2 : FunLike F A B] [AddMonoidHomClass F A B] (f : F),
  f 1 = 1 → ∀ (n : ℕ) [inst_4 : n.AtLeastTwo], f (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.preimage_closedBall : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (h : α ≃ᵢ β) (x : β) (r : ℝ),
  ⇑h ⁻¹' Metric.closedBall x r = Metric.closedBall (h.symm x) r
-- Init.Data.String.Basic
ByteArray.validateUTF8.go.congr_simp : ∀ (b b_1 : ByteArray) (e_b : b = b_1) (i i_1 : ℕ) (e_i : i = i_1) (hi : i ≤ b.size),
  ByteArray.validateUTF8.go b i hi = ByteArray.validateUTF8.go b_1 i_1 ⋯
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.coe_top : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : Nonempty α], ↑⊤ = Set.univ
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.subset_sdiff_union`. -/
Set.subset_diff_union : ∀ {α : Type u_1} (s t : Set α), s ⊆ s \ t ∪ t
-- Mathlib.Order.Basic
Ne.lt_of_le' : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, a ≠ b → b ≤ a → b < a
-- Mathlib.Topology.Algebra.StarSubalgebra
/-- The coercion from an elemental algebra to the full algebra as a `IsClosedEmbedding`.  -/
StarAlgebra.elemental.isClosedEmbedding_coe : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : StarRing A] [inst_5 : IsSemitopologicalSemiring A] [inst_6 : ContinuousStar A]
  [inst_7 : Algebra R A] [inst_8 : StarModule R A] (x : A), Topology.IsClosedEmbedding Subtype.val
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Any costructured arrow factors through a universal arrow.  -/
CategoryTheory.CostructuredArrow.IsUniversal.fac_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {f : CategoryTheory.CostructuredArrow S T} (h : f.IsUniversal)
  (g : CategoryTheory.CostructuredArrow S T) {Z : D} (h_1 : T ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S.map (h.lift g)) (CategoryTheory.CategoryStruct.comp f.hom h_1) =
    CategoryTheory.CategoryStruct.comp g.hom h_1
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.map_eq_lift : ∀ {α : Type u} {β : Type v} {f : α → β}, FreeGroup.map f = FreeGroup.lift (FreeGroup.of ∘ f)
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.id_apply : ∀ (M : Type u_10) [inst : One M] (x : M), (OneHom.id M) x = x
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.lift_quot_mk : ∀ {G : Type u_1} {M : Type u_4} [inst : Group G] [inst_1 : Monoid M] (N : Subgroup G) [nN : N.Normal] {φ : G →* M}
  (HN : N ≤ φ.ker) (g : G), (QuotientGroup.lift N φ HN) (Quot.mk (⇑(QuotientGroup.leftRel N)) g) = φ g
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.mul_iff_left : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β]
  [inst_1 : CommGroup β] [IsTopologicalGroup β],
  MeasureTheory.StronglyMeasurable f → (MeasureTheory.StronglyMeasurable (g * f) ↔ MeasureTheory.StronglyMeasurable g)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.WorkspaceClientCapabilities.mk : Option Bool → Option Lean.Lsp.WorkspaceEditClientCapabilities → Lean.Lsp.WorkspaceClientCapabilities
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.const_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {a : X} {b : Y}
  (ha : IsOpen {a}) (hb : IsOpen {b}) (x : X), ↑(OpenPartialHomeomorph.const ha hb) x = b
-- Mathlib.Topology.UniformSpace.UniformConvergence
TendstoUniformly.prodMk : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
  {ι' : Type u_5} {β' : Type u_6} [inst_1 : UniformSpace β'] {F' : ι' → α → β'} {f' : α → β'} {p' : Filter ι'},
  TendstoUniformly F f p →
    TendstoUniformly F' f' p' → TendstoUniformly (fun i a => (F i.1 a, F' i.2 a)) (fun a => (f a, f' a)) (p ×ˢ p')
-- Mathlib.RepresentationTheory.Invariants
Rep.invariantsAdjunction_homEquiv_symm_apply_hom : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Group G] {X : ModuleCat k} {Y : Rep.{u_1, u, v} k G}
  (f : X ⟶ (Rep.invariantsFunctor k G).obj Y),
  (Rep.Hom.hom (((Rep.invariantsAdjunction k G).homEquiv X Y).symm f)).toLinearMap =
    Y.ρ.invariants.subtype ∘ₗ ModuleCat.Hom.hom f