mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.addAction : {α : Type u_4} →
  {M : Type u_5} →
    [inst : AddMonoid α] →
      [inst_1 : AddZeroClass M] →
        [inst_2 : AddAction α M] → [VAddAssocClass α M M] → (c : AddCon M) → AddAction α c.Quotient
-- Mathlib.Algebra.Order.Monoid.Lex
OrderMonoidHom.snd_comp_inl : ∀ (α : Type u_1) (β : Type u_2) [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : Monoid β] [inst_3 : Preorder β],
  (OrderMonoidHom.snd α β).comp (OrderMonoidHom.inl α β) = 1
-- Mathlib.Order.Filter.IsBounded
Filter.isBoundedUnder_ge_add : ∀ {α : Type u_5} {f : Filter α} {R : Type u_6} [inst : Preorder R] [inst_1 : Add R] [AddLeftMono R] [AddRightMono R]
  {u v : α → R},
  Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f u →
    Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f v → Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f (u + v)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.initialBound_le_bound : ∀ (ε : ℝ) (l : ℕ), SzemerediRegularity.initialBound ε l ≤ SzemerediRegularity.bound ε l
-- Mathlib.Data.FinEnum.Option
/-- For an empty type, the recursion principle evaluates to whatever `congr`
makes of the base case.
 -/
FinEnum.recEmptyOption_of_card_eq_zero : ∀ {P : Type u → Sort v} (finChoice : (n : ℕ) → Fin (n + 1))
  (congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → FinEnum.card β = FinEnum.card α → P α → P β)
  (empty : P PEmpty.{u + 1}) (option : {α : Type u} → FinEnum α → P α → P (Option α)) (α : Type u) [inst : FinEnum α]
  (h : FinEnum.card α = 0) (x : FinEnum PEmpty.{u + 1}),
  FinEnum.recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option) α = congr x inst ⋯ empty
-- Mathlib.Order.CompleteLattice.Defs
sInf_lt_iff : ∀ {α : Type u_1} [inst : CompleteLinearOrder α] {s : Set α} {b : α}, sInf s < b ↔ ∃ a ∈ s, a < b
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.op_intCast : ∀ {R : Type u_1} [inst : IntCast R] (n : ℤ), MulOpposite.op ↑n = ↑n
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
/-- Idempotent operators are equal iff their range and kernels are.  -/
ContinuousLinearMap.IsIdempotentElem.ext_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : M →L[R] M},
  IsIdempotentElem p → IsIdempotentElem q → (p = q ↔ (↑p).range = (↑q).range ∧ (↑p).ker = (↑q).ker)
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Sieve.overEquiv_symm_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Over X}
  (S : CategoryTheory.Sieve Y.left) {Z : CategoryTheory.Over X} (f : Z ⟶ Y),
  ((CategoryTheory.Sieve.overEquiv Y).symm S).arrows f ↔ S.arrows (CategoryTheory.Over.Hom.left f)
-- Mathlib.Order.Hom.BoundedLattice
OrderIsoClass.toSupBotHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : SemilatticeSup α]
  [inst_2 : OrderBot α] [inst_3 : SemilatticeSup β] [inst_4 : OrderBot β] [OrderIsoClass F α β], SupBotHomClass F α β
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Set.image_multiset_sum : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_4} [inst : FunLike F α β] [inst_1 : AddCommMonoid α]
  [inst_2 : AddCommMonoid β] [AddMonoidHomClass F α β] (f : F) (m : Multiset (Set α)),
  ⇑f '' m.sum = (Multiset.map (fun s => ⇑f '' s) m).sum
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.unitsMulDistribMulAction : {M : Type u_2} → [inst : Monoid M] → MulDistribMulAction (ConjAct Mˣ) M
-- Mathlib.GroupTheory.Finiteness
AddSubmonoid.FG.finset_sup : ∀ {M : Type u_1} [inst : AddMonoid M] {ι : Type u_3} (s : Finset ι) (P : ι → AddSubmonoid M),
  (∀ i ∈ s, (P i).FG) → (s.sup P).FG
