mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.Hom
/-- If a bounded group homomorphism map is constructed from a group homomorphism via the constructor
`AddMonoidHom.mkNormedAddGroupHom`, then its norm is bounded by the bound given to the constructor
if it is nonnegative.  -/
NormedAddGroupHom.mkNormedAddGroupHom_norm_le : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂] (f : V₁ →+ V₂)
  {C : ℝ}, 0 ≤ C → ∀ (h : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖), ‖f.mkNormedAddGroupHom C h‖ ≤ C
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.zero_caratheodory : ∀ {α : Type u_1}, MeasureTheory.OuterMeasure.caratheodory 0 = ⊤
-- Lean.Declaration
Lean.ReducibilityHints.regular.sizeOf_spec : ∀ (a : UInt32), sizeOf (Lean.ReducibilityHints.regular a) = 1 + sizeOf a
-- Mathlib.Data.ENat.Basic
instPreorderENat : Preorder ℕ∞
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
/-- The functor which sends a triangle `X ⟶ Y ⟶ Z ⟶ X⟦1⟧` in `C` to the triangle
`op Z ⟶ op Y ⟶ op X ⟶ (op Z)⟦1⟧` in `Cᵒᵖ` (without introducing signs).  -/
CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      CategoryTheory.Functor (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ (CategoryTheory.Pretriangulated.Triangle Cᵒᵖ)
-- Mathlib.LinearAlgebra.TensorProduct.Basic
/-- **Alias** of `TensorProduct.mapOfCompatibleSMul`.

---

If M and N are both R- and A-modules and their actions on them commute,
and if the A-action on `M ⊗[R] N` can switch between the two factors, then there is a
canonical S-linear map from `M ⊗[A] N` to `M ⊗[R] N`,
where `S` is any other ring acting on `M` and whose action commutes with the `A` and `R`-actions.  -/
TensorProduct.mapOfCompatibleSMul' : (R : Type u_1) →
  [inst : CommSemiring R] →
    (A : Type u_22) →
      (S : Type u_23) →
        (M : Type u_24) →
          (N : Type u_25) →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : AddCommMonoid N] →
                [inst_3 : Module R M] →
                  [inst_4 : Module R N] →
                    [inst_5 : CommSemiring A] →
                      [inst_6 : Module A M] →
                        [inst_7 : Module A N] →
                          [SMulCommClass R A M] →
                            [inst_9 : CommSemiring S] →
                              [inst_10 : Module S M] →
                                [inst_11 : SMulCommClass R S M] →
                                  [inst_12 : SMulCommClass A S M] →
                                    [TensorProduct.CompatibleSMul R A M N] →
                                      TensorProduct A M N →ₗ[S] TensorProduct R M N
-- Init.Data.UInt.Bitwise
UInt16.not_not : ∀ {a : UInt16}, ~~~~~~a = a
-- Mathlib.Computability.StateTransition
StateTransition.tr_reaches : ∀ {σ₁ : Type u_1} {σ₂ : Type u_2} {f₁ : σ₁ → Option σ₁} {f₂ : σ₂ → Option σ₂} {tr : σ₁ → σ₂ → Prop},
  StateTransition.Respects f₁ f₂ tr →
    ∀ {a₁ : σ₁} {a₂ : σ₂},
      tr a₁ a₂ → ∀ {b₁ : σ₁}, StateTransition.Reaches f₁ a₁ b₁ → ∃ b₂, tr b₁ b₂ ∧ StateTransition.Reaches f₂ a₂ b₂
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.toAddMon.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.AddGrp C), A.toAddMon = { X := A.X, addMon := A.addGrp.toAddMonObj }
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
_private.Mathlib.RingTheory.Bialgebra.MonoidAlgebra.0.AddMonoidAlgebra.mapDomainOfBialgHomFun.eq_1 : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : AddGroup G]
  [inst_3 : AddGroup H] (f : AddMonoidAlgebra R G →ₐc[R] AddMonoidAlgebra R H) (g : G),
  AddMonoidAlgebra.mapDomainOfBialgHomFun✝ f g = Exists.choose ⋯
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.forget₂AddMon_obj_addMon : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (R : CategoryTheory.RingObjCat C),
  ((CategoryTheory.RingObjCat.forget₂AddMon C).obj R).addMon = R.ringObj.toAddMonObj
