mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Abelian.Projective.Extend
/-- The quasi-isomorphism `R.cochainComplex ⟶ (CochainComplex.singleFunctor C 0).obj X`
in `CochainComplex C ℤ` when `R` is a projective resolution of `X`.  -/
CategoryTheory.ProjectiveResolution.π' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        {X : C} →
          (R : CategoryTheory.ProjectiveResolution X) → R.cochainComplex ⟶ (CochainComplex.singleFunctor C 0).obj X
-- Init.Data.SInt.Basic
instAddInt8 : Add Int8
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.exists_of_le : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] {T S_1 : E →ₛₗ.[σ] F},
  T ≤ S_1 → ∀ (x : ↥T.domain), ∃ y, ↑x = ↑y ∧ ↑T x = ↑S_1 y
-- Std.Time.Format.Modifier
/-- Hour and minute with colon (e.g., "+01:30")
 -/
Std.Time.OffsetX.hourMinuteColon : Std.Time.OffsetX
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanFinrank_map_eq_of_injective : ∀ {R : Type u_1} {S : Type u_2} {M : Type u} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S}
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] {L : Type v} [inst_4 : AddCommMonoid L] [inst_5 : Module S L]
  [inst_6 : RingHomSurjective σ] (f : M →ₛₗ[σ] L),
  Function.Injective ⇑f → ∀ {p : Submodule R M}, (Submodule.map f p).spanFinrank = p.spanFinrank
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.of_subsingleton : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [Subsingleton α],
  MeasureTheory.NullMeasurableSet s μ
-- Mathlib.Order.Cover
WCovBy.covBy_of_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ⩿ b → a < b → a ⋖ b
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Name.beq.eq_4 : ∀ (x x_1 : Lean.Name),
  (x = Lean.Name.anonymous → x_1 = Lean.Name.anonymous → False) →
    (∀ (p₁ : Lean.Name) (s₁ : String) (p₂ : Lean.Name) (s₂ : String), x = p₁.str s₁ → x_1 = p₂.str s₂ → False) →
      (∀ (p₁ : Lean.Name) (n₁ : ℕ) (p₂ : Lean.Name) (n₂ : ℕ), x = p₁.num n₁ → x_1 = p₂.num n₂ → False) →
        x.beq x_1 = false
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.mem_range_scalar_iff_commute_transvectionStruct : ∀ {n : Type u_1} {R : Type u₂} [inst : DecidableEq n] [inst_1 : CommRing R] [inst_2 : Fintype n] {M : Matrix n n R},
  M ∈ Set.range ⇑(Matrix.scalar n) ↔ ∀ (t : Matrix.TransvectionStruct n R), Commute t.toMatrix M
