mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Filtered.Basic
/-- `coeq_condition f f'`, for morphisms `f f' : j ⟶ j'`, is the proof that
`f ≫ coeqHom f f' = f' ≫ coeqHom f f'`.
 -/
CategoryTheory.IsFiltered.coeq_condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {j j' : C}
  (f f' : j ⟶ j') {Z : C} (h : CategoryTheory.IsFiltered.coeq f f' ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsFiltered.coeqHom f f') h) =
    CategoryTheory.CategoryStruct.comp f'
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsFiltered.coeqHom f f') h)
-- Mathlib.Order.UpperLower.Fibration
Relation.fibration_iff_isLowerSet_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : LE β],
  Relation.Fibration (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) f ↔ ∀ (s : Set α), IsLowerSet s → IsLowerSet (f '' s)
-- Lean.Meta.HaveTelescope
Lean.Meta.ZetaUnusedMode.singlePass.sizeOf_spec : sizeOf Lean.Meta.ZetaUnusedMode.singlePass = 1
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.cons.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (rank : ℕ) (val : α) (node : Batteries.BinomialHeap.Imp.HeapNode α)
  (next : Batteries.BinomialHeap.Imp.Heap α),
  sizeOf (Batteries.BinomialHeap.Imp.Heap.cons rank val node next) =
    1 + sizeOf rank + sizeOf val + sizeOf node + sizeOf next
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.insertMin.match_3.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → Sort u_3) (sz : ℕ)
  (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
  (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced)
  (h_1 : (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) → motive Std.DTreeMap.Internal.Impl.leaf hr)
  (h_2 :
    (sz : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l' r' : Std.DTreeMap.Internal.Impl α β) →
            (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced) →
              motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr),
  (match Std.DTreeMap.Internal.Impl.inner sz k' v' l' r', hr with
    | Std.DTreeMap.Internal.Impl.leaf, hr => h_1 hr
    | Std.DTreeMap.Internal.Impl.inner sz k' v' l' r', hr => h_2 sz k' v' l' r' hr) =
    h_2 sz k' v' l' r' hr
-- Lean.Environment
_private.Lean.Environment.0.Lean.EnvExtension.modifyState.unsafe_1 : {σ : Type} → Lean.EnvExtension σ → Lean.Environment → (σ → σ) → Array Lean.EnvExtensionState
-- Qq.AssertInstancesCommute
Qq.doElemAssertInstancesCommute : Lean.ParserDescr
-- Std.Http.Data.URI.Basic
/-- A numeric port value is present (for example, `example.com:443`).
 -/
Std.Http.URI.Port.value : UInt16 → Std.Http.URI.Port
-- Mathlib.Topology.Category.LightProfinite.Cartesian
LightProfinite.instCartesianMonoidalCategory : CategoryTheory.CartesianMonoidalCategory LightProfinite
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.let.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {decl : Lean.Compiler.LCNF.LetDecl pu} {k : Lean.Compiler.LCNF.Code pu}
  {decl_1 : Lean.Compiler.LCNF.LetDecl pu} {k_1 : Lean.Compiler.LCNF.Code pu},
  Lean.Compiler.LCNF.Code.let decl k = Lean.Compiler.LCNF.Code.let decl_1 k_1 → decl = decl_1 ∧ k = k_1
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.instSmulZeroClassRight : {𝕜 : Type u_2} →
  {α : Type u_5} →
    {M : Type u_7} → [inst : Zero 𝕜] → [inst_1 : LE α] → [SMulZeroClass M 𝕜] → SMulZeroClass M (IncidenceAlgebra 𝕜 α)
-- Mathlib.Order.Filter.Cofinite
Set.infinite_iff_frequently_cofinite : ∀ {α : Type u_2} {s : Set α}, s.Infinite ↔ ∃ᶠ (x : α) in Filter.cofinite, x ∈ s
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.epi_iff_mk_eq_top : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Balanced C] (f : X ⟶ Y)
  [inst_2 : CategoryTheory.Mono f], CategoryTheory.Epi f ↔ CategoryTheory.Subobject.mk f = ⊤
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.levelsEqualUpToIdsCore : Lean.Level → Lean.Level → Aesop.EqualUpToIdsM Bool
-- Mathlib.Analysis.Normed.Algebra.Unitization
Unitization.isUniformEmbedding_addEquiv : ∀ {A : Type u_2} [inst : NonUnitalNormedRing A] {𝕜 : Type u_3} [inst_1 : NontriviallyNormedField 𝕜],
  IsUniformEmbedding ⇑(Unitization.addEquiv 𝕜 A)
