mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.ContMDiffMap
ContMDiffMap.instFunLike : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {H' : Type u_5} →
                      [inst_6 : TopologicalSpace H'] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {M : Type u_6} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {M' : Type u_7} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] →
                                        {n : WithTop ℕ∞} → FunLike (ContMDiffMap I I' M M' n) M M'
-- Init.Data.Array.Basic
Array.popWhile_empty : ∀ {α : Type u} {p : α → Bool}, Array.popWhile p #[] = #[]
-- Batteries.Data.List.Perm
List.Perm.coe_idxBij : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : ReflBEq α] {xs ys : List α} (h : xs.Perm ys) {i : Fin xs.length},
  ↑(h.idxBij i) = List.idxOfNth xs[i] ys (List.countBefore xs[i] xs ↑i)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- If a matrix has a repeated column, the determinant will be zero.  -/
Matrix.det_zero_of_column_eq : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {M : Matrix n n R}
  {i j : n}, i ≠ j → (∀ (k : n), M k i = M k j) → M.det = 0
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.Language.presburger.instNatCastTerm : {α : Type u_1} → NatCast (FirstOrder.Language.presburger.Term α)
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.unitCompPartialBijective_symm_apply : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {i : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Reflective i] (A : C) {B : C} (hB : i.essImage B)
  (f : i.obj ((CategoryTheory.reflector i).obj A) ⟶ B),
  (CategoryTheory.unitCompPartialBijective A hB).symm f =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.reflectorAdjunction i).unit.app A) f
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_add_one : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.T R (n + 1) = 2 * Polynomial.X * Polynomial.Chebyshev.T R n - Polynomial.Chebyshev.T R (n - 1)
-- Mathlib.FieldTheory.Galois.Basic
IntermediateField.restrictRestrictAlgEquivMapHom.eq_1 : ∀ (F : Type u_1) (K : Type u_2) (L : Type u_3) (E : Type u_4) [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Field E] [inst_4 : Algebra F K] [inst_5 : Algebra F L] [inst_6 : Algebra F E] [inst_7 : Algebra K E]
  [inst_8 : Algebra L E] [inst_9 : IsScalarTower F K E] [inst_10 : IsScalarTower F L E] [inst_11 : Normal F K],
  IntermediateField.restrictRestrictAlgEquivMapHom F K L E =
    (AlgEquiv.restrictNormalHom K).comp (MulSemiringAction.toAlgAut Gal(E/L) F E)
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.lt_iff_le_not_ge : ∀ (a b : ℚ), a < b ↔ a ≤ b ∧ ¬b ≤ a
-- Mathlib.Topology.Connected.PathConnected
/-- This is a special case of `NormedSpace.instPathConnectedSpace` (and
`IsTopologicalAddGroup.pathConnectedSpace`). It exists only to simplify dependencies.  -/
Real.instPathConnectedSpace : PathConnectedSpace ℝ
-- Mathlib.Order.Disjoint
codisjoint_bot : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {a : α}, Codisjoint a ⊥ ↔ a = ⊤
-- Mathlib.Logic.Equiv.Basic
/-- The `Pi`-type `∀ i, π i` is equivalent to the type of sections `f : ι → Σ i, π i` of the
`Sigma` type such that for all `i` we have `(f i).fst = i`.  -/
Equiv.piEquivSubtypeSigma : (ι : Type u_10) → (π : ι → Type u_9) → ((i : ι) → π i) ≃ { f // ∀ (i : ι), (f i).fst = i }
-- Init.Data.Int.Lemmas
Int.instNeZeroHMul : ∀ {a b : ℤ} [NeZero a] [NeZero b], NeZero (a * b)
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.coe_sub : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) (x y : ↥H), ↑(x - y) = ↑x - ↑y
-- Init.Data.Array.Basic
Array.anyM.loop : {α : Type u} →
  {m : Type → Type w} → [Monad m] → (α → m Bool) → (as : Array α) → (stop : ℕ) → stop ≤ as.size → ℕ → m Bool
