mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.NonIntegrable
not_integrableOn_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} {k : Set ℝ} (l : Filter ℝ) [l.NeBot] [Filter.TendstoIxxClass Set.Icc l l],
  k ∈ l →
    (∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x) →
      Filter.Tendsto (fun x => ‖f x‖) l Filter.atTop →
        deriv f =O[l] g → ¬MeasureTheory.IntegrableOn g k MeasureTheory.volume
-- Init.Data.String.Termination
String.Slice.Pos.prev_prev_lt : ∀ {s : String.Slice} {p : s.Pos} {h : p ≠ s.startPos} {h' : p.prev h ≠ s.startPos}, (p.prev h).prev h' < p
-- Mathlib.Combinatorics.Quiver.SingleObj
Quiver.SingleObj.toPrefunctor_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ),
  Quiver.SingleObj.toPrefunctor (g ∘ f) = Quiver.SingleObj.toPrefunctor f ⋙q Quiver.SingleObj.toPrefunctor g
-- Mathlib.Order.CountableSupClosed
sup_mem_countableSupClosure : ∀ {α : Type u_2} {s : Set α} {a b : α} [inst : SemilatticeSup α], a ∈ s → b ∈ s → a ⊔ b ∈ countableSupClosure s
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.homologyFunctorFactors_hom_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {K L : CochainComplex C ℤ} (f : K ⟶ L) (n : ℤ),
  CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctor C n).map (DerivedCategory.Q.map f))
      ((DerivedCategory.homologyFunctorFactors C n).hom.app L) =
    CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctorFactors C n).hom.app K)
      (HomologicalComplex.homologyMap f n)
-- Mathlib.Topology.Constructions
Topology.IsEmbedding.sigmaMk : ∀ {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] {i : ι}, Topology.IsEmbedding (Sigma.mk i)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.tail : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.IsPath → p.tail.IsPath
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.comap_injective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N},
  Function.Surjective ⇑f → Function.Injective (Subgroup.comap f)
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.mem_or_inv_mem : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (x : K), x ∈ A ∨ x⁻¹ ∈ A
-- Mathlib.Data.Quot
Quot.liftOn₂_mk : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : α → α → Prop} {s : β → β → Prop} (a : α) (b : β) (f : α → β → γ)
  (hr : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂ → f a b₁ = f a b₂) (hs : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂ → f a₁ b = f a₂ b),
  (Quot.mk r a).liftOn₂ (Quot.mk s b) f hr hs = f a b
-- Mathlib.Tactic.Positivity.Basic
Mathlib.Meta.Positivity.ite_nonneg : ∀ {α : Type u_1} [inst : Zero α] (p : Prop) [inst_1 : Decidable p] {a b : α} [inst_2 : LE α],
  0 ≤ a → 0 ≤ b → 0 ≤ if p then a else b
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.toSubsemiring_eq_top : ∀ {R : Type u} [inst : NonAssocRing R] {S : Subring R}, S.toSubsemiring = ⊤ ↔ S = ⊤
-- Mathlib.Algebra.Module.Submodule.Ker
Submodule.comap_bot : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (f : M →ₛₗ[τ₁₂] M₂), Submodule.comap f ⊥ = f.ker
-- Init.Data.Array.Attach
Array.getElem_pmap : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) {xs : Array α} (h : ∀ a ∈ xs, p a) {i : ℕ}
  (hi : i < (Array.pmap f xs h).size), (Array.pmap f xs h)[i] = f xs[i] ⋯