-- Mathlib.Analysis.Convex.Cone.InnerDual
ProperCone.innerDual_sUnion : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : CompleteSpace E]
  (S : Set (Set E)), ProperCone.innerDual (⋃₀ S) = sInf (ProperCone.innerDual '' S)
-- Mathlib.Order.Filter.Pointwise
Filter.vadd_pure : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f : Filter α} {b : β}, f +ᵥ pure b = Filter.map (fun x => x +ᵥ b) f
-- Lean.Expr
Lean.Expr.hash : Lean.Expr → UInt64
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- **Alias** of `MeasureTheory.StronglyMeasurable.fun_const_vadd`.

---

Eta-expanded form of `MeasureTheory.StronglyMeasurable.const_vadd` -/
MeasureTheory.StronglyMeasurable.const_vadd' : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] {𝕜 : Type u_5}
  [inst_1 : VAdd 𝕜 β] [ContinuousConstVAdd 𝕜 β],
  MeasureTheory.StronglyMeasurable f → ∀ (c : 𝕜), MeasureTheory.StronglyMeasurable fun i => c +ᵥ f i
-- Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
/-- The functor establishing the equivalence `StructuredArrow.commaMapEquivalence`.  -/
CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {L : CategoryTheory.Functor C T} →
              {R : CategoryTheory.Functor D T} →
                {C' : Type u₄} →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} C'] →
                    {D' : Type u₅} →
                      [inst_4 : CategoryTheory.Category.{v₅, u₅} D'] →
                        {T' : Type u₆} →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] →
                            {L' : CategoryTheory.Functor C' T'} →
                              {R' : CategoryTheory.Functor D' T'} →
                                {F₁ : CategoryTheory.Functor C C'} →
                                  {F₂ : CategoryTheory.Functor D D'} →
                                    {F : CategoryTheory.Functor T T'} →
                                      (α : F₁.comp L' ⟶ L.comp F) →
                                        (β : R.comp F ⟶ F₂.comp R') →
                                          [inst_6 : CategoryTheory.IsIso β] →
                                            (X : CategoryTheory.Comma L' R') →
                                              CategoryTheory.Functor
                                                (CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β))
                                                (CategoryTheory.Comma
                                                  (CategoryTheory.StructuredArrow.map₂
                                                    (CategoryTheory.CategoryStruct.id (L'.obj X.left)) α)
                                                  (CategoryTheory.StructuredArrow.map₂ X.hom (CategoryTheory.inv β)))
-- Mathlib.Order.Interval.Finset.Basic
Finset.filter_gt_eq_Iio : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] {a : α} [inst_2 : Fintype α]
  [inst_3 : DecidablePred fun x => x < a], {x | x < a} = Finset.Iio a
-- Mathlib.Algebra.Tropical.Basic
Tropical.surjective_trop : ∀ {R : Type u}, Function.Surjective Tropical.trop
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
ENNReal.measurable_toNNReal : Measurable ENNReal.toNNReal
-- Mathlib.Data.Sym.Basic
Sym.cast.congr_simp : ∀ {α : Type u_1} {n m : ℕ} (h : n = m), Sym.cast h = Sym.cast h
-- Aesop.Tree.Data
Aesop.Goal.unsafeQueue : Aesop.Goal → Aesop.UnsafeQueue
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- The adjoint triple `H.op ⊣ G.op ⊣ F.op` dual to an adjoint triple `F ⊣ G ⊣ H`.  -/
CategoryTheory.Adjunction.Triple.op : {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} →
          {G : CategoryTheory.Functor D C} →
            {H : CategoryTheory.Functor C D} →
              CategoryTheory.Adjunction.Triple F G H → CategoryTheory.Adjunction.Triple H.op G.op F.op
-- Std.Async.Process
/-- Returns the total system memory in bytes.
 -/
Std.IO.Process.totalMemory : IO UInt64
-- Mathlib.Topology.MetricSpace.HausdorffAlexandroff
cantorToHilbert_continuous : Continuous cantorToHilbert
-- Mathlib.Analysis.SpecialFunctions.CompareExp
Complex.IsExpCmpFilter.isBigO_im_pow_re : ∀ {l : Filter ℂ}, Complex.IsExpCmpFilter l → ∀ (n : ℕ), (fun z => z.im ^ n) =O[l] fun z => Real.exp z.re
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- The character of level `d` through which `χ` factors is uniquely determined.  -/
DirichletCharacter.FactorsThrough.existsUnique : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} {χ : DirichletCharacter R n} {d : ℕ} [NeZero n]
  (h : χ.FactorsThrough d), ∃! χ', χ = (DirichletCharacter.changeLevel ⋯) χ'
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.coe_coindV : ∀ {R : Type u_1} {V : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace V]
  [inst_3 : IsTopologicalAddGroup V] [inst_4 : Module R V] {G : Type u_7} {H : Type u_8} [inst_5 : Group G]
  [inst_6 : TopologicalSpace G] [inst_7 : TopologicalSpace R] [inst_8 : ContinuousSMul R V] [inst_9 : Group H]
  [inst_10 : TopologicalSpace H] (φ : G →ₜ* H) (π : ContRepresentation R G V),
  ↑(ContRepresentation.coindV φ π) = {f | ∀ (g : G) (h : H), f (φ g * h) = (π g) (f h)}
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.map_appTop_coord : ∀ {n : Type u} {S T : AlgebraicGeometry.Scheme} (f : S ⟶ T) (i : n),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.AffineSpace.map n f)))
      (AlgebraicGeometry.AffineSpace.coord T i) =
    AlgebraicGeometry.AffineSpace.coord S i
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.lift_unique : ∀ {A : Type u_4} [inst : CommRing A] {K : Type u_5} [inst_1 : Field K] {L : Type u_7} [inst_2 : Field L]
  [inst_3 : Algebra A K] [inst_4 : IsFractionRing A K] {g : A →+* L} (hg : Function.Injective ⇑g) {f : K →+* L},
  (∀ (x : A), f ((algebraMap A K) x) = g x) → IsFractionRing.lift hg = f
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.bicategoricalComp_refl : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
  CategoryTheory.bicategoricalComp η θ = CategoryTheory.CategoryStruct.comp η θ
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Expr : Type
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.isoWhiskerLeft_right : ∀ {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] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) {G H : CategoryTheory.Functor C D}
  (α : G ≅ H) (K : CategoryTheory.Functor D E),
  F.isoWhiskerLeft (CategoryTheory.Functor.isoWhiskerRight α K) =
    (F.associator G K).symm ≪≫ CategoryTheory.Functor.isoWhiskerRight (F.isoWhiskerLeft α) K ≪≫ F.associator H K
-- Lean.Meta.Tactic.Grind.Types
/-- Checks invariants of all registered solvers.  -/
Lean.Meta.Grind.Solvers.checkInvariants : Lean.Meta.Grind.GoalM Unit
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.d₁₂_apply_mem_cocycles₂ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G} (x : G → ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.d₁₂ A)) x ∈ groupCohomology.cocycles₂ A
-- Lean.Elab.Arg
Lean.Elab.Term.NamedArg.mk : Lean.Syntax → Lean.Name → Lean.Elab.Term.Arg → ℕ → Lean.Elab.Term.NamedArg
-- Mathlib.Topology.Bornology.Basic
Bornology.isCobounded_ofBounded_iff : ∀ {α : Type u_2} {s : Set α} (B : Set (Set α)) {empty_mem : ∅ ∈ B} {subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B}
  {union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B} {sUnion_univ : ∀ (x : α), {x} ∈ B}, Bornology.IsCobounded s ↔ sᶜ ∈ B
-- Std.Sat.CNF.Basic
Std.Sat.CNF.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (clauses : Array (Std.Sat.CNF.Clause α)),
  sizeOf { clauses := clauses } = 1 + sizeOf clauses
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- This is a slightly more convenient method to verify that a cokernel cofork is a colimit cocone.
It only asks for a proof of facts that carry any mathematical content  -/
CategoryTheory.Limits.isColimitAux : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          (t : CategoryTheory.Limits.CokernelCofork f) →
            (desc : (s : CategoryTheory.Limits.CokernelCofork f) → t.pt ⟶ s.pt) →
              (∀ (s : CategoryTheory.Limits.CokernelCofork f),
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π t) (desc s) =
                    CategoryTheory.Limits.Cofork.π s) →
                (∀ (s : CategoryTheory.Limits.CokernelCofork f) (m : t.pt ⟶ s.pt),
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π t) m =
                        CategoryTheory.Limits.Cofork.π s →
                      m = desc s) →
                  CategoryTheory.Limits.IsColimit t
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.getElem_sdiv.match_1.eq_2 : ∀ (motive : Bool → Bool → Sort u_1) (h_1 : Unit → motive false false) (h_2 : Unit → motive false true)
  (h_3 : Unit → motive true false) (h_4 : Unit → motive true true),
  (match false, true with
    | false, false => h_1 ()
    | false, true => h_2 ()
    | true, false => h_3 ()
    | true, true => h_4 ()) =
    h_2 ()
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasStrictFDerivAt.neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E}, HasStrictFDerivAt f f' x → HasStrictFDerivAt (-f) (-f') x
-- Mathlib.Topology.Algebra.ConstMulAction
Homeomorph.smul.eq_1 : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [inst_3 : ContinuousConstSMul G α] (γ : G),
  Homeomorph.smul γ = { toEquiv := MulAction.toPerm γ, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- Two vectors have inner product 0 if and only if the angle between
them is π/2.  -/
InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  inner ℝ x y = 0 ↔ InnerProductGeometry.angle x y = Real.pi / 2
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.measurableCylinders.eq_1 : ∀ {ι : Type u_2} (α : ι → Type u_1) [inst : (i : ι) → MeasurableSpace (α i)],
  MeasureTheory.measurableCylinders α = ⋃ s, ⋃ S, ⋃ (_ : MeasurableSet S), {MeasureTheory.cylinder s S}
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.realizeValue.unsafe_10 : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → NonScalar → Lean.PHashMap α (Task Dynamic)
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.mk_le_mk : ∀ {M : Type u_1} [inst : MulOneClass M] {s t : Subsemigroup M} (h_one : 1 ∈ s.carrier) (h_one' : 1 ∈ t.carrier),
  { toSubsemigroup := s, one_mem' := h_one } ≤ { toSubsemigroup := t, one_mem' := h_one' } ↔ s ≤ t
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.toOverUnit_obj_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : C), ((CategoryTheory.toOverUnit C).obj X).hom = CategoryTheory.SemiCartesianMonoidalCategory.toUnit X
-- Init.Data.List.Lemmas
List.map_dropLast : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α}, List.map f l.dropLast = (List.map f l).dropLast
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.HasHomotopyFiber.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} {F G : HomologicalComplex C c} {φ : F ⟶ G},
  (∀ (i j : α), c.Rel i j → CategoryTheory.Limits.HasBinaryBiproduct (G.X i) (F.X j)) →
    HomologicalComplex.HasHomotopyFiber φ
