mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Homotopy.TopCat.Path
TopCat.Path.mk.inj : ∀ {X : TopCat} {x y : ↑X} {hom : TopCat.I ⟶ X}
  {hom₀ : autoParam ((CategoryTheory.ConcreteCategory.hom hom) 0 = x) TopCat.Path.hom₀._autoParam}
  {hom₁ : autoParam ((CategoryTheory.ConcreteCategory.hom hom) 1 = y) TopCat.Path.hom₁._autoParam}
  {hom_1 : TopCat.I ⟶ X}
  {hom₀_1 : autoParam ((CategoryTheory.ConcreteCategory.hom hom_1) 0 = x) TopCat.Path.hom₀._autoParam}
  {hom₁_1 : autoParam ((CategoryTheory.ConcreteCategory.hom hom_1) 1 = y) TopCat.Path.hom₁._autoParam},
  { hom := hom, hom₀ := hom₀, hom₁ := hom₁ } = { hom := hom_1, hom₀ := hom₀_1, hom₁ := hom₁_1 } → hom = hom_1
-- Mathlib.LinearAlgebra.Basis.SMul
Module.Basis.isUnitSMul_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : Module.Basis ι R M} {w : ι → R} (hw : ∀ (i : ι), IsUnit (w i)) (i : ι), (v.isUnitSMul hw) i = w i • v i
-- Lean.ToExpr
_private.Lean.ToExpr.0.Lean.Name.toExprAux.isSimple : Lean.Name → ℕ → Bool
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.InternalState.deferred : Lean.Doc.InternalState → Array Lean.Doc.DeferredCheck
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.dec : Lean.FVarId → Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof
-- Mathlib.Order.Hom.Lattice
SupHom.instPartialOrder : {α : Type u_2} → {β : Type u_3} → [inst : Max α] → [inst_1 : SemilatticeSup β] → PartialOrder (SupHom α β)
-- Mathlib.Topology.Separation.Hausdorff
disjoint_nhds_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] {x y : X}, Disjoint (nhds x) (nhds y) ↔ x ≠ y
-- Mathlib.CategoryTheory.Presentable.Directed
/-- If `κ` is a cardinal, this structure contains the data of a `κ`-bounded diagram
in a category `J`.  -/
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram : (J : Type w) → [CategoryTheory.SmallCategory J] → Cardinal.{w} → Type w
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.C_mul : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.Splits → ∀ (a : R), (Polynomial.C a * f).Splits
-- Qq.Typ
/-- Gets the type of a quoted expression.   -/
Qq.Quoted.ty : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
-- Lean.Meta.Tactic.Cleanup
/-- We include `p` in the used-set, if `p` is a proposition that contains a `x` that is in the used-set.  -/
_private.Lean.Meta.Tactic.Cleanup.0.Lean.Meta.cleanupCore.collectPropsStep : StateRefT' IO.RealWorld (Bool × Lean.FVarIdSet) Lean.MetaM Unit
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.tmul_comm : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Invertible R M] {m₁ m₂ : M}, m₁ ⊗ₜ[R] m₂ = m₂ ⊗ₜ[R] m₁
-- Std.Http.Data.URI.Encoding
/-- Encodes a raw string into an encoded fragment component.
 -/
Std.Http.URI.EncodedFragment.encode : String → Std.Http.URI.EncodedFragment
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.RootForm.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [inst_5 : Fintype ι],
  P.RootForm = ∑ i, LinearMap.smulRight (P.coroot' i) (P.coroot' i)
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasLaw.isProbabilityMeasure_iff : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.HasLaw X μ P → (MeasureTheory.IsProbabilityMeasure P ↔ MeasureTheory.IsProbabilityMeasure μ)
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.map_mapRingHom_eval_map_eval : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (p : Polynomial (Polynomial R))
  (q : Polynomial R) (r : R),
  Polynomial.eval (f r) (Polynomial.eval (Polynomial.map f q) (Polynomial.map (Polynomial.mapRingHom f) p)) =
    f (Polynomial.eval r (Polynomial.eval q p))
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_norm : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  {f : α → E},
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ (p : ENNReal), MeasureTheory.lpNorm (fun x => ‖f x‖) p μ = MeasureTheory.lpNorm f p μ
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mfderiv_extChartAt_inverse_comp_mfderivWithin_extChartAT_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {x : M} [IsManifold I 2 M] (Y : TangentSpace I x),
  ((mfderiv% ↑(extChartAt I x) x).inverse ∘SL
        (mfderiv[Set.range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) x)).inverse)
      Y =
    Y
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instLieModule : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) [inst_5 : LieAlgebra R L]
  [LieModule R L M], LieModule R L ↥N
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.NatIso.mapHomologicalComplex_hom_app_f : ∀ {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] {F G : CategoryTheory.Functor W₁ W₂}
  [inst_4 : F.PreservesZeroMorphisms] [inst_5 : G.PreservesZeroMorphisms] (α : F ≅ G) (c : ComplexShape ι)
  (C : HomologicalComplex W₁ c) (x : ι),
  ((CategoryTheory.NatIso.mapHomologicalComplex α c).hom.app C).f x = α.hom.app (C.X x)