-- Mathlib.Combinatorics.Configuration
/-- Number of lines through a given point.  -/
Configuration.pointCount : (P : Type u_1) → {L : Type u_2} → [Membership P L] → L → ℕ
-- Mathlib.Analysis.CStarAlgebra.Unitization
/-- A C⋆-algebra over a densely normed field is a regular normed algebra.  -/
CStarRing.instRegularNormedAlgebra : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : DenselyNormedField 𝕜] [inst_1 : NonUnitalNormedRing E] [inst_2 : StarRing E]
  [CStarRing E] [inst_4 : NormedSpace 𝕜 E] [inst_5 : IsScalarTower 𝕜 E E] [inst_6 : SMulCommClass 𝕜 E E],
  RegularNormedAlgebra 𝕜 E
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
ContinuousLinearMap.toUniformConvergenceCLM_symm_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul 𝕜₂ F] {𝔖 : Set (Set E)} {A : UniformConvergenceCLM σ F 𝔖} {x : E},
  ((ContinuousLinearMap.toUniformConvergenceCLM σ F 𝔖).symm A) x = A x
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeDTR.go.match_1.eq_3 : ∀ {α : Type u_1} (motive : ℕ → List α → Array α → Sort u_2) (n : ℕ) (acc : Array α)
  (h_1 : (n : ℕ) → (x : α) → (xs : List α) → (acc : Array α) → motive n.succ (x :: xs) acc)
  (h_2 : (x : List α) → (acc : Array α) → motive 0 x acc) (h_3 : (n : ℕ) → (acc : Array α) → motive n [] acc),
  (n = 0 → False) →
    (match n, [], acc with
      | n.succ, x :: xs, acc => h_1 n x xs acc
      | 0, x, acc => h_2 x acc
      | n, [], acc => h_3 n acc) =
      h_3 n acc
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.map.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β),
  LowerSet.map f =
    {
      toEquiv :=
        { toFun := fun s => { carrier := ⇑f '' ↑s, lower' := ⋯ },
            invFun := fun t => { carrier := ⇑f ⁻¹' ↑t, lower' := ⋯ }, left_inv := ⋯, right_inv := ⋯,
            map_rel_iff' := ⋯ }.toEquiv,
      map_rel_iff' := ⋯ }
-- Mathlib.Algebra.Group.Units.Equiv
val_toAddUnits_apply : ∀ {G : Type u_5} [inst : AddGroup G] (x : G), ↑(toAddUnits x) = x
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.costar_fst : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] (φ : U ⥤q V) (u : U) (a : Quiver.Costar u),
  (φ.costar u a).fst = φ.obj a.fst
-- Mathlib.Algebra.GroupWithZero.Action.Defs
SMulZeroClass.toSMul : {M : Type u_12} → {A : Type u_13} → {inst : Zero A} → [self : SMulZeroClass M A] → SMul M A
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.iteratedSliceEquiv_counitIso : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X),
  f.iteratedSliceEquiv.counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun g =>
        CategoryTheory.Over.isoMk
          (CategoryTheory.Iso.refl ((f.iteratedSliceBackward.comp f.iteratedSliceForward).obj g).left) ⋯)
      ⋯
-- Mathlib.Logic.Equiv.Prod
/-- Type product is commutative up to an equivalence: `α × β ≃ β × α`. This is `Prod.swap` as an
equivalence.  -/
Equiv.prodComm : (α : Type u_9) → (β : Type u_10) → α × β ≃ β × α
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
AEMeasurable.real_toNNReal : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → ℝ} {μ : MeasureTheory.Measure α},
  AEMeasurable f μ → AEMeasurable (fun x => (f x).toNNReal) μ
-- Mathlib.Topology.Algebra.FilterBasis
/-- The neighborhood function of an `AddGroupFilterBasis`.  -/
AddGroupFilterBasis.N : {G : Type u} → [inst : AddGroup G] → AddGroupFilterBasis G → G → Filter G
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.IsCommMonObj.mul_comm_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} (X : C) {inst_3 : CategoryTheory.MonObj X}
  [self : CategoryTheory.IsCommMonObj X] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (β_ X X).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.id_comp : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X Y : CategoryTheory.FreeMonoidalCategory C} (f : X.Hom Y), CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- An oriented angle is unchanged by replacing the first point with the midpoint of the segment
