mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Rigid.Functor
CategoryTheory.leftDualFunctor_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.LeftRigidCategory C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.leftDualFunctor C).map f = (ᘁf).op.mop
-- Mathlib.FieldTheory.SeparablyGenerated
MvPolynomial.isAlgebraic_of_mem_vars_of_forall_totalDegree_le : ∀ {k : Type u_1} {K : Type u_2} {ι : Type u_3} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {a : ι → K}
  {F : MvPolynomial ι k},
  (∀ (F' : MvPolynomial ι k), F' ≠ 0 → (MvPolynomial.aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree) →
    (MvPolynomial.aeval a) F = 0 → ∀ i ∈ F.vars, IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)
-- Mathlib.Algebra.DirectSum.Basic
/-- Isomorphism obtained by separating the term of index `none` of a direct sum over `Option ι`.  -/
DirectSum.addEquivProdDirectSum : {ι : Type v} →
  {α : Option ι → Type w} →
    [inst : (i : Option ι) → AddCommMonoid (α i)] →
      (DirectSum (Option ι) fun i => α i) ≃+ α none × DirectSum ι fun i => α (some i)
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.stabilizer_vadd_eq_left : ∀ {G : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : AddAction G β]
  [inst_3 : VAdd α β] [VAddAssocClass G α β] (a : α) (b : β),
  (Function.Injective fun x => x +ᵥ b) → AddAction.stabilizer G (a +ᵥ b) = AddAction.stabilizer G a
-- Mathlib.Order.CountableSupClosed
mem_countableSupClosure_iff_iSup : ∀ {α : Type u_2} {s : Set α} {a : α} [inst : CompleteLattice α],
  a ∈ countableSupClosure s ↔ ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨆ n, t n = a
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.r_rfl : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] (a : α × α), Lean.Grind.IntModule.OfNatModule.r α a a
-- Init.Data.List.Attach
List.pmap_eq_pmapImpl : @List.pmap = @List.pmapImpl
-- Init.Data.Iterators.Basic
Std.IterM.TerminationMeasures.Finite.mk.sizeOf_spec : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] [inst_1 : SizeOf α]
  [inst_2 : (a : Type w) → SizeOf (m a)] [inst_3 : SizeOf β] (it : Std.IterM m β), sizeOf { it := it } = 1 + sizeOf it
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  k ∉ t → l.contains k = false → (Std.ExtDTreeMap.Const.insertManyIfNewUnit t l).getKey? k = none
-- Mathlib.Topology.Algebra.Ring.Real
instIsTopologicalRingReal : IsTopologicalRing ℝ
-- Lean.Exception
Lean.MonadError.toAddErrorMessageContext : {m : Type → Type} → [self : Lean.MonadError m] → Lean.AddErrorMessageContext m
-- Mathlib.CategoryTheory.DifferentialObject
/-- The shift functor on `DifferentialObject S C`.  -/
CategoryTheory.DifferentialObject.shiftFunctor : {S : Type u_1} →
  [inst : AddCommGroupWithOne S] →
    (C : Type u) →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.HasShift C S] →
            S → CategoryTheory.Functor (CategoryTheory.DifferentialObject S C) (CategoryTheory.DifferentialObject S C)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.getElem?_toArray_eq : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_4 : Std.Rxi.IsAlwaysFinite α] {i : ℕ}, r.toArray[i]? = Std.PRange.least?.bind (Std.PRange.succMany? i)
-- Mathlib.Data.Finset.Empty
Finset.Nonempty.to_subtype : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → Nonempty ↥s
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.monMonoidal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → CategoryTheory.MonoidalCategory (CategoryTheory.AddMon C)
-- Init.Data.SInt.Basic
instReprAtomInt64 : ReprAtom Int64
-- Init.Data.Float.Float32
/-- Checks whether a floating-point number is a positive or negative infinite number, but not a finite
number or `NaN`.

