mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Independence.Process.Basic
/-- If `X` and `Y` are two independent processes and for all `i`, `X' i` is almost everywhere equal
to `X i`, and for all `j`, `Y' j` is almost everywhere equal to `Y j`,
then `X'` is independent from `Y'`. This implies that independence results about
measurable processes should generally also hold
for processes whose marginals are only a.e.-measurable.  -/
ProbabilityTheory.IndepFun.process_congr : ∀ {S : Type u_1} {T : Type u_2} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : S → Type u_4}
  {𝓨 : T → Type u_5} [inst : (i : S) → MeasurableSpace (𝓧 i)] [inst_1 : (j : T) → MeasurableSpace (𝓨 j)]
  {X X' : (i : S) → Ω → 𝓧 i} {Y Y' : (j : T) → Ω → 𝓨 j},
  ProbabilityTheory.IndepFun (fun ω i => X i ω) (fun ω j => Y j ω) P →
    (∀ (i : S), X i =ᵐ[P] X' i) →
      (∀ (j : T), Y j =ᵐ[P] Y' j) → ProbabilityTheory.IndepFun (fun ω i => X' i ω) (fun ω j => Y' j ω) P
-- Init.Data.Option.Lemmas
Option.join_beq_some : ∀ {α : Type u_1} [inst : BEq α] {o : Option (Option α)} {a : α}, (o.join == some a) = (o == some (some a))
-- Lean.Language.Basic
Lean.Language.instInhabitedSnapshotTree.default : Lean.Language.SnapshotTree
-- Mathlib.Topology.Sheaves.PresheafOfFunctions
/-- The presheaf of functions on `X` with values in a type `T`.
There is no requirement that the functions are continuous, here.
 -/
TopCat.presheafToType : (X : TopCat) → Type u_1 → TopCat.Presheaf (Type (max u_1 u_2)) X
-- Lean.Server.AsyncList
/-- Spawns a `Task` returning the prefix of elements up to (including) the first element for which `p` is true.
When `p` is not true of any element, it returns the entire list.  -/
Lean.AsyncList.waitUntil : {α : Type u_1} → {ε : Type u_2} → (α → Bool) → Lean.AsyncList ε α → Lean.Server.ServerTask (List α × Option ε)
-- Mathlib.Topology.UniformSpace.UniformConvergence
uniformCauchySeqOn_iff_uniformCauchySeqOnFilter : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι},
  UniformCauchySeqOn F p s ↔ UniformCauchySeqOnFilter F p (Filter.principal s)
-- Std.Data.Internal.List.Associative
Std.Internal.List.replaceEntry_nil : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {k : α} {v : β k}, Std.Internal.List.replaceEntry k v [] = []
-- Mathlib.Data.ENNReal.Inv
ENNReal.orderIsoIicOneBirational_apply_coe : ∀ (x : ENNReal), ↑(ENNReal.orderIsoIicOneBirational x) = (x⁻¹ + 1)⁻¹
-- Mathlib.CategoryTheory.Limits.Over
/-- If `F` has a colimit, then the cocone `colimit.toOver F` with cocone point `𝟙 (colimit F)` is
also a colimit cocone.  -/
CategoryTheory.Limits.colimit.isColimitToOver : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasColimit F] →
            CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.colimit.toOver F)
-- Mathlib.CategoryTheory.Enriched.Basic
/-- A natural transformation between two enriched functors is a `𝟙_ V`-graded natural
transformation.  -/
CategoryTheory.EnrichedNatTrans : {V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₁} →
        [inst_2 : CategoryTheory.EnrichedCategory V C] →
          {D : Type u₂} →
            [inst_3 : CategoryTheory.EnrichedCategory V D] →
              CategoryTheory.EnrichedFunctor V C D → CategoryTheory.EnrichedFunctor V C D → Type (max u₁ w)
-- Mathlib.Topology.Algebra.Support
range_subset_insert_image_mulTSupport : ∀ {X : Type u_1} {α : Type u_2} [inst : One α] [inst_1 : TopologicalSpace X] (f : X → α),
  Set.range f ⊆ insert 1 (f '' mulTSupport f)