between it and the second point.  -/
EuclideanGeometry.oangle_midpoint_left : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  (p₁ p₂ p₃ : P), EuclideanGeometry.oangle (midpoint ℝ p₁ p₂) p₂ p₃ = EuclideanGeometry.oangle p₁ p₂ p₃
-- Mathlib.Data.Real.Basic
/-- The underlying Cauchy completion  -/
Real.cauchy : ℝ → CauSeq.Completion.Cauchy abs
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
AlgebraicGeometry.ValuativeCommSq.mk.inj : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {R : Type u} {commRing : CommRing R} {domain : IsDomain R}
  {valuationRing : ValuationRing R} {K : Type u} {field : Field K} {algebra : Algebra R K}
  {isFractionRing : IsFractionRing R K} {i₁ : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ X}
  {i₂ : AlgebraicGeometry.Spec (CommRingCat.of R) ⟶ Y}
  {commSq : CategoryTheory.CommSq i₁ (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K))) f i₂}
  {R_1 : Type u} {commRing_1 : CommRing R_1} {domain_1 : IsDomain R_1} {valuationRing_1 : ValuationRing R_1}
  {K_1 : Type u} {field_1 : Field K_1} {algebra_1 : Algebra R_1 K_1} {isFractionRing_1 : IsFractionRing R_1 K_1}
  {i₁_1 : AlgebraicGeometry.Spec (CommRingCat.of K_1) ⟶ X} {i₂_1 : AlgebraicGeometry.Spec (CommRingCat.of R_1) ⟶ Y}
  {commSq_1 : CategoryTheory.CommSq i₁_1 (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R_1 K_1))) f i₂_1},
  { R := R, commRing := commRing, domain := domain, valuationRing := valuationRing, K := K, field := field,
        algebra := algebra, isFractionRing := isFractionRing, i₁ := i₁, i₂ := i₂, commSq := commSq } =
      { R := R_1, commRing := commRing_1, domain := domain_1, valuationRing := valuationRing_1, K := K_1,
        field := field_1, algebra := algebra_1, isFractionRing := isFractionRing_1, i₁ := i₁_1, i₂ := i₂_1,
        commSq := commSq_1 } →
    R = R_1 ∧ commRing ≍ commRing_1 ∧ K = K_1 ∧ field ≍ field_1 ∧ algebra ≍ algebra_1 ∧ i₁ ≍ i₁_1 ∧ i₂ ≍ i₂_1
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.mem_skeletonLT_iff : ∀ {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [inst : T2Space X] [inst_1 : Topology.CWComplex C] {n : ℕ∞}
  {x : X}, x ∈ Topology.RelCWComplex.skeletonLT C n ↔ ∃ m, ∃ (_ : ↑m < n), ∃ j, x ∈ Topology.RelCWComplex.openCell m j
-- Mathlib.Data.Nat.Digits.Lemmas
List.card_fixedLengthDigits : ∀ {b : ℕ} (hb : 1 < b) (l : ℕ), (List.fixedLengthDigits hb l).card = b ^ l
-- Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul : ∀ {α : Type u_1} {F : Type u_3} {G : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] [inst_1 : NormedAddCommGroup G] {f : α → F} {g : α → G} {c : ℝ},
  (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖) →
    ∀ (p : ENNReal), MeasureTheory.eLpNorm f p μ ≤ ENNReal.ofReal c * MeasureTheory.eLpNorm g p μ
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isPrincipal_mul_one : Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) 1
-- Mathlib.Analysis.Calculus.FDeriv.Pow
DifferentiableWithinAt.pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {x : E}
  {s : Set E}, DifferentiableWithinAt 𝕜 f s x → ∀ (n : ℕ), DifferentiableWithinAt 𝕜 (f ^ n) s x
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.ofHom.eq_1 : ∀ {X Y : Type u} [inst : Add X] [inst_1 : Add Y] (f : X →ₙ+ Y),
  AddMagmaCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.IsReproducing.span_eq_top : ∀ {R : Type u_7} {M : Type u_8} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {C : ConvexCone R M}, C.IsReproducing → Submodule.span R ↑C = ⊤
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.zero_add_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.AddMonObj M] {Z : C} (f : Z ⟶ M),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero f)
      CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom f
-- Lean.Parser.Do
Lean.Parser.Term.leftArrow.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.toList_ensureTermination : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.ensureTermination.toList = it.toList
-- Lean.Parser.Basic
Lean.Parser.TokenMap.instEmptyCollection : {α : Type} → EmptyCollection (Lean.Parser.TokenMap α)
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Computation.Corec.f.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : α ⊕ β → Sort u_3) →
      (x : α ⊕ β) → ((a : α) → motive (Sum.inl a)) → ((val : β) → motive (Sum.inr val)) → motive x
-- Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
HomotopicalAlgebra.RelativeCellComplex.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w'} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J] {α : J → Type t} {A B : (j : J) → α j → C}
  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} {X Y : C} {f : X ⟶ Y} [inst_5 : SizeOf C] [inst_6 : SizeOf J]
  [inst_7 : (a : J) → SizeOf (α a)] (toTransfiniteCompositionOfShape : CategoryTheory.TransfiniteCompositionOfShape J f)
  (attachCells :
    (j : J) →
      ¬IsMax j →
        HomotopicalAlgebra.AttachCells (basicCell j)
          (toTransfiniteCompositionOfShape.F.map (CategoryTheory.homOfLE ⋯))),
  sizeOf { toTransfiniteCompositionOfShape := toTransfiniteCompositionOfShape, attachCells := attachCells } =
    1 + sizeOf toTransfiniteCompositionOfShape
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.prodMk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β} {g : α → γ} {s : Set α} {x : α},
  ContinuousWithinAt f s x → ContinuousWithinAt g s x → ContinuousWithinAt (fun x => (f x, g x)) s x
-- Init.Data.List.Lemmas
/-- If one has `l.get i` in an expression (with `i : Fin l.length`) and `h : l = l'`,
`rw [h]` will give a "motive is not type correct" error, as it cannot rewrite the
`i : Fin l.length` to `Fin l'.length` directly. The theorem `get_of_eq` can be used to make
such a rewrite, with `rw [get_of_eq h]`.
 -/