This function has a logical model in terms of `Float32.Model`. It is compiled to the C operator `isinf`.
 -/
Float32.isInf : Float32 → Bool
-- Init.Data.ByteArray.Basic
/-- The number of bytes remaining in the iterator.
 -/
ByteArray.Iterator.remainingBytes : ByteArray.Iterator → ℕ
-- Lean.Parser.Extra
Lean.Parser.withOpen.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Init.Data.String.Substring
_private.Init.Data.String.Substring.0.Substring.Raw.nextn.match_1.eq_1 : ∀ (motive : Substring.Raw → ℕ → String.Pos.Raw → Sort u_1) (x : Substring.Raw) (p : String.Pos.Raw)
  (h_1 : (x : Substring.Raw) → (p : String.Pos.Raw) → motive x 0 p)
  (h_2 : (ss : Substring.Raw) → (i : ℕ) → (p : String.Pos.Raw) → motive ss i.succ p),
  (match x, 0, p with
    | x, 0, p => h_1 x p
    | ss, i.succ, p => h_2 ss i p) =
    h_1 x p
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstr.mk.inj : ∀ {p : Lean.Grind.CommRing.Poly} {strict : Bool} {h : Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof}
  {p_1 : Lean.Grind.CommRing.Poly} {strict_1 : Bool} {h_1 : Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof},
  { p := p, strict := strict, h := h } = { p := p_1, strict := strict_1, h := h_1 } →
    p = p_1 ∧ strict = strict_1 ∧ h = h_1
-- Mathlib.Order.Hom.BoundedLattice
instCoeTCInfTopHomOfInfTopHomClass.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Min α] [inst_2 : Min β] [inst_3 : Top α]
  [inst_4 : Top β] [inst_5 : InfTopHomClass F α β],
  instCoeTCInfTopHomOfInfTopHomClass = { coe := fun f => { toFun := ⇑f, map_inf' := ⋯, map_top' := ⋯ } }
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.isRegularMono_of_regularMono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (h : CategoryTheory.RegularMono f),
  CategoryTheory.IsRegularMono f
