mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.EqToHom
/-- A variant on `eqToHom_naturality` that helps Lean identify the families `f` and `g`.  -/
CategoryTheory.eqToHom_iso_hom_naturality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ≅ g b)
  {j j' : β} (w : j = j') {Z : C} (h : g j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (z j).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (z j').hom h)
-- Mathlib.Algebra.Group.Conj
IsConj.trans : ∀ {α : Type u} [inst : Monoid α] {a b c : α}, IsConj a b → IsConj b c → IsConj a c
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.List.forIn'_cons.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.yield b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_2 b
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T T' T'' : D} {S : CategoryTheory.Functor C D} {f : T ⟶ T'} {f' : T' ⟶ T''}
  {h : CategoryTheory.CostructuredArrow S T},
  (CategoryTheory.CostructuredArrow.map (CategoryTheory.CategoryStruct.comp f f')).obj h =
    (CategoryTheory.CostructuredArrow.map f').obj ((CategoryTheory.CostructuredArrow.map f).obj h)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
/-- The nonsingular condition underlying a nonsingular Jacobian point on `W`.  -/
WeierstrassCurve.Jacobian.Point.nonsingular : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (self : W'.Point), W'.NonsingularLift self.point
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, returning `fallback` if no such pair exists.
 -/
Std.TreeMap.Raw.getEntryLED : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → α × β → α × β
-- Init.Data.String.Lemmas.IsEmpty
String.ne_empty_of_lt : ∀ {s : String} {p q : s.Pos}, p < q → s ≠ ""
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than or equal to the
given key, panicking if no such key exists.
 -/
Std.ExtDTreeMap.getKeyGE! : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtDTreeMap α β cmp → α → α
-- Mathlib.CategoryTheory.ExtremalEpi
CategoryTheory.instExtremalEpiOfStrongEpi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.StrongEpi f],
  CategoryTheory.ExtremalEpi f
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_sub_nsmul' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℕ), toIcoMod hp (a - m • p) b = toIcoMod hp a b - m • p
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List α} {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
      k ∈ l → (Std.ExtTreeMap.unitOfList l cmp).getKeyD k' fallback = k
-- Mathlib.Data.Finset.Sym
Finset.mem_sym2_iff : ∀ {α : Type u_1} {s : Finset α} {m : Sym2 α}, m ∈ s.sym2 ↔ ∀ a ∈ m, a ∈ s
-- Mathlib.Algebra.BigOperators.Ring.Finset
Fintype.prod_add : ∀ {ι : Type u_5} {R : Type u_7} [inst : Fintype ι] [inst_1 : CommSemiring R] [inst_2 : DecidableEq ι] (f g : ι → R),
  ∏ a, (f a + g a) = ∑ t, (∏ a ∈ t, f a) * ∏ a ∈ tᶜ, g a
-- Lean.Server.Completion.CompletionUtils
Lean.Server.Completion.HoverInfo.inside : ℕ → Lean.Server.Completion.HoverInfo
-- Mathlib.Algebra.Order.IsBotOne
/-- **Alias** of `eq_zero_of_nonpos`.

---

**Alias** of the forward direction of `nonpos_iff_eq_zero`. -/
LE.le.eq_zero : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : Zero α] [IsBotZeroClass α], a ≤ 0 → a = 0
-- Mathlib.Algebra.Homology.Embedding.Extend
_private.Mathlib.Algebra.Homology.Embedding.Extend.0.HomologicalComplex.extend.d.match_1.eq_1 : ∀ {ι : Type u_1} (motive : Option ι → Option ι → Sort u_2) (x : Option ι) (h_1 : (x : Option ι) → motive none x)
  (h_2 : (i j : ι) → motive (some i) (some j)) (h_3 : (val : ι) → motive (some val) none),
  (match none, x with
    | none, x => h_1 x
    | some i, some j => h_2 i j
    | some val, none => h_3 val) =
    h_1 x
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.Sigma.ι_π_of_ne : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {β : Type w} [inst_2 : DecidableEq β] (f : β → C) [inst_3 : CategoryTheory.Limits.HasCoproduct f] {b c : β},
  b ≠ c → CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) (CategoryTheory.Limits.Sigma.π f c) = 0
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsNonloop.exists_mem_isCocircuit : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsNonloop e → ∃ K, M.IsCocircuit K ∧ e ∈ K
-- Mathlib.CategoryTheory.Abelian.Transfer
CategoryTheory.AsSmall.preadditive : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Preadditive C] → CategoryTheory.Preadditive (CategoryTheory.AsSmall C)
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.inclusion.eq_1 : ∀ {R : Type u} [inst : NonAssocRing R] {S T : Subring R} (h : S ≤ T), Subring.inclusion h = S.subtype.codRestrict T ⋯
-- Lean.Elab.Tactic.Omega.Core
/-- The "irrelevant" facts which do not involve the target variable.  -/
Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData.irrelevant : Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData → List Lean.Elab.Tactic.Omega.Fact
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.ContainsIdentities.inf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.MorphismProperty C}
  [P.ContainsIdentities] [Q.ContainsIdentities], (P ⊓ Q).ContainsIdentities
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix_comp : ∀ {R : Type u_1} [inst : CommSemiring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n]
  [inst_2 : DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : Module R M₁] [inst_6 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂)
  [inst_7 : Fintype m] {M₃ : Type u_7} [inst_8 : AddCommMonoid M₃] [inst_9 : Module R M₃] (v₃ : Module.Basis l R M₃)
  [inst_10 : Finite l] [inst_11 : DecidableEq m] (f : M₂ →ₗ[R] M₃) (g : M₁ →ₗ[R] M₂),
  (LinearMap.toMatrix v₁ v₃) (f ∘ₗ g) = (LinearMap.toMatrix v₂ v₃) f * (LinearMap.toMatrix v₁ v₂) g
