mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Lean.Meta.CongrTheorems
Lean.Meta.instFastSubsingletonDecidable : ∀ {p : Prop}, Lean.Meta.FastSubsingleton (Decidable p)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_right_le_size_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₂.size ≤ (m₁ ∪ m₂).size
-- Aesop.BaseM
/-- The rule pattern cache.  -/
Aesop.BaseM.State.rulePatternCache : Aesop.BaseM.State → Aesop.RulePatternCache
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.USquash.inflate_deflate : ∀ {α : Type v} {x : Std.Internal.Small α} {x_1 : α}, (Std.Internal.USquash.deflate x_1).inflate = x_1
-- Mathlib.Algebra.Module.Equiv.Defs
/-- The additive equivalence of types underlying a linear equivalence.  -/
LinearEquiv.toAddEquiv : {R : Type u_14} →
  {S : Type u_15} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {σ : R →+* S} →
          {σ' : S →+* R} →
            [inst_2 : RingHomInvPair σ σ'] →
              [inst_3 : RingHomInvPair σ' σ] →
                {M : Type u_16} →
                  {M₂ : Type u_17} →
                    [inst_4 : AddCommMonoid M] →
                      [inst_5 : AddCommMonoid M₂] →
                        [inst_6 : Module R M] → [inst_7 : Module S M₂] → (M ≃ₛₗ[σ] M₂) → M ≃+ M₂
-- Batteries.Data.List.Lemmas
List.mem_diff_of_mem : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l₁ l₂ : List α}, a ∈ l₁ → a ∉ l₂ → a ∈ l₁.diff l₂
-- Mathlib.Topology.ContinuousMap.Star
/-- `ContinuousMap.compStarAlgHom` is functorial.  -/
ContinuousMap.compStarAlgHom_comp : ∀ (X : Type u_1) {𝕜 : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [inst : TopologicalSpace X]
  [inst_1 : CommSemiring 𝕜] [inst_2 : TopologicalSpace A] [inst_3 : Semiring A] [inst_4 : IsTopologicalSemiring A]
  [inst_5 : Star A] [inst_6 : ContinuousStar A] [inst_7 : Algebra 𝕜 A] [inst_8 : TopologicalSpace B]
  [inst_9 : Semiring B] [inst_10 : IsTopologicalSemiring B] [inst_11 : Star B] [inst_12 : ContinuousStar B]
  [inst_13 : Algebra 𝕜 B] [inst_14 : TopologicalSpace C] [inst_15 : Semiring C] [inst_16 : IsTopologicalSemiring C]
  [inst_17 : Star C] [inst_18 : ContinuousStar C] [inst_19 : Algebra 𝕜 C] (φ : A →⋆ₐ[𝕜] B) (ψ : B →⋆ₐ[𝕜] C)
  (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ),
  ContinuousMap.compStarAlgHom X (ψ.comp φ) ⋯ =
    (ContinuousMap.compStarAlgHom X ψ hψ).comp (ContinuousMap.compStarAlgHom X φ hφ)
-- Mathlib.GroupTheory.Nilpotent
Subgroup.upperCentralSeriesAux.match_1.congr_eq_2 : ∀ (motive : ℕ → Sort u_1) (x : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ) (n : ℕ),
  x = n.succ →
    (match x with
      | 0 => h_1 ()
      | n.succ => h_2 n) ≍
      h_2 n
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegralFun_trans_of_lt_half : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b c : E} {t : ℝ}
  (ω : E → E →L[𝕜] F) (γab : Path a b) (γbc : Path b c),
  t < 1 / 2 → curveIntegralFun ω (γab.trans γbc) t = 2 • curveIntegralFun ω γab (2 * t)
-- Mathlib.Order.RelIso.Basic
RelHom.comp_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (g : s →r t)
  (f : r →r s) (x : α), (g.comp f) x = g (f x)
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.swapLeft.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ), κ.swapLeft = κ.comap Prod.swap ⋯
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.zero.eq_1 : ∀ {α : Type u_2} [inst : Zero α], Finset.zero = { zero := {0} }
-- Mathlib.Logic.Equiv.Defs
/-- A version of `Equiv.arrowCongr` in `Type`, rather than `Sort`.

The `equiv_rw` tactic is not able to use the default `Sort` level `Equiv.arrowCongr`,
because Lean's universe rules will not unify `?l_1` with `imax (1 ?m_1)`.
 -/
Equiv.arrowCongr' : {α₁ : Type u_1} → {β₁ : Type u_2} → {α₂ : Type u_3} → {β₂ : Type u_4} → α₁ ≃ α₂ → β₁ ≃ β₂ → (α₁ → β₁) ≃ (α₂ → β₂)
-- Std.Http.Test.Helpers
/-- Assert the response is byte-for-byte equal to `expected`.
Use sparingly — prefer `assertStatus` + `assertContains` for 200 responses.
 -/
Std.Http.Internal.Test.assertExact : ByteArray → String → IO Unit
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput.rhs : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig → aig.Ref
-- Mathlib.Topology.Order.NhdsSet
nhdsSet_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a : α},
  nhdsSet (Set.Ici a) = nhds a ⊔ Filter.principal (Set.Ioi a)
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.isPositive_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {T : ι → E →ₗ[𝕜] E} (s : Finset ι), (∀ i ∈ s, (T i).IsPositive) → (∑ i ∈ s, T i).IsPositive
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.weierstrassP_coe : ∀ (L : PeriodPair) (l : ↥L.lattice), L.weierstrassP ↑l = 0
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Build a new pseudometric space from an old one where the bundled topological structure is
provably (but typically non-definitionaly) equal to some given topological structure.
See Note [forgetful inheritance].
See Note [reducible non-instances].
 -/
