mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Remove an element from the tree using a cut function.
The `cut` function is used to locate an element in the tree:
it returns `.gt` if we go too high and `.lt` if we go too low;
if it returns `.eq` we will remove the element.
(The function `cmp k` for some key `k` is a valid cut function, but we can also use cuts that
are not of this form as long as they are suitably monotonic.)
 -/
RBTree.RBSet.erase : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp → (α → Ordering) → RBTree.RBSet α cmp
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.isDenseEmbedding_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X] [NoncompactSpace X], IsDenseEmbedding OnePoint.some
-- Std.Do.WP.SimpLemmas
Except.mapError.eq_2 : ∀ {ε : Type u} {ε' : Type u_1} {α : Type u_2} (f : ε → ε') (v : α), Except.mapError f (Except.ok v) = Except.ok v
-- Mathlib.Analysis.Distribution.Sobolev
TemperedDistribution.memSobolev_zero_iff : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : NormedSpace ℂ F] [inst_7 : CompleteSpace F] {p : ENNReal} [hp : Fact (1 ≤ p)]
  {f : TemperedDistribution E F},
  TemperedDistribution.MemSobolev 0 p f ↔ ∃ f', f = MeasureTheory.Lp.toTemperedDistribution f'
-- Mathlib.Geometry.Convex.Cone.Face.Basic
PointedCone.IsFaceOf.add_mem_iff_mem : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C F : PointedCone R M},
  F.IsFaceOf C → ∀ {x y : M}, x ∈ C → y ∈ C → (x + y ∈ F ↔ x ∈ F ∧ y ∈ F)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {k : α} {f : Option (β k) → Option (β k)}, (t.alter k f).get? k = f (t.get? k)
-- Mathlib.LinearAlgebra.Matrix.ToLin
Module.Basis.linearMap_apply_apply : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {ι₁ : Type u_6} {ι₂ : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M₁] [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂]
  [inst_5 : Fintype ι₁] [inst_6 : Fintype ι₂] [inst_7 : DecidableEq ι₁] (b₁ : Module.Basis ι₁ R M₁)
  (b₂ : Module.Basis ι₂ R M₂) (ij : ι₂ × ι₁) (k : ι₁), ((b₁.linearMap b₂) ij) (b₁ k) = if ij.2 = k then b₂ ij.1 else 0
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitIterator.instIteratorIdSubslice.match_3.eq_4 : ∀ {σ : String.Slice → Type} [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  {s : String.Slice} (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)) (motive : searcher.Step → Sort u_1)
  (property : searcher.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (searcher' : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (startPos endPos : s.Pos) →
        (hps :
            searcher.IsPlausibleStep
              (Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos))) →
          ⟨Std.IterStep.done, property⟩ =
              ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos), hps⟩ →
            motive ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos), hps⟩)
  (h_2 :
    (searcher' : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (startPos endPos : s.Pos) →
        (hps :
            searcher.IsPlausibleStep
              (Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos))) →
          ⟨Std.IterStep.done, property⟩ =
              ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps⟩ →
            motive ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps⟩)
  (h_3 :
    (searcher' : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (hps : searcher.IsPlausibleStep (Std.IterStep.skip searcher')) →
        ⟨Std.IterStep.done, property⟩ = ⟨Std.IterStep.skip searcher', hps⟩ → motive ⟨Std.IterStep.skip searcher', hps⟩)
  (h_4 :
    (property_1 : searcher.IsPlausibleStep Std.IterStep.done) →
      ⟨Std.IterStep.done, property⟩ = ⟨Std.IterStep.done, property_1⟩ → motive ⟨Std.IterStep.done, property_1⟩),
  (match h : ⟨Std.IterStep.done, property⟩ with
    | ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos), hps⟩ =>
      h_1 searcher' startPos endPos hps h
    | ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps⟩ =>
      h_2 searcher' startPos endPos hps h
    | ⟨Std.IterStep.skip searcher', hps⟩ => h_3 searcher' hps h
    | ⟨Std.IterStep.done, property_1⟩ => h_4 property_1 h) =
    h_4 property ⋯
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
/-- For a real number `m`, Liouville's constant is
$$
\sum_{i=0}^\infty\frac{1}{m^{i!}}.
$$
The series converges only for `1 < m`. However, there is no restriction on `m`, since,
if the series does not converge, then the sum of the series is defined to be zero.
 -/