-- Init.Data.Fin.Basic
Fin.coeToNat : {n : ℕ} → CoeOut (Fin n) ℕ
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instMonoid : {α : Type u_1} → [Monoid α] → Monoid αᵐᵒᵖ
-- Init.Data.Int.Order
Int.negSucc_not_pos : ∀ (n : ℕ), 0 < Int.negSucc n ↔ False
-- Mathlib.Data.ENat.Basic
ENat.natCast_le_natCast : ∀ {n m : ℕ}, ↑n ≤ ↑m ↔ n ≤ m
-- Mathlib.Order.UpperLower.Prod
LowerSet.prod_inf_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (s₁ s₂ : LowerSet α) (t₁ t₂ : LowerSet β),
  s₁ ×ˢ t₁ ⊓ s₂ ×ˢ t₂ = (s₁ ⊓ s₂) ×ˢ (t₁ ⊓ t₂)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.minKeyD_modify_eq_minKeyD : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [Std.LawfulEqOrd α],
  t.WF →
    ∀ {k : α} {f : β → β} {fallback : α},
      (Std.DTreeMap.Internal.Impl.Const.modify k f t).minKeyD fallback = t.minKeyD fallback
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The left map in the right unitality square.
 -/
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.leftMapᵣ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          (F : CategoryTheory.Functor C D) → F.comp (CategoryTheory.MonoidalCategory.tensorUnitRight D) ⟶ F
-- Mathlib.Topology.Algebra.Module.PerfectPairing
/-- **Alias** of `LinearMap.IsContPerfPair.continuous_uncurry`. -/
LinearMap.continuous_uncurry_of_isContPerfPair : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {inst : CommRing R} {inst_1 : TopologicalSpace R}
  {inst_2 : AddCommGroup M} {inst_3 : Module R M} {inst_4 : TopologicalSpace M} {inst_5 : AddCommGroup N}
  {inst_6 : Module R N} {inst_7 : TopologicalSpace N} (p : M →ₗ[R] N →ₗ[R] R) [self : p.IsContPerfPair],
  Continuous fun x =>
    match x with
    | (x, y) => (p x) y
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.coconeOfLE_ι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : PartialOrder J] {j : J}
  (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {i : J} (hi : i ≤ j) (i_1 : ↑(Set.Iio i)),
  (CategoryTheory.SmallObject.coconeOfLE F hi).ι.app i_1 = F.map (CategoryTheory.homOfLE ⋯)
-- Mathlib.NumberTheory.LSeries.SumCoeff
_private.Mathlib.NumberTheory.LSeries.SumCoeff.0.LSeriesSummable_of_sum_norm_bigO_aux : ∀ {f : ℕ → ℂ} {r : ℝ} {s : ℂ},
  f 0 = 0 →
    ((fun n => ∑ k ∈ Finset.Icc 1 n, ‖f k‖) =O[Filter.atTop] fun n => ↑n ^ r) → 0 ≤ r → r < s.re → LSeriesSummable f s
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
_private.Mathlib.LinearAlgebra.Matrix.SemiringInverse.0.Matrix.adjp_none_right : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (s : ℤˣ)
  (A : Matrix (Option n) (Option n) R) (i : Option n),
  Matrix.adjp s A i none =
    Matrix.detp (Equiv.Perm.sign (Equiv.swap none i) * s) (A.submatrix some (⇑(Equiv.swap none i) ∘ some))
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coeAddMonoidHom_apply : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddZeroClass α] (s : Finset α), Finset.coeAddMonoidHom s = ↑s
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
/-- Construct a pseudofunctor from a lax functor whose `mapId` and `mapComp` are isomorphisms.  -/
CategoryTheory.Pseudofunctor.mkOfLax : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (F : CategoryTheory.LaxFunctor B C) → F.PseudoCore → CategoryTheory.Pseudofunctor B C
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Any type satisfying `RingHomClass` can be cast into `RingHom` via `RingHomClass.toRingHom`.  -/
instCoeTCRingHom : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        {x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → [RingHomClass F α β] → CoeTC F (α →+* β)
-- Mathlib.Algebra.Star.SelfAdjoint
IsStarNormal.smul : ∀ {R : Type u_3} {A : Type u_4} [inst : SMul R A] [inst_1 : Star R] [inst_2 : Star A] [inst_3 : Mul A] [StarModule R A]
  [SMulCommClass R A A] [IsScalarTower R A A] (r : R) (a : A) [ha : IsStarNormal a], IsStarNormal (r • a)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Sized.rotateR : ∀ {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α}, l.Sized → r.Sized → (l.rotateR x r).Sized
-- Lean.Meta.Sym.Pattern
Lean.Meta.Sym.MatchUnifyResult.mk.injEq : ∀ (us : List Lean.Level) (args : Array Lean.Expr) (unresolvedInsts : Array Lean.MVarId) (us_1 : List Lean.Level)
  (args_1 : Array Lean.Expr) (unresolvedInsts_1 : Array Lean.MVarId),
  ({ us := us, args := args, unresolvedInsts := unresolvedInsts } =
      { us := us_1, args := args_1, unresolvedInsts := unresolvedInsts_1 }) =
    (us = us_1 ∧ args = args_1 ∧ unresolvedInsts = unresolvedInsts_1)
-- Init.Data.Vector.Basic
/-- Count the number of elements of a vector that satisfy the predicate `p`.  -/
Vector.countP : {α : Type u_1} → {n : ℕ} → (α → Bool) → Vector α n → ℕ
-- Mathlib.SetTheory.ZFC.Ordinal
/-- An ordinal is a transitive set of ordinals.  -/
ZFSet.isOrdinal_iff_forall_mem_isOrdinal : ∀ {x : ZFSet.{u}}, x.IsOrdinal ↔ x.IsTransitive ∧ ∀ y ∈ x, y.IsOrdinal
-- Lean.LibrarySuggestions.Basic
/-- Premises from a module whose name has one of the following components are not retrieved.

Use `run_cmd modifyEnv fun env => moduleDenyListExt.addEntry env module` to add a module to the deny list.
 -/
Lean.LibrarySuggestions.moduleDenyListExt : Lean.SimplePersistentEnvExtension String (List String)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.equivalenceOfIsTerminal_counitIso : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsTerminal X),
  (CategoryTheory.Over.equivalenceOfIsTerminal hX).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        CategoryTheory.Iso.refl
          (({ obj := fun Y => CategoryTheory.Over.mk (hX.from Y), map := fun {X_1 Y} f => CategoryTheory.Over.homMk f ⋯,
                    map_id := ⋯, map_comp := ⋯ }.comp
                (CategoryTheory.Over.forget X)).obj
            x))
      ⋯