-- Mathlib.CategoryTheory.Limits.Filtered
/-- For all filtered types of a size `w`, we have colimits  -/
CategoryTheory.Limits.HasFilteredColimitsOfSize.HasColimitsOfShape : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  [self : CategoryTheory.Limits.HasFilteredColimitsOfSize.{w', w, v, u} C] (I : Type w)
  [inst_1 : CategoryTheory.Category.{w', w} I] [CategoryTheory.IsFiltered I],
  CategoryTheory.Limits.HasColimitsOfShape I C
-- Mathlib.Algebra.Order.UpperLower
IsLowerSet.div_right : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α] {s t : Set α},
  IsLowerSet s → IsLowerSet (s / t)
-- Mathlib.Algebra.Algebra.Spectrum.Basic
/-- the assumption `(σ a).Nonempty` is necessary and cannot be removed without
further conditions on the algebra `A` and scalar field `𝕜`.  -/
spectrum.smul_eq_smul : ∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] [Nontrivial A] (k : 𝕜) (a : A),
  (spectrum 𝕜 a).Nonempty → spectrum 𝕜 (k • a) = k • spectrum 𝕜 a
-- Mathlib.Algebra.Group.Basic
eq_mul_of_div_eq : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, a / c = b → a = b * c
-- Mathlib.RingTheory.Algebraic.Basic
isAlgebraic_ratCast : ∀ (R : Type u) {A : Type v} [inst : DivisionRing A] [inst_1 : Field R] [inst_2 : Algebra R A] (n : ℚ), IsAlgebraic R ↑n
-- Mathlib.Data.Nat.ChineseRemainder
/-- The natural number less than `(m.map s).prod` congruent to
`a i` mod `s i` for all  `i ∈ m`.  -/
Nat.chineseRemainderOfMultiset : {ι : Type u_1} →
  (a s : ι → ℕ) →
    {m : Multiset ι} →
      m.Nodup →
        (∀ i ∈ m, s i ≠ 0) → {x | x ∈ m}.Pairwise (Function.onFun Nat.Coprime s) → { k // ∀ i ∈ m, k ≡ a i [MOD s i] }
-- Mathlib.Order.DirectedInverseSystem
_private.Mathlib.Order.DirectedInverseSystem.0.DirectLimit.lift₂Aux.congr_simp : ∀ {ι : Type u_1} [inst : Preorder ι] {F₁ : ι → Type u_2} {F₂ : ι → Type u_3} {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6}
  (f₁ : (i j : ι) → (h : i ≤ j) → T₁ h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)]
  [inst_2 : DirectedSystem F₁ fun x1 x2 x3 => ⇑(f₁ x1 x2 x3)] {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7}
  (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) [inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)]
  [inst_4 : DirectedSystem F₂ fun x1 x2 x3 => ⇑(f₂ x1 x2 x3)] [inst_5 : IsDirectedOrder ι] {C : Sort u_9}
  (ih : (i : ι) → F₁ i → F₂ i → C)
  (compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y))
  (z : (i : ι) × F₁ i) (w : (i : ι) × F₂ i),
  DirectLimit.lift₂Aux✝ f₁ f₂ ih compat z w = DirectLimit.lift₂Aux✝ f₁ f₂ ih compat z w
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.MVarValue : Type
-- Init.Data.Array.Range
Array.range_ne_empty_iff : ∀ {n : ℕ}, Array.range n ≠ #[] ↔ n ≠ 0
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.le_comap_of_map_le : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (S : AddSubsemigroup M) {T : AddSubsemigroup N}
  {f : M →ₙ+ N}, AddSubsemigroup.map f S ≤ T → S ≤ AddSubsemigroup.comap f T
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommProd_eq_prod : ∀ {α : Type u_6} [inst : CommMonoid α] (s : Multiset α), s.noncommProd ⋯ = s.prod
-- Lean.Elab.Exception
Lean.Elab.abortCommandExceptionId : Lean.InternalExceptionId
-- Mathlib.CategoryTheory.Functor.Hom
CategoryTheory.Functor.hom_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (p : Cᵒᵖ × C),
  (CategoryTheory.Functor.hom C).obj p = (Opposite.unop p.1 ⟶ p.2)
