mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.posPart_eq_zero_iff : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A] [StarOrderedRing A]
  [NonnegSpectrumClass ℝ A] (a : A), autoParam (IsSelfAdjoint a) CFC.posPart_eq_zero_iff._auto_1 → (a⁺ = 0 ↔ a ≤ 0)
-- Mathlib.Algebra.Group.End
/-- Lift a monoid homomorphism `f : G →* Function.End α` to a monoid homomorphism
`f : G →* Equiv.Perm α`.  -/
MonoidHom.toHomPerm : {α : Type u_4} → {G : Type u_7} → [inst : Group G] → (G →* Function.End α) → G →* Equiv.Perm α
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.toList.eq_1 : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (p : Equiv.Perm α) (x : α),
  p.toList x = List.iterate (⇑p) x (p.cycleOf x).support.card
-- Mathlib.Probability.Process.LocalProperty
_private.Mathlib.Probability.Process.LocalProperty.0.ProbabilityTheory.mkStrictMonoAux.eq_def : ∀ (x : ℕ → ℕ) (x_1 : ℕ),
  ProbabilityTheory.mkStrictMonoAux✝ x x_1 =
    match x_1 with
    | 0 => x 0
    | n.succ => max (x (n + 1)) (ProbabilityTheory.mkStrictMonoAux✝ x n) + 1
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.instIsIsoAppUnitLanAdjunctionOfHasPointwiseLeftKanExtension : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] [L.Full] [L.Faithful] (F : CategoryTheory.Functor C H)
  [L.HasPointwiseLeftKanExtension F] [inst_6 : ∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F],
  CategoryTheory.IsIso ((L.lanAdjunction H).unit.app F)
-- Std.Http.Data.URI.Basic
/-- Returns a new URI with the path replaced.
 -/
Std.Http.URI.withPath : Std.Http.URI → Std.Http.URI.Path → Std.Http.URI
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.node.inj : ∀ {α : Type u} {size : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} {size_1 : ℕ} {l_1 : Ordnode α} {x_1 : α}
  {r_1 : Ordnode α},
  Ordnode.node size l x r = Ordnode.node size_1 l_1 x_1 r_1 → size = size_1 ∧ l = l_1 ∧ x = x_1 ∧ r = r_1
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_sub_comm : ∀ {α : Type u_1} {E : Type u_4} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] (f g : α → E) (p : ENNReal)
  (μ : MeasureTheory.Measure α), MeasureTheory.eLpNorm (f - g) p μ = MeasureTheory.eLpNorm (g - f) p μ
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.spanIntRootSupport : ∀ {ι : 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} (b : P.Base),
  Submodule.span ℤ (P.rootSpanMem ℤ '' ↑b.support) = ⊤
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_iff_isZero_rightHomology : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology], S.Exact ↔ CategoryTheory.Limits.IsZero S.rightHomology
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.totalAux.ιMapObj_D₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁₂ i₁₂' : I₁₂) (i : I₁ × I₂) (h : c₁.π c₂ c₁₂ i = i₁₂),
  CategoryTheory.CategoryStruct.comp (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ h) (K.D₂ c₁₂ i₁₂ i₁₂') =
    K.d₂ c₁₂ i.1 i.2 i₁₂'
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.ofFun_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β] (f : α → β)
  (hf : autoParam (OmegaCompletePartialOrder.ωScottContinuous f) OmegaCompletePartialOrder.ContinuousHom.ofFun._auto_1)
  (a : α), (OmegaCompletePartialOrder.ContinuousHom.ofFun f hf) a = f a