-- Mathlib.Data.Set.NAry
Set.image2_image2_image2_comm : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {ε : Type u_9} {ε' : Type u_10} {ζ : Type u_11}
  {ζ' : Type u_12} {ν : Type u_13} {s : Set α} {t : Set β} {u : Set γ} {v : Set δ} {f : ε → ζ → ν} {g : α → β → ε}
  {h : γ → δ → ζ} {f' : ε' → ζ' → ν} {g' : α → γ → ε'} {h' : β → δ → ζ'},
  (∀ (a : α) (b : β) (c : γ) (d : δ), f (g a b) (h c d) = f' (g' a c) (h' b d)) →
    Set.image2 f (Set.image2 g s t) (Set.image2 h u v) = Set.image2 f' (Set.image2 g' s u) (Set.image2 h' t v)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.neg_equiv : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P Q : Fin 3 → R}, P ≈ Q → W'.neg P ≈ W'.neg Q
-- Mathlib.MeasureTheory.Measure.Restrict
MeasurableEquiv.restrict_map : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} (e : α ≃ᵐ β)
  (μ : MeasureTheory.Measure α) (s : Set β),
  (MeasureTheory.Measure.map (⇑e) μ).restrict s = MeasureTheory.Measure.map (⇑e) (μ.restrict (⇑e ⁻¹' s))
-- Init.Data.Int.Gcd
Int.lcm_mul_left_left_eq_mul_of_lcm_eq_mul : ∀ {n m k : ℤ}, n.lcm m = n.natAbs * m.natAbs → (k * n).lcm m = n.natAbs * k.lcm m
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
Mathlib.Tactic.Linarith.SimplexAlgorithm.instUsableInSimplexAlgorithmDenseMatrix : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm Mathlib.Tactic.Linarith.SimplexAlgorithm.DenseMatrix
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.norm_le_of_nonempty : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] [Nonempty α]
  {f : BoundedContinuousFunction α β} {M : ℝ}, ‖f‖ ≤ M ↔ ∀ (x : α), ‖f x‖ ≤ M
-- Init.Data.List.Find
List.idxOf?_cons : ∀ {α : Type u_1} [inst : BEq α] {a : α} {xs : List α} {b : α},
  List.idxOf? b (a :: xs) = if (a == b) = true then some 0 else Option.map (fun x => x + 1) (List.idxOf? b xs)
-- Mathlib.Algebra.Ring.Idempotent
IsIdempotentElem.add_sub_mul_of_commute : ∀ {R : Type u_1} [inst : NonUnitalRing R] {a b : R},
  Commute a b → IsIdempotentElem a → IsIdempotentElem b → IsIdempotentElem (a + b - a * b)
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.LeftAdjointCommShift.iso_hom_app_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddGroup A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] (a b : A) (h : a + b = 0) [inst_5 : G.CommShift A] (X : C) {Z : D}
  (h_1 : (CategoryTheory.shiftFunctor D a).obj (F.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.LeftAdjointCommShift.iso adj a).hom.app X) h_1 =
    CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C a).map (adj.unit.app X)))
      (CategoryTheory.CategoryStruct.comp
        (F.map
          ((CategoryTheory.shiftFunctor C a).map
            (G.map ((CategoryTheory.shiftFunctorCompIsoId D a b h).inv.app (F.obj X)))))
        (CategoryTheory.CategoryStruct.comp
          (F.map
            ((CategoryTheory.shiftFunctor C a).map
              ((CategoryTheory.Functor.commShiftIso G b).hom.app ((CategoryTheory.shiftFunctor D a).obj (F.obj X)))))
          (CategoryTheory.CategoryStruct.comp
            (F.map
              ((CategoryTheory.shiftFunctorCompIsoId C b a ⋯).hom.app
                (G.obj ((CategoryTheory.shiftFunctor D a).obj (F.obj X)))))
            (CategoryTheory.CategoryStruct.comp (adj.counit.app ((CategoryTheory.shiftFunctor D a).obj (F.obj X)))
              h_1))))
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.bound : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (f : E [⋀^ι]→L[𝕜] F),
  ∃ C, 0 < C ∧ ∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i, ‖m i‖
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.opEquiv.match_3.eq_2 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (x y : (CategoryTheory.WithInitial C)ᵒᵖ) → (Opposite.unop y ⟶ Opposite.unop x) → (x ⟶ y) → Sort u_3) (a : C)
  (x :
    Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶
      Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of a)))
  (x_1 : Opposite.op (CategoryTheory.WithInitial.of a) ⟶ Opposite.op CategoryTheory.WithInitial.star)
  (h_1 :
    (x y : C) →
      (f :
          Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of y)) ⟶
            Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of x))) →
        (x_2 : Opposite.op (CategoryTheory.WithInitial.of x) ⟶ Opposite.op (CategoryTheory.WithInitial.of y)) →
          motive (Opposite.op (CategoryTheory.WithInitial.of x)) (Opposite.op (CategoryTheory.WithInitial.of y)) f x_2)
  (h_2 :
    (a : C) →
      (x :
          Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶
            Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of a))) →
        (x_2 : Opposite.op (CategoryTheory.WithInitial.of a) ⟶ Opposite.op CategoryTheory.WithInitial.star) →
          motive (Opposite.op (CategoryTheory.WithInitial.of a)) (Opposite.op CategoryTheory.WithInitial.star) x x_2)
  (h_3 :
    (x :
        Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶
          Opposite.unop (Opposite.op CategoryTheory.WithInitial.star)) →
      (x_2 : Opposite.op CategoryTheory.WithInitial.star ⟶ Opposite.op CategoryTheory.WithInitial.star) →
        motive (Opposite.op CategoryTheory.WithInitial.star) (Opposite.op CategoryTheory.WithInitial.star) x x_2),
  (match Opposite.op (CategoryTheory.WithInitial.of a), Opposite.op CategoryTheory.WithInitial.star, x, x_1 with
    | Opposite.op (CategoryTheory.WithInitial.of x), Opposite.op (CategoryTheory.WithInitial.of y), f, x_2 =>
      h_1 x y f x_2
    | Opposite.op (CategoryTheory.WithInitial.of a), Opposite.op CategoryTheory.WithInitial.star, x, x_2 => h_2 a x x_2
    | Opposite.op CategoryTheory.WithInitial.star, Opposite.op CategoryTheory.WithInitial.star, x, x_2 => h_3 x x_2) =
    h_2 a x x_1
