mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.LocalRing.Pullback
RingHom.isLocalRing_eqLocus : ∀ {R : Type u_1} {T : Type u_3} [inst : Ring R] [inst_1 : Semiring T] [IsLocalRing R] (f g : R →+* T),
  IsLocalRing ↥(f.eqLocus g)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_eq_eval_map : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (g : σ → S₁) (p : MvPolynomial σ R), MvPolynomial.eval₂ f g p = (MvPolynomial.eval g) ((MvPolynomial.map f) p)
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- A weight function is nontorsion if its values are not torsion.  -/
MvPolynomial.NonTorsionWeight : {M : Type u_2} → {σ : Type u_3} → [AddCommMonoid M] → (σ → M) → Prop
-- Mathlib.Data.Set.Operations
Set.mapsTo_image : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Set α), Set.MapsTo f s (f '' s)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Functor.map_hom_inv_assoc : ∀ {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 : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.IsIso f] {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.inv f)) h) = h
-- Std.Http.Data.Status
Std.Http.Status.imATeapot.sizeOf_spec : sizeOf Std.Http.Status.imATeapot = 1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.forM_eq_forM_toArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α × β → m PUnit.{w + 1}}, forM t f = Array.forM f t.toArray
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_cau_seq : {p : ℕ} →
  [inst : Fact (Nat.Prime p)] →
    {R : Type u_1} →
      [inst_1 : CommSemiring R] →
        [inst_2 : Algebra R ℤ_[p]] →
          {F : Polynomial R} →
            {a : ℤ_[p]} →
              ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 → CauSeq ℤ_[p] norm
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constEntryAtIdxD_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {i : ℕ} {fallback : α × β},
          Std.DTreeMap.Internal.Impl.Const.entryAtIdxD t₁ i fallback =
            Std.DTreeMap.Internal.Impl.Const.entryAtIdxD t₂ i fallback
-- Mathlib.Algebra.Module.LinearMap.Basic
LinearMap.instSMulCommClassDomMulAct : ∀ {R : Type u_1} {R' : Type u_2} {M : Type u_4} {M' : Type u_5} [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'}
  {S' : Type u_6} {T' : Type u_7} [inst_6 : Monoid S'] [inst_7 : DistribMulAction S' M] [inst_8 : SMulCommClass R S' M]
  [inst_9 : Monoid T'] [inst_10 : DistribMulAction T' M] [inst_11 : SMulCommClass R T' M] [SMulCommClass S' T' M],
  SMulCommClass S'ᵈᵐᵃ T'ᵈᵐᵃ (M →ₛₗ[σ₁₂] M')
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.BundledIterM.step.eq_1 : ∀ {β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : LawfulMonad m] (it : Std.BundledIterM m β),
  it.step = Std.Iterators.HetT.map (Std.IterStep.mapIterator Std.BundledIterM.ofIterM) it.iterator.stepAsHetT
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsTrail.dropUntil : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v w : V} {p : G.Walk v w},
  p.IsTrail → ∀ (h : u ∈ p.support), (p.dropUntil u h).IsTrail
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousLinearMap.coe_flipMultilinearEquiv : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : SeminormedAddCommGroup G']
  [inst_6 : NormedSpace 𝕜 G'] [inst_7 : Fintype ι],
  ⇑(ContinuousLinearMap.flipMultilinearEquiv 𝕜 E G G') = ContinuousLinearMap.flipMultilinear
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
MonCat.Hom.Simps.hom : (X Y : MonCat) → X.Hom Y → ↑X →* ↑Y
-- Mathlib.Analysis.Convex.StdSimplex
/-- Every vector in `stdSimplex 𝕜 ι` has `max`-norm at most `1`.  -/
stdSimplex_subset_closedBall : ∀ {ι : Type u_1} [inst : Fintype ι], stdSimplex ℝ ι ⊆ Metric.closedBall 0 1
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.norm_apply : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K),
  NumberField.mixedEmbedding.norm x = ∏ w, (NumberField.mixedEmbedding.normAtPlace w) x ^ w.mult
-- Mathlib.Algebra.Module.TransferInstance
Equiv.linearEquiv_symm_apply : ∀ {R : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring R] (e : α ≃ β) (b : β) [inst_1 : AddCommMonoid β]
  [inst_2 : Module R β], (Equiv.linearEquiv R e).symm b = e.symm b
-- Mathlib.MeasureTheory.Group.Defs
MeasureTheory.Measure.instSMulInvariantMeasureSubtypeMemSubmonoidOfIsMulLeftInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : Monoid G] (s : Submonoid G)
  [μ.IsMulLeftInvariant], MeasureTheory.SMulInvariantMeasure (↥s) G μ
-- Mathlib.Algebra.GroupWithZero.Units.Basic
zpow_ne_zero : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀} (n : ℤ), a ≠ 0 → a ^ n ≠ 0
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.Injective.isExpansionOn_default : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {ϕ : L →ᴸ L'}
  [inst : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => ϕ.onFunction f)]
  [inst_1 : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => ϕ.onRelation r)],
  ϕ.Injective → ∀ (M : Type u_1) [inst_2 : Inhabited M] [inst_3 : L.Structure M], ϕ.IsExpansionOn M
-- Mathlib.RingTheory.ZMod.UnitsCyclic
ZMod.isCyclic_units_two_pow_iff : ∀ (n : ℕ), IsCyclic (ZMod (2 ^ n))ˣ ↔ n ≤ 2
-- Mathlib.Order.Filter.AtTopBot.Interval
Finset.tendsto_Ioo_atBot_prod_atTop : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [NoBotOrder α] [NoTopOrder α],
  Filter.Tendsto (fun p => Finset.Ioo p.1 p.2) (Filter.atBot ×ˢ Filter.atTop) Filter.atTop
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.embDomain_add : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddMonoid R]
  [inst_2 : PartialOrder Γ'] (f : Γ ↪o Γ') (x y : HahnSeries Γ R),
  HahnSeries.embDomain f (x + y) = HahnSeries.embDomain f x + HahnSeries.embDomain f y
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
PresheafOfModules.toPresheaf_map_sheafificationHomEquiv : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  [inst_3 : J.WEqualsLocallyBijective AddCommGrpCat] [inst_4 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  {P : PresheafOfModules R₀} {F : SheafOfModules R} (f : (PresheafOfModules.sheafification α).obj P ⟶ F),
  (PresheafOfModules.toPresheaf R₀).map ((PresheafOfModules.sheafificationHomEquiv α) f) =
    ((CategoryTheory.sheafificationAdjunction J AddCommGrpCat).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F))
      ((SheafOfModules.toSheaf R).map f)
