mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.subst.inj : ∀ {x : Int.Internal.Linear.Var} {c₁ : Lean.Meta.Grind.Arith.Cutsat.EqCnstr}
  {c₂ : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr} {x_1 : Int.Internal.Linear.Var}
  {c₁_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr} {c₂_1 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr},
  Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.subst x c₁ c₂ =
      Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.subst x_1 c₁_1 c₂_1 →
    x = x_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicones.functoriality_map_hom : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [inst_2 : CategoryTheory.Category.{uD', uD} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : J → C) (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms] {X Y : CategoryTheory.Limits.Bicone F} (f : X ⟶ Y),
  ((CategoryTheory.Limits.Bicones.functoriality F G).map f).hom = G.map f.hom
-- Mathlib.FieldTheory.NormalizedTrace
/-- The normalized trace map is non-trivial.  -/
Algebra.normalizedTrace_ne_zero : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] [inst_3 : CharZero F]
  [inst_4 : Algebra.IsIntegral F K], Algebra.normalizedTrace F K ≠ 0
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.coe_coalgHom_mk : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  {f : A →ₗc[R] B} (h : f.toFun 1 = 1) (h₁ : ∀ (x y : A), f.toFun (x * y) = f.toFun x * f.toFun y),
  ↑{ toCoalgHom := f, map_one' := h, map_mul' := h₁ } = f
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.prod_apply : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} {γ : Type u_5} {δ : Type u_6} [inst : SMul M α] [inst_1 : SMul N γ]
  [inst_2 : SMul N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : α →ₑ[σ] δ), ⇑(f.prod g) = fun x => (f x, g x)
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.iInf_normalizer_le_normalizer_iInf : ∀ {G : Type u_1} [inst : Group G] {ι : Sort u_6} (H : ι → Subgroup G),
  ⨅ i, Subgroup.normalizer ↑(H i) ≤ Subgroup.normalizer ↑(⨅ i, H i)
-- Mathlib.Algebra.Order.Ring.Pow
/-- Bernoulli's inequality for `b / a`, written after multiplication by the denominators.

This version works for partially ordered commutative semirings,
but explicitly assumes that `b ^ 2` and `(a + b) ^ 2` are nonnegative.  -/
pow_add_mul_le_add_pow_of_sq_nonneg : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] {a b : R},
  0 ≤ a → 0 ≤ b ^ 2 → 0 ≤ (a + b) ^ 2 → 0 ≤ 2 * a + b → ∀ (n : ℕ), a ^ n + ↑n * a ^ (n - 1) * b ≤ (a + b) ^ n
-- Mathlib.GroupTheory.Nilpotent
Subgroup.instCharacteristicUpperCentralSeries : ∀ (G : Type u_1) [inst : Group G] (n : ℕ), (Subgroup.upperCentralSeries G n).Characteristic
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
RingHom.IsIntegralElem.of_neg : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {x : S},
  f.IsIntegralElem (-x) → f.IsIntegralElem x
-- Mathlib.Algebra.Module.Defs
/-- A module over a `Subsingleton` semiring is a `Subsingleton`. We cannot register this
as an instance because Lean has no way to guess `R`.  -/
Module.subsingleton : ∀ (R : Type u_5) (M : Type u_6) [inst : MonoidWithZero R] [Subsingleton R] [inst_2 : Zero M] [MulActionWithZero R M],
  Subsingleton M
-- Mathlib.CategoryTheory.Category.RelCat
CategoryTheory.RelCat.unopFunctor_comp_opFunctor_eq : CategoryTheory.RelCat.unopFunctor.comp CategoryTheory.RelCat.opFunctor =
  CategoryTheory.Functor.id CategoryTheory.RelCatᵒᵖ
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.IsLeftInversion.eq_1 : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w t : W),
  cs.IsLeftInversion w t = (cs.IsReflection t ∧ cs.length (t * w) < cs.length w)
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.instInhabited : {Γ : Type u_1} →
  {R : Type u_3} →
    {α : Type u_5} → [inst : PartialOrder Γ] → [inst_1 : AddCommMonoid R] → Inhabited (HahnSeries.SummableFamily Γ R α)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_apply_pi : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {ι : Type u_3}
  (f : ι → R → R) (a : A) (ha : autoParam (p a) cfc_apply_pi._auto_1)
  (hf : autoParam (∀ (i : ι), ContinuousOn (f i) (spectrum R a)) cfc_apply_pi._auto_3),
  (fun i => cfc (f i) a) = fun i => (cfcHom ha) { toFun := (spectrum R a).domRestrict (f i), continuous_toFun := ⋯ }