-- Std.Http.Server.Config
/-- Maximum number of requests per connection.
 -/
Std.Http.Config.maxRequests : Std.Http.Config → ℕ
-- Init.Data.Fin.Lemmas
Fin.lt_or_le : ∀ {n : ℕ} (a b : Fin n), a < b ∨ b ≤ a
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.mkBEqCached_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) {input : aig.BinaryInput},
  aig.decls.size ≤ (aig.mkBEqCached input).aig.decls.size
-- Mathlib.Topology.Algebra.Module.ModuleTopology
eq_moduleTopology : ∀ (R : Type u_1) [inst : TopologicalSpace R] (A : Type u_2) [inst_1 : Add A] [inst_2 : SMul R A]
  [τA : TopologicalSpace A] [IsModuleTopology R A], τA = moduleTopology R A
-- Mathlib.Algebra.Lie.BaseChange
LieSubmodule.mem_baseChange_iff : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : CommRing A] [inst_8 : Algebra R A] {N : LieSubmodule R L M}
  {m : TensorProduct R A M},
  m ∈ LieSubmodule.baseChange A N ↔ m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
-- Mathlib.Topology.Algebra.Monoid
/-- If the action of `R` on `A` commutes with left-multiplication, then continuous multiplication
implies continuous scalar multiplication by constants.

Notably, this instance applies when `R = Aᵐᵒᵖ`.  -/
SMulCommClass.continuousConstSMul : ∀ {R : Type u_6} {A : Type u_7} [inst : Monoid A] [inst_1 : SMul R A] [SMulCommClass R A A]
  [inst_3 : TopologicalSpace A] [SeparatelyContinuousMul A], ContinuousConstSMul R A
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.sameCycle_pow_right : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℕ}, f.SameCycle x ((f ^ n) y) ↔ f.SameCycle x y
-- Mathlib.Order.CompleteLattice.Defs
/-- A complete linear order is a linear order whose lattice structure is complete.  -/
CompleteLinearOrder : Type u_8 → Type u_8
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
/-- Construct a walk from a list of darts where adjacent darts in the list are also adjacent
in the graph  -/
SimpleGraph.Walk.ofDarts : {V : Type u} →
  {G : SimpleGraph V} →
    (l : List G.Dart) →
      (hne : l ≠ []) → List.IsChain G.DartAdj l → G.Walk (l.head hne).toProd.1 (l.getLast hne).toProd.2
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.MkTableKey.normExpr : Lean.Expr → Lean.Meta.SynthInstance.MkTableKey.M Lean.Expr
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.le_arch : ∀ {d : ℕ} (a : ℤ√↑d), ∃ n, a ≤ ↑n
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.fromNondegComplex_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C] (n : ℕ) {Z : C}
  (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj X).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (s.fromNondegComplex.f n) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (s.ι n) (AlgebraicTopology.DoldKan.PInfty.f n)) h
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_congr_subtype : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (f : β → α) {P Q : β → Prop},
  (∀ (x : β), P x ↔ Q x) → ∏' (x : { x // P x }), f ↑x = ∏' (x : { x // Q x }), f ↑x
-- Lean.Meta.Tactic.Grind.Proof
/-- Returns a proof of `lhs = rhs` (`lhs ≍ rhs`) if `heq = false` (`heq = true`).
If `heq = false`, this function assumes that `lhs` and `rhs` have the same type.
 -/
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.mkEqProofCore : Lean.Expr → Lean.Expr → Bool → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.Order.Fin.Basic
Fin.strictMono_succ : ∀ {n : ℕ}, StrictMono Fin.succ
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
/-- A `1`-simplex  -/
SSet.Truncated.Edge.edge : {X : SSet.Truncated 2} →
  {x₀ x₁ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })} →
    SSet.Truncated.Edge x₀ x₁ → X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.Edge._proof_2 })
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
/-- A version of `cfcₙ_eq_cfcₙL` in terms of `ContinuousMapZero.mkD`  -/
cfcₙ_eq_cfcₙL_mkD : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] (f : R → R) (a : A)
  (ha : autoParam (p a) _auto_184✝), cfcₙ f a = (cfcₙL ha) (ContinuousMapZero.mkD ((quasispectrum R a).domRestrict f) 0)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_insertIfNew!_le_minKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k} {km kmi : α},
  t.minKey? = some km →
    (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).minKey?.get ⋯ = kmi → (compare kmi km).isLE = true
