mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
/-- The trifunctor `X₁ X₂ X₃ ↦ X₂ ⊗ (X₃ ⊗ X₁)`  -/
CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁' : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.MonoidalCategory C] →
      CategoryTheory.Functor C (CategoryTheory.Functor C (CategoryTheory.Functor C C))
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.Producer.mk.injEq : ∀ (chunk : Std.Http.Chunk) (done : IO.Promise Bool) (chunk_1 : Std.Http.Chunk) (done_1 : IO.Promise Bool),
  ({ chunk := chunk, done := done } = { chunk := chunk_1, done := done_1 }) = (chunk = chunk_1 ∧ done = done_1)
-- Mathlib.MeasureTheory.Measure.IntegralCharFun
/-- A bound on the measure of the set `{x | r < |⟪a, x⟫|}` in terms of the integral of
the characteristic function, for a probability measure on an inner product space.  -/
MeasureTheory.measureReal_abs_inner_gt_le_integral_charFun : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {mE : MeasurableSpace E}
  [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure μ] {a : E} {r : ℝ},
  0 < r →
    μ.real {x | r < |inner ℝ a x|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - MeasureTheory.charFun μ (t • a)‖
-- Mathlib.LinearAlgebra.TensorProduct.Pi
TensorProduct.piScalarRight_symm_single : ∀ (R : Type u_1) [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (N : Type u_3)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Module S N] [inst_6 : IsScalarTower R S N] (ι : Type u_4)
  [inst_7 : Fintype ι] [inst_8 : DecidableEq ι] (x : N) (i : ι),
  (TensorProduct.piScalarRight R S N ι).symm (Pi.single i x) = x ⊗ₜ[R] Pi.single i 1
-- Mathlib.NumberTheory.LocalField.Basic
/-- The value group of a local field is (uniquely) isomorphic to `ℤᵐ⁰`.  -/
IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : ValuativeRel K] →
      [inst_2 : TopologicalSpace K] →
        [IsNonarchimedeanLocalField K] → ValuativeRel.ValueGroupWithZero K ≃*o WithZero (Multiplicative ℤ)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H2_induction_on : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} {C : ↑(groupHomology.H2 A) → Prop}
  (x : ↑(groupHomology.H2 A)),
  (∀ (x : ↥(groupHomology.cycles₂ A)), C ((CategoryTheory.ConcreteCategory.hom (groupHomology.H2π A)) x)) → C x
-- Mathlib.ModelTheory.Satisfiability
/-- Any theory with an infinite model has arbitrarily large models.  -/
FirstOrder.Language.Theory.exists_large_model_of_infinite_model : ∀ {L : FirstOrder.Language} (T : L.Theory) (κ : Cardinal.{w}) (M : Type w') [inst : L.Structure M] [M ⊨ T] [Infinite M],
  ∃ N, Cardinal.lift.{max u v w, w} κ ≤ Cardinal.mk ↑N
-- Mathlib.RingTheory.DedekindDomain.Dvr
IsDedekindDomainDvr.mk : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsDomain A] [toIsNoetherian : IsNoetherian A A],
  (∀ (P : Ideal A), P ≠ ⊥ → ∀ (x : P.IsPrime), IsDiscreteValuationRing (Localization.AtPrime P)) → IsDedekindDomainDvr A