-- Mathlib.NumberTheory.LSeries.Linearity
LSeriesHasSum.add : ∀ {f g : ℕ → ℂ} {s a b : ℂ}, LSeriesHasSum f s a → LSeriesHasSum g s b → LSeriesHasSum (f + g) s (a + b)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.instDecidableRel_induce_adj : {V : Type u} →
  {G : SimpleGraph V} →
    {G' : G.Subgraph} →
      (s : Set V) → [(a : V) → Decidable (a ∈ s)] → [DecidableRel G'.Adj] → DecidableRel (G'.induce s).Adj
-- Mathlib.Order.Concept
/-- The formal concepts of a relation. A concept of `r : α → β → Prop` is a pair of sets `s`, `t`
such that `s` is the set of all elements that are `r`-related to all of `t` and `t` is the set of
all elements that are `r`-related to all of `s`.  -/
Concept : (α : Type u_2) → (β : Type u_3) → (α → β → Prop) → Type (max u_2 u_3)
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.hasColimits_ringCat : CategoryTheory.Limits.HasColimits RingCat
-- Lean.Server.CodeActions.Provider
/-- Returns the info tree corresponding to a syntax, using `kind` and `range` for identification.
(This is not foolproof, but it is a fairly accurate proxy for `Syntax` equality and a lot cheaper
than deep comparison.)
 -/
Lean.CodeAction.findInfoTree? : Lean.SyntaxNodeKind →
  Lean.Syntax.Range →
    Option Lean.Elab.ContextInfo →
      Lean.Elab.InfoTree →
        (Lean.Elab.ContextInfo → Lean.Elab.Info → Bool) →
          optParam Bool false → Option (Lean.Elab.ContextInfo × Lean.Elab.InfoTree)
-- Mathlib.Data.DFinsupp.BigOperators
/-- **Alias** of `DFinsupp.coe_finsetSum`. -/
DFinsupp.coe_finset_sum : ∀ {ι : Type u} {β : ι → Type v} {α : Type u_1} [inst : (i : ι) → AddCommMonoid (β i)] (s : Finset α)
  (g : α → Π₀ (i : ι), β i), ⇑(∑ a ∈ s, g a) = ∑ a ∈ s, ⇑(g a)
-- Mathlib.Analysis.Asymptotics.LinearGrowth
Monotone.linearGrowthSup_nonneg : ∀ {u : ℕ → EReal}, Monotone u → u ≠ ⊥ → 0 ≤ LinearGrowth.linearGrowthSup u
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.hom_left_inv_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (e : f ≅ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left e.hom) (CategoryTheory.Over.Hom.left e.inv) =
    CategoryTheory.CategoryStruct.id f.left
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.IsTable.eq_prefixFunction : ∀ {b : ByteArray} {v : Array ℕ} (self : String.Slice.Pattern.Model.ForwardSliceSearcher.IsTable✝ b v) (i : ℕ)
  (hi : i < v.size), v[i] = String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ b i ⋯
-- Mathlib.Data.Sign.Defs
SignType.neg_one_le : ∀ (a : SignType), -1 ≤ a
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Lean.Int.fromExpr? : Lean.Expr → Lean.Meta.SimpM (Option ℤ)
-- Mathlib.Data.Setoid.Basic
Setoid.le_comap_map : ∀ {α : Type u_1} {β : Type u_2} {r : Setoid α} {f : α → β}, r ≤ Setoid.comap f (r.map f)
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.zipWithAll.go.eq_def : ∀ {α : Type u} {β : Type u_1} {γ : Type u_2} (f : Option α → Option β → γ) (as : Array α) (bs : Array β) (i : ℕ)
  (cs : Array γ),
  Array.zipWithAll.go✝ f as bs i cs =
    if i < max as.size bs.size then
      have a := as[i]?;
      have b := bs[i]?;
      Array.zipWithAll.go✝ f as bs (i + 1) (cs.push (f a b))
    else cs
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- Uses `left` co(ntra)variant.  -/
Left.inv_lt_one_iff : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a : α}, a⁻¹ < 1 ↔ 1 < a
-- Mathlib.Data.ENNReal.Inv
ENNReal.top_div_of_lt_top : ∀ {a : ENNReal}, a < ⊤ → ⊤ / a = ⊤
-- Mathlib.MeasureTheory.Measure.Prokhorov
/-- **Alias** of `isCompact_setOfPred_finiteMeasure_eq_of_compactSpace`.

---

In a compact space, the set of finite measures with mass `C` is compact.  -/
isCompact_setOf_finiteMeasure_eq_of_compactSpace : ∀ (E : Type u_1) [inst : MeasurableSpace E] [inst_1 : TopologicalSpace E] [T2Space E] [inst_3 : BorelSpace E]
  [CompactSpace E] (C : NNReal), IsCompact {μ | μ.mass = C}
