mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Defs
isLeftCancelMul_iff : ∀ (G : Type u) [inst : Mul G], IsLeftCancelMul G ↔ ∀ (a : G), IsLeftRegular a
-- Mathlib.Algebra.CubicDiscriminant
Cubic.of_d_eq_zero' : ∀ {R : Type u_1} [inst : Semiring R], { a := 0, b := 0, c := 0, d := 0 }.toPoly = 0
-- Mathlib.Order.Interval.Multiset
Multiset.Ico_filter_lt_of_right_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b c : α}
  [inst_2 : DecidablePred fun x => x < c],
  b ≤ c → Multiset.filter (fun x => x < c) (Multiset.Ico a b) = Multiset.Ico a b
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List (α × β)} {k fallback : α},
      (List.map Prod.fst l).contains k = false →
        (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).getKeyD k fallback = m.getKeyD k fallback
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
/-- The simplicial set that encodes a single isomorphism.
Its n-simplices are formal compositions of arrows in WalkingIso.  -/
SSet.coherentIso : SSet
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.reindex_tprod : ∀ {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7}
  [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] (e : ι ≃ ι₂) (f : (i : ι) → s i),
  (PiTensorProduct.reindex R s e) ((PiTensorProduct.tprod R) f) = (PiTensorProduct.tprod R) fun i => f (e.symm i)
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
/-- Any open cover is quasi-compact.  -/
AlgebraicGeometry.QuasiCompactCover.inst : ∀ {S : AlgebraicGeometry.Scheme} (𝒰 : S.OpenCover), AlgebraicGeometry.QuasiCompactCover 𝒰.toPreZeroHypercover
-- Aesop.Stats.Basic
Aesop.ScriptGenerated.Method.dynamic.sizeOf_spec : sizeOf Aesop.ScriptGenerated.Method.dynamic = 1
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioo.instCommSemigroup : {R : Type u_2} →
  [inst : CommSemiring R] → [inst_1 : PartialOrder R] → [IsStrictOrderedRing R] → CommSemigroup ↑(Set.Ioo 0 1)
-- Lean.Meta.Basic
Lean.Meta.instReprConfig_2.repr : Lean.Meta.Config → ℕ → Std.Format
-- Mathlib.Algebra.Notation.Lemmas
dite_pos : ∀ {α : Type u_1} [inst : Zero α] {p : Prop} [inst_1 : Decidable p] {a : p → α} {b : ¬p → α} [inst_2 : LT α],
  (∀ (h : p), 0 < a h) → (∀ (h : ¬p), 0 < b h) → 0 < dite p a b
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
interior_extChartAt_target_nonempty : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (I : ModelWithCorners 𝕜 E H) [inst_5 : ChartedSpace H M] (x : M), (interior (extChartAt I x).target).Nonempty
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- A morphism constructed with `nullHomotopic` is homotopic to zero.  -/
CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (S₁ S₂ : CategoryTheory.ShortComplex C) →
        (h₀ : S₁.X₁ ⟶ S₂.X₁) →
          (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) →
            (h₁ : S₁.X₂ ⟶ S₂.X₁) →
              (h₂ : S₁.X₃ ⟶ S₂.X₂) →
                (h₃ : S₁.X₃ ⟶ S₂.X₃) →
                  (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) →
                    CategoryTheory.ShortComplex.Homotopy (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) 0
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.coe_topEquiv : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M],
  ⇑FirstOrder.Language.Substructure.topEquiv = Subtype.val
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- The homology `S.homology` of a short complex is
the kernel of the morphism `S.fromOpcycles : S.opcycles ⟶ S.X₃`.  -/
CategoryTheory.ShortComplex.homologyIsKernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        [inst_2 : S.HasHomology] → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.homologyι ⋯)
-- Std.Time.Format.Modifier
Std.Time.instInhabitedOffsetZ.default : Std.Time.OffsetZ
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.inverse_id : ∀ {R : Type u_1} {M : Type u_2} [inst : TopologicalSpace M] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M], (ContinuousLinearMap.id R M).inverse = ContinuousLinearMap.id R M
-- Mathlib.Topology.UniformSpace.Dini
/-- **Dini's theorem**: if `F n` is a monotone increasing collection of continuous functions on a
set `s` converging pointwise to a continuous function `f`, then `F n` converges locally uniformly
to `f`.  -/
Monotone.tendstoLocallyUniformlyOn_of_forall_tendsto : ∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
  [inst_2 : NormedAddCommGroup G] [inst_3 : Lattice G] [HasSolidNorm G] [IsOrderedAddMonoid G] {F : ι → α → G}
  {f : α → G} {s : Set α},
  (∀ (i : ι), ContinuousOn (F i) s) →
    (∀ x ∈ s, Monotone fun x_1 => F x_1 x) →
      ContinuousOn f s →
        (∀ x ∈ s, Filter.Tendsto (fun x_1 => F x_1 x) Filter.atTop (nhds (f x))) →
          TendstoLocallyUniformlyOn F f Filter.atTop s
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- The rank of a finite module is finite.  -/
Module.rank_lt_aleph0 : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Finite R M], Module.rank R M < Cardinal.aleph0
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.List.mapA.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- If `K` is a field complete with respect to a nontrivial nonarchimedean multiplicative norm and
`L/K` is an algebraic extension, then any multiplicative ring norm on `L` extending the norm on
`K` coincides with the spectral norm.  -/
spectralNorm_unique_field_norm_ext : ∀ {K : Type u} [inst : NontriviallyNormedField K] {L : Type v} [inst_1 : Field L] [inst_2 : Algebra K L]
  [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] {f : AbsoluteValue L ℝ},
  (∀ (x : K), f ((algebraMap K L) x) = ‖x‖) → ∀ (x : L), f x = spectralNorm K L x
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coe_copy : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (p : FractionalIdeal S P) (s : Set P) (hs : s = ↑p), ↑(p.copy s hs) = s
-- Std.Time.DateTime
/-- Getter for the `Millisecond` inside of a `DateTime`.
 -/