-- Mathlib.Topology.Compactification.StoneCech
continuous_preStoneCechUnit : ∀ {α : Type u} [inst : TopologicalSpace α], Continuous preStoneCechUnit
-- Mathlib.Order.SuccPred.Basic
/-- **Alias** of the forward direction of `Order.le_pred_iff_isMin`. -/
IsMin.of_le_pred : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a : α}, a ≤ Order.pred a → IsMin a
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.tensorUnitImpl_src : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C],
  CategoryTheory.Dial.tensorUnitImpl.src = ⊤_ C
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_filter_not_contains_map_fst_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)}
  {hl₁ : Std.Internal.List.DistinctKeys l₁} {k : α},
  Std.Internal.List.containsKey k l₁ = false →
    Std.Internal.List.containsKey k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) = false
-- Mathlib.Analysis.Normed.Module.Basic
/-- Produces a `PseudoMetricSpace E` instance from a `SeminormedSpace.Core` on a type that
already has an existing topology. This requires a proof that the topology induced
by the norm is equal to the preexisting topology. See note [reducible non-instances].  -/
PseudoMetricSpace.ofSeminormedSpaceCoreReplaceTopology : {𝕜 : Type u_6} →
  {E : Type u_7} →
    [inst : NormedField 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Norm E] →
          [inst_3 : Module 𝕜 E] →
            [T : TopologicalSpace E] →
              (core : SeminormedSpace.Core 𝕜 E) →
                T = PseudoEMetricSpace.toUniformSpace.toTopologicalSpace → PseudoMetricSpace E
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Pullback a `CompletelyDistribLattice` along an injection.  -/
Function.Injective.completelyDistribLattice : {α : Type u} →
  {β : Type v} →
    [inst : Max α] →
      [inst_1 : Min α] →
        [inst_2 : LE α] →
          [inst_3 : LT α] →
            [inst_4 : SupSet α] →
              [inst_5 : InfSet α] →
                [inst_6 : Top α] →
                  [inst_7 : Bot α] →
                    [inst_8 : Compl α] →
                      [inst_9 : HImp α] →
                        [inst_10 : HNot α] →
                          [inst_11 : SDiff α] →
                            [inst_12 : CompletelyDistribLattice β] →
                              (f : α → β) →
                                Function.Injective f →
                                  (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) →
                                    (∀ {x y : α}, f x < f y ↔ x < y) →
                                      (∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) →
                                        (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) →
                                          (∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) →
                                            (∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) →
                                              f ⊤ = ⊤ →
                                                f ⊥ = ⊥ →
                                                  (∀ (a : α), f aᶜ = (f a)ᶜ) →
                                                    (∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) →
                                                      (∀ (a : α), f (￢a) = ￢f a) →
                                                        (∀ (a b : α), f (a \ b) = f a \ f b) →
                                                          CompletelyDistribLattice α
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.prodMap_apply : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [inst : SMul M α]
  [inst_1 : SMul M β] [inst_2 : SMul N γ] [inst_3 : SMul N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : β →ₑ[σ] δ),
  ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.mk.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] (m : M) (s : ℕ+),
  DivisibleHull.mk m s = LocalizedModule.mk m (PNat.equivNonZeroDivisorsNat s)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isEmpty_eq_false_of_isEmpty_erase_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).isEmpty = false → t.isEmpty = false
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of `SimpleGraph.Walk.support_bypass_subset_support`. -/
SimpleGraph.Walk.support_bypass_subset : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] (p : G.Walk u v), p.bypass.support ⊆ p.support
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_5} [inst_1 : CommRing K] [inst_2 : Algebra R K] [IsFractionRing R K]
  [Nontrivial R] {x : R}, x ∈ nonZeroDivisors R → (algebraMap R K) x ≠ 0
