mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_restoreM_ExceptT_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε α : Type u}
  {post : α → Pred} {epost : EPost.Cons✝ (ε → Pred) EPred} (x : m (Except ε α)),
  Std.Internal.Do.wp (MonadControl.restoreM x) post epost =
    Std.Internal.Do.wp x (Std.Internal.Do.EPost.Cons.pushExcept post epost) epost.tail
-- Lean.Meta.Tactic.SplitIf
/-- Split an `if-then-else` in the goal target.
If `useNewSemantics` is `true`, the flag `backward.split` is ignored.
 -/
Lean.Meta.splitIfTarget? : Lean.MVarId →
  optParam (Option Lean.Name) none →
    optParam Bool false → Lean.MetaM (Option (Lean.Meta.ByCasesSubgoal × Lean.Meta.ByCasesSubgoal))
-- Mathlib.ModelTheory.Syntax
/-- Sends a term with constants to a term with extra variables.  -/
FirstOrder.Language.Term.constantsToVars : {L : FirstOrder.Language} → {α : Type u'} → {γ : Type u_1} → (L.withConstants γ).Term α → L.Term (γ ⊕ α)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
/-- A functor that preserves zero morphisms also preserves the zero object.  -/
CategoryTheory.Functor.mapZeroObject : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_3 : CategoryTheory.Limits.HasZeroObject D] →
            [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] →
              [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] →
                (F : CategoryTheory.Functor C D) → [F.PreservesZeroMorphisms] → F.obj 0 ≅ 0
-- Mathlib.Logic.Encodable.Basic
Encodable.mem_decode₂ : ∀ {α : Type u_1} [inst : Encodable α] {n : ℕ} {a : α}, a ∈ Encodable.decode₂ α n ↔ Encodable.encode a = n
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {a : α} [inst : Inhabited α], ∅.getKey! a = default
-- Mathlib.Algebra.Group.End
Equiv.Perm.ofSubtype_subtypePerm_of_mem : ∀ {α : Type u_4} {p : α → Prop} [inst : DecidablePred p] {g : Equiv.Perm α} (hg : ∀ (x : α), p (g x) ↔ p x) {a : α},
  p a → (Equiv.Perm.ofSubtype (g.subtypePerm hg)) a = g a
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
/-- The data of a constructible set `s` in the prime spectrum of a ring is finitely many tuples
`(f, g₁, ..., gₙ)` such that `s = ⋃ (f, g₁, ..., gₙ), V(g₁, ..., gₙ) \ V(f)`.

To obtain `s` from its data, use `PrimeSpectrum.ConstructibleSetData.toSet`.  -/
PrimeSpectrum.ConstructibleSetData : Type u_1 → Type u_1
-- Mathlib.Topology.Algebra.Group.Basic
totallyDisconnectedSpace_iff_connectedComponent_zero : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G],
  TotallyDisconnectedSpace G ↔ connectedComponent 0 = {0}