-- Mathlib.Data.Fintype.Quotient
Quotient.finHRecOn.congr_simp : ∀ {ι : Type u_1} [inst : Fintype ι] {inst_1 : DecidableEq ι} [inst_2 : DecidableEq ι] {α : ι → Sort u_2}
  {S : (i : ι) → Setoid (α i)} {C : ((i : ι) → Quotient (S i)) → Sort u_4} (q : (i : ι) → Quotient (S i))
  (f f_1 : (a : (i : ι) → α i) → C fun x => ⟦a x⟧) (e_f : f = f_1)
  (h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a ≍ f b),
  Quotient.finHRecOn q f h = Quotient.finHRecOn q f_1 ⋯
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.bucket_updateBucket : ∀ {α : Type u} {β : α → Type v} [inst : Hashable α] (self : Array (Std.DHashMap.Internal.AssocList α β))
  (h : 0 < self.size) (k : α) (f : Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.bucket (Std.DHashMap.Internal.updateBucket self h k f) ⋯ k =
    f (Std.DHashMap.Internal.bucket self h k)
-- Mathlib.RingTheory.PrincipalIdealDomain
IsBezout.gcd_dvd_right : ∀ {R : Type u} [inst : CommRing R] (x y : R) [inst_1 : Submodule.IsPrincipal (Ideal.span {x, y})], IsBezout.gcd x y ∣ y
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.commSemiring : {α : Type u_1} →
  [inst : CommSemiring α] →
    [inst_1 : PartialOrder α] → [ZeroLEOneClass α] → [AddLeftMono α] → [PosMulMono α] → CommSemiring { x // 0 ≤ x }
-- Mathlib.Data.Set.Basic
Set.mem_powerset : ∀ {α : Type u} {x s : Set α}, x ⊆ s → x ∈ 𝒫 s
-- Mathlib.Order.Interval.Finset.Nat
Nat.card_Icc : ∀ (a b : ℕ), (Finset.Icc a b).card = b + 1 - a
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.instDecidableEqCont' : DecidableEq Turing.PartrecToTM2.Cont'
-- Mathlib.Topology.Order.Monotone
/-- A monotone function continuous at the infimum of a nonempty set sends this infimum to
the infimum of the image of this set.  -/
Monotone.map_csInf_of_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β]
  {f : α → β} {A : Set α},
  ContinuousAt f (sInf A) →
    Monotone f →
      A.Nonempty → autoParam (BddBelow A) Monotone.map_csInf_of_continuousAt._auto_1 → f (sInf A) = sInf (f '' A)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.basisFun.congr_simp : ∀ (p : ENNReal) (𝕜 : Type u_1) (ι : Type u_2) [inst : Finite ι] [inst_1 : Ring 𝕜],
  PiLp.basisFun p 𝕜 ι = PiLp.basisFun p 𝕜 ι
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.skeleton_monotone`. -/
Topology.CWComplex.skeleton_monotone : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D],
  Monotone (Topology.RelCWComplex.skeleton C)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
_private.Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme.0.AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjIso_hom_ι_assoc : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) {Z : AlgebraicGeometry.Scheme}
  (h : I.glueData.glued ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjIso✝ I U).hom
      (CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map I.gluedTo.base).obj ↑U).ι h) =
    CategoryTheory.CategoryStruct.comp (I.glueData.ι U) h
-- Init.Data.UInt.Lemmas
USize.one_mul : ∀ (a : USize), 1 * a = a
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.arrow_mk_mem_toSet_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Arrow.mk f ∈ P.toSet ↔ P f
-- Mathlib.Topology.Order.IntermediateValue
IsPreconnected.Ioi_csInf_subset : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α] {s : Set α},
  IsPreconnected s → BddBelow s → ¬BddAbove s → Set.Ioi (sInf s) ⊆ s
-- Mathlib.NumberTheory.Chebyshev
/-- The sum of `log p` over primes `p ≤ x`.  -/
Chebyshev.theta : ℝ → ℝ
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey!_insertManyIfNewUnit_emptyWithCapacity_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α] {l : List α}
  {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l →
      k ∈ l →
        (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).getKey!
            k' =
          k
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (α : F ⟶ G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : F.obj a ⟶ G.obj c}
  (h : CategoryTheory.CategoryStruct.comp (α.app a) (G.map (CategoryTheory.CategoryStruct.comp f g)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (α.naturality (CategoryTheory.CategoryStruct.comp f g)).hom h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g).hom (α.app c))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (α.app c)).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (α.naturality g).hom)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (α.app b) (G.map g)).inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (α.naturality f).hom (G.map g))
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Bicategory.associator (α.app a) (G.map f) (G.map g)).hom
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.Bicategory.whiskerLeft (α.app a) (G.mapComp f g).inv) h))))))
-- Mathlib.Combinatorics.Graph.Basic
Graph.banana_adj : ∀ {α : Type u_1} {β : Type u_2} {x y u v : α} {edgeSet : Set β},
  (Graph.banana u v edgeSet).Adj x y ↔ edgeSet.Nonempty ∧ s(x, y) = s(u, v)
-- Mathlib.Topology.MetricSpace.IsometricSMul
Prod.isIsometricSMul' : ∀ {M : Type u} {N : Type u_2} [inst : Mul M] [inst_1 : PseudoEMetricSpace M] [IsIsometricSMul M M] [inst_3 : Mul N]
  [inst_4 : PseudoEMetricSpace N] [IsIsometricSMul N N], IsIsometricSMul (M × N) (M × N)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.comp_hom : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] {X Y Z : CategoryTheory.MorphismProperty.Comma L R P Q W} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.MorphismProperty.Comma.Hom.hom (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MorphismProperty.Comma.Hom.hom f)
      (CategoryTheory.MorphismProperty.Comma.Hom.hom g)
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addLeftCancelSemigroup : {I : Type u} → {f : I → Type v₁} → [(i : I) → AddLeftCancelSemigroup (f i)] → AddLeftCancelSemigroup ((i : I) → f i)
-- Mathlib.CategoryTheory.Abelian.Projective.Extend
CategoryTheory.ProjectiveResolution.Hom.hom'_f_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  {R : CategoryTheory.ProjectiveResolution X} {X' : C} {R' : CategoryTheory.ProjectiveResolution X'} {f : X ⟶ X'}
  (φ : R.Hom R' f) (n : ℤ) (m : ℕ) (h : -↑m = n) {Z : C} (h_1 : R'.cochainComplex.X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (φ.hom'.f n) h_1 =
    CategoryTheory.CategoryStruct.comp (R.cochainComplexXIso n m h).hom
      (CategoryTheory.CategoryStruct.comp (φ.hom.f m)
        (CategoryTheory.CategoryStruct.comp (R'.cochainComplexXIso n m h).inv h_1))
-- Mathlib.Analysis.SpecificLimits.Basic
tendsto_pow_atTop_nhds_zero_of_lt_one : ∀ {𝕜 : Type u_4} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [ExistsAddOfLE 𝕜] [Archimedean 𝕜]
  [inst_5 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜},
  0 ≤ r → r < 1 → Filter.Tendsto (fun n => r ^ n) Filter.atTop (nhds 0)
-- Mathlib.Analysis.Complex.Conformal
/-- In cases where the **Cauchy-Riemann Equation** guarantees complex differentiability at `x`, the
complex derivative equals `ContinuousLinearMap.complexOfReal` of the real derivative.
 -/
complexOfReal_fderiv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {x : ℂ},
  DifferentiableAt ℝ f x →
    ∀ (h₂ : (fderiv ℝ f x) Complex.I = Complex.I • (fderiv ℝ f x) 1), (fderiv ℝ f x).complexOfReal h₂ = fderiv ℂ f x
-- Mathlib.Topology.Order.Basic
nhds_top_order : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : OrderTop α] [OrderTopology α],
  nhds ⊤ = ⨅ l, ⨅ (_ : l < ⊤), Filter.principal (Set.Ioi l)
-- Mathlib.Topology.Algebra.Module.Complement
/-- A submodule `p` is called *complemented* if there exists a continuous projection `M →ₗ[R] p`.  -/
Submodule.ClosedComplemented : {R : Type u_1} →
  [inst : Ring R] →
    {M : Type u_2} → [TopologicalSpace M] → [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → Submodule R M → Prop
-- Mathlib.MeasureTheory.Group.Defs
MeasureTheory.Measure.IsAddLeftInvariant.map_add_left_eq_self : ∀ {G : Type u_1} {inst : MeasurableSpace G} {inst_1 : Add G} {μ : MeasureTheory.Measure G} [self : μ.IsAddLeftInvariant]
  (g : G), MeasureTheory.Measure.map (fun x => g + x) μ = μ
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasStrictDerivAt.cpow : ∀ {f g : ℂ → ℂ} {f' g' x : ℂ},
  HasStrictDerivAt f f' x →
    HasStrictDerivAt g g' x →
      f x ∈ Complex.slitPlane →
        HasStrictDerivAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x
-- Mathlib.Algebra.Star.Basic
IsRegular.star : ∀ {R : Type u} [inst : Mul R] [inst_1 : StarMul R] {x : R}, IsRegular x → IsRegular (star x)
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- Scalar multiplication `• : R × A → A` is continuous if `R` is a topological
ring, and `A` is an `R` module with the module topology.  -/
ModuleTopology.continuousSMul : ∀ (R : Type u_1) [inst : TopologicalSpace R] (A : Type u_2) [inst_1 : Add A] [inst_2 : SMul R A], ContinuousSMul R A
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
le_abs : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] {a b : α}, a ≤ |b| ↔ a ≤ b ∨ a ≤ -b
-- Mathlib.Analysis.Analytic.Basic
analyticOn_empty : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}, AnalyticOn 𝕜 f ∅
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
WittVector.RecursionMain.succNthVal.congr_simp : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : CharP k p] [inst_2 : IsAlgClosed k]
  (n : ℕ) (a₁ a₁_1 : WittVector p k) (e_a₁ : a₁ = a₁_1) (a₂ a₂_1 : WittVector p k) (e_a₂ : a₂ = a₂_1)
  (bs bs_1 : Fin (n + 1) → k),
  bs = bs_1 →
    ∀ (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0),
      WittVector.RecursionMain.succNthVal p n a₁ a₂ bs ha₁ ha₂ =
        WittVector.RecursionMain.succNthVal p n a₁_1 a₂_1 bs_1 ⋯ ⋯
-- Mathlib.RepresentationTheory.Basic
Representation.apply_sub_id_partialSum_eq : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Ring k] [inst_1 : Monoid G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (n : ℕ) (g : G) (x : V),
  (ρ g - LinearMap.id) (Fin.partialSum (fun j => (ρ (g ^ ↑j)) x) (Fin.last (n + 1))) = (ρ (g ^ (n + 1))) x - x
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.instTensorUnit.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.MonObj.instTensorUnit =
    { one := CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C),
      mul :=
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom,
      one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }
-- Mathlib.CategoryTheory.EssentialImage
CategoryTheory.Functor.essImage_ι_comp : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C), (P.ι.comp F).essImage = P.map F
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
SSet.Subcomplex.hasDimensionLT_of_le : ∀ {X : SSet} {A B : X.Subcomplex}, A ≤ B → ∀ (d : ℕ) [B.toSSet.HasDimensionLT d], A.toSSet.HasDimensionLT d
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.parent'_lt : ∀ (self : Batteries.UnionFind) (i : ℕ) (h : i < self.arr.size), self.arr[i].parent < self.size
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.mk_eq_bot : ∀ {M : Type u_1} [inst : Add M] (carrier : Set M) (add_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a + b ∈ carrier),
  { carrier := carrier, add_mem' := add_mem' } = ⊥ ↔ carrier = ∅
-- Init.Data.Range.Polymorphic.UInt
UInt16.instHasSize_2 : Std.Rxi.HasSize UInt16
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
/-- This is an auxiliary definition used for constructing an instance of the non-unital continuous
functional calculus given an instance of the unital one on the unitization.

This is the natural non-unital star homomorphism obtained from the chain
```lean
calc
  C(σₙ 𝕜 a, 𝕜)₀ →⋆ₙₐ[𝕜] C(σₙ 𝕜 a, 𝕜) := ContinuousMapZero.toContinuousMapHom
  _             ≃⋆[𝕜] C(σ 𝕜 (↑a : A⁺¹), 𝕜) := Homeomorph.compStarAlgEquiv'
  _             →⋆ₐ[𝕜] A⁺¹ := cfcHom
```
This range of this map is contained in the range of `(↑) : A → A⁺¹` (see `cfcₙAux_mem_range_inr`),
and so we may restrict it to `A` to get the necessary homomorphism for the non-unital continuous
functional calculus.
 -/
cfcₙAux : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : StarRing A] →
          [inst_3 : NormedSpace 𝕜 A] →
            [inst_4 : IsScalarTower 𝕜 A A] →
              [inst_5 : SMulCommClass 𝕜 A A] →
                [inst_6 : StarModule 𝕜 A] →
                  {p : A → Prop} →
                    {p₁ : Unitization 𝕜 A → Prop} →
                      (∀ {x : A}, p₁ ↑x ↔ p x) →
                        (a : A) →
                          p a →
                            [ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁] →
                              ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜 →⋆ₙₐ[𝕜] Unitization 𝕜 A
-- Mathlib.RingTheory.Flat.Equalizer
LinearMap.tensorKerEquivOfSurjective_symm_tmul : ∀ {R : Type u_1} [inst : CommRing R] {N : Type u_4} {P : Type u_5} [inst_1 : AddCommGroup N] [inst_2 : AddCommGroup P]
  [inst_3 : Module R N] [inst_4 : Module R P] [inst_5 : Module.Flat R P] (f : N →ₗ[R] P) (hf : Function.Surjective ⇑f)
  (A : Type u_6) [inst_6 : AddCommGroup A] [inst_7 : Module R A] (a : A) (y : ↥f.ker),
  ↑((f.kerLTensorEquivOfSurjective hf A).symm (a ⊗ₜ[R] y)) = a ⊗ₜ[R] ↑y
-- Mathlib.Analysis.Calculus.FDeriv.Comp
DifferentiableWithinAt.comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} (x : E) {s : Set E} {g : F → G} {t : Set F},
  DifferentiableWithinAt 𝕜 g t (f x) →
    DifferentiableWithinAt 𝕜 f s x → Set.MapsTo f s t → DifferentiableWithinAt 𝕜 (g ∘ f) s x
-- Init.Data.Nat.Basic
Nat.mul_sub_right_distrib : ∀ (n m k : ℕ), (n - m) * k = n * k - m * k
-- Init.Core
/-- `Associative op` indicates `op` is an associative operation,
i.e. `(a ∘ b) ∘ c = a ∘ (b ∘ c)`.
 -/
Std.Associative : {α : Sort u} → (α → α → α) → Prop
-- Mathlib.RingTheory.Smooth.Local
Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsLocalRing S]
  [inst_3 : Algebra R S] (P : Type u_3) [inst_4 : CommRing P] [inst_5 : Algebra R P] [inst_6 : Algebra P S]
  [IsScalarTower R P S] [Algebra.FormallySmooth R P] [Module.Free P Ω[P⁄R]] [Module.Finite P Ω[P⁄R]],
  Function.Surjective ⇑(algebraMap P S) →
    (RingHom.ker (algebraMap P S)).FG →
      (Algebra.FormallySmooth R S ↔
        Function.Injective ⇑(KaehlerDifferential.cotangentComplexBaseChange R S P (IsLocalRing.ResidueField S)))
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.ofHom_id : ∀ {M : Type u} [inst : AddCommMonoid M],
  AddCommMonCat.ofHom (AddMonoidHom.id M) = CategoryTheory.CategoryStruct.id (AddCommMonCat.of M)
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- If two linear maps are equal, they are equal at each point.  -/
LinearMap.congr_fun : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  {f g : M →ₛₗ[σ] M₃}, f = g → ∀ (x : M), f x = g x
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {F : CategoryTheory.Functor J CommRingCat} →
      {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop} →
        {a a_1 : CommRingCat.Colimits.Prequotient F} → CommRingCat.Colimits.Relation F a a_1 → Prop
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.liftCover_coe : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {ι : Type u_5} {S : ι → Set α}
  {φ : (i : ι) → C(↑(S i), β)}
  {hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩}
  {hS : ∀ (x : α), ∃ i, S i ∈ nhds x} {i : ι} (x : ↑(S i)), (ContinuousMap.liftCover S φ hφ hS) ↑x = (φ i) x
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
/-- The (distinguished) triangle in `HomotopyCategory C (ComplexShape.up ℤ)` attached to a
degreewise split short exact sequence of cochain complexes.  -/
CochainComplex.trianglehOfDegreewiseSplit : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) →
        ((n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) →
          CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- If `f : MonoOver X`, then `mk' f.arrow` is of course just `f`, but not definitionally, so we
package it as an isomorphism.  -/
CategoryTheory.MonoOver.mkArrowIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → (f : CategoryTheory.MonoOver X) → CategoryTheory.MonoOver.mk f.arrow ≅ f
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.mem_set_smul_def : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_4}
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M] (s : Set S) (N : Submodule R M) (x : M),
  x ∈ s • N ↔ x ∈ sInf {p | ∀ ⦃r : S⦄ {n : M}, r ∈ s → n ∈ N → r • n ∈ p}
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.cos_add : ∀ (θ₁ θ₂ : Real.Angle), (θ₁ + θ₂).cos = θ₁.cos * θ₂.cos - θ₁.sin * θ₂.sin
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.Batteries.AssocList.find?.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Lean.Util.LeanOptions
Lean.LeanOption.mk.sizeOf_spec : ∀ (name : Lean.Name) (value : Lean.LeanOptionValue),
  sizeOf { name := name, value := value } = 1 + sizeOf name + sizeOf value