-- Mathlib.RingTheory.ChainOfDivisors
/-- The second element of a chain is irreducible.  -/
DivisorChain.second_of_chain_is_irreducible : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {q : Associates M} {n : ℕ},
  n ≠ 0 →
    ∀ {c : Fin (n + 1) → Associates M},
      StrictMono c → (∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i) → q ≠ 0 → Irreducible (c 1)
-- Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
/-- The coefficient of a monomial in a product `f * g` that can be reached in at most one way
as a product of monomials in the supports of `f` and `g` is a product.  -/
AddMonoidAlgebra.coeff_mul_add_of_uniqueAdd : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [inst_1 : Add A] {f g : AddMonoidAlgebra R A} {a0 b0 : A},
  UniqueAdd f.coeff.support g.coeff.support a0 b0 → (f * g).coeff (a0 + b0) = f.coeff a0 * g.coeff b0
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- Given a `k`-module `A` with a compatible `DistribMulAction` of `G`, and a function
`f : G → A` satisfying the 1-coboundary condition, produces a 1-coboundary for the representation
on `A` induced by the `DistribMulAction`.  -/
groupCohomology.coboundariesOfIsCoboundary₁ : {k G A : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : AddCommGroup A] →
        [inst_3 : Module k A] →
          [inst_4 : DistribMulAction G A] →
            [inst_5 : SMulCommClass G k A] →
              {f : G → A} →
                groupCohomology.IsCoboundary₁ f → ↥(groupCohomology.coboundaries₁ (Rep.ofDistribMulAction k G A))