-- Mathlib.Order.Basic
DenselyOrdered.mk : ∀ {α : Type u_5} [inst : LT α], (∀ (a₁ a₂ : α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂) → DenselyOrdered α
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.of_injective : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (i : ι), Function.Injective ⇑Monoid.CoprodI.of
-- Mathlib.Combinatorics.Enumerative.Catalan.Tree
BinaryTree.treesOfNumNodesEq.eq_1 : BinaryTree.treesOfNumNodesEq 0 = {BinaryTree.nil}
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Equiv.trans_apply : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} {E' : Type u_4} [inst_3 : AddGroup E'] {S' : AddGroupExtension N E' G}
  (equiv : S.Equiv S') {E'' : Type u_5} [inst_4 : AddGroup E''] {S'' : AddGroupExtension N E'' G}
  (equiv' : S'.Equiv S'') (a : E), (equiv.trans equiv') a = equiv' (equiv a)
-- Mathlib.Algebra.Category.Ring.FilteredColimits
CommRingCat.FilteredColimits.forget₂Ring_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ CommRingCat RingCat)
-- Init.Data.Nat.Basic
Nat.le_or_eq_of_le_add_one : ∀ {m n : ℕ}, m ≤ n + 1 → m ≤ n ∨ m = n + 1
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.coe_sub : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) (x y : ↥s), ↑(x - y) = ↑x - ↑y
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Summable.tsum_pos : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : AddCommGroup α] [inst_1 : PartialOrder α]
  [IsOrderedAddMonoid α] [inst_3 : TopologicalSpace α] [IsTopologicalAddGroup α] [OrderClosedTopology α] {g : ι → α}
  [L.LeAtTop] [L.NeBot], Summable g L → (∀ (i : ι), 0 ≤ g i) → ∀ (i : ι), 0 < g i → 0 < ∑'[L] (i : ι), g i