-- Mathlib.CategoryTheory.Shift.Induced
CategoryTheory.HasShift.Induced.zero.congr_simp : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_3} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D)
  (i i_1 : (a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F),
  i = i_1 →
    ∀ [inst_4 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Full]
      [inst_5 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Faithful],
      CategoryTheory.HasShift.Induced.zero F s i = CategoryTheory.HasShift.Induced.zero F s i_1
-- Mathlib.Data.List.Lattice
List.mem_of_mem_inter_right : ∀ {α : Type u_1} {l₁ l₂ : List α} {a : α} [inst : DecidableEq α], a ∈ l₁ ∩ l₂ → a ∈ l₂
-- Mathlib.Algebra.Group.Hom.Basic
AddMonoidHom.instNeg.eq_1 : ∀ {M : Type u_2} {G : Type u_5} [inst : AddZeroClass M] [inst_1 : AddCommGroup G],
  AddMonoidHom.instNeg = { neg := fun f => AddMonoidHom.mk' (fun g => -f g) ⋯ }
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- Subsemigroups of a semigroup `Multiplicative A` are isomorphic to additive subsemigroups
of `A`.  -/
Subsemigroup.toAddSubsemigroup' : {A : Type u_5} → [inst : Add A] → Subsemigroup (Multiplicative A) ≃o AddSubsemigroup A
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanModuleHierarchyImportedByParams.mk.injEq : ∀ (module module_1 : Lean.Lsp.LeanModule), ({ module := module } = { module := module_1 }) = (module = module_1)
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
/-- If `Γ` has finite index in `SL(2, ℤ)`, then so does `g⁻¹ Γ g ∩ SL(2, ℤ)` for any
`g ∈ GL(2, ℚ)`.  -/
CongruenceSubgroup.finiteIndex_conjGL : ∀ (g : GL (Fin 2) ℚ), (CongruenceSubgroup.conjGL ⊤ ((Matrix.GeneralLinearGroup.map (Rat.castHom ℝ)) g)).FiniteIndex
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, returning `none` if no such pair exists.
 -/
Std.ExtDTreeMap.Const.getEntryGE? : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Std.TransCmp cmp] → Std.ExtDTreeMap α (fun x => β) cmp → α → Option (α × β)
-- Mathlib.MeasureTheory.MeasurableSpace.Prod
/-- The comap of `Prod.map` is the product of the comaps.  -/
MeasurableSpace.comap_prodMap : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  (X : γ → α) (Y : δ → β),
  MeasurableSpace.comap (Prod.map X Y) (mα.prod mβ) = (MeasurableSpace.comap X mα).prod (MeasurableSpace.comap Y mβ)
-- Lean.Elab.InfoTree.Basic
/-- Obtains the `LocalContext` from this `CompletionInfo` if available and yields an empty context
otherwise.
 -/
Lean.Elab.CompletionInfo.lctx : Lean.Elab.CompletionInfo → Lean.LocalContext
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.Functor.map_isPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan h i) F],
  CategoryTheory.IsPullback f g h i → CategoryTheory.IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
-- Mathlib.AlgebraicGeometry.Morphisms.FlatRank
/-- The rank of a morphism `f : X ⟶ S` of schemes at a point `s : S`. When `f` is finite,
flat and locally of finite presentation, this is a locally constant function (see
`AlgebraicGeometry.isLocallyConstant_finrank`).  -/
AlgebraicGeometry.Scheme.Hom.finrank : {X S : AlgebraicGeometry.Scheme} → (X ⟶ S) → ↥S → ℕ
-- Mathlib.Tactic.Widget.StringDiagram
/-- The vertical position of a node in a string diagram.  -/
Mathlib.Tactic.Widget.StringDiagram.Node.vPos : Mathlib.Tactic.Widget.StringDiagram.Node → ℕ
-- Init.Data.Int.DivMod.Lemmas
Int.bdiv_add_bmod : ∀ (x : ℤ) (m : ℕ), ↑m * x.bdiv m + x.bmod m = x
-- Mathlib.Data.Finset.Fin
Finset.attachFin_subset_attachFin_iff : ∀ {n : ℕ} {s t : Finset ℕ} (hs : ∀ m ∈ s, m < n) (ht : ∀ m ∈ t, m < n), s.attachFin hs ⊆ t.attachFin ht ↔ s ⊆ t
-- Mathlib.Topology.Convenient.Category
instFaithfulTopCatContinuousGeneratedByCatToContinuousGeneratedByCat : ∀ {ι : Type t} (X : ι → Type u) [inst : (i : ι) → TopologicalSpace (X i)],
  (TopCat.toContinuousGeneratedByCat X).Faithful
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.intCast_add : ∀ {α : Type u} [inst : Lean.Grind.Ring α] (x y : ℤ), ↑(x + y) = ↑x + ↑y
-- Mathlib.Data.Set.Insert
Set.eq_of_nonempty_of_subsingleton' : ∀ {α : Type u_3} [Subsingleton α] {s : Set α} (t : Set α), s.Nonempty → ∀ [Nonempty ↑t], s = t
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
ENNReal.borelSpace : BorelSpace ENNReal
-- Mathlib.Order.Antisymmetrization
toAntisymmetrization_lt_toAntisymmetrization_iff : ∀ {α : Type u_1} {a b : α} [inst : Preorder α],
  toAntisymmetrization (fun x1 x2 => x1 ≤ x2) a < toAntisymmetrization (fun x1 x2 => x1 ≤ x2) b ↔ a < b