-- Mathlib.CategoryTheory.Preadditive.Projective.Preserves
/-- See `Functor.projective_obj_of_projective` for a variant taking `Projective X` as an explicit
argument.  -/
CategoryTheory.Functor.projective_obj : ∀ {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.PreservesProjectiveObjects] (X : C) [CategoryTheory.Projective X],
  CategoryTheory.Projective (F.obj X)
-- Mathlib.NumberTheory.Niven
IsIntegral.ratCast_iff : ∀ {α : Type u_1} [inst : DivisionRing α] [CharZero α] {q : ℚ}, IsIntegral ℤ ↑q ↔ IsIntegral ℤ q
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
/-- The composition of two strong epimorphisms is a strong epimorphism.  -/
CategoryTheory.strongEpi_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R)
  [CategoryTheory.StrongEpi f] [CategoryTheory.StrongEpi g],
  CategoryTheory.StrongEpi (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Analysis.Fourier.AddCircle
MeasureTheory.Integrable.fourier_smul : ∀ {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E]
  {f : AddCircle T → E},
  MeasureTheory.Integrable f AddCircle.haarAddCircle →
    ∀ (n : ℤ), MeasureTheory.Integrable (fun t => (fourier n) t • f t) AddCircle.haarAddCircle
-- Mathlib.Order.Preorder.Finite
Set.Finite.exists_maximalFor : ∀ {ι : Type u_1} {α : Type u_2} [inst : LE α] [IsTrans α LE.le] (f : ι → α) (s : Set ι),
  s.Finite → s.Nonempty → ∃ i, MaximalFor (fun x => x ∈ s) f i
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.erase_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {k : α}, ∅.erase k = ∅
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_monomial : ∀ {R : Type u} {a : R} {n : ℕ} [inst : Semiring R], a ≠ 0 → ((Polynomial.monomial n) a).natTrailingDegree = n
-- Mathlib.Logic.Equiv.Fintype
Equiv.Perm.viaFintypeEmbedding_apply_mem_range : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] (e : Equiv.Perm α) (f : α ↪ β) {b : β}
  (h : b ∈ Set.range ⇑f), (e.viaFintypeEmbedding f) b = f (e (f.invOfMemRange ⟨b, h⟩))
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instNormedSpaceOfNormedAlgebra : {α : Type u_1} →
  {𝕜 : Type u_2} →
    {R : Type u_3} →
      [inst : TopologicalSpace α] →
        [inst_1 : CompactSpace α] →
          [inst_2 : Zero α] →
            [inst_3 : NormedField 𝕜] →
              [inst_4 : NormedCommRing R] → [NormedAlgebra 𝕜 R] → NormedSpace 𝕜 (ContinuousMapZero α R)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Functor.prod_obj : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C D)
  (X : A × C), (F.prod G).obj X = (F.obj X.1, G.obj X.2)
-- Init.Data.BitVec.Basic
BitVec.instHShiftRight : {m n : ℕ} → HShiftRight (BitVec m) (BitVec n) (BitVec m)
-- Mathlib.Order.Interval.Finset.Basic
Finset.uIcc_subset_uIcc_right : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] {a b x : α},
  x ∈ Finset.uIcc a b → Finset.uIcc x b ⊆ Finset.uIcc a b