-- Mathlib.AlgebraicTopology.SingularHomology.Basic
/-- The adjunction `Hom(Cⁿ(-, X), F) ≃ Hom(X, F(Δ[n]))` for `X : C` and `F : Top ⥤ C`.  -/
AlgebraicTopology.singularChainComplexFunctorAdjunction : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        (n : ℕ) →
          (CategoryTheory.Functor.postcompose₂.obj (HomologicalComplex.eval C (ComplexShape.down ℕ) n)).obj
              (AlgebraicTopology.singularChainComplexFunctor C) ⊣
            (CategoryTheory.evaluation TopCat C).obj (SimplexCategory.toTop.{w}.obj { len := n })
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
_private.Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas.0.Nat.nthRoot.always_exists : ∀ (n a : ℕ), ∃ c, c ^ (n + 1) ≤ a ∧ a < (c + 1) ^ (n + 1)
-- Batteries.Data.Float.Lemmas
Float32.toBits_inj : ∀ {f f' : Float32}, f.toBits = f'.toBits ↔ f = f'
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyD.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k fallback : α) (size : ℕ) (k' : α) (v : β k')
  (l r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k' v l r).getKeyD k fallback =
    match compare k k' with
    | Ordering.lt => l.getKeyD k fallback
    | Ordering.gt => r.getKeyD k fallback
    | Ordering.eq => k'
-- Mathlib.Algebra.Group.TypeTags.Basic
toAdd_zpow : ∀ {α : Type u} [inst : SubNegMonoid α] (a : Multiplicative α) (z : ℤ),
  Multiplicative.toAdd (a ^ z) = z • Multiplicative.toAdd a
-- Batteries.Data.List.ArrayMap
List.toArrayMap_eq_toArray_map : ∀ {α : Type u} {β : Type v} (l : List α) (f : α → β), l.toArrayMap f = (List.map f l).toArray
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.mk : {X : Type u_2} →
  [inst : TopologicalSpace X] →
    {P : Set X → Set X → Prop} →
      (C U : Set X) →
        P C U →
          IsClosed C →
            IsOpen U →
              C ⊆ U →
                (∀ {c u : Set X},
                    IsClosed c →
                      P c u → IsOpen u → c ⊆ u → ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ P c v ∧ P (closure v) u) →
                  Urysohns.CU P
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.OplaxTrans.associator_hom_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H I : CategoryTheory.LaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) (a : B),
  (CategoryTheory.Lax.OplaxTrans.associator η θ ι).hom.as.app a =
    (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom
-- Mathlib.CategoryTheory.Monoidal.Center
/-- The underlying morphism between the first components of the objects involved  -/
CategoryTheory.Center.Hom.f : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → {X Y : CategoryTheory.Center C} → X.Hom Y → (X.fst ⟶ Y.fst)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.SupportsStmt.eq_3 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (S : Finset Λ) (a : Γ → σ → σ) (q : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1.SupportsStmt S (Turing.TM1.Stmt.load a q) = Turing.TM1.SupportsStmt S q
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.isIso_leftHomologyMap_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.IsIso φ] [inst_3 : S₁.HasLeftHomology]
  [inst_4 : S₂.HasLeftHomology], CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftHomologyMap φ)
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.unop_inj : ∀ {G : Type u_2} [inst : AddGroup G] {S T : AddSubgroup Gᵃᵒᵖ}, S.unop = T.unop ↔ S = T
-- Mathlib.Topology.UnitInterval
/-- Any open cover of the unit interval can be refined to a finite partition into subintervals.  -/
exists_monotone_Icc_subset_open_cover_unitInterval : ∀ {ι : Sort u_1} {c : ι → Set ↑unitInterval},
  (∀ (i : ι), IsOpen (c i)) →
    Set.univ ⊆ ⋃ i, c i →
      ∃ t, t 0 = 0 ∧ Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧ ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ c i
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.IsPlot.dSmooth_comp : ∀ {X : Type u_1} {Y : Type u_2} [inst : DiffeologicalSpace X] [inst_1 : DiffeologicalSpace Y] {n : ℕ}
  {p : EuclideanSpace ℝ (Fin n) → X} {f : X → Y}, Diffeology.IsPlot p → Diffeology.DSmooth f → Diffeology.IsPlot (f ∘ p)
-- Mathlib.Algebra.Polynomial.CoeffList
Polynomial.length_coeffList_eq_withBotSucc_degree : ∀ {R : Type u_1} [inst : Semiring R] (P : Polynomial R), P.coeffList.length = P.degree.succ
-- Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
SSet.prodStdSimplex.strictMono_orderHomOfSimplex_iff : ∀ {p q n : ℕ}
  (x :
    (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
          (SSet.stdSimplex.obj { len := q })).obj
      (Opposite.op { len := n }))
  {m : ℕ} (hm : p + q = m),
  StrictMono ⇑(SSet.prodStdSimplex.orderHomOfSimplex x hm) ↔ StrictMono ⇑(SSet.prodStdSimplex.objEquiv x)
-- Mathlib.CategoryTheory.Functor.OfSequence
CategoryTheory.Functor.ofOpSequence_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : ℕ → C} (f : (n : ℕ) → X (n + 1) ⟶ X n) (X_1 : ℕᵒᵖ),
  (CategoryTheory.Functor.ofOpSequence f).obj X_1 = X (Opposite.unop X_1)
-- Mathlib.Topology.MetricSpace.Infsep
Set.Finite.einfsep_exists_of_nontrivial : ∀ {α : Type u_1} [inst : EDist α] {s : Set α}, s.Finite → s.Nontrivial → ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y
-- Mathlib.Topology.ContinuousMap.T0Sierpinski
/-- The continuous map from `X` to the product of copies of the Sierpinski space, (one copy for each
open subset `u` of `X`). The `u` coordinate of `productOfMemOpens x` is given by `x ∈ u`.
 -/