-- Mathlib.LinearAlgebra.TensorAlgebra.Basis
/-- The `TensorAlgebra` of a free module over a commutative semiring with no zero-divisors has
no zero-divisors.  -/
TensorAlgebra.instNoZeroDivisors : ∀ {R : Type uR} {M : Type uM} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [NoZeroDivisors R] [Module.Free R M], NoZeroDivisors (TensorAlgebra R M)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mul_subset_mul_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s t₁ t₂ : Finset α}, t₁ ⊆ t₂ → s * t₁ ⊆ s * t₂
-- Mathlib.Algebra.QuadraticAlgebra.Basic
/-- The representative of the root in the quadratic algebra  -/
QuadraticAlgebra.omega : {R : Type u_2} → {a b : R} → [Zero R] → [One R] → QuadraticAlgebra R a b
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionOfComplement.trans_F : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {F' : Type u_6} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace 𝕜 F'] [inst_9 : TopologicalSpace H]
  [inst_10 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11}
  {N : Type u_13} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H M] [inst_13 : TopologicalSpace N]
  [inst_14 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N},
  Manifold.IsSubmersionOfComplement F I J n f → ∀ (e : F ≃L[𝕜] F'), Manifold.IsSubmersionOfComplement F' I J n f
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
SchwartzMap.lineDerivOp_apply_eq_fderiv : ∀ {E : Type u_5} {F : Type u_8} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  [inst_3 : NormedSpace ℝ E] (m : E) (f : SchwartzMap E F) (x : E), (LineDeriv.lineDerivOp m f) x = (fderiv ℝ (⇑f) x) m
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mul.go.induct_unfolding : ∀ (p₂ : Lean.Grind.CommRing.Poly)
  (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Prop),
  (∀ (acc : Lean.Grind.CommRing.Poly) (k : ℤ),
      motive (Lean.Grind.CommRing.Poly.num k) acc (acc.combine (Lean.Grind.CommRing.Poly.mulConst k p₂))) →
    (∀ (acc : Lean.Grind.CommRing.Poly) (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
        motive p (acc.combine (Lean.Grind.CommRing.Poly.mulMon k m p₂))
            (Lean.Grind.CommRing.Poly.mul.go p₂ p (acc.combine (Lean.Grind.CommRing.Poly.mulMon k m p₂))) →
          motive (Lean.Grind.CommRing.Poly.add k m p) acc
            (Lean.Grind.CommRing.Poly.mul.go p₂ p (acc.combine (Lean.Grind.CommRing.Poly.mulMon k m p₂)))) →
      ∀ (p₁ acc : Lean.Grind.CommRing.Poly), motive p₁ acc (Lean.Grind.CommRing.Poly.mul.go p₂ p₁ acc)
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.mul_add_left_left : ∀ {R : Type u_1} [inst : CommRing R] {x y : R}, IsRelPrime x y → ∀ (z : R), IsRelPrime (y * z + x) y
-- Init.Data.UInt.Bitwise
UInt16.toBitVec_not : ∀ {a : UInt16}, (~~~a).toBitVec = ~~~a.toBitVec
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.add_smul_of_not_equiv : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  ¬P ≈ Q → ∀ {u v : R}, IsUnit u → IsUnit v → W'.add (u • P) (v • Q) = (u * v) ^ 2 • W'.add P Q
-- Mathlib.RingTheory.Finiteness.FinitePresentationLocal
/-- If `S` is an `R`-algebra with a surjection from a finitely-presented `R`-algebra `A`, such that
localized at a spanning set `{ r }` of elements of `A`, `Sᵣ` is finitely-presented, then
`S` is finitely presented.
This is almost `finitePresentation_ofLocalizationSpanTarget`. The difference is,
that here the set `t` generates the unit ideal of `A`, while in the general version,
it only generates a quotient of `A`.
 -/
Algebra.FinitePresentation.of_span_eq_top_target_aux : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A : Type u_3}
  [inst_3 : CommRing A] [inst_4 : Algebra R A] [Algebra.FinitePresentation R A] (f : A →ₐ[R] S),
  Function.Surjective ⇑f →
    ∀ (t : Finset A),
      Ideal.span ↑t = ⊤ →
        (∀ (g : ↥t), Algebra.FinitePresentation R (Localization.Away (f ↑g))) → Algebra.FinitePresentation R S
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.epimorphisms : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.MorphismProperty.epimorphisms C).IsStableUnderCobaseChange
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.mem_iInf : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_4}
  (p : ι → Submodule R M) {x : M}, x ∈ ⨅ i, p i ↔ ∀ (i : ι), x ∈ p i