-- Std.Do.WP.SimpLemmas
Std.Do.WP.adapt_ReaderT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ρ ρ' α : Type u} {x : ReaderT ρ' m α}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.arg ρ ps)} [inst : Std.Do.WP m ps] (f : ρ → ρ'),
  (Std.Do.wp (ReaderT.adapt f x)).apply Q = fun r => (Std.Do.wp x).apply (fun a x => Q.1 a r, Q.2) (f r)
-- Mathlib.Order.Bounds.Basic
isGLB_empty_iff : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, IsGLB ∅ a ↔ IsTop a
-- Lean.Expr
Lean.Expr.appArg : (e : Lean.Expr) → e.isApp = true → Lean.Expr
-- Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
CategoryTheory.Functor.IsLocallyFaithful.functorPushforward_equalizer_mem : ∀ {C : Type uC} {inst : CategoryTheory.Category.{vC, uC} C} {D : Type uD} {inst_1 : CategoryTheory.Category.{vD, uD} D}
  {G : CategoryTheory.Functor C D} {K : CategoryTheory.GrothendieckTopology D} [self : G.IsLocallyFaithful K] {U V : C}
  (f₁ f₂ : U ⟶ V),
  G.map f₁ = G.map f₂ → CategoryTheory.Sieve.functorPushforward G (CategoryTheory.Sieve.equalizer f₁ f₂) ∈ K (G.obj U)