-- Mathlib.Algebra.Group.Nat.Hom
multiplesHom_apply : ∀ {M : Type u_1} [inst : AddMonoid M] (x : M) (n : ℕ), ((multiplesHom M) x) n = n • x
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The predicate `IsFraction` is "prelocal",
in the sense that if it holds on `U` it holds on any open subset `V` of `U`.
 -/
AlgebraicGeometry.StructureSheaf.isFractionPrelocal : (R M : Type u) →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] → TopCat.PrelocalPredicate (AlgebraicGeometry.StructureSheaf.Localizations M)
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.natDegree_linear : ∀ {R : Type u} {a b : R} [inst : Semiring R], a ≠ 0 → (Polynomial.C a * Polynomial.X + Polynomial.C b).natDegree = 1
-- Mathlib.Algebra.Lie.Submodule
/-- A morphism of Lie modules `f : M → M'` pulls back Lie submodules of `M'` to Lie submodules of
`M`.  -/
LieSubmodule.comap : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {M' : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : Module R M] →
                [inst_4 : LieRingModule L M] →
                  [inst_5 : AddCommGroup M'] →
                    [inst_6 : Module R M'] →
                      [inst_7 : LieRingModule L M'] → (M →ₗ⁅R,L⁆ M') → LieSubmodule R L M' → LieSubmodule R L M
-- Mathlib.Data.ZMod.Basic
ZMod.val_eq_zero : ∀ {n : ℕ} (a : ZMod n), a.val = 0 ↔ a = 0
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.fFunctor_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), CategoryTheory.ShortComplex.fFunctor.obj S = CategoryTheory.Arrow.mk S.f
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mem_ker_iff : ∀ {R : Type u_6} {M : Type u_8} {M' : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (S : Submonoid R) {g : M →ₗ[R] M'} [IsLocalizedModule S g] {m : M},
  m ∈ g.ker ↔ ∃ r ∈ S, r • m = 0
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.CoreSmallCategoryOfSet.smallCategoryOfSet_hom : ∀ {Ω : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (h : CategoryTheory.CoreSmallCategoryOfSet Ω C)
  (X Y : ↑h.obj), h.smallCategoryOfSet.hom X Y = h.hom X Y
-- Init.Data.Nat.Lemmas
Nat.add_eq_left : ∀ {a b : ℕ}, a + b = a ↔ b = 0
-- Mathlib.RingTheory.Localization.Integral
isIntegral_localization' : ∀ {R : Type u_5} {S : Type u_6} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  f.IsIntegral → ∀ (M : Submonoid R), (IsLocalization.map (Localization (Submonoid.map (↑f) M)) f ⋯).IsIntegral
-- Mathlib.Topology.Algebra.Group.Basic
tendsto_inv : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Inv G] [ContinuousInv G] (a : G),
  Filter.Tendsto Inv.inv (nhds a) (nhds a⁻¹)
-- Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Subgroup.properlyDiscontinuousSMul_iff_of_isFiniteRelIndex : ∀ {Γ : Type u_1} {α : Type u_2} [inst : Group Γ] [inst_1 : TopologicalSpace α] [inst_2 : MulAction Γ α]
  [ContinuousConstSMul Γ α] {G H : Subgroup Γ},
  G ≤ H → ∀ [G.IsFiniteRelIndex H], ProperlyDiscontinuousSMul (↥G) α ↔ ProperlyDiscontinuousSMul (↥H) α
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.extend_val_inl : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} (P : Algebra.Generators R S ι) (b : ι' → S) (i : ι), (P.extend b).val (Sum.inl i) = P.val i
-- Init.Data.Iterators.Consumers.Monadic.Access
/-- If `it` plausibly skips in its immediate next step, the successor iterator being `it'`, and
if `step` is a plausible `n`-th output step of `it'`, then `step` is also a plausible `n`-th
output step of `it`.
 -/
Std.IterM.IsPlausibleNthOutputStep.skip : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] {n : ℕ} {it it' : Std.IterM m β}
  {step : Std.IterStep (Std.IterM m β) β},
  it.IsPlausibleStep (Std.IterStep.skip it') →
    Std.IterM.IsPlausibleNthOutputStep n it' step → Std.IterM.IsPlausibleNthOutputStep n it step
-- Lean.Parser.Term
Lean.Parser.Term.scientific.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.Interval.Finset.Basic
/-- **Alias** of `Finset.Ico_sdiff_Ico_right`. -/
Finset.Ico_diff_Ico_right : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] (a b c : α),
  Finset.Ico a b \ Finset.Ico c b = Finset.Ico a (min b c)
-- Mathlib.Topology.UniformSpace.Defs
/-- The uniformity filter.  -/
UniformSpace.uniformity : {α : Type u} → [self : UniformSpace α] → Filter (α × α)
-- Mathlib.Computability.Encoding
Computability.Γ'.ket : Computability.Γ'
-- Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
/-- Integral curves are unique on open intervals.

If a $C^1$ vector field `v` admits two integral curves `γ γ' : ℝ → M` on some open interval
`Ioo a b`, and `γ t₀ = γ' t₀` for some `t ∈ Ioo a b`, then `γ` and `γ'` agree on `Ioo a b`.  -/
isMIntegralCurveOn_Ioo_eqOn_of_contMDiff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : IsManifold I 1 M] {γ γ' : ℝ → M} {v : (x : M) → TangentSpace I x} {t₀ : ℝ} [T2Space M] {a b : ℝ},
  t₀ ∈ Set.Ioo a b →
    (∀ t ∈ Set.Ioo a b, I.IsInteriorPoint (γ t)) →
      (ContMDiff I I.tangent 1 fun x => ⟨x, v x⟩) →
        IsMIntegralCurveOn γ v (Set.Ioo a b) →
          IsMIntegralCurveOn γ' v (Set.Ioo a b) → γ t₀ = γ' t₀ → Set.EqOn γ γ' (Set.Ioo a b)
-- Mathlib.Order.ScottContinuity
ScottContinuous.fst : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β], ScottContinuous Prod.fst
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
MonotoneOn.csInf_eq_of_subset_of_forall_exists_le : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : ConditionallyCompleteLattice β] {f : α → β} {s t : Set α},
  BddBelow (f '' t) → MonotoneOn f t → s ⊆ t → (∀ y ∈ t, ∃ x ∈ s, x ≤ y) → sInf (f '' s) = sInf (f '' t)
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.nhds_infty_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X],
  nhds OnePoint.infty = Filter.map OnePoint.some (Filter.coclosedCompact X) ⊔ pure OnePoint.infty
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap_desc_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCoequalizer f g]
  [inst_3 : CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)]
  [inst_4 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G] {X' Y' : D}
  (f' g' : X' ⟶ Y') [inst_5 : CategoryTheory.Limits.HasCoequalizer f' g'] (p : G.obj X ⟶ X') (q : G.obj Y ⟶ Y')
  (wf : CategoryTheory.CategoryStruct.comp (G.map f) q = CategoryTheory.CategoryStruct.comp p f')
  (wg : CategoryTheory.CategoryStruct.comp (G.map g) q = CategoryTheory.CategoryStruct.comp p g') {Z' : D} (h : Y' ⟶ Z')
  (wh : CategoryTheory.CategoryStruct.comp f' h = CategoryTheory.CategoryStruct.comp g' h) {Z : D} (h_1 : Z' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.coequalizer.π f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCoequalizer.iso G f g).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom (G.map f) (G.map g) f' g' p q wf wg))
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.desc h wh) h_1))) =
    CategoryTheory.CategoryStruct.comp q (CategoryTheory.CategoryStruct.comp h h_1)