-- Aesop.Nanos
Aesop.Nanos.mk.sizeOf_spec : ∀ (nanos : ℕ), sizeOf { nanos := nanos } = 1 + sizeOf nanos
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_range_succ_div_prod : ∀ {M : Type u_4} (f : ℕ → M) {n : ℕ} [inst : CommGroup M],
  (∏ i ∈ Finset.range (n + 1), f i) / ∏ i ∈ Finset.range n, f i = f n
-- Mathlib.AlgebraicTopology.Quasicategory.StrictBicategory
/-- The bicategory of quasicategories extracted from `QCat.CatEnrichedOrdinaryCat`.  -/
SSet.QCat.bicategory : CategoryTheory.Bicategory SSet.QCat
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLabel.parts : Array Lean.Elab.InlayHintLabelPart → Lean.Elab.InlayHintLabel
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.coeff_natDegree : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.coeff p.natDegree = p.leadingCoeff
-- Mathlib.RingTheory.DedekindDomain.SInteger
Set.integer_valuation_le_one : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R))
  (K : Type v) [inst_2 : Field K] [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (x : ↥(S.integer K))
  {v : IsDedekindDomain.HeightOneSpectrum R}, v ∉ S → (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑x ≤ 1
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
UniqueFactorizationMonoid.exists_reduced_factors' : ∀ {R : Type u_2} [inst : CommMonoidWithZero R] [UniqueFactorizationMonoid R] (a b : R),
  b ≠ 0 → ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Multipliable.tprod_eq_one_iff : ∀ {ι : Type u_1} {α : Type u_3} [inst : CommMonoid α] [inst_1 : PartialOrder α] [IsOrderedMonoid α]
  [CanonicallyOrderedMul α] [inst_4 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α},
  Multipliable f → (∏' (i : ι), f i = 1 ↔ ∀ (x : ι), f x = 1)
-- Mathlib.CategoryTheory.Core
CategoryTheory.Iso.core_inv_app_iso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : CategoryTheory.Core C),
  (α.core.inv.app X).iso.inv = α.hom.app X.of
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction_homEquiv_apply_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {F : CategoryTheory.Sheaf J A} {M : A}
  (f : Φ.presheafFiber.obj F.obj ⟶ M),
  ((Φ.skyscraperSheafAdjunction.homEquiv F M) f).hom = Φ.skyscraperPresheafHomEquiv f
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.coeFn_compMeasurePreserving : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {β : Type u_7} [inst_1 : MeasurableSpace β] {μb : MeasureTheory.Measure β} {f : α → β}
  (g : ↥(MeasureTheory.Lp E p μb)) (hf : MeasureTheory.MeasurePreserving f μ μb),
  ↑↑((MeasureTheory.Lp.compMeasurePreserving f hf) g) =ᵐ[μ] ↑↑g ∘ f
-- Mathlib.Algebra.Order.IsBotOne
/-- **Alias** of `pos_iff_ne_zero`. -/
zero_lt_iff : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : Zero α] [IsBotZeroClass α], 0 < a ↔ a ≠ 0
-- Mathlib.Algebra.Free
FreeMagma.lift_comp_of : ∀ {α : Type u} {β : Type v} [inst : Mul β] (f : α → β), ⇑(FreeMagma.lift f) ∘ FreeMagma.of = f
-- Init.Data.String.Slice
String.Slice.RevSplitIterator.instIteratorLoopOfMonad : {ρ : Type} →
  {ρ_1 : ρ} →
    {σ : String.Slice → Type} →
      [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
        [inst_1 : String.Slice.Pattern.ToBackwardSearcher ρ_1 σ] →
          {m : Type → Type u_1} →
            {n : Type u_2 → Type u_3} →
              {s : String.Slice} →
                [inst_2 : Monad m] → [Monad n] → Std.IteratorLoop (String.Slice.RevSplitIterator ρ_1 s) m n
-- Lean.Meta.InferType
_private.Lean.Meta.InferType.0.Lean.Meta.ArrowPropResult.true.sizeOf_spec : sizeOf Lean.Meta.ArrowPropResult.true✝ = 1
-- Mathlib.Algebra.DirectSum.Internal
/-- The commutative ring `A 0` inherited from `R` in the presence of `SetLike.GradedMonoid A`.  -/
SetLike.GradeZero.instCommRing : {ι : Type u_1} →
  {σ : Type u_2} →
    {R : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : AddCommMonoid ι] →
          [inst_2 : SetLike σ R] → [AddSubgroupClass σ R] → (A : ι → σ) → [SetLike.GradedMonoid A] → CommRing ↥(A 0)
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.instTransListSubtypeSetMemCompleteSublatticeTreeIsPrefix : {A : Type u_1} → Trans List.IsPrefix (fun x T => x ∈ T) fun x T => x ∈ T
-- Std.Tactic.Do.Syntax
/-- A single `frames` alternative `| f a _ c => frame`: a program pattern (a head identifier applied to
binder or `_` arguments, matched like the `until` pattern) and the frame assertion to apply when the
spec for that program is used during VC generation. The named binders (e.g. `a`, `c`) are in scope
in `frame`, bound to the matched arguments.
 -/
Lean.Parser.Tactic.frameAlt : Lean.ParserDescr
-- Mathlib.Order.CompleteBooleanAlgebra
disjoint_sSup_iff : ∀ {α : Type u} [inst : Order.Frame α] {a : α} {s : Set α}, Disjoint a (sSup s) ↔ ∀ b ∈ s, Disjoint a b
-- Mathlib.Algebra.Polynomial.Div
/-- **Alias** of `Polynomial.rootMultiplicity_eq_natFind_of_ne_zero`. -/
Polynomial.rootMultiplicity_eq_nat_find_of_nonzero : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R} (p0 : p ≠ 0) {a : R}
  [inst_1 : DecidablePred fun n => ¬(Polynomial.X - Polynomial.C a) ^ (n + 1) ∣ p],
  Polynomial.rootMultiplicity a p = Nat.find ⋯
-- Mathlib.RingTheory.Polynomial.UniqueFactorization
Polynomial.exists_irreducible_of_natDegree_pos : ∀ {R : Type u_1} [inst : CommSemiring R] [NoZeroDivisors R] [WfDvdMonoid R] {f : Polynomial R} [Nontrivial R],
  0 < f.natDegree → ∃ g, Irreducible g ∧ g ∣ f