-- Mathlib.Combinatorics.Quiver.Basic
Quiver.homOfEq_heq : ∀ {V : Type u_1} [inst : Quiver V] {X Y X' Y' : V} (hX : X = X') (hY : Y = Y') (f : X ⟶ Y), Quiver.homOfEq f hX hY ≍ f
-- Mathlib.RepresentationTheory.FDRep
FDRep.instCoeSortType : {R : Type u} → {G : Type v} → [inst : CommRing R] → [inst_1 : Monoid G] → CoeSort (FDRep R G) (Type u)
-- Mathlib.Dynamics.Ergodic.Ergodic
MeasureTheory.MeasurePreserving.ergodic_of_ergodic_semiconj : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {μ : MeasureTheory.Measure α} {β : Type u_2}
  {m' : MeasurableSpace β} {μ' : MeasureTheory.Measure β} {g : α → β},
  MeasureTheory.MeasurePreserving g μ μ' →
    Ergodic f μ → ∀ {f' : β → β}, Measurable f' → Function.Semiconj g f f' → Ergodic f' μ'
-- Mathlib.Dynamics.FixedPoints.Basic
Function.IsFixedPt.equiv_symm : ∀ {α : Type u_1} {x : α} {e : Equiv.Perm α}, Function.IsFixedPt (⇑e) x → Function.IsFixedPt (⇑(Equiv.symm e)) x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.mapArrowLeft_right : ∀ {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₃)} {f₁ f₁' : CategoryTheory.Arrow C₁}
  {f₂ : CategoryTheory.Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom)
  (sq : f₁ ⟶ f₁'), (sq₁₂.mapArrowLeft sq₁₂' sq).right = (F.map (CategoryTheory.Arrow.Hom.right sq)).app f₂.right
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Ideal.adic_module_basis : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  I.ringFilterBasis.SubmodulesBasis fun n => I ^ n • ⊤
-- Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
CategoryTheory.instEssentiallySmallIsCardinalPresentableOfHasCardinalFilteredGenerator : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.HasCardinalFilteredGenerator C κ],
  CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} (CategoryTheory.isCardinalPresentable C κ)
-- Init.Data.Range.Polymorphic.Nat
Std.instLawfulRcoIntersectionNat_3 : Std.Rco.LawfulRcoIntersection ℕ
-- Mathlib.Order.Heyting.Hom
BiheytingHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β] (f : BiheytingHom α β)
  (f' : α → β) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Init.Data.Iterators.Lemmas.Combinators.Append
Std.Iter.append_eq_toIter_append_toIterM : ∀ {α₁ α₂ β : Type w} [inst : Std.Iterator α₁ Id β] [inst_1 : Std.Iterator α₂ Id β] {it₁ : Std.Iter β}
  {it₂ : Std.Iter β}, it₁.append it₂ = (it₁.toIterM.append it₂.toIterM).toIter
-- Std.Data.DTreeMap.Raw.Basic
Std.DTreeMap.Raw.instMembership : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Membership α (Std.DTreeMap.Raw α β cmp)
-- Mathlib.Algebra.Group.Equiv.Opposite
AddOpposite.opMulEquiv_apply : ∀ {α : Type u_2} [inst : Mul α], ⇑AddOpposite.opMulEquiv = AddOpposite.op
-- Mathlib.Data.EReal.Basic
EReal.toReal_toENNReal : ∀ {x : EReal}, 0 ≤ x → x.toENNReal.toReal = x.toReal
-- Mathlib.Topology.Algebra.Order.Floor
continuousAt_fract : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [OrderClosedTopology α] [IsTopologicalAddGroup α] {x : α}, x ≠ ↑⌊x⌋ → ContinuousAt Int.fract x
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_pow : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Monoid β] (f : MeasureTheory.SimpleFunc α β)
  (n : ℕ), ⇑(f ^ n) = ⇑f ^ n
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.restrict_apply : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)}
  (f : BoxIntegral.BoxAdditiveMap ι M I₀) (I : WithTop (BoxIntegral.Box ι)) (hI : I ≤ I₀) (a : BoxIntegral.Box ι),
  (f.restrict I hI) a = f a
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.mem_closure_iff_of_isRelational : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M] [L.IsRelational] (s : Set M) (m : M),
  m ∈ (FirstOrder.Language.Substructure.closure L).toFun s ↔ m ∈ s
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
/-- The derivative of `expMap_single`, see `hasDerivAt_expMap_single`.
 -/
NumberField.mixedEmbedding.fundamentalCone.deriv_expMap_single : {K : Type u_1} → [inst : Field K] → NumberField.InfinitePlace K → ℝ → ℝ
-- Mathlib.Order.SupClosed
SupClosed.infClosure : ∀ {α : Type u_3} [inst : DistribLattice α] {s : Set α}, SupClosed s → SupClosed (infClosure s)
-- Std.Time.Date.Unit.Week
Std.Time.Week.OfYear.instDecidableLtOrdinal : {x y : Std.Time.Week.OfYear.Ordinal} → Decidable (x < y)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
/-- `SeparationQuotient.mk` as a continuous linear map.  -/
SeparationQuotient.mkCLM : (R : Type u_1) →
  (M : Type u_3) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          [inst_3 : TopologicalSpace M] →
            [inst_4 : ContinuousAdd M] → [inst_5 : ContinuousConstSMul R M] → M →L[R] SeparationQuotient M
-- Init.Core
/-- `strictOr` is the same as `or`, but it does not use short-circuit evaluation semantics:
both sides are evaluated, even if the first value is `true`.
 -/