List.get_of_eq : ∀ {α : Type u_1} {l l' : List α} (h : l = l') (i : Fin l.length), l.get i = l'.get ⟨↑i, ⋯⟩
-- Mathlib.Algebra.Homology.Augment
/-- There is a canonical chain map from the truncation of a cochain complex `C` to
the "single object" cochain complex consisting of the truncated object `C.X 0` in degree 0.
The components of this chain map are `C.d 0 1` in degree 0, and zero otherwise.
 -/
CochainComplex.toTruncate : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject V] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] →
        (C : CochainComplex V ℕ) → (CochainComplex.single₀ V).obj (C.X 0) ⟶ CochainComplex.truncate.obj C
-- Mathlib.Order.Filter.Pointwise
Filter.eventually_vadd_filter : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f : Filter β} {a : α} {p : β → Prop},
  (∀ᶠ (y : β) in a +ᵥ f, p y) ↔ ∀ᶠ (x : β) in f, p (a +ᵥ x)
-- Lean.Elab.Tactic.SimpTrace
Lean.Elab.Tactic.evalSimpTrace : Lean.Elab.Tactic.Tactic
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Iso.coe_induce : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} {s : Set V} {t : Set W} (φ : G ≃g G')
  (φst : Set.BijOn (⇑φ) s t), ⇑(φ.induce φst) = Set.MapsTo.restrict (⇑φ) s t ⋯
-- Mathlib.Algebra.Order.Group.Cone
AddGroupConeClass.mk : ∀ {S : Type u_1} {G : outParam (Type u_2)} [inst : AddCommGroup G] [inst_1 : SetLike S G]
  [toAddSubmonoidClass : AddSubmonoidClass S G], (∀ {C : S} {a : G}, a ∈ C → -a ∈ C → a = 0) → AddGroupConeClass S G
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- The limit `q` of the
inductively constructed sequence `qₖ` in the proof of Weierstrass division.  -/
PowerSeries.IsWeierstrassDivisorAt.div : {A : Type u_1} →
  [inst : CommRing A] →
    {g : PowerSeries A} →
      {I : Ideal A} → g.IsWeierstrassDivisorAt I → PowerSeries A → [IsPrecomplete I A] → PowerSeries A
-- Mathlib.CategoryTheory.IsoCat
/-- The strict inverse of a functor that is an isomorphism of categories, defined using
`Functor.objEquiv` on objects and `Functor.preimage` on morphisms.  -/
CategoryTheory.Functor.strictInv : {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] →
        (F : CategoryTheory.Functor C D) → [F.IsIso] → CategoryTheory.Functor D C
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Injective.State.fns : Lean.Meta.Grind.Injective.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.InjectiveInfo
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
/-- If `M` is a presheaf of modules, the cokernel cofork
`M.freeYonedaCoproductsCokernelCofork` is a colimit, which means that
`M` can be expressed as a cokernel of the morphism `M.toFreeYonedaCoproduct`
between coproducts of free presheaves of modules on Yoneda presheaves.  -/
PresheafOfModules.isColimitFreeYonedaCoproductsCokernelCofork : {C : Type u} →
  [inst : CategoryTheory.SmallCategory C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      (M : PresheafOfModules R) → CategoryTheory.Limits.IsColimit M.freeYonedaCoproductsCokernelCofork
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.write_self : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (T : Turing.Tape Γ), Turing.Tape.write T.head T = T
-- Mathlib.RingTheory.Flat.Rank
RingHom.finrank.eq_1 : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (x : PrimeSpectrum R),
  f.finrank x = Module.rankAtStalk S x
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.inducedOuterMeasure_exists_set : ∀ {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0}
  (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)),
  (∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) →
    (∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) →
      ∀ {s : Set α},
        (MeasureTheory.inducedOuterMeasure m P0 m0) s ≠ ⊤ →
          ∀ {ε : ENNReal},
            ε ≠ 0 →
              ∃ t,
                P t ∧
                  s ⊆ t ∧
                    (MeasureTheory.inducedOuterMeasure m P0 m0) t ≤ (MeasureTheory.inducedOuterMeasure m P0 m0) s + ε
-- Mathlib.Order.CompleteLattice.Finset
/-- **Alias** of `Finset.minimal_iff_forall_erase`. -/
Finset.minimal_iff_forall_diff_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] {P : Finset α → Prop} {s : Finset α},
  (∀ ⦃s t : Finset α⦄, P t → t ⊆ s → P s) → (Minimal P s ↔ P s ∧ ∀ x ∈ s, ¬P (s.erase x))