-- Mathlib.Algebra.Group.Units.Hom
/-- If two homomorphisms from a division monoid to a monoid are equal at a unit `x`, then they are
equal at `x⁻¹`.  -/
IsUnit.eq_on_inv : ∀ {F : Type u_1} {G : Type u_2} {N : Type u_3} [inst : DivisionMonoid G] [inst_1 : Monoid N] [inst_2 : FunLike F G N]
  [MonoidHomClass F G N] {x : G}, IsUnit x → ∀ (f g : F), f x = g x → f x⁻¹ = g x⁻¹
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.ι_D₁_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁₂ i₁₂' : I₁₂) (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂) {Z : C}
  (h_1 : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ h)
      (CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') h_1) =
    CategoryTheory.CategoryStruct.comp (K.d₁ c₁₂ i₁ i₂ i₁₂') h_1
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckStep.U.sizeOf_spec : sizeOf DyckStep.U = 1
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_inter_Ico : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] {a b c d : α},
  Finset.Ico a b ∩ Finset.Ico c d = Finset.Ico (max a c) (min b d)
-- Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
CategoryTheory.TwoSquare.GuitartExact.hComp_iff_of_equivalences : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃]
  {V₁ : CategoryTheory.Functor C₁ D₁} {T₁ : CategoryTheory.Functor C₁ C₂} {B₁ : CategoryTheory.Functor D₁ D₂}
  {V₂ : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare T₁ V₁ V₂ B₁) {V₃ : CategoryTheory.Functor C₃ D₃}
  (eT : C₂ ≌ C₃) (eB : D₂ ≌ D₃) (w' : eT.functor.comp V₃ ≅ V₂.comp eB.functor),
  (w.hComp w'.hom).GuitartExact ↔ w.GuitartExact
-- Mathlib.CategoryTheory.Monoidal.Hopf_
CategoryTheory.HopfObj.mul_antipode : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : C) [inst_3 : CategoryTheory.HopfObj A],
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul CategoryTheory.HopfObj.antipode =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.HopfObj.antipode CategoryTheory.HopfObj.antipode)
      (CategoryTheory.CategoryStruct.comp (β_ A A).hom CategoryTheory.MonObj.mul)
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
_private.Mathlib.CategoryTheory.Monoidal.Free.Coherence.0.CategoryTheory.FreeMonoidalCategory.normalizeMapAux.match_3.splitter : {C : Type u_1} →
  (motive : (x x_1 : CategoryTheory.FreeMonoidalCategory C) → x.Hom x_1 → Sort u_2) →
    (x x_1 : CategoryTheory.FreeMonoidalCategory C) →
      (x_2 : x.Hom x_1) →
        ((x : CategoryTheory.FreeMonoidalCategory C) → motive x x (CategoryTheory.FreeMonoidalCategory.Hom.id x)) →
          ((X Y Z : CategoryTheory.FreeMonoidalCategory C) →
              motive ((X.tensor Y).tensor Z) (X.tensor (Y.tensor Z))
                (CategoryTheory.FreeMonoidalCategory.Hom.α_hom X Y Z)) →
            ((X Y Z : CategoryTheory.FreeMonoidalCategory C) →
                motive (X.tensor (Y.tensor Z)) ((X.tensor Y).tensor Z)
                  (CategoryTheory.FreeMonoidalCategory.Hom.α_inv X Y Z)) →
              ((a : CategoryTheory.FreeMonoidalCategory C) →
                  motive (CategoryTheory.FreeMonoidalCategory.unit.tensor a) a
                    (CategoryTheory.FreeMonoidalCategory.Hom.l_hom a)) →
                ((a : CategoryTheory.FreeMonoidalCategory C) →
                    motive a (CategoryTheory.FreeMonoidalCategory.unit.tensor a)
                      (CategoryTheory.FreeMonoidalCategory.Hom.l_inv a)) →
                  ((a : CategoryTheory.FreeMonoidalCategory C) →
                      motive (a.tensor CategoryTheory.FreeMonoidalCategory.unit) a
                        (CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom a)) →
                    ((a : CategoryTheory.FreeMonoidalCategory C) →
                        motive a (a.tensor CategoryTheory.FreeMonoidalCategory.unit)
                          (CategoryTheory.FreeMonoidalCategory.Hom.ρ_inv a)) →
                      ((x x_3 Y : CategoryTheory.FreeMonoidalCategory C) →
                          (f : x.Hom Y) → (g : Y.Hom x_3) → motive x x_3 (f.comp g)) →
                        ((T X Y W : CategoryTheory.FreeMonoidalCategory C) →
                            (f : T.Hom Y) → (g : X.Hom W) → motive (T.tensor X) (Y.tensor W) (f.tensor g)) →
                          ((T Y₁ W : CategoryTheory.FreeMonoidalCategory C) →
                              (f : Y₁.Hom W) →
                                motive (T.tensor Y₁) (T.tensor W)
                                  (CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft T f)) →
                            ((T X₂ : CategoryTheory.FreeMonoidalCategory C) →
                                (f : T.Hom X₂) →
                                  (W : CategoryTheory.FreeMonoidalCategory C) →
                                    motive (T.tensor W) (X₂.tensor W) (f.whiskerRight W)) →
                              motive x x_1 x_2
-- Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
AddSubgroup.index_eq_natAbs_det : ∀ {E : Type u_1} [inst : AddCommGroup E] {ι : Type u_2} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι]
  (bE : Module.Basis ι ℤ E) (N : AddSubgroup E) (bN : Module.Basis ι ℤ ↥N), N.index = (bE.det fun x => ↑(bN x)).natAbs
-- Mathlib.Topology.Semicontinuity.Defs
HasOpenCGraph.hasOpenLowerSections : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β},
  HasOpenCGraph f → HasOpenLowerSections f
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.of.d.eq_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  {α : Type u_2} [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α] [inst_4 : DecidableEq α] (X : α → V)
  (d : (n : α) → X (n + 1) ⟶ X n) (i j : α),
  ChainComplex.of.d X d i j =
    if h : i = j + 1 then CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (d j) else 0
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.grind_filter_ : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.NonIntegrable
/-- If `f` is eventually differentiable along a nontrivial filter `l : Filter ℝ` that is generated
by convex sets, the norm of `f` tends to infinity along `l`, and `f' = O(g)` along `l`, where `f'`
is the derivative of `f`, then `g` is not integrable on any interval `a..b` such that
`[a, b] ∈ l`.  -/
not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_filter : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  {f : ℝ → E} {g : ℝ → F} {a b : ℝ} (l : Filter ℝ) [l.NeBot] [Filter.TendstoIxxClass Set.Icc l l],
  Set.uIcc a b ∈ l →
    (∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x) →
      Filter.Tendsto (fun x => ‖f x‖) l Filter.atTop → deriv f =O[l] g → ¬IntervalIntegrable g MeasureTheory.volume a b
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw₀.get?.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α]
  (m m_1 : Std.DHashMap.Internal.Raw₀ α β), m = m_1 → ∀ (a : α), m.get? a = m_1.get? a
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.linearIndependent_powers_iff_aeval : ∀ {R : Type u} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : M →ₗ[R] M) (v : M),
  (LinearIndependent R fun n => (f ^ n) v) ↔ ∀ (p : Polynomial R), ((Polynomial.aeval f) p) v = 0 → p = 0
-- Mathlib.Util.Export
Lean.Export.instCoeNameEntry : Coe Lean.Name Lean.Export.Entry
-- Mathlib.Tactic.Translate.TagUnfoldBoundary
_private.Mathlib.Tactic.Translate.TagUnfoldBoundary.0.Mathlib.Tactic.Translate.elabInsertCastAux.unfoldLHS? : Mathlib.Tactic.Translate.CastKind✝ → Lean.Expr → OptionT Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Algebra.Order.Star.Basic
star_right_conjugate_lt_conjugate : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {a b : R}, a < b → ∀ {c : R}, IsRegular c → c * a * star c < c * b * star c
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
multipliable_pnat_iff_multipliable_succ : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {f : ℕ → M},
  (Multipliable fun x => f ↑x) ↔ Multipliable fun x => f (x + 1)
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Modification.mk.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G} {app : (a : B) → η.app a ⟶ θ.app a}
  {naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b))
            (θ.naturality f).hom =
          CategoryTheory.CategoryStruct.comp (η.naturality f).hom
            (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f)))
      CategoryTheory.Pseudofunctor.StrongTrans.Modification.naturality._autoParam}
  {app_1 : (a : B) → η.app a ⟶ θ.app a}
  {naturality_1 :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app_1 b))
            (θ.naturality f).hom =
          CategoryTheory.CategoryStruct.comp (η.naturality f).hom
            (CategoryTheory.Bicategory.whiskerRight (app_1 a) (G.map f)))
      CategoryTheory.Pseudofunctor.StrongTrans.Modification.naturality._autoParam},
  { app := app, naturality := naturality } = { app := app_1, naturality := naturality_1 } → app = app_1
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.Def.onAdded : {γ : Type} → Lean.KeyedDeclsAttribute.Def γ → Bool → Lean.Name → Lean.KeyedDeclsAttribute.Key → Lean.AttrM Unit
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.isSome_succMany?_of_lt_length_toList : ∀ {α : Type u} {r : Std.Ric α} [inst : Std.PRange.Least? α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxc.IsAlwaysFinite α] {i : ℕ},
  i < r.toList.length → (Std.PRange.succMany? i Std.PRange.UpwardEnumerable.least).isSome = true
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_inf_sub_inf_le_abs : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α] [AddLeftMono α] (a b c : α), |a ⊓ c - b ⊓ c| ≤ |a - b|
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.hadamard_add : ∀ {α : Type u_1} {m : Type u_2} {n : Type u_3} (A B C : Matrix m n α) [inst : Distrib α],
  A.hadamard (B + C) = A.hadamard B + A.hadamard C