-- Mathlib.Data.Nat.Dist
Nat.dist_succ_succ : ∀ {i j : ℕ}, i.succ.dist j.succ = i.dist j
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.instCommShiftHomotopyCategoryIntUpQh : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → [inst_2 : HasDerivedCategory C] → DerivedCategory.Qh.CommShift ℤ
-- Std.Http.Data.Response
Std.Http.Response.Head.mk.sizeOf_spec : ∀ (status : Std.Http.Status) (version : Std.Http.Version) (headers : Std.Http.Headers),
  sizeOf { status := status, version := version, headers := headers } =
    1 + sizeOf status + sizeOf version + sizeOf headers
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_assoc : ∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12}
  {q : Type u_13} {r : Type u_14} {δ : Type u_19} {ξ : Type u_20} {ω : Type u_21} {ω' : Type u_22} (f : α → β → γ)
  (g : γ → δ → ω) (f' : α → ξ → ω') (g' : β → δ → ξ) (A : Matrix l m α) (B : Matrix n p β) (D : Matrix q r δ)
  (φ : ω ≃ ω'),
  (∀ (a : α) (b : β) (d : δ), φ (g (f a b) d) = f' a (g' b d)) →
    ((Matrix.reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r)).trans φ.mapMatrix)
        (Matrix.kroneckerMap g (Matrix.kroneckerMap f A B) D) =
      Matrix.kroneckerMap f' A (Matrix.kroneckerMap g' B D)
-- Mathlib.Analysis.Convex.Between
Wbtw.swap_right_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] [IsDomain R] [Module.IsTorsionFree R V] {x y z : P},
  Wbtw R x y z → (Wbtw R x z y ↔ y = z)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get?_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₂ → (m₁ ∩ m₂).get? k = none
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_Icc_eq_integral_Ioc' : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} [inst_2 : PartialOrder X] {x y : X},
  μ {x} = 0 → ∫ (t : X) in Set.Icc x y, f t ∂μ = ∫ (t : X) in Set.Ioc x y, f t ∂μ
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.exists : ∀ {V : Type u} {G : SimpleGraph V} {p : G.ConnectedComponent → Prop}, (∃ c, p c) ↔ ∃ v, p (G.connectedComponentMk v)
-- Mathlib.Tactic.MkIffOfInductiveProp
/-- `compactRelation bs as_ps`: Produce a relation of the form:
```lean
R := fun as ↦ ∃ bs, ⋀_i a_i = p_i[bs]
```
This relation is user-visible, so we compact it by removing each `b_j` where a `p_i = b_j`, and
hence `a_i = b_j`. We need to take care when there are `p_i` and `p_j` with `p_i = p_j = b_k`.
 -/
Mathlib.Tactic.MkIff.compactRelation : List Lean.Expr →
  List (Lean.Expr × Lean.Expr) → List (Option Lean.Expr) × List (Lean.Expr × Lean.Expr) × (Lean.Expr → Lean.Expr)
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Unitization.unitsFstOne_val_val_fst : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (x : ↥(Unitization.unitsFstOne R A)), (↑↑x).toProd.1 = 1
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.comp_apply : ∀ {X Y Z : FintypeCat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X.obj),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsSymm.isRefl : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M}, B.IsSymm → B.IsRefl
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.homMk_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Under X}
  (f : U.right ⟶ V.right)
  (w : autoParam (CategoryTheory.CategoryStruct.comp U.hom f = V.hom) CategoryTheory.Under.homMk._auto_1),
  (CategoryTheory.Under.homMk f w).right = f
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.continuousAt_coe_iff : ∀ {α : Type u_4} [inst : TopologicalSpace α] {x : NNReal} {f : ENNReal → α},
  ContinuousAt f ↑x ↔ ContinuousAt (f ∘ ENNReal.ofNNReal) x
-- Mathlib.Computability.EpsilonNFA
εNFA.IsPath.cons : ∀ {α : Type u} {σ : Type v} {M : εNFA α σ} (t s u : σ) (a : Option α) (x : List (Option α)),
  t ∈ M.step s a → M.IsPath t u x → M.IsPath s u (a :: x)
-- Mathlib.Data.Fintype.Sets
/-- `finset% t` elaborates `t` as a `Finset`.
If `t` is a `Set`, then inserts `Set.toFinset`.
Does not make use of the expected type; useful for big operators over finsets.
```
#check finset% Finset.range 2 -- Finset Nat
#check finset% (Set.univ : Set Bool) -- Finset Bool
```
 -/