-- Mathlib.RingTheory.WittVector.IsPoly
WittVector.IsPoly₂.map : ∀ {p : ℕ} {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Fact (Nat.Prime p)]
  {f : ⦃R : Type u⦄ → [CommRing R] → WittVector p R → WittVector p R → WittVector p R},
  WittVector.IsPoly₂ p f →
    ∀ (g : R →+* S) (x y : WittVector p R), (WittVector.map g) (f x y) = f ((WittVector.map g) x) ((WittVector.map g) y)
-- Mathlib.Topology.Algebra.Ring.Basic
IsSemitopologicalRing.toContinuousNeg : ∀ {R : Type u_2} {inst : TopologicalSpace R} {inst_1 : NonUnitalNonAssocRing R} [self : IsSemitopologicalRing R],
  ContinuousNeg R
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isLongestMatchAtChain_iff_isLongestMatchAtChain_beq : ∀ {c : Char} {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAtChain c pos pos' ↔
    String.Slice.Pattern.Model.IsLongestMatchAtChain (fun x => x == c) pos pos'
-- Mathlib.Data.Matrix.Mul
RingEquiv.isStablyFiniteRing_iff : ∀ {R : Type u_10} {S : Type u_11} {F : Type u_12} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : EquivLike F R S] [RingEquivClass F R S] (f : F), IsStablyFiniteRing R ↔ IsStablyFiniteRing S
-- Init.Data.List.Range
List.range'.eq_def : ∀ (x x_1 x_2 : ℕ),
  List.range' x x_1 x_2 =
    match x, x_1, x_2 with
    | x, 0, x_3 => []
    | s, n.succ, step => s :: List.range' (s + step) n step