liouvilleNumber : ℝ → ℝ
-- Mathlib.Algebra.Ring.Prod
RingHom.instRingHomSurjectiveProdSnd : ∀ (R : Type u_6) (S : Type u_7) [inst : Semiring R] [inst_1 : Semiring S], RingHomSurjective (RingHom.snd R S)
-- Mathlib.Algebra.Order.Field.Power
Even.zpow_abs : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] {p : ℤ}, Even p → ∀ (a : α), |a| ^ p = a ^ p
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.IsColimit.fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} {K : CategoryTheory.Limits.Multicofork I}
  (hK : CategoryTheory.Limits.IsColimit K) {T : C} (k : (a : J.R) → I.right a ⟶ T)
  (hk :
    ∀ (b : J.L),
      CategoryTheory.CategoryStruct.comp (I.fst b) (k (J.fst b)) =
        CategoryTheory.CategoryStruct.comp (I.snd b) (k (J.snd b)))
  (a : J.R), CategoryTheory.CategoryStruct.comp (K.π a) (CategoryTheory.Limits.Multicofork.IsColimit.desc hK k hk) = k a
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.mulLeft_zero_eq_zero : ∀ (R : Type u_14) (A : Type u_15) [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A], LinearMap.mulLeft R 0 = 0
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.inr_normalizationCoprodIso_hom_fromNormalization_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {U V : AlgebraicGeometry.Scheme} {iU : U ⟶ X} {iV : V ⟶ X}
  (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV))
  [inst_2 : AlgebraicGeometry.QuasiCompact iU] [inst_3 : AlgebraicGeometry.QuasiSeparated iU]
  [inst_4 : AlgebraicGeometry.QuasiCompact iV] [inst_5 : AlgebraicGeometry.QuasiSeparated iV]
  {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso f e).hom
        (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.fromNormalization f) h)) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.fromNormalization (CategoryTheory.CategoryStruct.comp iV f)) h
-- Mathlib.Topology.Covering.Quotient
/-- A function from a topological space `E` with an action by a discrete group to another
topological space `X` is a quotient covering map if it is a quotient map, the action is
continuous and transitive on fibers, and every point of `E` has a neighborhood whose translates
by the group elements are pairwise disjoint.  -/
IsAddQuotientCoveringMap : {E : Type u_1} →
  {X : Type u_2} →
    [TopologicalSpace E] →
      [TopologicalSpace X] → (E → X) → (G : Type u_4) → [inst : AddGroup G] → [AddAction G E] → Prop
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.ULiftYoneda.instFaithfulFunctorOppositeTypeUliftYoneda : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C], CategoryTheory.uliftYoneda.{w, v₁, u₁}.Faithful
-- Mathlib.MeasureTheory.Measure.Restrict
/-- Restrict a measure `μ` to a set `s` as an `ℝ≥0∞`-linear map.  -/
MeasureTheory.Measure.restrictₗ : {α : Type u_2} → {m0 : MeasurableSpace α} → Set α → MeasureTheory.Measure α →ₗ[ENNReal] MeasureTheory.Measure α
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.Hom.mk.congr_simp : ∀ {X Y : Pointed} (toFun toFun_1 : X.X → Y.X) (e_toFun : toFun = toFun_1) (map_point : toFun X.point = Y.point),
  { toFun := toFun, map_point := map_point } = { toFun := toFun_1, map_point := ⋯ }
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.mem_basicOpen : ∀ {R : Type u} [inst : CommSemiring R] (f : R) (x : PrimeSpectrum R), x ∈ PrimeSpectrum.basicOpen f ↔ f ∉ x.asIdeal
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Given `F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v`, this is the presheaf that is given by
`YonedaCollection F X` on objects.  -/
CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (A : CategoryTheory.Functor Cᵒᵖ (Type v)) →
      CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v) →
        CategoryTheory.Functor Cᵒᵖ (Type v)