TopologicalSpace.productOfMemOpens : (X : Type u_1) → [inst : TopologicalSpace X] → C(X, TopologicalSpace.Opens X → Prop)
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
tsum_int_eq_zero_add_two_mul_tsum_pnat : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G] [CompleteSpace G] [T2Space G]
  {f : ℤ → G}, Function.Even f → Summable f → ∑' (n : ℤ), f n = f 0 + 2 • ∑' (n : ℕ+), f ↑↑n
-- Init.Data.SInt.Lemmas
Int8.succ_mul : ∀ {a b : Int8}, (a + 1) * b = a * b + b
-- Mathlib.Algebra.Group.Action.Option
Option.VAdd.eq_1 : ∀ {M : Type u_1} {α : Type u_3} [inst : VAdd M α], Option.VAdd = { vadd := fun a => Option.map fun x => a +ᵥ x }
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.mulEquivOfLocalizations_right_inv_apply : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {k : S.LocalizationMap P} {x : M},
  (f.ofMulEquivOfLocalizations (f.mulEquivOfLocalizations k)) x = k x
-- Mathlib.Data.WSeq.Defs
Stream'.WSeq.IsFinite.mk : ∀ {α : Type u} {s : Stream'.WSeq α}, s.toList.Terminates → s.IsFinite
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.ext_iff : ∀ {M N : SemiNormedGrp₁} {f₁ f₂ : M ⟶ N},
  f₁ = f₂ ↔ ∀ (x : M.carrier), ↑(SemiNormedGrp₁.Hom.hom f₁) x = ↑(SemiNormedGrp₁.Hom.hom f₂) x
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.zero_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β] (x : α),
  0 x = 0