strictOr : Bool → Bool → Bool
-- Lean.ScopedEnvExtension
Lean.SimpleScopedEnvExtension.Descr.mk.sizeOf_spec : ∀ {α σ : Type} [inst : SizeOf α] [inst_1 : SizeOf σ]
  (name : autoParam Lean.Name Lean.SimpleScopedEnvExtension.Descr.name._autoParam) (addEntry : σ → α → σ) (initial : σ)
  (finalizeImport : σ → σ) (exportEntry? : Lean.Environment → α → Lean.OLeanEntries (Option α)),
  sizeOf
      { name := name, addEntry := addEntry, initial := initial, finalizeImport := finalizeImport,
        exportEntry? := exportEntry? } =
    1 + sizeOf name + sizeOf initial
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Kind.forInWithReturn.sizeOf_spec : sizeOf Lean.Elab.Term.Do.ToTerm.Kind.forInWithReturn = 1
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.apply_eq_one_iff : ∀ {α : Type u_1} (p : PMF α) (a : α), p a = 1 ↔ p.support = {a}
-- Mathlib.Data.Finset.Basic
Finset.disjoint_sdiff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, Disjoint s (t \ s)
-- Init.Data.List.Basic
List.flatMap_append : ∀ {α : Type u} {β : Type v} {xs ys : List α} {f : α → List β},
  List.flatMap f (xs ++ ys) = List.flatMap f xs ++ List.flatMap f ys
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.bounds_bddBelow : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  {f : NormedAddGroupHom V₁ V₂}, BddBelow {c | 0 ≤ c ∧ ∀ (x : V₁), ‖f x‖ ≤ c * ‖x‖}
-- Mathlib.Algebra.CharP.Lemmas
sum_pow_char : ∀ {R : Type u_3} [inst : CommSemiring R] (p : ℕ) [ExpChar R p] {ι : Type u_4} (s : Finset ι) (f : ι → R),
  (∑ i ∈ s, f i) ^ p = ∑ i ∈ s, f i ^ p
-- Mathlib.Topology.Constructions.SumProd
map_fst_nhds : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (x : X × Y),
  Filter.map Prod.fst (nhds x) = nhds x.1
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- If `t.unop : Cone F` is a limit cone, then `t : Cocone F.op` is a colimit cocone.  -/
CategoryTheory.Limits.isColimitOfUnop : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cocone F.op} →
            CategoryTheory.Limits.IsLimit t.unop → CategoryTheory.Limits.IsColimit t
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.zero : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (j : J),
  RingCat.Colimits.Relation F (RingCat.Colimits.Prequotient.of j 0) RingCat.Colimits.Prequotient.zero
-- Mathlib.Algebra.GroupWithZero.Associated
associated_unit_mul_right : ∀ {N : Type u_2} [inst : CommMonoid N] (a u : N), IsUnit u → Associated a (u * a)
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.instMonoidalFunctorFunctorCongrLeft : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (E : Type u_1) →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} E] →
            [inst_3 : CategoryTheory.MonoidalCategory E] → (e : C ≌ D) → e.congrLeft.functor.Monoidal
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
/-- Semilinear sets are closed under set addition.  -/
IsSemilinearSet.add : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s₁ s₂ : Set M},
  IsSemilinearSet s₁ → IsSemilinearSet s₂ → IsSemilinearSet (s₁ + s₂)
-- Mathlib.Data.Sign.Defs
sign_zero : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Preorder α] [inst_2 : DecidableLT α], SignType.sign 0 = 0
-- Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Submodule.finrank_quotient_eq_sum : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsDomain R] [inst_4 : IsPrincipalIdealRing R] (F : Type u_4) [inst_5 : CommRing F] [inst_6 : Algebra F R]
  [inst_7 : Module F M] [inst_8 : IsScalarTower F R M] {N : Submodule R M} {ι : Type u_5} [inst_9 : Fintype ι]
  (b : Module.Basis ι R M) [Nontrivial F] (h : Module.finrank R ↥N = Module.finrank R M)
  [∀ (i : ι), Module.Free F (R ⧸ Ideal.span {Submodule.smithNormalFormCoeffs b h i})]
  [∀ (i : ι), Module.Finite F (R ⧸ Ideal.span {Submodule.smithNormalFormCoeffs b h i})],
  Module.finrank F (M ⧸ N) = ∑ i, Module.finrank F (R ⧸ Ideal.span {Submodule.smithNormalFormCoeffs b h i})
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
csInf_zero : ∀ {M : Type u_1} [inst : ConditionallyCompleteLattice M] [inst_1 : Zero M], sInf 0 = 0
-- Init.Data.UInt.Lemmas
UInt32.toUSize_div : ∀ (a b : UInt32), (a / b).toUSize = a.toUSize / b.toUSize
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.MkEval.toMkEvalWhiskerRight : {m : Type → Type} → [self : Mathlib.Tactic.BicategoryLike.MkEval m] → Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight m
-- Init.Data.Nat.Bitwise.Basic
Nat.instOrOp : OrOp ℕ
-- Init.Data.Nat.ToString
_private.Init.Data.Nat.ToString.0.Nat.toDigits.eq_1 : ∀ (base n : ℕ), base.toDigits n = base.toDigitsCore (n + 1) n []
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.cast_eq_id : ∀ {α : Type u}, cast ⋯ = id
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
LinearIsometry.toContinuousLinearMap_lTensor : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (g : E →ₗᵢ[𝕜] F),
  (LinearIsometry.lTensor G g).toContinuousLinearMap = ContinuousLinearMap.lTensor G g.toContinuousLinearMap