-- Init.MetaTypes
Lean.NameGenerator.mk.sizeOf_spec : ∀ (namePrefix : Lean.Name) (idx : ℕ),
  sizeOf { namePrefix := namePrefix, idx := idx } = 1 + sizeOf namePrefix + sizeOf idx
-- Mathlib.Data.Finsupp.Indicator
Finsupp.indicator_apply : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] (s : Finset ι) (f : (i : ι) → i ∈ s → α) (i : ι)
  [inst_1 : DecidableEq ι], (Finsupp.indicator s f) i = if hi : i ∈ s then f i hi else 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_diff_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} [inst_1 : Inhabited (β k)],
      Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.diff m₂ ⋯).get! k = default
-- Mathlib.Order.Filter.NAry
Filter.map₂_left : ∀ {α : Type u_1} {β : Type u_3} {f : Filter α} {g : Filter β} [g.NeBot], Filter.map₂ (fun x x_1 => x) f g = f
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.instFintypePointsWithCircumcenterIndex : {n : ℕ} → Fintype (Affine.Simplex.PointsWithCircumcenterIndex n)
-- Mathlib.Analysis.Calculus.Gradient.Basic
hasGradientWithinAt_congr_set : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F} {s t : Set F},
  s =ᶠ[nhds x] t → (HasGradientWithinAt f f' s x ↔ HasGradientWithinAt f f' t x)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- Given an exact short complex `S` and a limit kernel fork `kf` for `S.g`, this is the
left homology data for `S` with `K := kf.pt` and `H := 0`.  -/
CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S : CategoryTheory.ShortComplex C} →
        S.Exact →
          [CategoryTheory.Limits.HasZeroObject C] →
            (kf : CategoryTheory.Limits.KernelFork S.g) → CategoryTheory.Limits.IsLimit kf → S.LeftHomologyData
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- An n-ary version of `Set.mul_mem_mul`.  -/
Set.multiset_prod_mem_multiset_prod : ∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] (t : Multiset ι) (f : ι → Set α) (g : ι → α),
  (∀ i ∈ t, g i ∈ f i) → (Multiset.map g t).prod ∈ (Multiset.map f t).prod
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
HasSum.mul : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [inst : TopologicalSpace α] [T3Space α]
  [inst_2 : NonUnitalNonAssocSemiring α] [IsTopologicalSemiring α] {f : ι → α} {g : κ → α} {s t : α},
  HasSum f s → HasSum g t → (Summable fun x => f x.1 * g x.2) → HasSum (fun x => f x.1 * g x.2) (s * t)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
OpensMeasurableSpace.separatesPoints : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α] [T0Space α],
  MeasurableSpace.SeparatesPoints α
-- Init.System.ST
ST.Ref.mk.inj : ∀ {σ α : Type} {ref : ST.RefPointed.type} {h : Nonempty α} {ref_1 : ST.RefPointed.type} {h_1 : Nonempty α},
  { ref := ref, h := h } = { ref := ref_1, h := h_1 } → ref = ref_1
-- Mathlib.CategoryTheory.Triangulated.Adjunction
CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedFunctorSymmOfInverse : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.Limits.HasZeroObject D] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : CategoryTheory.Preadditive D] [inst_6 : CategoryTheory.HasShift C ℤ] [inst_7 : CategoryTheory.HasShift D ℤ]
  [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_10 : CategoryTheory.Pretriangulated C]
  [inst_11 : CategoryTheory.Pretriangulated D] (E : C ≌ D) [inst_12 : E.inverse.CommShift ℤ]
  [h : E.inverse.IsTriangulated], E.symm.functor.IsTriangulated
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.ofπ.eq_1 : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (π : (relations.G →₀ A) →ₗ[A] M) (hπ : ∀ (r : relations.R), π (relations.relation r) = 0),
  Module.Relations.Solution.ofπ π hπ = { var := fun g => π fun₀ | g => 1, linearCombination_var_relation := ⋯ }