-- Mathlib.CategoryTheory.Monoidal.Types.Basic
CategoryTheory.braiding_hom_apply : ∀ {X Y : Type u} {x : X} {y : Y}, (CategoryTheory.ConcreteCategory.hom (β_ X Y).hom) (x, y) = (y, x)
-- Mathlib.CategoryTheory.Limits.Cones
/-- Change a cocone on `F : Jᵒᵖ ⥤ Cᵒᵖ` into a cone on `F.unop : J ⥤ C`.  -/
CategoryTheory.Limits.coneUnopOfCocone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} → CategoryTheory.Limits.Cocone F → CategoryTheory.Limits.Cone F.unop
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- A functor applied to a span is a span.  -/
CategoryTheory.Limits.spanCompIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          {X Y Z : C} →
            (f : X ⟶ Y) →
              (g : X ⟶ Z) → (CategoryTheory.Limits.span f g).comp F ≅ CategoryTheory.Limits.span (F.map f) (F.map g)
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
riemannZeta_eventually_ne_zero_nhds_one : ∀ᶠ (s : ℂ) in nhds 1, riemannZeta s ≠ 0
-- Mathlib.Combinatorics.Additive.ETransform
/-- An **e-transform**.
Turns `(s, t)` into `(s ∩ s +ᵥ e, t ∪ -e +ᵥ t)`. This reduces the sum of the two sets.  -/
Finset.addETransformLeft : {α : Type u_1} → [DecidableEq α] → [AddGroup α] → α → Finset α × Finset α → Finset α × Finset α
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.listR.eq_3 : ∀ {α : Type u_1} (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (parent : RBTree.RBNode.Path α),
  (RBTree.RBNode.Path.right c l v parent).listR = parent.listR
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
RootPairing.RootPositiveForm.rootLength_le_of_pairingIn_eq : ∀ {ι : 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} [Finite ι]
  [inst_6 : CharZero R] [inst_7 : P.IsCrystallographic] [IsDomain R] (B : RootPairing.RootPositiveForm ℤ P) {i j : ι},
  P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1 → B.rootLength i ≤ B.rootLength j
-- Mathlib.Data.Sum.Interval
Sum.instLocallyFiniteOrderBot : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → [LocallyFiniteOrderBot α] → [LocallyFiniteOrderBot β] → LocallyFiniteOrderBot (α ⊕ β)
-- Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
/-- In an Archimedean linearly ordered additive group (with the order topology), a
subgroup is discrete iff it is cyclic.  -/
AddSubgroup.discrete_iff_addCyclic : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [inst_3 : TopologicalSpace G]
  [OrderTopology G] [Archimedean G] {H : AddSubgroup G}, IsAddCyclic ↥H ↔ DiscreteTopology ↥H
-- Mathlib.Topology.CWComplex.Abstract.Basic
/-- A relative CW-complex is a morphism `f : X ⟶ Y` equipped with data expressing
that `Y` identifies to the colimit of a functor `F : ℕ ⥤ TopCat` with that
`F.obj 0 ≅ X` and for any `n : ℕ`, `F.obj (n + 1)` is obtained from `F.obj n`
by attaching `n`-disks.  -/
TopCat.RelativeCWComplex : {X Y : TopCat} → (X ⟶ Y) → Type (max (max (max (max 0 (u + 1)) u) (u + 1)) 0)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.smulCommClass : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type v} [inst : SMul R α] [inst_1 : SMul S α]
  [SMulCommClass R S α], SMulCommClass R S (Matrix m n α)