PseudoMetricSpace.replaceTopology : {γ : Type u_3} →
  [U : TopologicalSpace γ] →
    (m : PseudoMetricSpace γ) → U = PseudoMetricSpace.toUniformSpace.toTopologicalSpace → PseudoMetricSpace γ
-- Init.Data.Fin.Lemmas
Fin.castSucc_fin_succ : ∀ (n : ℕ) (j : Fin n), j.succ.castSucc = j.castSucc.succ
-- Mathlib.Order.SetNotation
/-- Notation for `Set.iInter`. Indexed intersection of a family of sets  -/
Set.«term⋂_,_» : Lean.ParserDescr
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.find?_insert : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.TransCmp cmp] (t : RBTree.RBSet α cmp) (v v' : α),
  (t.insert v).find? v' = if cmp v' v = Ordering.eq then some v else t.find? v'
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Zipper.step.match_3.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Lean.PersistentHashMap.Zipper α β → Sort u_3) →
      (x : Lean.PersistentHashMap.Zipper α β) →
        (Unit → motive Lean.PersistentHashMap.Zipper.done) →
          ((es : Subarray (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
              (z' : Lean.PersistentHashMap.Zipper α β) → motive (Lean.PersistentHashMap.Zipper.consEntries es z')) →
            ((keys : Subarray α) →
                (vals : Subarray β) →
                  (hsz : Std.Slice.size keys = Std.Slice.size vals) →
                    (z' : Lean.PersistentHashMap.Zipper α β) →
                      motive (Lean.PersistentHashMap.Zipper.consCollision keys vals hsz z')) →
              motive x
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithTop.instCompleteLinearOrder : {α : Type u_1} → [ConditionallyCompleteLinearOrderBot α] → CompleteLinearOrder (WithTop α)
-- Aesop.Tracing
Aesop.TraceOption.mk.injEq : ∀ (traceClass : Lean.Name) (option : Lean.Option Bool) (traceClass_1 : Lean.Name) (option_1 : Lean.Option Bool),
  ({ traceClass := traceClass, option := option } = { traceClass := traceClass_1, option := option_1 }) =
    (traceClass = traceClass_1 ∧ option = option_1)
-- Mathlib.Algebra.Order.ToIntervalMod
iUnion_Icc_add_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] [Archimedean α] {p : α},
  0 < p → ∀ (a : α), ⋃ n, Set.Icc (a + n • p) (a + (n + 1) • p) = Set.univ
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.prime_of_normalized_factor : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {a : α}, ∀ x ∈ UniqueFactorizationMonoid.normalizedFactors a, Prime x
-- Lean.Meta.CongrTheorems
Lean.Meta.CongrTheorem : Type
-- Mathlib.Tactic.Convert
_private.Mathlib.Tactic.Convert.0.Convert.elabExpensiveConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Convert.ExpensiveConfig
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumUniformlyOn.summableUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α], HasSumUniformlyOn f g s → SummableUniformlyOn f s
-- Std.Http.Data.URI.Encoding
/-- Creates an encoded fragment component from raw bytes, panicking on invalid encoding.
 -/
Std.Http.URI.EncodedFragment.ofByteArray! : ByteArray → Std.Http.URI.EncodedFragment
-- Mathlib.Order.UpperLower.Closure
lowerClosure_empty : ∀ {α : Type u_1} [inst : Preorder α], lowerClosure ∅ = ⊥
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mk'_eq_of_eq' : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) {a₁ b₁ : M} {a₂ b₂ : ↥S}, b₁ * ↑a₂ = a₁ * ↑b₂ → f.mk' a₁ a₂ = f.mk' b₁ b₂
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.instAddActionOfVAddCommClass : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {X : Type u_4} →
        {Y : Type u_5} →
          {σ : M → N} →
            [inst : VAdd M X] →
              [inst_1 : VAdd N Y] →
                [inst_2 : AddMonoid R] → [inst_3 : AddAction R Y] → [VAddCommClass N R Y] → AddAction R (X →ₑ[σ] Y)
-- Mathlib.Analysis.Calculus.Deriv.Pow
HasDerivWithinAt.fun_pow' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸]
  {f : 𝕜 → 𝔸} {f' : 𝔸} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' s x →
    ∀ (n : ℕ), HasDerivWithinAt (fun x => f x ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) s x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey?_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.DTreeMap.Const.ofList l cmp).getKey? k' = some k
-- Mathlib.Tactic.CongrExclamation
/-- For passes that synthesize a congruence lemma using one side of the equality,
we run the pass both for the left-hand side and the right-hand side. If `preferLHS` is `true`
then we start with the left-hand side.

This can be used to control which side's definitions are expanded when applying the
congruence lemma (if `preferLHS = true` then the RHS can be expanded).  -/
Congr!.Config.preferLHS : Congr!.Config → Bool
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.map_injective_iff : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁),
  Function.Injective ⇑(MvPolynomial.map f) ↔ Function.Injective ⇑f
-- Mathlib.ModelTheory.Basic
/-- Composition of first-order homomorphisms.  -/
FirstOrder.Language.Hom.comp : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] → {P : Type u_1} → [inst_2 : L.Structure P] → L.Hom N P → L.Hom M N → L.Hom M P
-- Std.Http.Protocol.H1.Parser
/-- Parses a status line and returns the status code plus recognized HTTP version when available.
Consumes and discards the reason phrase.