-- Init.Prelude
/-- The bytes of the string form valid UTF-8.  -/
String.isValidUTF8 : ∀ (self : String), self.toByteArray.IsValidUTF8
-- Mathlib.Topology.Order.AtTopBotIxx
tendsto_Ioi_atBot : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {a : X} {α : Type u_2}
  {l : Filter α} {f : α → ↑(Set.Ioi a)},
  autoParam (Order.IsPredPrelimit a) tendsto_Ioi_atBot._auto_1 →
    (Filter.Tendsto f l Filter.atBot ↔ Filter.Tendsto (fun x => ↑(f x)) l (nhdsWithin a (Set.Ioi a)))
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingSecond_succ_self_left : ∀ (n : ℕ), (n + 1).stirlingSecond n = (n + 1).choose 2
-- Mathlib.Dynamics.FixedPoints.Defs
Function.mem_fixedPoints : ∀ {α : Type u_1} {x : α} {f : α → α}, x ∈ Function.fixedPoints f ↔ Function.IsFixedPt f x
-- Init.Data.SInt.Lemmas
Int16.neg_mul_not_eq_add_mul : ∀ {a b : Int16}, -(a * ~~~b) = a + a * b
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- The type of bounded continuous functions, with the uniform distance, is a metric space.  -/
BoundedContinuousFunction.instMetricSpace : {α : Type u} →
  [inst : TopologicalSpace α] → {β : Type u_2} → [inst_1 : MetricSpace β] → MetricSpace (BoundedContinuousFunction α β)
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
/-- The quadratic character takes the value `1` on nonzero squares.  -/
quadraticChar_sq_one' : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] {a : F},
  a ≠ 0 → (quadraticChar F) (a ^ 2) = 1
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of `Left.neg_neg_iff`.

---