-- Std.Time.DateTime.Timestamp
Std.Time.instDecidableEqTimestamp.decEq : (x x_1 : Std.Time.Timestamp) → Decidable (x = x_1)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- The edge set of `G'` consists of a subset of edges of `G`.  -/
SimpleGraph.Subgraph.edgeSet : {V : Type u} → {G : SimpleGraph V} → G.Subgraph → Set (Sym2 V)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.mem_brange : ∀ {α : Type u_1} {o : Ordinal.{u_3}} {f : (a : Ordinal.{u_3}) → a < o → α} {a : α},
  a ∈ o.brange f ↔ ∃ i, ∃ (hi : i < o), f i hi = a
-- Init.PropLemmas
Decidable.not_and_iff_not_or_not' : ∀ {b a : Prop} [Decidable b], ¬(a ∧ b) ↔ ¬a ∨ ¬b
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
CategoryTheory.Functor.Monoidal.instPreservesColimitsOfShapeTensorLeftOfHasColimitsOfShape : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.CartesianMonoidalCategory C] {K : Type u_5}
  [inst_3 : CategoryTheory.Category.{v_5, u_5} K] [CategoryTheory.Limits.HasColimitsOfShape K C]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape K (CategoryTheory.MonoidalCategory.tensorLeft X)]
  {F : CategoryTheory.Functor J C},
  CategoryTheory.Limits.PreservesColimitsOfShape K (CategoryTheory.MonoidalCategory.tensorLeft F)
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
/-- For any `a` and `b`, `a ≤ a + b`  -/
CanonicallyOrderedAdd.le_add_self : ∀ {α : Type u_1} {inst : Add α} {inst_1 : LE α} [self : CanonicallyOrderedAdd α] (a b : α), a ≤ b + a
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey_alter_eq_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : Option β → Option β} {he : t.alter k f ≠ ∅},
  (t.alter k f).maxKey he = k ↔ (f t[k]?).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Lean.Attributes
Lean.AttributeApplicationTime.beforeElaboration.sizeOf_spec : sizeOf Lean.AttributeApplicationTime.beforeElaboration = 1
-- Std.Async.System
Std.Async.System.CPUInfo.mk.injEq : ∀ (model : String) (speed : ℕ) (times : Std.Async.System.CPUTimes) (model_1 : String) (speed_1 : ℕ)
  (times_1 : Std.Async.System.CPUTimes),
  ({ model := model, speed := speed, times := times } = { model := model_1, speed := speed_1, times := times_1 }) =
    (model = model_1 ∧ speed = speed_1 ∧ times = times_1)
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_hom_app_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'}
  {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)}
  (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.CategoryStruct.comp (f' j) p)
  {S'' : C} {q : S'' ⟶ S'} {ι'' : Type t''} {X'' : ι'' → C} {f'' : (k : ι'') → X'' k ⟶ S''} {β : ι'' → ι'}
  {q' : (k : ι'') → X'' k ⟶ X' (β k)}
  (w' :
    ∀ (k : ι''), CategoryTheory.CategoryStruct.comp (q' k) (f' (β k)) = CategoryTheory.CategoryStruct.comp (f'' k) q)
  (r : S'' ⟶ S) {r' : (k : ι'') → X'' k ⟶ X (α (β k))}
  (hr :
    autoParam (CategoryTheory.CategoryStruct.comp q p = r)
      CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso._auto_1)
  (hr' :
    autoParam (∀ (k : ι''), CategoryTheory.CategoryStruct.comp (q' k) (p' (β k)) = r' k)
      CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso._auto_3)
  (X_1 : F.DescentData f) (i : ι''),
  ((CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso F w w' r hr hr').hom.app X_1).hom i =
    (F.mapComp' (p' (β i)).op.toLoc (q' i).op.toLoc (r' i).op.toLoc ⋯).inv.toNatTrans.app (X_1.obj (α (β i)))
-- Mathlib.Analysis.Calculus.FDeriv.Norm
fderiv_norm_smul_neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {x : E} {t : ℝ},
  t < 0 → fderiv ℝ (fun x => ‖x‖) (t • x) = -fderiv ℝ (fun x => ‖x‖) x
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_eq_getD_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {a fallback : α},
  t.getD a fallback = (t.get? a).getD fallback
-- Mathlib.RingTheory.Algebraic.Defs
Algebra.IsAlgebraic.mk : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A],
  (∀ (x : A), IsAlgebraic R x) → Algebra.IsAlgebraic R A
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Icc_pred_right_eq_Ico_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : PredOrder α] {b : α},
  ¬IsMin b → ∀ (a : α), Finset.Icc a (Order.pred b) = Finset.Ico a b
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.toEnd' : ∀ (it : String.Legacy.Iterator), String.Legacy.Iterator.ValidFor it.s.toList.reverse [] it.toEnd
-- Mathlib.Algebra.Module.Injective
Module.Baer.of_injective : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] [Small.{v, u} R],
  Module.Injective R Q → Module.Baer R Q
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiff.swap : ∀ {𝕜 : 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] {M' : Type u_16} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {n : WithTop ℕ∞}, ContMDiff I I n Sum.swap
-- Mathlib.NumberTheory.PythagoreanTriples
PythagoreanTriple.isClassified_of_isPrimitiveClassified : ∀ {x y z : ℤ} (h : PythagoreanTriple x y z), h.IsPrimitiveClassified → h.IsClassified
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : SizeOf α] [inst_3 : SizeOf β]
  (toOrderHom : α →o β)
  (exists_map_eq_of_map_le' : ∀ ⦃a : α⦄ ⦃b : β⦄, toOrderHom.toFun a ≤ b → ∃ c, a ≤ c ∧ toOrderHom.toFun c = b),
  sizeOf { toOrderHom := toOrderHom, exists_map_eq_of_map_le' := exists_map_eq_of_map_le' } = 1 + sizeOf toOrderHom
-- Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
/-- A consequence of the special adjoint functor theorem: if `C` is complete, well-powered and
has a coseparator, then it is cocomplete.  -/
CategoryTheory.Limits.hasColimits_of_hasLimits_of_hasCoseparator : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C]
  [CategoryTheory.HasCoseparator C] [CategoryTheory.WellPowered.{v, v, u} C], CategoryTheory.Limits.HasColimits C