status-line = HTTP-version SP status-code SP [ reason-phrase ] CRLF
 -/
Std.Http.Protocol.H1.parseStatusLineRawVersion : Std.Http.Protocol.H1.Config → Std.Internal.Parsec.ByteArray.Parser (Std.Http.Status × Option Std.Http.Version)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonTextDocumentClientCapabilities.fromJson : Lean.Json → Except String Lean.Lsp.TextDocumentClientCapabilities
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.cyclesMap_comp_isoCycles₁_hom_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (x : ↑(groupHomology.cycles A 1)),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.isoCycles₁ B).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.cyclesMap f φ 1)) x) =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.mapCycles₁ f φ))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.isoCycles₁ A).hom) x)
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.elimMVarDeps : Array Lean.Expr → Lean.Expr → Lean.MetavarContext.MkBinding.M Lean.Expr
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_obj_obj_obj : ∀ {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.Precoherent C] (A : Type u_3)
  [inst_3 : CategoryTheory.Category.{v_3, u_3} A] (e : C ≌ D)
  (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A) (X_1 : Dᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongrPrecoherent A e).functor.obj X).obj.obj X_1 =
    X.obj.obj (Opposite.op (e.inverse.obj (Opposite.unop X_1)))
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.HasFiniteRange.comp_left : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [inst : Semiring K] [inst_1 : AddCommMonoid V]
  [inst_2 : Module K V] [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂] [inst_5 : AddCommMonoid V₃]
  [inst_6 : Module K V₃] {u : V →ₗ[K] V₂}, u.HasFiniteRange → ∀ (v : V₂ →ₗ[K] V₃), (v ∘ₗ u).HasFiniteRange
-- Mathlib.Algebra.Field.IsField
/-- Transferring from `IsField` to `Semifield`.  -/
IsField.toSemifield : {R : Type u} → [inst : Semiring R] → IsField R → Semifield R
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- An `Equiv` between representations could be built from a `LinearEquiv` and an assumption
proving the `G`-equivariance.  -/
ContRepresentation.Equiv.mk : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            {ρ : ContRepresentation R G V} →
                              {σ : ContRepresentation R G W} →
                                (e : V ≃L[R] W) → (∀ (g : G), ↑e ∘SL ρ g = σ g ∘SL ↑e) → ρ.Equiv σ
