mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.UInt.Bitwise
USize.toUInt16_not : ∀ (a : USize), (~~~a).toUInt16 = ~~~a.toUInt16
-- Mathlib.Topology.MetricSpace.Algebra
Pi.instIsBoundedSMul' : ∀ {ι : Type u_3} [inst : Fintype ι] {α : ι → Type u_4} {β : ι → Type u_5} [inst_1 : (i : ι) → PseudoMetricSpace (α i)]
  [inst_2 : (i : ι) → PseudoMetricSpace (β i)] [inst_3 : (i : ι) → Zero (α i)] [inst_4 : (i : ι) → Zero (β i)]
  [inst_5 : (i : ι) → SMul (α i) (β i)] [∀ (i : ι), IsBoundedSMul (α i) (β i)],
  IsBoundedSMul ((i : ι) → α i) ((i : ι) → β i)
-- Mathlib.Analysis.Analytic.Constructions
/-- The Cartesian product of analytic functions is analytic.  -/
AnalyticAt.prod : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {e : E} {f : E → F} {g : E → G},
  AnalyticAt 𝕜 f e → AnalyticAt 𝕜 g e → AnalyticAt 𝕜 (fun x => (f x, g x)) e
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey!_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF →
    ∀ {k k' : α} {f : Option β → Option β},
      (Std.DTreeMap.Raw.Const.alter t k f).getKey! k' =
        if cmp k k' = Ordering.eq then if (f (Std.DTreeMap.Raw.Const.get? t k)).isSome = true then k else default
        else t.getKey! k'
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Mathlib.Meta.Positivity.log_pos_of_isRat_neg : ∀ {e : ℝ} {d : ℕ} {n : ℤ}, Mathlib.Meta.NormNum.IsRat e n d → decide (↑n / ↑d < -1) = true → 0 < Real.log e
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.instCoeFunForall : {M : Type u_4} → {N : Type u_5} → [inst : Mul M] → [inst_1 : Mul N] → CoeFun (M ≃* N) fun x => M → N
-- Init.Meta.Defs
Lean.NameGenerator.curr : Lean.NameGenerator → Lean.Name
-- Mathlib.RingTheory.PowerSeries.Restricted
PowerSeries.isRestricted.neg : ∀ {R : Type u_1} [inst : NormedRing R] (c : ℝ) {f : PowerSeries R},
  PowerSeries.IsRestricted c f → PowerSeries.IsRestricted c (-f)
-- Mathlib.Algebra.DirectSum.Ring
/-- A graded version of `CommRing`.  -/
DirectSum.GCommRing : {ι : Type u_1} → (A : ι → Type u_2) → [AddCommMonoid ι] → [(i : ι) → AddCommGroup (A i)] → Type (max u_1 u_2)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.zero_lt_getElem!_toList_rcc_iff : ∀ {m n i : ℕ}, 0 < (m...=n).toList[i]! ↔ i < n + 1 - m ∧ 0 < i + m
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_univ`. -/
Set.diff_univ : ∀ {α : Type u_1} (s : Set α), s \ Set.univ = ∅
-- Qq.Macro
Qq.Impl.floatLevelAntiquot' : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadQuotation m] → Lean.Syntax → StateT (Array (Lean.Syntax × Lean.Syntax × Lean.Syntax)) m Lean.Syntax
-- Mathlib.Order.GaloisConnection.Basic
GaloisConnection.lowerBounds_u_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {u : α → β} {l : β → α},
  GaloisConnection l u → ∀ (s : Set α), lowerBounds (u '' s) = l ⁻¹' lowerBounds s
-- Lean.Compiler.Specialize
Lean.Compiler.SpecializeAttributeKind.nospecialize : Lean.Compiler.SpecializeAttributeKind
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_closedBall_mul_of_pos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (x : E) {r : ℝ},
  0 < r →
    ∀ (s : ℝ), μ (Metric.closedBall x (r * s)) = ENNReal.ofReal (r ^ Module.finrank ℝ E) * μ (Metric.closedBall 0 s)
-- Std.Sync.Barrier
_private.Std.Sync.Barrier.0.Std.BarrierState.mk.inj : ∀ {count generationId count_1 generationId_1 : ℕ},
  { count := count, generationId := generationId } = { count := count_1, generationId := generationId_1 } →
    count = count_1 ∧ generationId = generationId_1
-- Mathlib.CategoryTheory.Limits.Types.Products
/-- The categorical binary product in `Type u` is Cartesian product.  -/
CategoryTheory.Limits.Types.binaryProductIso : (X Y : Type u) → X ⨯ Y ≅ X × Y
-- Mathlib.Data.Matrix.Mul
Matrix.mulVec_injective : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonAssocSemiring α] [inst_1 : Fintype n],
  Function.Injective Matrix.mulVec
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.Monadic.isPlausibleStep_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α] {it : Std.IterM Id α}
  {step : Std.IterStep (Std.IterM Id α) α}, it.IsPlausibleStep step ↔ step = Std.Rxc.Iterator.Monadic.step it
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.HasEigenvector.apply_eq_smul : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {x : M}, f.HasEigenvector μ x → f x = μ • x
-- Mathlib.Order.WithBot
WithTop.instBoundedOrder : {α : Type u_1} → [inst : LE α] → [OrderBot α] → BoundedOrder (WithTop α)
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.unshift.eq_2 : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (q : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)) (z : F) (n : ℕ),
  q.unshift z n.succ = (continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm (q n)
-- Mathlib.Algebra.Group.Hom.Basic
ZeroHom.neg_apply : ∀ {M : Type u_8} {N : Type u_9} [inst : Zero M] [inst_1 : NegZeroClass N] (f : ZeroHom M N) (x : M), (-f) x = -f x
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
pinGroup.mem_unitary : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : CliffordAlgebra Q}, x ∈ pinGroup Q → x ∈ unitary (CliffordAlgebra Q)
-- Mathlib.RingTheory.WittVector.Basic
_private.Mathlib.RingTheory.WittVector.Basic.0.WittVector.ghostFun_sub : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (x y : WittVector p R),
  WittVector.ghostFun✝ (x - y) = WittVector.ghostFun✝ x - WittVector.ghostFun✝ y
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The fourth simplicial identity  -/
CategoryTheory.SimplicialObject.δ_comp_σ_of_gt_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {i : Fin (n + 2)} {j : Fin (n + 1)},
  j.castSucc < i →
    ∀ {Z : C} (h : X.obj (Opposite.op { len := n + 1 }) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.σ j.castSucc) (CategoryTheory.CategoryStruct.comp (X.δ i.succ) h) =
        CategoryTheory.CategoryStruct.comp (X.δ i) (CategoryTheory.CategoryStruct.comp (X.σ j) h)
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.isMatcherLikeCore : Lean.Environment → Lean.Name → Bool
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.comp_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {X Y Z : CategoryTheory.Grothendieck F} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).fiber =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp ((F.map g.base).toFunctor.map f.fiber) g.fiber)
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Shift invariance of `carrier` for the additive shift `shift`.  -/
SymbolicDynamics.FullShift.Subshift.mapsTo : ∀ {A : Type u_1} [inst : TopologicalSpace A] {G : Type u_2} [inst_1 : AddMonoid G]
  (self : SymbolicDynamics.FullShift.Subshift A G) (g : G),
  Set.MapsTo (SymbolicDynamics.FullShift.shift g) self.carrier self.carrier
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- Quotienting by equal ideals gives equivalent algebras.  -/
Ideal.quotientEquivAlgOfEq : (R₁ : Type u_1) →
  {A : Type u_3} →
    [inst : CommSemiring R₁] →
      [inst_1 : Ring A] →
        [inst_2 : Algebra R₁ A] →
          {I J : Ideal A} → [inst_3 : I.IsTwoSided] → [inst_4 : J.IsTwoSided] → I = J → (A ⧸ I) ≃ₐ[R₁] A ⧸ J
-- Mathlib.LinearAlgebra.Projectivization.PSL.PSL2
/-- SL-level generation: in the 2-element-index case, the join of the two `lineStab` subgroups
attached to the two coordinate axes is all of `SL ι F`.  -/
SL2Gen.SL_card_two_lineStab_sup_eq_top : ∀ {F : Type u_2} [inst : Field F],
  Matrix.SpecialLinearGroup.lineStab (F ∙ Pi.single 0 1) ⊔ Matrix.SpecialLinearGroup.lineStab (F ∙ Pi.single 1 1) = ⊤
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.homogeneousLocalizationAlgebra : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubgroupClass σ A] →
            [inst_3 : AddCommMonoid ι] →
              [inst_4 : DecidableEq ι] →
                {𝒜 : ι → σ} →
                  [inst_5 : GradedRing 𝒜] → {x : Submonoid A} → Algebra (HomogeneousLocalization 𝒜 x) (Localization x)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.HasSubobjectClassifier.truthIsSplitMono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasSubobjectClassifier C],
  CategoryTheory.IsSplitMono (CategoryTheory.HasSubobjectClassifier.truth C)
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.addMonoidHomCongrRight_apply : ∀ {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N₁]
  [inst_2 : AddCommMonoid N₂] (e : N₁ ≃+ N₂) (hmn : M →+ N₁), e.addMonoidHomCongrRight hmn = (↑e).comp hmn
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Comonad.isSplitEpi_iff_isIso_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Comonad C) (X : C)
  [CategoryTheory.IsIso T.δ], CategoryTheory.IsSplitEpi (T.ε.app X) ↔ CategoryTheory.IsIso (T.ε.app X)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_smul : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (A : Matrix n n R)
  (c : R), (c • A).det = c ^ Fintype.card n * A.det
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.MorphismProperty.morphismProperty_precoverage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.MorphismProperty C),
  P.precoverage.morphismProperty = P
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.basisRightAngleRotation.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o o_1 : Orientation ℝ E (Fin 2)),
  o = o_1 →
    ∀ (x x_1 : E) (e_x : x = x_1) (hx : x ≠ 0), o.basisRightAngleRotation x hx = o_1.basisRightAngleRotation x_1 ⋯
-- Mathlib.Data.Finite.Prod
Set.infinite_image2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : Set α} {t : Set β},
  (∀ b ∈ t, Set.InjOn (fun a => f a b) s) →
    (∀ a ∈ s, Set.InjOn (f a) t) → ((Set.image2 f s t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty)
-- Mathlib.SetTheory.Lists
/-- Equivalence of ZFA lists. Defined inductively.  -/
Lists.Equiv : {α : Type u_1} → Lists α → Lists α → Prop
-- Mathlib.Tactic.Algebra.Basic
/-- Decide if a coefficient is 1.  -/
Mathlib.Tactic.Algebra.RingCompute.isOne : {u v : Lean.Level} →
  {R : Q(Type u)} →
    {A : Q(Type v)} →
      {sR : Q(CommSemiring «$R»)} →
        {sA : Q(CommSemiring «$A»)} →
          (sAlg : Q(Algebra «$R» «$A»)) →
            Mathlib.Tactic.Ring.Common.Cache sR →
              {x : Q(«$A»)} → Mathlib.Tactic.Algebra.BaseType sAlg x → Option Q(Mathlib.Meta.NormNum.IsNat «$x» 1)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
SheafOfModules.evaluationPreservesLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Sheaf J RingCat}
  (F : CategoryTheory.Functor D (SheafOfModules R))
  [∀ (X : Cᵒᵖ),
      Small.{v, max u₂ v}
        ↑((F.comp (SheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj.obj X)))).sections]
  [CategoryTheory.Limits.HasLimitsOfShape D AddCommGrpCat] (X : Cᵒᵖ),
  CategoryTheory.Limits.PreservesLimit F (SheafOfModules.evaluation R X)
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.pos_of_isRat : ∀ {A : Type u_1} {e : A} {n : ℤ} {d : ℕ} [inst : Ring A] [inst_1 : LinearOrder A] [IsStrictOrderedRing A],
  Mathlib.Meta.NormNum.IsRat e n d → decide (0 < n) = true → 0 < e
-- Mathlib.Algebra.Ring.Parity
odd_sub_two : ∀ {α : Type u_2} [inst : Ring α] {a : α}, Odd (a - 2) ↔ Odd a
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasFDerivWithinAt.add : ∀ {𝕜 : 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] {f g : E → F}
  {f' g' : E →L[𝕜] F} {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x → HasFDerivWithinAt g g' s x → HasFDerivWithinAt (f + g) (f' + g') s x
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_zero : ∀ (a : ℤ), a.tdiv 0 = 0
-- Mathlib.Analysis.RCLike.Basic
RCLike.normSq_eq_zero : ∀ {K : Type u_1} [inst : RCLike K] {z : K}, RCLike.normSq z = 0 ↔ z = 0
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.commMonoid.eq_1 : ∀ {α : Type u_2} [inst : CommMonoid α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α],
  NonemptyInterval.commMonoid =
    { toMul := instMulNonemptyInterval, mul_assoc := ⋯, toOne := instOneNonemptyInterval, one_mul := ⋯, mul_one := ⋯,
      toNPow := NPow.ofPow, npow_zero := ⋯, npow_succ := ⋯, mul_comm := ⋯ }
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.neg_1 : ∀ {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}
  (x x' : CommRingCat.Colimits.Prequotient F) (x_1 : CommRingCat.Colimits.Relation F x x'),
  CommRingCat.Colimits.Relation.below x_1 → motive x x' x_1 → CommRingCat.Colimits.Relation.below ⋯
-- Mathlib.Topology.Instances.Int
Int.dist_eq' : ∀ (m n : ℤ), dist m n = ↑|m - n|
-- Lean.Data.NameTrie
Lean.NameTrie.find? : {β : Type u_1} → Lean.NameTrie β → Lean.Name → Option β
-- Mathlib.Analysis.RCLike.Inner
RCLike.wInner_one_eq_sum : ∀ {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [inst : Fintype ι] [inst_1 : RCLike 𝕜]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → InnerProductSpace 𝕜 (E i)]
  (f g : (i : ι) → E i), ⟪f, g⟫_[𝕜] = ∑ i, inner 𝕜 (f i) (g i)
-- Mathlib.Algebra.Category.AlgCat.Basic
/-- The equivalence of categories of `ℤ`-algebras and rings.  -/
AlgCat.intEquivalence : AlgCat ℤ ≌ RingCat
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
/-- A morphism between the cocomplexes  -/
CategoryTheory.ProjectiveResolution.Hom.hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {Z : C} →
          {P : CategoryTheory.ProjectiveResolution Z} →
            {Z' : C} →
              {P' : CategoryTheory.ProjectiveResolution Z'} → {f : Z ⟶ Z'} → P.Hom P' f → (P.complex ⟶ P'.complex)
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt) (X : C),
  CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncGE.obj a).map ((t.eTruncLTι b).app X)))
      ((t.eTruncLTGEIsoGELT a b).hom.app X) =
    (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X))
-- Mathlib.Data.QPF.Multivariate.Constructions.Prj
MvQPF.Prj.mvfunctor : {n : ℕ} → (i : Fin2 n) → MvFunctor (MvQPF.Prj i)
-- Mathlib.CategoryTheory.Sites.Canonical
CategoryTheory.GrothendieckTopology.yoneda_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X Y : C} (f : X ⟶ Y), (J.yoneda.map f).hom = CategoryTheory.yoneda.map f
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.le_mk_sdiff_add_mk : ∀ {α : Type u} (S T : Set α), Cardinal.mk ↑S ≤ Cardinal.mk ↑(S \ T) + Cardinal.mk ↑T
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.instInhabitedRingMode : Inhabited Mathlib.Tactic.RingNF.RingMode
-- Init.Data.String.Defs
String.instHSubRawSlice : HSub String.Pos.Raw String.Slice String.Pos.Raw
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.erased.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity}, sizeOf Lean.Compiler.LCNF.LetValue.erased = 1
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
/-- A normal element whose `ℂ`-quasispectrum is contained in `ℝ` is selfadjoint.  -/
QuasispectrumRestricts.isSelfAdjoint : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A] [inst_3 : Module ℂ A]
  [inst_4 : IsScalarTower ℂ A A] [inst_5 : SMulCommClass ℂ A A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal]
  (a : A), QuasispectrumRestricts a ⇑Complex.reCLM → ∀ [IsStarNormal a], IsSelfAdjoint a
-- Mathlib.Analysis.RCLike.Basic
/-- The canonical map between `RCLike` types. It maps `x : 𝕜` to `re x + im x * I`.  -/
RCLike.map : (𝕜 : Type u_3) → (𝕜' : Type u_4) → [inst : RCLike 𝕜] → [inst_1 : RCLike 𝕜'] → 𝕜 →L[ℝ] 𝕜'
-- Lean.Syntax
Lean.Syntax.Traverser.mk.inj : ∀ {cur : Lean.Syntax} {parents : Array Lean.Syntax} {idxs : Array ℕ} {cur_1 : Lean.Syntax}
  {parents_1 : Array Lean.Syntax} {idxs_1 : Array ℕ},
  { cur := cur, parents := parents, idxs := idxs } = { cur := cur_1, parents := parents_1, idxs := idxs_1 } →
    cur = cur_1 ∧ parents = parents_1 ∧ idxs = idxs_1
-- Mathlib.Algebra.Group.Defs
/-- `a ^ (n + 1) = a ^ n * a`  -/
DivInvMonoid.zpow_succ' : ∀ {G : Type u} [self : DivInvMonoid G] (n : ℕ) (a : G), a ^ ↑n.succ = a ^ ↑n * a
-- Mathlib.NumberTheory.Zsqrtd.Basic
_private.Mathlib.NumberTheory.Zsqrtd.Basic.0.Zsqrtd.Nonnegg.match_1.eq_2 : ∀ (motive : ℤ → ℤ → Sort u_1) (a b : ℕ) (h_1 : (a b : ℕ) → motive (Int.ofNat a) (Int.ofNat b))
  (h_2 : (a b : ℕ) → motive (Int.ofNat a) (Int.negSucc b)) (h_3 : (a b : ℕ) → motive (Int.negSucc a) (Int.ofNat b))
  (h_4 : (a a_1 : ℕ) → motive (Int.negSucc a) (Int.negSucc a_1)),
  (match Int.ofNat a, Int.negSucc b with
    | Int.ofNat a, Int.ofNat b => h_1 a b
    | Int.ofNat a, Int.negSucc b => h_2 a b
    | Int.negSucc a, Int.ofNat b => h_3 a b
    | Int.negSucc a, Int.negSucc a_1 => h_4 a a_1) =
    h_2 a b
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
/-- A split coequalizer diagram consists of morphisms

      f   π
    X ⇉ Y → Z
      g

satisfying `f ≫ π = g ≫ π` together with morphisms

      t   s
    X ← Y ← Z

satisfying `s ≫ π = 𝟙 Z`, `t ≫ g = 𝟙 Y` and `t ≫ f = π ≫ s`.

The name "coequalizer" is appropriate, since any split coequalizer is a coequalizer, see
`CategoryTheory.IsSplitCoequalizer.isCoequalizer`.
Split coequalizers are also absolute, since a functor preserves all the structure above.
 -/
CategoryTheory.IsSplitCoequalizer : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ⟶ Y) → (X ⟶ Y) → {Z : C} → (Y ⟶ Z) → Type v
-- Mathlib.Order.Category.Semilat
SemilatInfCat.dual_obj_X : ∀ (X : SemilatInfCat), (SemilatInfCat.dual.obj X).X = X.Xᵒᵈ
-- Mathlib.Order.Filter.Pointwise
Filter.vadd_bot : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f : Filter α}, f +ᵥ ⊥ = ⊥
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.IterM.step_intermediateDropWhileWithPostcondition.match_3.eq_3 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (h : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Init.Data.UInt.Lemmas
UInt8.ofNat_uInt64ToNat : ∀ (n : UInt64), UInt8.ofNat n.toNat = n.toUInt8
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_diff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, (m₁.diff m₂).get? k = if m₂.contains k = true then none else m₁.get? k
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.succ_natCast : ∀ (n : ℕ), Order.succ ↑n = ↑n + 1
-- Mathlib.Topology.Order.Lattice
/-- The supremum is continuous  -/
ContinuousSup.continuous_sup : ∀ {L : Type u_1} {inst : TopologicalSpace L} {inst_1 : Max L} [self : ContinuousSup L], Continuous fun p => p.1 ⊔ p.2
-- Init.Data.Iterators.Basic
Std.Iterators.FinitenessRelation.mk.injEq : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β]
  (Rel : Std.IterM m β → Std.IterM m β → Prop) (wf : WellFounded Rel)
  (subrelation : ∀ {it it' : Std.IterM m β}, it'.IsPlausibleSuccessorOf it → Rel it' it)
  (Rel_1 : Std.IterM m β → Std.IterM m β → Prop) (wf_1 : WellFounded Rel_1)
  (subrelation_1 : ∀ {it it' : Std.IterM m β}, it'.IsPlausibleSuccessorOf it → Rel_1 it' it),
  ({ Rel := Rel, wf := wf, subrelation := subrelation } = { Rel := Rel_1, wf := wf_1, subrelation := subrelation_1 }) =
    (Rel = Rel_1)
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_pow : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : FunLike F R S]
  [rc : RingHomClass F R S] (f : F) (I : Ideal R) (n : ℕ), Ideal.map f (I ^ n) = Ideal.map f I ^ n
-- Init.Data.Rat.Basic
Rat.normalize.den_nz : ∀ {num : ℤ} {den g : ℕ}, den ≠ 0 → g = num.natAbs.gcd den → den / g ≠ 0
-- Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
CategoryTheory.instMonoFunctorWhiskerRightOfPreservesMonomorphisms : ∀ {K : Type u} [inst : CategoryTheory.Category.{v, u} K] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {D : Type u''} [inst_2 : CategoryTheory.Category.{v'', u''} D] {F G : CategoryTheory.Functor K C} (f : F ⟶ G)
  [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Mono f] (H : CategoryTheory.Functor C D)
  [H.PreservesMonomorphisms], CategoryTheory.Mono (CategoryTheory.Functor.whiskerRight f H)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_smul : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : SMulZeroClass S R] (a : S) (b : Polynomial R),
  (a • b).toFinsupp = a • b.toFinsupp
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
DifferentiableOn.continuousMultilinear_apply_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {ι : Type u_5} {M : ι → Type u_6} [inst_3 : (i : ι) → NormedAddCommGroup (M i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (M i)] {H : Type u_7} [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H]
  {c : E → ContinuousMultilinearMap 𝕜 M H} [Finite ι],
  DifferentiableOn 𝕜 c s → ∀ (u : (i : ι) → M i), DifferentiableOn 𝕜 (fun y => (c y) u) s
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' fallback : α},
  cmp k k' = Ordering.eq → t.getKeyD k fallback = t.getKeyD k' fallback
-- Mathlib.CategoryTheory.Products.Unitor
/-- The equivalence of categories expressing left unity of products of categories.  -/
CategoryTheory.prod.leftUnitorEquivalence : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Discrete PUnit.{w + 1} × C ≌ C