-- Mathlib.Data.Nat.WithBot
Nat.WithBot.add_eq_three_iff : ∀ {n m : WithBot ℕ}, n + m = 3 ↔ n = 0 ∧ m = 3 ∨ n = 1 ∧ m = 2 ∨ n = 2 ∧ m = 1 ∨ n = 3 ∧ m = 0
-- Std.Data.ExtDHashMap.Basic
Std.ExtDHashMap.instReflBEq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] [inst_1 : (k : α) → BEq (β k)]
  [∀ (k : α), ReflBEq (β k)], ReflBEq (Std.ExtDHashMap α β)
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- Hausdorff measure on an (e)metric space.  -/
MeasureTheory.Measure.hausdorffMeasure : {X : Type u_2} → [inst : EMetricSpace X] → [inst_1 : MeasurableSpace X] → [BorelSpace X] → ℝ → MeasureTheory.Measure X
-- Init.Core
DoResultSBC.break.injEq : ∀ {α σ : Type u} (a a_1 : σ), (DoResultSBC.break a = DoResultSBC.break a_1) = (a = a_1)
-- Mathlib.Analysis.Normed.Group.Basic
ball_eq_norm_inv_mul_lt : ∀ {E : Type u_5} [inst : SeminormedGroup E] (y : E) (ε : ℝ), Metric.ball y ε = {x | ‖x⁻¹ * y‖ < ε}
-- Mathlib.Algebra.Star.Subsemiring
/-- Reinterpret a `StarSubsemiring` as a `Subsemiring`.  -/
StarSubsemiring.toSubsemiring : {R : Type v} → [inst : NonAssocSemiring R] → [inst_1 : Star R] → StarSubsemiring R → Subsemiring R
-- Mathlib.RingTheory.Extension.Presentation.Core
/-- The core coerced to a type for performance reasons.  -/
Algebra.Presentation.Core : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.Presentation R S ι σ → Type u_1
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapLeftHomologyIso_hom_naturality_assoc : ∀ {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.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasLeftHomology]
  [inst_6 : S₂.HasLeftHomology] [inst_7 : F.PreservesLeftHomologyOf S₁] [inst_8 : F.PreservesLeftHomologyOf S₂] {Z : D}
  (h : F.obj S₂.leftHomology ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap (F.mapShortComplex.map φ))
      (CategoryTheory.CategoryStruct.comp (S₂.mapLeftHomologyIso F).hom h) =
    CategoryTheory.CategoryStruct.comp (S₁.mapLeftHomologyIso F).hom
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.leftHomologyMap φ)) h)
-- Init.Data.Float.Model.Unpacked.Pack.Lemmas
Float.Model.UnpackedFloat.packComponents.eq_1 : ∀ (spec : Float.Model.Format) (sign : Float.Model.UnpackedFloat.Sign) (exponent : BitVec spec.exponentBits)
  (mantissa : BitVec spec.mantissaBitsWithoutImplicit),
  Float.Model.UnpackedFloat.packComponents spec sign exponent mantissa = sign.toBitVec ++ exponent ++ mantissa
-- Mathlib.Topology.Algebra.ConstMulAction
continuousWithinAt_const_smul_iff : ∀ {α : Type u_2} {β : Type u_3} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [ContinuousConstSMul G α] [inst_4 : TopologicalSpace β] {f : β → α} {b : β} {s : Set β} (c : G),
  ContinuousWithinAt (fun x => c • f x) s b ↔ ContinuousWithinAt f s b
-- Mathlib.NumberTheory.Real.Irrational
Irrational.mul_cases : ∀ {x y : ℝ}, Irrational (x * y) → Irrational x ∨ Irrational y
-- Aesop.Util.UnionFind
Aesop.instInhabitedUnionFind : {a : Type u_1} → {a_1 : BEq a} → {a_2 : Hashable a} → Inhabited (Aesop.UnionFind a)
-- Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
iteratedDeriv_comp_two : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {g f : 𝕜 → 𝕜} {x : 𝕜},
  ContDiffAt 𝕜 2 g (f x) →
    ContDiffAt 𝕜 2 f x →
      iteratedDeriv 2 (g ∘ f) x = iteratedDeriv 2 g (f x) * deriv f x ^ 2 + deriv g (f x) * iteratedDeriv 2 f x
-- Mathlib.Algebra.Ring.NegOnePow
Int.negOnePow_add : ∀ (n₁ n₂ : ℤ), (n₁ + n₂).negOnePow = n₁.negOnePow * n₂.negOnePow
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.enrichedFunctorTypeEquivFunctor_symm_apply_obj : ∀ {C : Type u₁} [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] {D : Type u₂}
  [𝒟 : CategoryTheory.EnrichedCategory (Type v) D] (F : CategoryTheory.Functor C D) (X : C),
  (CategoryTheory.enrichedFunctorTypeEquivFunctor.symm F).obj X = F.obj X
-- Mathlib.Combinatorics.HalesJewett
/-- The common endpoint of the lines in the color-focused collection.  -/
Combinatorics.Line.ColorFocused.focus : {α : Type u_5} →
  {ι : Type u_6} → {κ : Type u_7} → {C : (ι → Option α) → κ} → Combinatorics.Line.ColorFocused C → ι → Option α
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.forget₂Mon.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.AddGrp.forget₂Mon C = CategoryTheory.inducedFunctor CategoryTheory.AddGrp.toAddMon
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker_domRestrict : ∀ {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₂}
  (p : Submodule R M) (f : M →ₛₗ[τ₁₂] M₂), (f.domRestrict p).ker = Submodule.comap p.subtype f.ker