Std.Time.DateTime.millisecond : Std.Time.DateTime → Std.Time.Millisecond.Ordinal
-- Mathlib.Order.Circular
/-- `a` is between `a` and `a`.  -/
CircularPreorder.btw_refl : ∀ {α : Type u_1} [self : CircularPreorder α] (a : α), btw a a a
-- Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
/-- If `s` has the unique differential property, `f` is differentiable on `s` and its derivative
at every point of `s` has dense range, then `f '' s` has the unique differential property.
This version uses the `HasMFDerivWithinAt` predicate.  -/
UniqueMDiffOn.image_denseRange' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {s : Set M},
  UniqueMDiff[s] →
    ∀ {f : M → M'} {f' : M → E →L[𝕜] E'},
      (∀ x ∈ s, HasMFDerivAt[s] f x (f' x)) → (∀ x ∈ s, DenseRange ⇑(f' x)) → UniqueMDiff[f '' s]
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.coeFnMonoidHom.eq_1 : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : Monoid R]
  [inst_3 : BoundedMul R] [inst_4 : ContinuousMul R],
  BoundedContinuousFunction.coeFnMonoidHom = { toFun := DFunLike.coe, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Polynomial.Eval.Degree
Polynomial.mapEquiv_apply : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (e : R ≃+* S) (a : Polynomial R),
  (Polynomial.mapEquiv e) a = Polynomial.map (↑e) a
-- Mathlib.Analysis.Normed.Group.Defs
NormedAddCommGroup.toNormedAddGroup.eq_1 : ∀ {E : Type u_5} [inst : NormedAddCommGroup E],
  NormedAddCommGroup.toNormedAddGroup =
    { toNorm := inst.toNorm, toAddGroup := inst.toAddGroup, toMetricSpace := inst.toMetricSpace, dist_eq := ⋯ }
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.step_cons : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {t : Std.DTreeMap.Internal.Impl α β}
  {it : Std.DTreeMap.Internal.Zipper α β},
  (Std.DTreeMap.Internal.Zipper.cons k v t it).step =
    Std.IterStep.yield { internalState := Std.DTreeMap.Internal.Zipper.prependMap t it } ⟨k, v⟩
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁'_obj_map_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (G : C)
  {X Y : C} (g : X ⟶ Y) (X_1 : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁' C).obj G).map g).app X_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X_1 G).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight g X_1)
          G)
        (CategoryTheory.MonoidalCategoryStruct.associator Y X_1 G).hom)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.norm_ofReal_cpow_eventually_eq_atTop : ∀ (c : ℂ), (fun t => ‖↑t ^ c‖) =ᶠ[Filter.atTop] fun t => t ^ c.re