-- Mathlib.Data.List.MinMax
List.le_min_of_forall_le : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : OrderTop α] (l : List α) (a : α),
  (∀ x ∈ l, a ≤ x) → a ≤ List.foldr min ⊤ l
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.toArray_toList : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.toList.toArray = it.toArray
-- Mathlib.ModelTheory.Syntax
/-- Substitutes the variables in a given term with terms.  -/
FirstOrder.Language.Term.subst : {L : FirstOrder.Language} → {α : Type u'} → {β : Type v'} → L.Term α → (α → L.Term β) → L.Term β
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.comp_base : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  (g : Y ⟶ Z), (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base
-- Mathlib.Algebra.Algebra.ZMod
ZMod.algebraOfModule.proof : ∀ (n : ℕ) (R : Type u_2) [inst : Ring R] [inst_1 : Module (ZMod n) R] (r : ZMod n) (x : R),
  r • 1 * x = r • x ∧ x * r • 1 = r • x
-- Lean.Parser.Syntax
Lean.Parser.Command.mixfixKind : Lean.Parser.Parser
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
/-- **Alias** of the reverse direction of `quasispectrum.algebraMap_mem_iff`. -/
quasispectrum.algebraMap_mem : ∀ (S : Type u_3) {R : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Field S] [inst_2 : NonUnitalRing A]
  [inst_3 : Algebra R S] [inst_4 : Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [inst_7 : Module R A]
  [IsScalarTower R S A] {a : A} {r : R}, r ∈ quasispectrum R a → (algebraMap R S) r ∈ quasispectrum S a
-- Mathlib.Topology.Order.Bornology
IsOrderBornology.atBot_le_cobounded : ∀ {α : Type u_1} [inst : Bornology α] [inst_1 : Preorder α] [IsOrderBornology α] [NoMinOrder α],
  Filter.atBot ≤ Bornology.cobounded α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionOptions.resolveProvider : Lean.Lsp.CompletionOptions → Bool
-- Mathlib.CategoryTheory.EssentialImage
/-- Pre-composing by an essentially surjective functor doesn't change the essential image.  -/
CategoryTheory.Functor.essImage_comp_of_essSurj : ∀ {C : Type u₁} {D : Type u₂} {E : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [F.EssSurj], (F.comp G).essImage = G.essImage
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ D` creates limits of `K.leftOp : Jᵒᵖ ⥤ C`, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` creates
colimits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.createsColimitOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (K : CategoryTheory.Functor J Cᵒᵖ) →
              (F : CategoryTheory.Functor C D) →
                [CategoryTheory.CreatesLimit K.leftOp F] → CategoryTheory.CreatesColimit K F.op
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.expand_mul : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (q : ℕ) (hq : q ≠ 0) (φ : MvPowerSeries σ R),
  (MvPowerSeries.expand (p * q) ⋯) φ = (MvPowerSeries.expand p hp) ((MvPowerSeries.expand q hq) φ)
-- Mathlib.NumberTheory.LSeries.Basic
/-- We introduce notation `↗f` for `f` interpreted as a function `ℕ → ℂ`.

Let `R` be a ring with a coercion to `ℂ`. Then we can write `↗χ` when `χ : DirichletCharacter R`
or `↗f` when `f : ArithmeticFunction R` or simply `f : N → R` with a coercion from `ℕ` to `N`
as an argument to `LSeries`, `LSeriesHasSum`, `LSeriesSummable` etc.  -/
LSeries.notation.«term↗_» : Lean.ParserDescr
-- Mathlib.Data.Fintype.Basic
/-- Embed `Fin n` into `Fin (n + 1)` by prepending zero to the `univ`  -/
Fin.univ_succ : ∀ (n : ℕ), Finset.univ = Finset.cons 0 (Finset.map { toFun := Fin.succ, inj' := ⋯ } Finset.univ) ⋯
-- Lean.Declaration
Lean.instInhabitedRecursorRule : Inhabited Lean.RecursorRule
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.diag_toFun : ∀ (A : Type u_2) [inst : AddMonoid A] [inst_1 : TopologicalSpace A] (i : A), (ContinuousAddMonoidHom.diag A) i = (i, i)
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.getHSMulNatInst : Lean.Level → Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
isUniformEmbedding_translate_add : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] (a : α),
  IsUniformEmbedding fun x => x + a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_erase!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → ∀ {k : α}, (Std.DTreeMap.Internal.Impl.erase! k t).getKey! k = default
-- Mathlib.Order.DirectedInverseSystem
/-- Over a well-ordered type, construct a family of bijections by transfinite recursion.  -/
InverseSystem.globalEquiv : {ι : Type u_6} →
  {F : ι → Type u_7} →
    {X : ι → Type u_8} →
      [inst : LinearOrder ι] →
        {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} →
          [WellFoundedLT ι] →
            [inst_2 : SuccOrder ι] →
              [InverseSystem f] →
                ((i : ι) → ¬IsMax i → { e // ∀ (x : F (Order.succ i)), (e x).1 = f ⋯ x }) →
                  ((i : ι) → Order.IsSuccPrelimit i → { e // ∀ (x : F i) (l : ↑(Set.Iio i)), ↑(e x) l = f ⋯ x }) →
                    (i : ι) → F i ≃ InverseSystem.piLT X i
-- Mathlib.Order.Fin.Basic
Fin.castLEOrderEmb_toEmbedding : ∀ {m n : ℕ} (h : n ≤ m), (Fin.castLEOrderEmb h).toEmbedding = { toFun := Fin.castLE h, inj' := ⋯ }
-- Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
/-- In this version of the lemma, the inclusion homs `iUV` can be specified directly by the user,
which can be more convenient in practice.
 -/
TopCat.Sheaf.eq_of_locally_eq' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.HasLimitsOfSize.{x, x, v_1, u_1} C] [(CategoryTheory.forget C).ReflectsIsomorphisms]
  [CategoryTheory.Limits.PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)] {X : TopCat}
  (F : TopCat.Sheaf C X) {ι : Type u_4} (U : ι → TopologicalSpace.Opens ↑X) (V : TopologicalSpace.Opens ↑X)
  (iUV : (i : ι) → U i ⟶ V),
  V ≤ iSup U →
    ∀ (s t : CategoryTheory.ToType (F.obj.obj (Opposite.op V))),
      (∀ (i : ι),
          (CategoryTheory.ConcreteCategory.hom (F.obj.map (iUV i).op)) s =
            (CategoryTheory.ConcreteCategory.hom (F.obj.map (iUV i).op)) t) →
        s = t
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_const_mul_id : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (r : R) (a : A),
  autoParam (p a) cfc_const_mul_id._auto_1 → cfc (fun x => r * x) a = r • a
-- Mathlib.Algebra.Order.Star.Basic
star_right_conjugate_nonneg : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {a : R}, 0 ≤ a → ∀ (c : R), 0 ≤ c * a * star c
-- Init.Data.Vector.Lemmas
Vector.getElem?_set! : ∀ {α : Type u_1} {n i j : ℕ} {xs : Vector α n} {x : α},
  (xs.set! i x)[j]? = if i = j then if i < n then some x else none else xs[j]?
-- Init.Data.Float.Model.Float32
Float32.Model.instAdd : Add Float32.Model
-- Mathlib.CategoryTheory.Limits.Presentation
/-- The canonical colimit presentation of any object over a point.  -/
CategoryTheory.Limits.ColimitPresentation.self : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → (X : C) → CategoryTheory.Limits.ColimitPresentation PUnit.{s + 1} X
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.card_aux₁ : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {P : Finpartition Finset.univ} {u : Finset α},
  u.card =
      Fintype.card α / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card +
        (Fintype.card α / P.parts.card -
          Fintype.card α / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card) →
    (4 ^ P.parts.card -
            (Fintype.card α / P.parts.card -
              Fintype.card α / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card)) *
          (Fintype.card α / SzemerediRegularity.stepBound P.parts.card) +
        (Fintype.card α / P.parts.card -
            Fintype.card α / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card) *
          (Fintype.card α / SzemerediRegularity.stepBound P.parts.card + 1) =
      u.card
-- Mathlib.Data.Quot
/-- Always-true relation as a `Setoid`.

Note that in later files the preferred spelling is `⊤ : Setoid α`.  -/
trueSetoid : {α : Sort u_1} → Setoid α
-- Mathlib.Data.Real.Basic
Real.ratCast_lt : ∀ {x y : ℚ}, ↑x < ↑y ↔ x < y
-- Init.Prelude
of_decide_eq_self_eq_true : ∀ {α : Sort u_1} [inst : DecidableEq α] (a : α), decide (a = a) = true
-- Mathlib.Algebra.Algebra.Prod
AlgHom.fst_apply : ∀ (R : Type u_1) {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (a : A × B), (AlgHom.fst R A B) a = a.1
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.enrichedHom_condition'_assoc : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] {i j : J} (f : i ⟶ j) {Z : V}
  (h : (F₁.obj i ⟶[V] F₂.obj j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedHomπ V F₁ F₂ i)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F₁.obj i ⟶[V] F₂.obj i)).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F₁.obj i ⟶[V] F₂.obj i)
            ((CategoryTheory.eHomEquiv V) (F₂.map f)))
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j)) h))) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedHomπ V F₁ F₂ j)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F₁.obj j ⟶[V] F₂.obj j)).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((CategoryTheory.eHomEquiv V) (F₁.map f))
            (F₁.obj j ⟶[V] F₂.obj j))
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)) h)))
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.mul_spec_asOver_spec_left : ∀ {R A : CommRingCat} [inst : Bialgebra ↑R ↑A],
  CategoryTheory.Over.Hom.left CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso ↑R ↑A ↑A).hom
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑(Bialgebra.comulAlgHom ↑R ↑A)))
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- The localization of a torsion-free monoid is torsion-free.  -/
AddLocalization.instIsAddTorsionFree : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} [IsAddTorsionFree M],
  IsAddTorsionFree (AddLocalization S)