-- Mathlib.Data.Multiset.Basic
Multiset.empty_toList : ∀ {α : Type u_1} {s : Multiset α}, s.toList.isEmpty = true ↔ s = 0
-- Init.Data.List.Attach
/-- Unsafe implementation of `attachWith` that takes advantage of the fact that the representation of
`List {x // P x}` is the same as the input `List α`.
 -/
_private.Init.Data.List.Attach.0.List.attachWithImpl : {α : Type u_1} → (l : List α) → (P : α → Prop) → (∀ x ∈ l, P x) → List { x // P x }
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.union_zeroLocus : ∀ {R : Type u} [inst : CommSemiring R] (s s' : Set R),
  PrimeSpectrum.zeroLocus s ∪ PrimeSpectrum.zeroLocus s' = PrimeSpectrum.zeroLocus ↑(Ideal.span s ⊓ Ideal.span s')
-- Mathlib.Algebra.Order.Quantale
sSup_add_distrib : ∀ {α : Type u_1} {x : α} {s : Set α} [inst : AddSemigroup α] [inst_1 : CompleteLattice α] [IsAddQuantale α],
  sSup s + x = ⨆ y ∈ s, y + x
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X : C}
  {h₁ h₂ : CategoryTheory.MonObj X}, h₁ = h₂ ↔ CategoryTheory.MonObj.mul = CategoryTheory.MonObj.mul
-- Mathlib.Data.Real.ConjExponents
/-- The conjugate exponent of `p` is `q = p/(p-1)`, so that `p⁻¹ + q⁻¹ = 1`.  -/
NNReal.conjExponent : NNReal → NNReal
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.instLocallyCompactSpaceCoeCofiniteOfAddSubgroupClassOfIsTopologicalAddGroupOfCompactSpaceSubtypeMem : ∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  [inst_1 : (i : ι) → TopologicalSpace (R i)] [hBopen : Fact (∀ (i : ι), IsOpen ↑(B i))]
  [inst_2 : (i : ι) → AddGroup (R i)] [∀ (i : ι), AddSubgroupClass (S i) (R i)] [∀ (i : ι), IsTopologicalAddGroup (R i)]
  [hAcompact : ∀ (i : ι), CompactSpace ↥(B i)],
  LocallyCompactSpace (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) Filter.cofinite)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addX.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) (P Q : Fin 3 → R),
  W'.addX P Q =
    P 0 * Q 0 ^ 2 * P 2 ^ 2 - 2 * P 1 * Q 1 * P 2 * Q 2 + P 0 ^ 2 * Q 0 * Q 2 ^ 2 - W'.a₁ * P 0 * Q 1 * P 2 ^ 2 * Q 2 -
                  W'.a₁ * P 1 * Q 0 * P 2 * Q 2 ^ 2 +
                2 * W'.a₂ * P 0 * Q 0 * P 2 ^ 2 * Q 2 ^ 2 -
              W'.a₃ * Q 1 * P 2 ^ 4 * Q 2 -
            W'.a₃ * P 1 * P 2 * Q 2 ^ 4 +
          W'.a₄ * Q 0 * P 2 ^ 4 * Q 2 ^ 2 +
        W'.a₄ * P 0 * P 2 ^ 2 * Q 2 ^ 4 +
      2 * W'.a₆ * P 2 ^ 4 * Q 2 ^ 4
-- Mathlib.Analysis.Normed.Group.Pointwise
ball_add_singleton : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x y : E), Metric.ball x δ + {y} = Metric.ball (x + y) δ
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_ball : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : PseudoMetricSpace α] [OpensMeasurableSpace α] {x : α} {r : ι → ℝ},
  Filter.Tendsto r l Filter.atTop → MeasureTheory.AECover μ l fun i => Metric.ball x (r i)
-- Init.Data.Float.Model.Float32
/-- Returns `true` if the float is positive or negative infinity.
 -/
Float32.Model.isInf : Float32.Model → Bool
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_diff_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} [inst_1 : Inhabited (β k)],
      Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.diff m₂ ⋯).get! k = m₁.get! k
-- Mathlib.NumberTheory.ADEInequality
ADEInequality.A'.eq_1 : ∀ (q r : ℕ+), ADEInequality.A' q r = {1, q, r}