-- Mathlib.Topology.Semicontinuity.Defs
/-- A function `f : α → Set β` is lower hemicontinuous on a set `s` if, whenever `x ∈ s` and `t` is
an open set intersecting `f x`, then `t` also intersects `f x'` for all `x'` sufficiently close to
`x` within `s`.  -/
LowerHemicontinuousOn : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → [TopologicalSpace β] → (α → Set β) → Set α → Prop
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.map_ofNat_star : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : NonAssocSemiring α] [inst_2 : StarRing α] (d : ℕ)
  [inst_3 : d.AtLeastTwo], (OfNat.ofNat d).map star = OfNat.ofNat d
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.mapM : {α : Type u} →
  {β : Type v} →
    {σ : Type u} →
      {m : Type u → Type w} →
        [Monad m] →
          {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α β → (β → m σ) → m (Lean.PersistentHashMap α σ)
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
Matrix.GeneralLinearGroup.map_center_le : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] {S : Type u_3}
  [inst_3 : CommRing S] (f : R →+* S),
  Subgroup.center (GL n R) ≤ Subgroup.comap (Matrix.GeneralLinearGroup.map f) (Subgroup.center (GL n S))
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.isIso_ιTruncLE_iff : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncLE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C], CategoryTheory.IsIso (K.ιTruncLE e) ↔ K.IsStrictlySupported e
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.MapFactorizationData.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {W₁ W₂ : CategoryTheory.MorphismProperty C} {X Y : C}
  {f : X ⟶ Y} {Z : C} {i : X ⟶ Z} {p : Z ⟶ Y}
  {fac :
    autoParam (CategoryTheory.CategoryStruct.comp i p = f)
      CategoryTheory.MorphismProperty.MapFactorizationData.fac._autoParam}
  {hi : W₁ i} {hp : W₂ p} {Z_1 : C} {i_1 : X ⟶ Z_1} {p_1 : Z_1 ⟶ Y}
  {fac_1 :
    autoParam (CategoryTheory.CategoryStruct.comp i_1 p_1 = f)
      CategoryTheory.MorphismProperty.MapFactorizationData.fac._autoParam}
  {hi_1 : W₁ i_1} {hp_1 : W₂ p_1},
  { Z := Z, i := i, p := p, fac := fac, hi := hi, hp := hp } =
      { Z := Z_1, i := i_1, p := p_1, fac := fac_1, hi := hi_1, hp := hp_1 } →
    Z = Z_1 ∧ i ≍ i_1 ∧ p ≍ p_1
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex_π : ∀ {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) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex._auto_3),
  (X.leftHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).π =
    CategoryTheory.Limits.cokernel.π (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯)
-- Mathlib.Condensed.Discrete.Basic
Condensed.discrete_obj : ∀ (C : Type w) [inst : CategoryTheory.Category.{u + 1, w} C]
  [inst_1 : CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) C] (X : C),
  (Condensed.discrete C).obj X =
    (CategoryTheory.presheafToSheaf (CategoryTheory.coherentTopology CompHaus) C).obj
      ((CategoryTheory.Functor.const CompHausᵒᵖ).obj X)
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_add_one : ∀ (o : Ordinal.{u_1}), (o + 1).cof = 1
-- Init.Data.Range.Polymorphic.PRange
Std.instDecidableEqRii.decEq : {α : Type u_1} → [DecidableEq α] → (x x_1 : Std.Rii α) → Decidable (x = x_1)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.hasSMul' : {ι : Type u_1} →
  {R : Type u_4} →
    [inst : CommSemiring R] →
      {R₁ : Type u_5} →
        {s : ι → Type u_7} →
          [inst_1 : (i : ι) → AddCommMonoid (s i)] →
            [inst_2 : (i : ι) → Module R (s i)] →
              [inst_3 : Monoid R₁] →
                [inst_4 : DistribMulAction R₁ R] → [SMulCommClass R₁ R R] → SMul R₁ (PiTensorProduct R fun i => s i)
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.freeOn_restrict : ∀ {α : Type u_1} {E R : Set α}, R ⊆ E → (Matroid.freeOn E).restrict R = Matroid.freeOn R
-- Init.Data.RArray
Lean.RArray.leaf.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (a : α), sizeOf (Lean.RArray.leaf a) = 1 + sizeOf a
-- Mathlib.Data.Sym.Basic
Sym.coe_append : ∀ {α : Type u_1} {n n' : ℕ} (s : Sym α n) (s' : Sym α n'), ↑(s.append s') = ↑s + ↑s'
-- Mathlib.Data.Fin.Basic
Fin.natCast_le_natCast : ∀ {n a b : ℕ}, a ≤ n → b ≤ n → (↑a ≤ ↑b ↔ a ≤ b)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.st_add : ∀ {x y : ℝ*}, ¬x.Infinite → ¬y.Infinite → (x + y).st = x.st + y.st
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.algHom_ext'_iff : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {A : Type u_2} {B : Type u_3} [inst_1 : CommSemiring A]
  [inst_2 : CommSemiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] {f g : MvPolynomial σ A →ₐ[R] B},
  f = g ↔
    f.comp (IsScalarTower.toAlgHom R A (MvPolynomial σ A)) = g.comp (IsScalarTower.toAlgHom R A (MvPolynomial σ A)) ∧
      ∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)