-- Mathlib.Data.Finset.Basic
Finset.inter_erase : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s t : Finset α), s ∩ t.erase a = (s ∩ t).erase a
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.MonoidalCategory.instMonoidalCategoryStruct : {R : Type u} → [inst : CommRing R] → CategoryTheory.MonoidalCategoryStruct (ModuleCat R)
-- Mathlib.GroupTheory.Finiteness
Submonoid.iSup_map_mulSingle : ∀ {ι : Type u_3} [Finite ι] {M : ι → Type u_4} [inst : (i : ι) → Monoid (M i)] {P : (i : ι) → Submonoid (M i)}
  [inst_1 : DecidableEq ι], ⨆ i, Submonoid.map (MonoidHom.mulSingle M i) (P i) = Submonoid.pi Set.univ P
-- Mathlib.LinearAlgebra.Dual.Defs
Module.mapEvalEquiv_apply : ∀ (R : Type u_3) (M : Type u_4) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.IsReflexive R M] (W : Submodule R M),
  (Module.mapEvalEquiv R M) W = Submodule.map (Module.Dual.eval R M) W
-- Init.Control.Lawful.MonadAttach.Instances
_private.Init.Control.Lawful.MonadAttach.Instances.0.EStateM.bind.match_1.eq_2 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (e : ε) (s : σ)
  (h_1 : (a : α) → (s : σ) → motive (EStateM.Result.ok a s))
  (h_2 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)),
  (match EStateM.Result.error e s with
    | EStateM.Result.ok a s => h_1 a s
    | EStateM.Result.error e s => h_2 e s) =
    h_2 e s
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.toList_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β}
  {f : (a : α) → β a → Option (γ a)},
  m.WF →
    (Std.DHashMap.Raw.filterMap f m).toList.Perm
      (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) m.toList)