-- Mathlib.Order.Concept
Concept.mk.sizeOf_spec : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} [inst : SizeOf α] [inst_1 : SizeOf β]
  [inst_2 : (a : α) → (a_1 : β) → SizeOf (r a a_1)] (extent : Set α) (intent : Set β)
  (upperPolar_extent : upperPolar r extent = intent) (lowerPolar_intent : lowerPolar r intent = extent),
  sizeOf
      { extent := extent, intent := intent, upperPolar_extent := upperPolar_extent,
        lowerPolar_intent := lowerPolar_intent } =
    1 + sizeOf upperPolar_extent + sizeOf lowerPolar_intent
-- Mathlib.Geometry.Manifold.Riemannian.Basic
/-- If points are close for the topology, then their Riemannian distance is small.  -/
eventually_riemannianEDist_lt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : Bundle.RiemannianBundle fun x => TangentSpace I x] [inst_6 : IsManifold I 1 M]
  [IsContinuousRiemannianBundle E fun x => TangentSpace I x] (x : M) {c : ENNReal},
  0 < c → ∀ᶠ (y : M) in nhds x, Manifold.riemannianEDist I x y < c
-- Init.Data.Iterators.Combinators.Append
/-- This combinator is only useful for advanced use cases.

Given an iterator `it₂`, returns an iterator that behaves exactly like `it₂` but is of the same
type as `it₁.append it₂` (after `it₁` has been exhausted).
This is useful for constructing intermediate states of the append iterator.

**Marble diagram:**

```text
it₂                        --a--b--⊥
Iter.appendSnd α₁ it₂      --a--b--⊥
```

**Termination properties:**

* `Finite` instance: only if `it₂` and iterators of type `α₁` are finite
* `Productive` instance: only if `it₂` and iterators of type `α₁` are productive

Note: If iterators of type `α₁` are not finite, then `append α₁ it₂` can be productive while `it₂` is not.
The standard library does not provide a `Productive` instance for this case.

**Performance:**

This combinator incurs an additional O(1) cost with each output of `it₂`.
 -/
Std.Iter.Intermediate.appendSnd : {α₂ β : Type w} → [Std.Iterator α₂ Id β] → (α₁ : Type w) → Std.Iter β → Std.Iter β
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.derivFamily_limit : ∀ {ι : Type u_1} (f : ι → Ordinal.{u_2} → Ordinal.{u_2}) {o : Ordinal.{u_2}},
  Order.IsSuccLimit o → Ordinal.derivFamily f o = ⨆ b, Ordinal.derivFamily f ↑b
-- Mathlib.Topology.Algebra.Support
exists_compact_iff_hasCompactSupport : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : Zero β] {f : α → β} [R1Space α],
  (∃ K, IsCompact K ∧ ∀ x ∉ K, f x = 0) ↔ HasCompactSupport f
-- Mathlib.Order.PiLex
Pi.colex_le_iff_of_unique : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : Unique ι] [inst_1 : LinearOrder ι] [inst_2 : (i : ι) → PartialOrder (β i)]
  {x y : Colex ((i : ι) → β i)}, x ≤ y ↔ x default ≤ y default
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.pushout_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {A B A' : C}
  (f : A ⟶ A') (g : A ⟶ B) [inst_1 : CategoryTheory.Limits.HasPushout f g] [P.IsStableUnderCobaseChangeAlong g],
  P f → P (CategoryTheory.Limits.pushout.inr f g)
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccLimit.ne_bot : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : OrderBot α], Order.IsSuccLimit a → a ≠ ⊥