-- Lean.Parser.Types
Lean.Parser.CacheableParserContext.prec : Lean.Parser.CacheableParserContext → ℕ
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.getKey_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {a : α} {h : a ∈ m},
  m.getKey a h = Std.DHashMap.Internal.Raw₀.getKey ⟨m, ⋯⟩ a ⋯
-- Mathlib.Topology.Category.Compactum
instInhabitedCompactum : Inhabited Compactum
-- Init.Meta.Defs
Lean.monadNameGeneratorLift : (m n : Type → Type) → [MonadLift m n] → [Lean.MonadNameGenerator m] → Lean.MonadNameGenerator n
-- Lean.Data.DeclarationRange
Lean.DeclarationRange.mk.inj : ∀ {pos : Lean.Position} {charUtf16 : ℕ} {endPos : Lean.Position} {endCharUtf16 : ℕ} {pos_1 : Lean.Position}
  {charUtf16_1 : ℕ} {endPos_1 : Lean.Position} {endCharUtf16_1 : ℕ},
  { pos := pos, charUtf16 := charUtf16, endPos := endPos, endCharUtf16 := endCharUtf16 } =
      { pos := pos_1, charUtf16 := charUtf16_1, endPos := endPos_1, endCharUtf16 := endCharUtf16_1 } →
    pos = pos_1 ∧ charUtf16 = charUtf16_1 ∧ endPos = endPos_1 ∧ endCharUtf16 = endCharUtf16_1
-- Mathlib.Data.Analysis.Topology
/-- The topological space realizer made of the open sets.  -/
Ctop.Realizer.id : {α : Type u_1} → [inst : TopologicalSpace α] → Ctop.Realizer α
-- Mathlib.RepresentationTheory.Homological.Resolution
Rep.barResolution_complex : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Group G], (Rep.barResolution k G).complex = Rep.barComplex k G
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.equiv_iff_toArray_perm : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp},
  t₁.Equiv t₂ ↔ t₁.toArray.Perm t₂.toArray
-- Init.Control.ExceptCps
ExceptCpsT.instLawfulMonad : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2}, LawfulMonad (ExceptCpsT σ m)
-- Batteries.Lean.EStateM
EStateM.run'_adaptExcept : ∀ {ε σ α : Type u_1} (f : ε → ε) (x : EStateM ε σ α) (s : σ), (EStateM.adaptExcept f x).run' s = x.run' s
-- Init.Data.Vector.Lemmas
Vector.instDecidableForallVectorZero : {α : Type u_1} → (P : Vector α 0 → Prop) → [Decidable (P #v[])] → Decidable (∀ (xs : Vector α 0), P xs)
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.any.match_1.eq_1 : ∀ (motive : (x : ℕ) → ((i : ℕ) → i < x → Bool) → Sort u_1) (f : (i : ℕ) → i < 0 → Bool)
  (h_1 : (f : (i : ℕ) → i < 0 → Bool) → motive 0 f)
  (h_2 : (n : ℕ) → (f : (i : ℕ) → i < n.succ → Bool) → motive n.succ f),
  (match 0, f with
    | 0, f => h_1 f
    | n.succ, f => h_2 n f) =
    h_1 f
-- Mathlib.LinearAlgebra.LinearPMap
Submodule.toLinearPMap_graph_eq : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] (g : Submodule R (E × F)),
  (∀ x ∈ g, x.1 = 0 → x.2 = 0) → g.toLinearPMap.graph = g
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.mulEquivHaarChar_eq : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalGroup G] [inst_5 : LocallyCompactSpace G] (μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsHaarMeasure] [μ.Regular] (φ : G ≃ₜ* G),
  MeasureTheory.mulEquivHaarChar φ = μ.haarScalarFactor (MeasureTheory.Measure.map (⇑φ) μ)
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
AffineBasis.exists_affineBasis_of_finiteDimensional : ∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : DivisionRing k] [inst_3 : Module k V] [inst_4 : Fintype ι] [FiniteDimensional k V],
  Fintype.card ι = Module.finrank k V + 1 → Nonempty (AffineBasis ι k P)
-- Mathlib.Algebra.Order.Hom.Basic
/-- `RingSeminormClass F α` states that `F` is a type of `β`-valued seminorms on the ring `α`.

You should extend this class when you extend `RingSeminorm`.  -/
RingSeminormClass : (F : Type u_7) →
  (α : outParam (Type u_8)) →
    (β : outParam (Type u_9)) → [NonUnitalNonAssocRing α] → [Semiring β] → [PartialOrder β] → [FunLike F α β] → Prop