-- Init.Omega.Int
Lean.Omega.Int.not_lt_of_le : ∀ {x y : ℤ}, y ≤ x → ¬x < y
-- Std.Data.ExtTreeMap.Lemmas
/-- Variant of `getElem_map` that holds without `LawfulEqCmp`.  -/
Std.ExtTreeMap.getElem_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → γ} {k : α} {h' : k ∈ Std.ExtTreeMap.map f t}, (Std.ExtTreeMap.map f t)[k] = f (t.getKey k ⋯) t[k]
-- Init.Data.Repr
Prod.reprTuple : {α : Type u_1} → {β : Type u_2} → [Repr α] → [ReprTuple β] → α × β → List Std.Format → List Std.Format
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_ofNat : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (g : σ → S₁) (n : ℕ) [inst_2 : n.AtLeastTwo], MvPolynomial.eval₂ f g (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Order.BooleanAlgebra.Defs
BooleanAlgebra.toDistribLattice : {α : Type u} → [self : BooleanAlgebra α] → DistribLattice α
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.nonAssocRing.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] [inst_1 : AddZeroClass M],
  AddMonoidAlgebra.nonAssocRing =
    { toNonUnitalNonAssocRing := AddMonoidAlgebra.nonUnitalNonAssocRing,
      toOne := AddMonoidAlgebra.nonAssocSemiring.toOne, one_mul := ⋯, mul_one := ⋯,
      toNatCast := AddMonoidAlgebra.nonAssocSemiring.toNatCast, natCast_zero := ⋯, natCast_succ := ⋯,
      intCast := fun z => AddMonoidAlgebra.single 0 ↑z, intCast_ofNat := ⋯, intCast_negSucc := ⋯ }
-- Mathlib.Topology.Algebra.Valued.WithVal
/-- Lift a `RingEquiv` to `WithVal`.  -/
WithVal.congr : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] →
      [inst_1 : Ring R] →
        (v : Valuation R Γ₀) →
          {S : Type u_3} →
            [inst_2 : Ring S] →
              {Λ₀ : Type u_4} →
                [inst_3 : LinearOrderedCommGroupWithZero Λ₀] → (w : Valuation S Λ₀) → R ≃+* S → WithVal v ≃+* WithVal w
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquivClass.isDedekindFiniteMonoid_iff : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : MulOne α] [inst_2 : MulOne β]
  [MulEquivClass F α β] [OneHomClass F α β] (f : F), IsDedekindFiniteMonoid α ↔ IsDedekindFiniteMonoid β
-- Mathlib.Analysis.InnerProductSpace.Continuous
Dense.eq_of_inner_left : ∀ {E : Type u_4} (𝕜 : Type u_7) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x y : E} {S : Set E}, Dense S → (∀ v ∈ S, inner 𝕜 x v = inner 𝕜 y v) → x = y
-- Mathlib.Analysis.Analytic.Constructions
/-- `(f x)⁻¹` is analytic away from `f x = 0`  -/
AnalyticAt.inv : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝}
  {x : E}, AnalyticAt 𝕜 f x → f x ≠ 0 → AnalyticAt 𝕜 f⁻¹ x
-- Lean.Data.SSet
Lean.SSet.instInhabited : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Inhabited (Lean.SSet α)
-- Mathlib.Geometry.Manifold.Instances.Real
Icc_chartedSpaceChartAt_of_le_top : ∀ {x y : ℝ} [hxy : Fact (x < y)] {z : ↑(Set.Icc x y)}, ↑z < y → chartAt (EuclideanHalfSpace 1) z = IccLeftChart x y
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.D₃.eq_1 : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : 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_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (j j' : ι₄)
  [inst_23 : HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄],
  HomologicalComplex.mapBifunctor₂₃.D₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j' =
    HomologicalComplex.mapBifunctor₂₃.mapBifunctor₂₃Desc c₁₂ fun i₁ i₂ i₃ x =>
      HomologicalComplex.mapBifunctor₂₃.d₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.factors_of_factors_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {P : CategoryTheory.Subobject Z} (f : X ⟶ Y)
  {g : Y ⟶ Z}, P.Factors g → P.Factors (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.GroupTheory.FiniteAbelian.Basic
AddSubgroup.isFiniteRelIndex_map_nsmulAddMonoidHom_of_fg : ∀ {A : Type u_1} [inst : AddCommGroup A] {B : AddSubgroup A},
  B.FG → ∀ {n : ℕ}, n ≠ 0 → (AddSubgroup.map (nsmulAddMonoidHom n) B).IsFiniteRelIndex B