-- Mathlib.Order.Filter.AtTopBot.Monoid
/-- In an ordered multiplicative monoid, if `f` and `g` tend to `-∞`, then so does `f * g`.

Earlier, this name was used for a similar lemma about rings (with conclusion `f * g → +∞`),
which is now called `Filter.Tendsto.atBot_mul_atBot₀`.  -/
Filter.Tendsto.atBot_mul_atBot : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedMonoid M] {l : Filter α}
  {f g : α → M},
  Filter.Tendsto f l Filter.atBot → Filter.Tendsto g l Filter.atBot → Filter.Tendsto (fun x => f x * g x) l Filter.atBot
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addY_self : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P : Fin 3 → R}, W'.Equation P → W'.addY P P = 0
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.instInhabitedFunIndParamKind : Inhabited Lean.Meta.FunIndParamKind
-- Mathlib.GroupTheory.Perm.Support
/-- If g and c commute, then g stabilizes the support of c  -/
Equiv.Perm.mem_support_iff_of_commute : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g c : Equiv.Perm α},
  Commute g c → ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
-- Init.Data.Fin.Lemmas
Fin.val_subNat : ∀ {n m : ℕ} (i : Fin (n + m)) (h : m ≤ ↑i), ↑(Fin.subNat m i h) = ↑i - m
-- Std.Sync.Mutex
/-- Wakes up all other threads executing `wait`.  -/
Std.Condvar.notifyAll : Std.Condvar → BaseIO Unit
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- A uniformly Cauchy sequence converges uniformly to its limit  -/
UniformCauchySeqOnFilter.tendstoUniformlyOnFilter_of_tendsto : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
  {p' : Filter α},
  UniformCauchySeqOnFilter F p p' →
    (∀ᶠ (x : α) in p', Filter.Tendsto (fun n => F n x) p (nhds (f x))) → TendstoUniformlyOnFilter F f p p'
-- Mathlib.Topology.Constructions.SumProd
IsOpen.prod : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {t : Set Y},
  IsOpen s → IsOpen t → IsOpen (s ×ˢ t)
-- Mathlib.Data.Sym.Sym2
Sym2.mul.eq_1 : ∀ {M : Type u_4} [inst : CommMagma M], Sym2.mul = Sym2.lift ⟨fun x1 x2 => x1 * x2, ⋯⟩
-- Mathlib.Algebra.BigOperators.Pi
prod_indicator_apply : ∀ {ι : Type u_1} {κ : Type u_2} {R : Type u_5} [inst : CommSemiring R] (s : Finset ι) (f : ι → Set κ) (g : ι → κ → R)
  (j : κ), ∏ i ∈ s, (f i).indicator (g i) j = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i) j
-- Mathlib.Order.WellFounded
Function.isMinimalFor_argminOn : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) [inst : LinearOrder β] [inst_1 : WellFoundedLT β] (s : Set α)
  (hs : s.Nonempty), MinimalFor (fun x => x ∈ s) f (Function.argminOn f s hs)