finsetStx : Lean.ParserDescr
-- Mathlib.Topology.Maps.Proper.Basic
/-- A constant map to a T₁ space is proper if and only if its domain is compact.  -/
isProperMap_const_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T1Space Y] (y : Y),
  (IsProperMap fun x => y) ↔ CompactSpace X
-- Init.Data.UInt.Lemmas
UInt16.toNat_ofNatClamp_of_le : ∀ {n : ℕ}, UInt16.size ≤ n → (UInt16.ofNatClamp n).toNat = UInt16.size - 1
-- Lean.Compiler.ExternAttr
Lean.ExternEntry.adhoc : Lean.Name → Lean.ExternEntry
-- Mathlib.Topology.Category.CompHausLike.Basic
/-- If `P` implies `P'`, then the functor from `CompHausLike P` to `CompHausLike P'` is fully
faithful.  -/
CompHausLike.fullyFaithfulToCompHausLike : {P P' : TopCat → Prop} →
  (h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop) → (CompHausLike.toCompHausLike h).FullyFaithful
-- Mathlib.CategoryTheory.Shift.Pullback
CategoryTheory.pullbackShiftFunctorZero'_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] [inst_3 : CategoryTheory.HasShift C B] (φ : A →+ B) (X : CategoryTheory.PullbackShift C φ),
  (CategoryTheory.shiftFunctorZero (CategoryTheory.PullbackShift C φ) A).hom.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.pullbackShiftIso C φ 0 (φ 0) ⋯).hom.app X)
      ((CategoryTheory.shiftFunctorZero' C (φ 0) ⋯).hom.app X)
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.hrecOn₂.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {cM : AddCon M} {cN : AddCon N}
  {φ : cM.Quotient → cN.Quotient → Sort u_4} (a : cM.Quotient) (b : cN.Quotient) (f : (x : M) → (y : N) → φ ↑x ↑y)
  (h : ∀ (x : M) (y : N) (x' : M) (y' : N), cM x x' → cN y y' → f x y ≍ f x' y'),
  AddCon.hrecOn₂ a b f h = Quotient.hrecOn₂' a b f h
-- Mathlib.Topology.Order.T5
Set.ordT5Nhd_mem_nhdsSet : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {s t : Set X},
  Disjoint s (closure t) → s.ordT5Nhd t ∈ nhdsSet s
-- Mathlib.Topology.Algebra.Module.Cardinality
/-- In a nontrivial topological vector space over a complete nontrivially normed field, any
countable set has dense complement.  -/
Set.Countable.dense_compl : ∀ {E : Type u} (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [Nontrivial E] [inst_5 : TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {s : Set E},
  s.Countable → Dense sᶜ
-- Mathlib.Order.BoundedOrder.Basic
Prod.instBot.eq_1 : ∀ (α : Type u) (β : Type v) [inst : Bot α] [inst_1 : Bot β], Prod.instBot α β = { bot := (⊥, ⊥) }
-- Init.Data.SInt.Lemmas
Int8.toNatClampNeg_toISize : ∀ (x : Int8), x.toISize.toNatClampNeg = x.toNatClampNeg
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_wcovBy_toIcoDiv : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocDiv hp a b ⩿ toIcoDiv hp a b
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- A separating family of seminorms induces a T₁ topology.  -/
WithSeminorms.T1_of_separating : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {p : SeminormFamily 𝕜 E ι},
  WithSeminorms p → (∀ (x : E), x ≠ 0 → ∃ i, (p i) x ≠ 0) → T1Space E
-- Mathlib.CategoryTheory.Category.Cat.Limit
CategoryTheory.Cat.HasLimits.id_def : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat)
  (X : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)),
  CategoryTheory.CategoryStruct.id X =
    CategoryTheory.Limits.Types.Limit.mk (CategoryTheory.Cat.HasLimits.homDiagram X X)
      (fun x =>
        CategoryTheory.CategoryStruct.id
          ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Cat.objects) x))
            X))
      ⋯
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue : Type
-- Mathlib.Algebra.Divisibility.Units
isRelPrime_mul_unit_left_right : ∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α}, IsUnit x → (IsRelPrime y (x * z) ↔ IsRelPrime y z)
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.instMulZeroClass : {α : Type u_1} → [DecidableEq α] → [MulZeroClass α] → MulZeroClass (WithTop α)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_reflectsPullback_of_right : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f],
  CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan g f)
    AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.continuous_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β], Continuous fun x => x.1 ×ˢ x.2
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.CertificateOracle.mk.sizeOf_spec : ∀ (produceCertificate : List Mathlib.Tactic.Linarith.Comp → ℕ → Lean.MetaM (Std.HashMap ℕ ℕ)),
  sizeOf { produceCertificate := produceCertificate } = 1
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.coprod.eq_1 : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddCommMonoid P] (f : M →+ P) (g : N →+ P),
  f.coprod g = f.comp (AddMonoidHom.fst M N) + g.comp (AddMonoidHom.snd M N)
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.preservesLimit_of_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} {B : Type u₄} [inst_4 : CategoryTheory.Category.{v₄, u₄} B]
  {H : CategoryTheory.Functor E B} [CategoryTheory.Limits.PreservesLimit (F.comp G) H],
  CategoryTheory.Limits.PreservesLimit G H
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.map_equiv_fun : ∀ {Ω : Type u_1} {E : Type u_2} {F : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [inst_3 : NormedSpace ℝ E]
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace ℝ F] [inst_6 : MeasurableSpace F] [BorelSpace F],
  ProbabilityTheory.HasGaussianLaw X P → ∀ (L : E ≃L[ℝ] F), ProbabilityTheory.HasGaussianLaw (fun ω => L (X ω)) P