-- Lean.Server.ServerTask
Lean.Server.ServerTask.task : {α : Type u} → Lean.Server.ServerTask α → Task α
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.eq_one_of_map_eq_one : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {S : Type u_1} [inst_1 : Semiring S] [Nontrivial S] (f : R →+* S),
  p.Monic → Polynomial.map f p = 1 → p = 1
-- Mathlib.Topology.Algebra.LinearTopology
/-- To show that `M` is linearly-topologized as an `R`-module, it suffices to show
that it has a basis of neighborhoods of zero made of `R`-submodules.

Note: for technical reasons detailed in the module docstring, Lean sometimes struggles to find the
right `SMulMemClass` instance. See `IsLinearTopology.mk_of_hasBasis'` for a more
explicit variant.  -/
IsLinearTopology.mk_of_hasBasis : ∀ (R : Type u_1) {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] {ι : Sort u_4} {S : Type u_5} [inst_4 : SetLike S M] [SMulMemClass S R M]
  [AddSubmonoidClass S M] {p : ι → Prop} {s : ι → S}, ((nhds 0).HasBasis p fun i => ↑(s i)) → IsLinearTopology R M
-- Mathlib.Algebra.Order.GroupWithZero.Defs
MulLeftMono.toPosMulReflectLT : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [MulLeftReflectLT α], PosMulReflectLT α
-- Mathlib.Data.Set.Lattice
Set.nonempty_iUnion : ∀ {α : Type u_1} {ι : Sort u_5} {s : ι → Set α}, (⋃ i, s i).Nonempty ↔ ∃ i, (s i).Nonempty
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.truncLE'_d_eq_toCycles : ∀ {ι : 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']
  {i j : ι} (hij : c.Rel i j) {i' j' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hj : e.BoundaryLE j),
  (K.truncLE' e).d i j =
    CategoryTheory.CategoryStruct.comp (K.truncLE'XIso e hi' ⋯).hom
      (CategoryTheory.CategoryStruct.comp (K.toCycles i' j') (K.truncLE'XIsoCycles e hj' hj).inv)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile.0.Std.Iterators.Types.DropWhile.instIterator.match_3.eq_1 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β]
  {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)} (it : Std.IterM m β)
  (motive : it.internalState.inner.Step → Sort u_3) (it' : Std.IterM m β) (out : β)
  (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) →
        (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
          motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 :
    (it' : Std.IterM m β) →
      (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it' out h
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (t.insertIfNew k v).isEmpty = false
-- Mathlib.SetTheory.Cardinal.Basic
/-- A variant of `lift_iSup_le_lift_iSup` with universes specialized via `w = v` and `w' = v'`.
This is sometimes necessary to avoid universe unification issues.  -/
Cardinal.lift_iSup_le_lift_iSup' : ∀ {ι : Type v} {ι' : Type v'} {f : ι → Cardinal.{v}} {f' : ι' → Cardinal.{v'}},
  BddAbove (Set.range f) →
    BddAbove (Set.range f') →
      ∀ (g : ι → ι'),
        (∀ (i : ι), Cardinal.lift.{v', v} (f i) ≤ Cardinal.lift.{v, v'} (f' (g i))) →
          Cardinal.lift.{v', v} (iSup f) ≤ Cardinal.lift.{v, v'} (iSup f')
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.abs_tendsto_atTop_iff : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜)
  [OrderTopology 𝕜], Filter.Tendsto (fun x => |Polynomial.eval x P|) Filter.atTop Filter.atTop ↔ 0 < P.degree
-- Init.Grind.ToInt
Lean.Grind.IntInterval.co.injEq : ∀ (lo hi lo_1 hi_1 : ℤ),
  (Lean.Grind.IntInterval.co lo hi = Lean.Grind.IntInterval.co lo_1 hi_1) = (lo = lo_1 ∧ hi = hi_1)
-- Mathlib.Data.List.Lex
Decidable.List.Lex.ne_iff : ∀ {α : Type u} [DecidableEq α] {l₁ l₂ : List α},
  l₁.length ≤ l₂.length → (List.Lex (fun x1 x2 => x1 ≠ x2) l₁ l₂ ↔ l₁ ≠ l₂)
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isLE_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) (n : ℤ), K.IsLE n ↔ ∀ (i : ℤ), n < i → HomologicalComplex.ExactAt K i
-- Init.Data.String.Slice
/-- Creates a new slice that contains the longest prefix of `s` for which `pat` matched
\(potentially repeatedly\).

Examples:

* `"red green blue".toSlice.dropWhile Char.isLower == " green blue".toSlice`

* `"red green blue".toSlice.dropWhile 'r' == "ed green blue".toSlice`

* `"red red green blue".toSlice.dropWhile "red " == "green blue".toSlice`

* `"red green blue".toSlice.dropWhile (fun (_ : Char) => true) == "".toSlice`
 -/
String.Slice.dropWhile : {ρ : Type} → String.Slice → (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → String.Slice
-- Mathlib.Algebra.Ring.Associator
AddMonoidHom.associator_apply : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (a b c : R), ((AddMonoidHom.associator a) b) c = associator a b c
-- Mathlib.Algebra.Order.Group.Action.Synonym
Lex.instIsScalarTower' : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : SMul M N] [inst_1 : SMul M α] [inst_2 : SMul N α]
  [IsScalarTower M N α], IsScalarTower M (Lex N) α
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabOpen : Lean.Elab.Command.CommandElab
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.toReducedWord : {G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} →
      {d : HNNExtension.NormalWord.TransversalPair G A B} →
        HNNExtension.NormalWord d → HNNExtension.NormalWord.ReducedWord G A B
-- Mathlib.LinearAlgebra.Eigenspace.Pi
Module.End.injOn_iInf_maxGenEigenspace : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (f : ι → Module.End R M) [IsDomain R] [Module.IsTorsionFree R M],
  Set.InjOn (fun χ => ⨅ i, (f i).maxGenEigenspace (χ i)) {χ | ⨅ i, (f i).maxGenEigenspace (χ i) ≠ ⊥}
-- Mathlib.Tactic.Linter.EmptyLine
/-- `filterMapM stx f` takes as input a `Syntax` `stx` and a monadic function `f : Syntax → m α`.
It produces the array of the `some` values that `f` takes while traversing `stx`.

See `filterMap` for a non-monadic version.
 -/
Lean.Syntax.filterMapM : {m : Type → Type} → [Monad m] → {α : Type} → Lean.Syntax → (Lean.Syntax → m (Option α)) → m (Array α)
-- Mathlib.CategoryTheory.Sites.Point.Conservative
CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.mk' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {P : CategoryTheory.ObjectProperty J.Point} [CategoryTheory.LocallySmall.{w, v, u} C]
  [CategoryTheory.HasSheafify J (Type w)],
  (∀ ⦃X : C⦄ (S : CategoryTheory.Sieve X),
      (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
          ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (CategoryTheory.ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
        S ∈ J X) →
    P.IsConservativeFamilyOfPoints
-- Mathlib.Order.Filter.Ultrafilter.Basic
Filter.notMem_hyperfilter_of_finite : ∀ {α : Type u} [inst : Infinite α] {s : Set α}, s.Finite → s ∉ Filter.hyperfilter α
-- Mathlib.Order.Antichain
IsStrongAntichain.mono : ∀ {α : Type u_1} {r₁ r₂ : α → α → Prop} {s : Set α}, IsStrongAntichain r₁ s → r₂ ≤ r₁ → IsStrongAntichain r₂ s
-- Mathlib.GroupTheory.Subgroup.Center
CommGroup.center_eq_top : ∀ {G : Type u_2} [inst : CommGroup G], Subgroup.center G = ⊤
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inverseAssociator_map_inl : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.sum.inverseAssociator C D E).map ((CategoryTheory.Sum.inl_ C (D ⊕ E)).map f) =
    (CategoryTheory.Sum.inl_ (C ⊕ D) E).map ((CategoryTheory.Sum.inl_ C D).map f)
-- Lean.Util.CollectFVars
Lean.CollectFVars.instInhabitedState.default : Lean.CollectFVars.State
-- Mathlib.Data.Num.Basic
ZNum.pos.inj : ∀ {a a_1 : PosNum}, ZNum.pos a = ZNum.pos a_1 → a = a_1
-- Mathlib.Logic.Godel.GodelBetaFunction
/-- Inverse of Gödel's Beta Function. This is similar to `Encodable.encodeList`, but it is easier
to prove that it is arithmetically definable.  -/
Nat.unbeta : List ℕ → ℕ
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpExtensionMap : Type
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- commutation with `ι`  -/
CategoryTheory.ShortComplex.RightHomologyMapData.commι : ∀ {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₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (self : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂),
  CategoryTheory.CategoryStruct.comp self.φH h₂.ι = CategoryTheory.CategoryStruct.comp h₁.ι self.φQ
-- Mathlib.Data.String.Basic
_private.Mathlib.Data.String.Basic.0.String.Legacy.Iterator.next.eq_1 : ∀ (s : String) (i : String.Pos.Raw), { s := s, i := i }.next = { s := s, i := String.Pos.Raw.next s i }
-- Mathlib.Combinatorics.Hall.Finite
/-- This is the version of **Hall's Marriage Theorem** in terms of indexed
families of finite sets `t : ι → Finset α` with `ι` finite.
It states that there is a set of distinct representatives if and only
if every union of `k` of the sets has at least `k` elements.

See `Finset.all_card_le_biUnion_card_iff_exists_injective` for a version
where the `Finite ι` constraint is removed.
 -/
Finset.all_card_le_biUnion_card_iff_existsInjective' : ∀ {ι : Type u_1} {α : Type u_2} [Finite ι] [inst : DecidableEq α] (t : ι → Finset α),
  (∀ (s : Finset ι), s.card ≤ (s.biUnion t).card) ↔ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
-- Mathlib.Analysis.Fourier.Convolution
/-- The convolution is continuous in the left argument.

Note that since `𝓢(E, F)` is not a normed space, uncurried and curried continuity do not
coincide.  -/
SchwartzMap.convolution_continuous_left : ∀ {𝕜 : Type u_1} {E : Type u_3} {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E]
  [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E] [inst_6 : NormedAddCommGroup F₁] [inst_7 : NormedSpace ℂ F₁]
  [inst_8 : NormedSpace 𝕜 F₁] [inst_9 : SMulCommClass ℂ 𝕜 F₁] [inst_10 : NormedAddCommGroup F₂]
  [inst_11 : NormedSpace ℂ F₂] [inst_12 : NormedSpace 𝕜 F₂] [inst_13 : SMulCommClass ℂ 𝕜 F₂]
  [inst_14 : NormedAddCommGroup F₃] [inst_15 : NormedSpace ℂ F₃] [inst_16 : NormedSpace 𝕜 F₃]
  [inst_17 : SMulCommClass ℂ 𝕜 F₃] (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃) (g : SchwartzMap E F₂),
  Continuous fun x => ((SchwartzMap.convolution B) x) g
-- Mathlib.CategoryTheory.Preadditive.Opposite
CategoryTheory.op_zsmul : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} (k : ℤ)
  (f : X ⟶ Y), (k • f).op = k • f.op
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.size.match_1.eq_2 : ∀ {α : Type u_1} (motive : Ordnode α → Sort u_2) (sz : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α)
  (h_1 : Unit → motive Ordnode.nil)
  (h_2 : (sz : ℕ) → (l : Ordnode α) → (x : α) → (r : Ordnode α) → motive (Ordnode.node sz l x r)),
  (match Ordnode.node sz l x r with
    | Ordnode.nil => h_1 ()
    | Ordnode.node sz l x r => h_2 sz l x r) =
    h_2 sz l x r
-- Batteries.Data.List.Basic
/-- `xs.toChunks n` splits the list into sublists of size at most `n`,
such that `(xs.toChunks n).join = xs`.
```
[1, 2, 3, 4, 5, 6, 7, 8].toChunks 10 = [[1, 2, 3, 4, 5, 6, 7, 8]]
[1, 2, 3, 4, 5, 6, 7, 8].toChunks 3 = [[1, 2, 3], [4, 5, 6], [7, 8]]
[1, 2, 3, 4, 5, 6, 7, 8].toChunks 2 = [[1, 2], [3, 4], [5, 6], [7, 8]]
[1, 2, 3, 4, 5, 6, 7, 8].toChunks 0 = [[1, 2, 3, 4, 5, 6, 7, 8]]
```
 -/
List.toChunks : {α : Type u_1} → ℕ → List α → List (List α)
-- Mathlib.Topology.Algebra.Module.Complement
/-- **Alias** of `Submodule.IsTopCompl.continuous_projectionOnto`. -/
Submodule.IsTopCompl.continuous_linearProjOfIsCompl : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q), Continuous ⇑(p.projectionOnto q ⋯)
-- Lean.Elab.Tactic.Basic
/-- Return the first goal.  -/
Lean.Elab.Tactic.getMainGoal : Lean.Elab.Tactic.TacticM Lean.MVarId
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.enrichedHom.congr_simp : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₁_1 : CategoryTheory.Functor J C) (e_F₁ : F₁ = F₁_1)
  (F₂ F₂_1 : CategoryTheory.Functor J C) (e_F₂ : F₂ = F₂_1)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂],
  CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂ =
    CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁_1 F₂_1
-- Init.Data.UInt.Lemmas
USize.neg_neg : ∀ {a : USize}, - -a = a
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.toLegacyIterator.eq_1 : ∀ (s : String) (b stopPos : String.Pos.Raw),
  { str := s, startPos := b, stopPos := stopPos }.toLegacyIterator = { s := s, i := b }
-- Mathlib.Data.List.Permutation
List.map_permutations' : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (ts : List α),
  List.map (List.map f) ts.permutations' = (List.map f ts).permutations'
-- Mathlib.CategoryTheory.Functor.Flat
/-- Representably coflat functors preserve finite colimits.  -/
CategoryTheory.preservesFiniteColimits_of_coflat : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.RepresentablyCoflat F],
  CategoryTheory.Limits.PreservesFiniteColimits F
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- The rotation of a vector by `θ` has an angle of `-θ` from that vector.  -/
Orientation.oangle_rotation_self_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x : V}, x ≠ 0 → ∀ (θ : Real.Angle), o.oangle ((o.rotation θ) x) x = -θ
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.MorphismProperty.Over.instPreservesFiniteLimitsTopPullback : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T)
  [inst_1 : CategoryTheory.Limits.HasPullbacks T] [P.IsMultiplicative] [inst_3 : P.IsStableUnderBaseChange]
  [P.HasOfPostcompProperty P] {X Y : T} (f : X ⟶ Y),
  CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MorphismProperty.Over.pullback P ⊤ f)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_mul_lt_iff_left_lt_of_ne_zero : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
  {p p' q : MvPolynomial σ R},
  p ≠ 0 →
    q ≠ 0 → (m.toSyn (m.degree (p * q)) < m.toSyn (m.degree (p' * q)) ↔ m.toSyn (m.degree p) < m.toSyn (m.degree p'))
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_hom_inv_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y : C} (s : X ⟶ Y) (hs : W s),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).map s)
      (CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv s hs) =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj X)