-- Mathlib.CategoryTheory.Localization.Monoidal.Functor
CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_ε : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.MonoidalCategory C] [inst_4 : CategoryTheory.MonoidalCategory D]
  [inst_5 : CategoryTheory.MonoidalCategory E] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [inst_6 : L.IsLocalization W] [inst_7 : L.Monoidal] (F : CategoryTheory.Functor D E) (G : CategoryTheory.Functor C E)
  [inst_8 : G.Monoidal] [inst_9 : W.ContainsIdentities] [inst_10 : CategoryTheory.Localization.Lifting L W G F],
  CategoryTheory.Functor.LaxMonoidal.ε F =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε G)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Localization.Lifting.iso L W G F).inv.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        (F.map (CategoryTheory.Functor.OplaxMonoidal.η L)))
-- Init.Data.String.PosRaw
String.Pos.Raw.offsetBy_unoffsetBy_of_le : ∀ {p q : String.Pos.Raw}, q ≤ p → (p.unoffsetBy q).offsetBy q = p
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
/-- Killing the zeroth coefficient in a formal multilinear series  -/
FormalMultilinearSeries.removeZero : {𝕜 : Type u} →
  {E : Type v} →
    {F : Type w} →
      [inst : Semiring 𝕜] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : Module 𝕜 E] →
            [inst_3 : TopologicalSpace E] →
              [inst_4 : ContinuousAdd E] →
                [inst_5 : ContinuousConstSMul 𝕜 E] →
                  [inst_6 : AddCommMonoid F] →
                    [inst_7 : Module 𝕜 F] →
                      [inst_8 : TopologicalSpace F] →
                        [inst_9 : ContinuousAdd F] →
                          [inst_10 : ContinuousConstSMul 𝕜 F] →
                            FormalMultilinearSeries 𝕜 E F → FormalMultilinearSeries 𝕜 E F
-- Batteries.Data.Array.Scan
Array.getElem_scanl_zero : ∀ {β : Type u_1} {α : Type u_2} {init : β} {as : Array α} {f : β → α → β}, (Array.scanl f init as)[0] = init
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.w' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
  {i : Y ⟶ Z},
  CategoryTheory.CommSq f g h i → CategoryTheory.CategoryStruct.comp g i = CategoryTheory.CategoryStruct.comp f h
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Cokleisli.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Comonad C) (of of_1 : C),
  ({ of := of } = { of := of_1 }) = (of = of_1)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_sdiff_le_sum_sdiff : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M] {f : ι → M}
  {s t : Finset ι} [inst_3 : DecidableEq ι], ∑ i ∈ s \ t, f i ≤ ∑ i ∈ t \ s, f i ↔ ∑ i ∈ s, f i ≤ ∑ i ∈ t, f i
-- Batteries.Recycling.RBTree.Basic
/-- Inserting into a well-formed tree yields another well-formed tree.
(See `Ordered.insert` and `Balanced.insert` for the actual proofs.)  -/
RBTree.RBNode.WF.insert : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : RBTree.RBNode α} {a : α},
  RBTree.RBNode.WF cmp t → RBTree.RBNode.WF cmp (RBTree.RBNode.insert cmp t a)