-- Mathlib.Order.Filter.CountableInter
Filter.EventuallyEq.countable_iInter : ∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {s t : ι → Set α},
  (∀ (i : ι), s i =ᶠ[l] t i) → ⋂ i, s i =ᶠ[l] ⋂ i, t i
-- Mathlib.AlgebraicGeometry.PullbackCarrier
/-- Given a triple `(x, y, s)` with `f x = s = f y` there exists `t : X ×[S] Y` above
`x` and `ỳ`. For the unpacked version without `Triplet`, see
`AlgebraicGeometry.Scheme.Pullback.exists_preimage`.  -/
AlgebraicGeometry.Scheme.Pullback.Triplet.exists_preimage : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g),
  ∃ t, (CategoryTheory.Limits.pullback.fst f g) t = T.x ∧ (CategoryTheory.Limits.pullback.snd f g) t = T.y
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey!_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  t.WF →
    ∀ [inst : Inhabited α] {k k' : α} {f : β → β},
      (Std.DTreeMap.Raw.Const.modify t k f).getKey! k' =
        if cmp k k' = Ordering.eq then if k ∈ t then k else default else t.getKey! k'
-- Mathlib.Algebra.Homology.HomologicalComplex
CochainComplex.mk'_X_0 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ : V)
  (d₀ : X₀ ⟶ X₁)
  (succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' CategoryTheory.CategoryStruct.comp f d = 0),
  (CochainComplex.mk' X₀ X₁ d₀ fun {X₀ X₁} => succ').X 0 = X₀
-- Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_snd : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁}
  {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂) (sq₁₃ : G.PullbackObjObj f₁ f₃)
  (α : CategoryTheory.Arrow.mk sq₁₂.ι ⟶ CategoryTheory.Arrow.mk f₃),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α)) sq₁₃.snd =
    adj₂.homEquiv (CategoryTheory.Arrow.Hom.right α)
-- Mathlib.Algebra.HierarchyDesign
/-- When type class inference applies an instance, it attempts to solve the sub-goals from left to
right (it used to be from right to left in lean 3). For example in
```
instance {p : α → Sort*} [∀ x, IsEmpty (p x)] [Nonempty α] : IsEmpty (∀ x, p x)
```
we make sure to write `[∀ x, IsEmpty (p x)]` on the left of `[Nonempty α]` to avoid an expensive
search for `Nonempty α` when there is no instance for `∀ x, IsEmpty (p x)`.

This helps to speed up failing type class searches, for example those triggered by `simp` lemmas.

In some situations, we can't reorder type class assumptions because one depends on the other,
for example in
```
instance {G : Type*} [Group G] [IsKleinFour G] : IsAddKleinFour (Additive G)
```
where the `Group G` instance appears in `IsKleinFour G`. Future work may be done to improve the
type class synthesis order in this situation.
 -/
LibraryNote.instance_argument_order : Batteries.Util.LibraryNote
-- Mathlib.CategoryTheory.Category.Pointed
/-- Composition of morphisms of `Pointed`.  -/
Pointed.Hom.comp : {X Y Z : Pointed} → X.Hom Y → Y.Hom Z → X.Hom Z
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.EffectiveEpiFamilyStruct.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {B : C} {α : Type u_2} {X : α → C}
  {π : (a : α) → X a ⟶ B} [inst_1 : SizeOf C] [inst_2 : SizeOf α]
  (desc :
    {W : C} →
      (e : (a : α) → X a ⟶ W) →
        (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
            CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
              CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) →
          (B ⟶ W))
  (fac :
    ∀ {W : C} (e : (a : α) → X a ⟶ W)
      (h :
        ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
          CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
            CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂))
      (a : α), CategoryTheory.CategoryStruct.comp (π a) (desc e ⋯) = e a)
  (uniq :
    ∀ {W : C} (e : (a : α) → X a ⟶ W)
      (h :
        ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
          CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
            CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂))
      (m : B ⟶ W), (∀ (a : α), CategoryTheory.CategoryStruct.comp (π a) m = e a) → m = desc e ⋯),
  sizeOf { desc := desc, fac := fac, uniq := uniq } = 1