-- Mathlib.LinearAlgebra.TensorProduct.Decomposition
DirectSum.toBaseChange_injective : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (ℳ : ι → Submodule R M) [inst_3 : DecidableEq ι] [DirectSum.Decomposition ℳ]
  [inst_5 : CommSemiring S] [inst_6 : Algebra R S] (i : ι), Function.Injective ⇑(Submodule.toBaseChange S (ℳ i))
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.dirac_conv : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M] (x : M)
  (μ : MeasureTheory.Measure M) [MeasureTheory.SFinite μ],
  (MeasureTheory.Measure.dirac x).conv μ = MeasureTheory.Measure.map (fun y => x + y) μ
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- A nonarchimedean norm on an additive group `G` is a function `f : G → ℝ` that preserves zero, is
nonarchimedean and such that `f (-x) = f x` and `f x = 0 → x = 0` for all `x`.  -/
NonarchAddGroupNorm : (G : Type u_6) → [AddGroup G] → Type u_6
-- Mathlib.Algebra.Group.ForwardDiff
/-- Linear-endomorphism version of the forward difference operator.  -/
fwdDiff_aux.fwdDiffₗ : (M : Type u_1) → (G : Type u_2) → [AddCommMonoid M] → [inst : AddCommGroup G] → M → Module.End ℤ (M → G)
-- Mathlib.Order.Filter.Extr
IsExtrOn.on_preimage : ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {s : Set α} (g : δ → α) {b : δ},
  IsExtrOn f s (g b) → IsExtrOn (f ∘ g) (g ⁻¹' s) b
-- Mathlib.RingTheory.Localization.FractionRing
FractionRing.mk_eq_div : ∀ (A : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A] {r : A} {s : ↥(nonZeroDivisors A)},
  Localization.mk r s = (algebraMap A (FractionRing A)) r / (algebraMap A (FractionRing A)) ↑s
-- Mathlib.GroupTheory.Goursat
AddSubgroup.normal_goursatFst : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] {I : AddSubgroup (G × H)},
  Function.Surjective (Prod.fst ∘ ⇑I.subtype) → I.goursatFst.Normal
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.RightAdjoint.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {left : a ⟶ b} →
        (right : b ⟶ a) → CategoryTheory.Bicategory.Adjunction left right → CategoryTheory.Bicategory.RightAdjoint left
-- Mathlib.Algebra.Colimit.Module
/-- The universal property of the direct limit: maps from the components to another abelian group
that respect the directed system structure (i.e. make some diagram commute) give rise
to a unique map out of the direct limit.  -/
AddCommGroup.DirectLimit.lift : {ι : Type u_2} →
  [inst : Preorder ι] →
    (G : ι → Type u_3) →
      [inst_1 : (i : ι) → AddCommMonoid (G i)] →
        (f : (i j : ι) → i ≤ j → G i →+ G j) →
          [inst_2 : DecidableEq ι] →
            (P : Type u_4) →
              [inst_3 : AddCommMonoid P] →
                (g : (i : ι) → G i →+ P) →
                  (∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) →
                    AddCommGroup.DirectLimit G f →+ P
-- Init.Data.Nat.Basic
Nat.le_of_not_le : ∀ {a b : ℕ}, ¬b ≤ a → a ≤ b
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_smul : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [inst : SMul M G] (n : M) (f : α → G), ↑(n • f) = n • ↑f
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.ComponentCompl.infinite_iff_in_all_ranges : ∀ {V : Type u} {G : SimpleGraph V} {K : Finset V} (C : G.ComponentCompl ↑K),
  C.supp.Infinite ↔ ∀ (L : Finset V) (h : K ⊆ L), ∃ D, SimpleGraph.ComponentCompl.hom h D = C
-- Mathlib.Order.Circular
/-- **Alias** of `sbtw_cyclic_right`. -/
SBtw.sbtw.cyclic_right : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw c a b