-- Mathlib.CategoryTheory.Adjunction.Parametrized
CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_two_assoc : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ : C₁} {X₂ Y₂ : C₂} {X₃ : C₃}
  (f₂ : X₂ ⟶ Y₂) (g : Y₂ ⟶ (G.obj (Opposite.op X₁)).obj X₃) {Z : C₃} (h : X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (adj₂.homEquiv.symm (CategoryTheory.CategoryStruct.comp f₂ g)) h =
    CategoryTheory.CategoryStruct.comp ((F.obj X₁).map f₂) (CategoryTheory.CategoryStruct.comp (adj₂.homEquiv.symm g) h)
-- Mathlib.Algebra.Field.Defs
DivisionSemiring.toGroupWithZero : {K : Type u_2} → [self : DivisionSemiring K] → GroupWithZero K
-- Lean.Parser.Types
/-- Returns the next position in the input string after position `p`. If `p` is not a valid position or
`p = c.endPos`, returns the position one byte after `p`.

A run-time bounds check is performed to determine whether `p` is at the end of the string. If a
bounds check has already been performed, use `InputContext.next'` to avoid a repeated check.
 -/
Lean.Parser.InputContext.next : Lean.Parser.InputContext → String.Pos.Raw → String.Pos.Raw
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- This definition endows a completely metrizable space with a complete metric. Use it as:
`letI := upgradeIsCompletelyMetrizable X`.  -/
TopologicalSpace.upgradeIsCompletelyMetrizable : (X : Type u_3) →
  [inst : TopologicalSpace X] →
    [TopologicalSpace.IsCompletelyMetrizableSpace X] → TopologicalSpace.UpgradedIsCompletelyMetrizableSpace X
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.support_expand_subset : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : MvPowerSeries σ R),
  Function.support ((MvPowerSeries.expand p hp) φ) ⊆ (fun x => p • x) '' Function.support φ
-- Batteries.Data.Array.Scan
Array.scanrM_pure : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} [inst : Monad m] [LawfulMonad m] {f : α → β → β}
  {as : Array α}, Array.scanrM (fun x1 x2 => pure (f x1 x2)) init as = pure (Array.scanr f init as)
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.instHasColimitsOfShape : ∀ {C : Type u_1} {ι : Type u_2} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} J] {c : ComplexShape ι}
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasColimitsOfShape J C],
  CategoryTheory.Limits.HasColimitsOfShape J (HomologicalComplex C c)
-- Mathlib.Analysis.RCLike.Sqrt
Complex.re_sqrt_ofReal : ∀ {a : ℝ}, (↑a).sqrt.re = √a
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.cofan_inj_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  {Δ : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ),
  (s.cofan Δ).inj A = CategoryTheory.CategoryStruct.comp (s.ι (Opposite.unop A.fst).len) (X.map A.e.op)
-- Mathlib.Order.UpperLower.Relative
IsRelLowerSet.prop_of_mem : ∀ {α : Type u_1} {s : Set α} {a : α} {P : α → Prop} [inst : LE α], IsRelLowerSet s P → a ∈ s → P a
-- Mathlib.Combinatorics.SimpleGraph.Prod
/-- The embedding of `G` into `G □ H` given by `b`.  -/
SimpleGraph.boxProdLeft : {α : Type u_1} → {β : Type u_2} → (G : SimpleGraph α) → (H : SimpleGraph β) → β → G ↪g G □ H
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.orthogonalProjectionOnto.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection], K.orthogonalProjectionOnto = K.projectionOntoL Kᗮ ⋯
-- Mathlib.SetTheory.Ordinal.Notation
/-- A normal form ordinal notation has the form