-- Mathlib.SetTheory.Lists
Lists'.Subset.refl : ∀ {α : Type u_1} {l : Lists' α true}, l ⊆ l
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapTrifunctorMapIso_inv : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  {F F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))} (e : F ≅ F')
  (I₁ : Type u_7) (I₂ : Type u_8) (I₃ : Type u_9),
  (CategoryTheory.GradedObject.mapTrifunctorMapIso e I₁ I₂ I₃).inv =
    CategoryTheory.GradedObject.mapTrifunctorMapNatTrans e.inv I₁ I₂ I₃
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.norm_add_le : ∀ {α : Type u_1} [inst : DecidableEq α] (x y : FreeAddGroup α), (x + y).norm ≤ x.norm + y.norm
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.mk_dvd_mk : ∀ {M : Type u_1} [inst : CommMonoid M] {a b : M}, Associates.mk a ∣ Associates.mk b ↔ a ∣ b
-- Mathlib.Topology.Algebra.Module.LinearPMap
LinearPMap.HasCore.le_domain : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R] [inst_10 : ContinuousSMul R E]
  [inst_11 : ContinuousSMul R F] {f : E →ₗ.[R] F} {S : Submodule R E}, f.HasCore S → S ≤ f.domain
-- Mathlib.RingTheory.AdicCompletion.Exactness
/-- Adic completion preserves injectivity of finite modules over a Noetherian ring.  -/
AdicCompletion.map_injective : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) {M : Type u} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u} [inst_3 : AddCommGroup N] [inst_4 : Module R N] [IsNoetherianRing R] [Module.Finite R N] {f : M →ₗ[R] N},
  Function.Injective ⇑f → Function.Injective ⇑(AdicCompletion.map I f)