-- Mathlib.Analysis.SpecialFunctions.Log.InvLog
Real.differentiableOn_inv_log' : DifferentiableOn ℝ (fun x => (Real.log x)⁻¹) {-1, 0, 1}ᶜ
-- Mathlib.Data.Vector3
_private.Mathlib.Data.Vector3.0.Fin2.toNat.match_1.eq_1 : ∀ (motive : (x : ℕ) → Fin2 x → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (n + 1) Fin2.fz)
  (h_2 : (n : ℕ) → (i : Fin2 n) → motive (n + 1) i.fs),
  (match n + 1, Fin2.fz with
    | .(n + 1), Fin2.fz => h_1 n
    | .(n + 1), i.fs => h_2 n i) =
    h_1 n
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Sheaf.isLocallyInjective_sheafToPresheaf_map_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] {J : CategoryTheory.GrothendieckTopology C}
  {F₁ F₂ : CategoryTheory.Sheaf J D} (φ : F₁ ⟶ F₂),
  CategoryTheory.Presheaf.IsLocallyInjective J ((CategoryTheory.sheafToPresheaf J D).map φ) ↔
    CategoryTheory.Sheaf.IsLocallyInjective φ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_insertIfNew_le_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k : α} {v : β k},
  (compare (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.minKey! k).isLE = true
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.upperBound?_reverse : ∀ {α : Type u_1} (t : RBTree.RBNode α) (cut : α → Ordering) (ub : Option α),
  RBTree.RBNode.upperBound? cut t.reverse ub = RBTree.RBNode.lowerBound? (fun x => (cut x).swap) t ub
-- Mathlib.Analysis.Normed.Lp.ProdLp
LinearIsometryEquiv.withLpUniqueProd_apply : ∀ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : Semiring 𝕜]
  [inst_1 : SeminormedAddCommGroup α] [inst_2 : Module 𝕜 α] [inst_3 : SeminormedAddCommGroup β] [inst_4 : Module 𝕜 β]
  [inst_5 : Unique α] (x : WithLp p (α × β)), (LinearIsometryEquiv.withLpUniqueProd p 𝕜 α β) x = x.snd
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.mk_left_injective : ∀ {α : Type u_1} [inst : AddCommMonoid α] [IsCancelAdd α] {s : AddSubmonoid α} (b : ↥s),
  Function.Injective fun a => AddLocalization.mk a b
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.Nondegenerate.congr_simp : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : NonUnitalNonAssocSemiring R] [inst_1 : Finite m]
  [inst_2 : Finite n] (M M_1 : Matrix m n R), M = M_1 → M.Nondegenerate = M_1.Nondegenerate
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.instAdd : {ι : Type u_1} →
  {M : Type u_2} →
    [inst : AddCommMonoid M] → {I₀ : WithTop (BoxIntegral.Box ι)} → Add (BoxIntegral.BoxAdditiveMap ι M I₀)