`ω ^ a₁ * n₁ + ω ^ a₂ * n₂ + ⋯ + ω ^ aₖ * nₖ`

where `a₁ > a₂ > ⋯ > aₖ` and all the `aᵢ` are also in normal form.

We will essentially only be interested in normal form ordinal notations, but to avoid complicating
the algorithms, we define everything over general ordinal notations and only prove correctness with
normal form as an invariant.  -/
ONote.NF : ONote → Prop
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
/-- The map between the exact sequences `S₁.X₁.homology i ⟶ S₁.X₂.homology i ⟶ S₁.X₃.homology i`
and `S₂.X₁.homology i ⟶ S₂.X₂.homology i ⟶ S₂.X₃.homology i` that is induced by `φ : S₁ ⟶ S₂`.  -/
HomologicalComplex.HomologySequence.mapComposableArrows₂ : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Abelian C] →
        {c : ComplexShape ι} →
          {S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} →
            (S₁ ⟶ S₂) →
              (i : ι) →
                HomologicalComplex.HomologySequence.composableArrows₂ S₁ i ⟶
                  HomologicalComplex.HomologySequence.composableArrows₂ S₂ i
-- Lean.Elab.Arg
Lean.Elab.Term.expandArgs : Array Lean.Syntax → Lean.MetaM (Array Lean.Elab.Term.NamedArg × Array Lean.Elab.Term.Arg × Bool)
-- Std.Net.Addr
Std.Net.IPAddr.v4.sizeOf_spec : ∀ (addr : Std.Net.IPv4Addr), sizeOf (Std.Net.IPAddr.v4 addr) = 1 + sizeOf addr
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.OverArrows.val_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) {X : C}
  (s : CategoryTheory.yoneda.obj X ⟶ A) (u : F.obj (Opposite.op X))
  (h : CategoryTheory.OverPresheafAux.MakesOverArrow η s u), CategoryTheory.OverPresheafAux.OverArrows.val ⟨u, h⟩ = u
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Injective.instInhabitedState.default : Lean.Meta.Grind.Injective.State
-- Mathlib.Algebra.Star.SelfAdjoint
IsStarNormal.one : ∀ {R : Type u_1} [inst : MulOneClass R] [inst_1 : StarMul R], IsStarNormal 1
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.shiftFunctor_map_f : ∀ {S : Type u_1} [inst : AddCommGroupWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (n : S)
  {X Y : CategoryTheory.DifferentialObject S C} (f : X ⟶ Y),
  ((CategoryTheory.DifferentialObject.shiftFunctor C n).map f).f = (CategoryTheory.shiftFunctor C n).map f.f
-- Mathlib.Order.Hom.BoundedLattice
/-- `id` as an `InfTopHom`.  -/
InfTopHom.id : (α : Type u_2) → [inst : Min α] → [inst_1 : Top α] → InfTopHom α α
-- Init.Data.List.Basic
List.replicateTR_loop_eq : ∀ {α : Type u_1} {a : α} {acc : List α} (n : ℕ), List.replicateTR.loop a n acc = List.replicate n a ++ acc
-- Init.Data.List.Lemmas
List.contains_iff_mem : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {as : List α}, as.contains a = true ↔ a ∈ as
-- Mathlib.Order.RelSeries
/-- For two types `α, β` and relation on them `r, s`, if `f : α → β` preserves relation `r`, then an
`r`-series can be pushed out to an `s`-series by
`a₀ -r→ a₁ -r→ ... -r→ aₙ ↦ f a₀ -s→ f a₁ -s→ ... -s→ f aₙ`
 -/
RelSeries.map : {α : Type u_1} → {r : SetRel α α} → {β : Type u_2} → {s : SetRel β β} → RelSeries r → r.Hom s → RelSeries s
-- Init.Data.UInt.Bitwise
USize.shiftLeft_add_of_toNat_lt : ∀ {a b c : USize}, b.toNat + c.toNat < System.Platform.numBits → a <<< (b + c) = a <<< b <<< c
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- The identity map of the `SubAddAction` of the `fixingAddSubgroup`
into the ambient set, as an equivariant map.  -/
SubAddAction.ofFixingAddSubgroup_equivariantMap : (M : Type u_1) →
  {α : Type u_2} →
    [inst : AddGroup M] →
      [inst_1 : AddAction M α] →
        (s : Set α) → ↥(SubAddAction.ofFixingAddSubgroup M s) →ₑ[⇑(fixingAddSubgroup M s).subtype] α
-- Mathlib.Order.WithBot
WithBot.canLift : ∀ {α : Type u_1}, CanLift (WithBot α) α WithBot.some fun r => r ≠ ⊥
-- Init.Data.SInt.Bitwise
UInt16.toInt16_and : ∀ (a b : UInt16), (a &&& b).toInt16 = a.toInt16 &&& b.toInt16
-- Mathlib.Data.Fintype.Pigeonhole
/-- If `‖β‖ < ‖α‖` there are no embeddings `α ↪ β`.
This is a formulation of the pigeonhole principle.

Note this cannot be an instance as it needs `h`.  -/
Function.Embedding.isEmpty_of_card_lt : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β],
  Fintype.card β < Fintype.card α → IsEmpty (α ↪ β)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instAbelian : (k : Type u) → (G : Type v) → [inst : Ring k] → [inst_1 : Monoid G] → CategoryTheory.Abelian (Rep.{w, u, v} k G)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.direction_sInf_of_mem_sInf : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (t : Set (AffineSubspace k P)), ∀ p ∈ sInf t, (sInf t).direction = ⨅ s ∈ t, s.direction
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` reflects limits, then `F : C ⥤ Dᵒᵖ` reflects colimits.  -/
CategoryTheory.Limits.reflectsColimitsOfSize_of_leftOp : ∀ {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.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp],
  CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.Data.Rat.Cast.CharZero
Rat.cast_divInt : ∀ {α : Type u_3} [inst : DivisionRing α] [CharZero α] (a b : ℤ), ↑(Rat.divInt a b) = ↑a / ↑b
-- Mathlib.Topology.Spectral.Prespectral
PrespectralSpace.mk : ∀ {X : Type u_3} [inst : TopologicalSpace X],
  TopologicalSpace.IsTopologicalBasis {U | IsOpen U ∧ IsCompact U} → PrespectralSpace X
-- Mathlib.Order.WithBot
WithTop.ofDual_lt_iff : ∀ {α : Type u_1} [inst : LT α] {x : WithBot α} {y : WithTop αᵒᵈ}, WithTop.ofDual y < x ↔ WithBot.toDual x < y
-- Mathlib.CategoryTheory.Monad.Basic
/-- The unit for the monad.  -/
CategoryTheory.Monad.η : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (self : CategoryTheory.Monad C) → CategoryTheory.Functor.id C ⟶ self.toFunctor
-- Mathlib.Data.QPF.Univariate.Basic
/-- coinductive type defined as the final coalgebra of a qpf  -/
QPF.Cofix : (F : Type u → Type u) → [q : QPF F] → Type u
-- Mathlib.Topology.Algebra.Constructions
MulOpposite.comap_op_nhds : ∀ {M : Type u_1} [inst : TopologicalSpace M] (x : Mᵐᵒᵖ),
  Filter.comap MulOpposite.op (nhds x) = nhds (MulOpposite.unop x)
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.weightedHomogeneousComponent_mem : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M)
  (φ : MvPolynomial σ R) (m : M),
  (MvPolynomial.weightedHomogeneousComponent w m) φ ∈ MvPolynomial.weightedHomogeneousSubmodule R w m
-- Lean.Data.Lsp.Internal
Lean.Lsp.ImportInfo.mk : String → Bool → Bool → Bool → Lean.Lsp.ImportInfo