-- Init.Data.SInt.Lemmas
Int8.toInt32_mod : ∀ (a b : Int8), (a % b).toInt32 = a.toInt32 % b.toInt32
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.instSetLike.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M], Submonoid.instSetLike = { coe := fun s => s.carrier, coe_injective := ⋯ }
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.dmuld : ∀ {d : ℤ}, Zsqrtd.sqrtd * Zsqrtd.sqrtd = ↑d
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Cardinal.mk_add_le : ∀ {M : Type u_2} [inst : Add M] {s t : Set M}, Cardinal.mk ↑(s + t) ≤ Cardinal.mk ↑s * Cardinal.mk ↑t
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.Quotient.map_cast : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X}
  (p : Path.Homotopic.Quotient x y) {x' y' : X} {hx : x' = x} {hy : y' = y} {f : C(X, Y)},
  (p.cast hx hy).map f = (p.map f).cast ⋯ ⋯
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.opNorm_neg : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂), ‖-f‖ = ‖f‖
-- Init.Data.UInt.Lemmas
UInt32.toUInt64_ofFin : ∀ {n : Fin UInt32.size}, (UInt32.ofFin n).toUInt64 = UInt64.ofNatLT ↑n ⋯
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement'.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (H K : AddSubgroup G), H.IsComplement' K = AddSubgroup.IsComplement ↑H ↑K
-- Mathlib.RingTheory.Ideal.Operations
Ideal.radical.eq_1 : ∀ {R : Type u} [inst : CommSemiring R] (I : Ideal R),
  I.radical = { carrier := {r | ∃ n, r ^ n ∈ I}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
-- Init.Data.SInt.Bitwise
Int8.not_or_self : ∀ {a : Int8}, ~~~a ||| a = -1
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Constructor for morphisms in `ComposableArrows C 1`.  -/
CategoryTheory.ComposableArrows.homMk₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {F G : CategoryTheory.ComposableArrows C 1} →
      (left :
          F.obj' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4 ⟶
            G.obj' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4) →
        (right :
            F.obj' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5 ⟶
              G.obj' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5) →
          autoParam
              (CategoryTheory.CategoryStruct.comp
                  (F.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4
                    CategoryTheory.ComposableArrows.homMk₁._proof_5)
                  right =
                CategoryTheory.CategoryStruct.comp left
                  (G.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4
                    CategoryTheory.ComposableArrows.homMk₁._proof_5))
              CategoryTheory.ComposableArrows.homMk₁._auto_1 →
            (F ⟶ G)
-- Mathlib.Algebra.Symmetrized
SymAlg.instIsEmpty : ∀ {α : Type u_1} [IsEmpty α], IsEmpty αˢʸᵐ
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.span_weight_isNonZero_eq_top : ∀ (K : Type u_2) (L : Type u_3) [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] (H : LieSubalgebra K L) [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L],
  Submodule.span K (LieModule.Weight.toLinear K (↥H) L '' {α | α.IsNonZero}) = ⊤
-- Mathlib.Topology.EMetricSpace.Defs
/-- Creating a uniform space from an extended distance. We assume that
there is a preexisting topology, for which the neighborhoods can be expressed using the distance,
and we make sure that the uniform space structure we construct has a topology which is defeq
to the original one.  -/
uniformSpaceOfEDistOfHasBasis : {α : Type u} →
  [inst : TopologicalSpace α] →
    (edist : α → α → ENNReal) →
      (∀ (x : α), edist x x = 0) →
        (∀ (x y : α), edist x y = edist y x) →
          (∀ (x y z : α), edist x z ≤ edist x y + edist y z) →
            (∀ (x : α), (nhds x).HasBasis (fun c => 0 < c) fun c => {y | edist x y < c}) → UniformSpace α
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
ClosedSubmodule.orthogonal_injective : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [CompleteSpace E], Function.Injective fun K => Kᗮ
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
FreeAbelianGroup.card_support_eq_zero : ∀ {X : Type u_1} {a : FreeAbelianGroup X}, a.support.card = 0 ↔ a = 0
-- Mathlib.Order.Partition.Basic
Partition.le_def : ∀ {α : Type u_1} {s : α} [inst : CompleteLattice α] {P Q : Partition s}, P ≤ Q ↔ ∀ x ∈ P, ∃ y ∈ Q, x ≤ y
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.alter.match_1.splitter : {α : Type u_3} →
  {β : α → Type u_1} →
    (a : α) →
      (motive : Option (β a) → Sort u_2) →
        (x : Option (β a)) → (Unit → motive none) → ((b : β a) → motive (some b)) → motive x
-- Lean.Data.JsonRpc
Lean.IO.FS.Stream.writeMessage : IO.FS.Stream → Lean.JsonRpc.Message → IO Unit
-- Init.Data.List.Lemmas
List.all_append : ∀ {α : Type u_1} {f : α → Bool} {xs ys : List α}, (xs ++ ys).all f = (xs.all f && ys.all f)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Cell.ofOption.match_1.eq_1 : ∀ {α : Type u_3} {β : α → Type u_1} (k : α) (motive : Option (β k) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (v : β k) → motive (some v)),
  (match none with
    | none => h_1 ()
    | some v => h_2 v) =
    h_1 ()
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
/-- The product cone in `Cat` is indeed a product.  -/
CategoryTheory.Cat.isLimitProdCone : (X Y : CategoryTheory.Cat) → CategoryTheory.Limits.IsLimit (X.prodCone Y)
-- Lean.Meta.ReduceEval
Lean.Meta.instReduceEvalList : {α : Type} → [Lean.Meta.ReduceEval α] → Lean.Meta.ReduceEval (List α)
-- Mathlib.Data.PNat.Factors
PrimeMultiset.prod_dvd_iff : ∀ {u v : PrimeMultiset}, u.prod ∣ v.prod ↔ u ≤ v
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CongrTable : Lean.Meta.Grind.ENodeMap → Type
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isCoboundary₂_of_mem_coboundaries₂ : ∀ {k G A : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup A] [inst_3 : Module k A]
  [inst_4 : DistribMulAction G A] [inst_5 : SMulCommClass G k A],
  ∀ f ∈ groupCohomology.coboundaries₂ (Rep.ofDistribMulAction k G A), groupCohomology.IsCoboundary₂ f
-- Init.Data.Array.Lemmas
Array.mem_iff_append : ∀ {α : Type u_1} {a : α} {xs : Array α}, a ∈ xs ↔ ∃ as bs, xs = as.push a ++ bs