-- Mathlib.Algebra.Group.Units.Basic
LeftCancelMonoid.eq_one_of_mul_right : ∀ {α : Type u} [inst : LeftCancelMonoid α] [Subsingleton αˣ] {a b : α}, a * b = 1 → a = 1
-- Init.Data.SInt.Basic
/-- Subtracts one 16-bit signed integer from another, wrapping around on over- or underflow. Usually
accessed via the `-` operator.

This function is overridden at runtime with an efficient implementation.
 -/
Int16.sub : Int16 → Int16 → Int16
-- Mathlib.Order.Partition.Basic
Partition.IsRepFun.apply_eq_apply_iff : ∀ {α : Type u_1} {u : Set α} {P : Partition u} {f : α → α} {a b : α}, P.IsRepFun f → (f a = f b ↔ a = b ∨ P.Rel a b)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.map_Δ' : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : W.IsElliptic] {A : Type v} [inst_2 : CommRing A]
  (f : R →+* A), (W.map f).Δ' = (Units.map ↑f) W.Δ'
-- Mathlib.Order.Heyting.Basic
/-- `p → q → r ↔ q ∧ p → r`  -/
le_himp_iff' : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, a ≤ b ⇨ c ↔ b ⊓ a ≤ c
-- Mathlib.Logic.Equiv.Option
Equiv.optionSubtype_apply_symm_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (x : β) (e : { e // e none = x }) (b : { y // y ≠ x }),
  some (((Equiv.optionSubtype x) e).symm b) = (↑e).symm ↑b
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesWithinOnBall.neg : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {pf : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f pf s x r → HasFPowerSeriesWithinOnBall (-f) (-pf) s x r
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_erase_le : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, (m.erase k).size ≤ m.size
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.unitsComplexConj.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K]
  [inst_3 : Algebra.IsIntegral ℚ K], NumberField.IsCMField.unitsComplexConj K = NumberField.IsCMField.unitsComplexConj K
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.tanh_periodic : Function.Periodic Complex.tanh (↑Real.pi * Complex.I)
-- Mathlib.GroupTheory.Nilpotent
Subgroup.lowerCentralSeries_succ_eq_bot : ∀ {G : Type u_1} [inst : Group G] (S : Subgroup G) {n : ℕ},
  S.lowerCentralSeries n ≤ Subgroup.center G → S.lowerCentralSeries (n + 1) = ⊥
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastArithShiftRight : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w0 : ℕ} (aig : Std.Sat.AIG α)
  (target : aig.ArbitraryShiftTarget w0) (lhs : BitVec w0) (rhs : BitVec target.n) (assign : α → Bool),
  (∀ (idx : ℕ) (hidx : idx < w0), ⟦assign, { aig := aig, ref := target.target.get idx hidx }⟧ = lhs.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < target.n),
        ⟦assign, { aig := aig, ref := target.distance.get idx hidx }⟧ = rhs.getLsbD idx) →
      ∀ (idx : ℕ) (hidx : idx < w0),
        ⟦assign,
            { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight aig target).aig,
              ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight aig target).vec.get idx hidx }⟧ =
          (lhs.sshiftRight' rhs).getLsbD idx
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiff_iff_continuous_differentiable : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : ℕ∞},
  ContDiff 𝕜 (↑n) f ↔
    (∀ (m : ℕ), ↑m ≤ n → Continuous fun x => iteratedFDeriv 𝕜 m f x) ∧
      ∀ (m : ℕ), ↑m < n → Differentiable 𝕜 fun x => iteratedFDeriv 𝕜 m f x
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.shortComplexMap_comp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) {i' j' k' l' : ι}
  (f₁' : i' ⟶ j') (f₂' : j' ⟶ k') (f₃' : k' ⟶ l') {i'' j'' k'' l'' : ι} (f₁'' : i'' ⟶ j'') (f₂'' : j'' ⟶ k'')
  (f₃'' : k'' ⟶ l'')
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃')
  (β : CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃' ⟶ CategoryTheory.ComposableArrows.mk₃ f₁'' f₂'' f₃'')
  (n₀ n₁ n₂ : ℤ) (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.shortComplexMap_comp._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.shortComplexMap_comp._auto_3),
  X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (CategoryTheory.CategoryStruct.comp α β) n₀ n₁ n₂ hn₁ hn₂ =
    CategoryTheory.CategoryStruct.comp (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂)
      (X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂)
-- Mathlib.Algebra.Category.ModuleCat.Limits
/-- The diagram (in the sense of `CategoryTheory`) of an unbundled `directLimit` of modules.  -/
ModuleCat.directLimitDiagram : {R : Type u} →
  [inst : Ring R] →
    {ι : Type v} →
      [inst_1 : Preorder ι] →
        (G : ι → Type v) →
          [inst_2 : (i : ι) → AddCommGroup (G i)] →
            [inst_3 : (i : ι) → Module R (G i)] →
              (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) →
                [DirectedSystem G fun i j h => ⇑(f i j h)] → CategoryTheory.Functor ι (ModuleCat R)
-- Aesop.Rule
Aesop.RegularRule.safe.injEq : ∀ (r r_1 : Aesop.SafeRule), (Aesop.RegularRule.safe r = Aesop.RegularRule.safe r_1) = (r = r_1)
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.mirror_inj : ∀ {R : Type u_1} [inst : Semiring R] {p q : Polynomial R}, p.mirror = q.mirror ↔ p = q
-- Mathlib.Tactic.Sat.FromLRAT
/-- Construct an individual proof step `⊢ ctx.proof c`.

* `db`: the current global context
* `ns`, `clause`: the new clause
* `pf`: the LRAT proof trace
* `ctx`: the main formula

The proof has three steps:

1. Introduce local assumptions `have h1 : ctx.proof c1 := p1` for each clause `c1`
   referenced in the proof. We actually do all the introductions at once,
   as in `(fun h1 h2 h3 ↦ ...) p1 p2 p3`, because we want `p_i` to not be under any binders
   to avoid the cost of `instantiate` during typechecking and get the benefits of dag-like
   sharing in the `pi` (which are themselves previous proof steps which may be large terms).
   The hypotheses are in `gctx`, keyed on the clause ID.

2. Unfold `⊢ ctx.proof [a, b, c]` to
   `∀ v, v.satisfies_fmla ctx → v.neg a → v.neg b → v.neg c → False` and `intro v hv ha hb hc`,
   storing each `ha : v.neg a` in `lctx`, keyed on the literal `a`.

3. For each LRAT step `hc : ctx.proof [x, y]`, `hc v hv : v.neg x → v.neg y → False`.
   We look for a literal that is not falsified in the clause. Since it is a unit propagation
   step, there can be at most one such literal.
   * If `x` is the non-falsified clause, let `x'` denote the negated literal of `x`.
     Then `x'.negate` reduces to `x`, so `hnx : v.neg x'.negate |- hc v hv hnx hy : False`,
     so we construct the term
       `by_cases (fun hnx : v.neg x'.negate ↦ hc v hv hnx hy) (fun hx : v.neg x ↦ ...)`
     and `hx` is added to the local context.
   * If all clauses are falsified, then we are done: `hc v hv hx hy : False`.
 -/
Mathlib.Tactic.Sat.buildProofStep : Std.HashMap ℕ Mathlib.Tactic.Sat.Clause → Array ℤ → Array ℤ → Lean.Expr → Lean.Expr → Except String Lean.Expr
-- Init.Data.Nat.Basic
Nat.not_ge_eq : ∀ (a b : ℕ), (¬a ≥ b) = (a + 1 ≤ b)
-- Mathlib.Algebra.Group.Hom.Basic
zpowGroupHom.eq_1 : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (n : ℤ),
  zpowGroupHom n = { toFun := fun x => x ^ n, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.comp₂_iso_inv : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Pith B} {x y z : a ⟶ b}
  {f : x ⟶ y} {g : y ⟶ z},
  (CategoryTheory.CategoryStruct.comp f g).iso.inv = CategoryTheory.CategoryStruct.comp g.iso.inv f.iso.inv
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.sectR_obj : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] (b : B) (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  (a : C), (CategoryTheory.Bicategory.Prod.sectR b C).obj a = (b, a)