-- Mathlib.RepresentationTheory.Intertwining
/-- An intertwining map is the same thing as a linear map over the group ring.  -/
Representation.IntertwiningMap.equivLinearMapAsModule : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : CommSemiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    (ρ : Representation A G V) →
                      (σ : Representation A G W) → ρ.IntertwiningMap σ ≃ₗ[A] ρ.asModule →ₗ[MonoidAlgebra A G] σ.asModule
-- Mathlib.RingTheory.Valuation.Basic
Valuation.isNontrivial_of_isEquiv : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v : Valuation R Γ₀} {v' : Valuation R Γ'₀},
  v.IsEquiv v' → v.IsNontrivial → v'.IsNontrivial
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U)
  (f : ↑(X.presheaf.obj (Opposite.op U))),
  (TopologicalSpace.Opens.map hU.fromSpec.base).obj (X.basicOpen f) = PrimeSpectrum.basicOpen f
-- Mathlib.LinearAlgebra.Matrix.Echelon.Basic
/-- `c` is the leading position of row `i`.  -/
Matrix.IsLeadingEntry : {m : Type u_1} → {n : Type u_2} → {R : Type v} → [Zero R] → [LT n] → Matrix m n R → m → n → Prop
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_eq_natDegree : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {p : Polynomial R} {q : Polynomial S},
  p.degree = q.degree → p.natDegree = q.natDegree
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.CountablySeparated.mono : ∀ {α : Type u_1} {m m' : MeasurableSpace α} [hsep : MeasurableSpace.CountablySeparated α],
  m ≤ m' → MeasurableSpace.CountablySeparated α
-- Mathlib.Logic.Basic
or_congr_right' : ∀ {a b c : Prop}, (¬a → (b ↔ c)) → (a ∨ b ↔ a ∨ c)
-- Mathlib.Data.Vector.Basic
/-- Two `v w : Vector α n` are equal iff they are equal at every single index.  -/
List.Vector.ext : ∀ {α : Type u_1} {n : ℕ} {v w : List.Vector α n}, (∀ (m : Fin n), v.get m = w.get m) → v = w
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffWithinAt_iff_target_of_mem_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M}
  {y : M'} {n : WithTop ℕ∞} [IsManifold I' n M'],
  f x ∈ (chartAt H' y).source →
    (ContMDiffWithinAt I I' n f s x ↔
      ContinuousWithinAt f s x ∧ ContMDiffWithinAt I (modelWithCornersSelf 𝕜 E') n (↑(extChartAt I' y) ∘ f) s x)
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.mem_factors'_of_dvd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a p : α},
  a ≠ 0 → ∀ (hp : Irreducible p), p ∣ a → ⟨Associates.mk p, ⋯⟩ ∈ Associates.factors' a
-- Mathlib.Topology.Connected.Basic
IsPreconnected.preimage_of_isClosedMap : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set β},
  IsPreconnected s → ∀ {f : α → β}, Function.Injective f → IsClosedMap f → s ⊆ Set.range f → IsPreconnected (f ⁻¹' s)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.comap_iInf : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_1}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] {ι : Sort u_2} (f : F)
  (s : ι → NonUnitalSubsemiring S), NonUnitalSubsemiring.comap f (iInf s) = ⨅ i, NonUnitalSubsemiring.comap f (s i)