mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Creates
/-- The identity functor creates all limits.  -/
CategoryTheory.idCreatesLimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₁, u₁, u₁} (CategoryTheory.Functor.id C)
-- Mathlib.CategoryTheory.Subfunctor.OfSection
CategoryTheory.Subfunctor.ofSection_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : Cᵒᵖ}
  (x : F.obj X) (U : Cᵒᵖ),
  (CategoryTheory.Subfunctor.ofSection x).obj U = {u | ∃ f, (CategoryTheory.ConcreteCategory.hom (F.map f)) x = u}
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.logMap_normAtAllPlaces : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K),
  NumberField.mixedEmbedding.logMap
      (NumberField.mixedEmbedding.mixedSpaceOfRealSpace (NumberField.mixedEmbedding.normAtAllPlaces x)) =
    NumberField.mixedEmbedding.logMap x
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.support_mono : ∀ {V : Type u} {G G' : SimpleGraph V}, G ≤ G' → G.support ⊆ G'.support
-- Init.Data.String.Iterator
String.Legacy.Iterator.sizeOf_eq : ∀ (i : String.Legacy.Iterator), sizeOf i = i.s.utf8ByteSize - i.i.byteIdx
-- Mathlib.CategoryTheory.Monad.Algebra
/-- Given a monad morphism from `T₂` to `T₁`, we get a functor from the algebras of `T₁` to algebras of
`T₂`.
 -/
CategoryTheory.Monad.algebraFunctorOfMonadHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T₁ T₂ : CategoryTheory.Monad C} → (T₂ ⟶ T₁) → CategoryTheory.Functor T₁.Algebra T₂.Algebra
-- Mathlib.LinearAlgebra.Pi
LinearEquiv.funUnique_symm_apply : ∀ (ι : Type u_5) (R : Type u_6) (M : Type u_7) [inst : Unique ι] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M], ⇑(LinearEquiv.funUnique ι R M).symm = ⇑(AddEquiv.funUnique ι M).symm
-- Std.Time.Format.Modifier
Std.Time.ZoneName.short.sizeOf_spec : sizeOf Std.Time.ZoneName.short = 1
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsLittleO.right_isBigO_sub : ∀ {α : Type u_1} {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {l : Filter α} {f₁ f₂ : α → E'},
  f₁ =o[l] f₂ → f₂ =O[l] fun x => f₂ x - f₁ x
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.dropLast_cons_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v w w' : V} (h : G.Adj u v) (h₂ : G.Adj v w) (p : G.Walk w w'),
  (SimpleGraph.Walk.cons h (SimpleGraph.Walk.cons h₂ p)).dropLast =
    SimpleGraph.Walk.cons h (SimpleGraph.Walk.cons h₂ p).dropLast
-- Mathlib.Order.Notation
HasCompl.mk : {α : Type u_1} → (α → α) → HasCompl α
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsFinite.instOfIsIsoScheme : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f], AlgebraicGeometry.IsFinite f
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- The remainder `r` in Weierstrass division, denoted by `f %ʷ g`. Note that when the image of
`g` in the residue field is zero, this is defined to be zero.  -/
PowerSeries.weierstrassMod : {A : Type u_1} →
  [inst : CommRing A] →
    [inst_1 : IsLocalRing A] →
      PowerSeries A → PowerSeries A → [IsPrecomplete (IsLocalRing.maximalIdeal A) A] → Polynomial A
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoTree.brecOn_3.eq : ∀ {motive_1 : Lean.Elab.InfoTree → Sort u} {motive_2 : Lean.PersistentArray Lean.Elab.InfoTree → Sort u}
  {motive_3 : Lean.PersistentArrayNode Lean.Elab.InfoTree → Sort u} {motive_4 : Array Lean.Elab.InfoTree → Sort u}
  {motive_5 : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u}
  {motive_6 : List Lean.Elab.InfoTree → Sort u} {motive_7 : List (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u}
  (t : Array Lean.Elab.InfoTree) (F_1 : (t : Lean.Elab.InfoTree) → t.below → motive_1 t)
  (F_2 : (t : Lean.PersistentArray Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_1 t → motive_2 t)
  (F_3 : (t : Lean.PersistentArrayNode Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_2 t → motive_3 t)
  (F_4 : (t : Array Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_3 t → motive_4 t)
  (F_5 : (t : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree)) → Lean.Elab.InfoTree.below_4 t → motive_5 t)
  (F_6 : (t : List Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_5 t → motive_6 t)
  (F_7 : (t : List (Lean.PersistentArrayNode Lean.Elab.InfoTree)) → Lean.Elab.InfoTree.below_6 t → motive_7 t),
  Lean.Elab.InfoTree.brecOn_3 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 =
    F_4 t (Lean.Elab.InfoTree.brecOn_3.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7).2
-- Mathlib.RingTheory.PrincipalIdealDomain
IsBezout.dvd_gcd : ∀ {R : Type u} [inst : CommRing R] {x y z : R} [inst_1 : Submodule.IsPrincipal (Ideal.span {x, y})],
  z ∣ x → z ∣ y → z ∣ IsBezout.gcd x y
-- Mathlib.SetTheory.Ordinal.Veblen
/-- `veblenWith f o` is always normal for `o ≠ 0`. See `isNormal_veblenWith` for a version which
assumes `IsNormal f`.  -/
Ordinal.isNormal_veblenWith' : ∀ {o : Ordinal.{u}} (f : Ordinal.{u} → Ordinal.{u}), o ≠ 0 → Order.IsNormal (Ordinal.veblenWith f o)
-- Mathlib.Order.CompleteLattice.Chain
/-- **Hausdorff's maximality principle**

There exists a maximal totally ordered set of `α`.
Note that we do not require `α` to be partially ordered by `r`.  -/
maxChain_spec : ∀ {α : Type u_1} {r : α → α → Prop}, IsMaxChain r (maxChain r)
-- Std.Http.Data.Status
/-- 401 Unauthorized
 -/
Std.Http.Status.unauthorized : Std.Http.Status
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelIsoOfEq_inv_comp_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f g : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f] [inst_3 : CategoryTheory.Limits.HasKernel g] (h : f = g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelIsoOfEq h).inv (CategoryTheory.Limits.kernel.ι f) =
    CategoryTheory.Limits.kernel.ι g
-- Mathlib.Data.Finset.PImage
/-- Convert an `o : Part α` with decidable `Part.Dom o` to `Finset α`.  -/
Part.toFinset : {α : Type u_1} → (o : Part α) → [Decidable o.Dom] → Finset α
-- Mathlib.Data.Set.Function
Set.RightInvOn.eqOn : ∀ {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β} {f' : β → α}, Set.RightInvOn f' f t → Set.EqOn (f ∘ f') id t
-- Mathlib.Algebra.Order.Group.Opposite
AddOpposite.one_le_op : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] {a : α}, 1 ≤ AddOpposite.op a ↔ 1 ≤ a
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.subset_iff : ∀ {x y : PSet.{u_1}}, ZFSet.mk x ⊆ ZFSet.mk y ↔ x ⊆ y
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.mk'.sizeOf_spec : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : SizeOf C] [inst_3 : SizeOf D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C)
  (unitIso : CategoryTheory.Functor.id C ≅ functor.comp inverse)
  (counitIso : inverse.comp functor ≅ CategoryTheory.Functor.id D)
  (functor_unitIso_comp :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (functor.map (unitIso.hom.app X)) (counitIso.hom.app (functor.obj X)) =
          CategoryTheory.CategoryStruct.id (functor.obj X))
      CategoryTheory.Equivalence.functor_unitIso_comp._autoParam),
  sizeOf
      { functor := functor, inverse := inverse, unitIso := unitIso, counitIso := counitIso,
        functor_unitIso_comp := functor_unitIso_comp } =
    1 + sizeOf functor + sizeOf inverse + sizeOf unitIso + sizeOf counitIso
-- Mathlib.CategoryTheory.Monad.Types
CategoryTheory.kleisliCatEquivKleisli_counitIso : ∀ (m : Type u → Type u) [inst : Monad m] [inst_1 : LawfulMonad m],
  (CategoryTheory.kleisliCatEquivKleisli m).counitIso =
    CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.Iso.refl X) ⋯
-- Init.Data.List.Sublist
List.suffix_concat_iff : ∀ {α : Type u_1} {l₁ l₂ : List α} {a : α}, l₁ <:+ l₂ ++ [a] ↔ l₁ = [] ∨ ∃ t, l₁ = t ++ [a] ∧ t <:+ l₂
-- Mathlib.Logic.Function.Basic
Function.onFun_onFun_eq : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (f : α → α → γ) (g : β → α) (h : δ → β),
  Function.onFun (Function.onFun f g) h = Function.onFun f (g ∘ h)
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.holo' : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (self : ModularForm Γ k), MDiff ⇑self.toSlashInvariantForm
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.concaveOn_cfcₙ_of_concaveOn_cfc : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {f : ℝ → ℝ} {s : Set A},
  ConcaveOn ℝ (Unitization.inr '' s) (cfc f) → ConcaveOn ℝ s (cfcₙ f)
-- Init.Prelude
/-- A `macro` has type `Macro`, which is a `Syntax → MacroM Syntax`: it
receives an input syntax and is supposed to "expand" it into another piece of
syntax.
 -/
Lean.Macro : Type
-- Mathlib.Topology.UnitInterval
Set.Icc.addNSMul.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] {a b : α} (h : a ≤ b) (δ : α) (n : ℕ),
  Set.Icc.addNSMul h δ n = Set.projIcc a b h (a + n • δ)
-- Mathlib.Algebra.Free
FreeMagma.instLawfulTraversable : LawfulTraversable FreeMagma
-- Mathlib.Algebra.GroupWithZero.Commute
Commute.inv_left₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {a b : G₀}, Commute a b → Commute a⁻¹ b
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.le_fromEdgeSet_iff : ∀ {V : Type u} (G : SimpleGraph V) (s : Set (Sym2 V)), G ≤ SimpleGraph.fromEdgeSet s ↔ G.edgeSet ⊆ s
-- Mathlib.Data.FinEnum
FinEnum.Subtype.finEnum : {α : Type u} → [FinEnum α] → (p : α → Prop) → [DecidablePred p] → FinEnum { x // p x }
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.mk_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F : CategoryTheory.Functor C V), { functor := F }.functor = F
-- Mathlib.Analysis.Normed.Group.Basic
mem_ball_iff_norm''' : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] {a b : E} {r : ℝ}, b ∈ Metric.ball a r ↔ ‖a / b‖ < r
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.apply_le_norm : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] (f : C(α, ℝ)) (x : α), f x ≤ ‖f‖
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_alter_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)}, k ∈ m.alter k f ↔ (f (m.get? k)).isSome = true
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Ico_mul_Ioc_subset' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] [MulLeftStrictMono α] [MulRightStrictMono α] (a b c d : α),
  Set.Ico a b * Set.Ioc c d ⊆ Set.Ioo (a * c) (b * d)
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
/-- A `2 × 2` matrix is *hyperbolic* if its discriminant is strictly positive.  -/
Matrix.IsHyperbolic : {R : Type u_1} → [CommRing R] → [Preorder R] → Matrix (Fin 2) (Fin 2) R → Prop
-- Mathlib.MeasureTheory.Constructions.UnitInterval
unitInterval.measurable_symm : Measurable unitInterval.symm
-- Mathlib.Combinatorics.Quiver.Covering
/-- A prefunctor is a covering of quivers if it defines bijections on all stars and costars.  -/
Prefunctor.IsCovering : {U : Type u_1} → [inst : Quiver U] → {V : Type u_2} → [inst_1 : Quiver V] → U ⥤q V → Prop
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
MeasureTheory.TendstoInMeasure.congr' : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : EDist E]
  {l : Filter ι} {f f' : ι → α → E} {g g' : α → E},
  (∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i) →
    g =ᵐ[μ] g' → MeasureTheory.TendstoInMeasure μ f l g → MeasureTheory.TendstoInMeasure μ f' l g'
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.ofList_eq_insertMany_empty : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α}, Std.TreeSet.Raw.ofList l cmp = ∅.insertMany l
-- Mathlib.RingTheory.Polynomial.Subring
Polynomial.coeffs_ofSubring : ∀ {R : Type u_1} [inst : Ring R] (T : Subring R) {p : Polynomial ↥T}, ↑(Polynomial.ofSubring T p).coeffs ⊆ ↑T
-- Mathlib.Topology.WithTopology
WithTopology.preimage_ofTopology : ∀ {X : Type u_1} (t : TopologicalSpace X) (s : Set X), WithTopology.ofTopology ⁻¹' s = WithTopology.toTopology t '' s
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cone.forget`.

---

Forget the cone structure and obtain just the cone point.  -/
CategoryTheory.Limits.Cones.forget : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        (F : CategoryTheory.Functor J C) → CategoryTheory.Functor (CategoryTheory.Limits.Cone F) C
-- Aesop.Tree.Data
Aesop.TreeSpec.mk.inj : ∀ {Goal Rapp MVarCluster : Type} {introGoal : Aesop.GoalData Rapp MVarCluster → Goal}
  {elimGoal : Goal → Aesop.GoalData Rapp MVarCluster} {introRapp : Aesop.RappData Goal MVarCluster → Rapp}
  {elimRapp : Rapp → Aesop.RappData Goal MVarCluster} {introMVarCluster : Aesop.MVarClusterData Goal Rapp → MVarCluster}
  {elimMVarCluster : MVarCluster → Aesop.MVarClusterData Goal Rapp} {Goal_1 Rapp_1 MVarCluster_1 : Type}
  {introGoal_1 : Aesop.GoalData Rapp_1 MVarCluster_1 → Goal_1}
  {elimGoal_1 : Goal_1 → Aesop.GoalData Rapp_1 MVarCluster_1}
  {introRapp_1 : Aesop.RappData Goal_1 MVarCluster_1 → Rapp_1}
  {elimRapp_1 : Rapp_1 → Aesop.RappData Goal_1 MVarCluster_1}
  {introMVarCluster_1 : Aesop.MVarClusterData Goal_1 Rapp_1 → MVarCluster_1}
  {elimMVarCluster_1 : MVarCluster_1 → Aesop.MVarClusterData Goal_1 Rapp_1},
  { Goal := Goal, Rapp := Rapp, MVarCluster := MVarCluster, introGoal := introGoal, elimGoal := elimGoal,
        introRapp := introRapp, elimRapp := elimRapp, introMVarCluster := introMVarCluster,
        elimMVarCluster := elimMVarCluster } =
      { Goal := Goal_1, Rapp := Rapp_1, MVarCluster := MVarCluster_1, introGoal := introGoal_1, elimGoal := elimGoal_1,
        introRapp := introRapp_1, elimRapp := elimRapp_1, introMVarCluster := introMVarCluster_1,
        elimMVarCluster := elimMVarCluster_1 } →
    Goal = Goal_1 ∧
      Rapp = Rapp_1 ∧
        MVarCluster = MVarCluster_1 ∧
          introGoal ≍ introGoal_1 ∧
            elimGoal ≍ elimGoal_1 ∧
              introRapp ≍ introRapp_1 ∧
                elimRapp ≍ elimRapp_1 ∧ introMVarCluster ≍ introMVarCluster_1 ∧ elimMVarCluster ≍ elimMVarCluster_1
-- Mathlib.RingTheory.SimpleModule.Isotypic
IsIsotypicOfType.of_isotypicComponent_eq_top : ∀ {R : Type u_2} {M : Type u} {S : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup S]
  [inst_3 : Module R M] [inst_4 : Module R S] [IsSimpleModule R S], isotypicComponent R M S = ⊤ → IsIsotypicOfType R M S
-- Mathlib.Data.Multiset.Dedup
Multiset.dedup_subset : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), s.dedup ⊆ s
-- Mathlib.Condensed.TopComparison
/-- An auxiliary lemma to that allows us to use `IsQuotientMap.lift` in the proof of
`equalizerCondition_yonedaPresheaf`.
 -/
factorsThrough_of_pullbackCondition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C TopCat) (X : Type w')
  [inst_1 : TopologicalSpace X] {Z B : C} {π : Z ⟶ B} [inst_2 : CategoryTheory.Limits.HasPullback π π]
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan π π) G] {a : C(↑(G.obj Z), X)},
  ⇑a ∘ ⇑(CategoryTheory.ConcreteCategory.hom (G.map (CategoryTheory.Limits.pullback.fst π π))) =
      ⇑a ∘ ⇑(CategoryTheory.ConcreteCategory.hom (G.map (CategoryTheory.Limits.pullback.snd π π))) →
    Function.FactorsThrough ⇑a ⇑(CategoryTheory.ConcreteCategory.hom (G.map π))
-- Mathlib.Order.Heyting.Basic
CoheytingAlgebra.toBoundedOrder.eq_1 : ∀ {α : Type u_2} [inst : CoheytingAlgebra α],
  CoheytingAlgebra.toBoundedOrder = { toOrderTop := inst.toOrderTop, toOrderBot := inst.toOrderBot }
-- Mathlib.Algebra.Order.Group.PosPart
/-- See also `negPart_nonpos`.  -/
negPart_nonpos' : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : SubNegMonoid α] {a : α}, a⁻ ≤ 0 ↔ -a ≤ 0
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
/-- Implementation detail:
the object level of `pairwiseToOpensLeCover : Pairwise ι ⥤ OpensLeCover U`
 -/
TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverObj : {X : TopCat} →
  {ι : Type u_2} →
    (U : ι → TopologicalSpace.Opens ↑X) → CategoryTheory.Pairwise ι → TopCat.Presheaf.SheafCondition.OpensLeCover U
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A constant multiplier of the weights in `weightedVSubOfPoint` may be moved outside the
sum.  -/
Finset.weightedVSubOfPoint_const_smul : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (b : P) (c : k),
  (s.weightedVSubOfPoint p b) (c • w) = c • (s.weightedVSubOfPoint p b) w
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_hom_app_hom₁ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero C).hom.app X).hom₁ =
    (CategoryTheory.shiftFunctorZero C ℤ).hom.app X.obj₁
-- Mathlib.Topology.Category.FinTopCat
FinTopCat.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} FinTopCat
-- Mathlib.Algebra.Group.PUnit
PUnit.one_eq : 1 = PUnit.unit
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.indicatorConstLp_inj : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {s t : Set α} (hs : MeasurableSet s) (hsμ : μ s ≠ ⊤) (ht : MeasurableSet t)
  (htμ : μ t ≠ ⊤) {c : E},
  c ≠ 0 → (MeasureTheory.indicatorConstLp p hs hsμ c = MeasureTheory.indicatorConstLp p ht htμ c ↔ s =ᵐ[μ] t)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.id_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.AddMonObj A] (M : CategoryTheory.AddMod D A),
  M.id.hom = CategoryTheory.CategoryStruct.id M.X
-- Std.Internal.Parsec.ByteArray
ByteArray.Iterator.next'.congr_simp : ∀ (it it_1 : ByteArray.Iterator) (e_it : it = it_1) (_h : it.hasNext = true), it.next' _h = it_1.next' ⋯
-- Mathlib.Topology.Category.CompHausLike.Basic
/-- The underlying topological space satisfies P.  -/
CompHausLike.prop : ∀ {P : TopCat → Prop} (self : CompHausLike P), P self.toTop
-- Mathlib.NumberTheory.ModularForms.Petersson
UpperHalfPlane.IsZeroAtImInfty.of_exp_decay : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] {f : UpperHalfPlane → E},
  (∃ c > 0, f =O[UpperHalfPlane.atImInfty] fun τ => Real.exp (-c * τ.im)) → UpperHalfPlane.IsZeroAtImInfty f
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
/-- A sufficient condition for injectivity of `NonUnitalSubalgebra.unitization` when the scalars
are a commutative ring. When the scalars are a field, one should use the more natural
`NonUnitalStarSubalgebra.unitization_injective` whose hypothesis is easier to verify.  -/
AlgHomClass.unitization_injective' : ∀ {F : Type u_1} {R : Type u_2} {S : Type u_3} {A : Type u_4} [inst : CommRing R] [inst_1 : Ring A]
  [inst_2 : Algebra R A] [inst_3 : SetLike S A] [hSA : NonUnitalSubringClass S A] [hSRA : SMulMemClass S R A] (s : S),
  (∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s) →
    ∀ [inst_4 : FunLike F (Unitization R ↥s) A] [AlgHomClass F R (Unitization R ↥s) A] (f : F),
      (∀ (x : ↥s), f ↑x = ↑x) → Function.Injective ⇑f
-- Init.Data.Nat.Lcm
Nat.lcm_zero_left : ∀ (m : ℕ), Nat.lcm 0 m = 0
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.trStmts₁.eq_6 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (x : Turing.TM2.Stmt Γ Λ σ),
  (∀ (k : K) (f : σ → Γ k) (q : Turing.TM2.Stmt Γ Λ σ), x = Turing.TM2.Stmt.push k f q → False) →
    (∀ (k : K) (f : σ → Option (Γ k) → σ) (q : Turing.TM2.Stmt Γ Λ σ), x = Turing.TM2.Stmt.peek k f q → False) →
      (∀ (k : K) (f : σ → Option (Γ k) → σ) (q : Turing.TM2.Stmt Γ Λ σ), x = Turing.TM2.Stmt.pop k f q → False) →
        (∀ (a : σ → σ) (q : Turing.TM2.Stmt Γ Λ σ), x = Turing.TM2.Stmt.load a q → False) →
          (∀ (a : σ → Bool) (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ), x = Turing.TM2.Stmt.branch a q₁ q₂ → False) →
            Turing.TM2to1.trStmts₁ x = ∅
-- Mathlib.RingTheory.Valuation.Extension
/-- The valuation `vR` on `R` is equivalent to the comap of the valuation `vA` on `A`  -/
Valuation.HasExtension.val_isEquiv_comap : ∀ {R : Type u_1} {A : Type u_2} {ΓR : Type u_3} {ΓA : Type u_4} {inst : CommRing R} {inst_1 : Ring A}
  {inst_2 : LinearOrderedCommMonoidWithZero ΓR} {inst_3 : LinearOrderedCommMonoidWithZero ΓA} {inst_4 : Algebra R A}
  {vR : Valuation R ΓR} {vA : Valuation A ΓA} [self : vR.HasExtension vA],
  vR.IsEquiv (Valuation.comap (algebraMap R A) vA)
-- Init.Data.Int.DivMod.Lemmas
Int.neg_tmod_self : ∀ (a : ℤ), (-a).tmod a = 0
-- Mathlib.Logic.Relator
Relator.LeftTotal.trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r₁₂ : α → β → Prop} {r₂₃ : β → γ → Prop} {r₁₃ : α → γ → Prop},
  (∀ (a : α) (b : β) (c : γ), r₁₂ a b → r₂₃ b c → r₁₃ a c) →
    Relator.LeftTotal r₁₂ → Relator.LeftTotal r₂₃ → Relator.LeftTotal r₁₃
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trCont.match_1.eq_2 : ∀ (motive : Turing.ToPartrec.Cont → Sort u_1) (c : Turing.ToPartrec.Code) (a : List ℕ) (k : Turing.ToPartrec.Cont)
  (h_1 : Unit → motive Turing.ToPartrec.Cont.halt)
  (h_2 :
    (c : Turing.ToPartrec.Code) →
      (a : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₁ c a k))
  (h_3 : (a : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₂ a k))
  (h_4 : (c : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.comp c k))
  (h_5 : (c : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.fix c k)),
  (match Turing.ToPartrec.Cont.cons₁ c a k with
    | Turing.ToPartrec.Cont.halt => h_1 ()
    | Turing.ToPartrec.Cont.cons₁ c a k => h_2 c a k
    | Turing.ToPartrec.Cont.cons₂ a k => h_3 a k
    | Turing.ToPartrec.Cont.comp c k => h_4 c k
    | Turing.ToPartrec.Cont.fix c k => h_5 c k) =
    h_2 c a k
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote'.go.match_1.congr_eq_1 : ∀ (motive : Lean.Grind.CommRing.Poly → Sort u_1) (p : Lean.Grind.CommRing.Poly)
  (h_1 : Unit → motive (Lean.Grind.CommRing.Poly.num 0)) (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Poly.num k))
  (h_3 :
    (k : ℤ) →
      (m : Lean.Grind.CommRing.Mon) → (p : Lean.Grind.CommRing.Poly) → motive (Lean.Grind.CommRing.Poly.add k m p)),
  p = Lean.Grind.CommRing.Poly.num 0 →
    (match p with
      | Lean.Grind.CommRing.Poly.num 0 => h_1 ()
      | Lean.Grind.CommRing.Poly.num k => h_2 k
      | Lean.Grind.CommRing.Poly.add k m p => h_3 k m p) ≍
      h_1 ()
-- Mathlib.Analysis.Convex.Intrinsic
/-- Naturality of intrinsic interior under a map whose induced map on affine spans is a
homeomorphism. It is introduced here to share the proof of the affine equivalence and affine
isometry versions below.  -/
_private.Mathlib.Analysis.Convex.Intrinsic.0.intrinsicInterior_image_of_homeomorph_affineSpan : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Q : Type u_4} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V]
  [inst_2 : Module 𝕜 V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module 𝕜 W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] {f : P → Q} {s : Set P}
  (e : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))),
  (∀ [inst_9 : Nonempty ↑s], IsHomeomorph e) →
    (∀ [inst_9 : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x) →
      intrinsicInterior 𝕜 (f '' s) = f '' intrinsicInterior 𝕜 s
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.instEmptyCollection : {α : Type u} → {β : α → Type v} → EmptyCollection (Std.DHashMap.Raw α β)