-- Mathlib.Data.Nat.Pairing
/-- An equivalence between `ℕ × ℕ` and `ℕ`.  -/
Nat.pairEquiv : ℕ × ℕ ≃ ℕ
-- Batteries.Tactic.GeneralizeProofs
/-- Runs `x` with an additional local variable.  -/
Batteries.Tactic.GeneralizeProofs.MAbs.withLocal : {α : Type} → Lean.Expr → Batteries.Tactic.GeneralizeProofs.MAbs α → Batteries.Tactic.GeneralizeProofs.MAbs α
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.union_vadd_inter_subset_union : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s₁ s₂ : Finset α} {t₁ t₂ : Finset β}
  [inst_2 : DecidableEq α], (s₁ ∪ s₂) +ᵥ t₁ ∩ t₂ ⊆ (s₁ +ᵥ t₁) ∪ (s₂ +ᵥ t₂)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.singleton_self : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X), CategoryTheory.Presieve.singleton f f
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.neg_f_apply : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : C ⟶ D) (i : ι), (-f).f i = -f.f i
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.IsEdgeReachable.trans : ∀ {V : Type u_1} {G : SimpleGraph V} {k : ℕ} {u v w : V},
  G.IsEdgeReachable k u v → G.IsEdgeReachable k v w → G.IsEdgeReachable k u w
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mod_eq_zero_of_dvd : ∀ {a b : Ordinal.{u_4}}, b ∣ a → a % b = 0
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.changeFunctor_counitIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {G : CategoryTheory.Functor C D} (iso : e.functor ≅ G) (X : D),
  (e.changeFunctor iso).counitIso.hom.app X =
    CategoryTheory.CategoryStruct.comp (iso.inv.app (e.inverse.obj X)) (e.counitIso.hom.app X)