Uses `left` co(ntra)variant.  -/
neg_neg_iff_pos : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a : α}, -a < 0 ↔ 0 < a
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the reverse direction of `lowerSemicontinuousAt_iff_frequently`. -/
LowerSemicontinuousAt.of_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β} {x : α},
  (∀ (y : β), (∃ᶠ (x' : α) in nhds x, f x' ≤ y) → f x ≤ y) → LowerSemicontinuousAt f x
-- Mathlib.Logic.Equiv.Defs
Equiv.bijectiveEquiv_apply : ∀ {α : Sort u} {β : Sort v} (f : { f // Function.Bijective f }), Equiv.bijectiveEquiv f = Equiv.ofBijective ↑f ⋯
-- Mathlib.Topology.Closure
closure_sdiff_frontier : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X), closure s \ frontier s = interior s
-- Mathlib.LinearAlgebra.Pi
/-- Transport dependent functions through an equivalence of the base space.

This is `Equiv.piCongrLeft'` as a `LinearEquiv`.  -/
LinearEquiv.piCongrLeft' : (R : Type u) →
  {ι : Type x} →
    {ι' : Type x'} →
      [inst : Semiring R] →
        (φ : ι → Type u_1) →
          [inst_1 : (i : ι) → AddCommMonoid (φ i)] →
            [inst_2 : (i : ι) → Module R (φ i)] → (e : ι ≃ ι') → ((i' : ι) → φ i') ≃ₗ[R] (i : ι') → φ (e.symm i)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.units_inv_apply_apply : ∀ (f : CircleDeg1Liftˣ) (x : ℝ), ↑f⁻¹ (↑f x) = x
-- Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsISup : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Sort u_1} (P : α → CategoryTheory.ObjectProperty C)
  [∀ (a : α), (P a).IsClosedUnderIsomorphisms], (⨆ a, P a).IsClosedUnderIsomorphisms
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_apply_of_lt_aleph0 : ∀ {c : Cardinal.{u}} (h : c < Cardinal.aleph0), Cardinal.toNat c = Classical.choose ⋯
-- Mathlib.CategoryTheory.CofilteredSystem
/-- If `F` is nonempty at each index and Mittag-Leffler, then so is `F.toEventualRanges`.  -/
CategoryTheory.Functor.toEventualRanges_nonempty : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v))
  [inst_1 : CategoryTheory.IsCofilteredOrEmpty J],
  F.IsMittagLeffler → ∀ [∀ (j : J), Nonempty (F.obj j)] (j : J), Nonempty (F.toEventualRanges.obj j)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpL1_measure_zero : ∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α}
  {f : α → F'} (hm : m ≤ m0), MeasureTheory.condExpL1 hm 0 f = 0
-- Mathlib.SetTheory.ZFC.Ordinal
/-- The von Neumann ordinal corresponding to a given `Ordinal`, as a `ZFSet`.

The elements of `o.toZFSet` are all `a.toZFSet` with `a < o`.  -/
Ordinal.toZFSet : Ordinal.{u} → ZFSet.{u}
-- Mathlib.Algebra.Notation.Pi.Defs
Function.smul_const : ∀ {ι : Type u_1} {M : Type u_7} {α : Type u_2} [inst : SMul α M] (b : α) (a : M),
  b • Function.const ι a = Function.const ι (b • a)
-- Mathlib.Data.Nat.Cast.Commute
Nat.cast_add_one_comm : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] (n : ℕ), ↑n + 1 = 1 + ↑n
-- Mathlib.Order.Notation
Bot.ext : ∀ {α : Type u_1} {x y : Bot α}, ⊥ = ⊥ → x = y
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- Composition of morphisms of locally ringed spaces.  -/
AlgebraicGeometry.LocallyRingedSpace.comp : {X Y Z : AlgebraicGeometry.LocallyRingedSpace} → X.Hom Y → Y.Hom Z → X.Hom Z
-- Mathlib.SetTheory.ZFC.PSet
/-- The pre-set union operator  -/
PSet.sUnion : PSet.{u_1} → PSet.{u_1}
-- Mathlib.Data.Set.Finite.Basic
Set.fintypeSep : {α : Type u} → (s : Set α) → (p : α → Prop) → [Fintype ↑s] → [DecidablePred p] → Fintype ↑{a | a ∈ s ∧ p a}
-- Lean.Parser.Do
Lean.Parser.Term.doRepeatUntil : Lean.Parser.Parser
-- Mathlib.Algebra.Vertex.HVertexOperator
HVertexOperator.of_coeff_coeff : ∀ {Γ : Type u_1} [inst : PartialOrder Γ] {R : Type u_2} {V : Type u_3} {W : Type u_4} [inst_1 : CommRing R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddCommGroup W] [inst_5 : Module R W]
  (A : HVertexOperator Γ R V W), HVertexOperator.of_coeff (HVertexOperator.coeff A) ⋯ = A
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
AlgebraicGeometry.Proj.affineOpenCover.eq_1 : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜],
  AlgebraicGeometry.Proj.affineOpenCover 𝒜 =
    AlgebraicGeometry.Proj.affineOpenCoverOfIrrelevantLESpan 𝒜 (fun i => ↑i.snd) ⋯ ⋯ ⋯
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.precheckBinopLazy : Lean.Elab.Term.Quotation.Precheck
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.MsgEmbed.brecOn_4.go : {motive_1 : Lean.Widget.MsgEmbed → Sort u} →
  {motive_2 : Lean.Widget.TaggedText Lean.Widget.MsgEmbed → Sort u} →
    {motive_3 :
        Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
            (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren) →
          Sort u} →
      {motive_4 : Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Sort u} →
        {motive_5 : List (Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Sort u} →
          (t : List (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) →
            ((t : Lean.Widget.MsgEmbed) → t.below → motive_1 t) →
              ((t : Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Lean.Widget.MsgEmbed.below_1 t → motive_2 t) →
                ((t :
                      Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
                        (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren)) →
                    Lean.Widget.MsgEmbed.below_2 t → motive_3 t) →
                  ((t : Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) →
                      Lean.Widget.MsgEmbed.below_3 t → motive_4 t) →
                    ((t : List (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) →
                        Lean.Widget.MsgEmbed.below_4 t → motive_5 t) →
                      motive_5 t ×' Lean.Widget.MsgEmbed.below_4 t
-- Lean.Parser.Command
Lean.Parser.Command.abbrev.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Algebra.Algebra
Algebra.elemental.le_centralizer_centralizer : ∀ (R : Type u_1) [inst : CommSemiring R] {A : Type u} [inst_1 : TopologicalSpace A] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : IsSemitopologicalSemiring A] [T2Space A] (x : A),
  Algebra.elemental R x ≤ Subalgebra.centralizer R ↑(Subalgebra.centralizer R {x})
-- Init.Data.Vector.Nat
Vector.prod_eq_zero_iff_exists_zero_nat : ∀ {n : ℕ} {xs : Vector ℕ n}, xs.prod = 0 ↔ ∃ x ∈ xs, x = 0
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.HalfBraiding.naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X : C}
  (self : CategoryTheory.HalfBraiding X) {U U' : C} (f : U ⟶ U'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (self.β U').hom =
    CategoryTheory.CategoryStruct.comp (self.β U).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α},
  l.contains k = false → (Std.HashSet.ofList l).getD k fallback = fallback
-- Mathlib.Algebra.Homology.ShortComplex.Ab
/-- The explicit left homology data of a short complex of abelian group that is
given by a kernel and a quotient given by the `AddMonoidHom` API.  -/
CategoryTheory.ShortComplex.abLeftHomologyData : (S : CategoryTheory.ShortComplex Ab) → S.LeftHomologyData
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey_unitOfList_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l →
      k ∈ l → ∀ {h' : k' ∈ Std.DHashMap.Raw.Const.unitOfList l}, (Std.DHashMap.Raw.Const.unitOfList l).getKey k' h' = k
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isEmpty_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering}, ∅.isEmpty = true
-- Mathlib.Analysis.Normed.Module.Convex
convex_closedBall : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (a : E) (r : ℝ),
  Convex ℝ (Metric.closedBall a r)
-- Mathlib.GroupTheory.ArchimedeanDensely
instWellFoundedGTWithZeroMultiplicativeIntLeOne : WellFoundedGT { v // v ≤ 1 }
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval_add : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p q : MvPolynomial σ R} {f : σ → R},
  (MvPolynomial.eval f) (p + q) = (MvPolynomial.eval f) p + (MvPolynomial.eval f) q
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.mul_sub_right_right_iff : ∀ {R : Type u} [inst : CommRing R] {x y z : R}, IsCoprime x (z * x - y) ↔ IsCoprime x y
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.NormalizedHom.nil.injEq : ∀ (e : Mathlib.Tactic.BicategoryLike.Mor₁) (a : Mathlib.Tactic.BicategoryLike.Obj)
  (e_1 : Mathlib.Tactic.BicategoryLike.Mor₁) (a_1 : Mathlib.Tactic.BicategoryLike.Obj),
  (Mathlib.Tactic.BicategoryLike.NormalizedHom.nil e a = Mathlib.Tactic.BicategoryLike.NormalizedHom.nil e_1 a_1) =
    (e = e_1 ∧ a = a_1)
-- Init.Data.String.Basic
String.Pos.ofCopy_inj : ∀ {s : String.Slice} {pos pos' : s.copy.Pos}, pos.ofCopy = pos'.ofCopy ↔ pos = pos'
-- Mathlib.Tactic.DefEqAbuse
_private.Mathlib.Tactic.DefEqAbuse.0.Lean.MessageData.VisitStep.descend.inj : ∀ {α : Type u_1} {butFirst butFirst_1 : Option α},
  Lean.MessageData.VisitStep.descend✝ butFirst = Lean.MessageData.VisitStep.descend✝ butFirst_1 → butFirst = butFirst_1
-- Mathlib.Order.Circular
/-- **Alias** of `not_btw_of_sbtw`. -/
SBtw.sbtw.not_btw : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → ¬btw c b a
-- Std.Http.Data.Status
Std.Http.Status.unauthorized.sizeOf_spec : sizeOf Std.Http.Status.unauthorized = 1
-- Init.Data.UInt.Lemmas
UInt8.lt_or_eq_of_le : ∀ {a b : UInt8}, a ≤ b → a < b ∨ a = b
-- Init.Data.Array.Lemmas
Array.foldl_toList_eq_map : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {acc : Array β} {G : α → β},
  (List.foldl (fun acc a => acc.push (G a)) acc l).toList = acc.toList ++ List.map G l
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
/-- The distinguished triangle attached to a spectral object `E : SpectralObject C ι`
and composable morphisms `f : i ⟶ j` and `g : j ⟶ k` in `ι`.  -/
CategoryTheory.Triangulated.SpectralObject.triangle : {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.Limits.HasZeroObject C] →
          [inst_3 : CategoryTheory.HasShift C ℤ] →
            [inst_4 : CategoryTheory.Preadditive C] →
              [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                [inst_6 : CategoryTheory.Pretriangulated C] →
                  CategoryTheory.Triangulated.SpectralObject C ι →
                    {i j k : ι} → (i ⟶ j) → (j ⟶ k) → CategoryTheory.Pretriangulated.Triangle C
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn'_roo : ∀ {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [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] [inst_4 : LT α]
  [inst_5 : DecidableLT α] [inst_6 : Std.PRange.UpwardEnumerable α] [inst_7 : Std.Rxo.IsAlwaysFinite α]
  [inst_8 : Std.PRange.LawfulUpwardEnumerable α] [inst_9 : Std.PRange.LawfulUpwardEnumerableLT α] {xs : Std.Roo α}
  {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Std.Internal.Do.Invariant xs.toList β Pred)
  {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur ⋯ b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ forIn' xs init f ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Mathlib.Algebra.GroupWithZero.Invertible
mul_inv_cancel_of_invertible : ∀ {α : Type u} [inst : GroupWithZero α] (a : α) [Invertible a], a * a⁻¹ = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullback.diagonal_snd_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullback f f] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f f) h) =
    h
-- Init.Data.List.Basic
List.tail?_nil : ∀ {α : Type u}, [].tail? = none
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Fintype.prod_fiberwise' : ∀ {M : Type u_4} {κ : Type u_6} {ι : Type u_7} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : CommMonoid M]
  [inst_3 : DecidableEq κ] (g : ι → κ) (f : κ → M), ∏ j, ∏ _i, f j = ∏ i, f (g i)
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
CategoryTheory.Functor.Fiber.instFaithfulFiberInclusion : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} {S : 𝒮}, CategoryTheory.Functor.Fiber.fiberInclusion.Faithful
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.openCell_subset_closedCell`. -/
Topology.CWComplex.openCell_subset_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.openCell n i ⊆ Topology.RelCWComplex.closedCell n i
-- Mathlib.Algebra.Ring.GeomSum
geom_sum_succ' : ∀ {R : Type u_1} [inst : Semiring R] {x : R} {n : ℕ},
  ∑ i ∈ Finset.range (n + 1), x ^ i = x ^ n + ∑ i ∈ Finset.range n, x ^ i
-- Mathlib.CategoryTheory.Comma.Over.StrictInitial
CategoryTheory.underEquivOfIsTerminal_counitIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X),
  (CategoryTheory.underEquivOfIsTerminal.{w, v_1, u_1} X h).counitIso =
    CategoryTheory.Iso.refl
      ((CategoryTheory.Functor.fromPUnit (CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.id X))).comp
        (CategoryTheory.Functor.star (CategoryTheory.Under X)))
-- Mathlib.Order.SymmDiff
le_symmDiff_iff_right : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a b : α), b ≤ symmDiff a b ↔ Disjoint a b
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.instLieRingOfTwoCocycle : {R : Type u_1} →
  {L : Type u_3} →
    {M : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [inst_6 : LieModule R L M] →
                    (c : ↥(LieModule.Cohomology.twoCocycle R L M)) → LieRing (LieAlgebra.ofTwoCocycle c)
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
/-- The isomorphism `eB.functor ⋙ e'.inverse ⋙ e'.functor ≅ eB.functor` deduced
from the counit isomorphism of `e'`.  -/
AlgebraicTopology.DoldKan.Compatibility.τ₀ : {A' : Type u_2} →
  {B : Type u_3} →
    {B' : Type u_4} →
      [inst : CategoryTheory.Category.{v_2, u_2} A'] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} B] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] →
            {eB : B ≌ B'} → {e' : A' ≌ B'} → eB.functor.comp (e'.inverse.comp e'.functor) ≅ eB.functor
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Functor.mapComon_obj_comon_comul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] (A : CategoryTheory.Comon C),
  CategoryTheory.ComonObj.comul =
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.ComonObj.comul)
      (CategoryTheory.Functor.OplaxMonoidal.δ F A.X A.X)
-- Init.Data.SInt.Lemmas
Int32.neg_add_mul_eq_mul_not : ∀ {a b : Int32}, -(a + a * b) = a * ~~~b
-- Mathlib.Topology.Compactness.Lindelof
Set.Subsingleton.isLindelof : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, s.Subsingleton → IsLindelof s
-- Batteries.Data.List.Basic
/-- `go : List α → Array (List α) → Array (List α)` handles the insertion of
a new list into all the lists in the array:
`go [a, b, c] #[l₁, l₂, l₃] = #[a::l₁, b::l₂, c::l₃]`.
If the new list is too short, the later lists are unchanged, and if it is too long
the array is extended:
```
go [a] #[l₁, l₂, l₃] = #[a::l₁, l₂, l₃]
go [a, b, c, d] #[l₁, l₂, l₃] = #[a::l₁, b::l₂, c::l₃, [d]]
```
 -/
List.transpose.go : {α : Type u_1} → List α → Array (List α) → Array (List α)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_map : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {β : Type u_10}
  [inst_6 : MeasurableSpace β] {φ : X → β},
  Measurable φ →
    ∀ {f : β → E},
      MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map φ μ.variation) →
        μ.Integrable (f ∘ φ) → ∫ᵛ (y : β), f y ∂[B; μ.map φ] = ∫ᵛ (x : X), f (φ x) ∂[B; μ]
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.secondCountableTopology : ∀ {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis b → b.Countable → SecondCountableTopology α
-- Mathlib.Algebra.Category.CommHopfAlgCat
commHopfAlgCatEquivCogrpCommAlgCat_counitIso_inv_app : ∀ (R : Type u) [inst : CommRing R] (X : (CategoryTheory.Grp (CommAlgCat R)ᵒᵖ)ᵒᵖ),
  (commHopfAlgCatEquivCogrpCommAlgCat R).counitIso.inv.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
/-- The weighted limit of `F` for the weight `coyoneda.obj (op j)` is `F.obj j`.  -/
CategoryTheory.Limits.WeightedCone.isLimitCoyoneda : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        (F : CategoryTheory.Functor J C) → (j : J) → (CategoryTheory.Limits.WeightedCone.coyoneda F j).IsLimit