-- Lean.Level
Lean.Level.PP.Result.maxNode : List Lean.Level.PP.Result → Lean.Level.PP.Result
-- Mathlib.Algebra.Lie.Weights.Linear
LieModule.trace_comp_toEnd_genWeightSpace_eq : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] [IsDomain R]
  [IsPrincipalIdealRing R] [Module.Free R M] [Module.Finite R M] [inst_11 : LieRing.IsNilpotent L] (χ : L → R),
  ⇑(LinearMap.trace R ↥(LieModule.genWeightSpace M χ) ∘ₗ ↑(LieModule.toEnd R L ↥(LieModule.genWeightSpace M χ))) =
    Module.finrank R ↥(LieModule.genWeightSpace M χ) • χ
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
/-- If a measurable space is countably generated and separates points, it arises as
the Borel sets of some second countable t4 topology (i.e. a separable metrizable one).  -/
exists_borelSpace_of_countablyGenerated_of_separatesPoints : ∀ (α : Type u_5) [m : MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] [MeasurableSpace.SeparatesPoints α],
  ∃ x, SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.instVAddCommClass_1 : ∀ {R : Type u_1} {M : Type u_3} {X : Type u_4} [inst : AddMonoid M] {S : AddSubmonoid M}
  [inst_1 : AddOreLocalization.AddOreSet S] [inst_2 : AddAction M X] [inst_3 : VAdd R X] [inst_4 : VAdd R M]
  [inst_5 : VAddAssocClass R M M] [inst_6 : VAddAssocClass R M X] [VAddCommClass R M M],
  VAddCommClass R (AddOreLocalization S M) (AddOreLocalization S X)
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.smulInvariantMeasure_map_smul : ∀ {M : Type uM} {N : Type uN} {α : Type uα} [inst : MeasurableSpace α] [inst_1 : SMul M α] [inst_2 : SMul N α]
  [SMulCommClass N M α] [MeasurableConstSMul M α] [MeasurableConstSMul N α] (μ : MeasureTheory.Measure α)
  [MeasureTheory.SMulInvariantMeasure M α μ] (n : N),
  MeasureTheory.SMulInvariantMeasure M α (MeasureTheory.Measure.map (fun x => n • x) μ)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
/-- If `f g : α → ℝ≥0∞` are two functions and one of them is (a.e.) measurable, then the Lebesgue
integral of `f + g` equals the sum of integrals. This lemma assumes that `g` is integrable, see also
`MeasureTheory.lintegral_add_left` and primed versions of these lemmas.  -/
MeasureTheory.lintegral_add_right : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) {g : α → ENNReal},
  Measurable g → ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
-- Mathlib.Data.Part
Part.some_mod_some : ∀ {α : Type u_1} [inst : Mod α] (a b : α), Part.some a % Part.some b = Part.some (a % b)
-- Mathlib.LinearAlgebra.Matrix.Permutation
Matrix.permMatrix_one : ∀ {n : Type u_1} {R : Type u_2} [inst : DecidableEq n] [inst_1 : Zero R] [inst_2 : One R], Equiv.Perm.permMatrix R 1 = 1
-- Mathlib.Data.FinEnum
/-- create a `FinEnum` instance from an exhaustive list without duplicates  -/
FinEnum.ofNodupList : {α : Type u} → [DecidableEq α] → (xs : List α) → (∀ (x : α), x ∈ xs) → xs.Nodup → FinEnum α
-- Mathlib.NumberTheory.ADEInequality
ADEInequality.lt_four : ∀ {q r : ℕ+}, q ≤ r → 1 < ADEInequality.sumInv {2, q, r} → q < 4
-- Mathlib.Computability.TuringMachine.Tape
_private.Mathlib.Computability.TuringMachine.Tape.0.Turing.Tape.nth.match_1.eq_2 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive (Int.ofNat n.succ))
  (h_3 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.ofNat n.succ with
    | 0 => h_1 ()
    | Int.ofNat n.succ => h_2 n
    | Int.negSucc n => h_3 n) =
    h_2 n
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.coe_finset_sup : ∀ {ι : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] (s : Finset ι) (U : ι → TopologicalSpace.Clopens α),
  ↑(s.sup U) = ⋃ i ∈ s, ↑(U i)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.reflexion_comp_left : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion
    CategoryTheory.Limits.WalkingReflexivePair.Hom.left =
  CategoryTheory.CategoryStruct.id CategoryTheory.Limits.WalkingReflexivePair.zero
-- Mathlib.Order.Hom.Order
OrderHom.coe_inf : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : SemilatticeInf β] (f g : α →o β), ⇑(f ⊓ g) = ⇑f ⊓ ⇑g
-- Mathlib.Analysis.Convex.Visible
/-- If `s` is a closed set of dimension `d` and `x` is a point outside of its convex hull,
then `x` sees at least `d` points of the convex hull of `s` that actually lie in `s`.  -/
rank_le_card_isVisible : ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] {s : Set V} {x : V} [inst_2 : TopologicalSpace V]
  [IsTopologicalAddGroup V] [ContinuousSMul ℝ V],
  IsClosed ((convexHull ℝ) s) →
    x ∉ (convexHull ℝ) s →
      Module.rank ℝ ↥(Submodule.span ℝ (-x +ᵥ s)) ≤ Cardinal.mk ↑{y | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x y}