-- Mathlib.Topology.TietzeExtension
/-- **Tietze extension theorem** for `TietzeExtension` spaces. Let `e` be a closed embedding of a
nonempty topological space `X₁` into a normal topological space `X`. Let `f` be a continuous
function on `X₁` with values in a `TietzeExtension` space `Y`. Then there exists a
continuous function `g : C(X, Y)` such that `g ∘ e = f`.  -/
ContinuousMap.exists_extension : ∀ {X₁ : Type u₁} [inst : TopologicalSpace X₁] {X : Type u} [inst_1 : TopologicalSpace X] [NormalSpace X] {e : X₁ → X}
  {Y : Type v} [inst_3 : TopologicalSpace Y] [TietzeExtension Y] (he : Topology.IsClosedEmbedding e) (f : C(X₁, Y)),
  ∃ g, g.comp { toFun := e, continuous_toFun := ⋯ } = f
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.continuousOn_rpowIntegrand₁₂_uncurry : ∀ {p : ℝ}, p ∈ Set.Ioi 1 → ∀ s ⊆ Set.Ici 0, ContinuousOn (Function.uncurry p.rpowIntegrand₁₂) (Set.Ioi 0 ×ˢ s)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.coeFiniteAt : {V : Type u} →
  {G : SimpleGraph V} →
    {G' : G.Subgraph} → (v : ↑G'.verts) → [Fintype ↑(G'.neighborSet ↑v)] → Fintype ↑(G'.coe.neighborSet v)
-- Mathlib.Logic.Equiv.Set
Equiv.self_comp_ofInjective_symm : ∀ {α : Sort u_3} {β : Type u_4} {f : α → β} (hf : Function.Injective f),
  f ∘ ⇑(Equiv.ofInjective f hf).symm = Subtype.val
-- Mathlib.Algebra.Homology.ExactSequenceFour
/-- If `S` is an exact sequence, this is the isomorphism from a cokernel
of `S.map' k (k + 1)` to a kernel of `S.map' (k + 2) (k + 3)`.  -/
CategoryTheory.ComposableArrows.Exact.cokerIsoKer' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Balanced C] →
        {n : ℕ} →
          {S : CategoryTheory.ComposableArrows C (n + 3)} →
            S.Exact →
              (k : ℕ) →
                (hk : k ≤ n) →
                  (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯)) →
                    (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) →
                      CategoryTheory.Limits.IsColimit cc → CategoryTheory.Limits.IsLimit kf → (cc.pt ≅ kf.pt)
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.superpolynomialDecay_param_pow_mul_iff : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k : α → β} (f : α → β) [inst : TopologicalSpace β] [inst_1 : Field β]
  [inst_2 : LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β],
  Filter.Tendsto k l Filter.atTop →
    ∀ (n : ℕ), Asymptotics.SuperpolynomialDecay l k (k ^ n * f) ↔ Asymptotics.SuperpolynomialDecay l k f
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.le_comap_map : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F}, S ≤ AddSubmonoid.comap f (AddSubmonoid.map f S)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
/-- If `C` is a locally `w`-small abelian category with enough projectives,
then `HasExt.{w} C` holds. We do not make this an instance though:
for a given category `C`, there may be different reasonable choices for
the universe `w`, and if we have two `HasExt.{w₁} C` and `HasExt.{w₂} C`
instances, we would have to specify the universe explicitly almost
everywhere, which would be an inconvenience. Then, we must be
very selective regarding `HasExt` instances.  -/
CategoryTheory.hasExt_of_enoughProjectives : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.EnoughProjectives C], CategoryTheory.HasExt C
-- Mathlib.Tactic.ClickSuggestions
/-- The component called by the `#click_suggestions` command.  -/
Mathlib.Tactic.ClickSuggestions.clickSuggestionsComponent : ProofWidgets.Component ProofWidgets.PanelWidgetProps
-- Mathlib.Algebra.Homology.ImageToKernel
/-- While `imageToKernel f g w` provides a morphism
`imageSubobject f ⟶ kernelSubobject g`
in terms of the subobject API,
this variant provides a morphism
`image f ⟶ kernel g`,
which is sometimes more convenient.
 -/
imageToKernel' : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      {A B C : V} →
        (f : A ⟶ B) →
          (g : B ⟶ C) →
            [inst_2 : CategoryTheory.Limits.HasKernels V] →
              [inst_3 : CategoryTheory.Limits.HasImages V] →
                CategoryTheory.CategoryStruct.comp f g = 0 →
                  (CategoryTheory.Limits.image f ⟶ CategoryTheory.Limits.kernel g)
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.hasNatPow : (p n : ℕ) → (R : Type u_1) → [CommRing R] → [Fact (Nat.Prime p)] → Pow (TruncatedWittVector p n R) ℕ
-- Mathlib.Computability.Encoding
Computability.instDecidableEqΓ'.decEq : (x x_1 : Computability.Γ') → Decidable (x = x_1)
-- Mathlib.Algebra.Star.StarRingHom
/-- Promote a bijective star ring homomorphism to a star ring equivalence.  -/
StarRingEquiv.ofBijective : {F : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : NonUnitalNonAssocSemiring A] →
        [inst_1 : Star A] →
          [inst_2 : NonUnitalNonAssocSemiring B] →
            [inst_3 : Star B] →
              [inst_4 : FunLike F A B] →
                [inst_5 : NonUnitalRingHomClass F A B] →
                  [NonUnitalStarRingHomClass F A B] → (f : F) → Function.Bijective ⇑f → A ≃⋆+* B
-- Mathlib.Control.LawfulFix
Pi.hasFix : {α : Type u_1} →
  {β : α → Type u_2} →
    {γ : (a : α) → β a → Type u_3} → [Fix ((x : Sigma β) → γ x.fst x.snd)] → Fix ((x : α) → (y : β x) → γ x y)
-- Mathlib.RingTheory.Localization.NumDen
IsFractionRing.mk'_num_den' : ∀ (A : Type u_1) [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] (x : K),
  (algebraMap A K) (IsFractionRing.num A x) / (algebraMap A K) ↑(IsFractionRing.den A x) = x