-- Mathlib.Order.RelSeries
SetRel.not_infiniteDimensional_iff : ∀ {α : Type u_1} {r : SetRel α α} [Nonempty α], ¬r.InfiniteDimensional ↔ r.FiniteDimensional
-- Mathlib.AlgebraicGeometry.Cover.Open
/-- Every open cover of a quasi-compact scheme can be refined into a finite subcover.
 -/
AlgebraicGeometry.Scheme.OpenCover.finiteSubcover : {X : AlgebraicGeometry.Scheme} → X.OpenCover → [H : CompactSpace ↥X] → X.OpenCover
-- Init.Prelude
/-- `` `char `` is the node kind of character literals like `'A'`.  -/
Lean.charLitKind : Lean.SyntaxNodeKind
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the forward direction of `Equiv.Perm.sameCycle_apply_right`. -/
Equiv.Perm.SameCycle.of_apply_right : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x (f y) → f.SameCycle x y
-- Init.Data.Option.Lemmas
Option.map_eq_some_iff : ∀ {α : Type u_1} {b : α} {α_1 : Type u_2} {x : Option α_1} {f : α_1 → α},
  Option.map f x = some b ↔ ∃ a, x = some a ∧ f a = b
-- Mathlib.Topology.Bases
TopologicalSpace.isSeparable_union : ∀ {α : Type u} [t : TopologicalSpace α] {s t_1 : Set α},
  TopologicalSpace.IsSeparable (s ∪ t_1) ↔ TopologicalSpace.IsSeparable s ∧ TopologicalSpace.IsSeparable t_1
-- Mathlib.GroupTheory.Index
/-- Typeclass for finite index subgroups.  -/
AddSubgroup.FiniteIndex : {G : Type u_3} → [inst : AddGroup G] → AddSubgroup G → Prop
-- Mathlib.Order.Minimal
/-- **Alias** of `image_monotone_setOfPred_minimal_mem`. -/
image_monotone_setOf_minimal_mem : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α → β},
  (∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)) →
    f '' {x | Minimal (fun x => x ∈ s) x} = {x | Minimal (fun x => x ∈ f '' s) x}
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.mapDomainRingHom_comp_algebraMap : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddMonoid M] [inst_4 : AddMonoid N] (f : M →+ N),
  (AddMonoidAlgebra.mapDomainRingHom A f).comp (algebraMap R (AddMonoidAlgebra A M)) =
    algebraMap R (AddMonoidAlgebra A N)
-- Lean.Meta.Sym.InstantiateS
/-- Similar to `Lean.Expr.instantiateRange`.
It assumes the input is maximally shared, and ensures the output is too.
It assumes `beginIdx ≤ endIdx` and `endIdx ≤ subst.size`
 -/
_private.Lean.Meta.Sym.InstantiateS.0.Lean.Meta.Sym.instantiateRangeS' : Lean.Expr → ℕ → ℕ → Array Lean.Expr → Lean.Meta.Sym.Internal.AlphaShareBuilderM Lean.Expr
-- Aesop.RuleTac.Forward.Basic
Aesop.instInhabitedForwardHypData.default : Aesop.ForwardHypData
-- Mathlib.Control.Monad.Cont
ContT.run_callCC : ∀ {r : Type u} {m : Type u → Type v} {α β : Type w} (f : MonadCont.Label α (ContT r m) β → ContT r m α) (k : α → m r),
  (MonadCont.callCC f).run k = (f { apply := fun x => ContT.mk fun x_1 => k x }).run k
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.map_star_mem_unitaryGroup_iff : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
  {U : Matrix n n α}, U.map star ∈ Matrix.unitaryGroup n α ↔ U ∈ Matrix.unitaryGroup n α
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- The natural transformation presenting `g`.  -/
CategoryTheory.IndParallelPairPresentation.ψ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      {f g : A ⟶ B} → (self : CategoryTheory.IndParallelPairPresentation f g) → self.F₁ ⟶ self.F₂
-- Mathlib.Algebra.GroupWithZero.Basic
instIsCancelMulZero : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀], IsCancelMulZero G₀
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
FredholmDecomposition.finite_X₀ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] (self : FredholmDecomposition 𝕜 E), FiniteDimensional 𝕜 ↥self.X₀
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.denom_C : ∀ {K : Type u} [inst : Field K] (c : K), (RatFunc.C c).denom = 1
-- Mathlib.Order.Monotone.Basic
AntitoneOn.strictAnti_iff_injOn : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : PartialOrder β] {f : α → β} {s : Set α},
  AntitoneOn f s → (StrictAntiOn f s ↔ Set.InjOn f s)
-- Mathlib.Analysis.Complex.ValueDistribution.Cartan
/-- Circle average of the function `fun a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖` that appears
in Cartan's formula, in the case where `f` has a zero at the origin.
 -/
ValueDistribution.circleAverage_log_norm_meromorphicTrailingCoeffAt_of_meromorphicOrderAt_pos : ∀ {f : ℂ → ℂ},
  0 < meromorphicOrderAt f 0 →
    Real.circleAverage (fun a => Real.log ‖meromorphicTrailingCoeffAt (fun x => f x - a) 0‖) 0 1 = 0
-- Mathlib.Topology.Algebra.ProperConstSMul
ProperConstVAdd.mk : ∀ {M : Type u_1} {X : Type u_2} [inst : VAdd M X] [inst_1 : TopologicalSpace X],
  (∀ (c : M), IsProperMap fun x => c +ᵥ x) → ProperConstVAdd M X
-- Mathlib.RingTheory.Noetherian.Basic
isNoetherian_pi : ∀ {R : Type u_1} [inst : Ring R] {ι : Type u_6} [Finite ι] {M : ι → Type u_7} [inst_2 : (i : ι) → AddCommGroup (M i)]
  [inst_3 : (i : ι) → Module R (M i)] [∀ (i : ι), IsNoetherian R (M i)], IsNoetherian R ((i : ι) → M i)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.mem_toList_unique : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [Std.TransCmp cmp] {t : RBTree.RBSet α cmp},
  x ∈ t.toList → y ∈ t.toList → cmp x y = Ordering.eq → x = y
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.continuousOn : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B) {S : Set A}, ContinuousOn (⇑e) S
-- Mathlib.Analysis.Analytic.Within
/-- `f` has power series `p` at `x` iff some local extension of `f` has that series  -/
hasFPowerSeriesWithinAt_iff_exists_hasFPowerSeriesAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E},
  HasFPowerSeriesWithinAt f p s x ↔ ∃ g, f =ᶠ[nhdsWithin x (insert x s)] g ∧ HasFPowerSeriesAt g p x
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Complex.partialGamma.eq_1 : ∀ (s : ℂ) (X : ℝ), s.partialGamma X = ∫ (x : ℝ) in 0..X, ↑(Real.exp (-x)) * ↑x ^ (s - 1)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.reverse_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  (SimpleGraph.Walk.cons h p).reverse = p.reverse.append (SimpleGraph.Walk.cons ⋯ SimpleGraph.Walk.nil)
-- Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
AlgebraicTopology.DoldKan.homotopyPToId.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C),
  AlgebraicTopology.DoldKan.homotopyPToId X 0 = Homotopy.refl (AlgebraicTopology.DoldKan.P 0)
-- Init.Data.List.Perm
List.perm_append_singleton : ∀ {α : Type u_1} (a : α) (l : List α), (l ++ [a]).Perm (a :: l)
-- Init.Data.Option.Array
Option.toArray_min : ∀ {α : Type u_1} [inst : Min α] {o o' : Option α}, (o ⊓ o').toArray = Array.zipWith min o.toArray o'.toArray
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.SimpCacheKey.mk.inj : ∀ {variant : Lean.Name} {extras : Array Lean.Elab.Tactic.Grind.ExtraTheorem} {variant_1 : Lean.Name}
  {extras_1 : Array Lean.Elab.Tactic.Grind.ExtraTheorem},
  { variant := variant, extras := extras } = { variant := variant_1, extras := extras_1 } →
    variant = variant_1 ∧ extras = extras_1
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.const_inj : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [l.NeBot] {a b : β}, ↑a = ↑b ↔ a = b
-- Mathlib.RingTheory.SimpleModule.Isotypic
IsIsotypicOfType.of_subsingleton : ∀ (R : Type u_2) (M : Type u) (S : Type u_4) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup S]
  [inst_3 : Module R M] [inst_4 : Module R S] [Subsingleton M], IsIsotypicOfType R M S
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.coe_ssubset_coe : ∀ {α : Type u_1} [inst : LE α] {s t : UpperSet α}, ↑s ⊂ ↑t ↔ t < s
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientWithinAt.congr_simp : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] (f f_1 : F → 𝕜),
  f = f_1 →
    ∀ (f' f'_1 : F),
      f' = f'_1 →
        ∀ (s s_1 : Set F),
          s = s_1 → ∀ (x x_1 : F), x = x_1 → HasGradientWithinAt f f' s x = HasGradientWithinAt f_1 f'_1 s_1 x_1
-- Mathlib.Data.Seq.Basic
Stream'.Seq.Pairwise.cons : ∀ {α : Type u} {R : α → α → Prop} {hd : α} {tl : Stream'.Seq α},
  (∀ x ∈ tl, R hd x) → Stream'.Seq.Pairwise R tl → Stream'.Seq.Pairwise R (Stream'.Seq.cons hd tl)
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateAddSubgroup.mk : ∀ {G : Type u_2} [inst : AddGroup G] {K : ℝ} {A : Set G},
  0 ∈ A → -A = A → CovByVAdd G K (2 • A) A → IsApproximateAddSubgroup K A
-- Mathlib.Algebra.Order.Monovary
Antivary.nsmul_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : AddCommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedAddMonoid β] {f : ι → α} {g : ι → β}, Antivary f g → ∀ (n : ℕ), Antivary f (n • g)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.IsSymmetric.adjoint_conj : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] {T : E →ₗ[𝕜] E},
  T.IsSymmetric → ∀ (S : F →ₗ[𝕜] E), (LinearMap.adjoint S ∘ₗ T ∘ₗ S).IsSymmetric
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
ruzsaSzemerediNumber_le : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α], ruzsaSzemerediNumber α ≤ (Fintype.card α).choose 3
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
/-- The rightmost object of the fork diagram of Equation (3) [MM92], which contains the data used
to check a family is compatible.
 -/
CategoryTheory.Equalizer.Sieve.SecondObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor Cᵒᵖ (Type (max v u)) → {X : C} → CategoryTheory.Sieve X → Type (max v u)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sin_sub_int_mul_two_pi : ∀ (x : ℂ) (n : ℤ), Complex.sin (x - ↑n * (2 * ↑Real.pi)) = Complex.sin x
-- Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.EditableDocumentCore.mk : Lean.Server.DocumentMeta →
  Lean.Language.Lean.InitialSnapshot →
    Lean.AsyncList IO.Error Lean.Server.Snapshots.Snapshot →
      Std.Mutex Lean.Server.FileWorker.DiagnosticsState → Lean.Server.FileWorker.EditableDocumentCore
-- Mathlib.RingTheory.Multiplicity
Prime.finiteMultiplicity_mul : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {p a b : α},
  Prime p → FiniteMultiplicity p a → FiniteMultiplicity p b → FiniteMultiplicity p (a * b)
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.Hom.mk.injEq : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {L L' : Φ.LeftResolution X₂} (f : L.X₁ ⟶ L'.X₁)
  (comm :
    autoParam (CategoryTheory.CategoryStruct.comp (Φ.functor.map f) L'.w = L.w)
      CategoryTheory.LocalizerMorphism.LeftResolution.Hom.comm._autoParam)
  (f_1 : L.X₁ ⟶ L'.X₁)
  (comm_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (Φ.functor.map f_1) L'.w = L.w)
      CategoryTheory.LocalizerMorphism.LeftResolution.Hom.comm._autoParam),
  ({ f := f, comm := comm } = { f := f_1, comm := comm_1 }) = (f = f_1)
-- Mathlib.Analysis.Normed.Operator.Conformal
LinearIsometry.isConformalMap : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : NormedField R] [inst_1 : SeminormedAddCommGroup M]
  [inst_2 : SeminormedAddCommGroup N] [inst_3 : NormedSpace R M] [inst_4 : NormedSpace R N] (f' : M →ₗᵢ[R] N),
  IsConformalMap f'.toContinuousLinearMap
-- Mathlib.Algebra.Module.Submodule.LinearMap
Submodule.injective_subtype : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M),
  Function.Injective ⇑p.subtype
-- Mathlib.Logic.Basic
exists_apply_eq_apply3' : ∀ {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} {δ : Sort u_6} {f : α → β → γ → δ} {a : α} {b : β} {c : γ},
  ∃ x y z, f a b c = f x y z
-- Mathlib.Data.Finset.Union
Finset.union_biUnion : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Finset α} {t : α → Finset β} [inst : DecidableEq β] [inst_1 : DecidableEq α],
  (s₁ ∪ s₂).biUnion t = s₁.biUnion t ∪ s₂.biUnion t
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] {c : CategoryTheory.Limits.Cone F}
  (hc : CategoryTheory.Limits.IsLimit c) (j : J),
  CategoryTheory.CategoryStruct.comp (hc.conePointUniqueUpToIso (CategoryTheory.Limits.limit.isLimit F)).hom
      (CategoryTheory.Limits.limit.π F j) =
    c.π.app j
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.up'_Rel : ∀ {α : Type u_2} [inst : Add α] [inst_1 : IsRightCancelAdd α] (a i j : α), (ComplexShape.up' a).Rel i j = (i + a = j)
-- Batteries.Control.Nondet.Basic
/-- `Nondet m α` is variation on `MLList m α` suitable for use with backtrackable monads `m`.

We think of `Nondet m α` as a nondeterministic value in `α`,
with the possible alternatives stored in a monadic lazy list.

Along with each `a : α` we store the backtrackable state, and ensure that monadic operations
on alternatives run with the appropriate state.

Operations on the nondeterministic value via `bind`, `mapM`, and `filterMapM`
run with the appropriate backtrackable state, and are responsible for updating the state themselves
(typically this doesn't need to be done explicitly,
but just happens as a side effect in the monad `m`).
 -/
Nondet : {σ : Type} → (m : Type → Type) → [Lean.MonadBacktrack σ m] → Type → Type
-- Lean.Level
Lean.Level.PP.Result.imaxNode.sizeOf_spec : ∀ (a : List Lean.Level.PP.Result), sizeOf (Lean.Level.PP.Result.imaxNode a) = 1 + sizeOf a
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.posSemidef_intCast_iff : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  [inst_4 : DecidableEq n] [Nonempty n] [Nontrivial R] (d : ℤ), (↑d).PosSemidef ↔ 0 ≤ d
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.addEquivAddHaarChar_smul_preimage : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalAddGroup G] [inst_5 : LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure]
  [μ.Regular] {X : Set G} (φ : G ≃ₜ+ G), MeasureTheory.addEquivAddHaarChar φ • μ (⇑φ ⁻¹' X) = μ X
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.mk_one : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R],
  ArchimedeanClass.mk 1 = 0
-- Mathlib.Topology.MetricSpace.Thickening
/-- The open thickening `Metric.thickening δ E` is contained in the closed thickening
`Metric.cthickening δ E` with the same radius.  -/
Metric.thickening_subset_cthickening : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α), Metric.thickening δ E ⊆ Metric.cthickening δ E
-- Mathlib.Order.Filter.IsBounded
OrderIso.isBoundedUnder_ge_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) {l : Filter γ} {u : γ → α},
  (Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) l fun x => e (u x)) ↔ Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) l u
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.toNNRealLinear_inj : ∀ {α : Type u_2} [inst : TopologicalSpace α] (Λ₁ Λ₂ : CompactlySupportedContinuousMap α ℝ →ₚ[ℝ] ℝ),
  CompactlySupportedContinuousMap.toNNRealLinear Λ₁ = CompactlySupportedContinuousMap.toNNRealLinear Λ₂ ↔ Λ₁ = Λ₂
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.op_sSup : ∀ {M : Type u_2} [inst : Add M] (S : Set (AddSubsemigroup M)), (sSup S).op = sSup (AddSubsemigroup.unop ⁻¹' S)
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.instPowSubtypeMemAddSubgroupNat : {R : Type u_1} → [inst : Ring R] → [inst_1 : StarRing R] → Pow ↥(selfAdjoint R) ℕ
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.isGE_iff_isZero_truncLT_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C),
  t.IsGE X n ↔ CategoryTheory.Limits.IsZero ((t.truncLT n).obj X)
-- Mathlib.Topology.MetricSpace.Pseudo.Real
Real.dist_le_of_mem_pi_Icc : ∀ {ι : Type u_1} [inst : Fintype ι] {x y x' y' : ι → ℝ}, x ∈ Set.Icc x' y' → y ∈ Set.Icc x' y' → dist x y ≤ dist x' y'
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instHashablePower : Hashable Lean.Grind.CommRing.Power
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.int_mul : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : NonAssocRing α],
  Function.Periodic f c → ∀ (n : ℤ), Function.Periodic f (↑n * c)
-- Mathlib.Topology.Order.LeftRightNhds
/-- The following statements are equivalent:

0. `s` is a neighborhood of `b` within `(-∞, b]`
1. `s` is a neighborhood of `b` within `[a, b]`
2. `s` is a neighborhood of `b` within `(a, b]`
3. `s` includes `(l, b]` for some `l ∈ [a, b)`
4. `s` includes `(l, b]` for some `l < b`  -/
TFAE_mem_nhdsLE : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a b : α},
  a < b →
    ∀ (s : Set α),
      [s ∈ nhdsWithin b (Set.Iic b), s ∈ nhdsWithin b (Set.Icc a b), s ∈ nhdsWithin b (Set.Ioc a b),
          ∃ l ∈ Set.Ico a b, Set.Ioc l b ⊆ s, ∃ l ∈ Set.Iio b, Set.Ioc l b ⊆ s].TFAE
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.prod.eq_1 : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : Monoid C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] (f : A →ₜ* B) (g : A →ₜ* C),
  f.prod g = { toMonoidHom := f.prod g.toMonoidHom, continuous_toFun := ⋯ }
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.map.eq_1 : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (α : F ⟶ G),
  CategoryTheory.Pseudofunctor.CoGrothendieck.map α =
    { obj := fun a => { base := a.base, fiber := (α.app { as := Opposite.op a.base }).toFunctor.obj a.fiber },
      map := fun {a b} f =>
        { base := f.base,
          fiber :=
            CategoryTheory.CategoryStruct.comp ((α.app { as := Opposite.op a.base }).toFunctor.map f.fiber)
              ((α.naturality f.base.op.toLoc).hom.toNatTrans.app b.fiber) },
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Reinterpret `f : α →ᵤ[𝔖] β` as an element of `α → β`.  -/
UniformOnFun.toFun : {α : Type u_1} → {β : Type u_2} → (𝔖 : Set (Set α)) → UniformOnFun α β 𝔖 ≃ (α → β)
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- Extension for the `positivity` tactic: `Besicovitch.SatelliteConfig.r`.  -/
Mathlib.Meta.Positivity.evalBesicovitchSatelliteConfigR : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.GroupTheory.Torsion
AddCommMonoid.addTorsion.eq_1 : ∀ (G : Type u_1) [inst : AddCommMonoid G],
  AddCommMonoid.addTorsion G = { carrier := {x | IsOfFinAddOrder x}, add_mem' := ⋯, zero_mem' := ⋯ }